src/HOL/IMP/VCG.thy

 (* Author: Tobias Nipkow *)
+
+subsection "Verification Condition Generation"
 
 theory VCG imports Hoare begin
 
-subsection "Verification Conditions"
+subsubsection "Annotated Commands"
 
-text\<open>Annotated commands: commands where loops are annotated with
-invariants.\<close>
+text\<open>Commands where loops are annotated with invariants.\<close>
 
 datatype acom =
   Askip                  ("SKIP") |
   Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
   Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |

 "strip (x ::= a) = (x ::= a)" |
 "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" |
 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |
 "strip ({_} WHILE b DO C) = (WHILE b DO strip C)"
 
-text\<open>Weakest precondition from annotated commands:\<close>
+subsubsection "Weeakest Precondistion and Verification Condition"
+
+text\<open>Weakest precondition:\<close>
 
 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
 "pre SKIP Q = Q" |
 "pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
 "pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" |

   ((\<forall>s. (I s \<and> bval b s \<longrightarrow> pre C I s) \<and>
         (I s \<and> \<not> bval b s \<longrightarrow> Q s)) \<and>
     vc C I)"
 
 
-text \<open>Soundness:\<close>
+subsubsection "Soundness"
 
 lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile> {pre C Q} strip C {Q}"
 proof(induction C arbitrary: Q)
   case (Awhile I b C)
   show ?case

 corollary vc_sound':
   "\<lbrakk> vc C Q; \<forall>s. P s \<longrightarrow> pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}"
 by (metis strengthen_pre vc_sound)
 
 
-text\<open>Completeness:\<close>
+subsubsection "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