src/HOL/IMP/VC.thy

-header "Verification Conditions"
+(* Author: Tobias Nipkow *)
 
 theory VC imports Hoare begin
 
-subsection "VCG via Weakest Preconditions"
+subsection "Verification Conditions"
 
 text{* Annotated commands: commands where loops are annotated with
 invariants. *}
 
 datatype acom =

 "strip (Aassign x a) = (x::=a)" |
 "strip (Aseq c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
 "strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
 "strip (Awhile I b c) = (WHILE b DO strip c)"
 
-subsection "Soundness"
+text {* Soundness: *}
 
 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}"
 proof(induction c arbitrary: Q)
   case (Awhile I b c)
   show ?case

 corollary vc_sound':
   "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}"
 by (metis strengthen_pre vc_sound)
 
 
-subsection "Completeness"
+text{* Completeness: *}
 
 lemma pre_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
 proof (induction c arbitrary: P P' s)
   case Aseq thus ?case by simp metis

 next
   case conseq thus ?case by(fast elim!: pre_mono vc_mono)
 qed
 
 
-subsection "An Optimization"
+text{* An Optimization: *}
 
 fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
 "vcpre ASKIP Q = (\<lambda>s. True, Q)" |
 "vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
 "vcpre (Aseq c\<^isub>1 c\<^isub>2) Q =