43158

1 
(* Author: Tobias Nipkow *)


2 


3 
header "Hoare Logic"


4 


5 
theory Hoare imports Big_Step begin


6 


7 
subsection "Hoare Logic for Partial Correctness"


8 


9 
type_synonym assn = "state \<Rightarrow> bool"


10 

45212

11 
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"

43158

12 
("_[_'/_]" [1000,0,0] 999)


13 
where "s[a/x] == s(x := aval a s)"


14 


15 
inductive


16 
hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)


17 
where


18 
Skip: "\<turnstile> {P} SKIP {P}" 


19 


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


21 


22 
Semi: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q}; \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>


23 
\<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}" 


24 


25 
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>


26 
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" 


27 


28 
While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>


29 
\<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}" 


30 


31 
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>


32 
\<Longrightarrow> \<turnstile> {P'} c {Q'}"


33 


34 
lemmas [simp] = hoare.Skip hoare.Assign hoare.Semi If


35 


36 
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Semi hoare.If


37 


38 
lemma strengthen_pre:


39 
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"


40 
by (blast intro: conseq)


41 


42 
lemma weaken_post:


43 
"\<lbrakk> \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile> {P} c {Q'}"


44 
by (blast intro: conseq)


45 


46 
text{* The assignment and While rule are awkward to use in actual proofs


47 
because their pre and postcondition are of a very special form and the actual


48 
goal would have to match this form exactly. Therefore we derive two variants


49 
with arbitrary pre and postconditions. *}


50 


51 
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"


52 
by (simp add: strengthen_pre[OF _ Assign])


53 


54 
lemma While':


55 
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"


56 
shows "\<turnstile> {P} WHILE b DO c {Q}"


57 
by(rule weaken_post[OF While[OF assms(1)] assms(2)])


58 


59 
end
