Theory Hoare

theory Hoare
imports Big_Step
(* Author: Tobias Nipkow *)

header "Hoare Logic"

theory Hoare imports Big_Step begin

subsection "Hoare Logic for Partial Correctness"

type_synonym assn = "state => bool"

definition
hoare_valid :: "assn => com => assn => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile> {P}c{Q} = (∀s t. P s ∧ (c,s) => t --> Q t)"

abbreviation state_subst :: "state => aexp => vname => state"
("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

inductive
hoare :: "assn => com => assn => bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
where
Skip: "\<turnstile> {P} SKIP {P}" |

Assign: "\<turnstile> {λs. P(s[a/x])} x::=a {P}" |

Seq: "[| \<turnstile> {P} c1 {Q}; \<turnstile> {Q} c2 {R} |]
==> \<turnstile> {P} c1;;c2 {R}"
|

If: "[| \<turnstile> {λs. P s ∧ bval b s} c1 {Q}; \<turnstile> {λs. P s ∧ ¬ bval b s} c2 {Q} |]
==> \<turnstile> {P} IF b THEN c1 ELSE c2 {Q}"
|

While: "\<turnstile> {λs. P s ∧ bval b s} c {P} ==>
\<turnstile> {P} WHILE b DO c {λs. P s ∧ ¬ bval b s}"
|

conseq: "[| ∀s. P' s --> P s; \<turnstile> {P} c {Q}; ∀s. Q s --> Q' s |]
==> \<turnstile> {P'} c {Q'}"


lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If

lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If

lemma strengthen_pre:
"[| ∀s. P' s --> P s; \<turnstile> {P} c {Q} |] ==> \<turnstile> {P'} c {Q}"
by (blast intro: conseq)

lemma weaken_post:
"[| \<turnstile> {P} c {Q}; ∀s. Q s --> Q' s |] ==> \<turnstile> {P} c {Q'}"
by (blast intro: conseq)

text{* The assignment and While rule are awkward to use in actual proofs
because their pre and postcondition are of a very special form and the actual
goal would have to match this form exactly. Therefore we derive two variants
with arbitrary pre and postconditions. *}


lemma Assign': "∀s. P s --> Q(s[a/x]) ==> \<turnstile> {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

lemma While':
assumes "\<turnstile> {λs. P s ∧ bval b s} c {P}" and "∀s. P s ∧ ¬ bval b s --> Q s"
shows "\<turnstile> {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])

end