src/HOL/IMP/VC.thy

 invariants. *}
 
 datatype acom =
   ASKIP |
   Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
-  Asemi   acom acom      ("_;/ _"  [60, 61] 60) |
+  Aseq   acom acom       ("_;/ _"  [60, 61] 60) |
   Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
   Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
 
 text{* Weakest precondition from annotated commands: *}
 
 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
 "pre ASKIP Q = Q" |
 "pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
-"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
+"pre (Aseq c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
 "pre (Aif b c\<^isub>1 c\<^isub>2) Q =
   (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
        (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
 "pre (Awhile I b c) Q = I"
 
 text{* Verification condition: *}
 
 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
 "vc ASKIP Q = (\<lambda>s. True)" |
 "vc (Aassign x a) Q = (\<lambda>s. True)" |
-"vc (Asemi c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
+"vc (Aseq c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
 "vc (Aif b c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" |
 "vc (Awhile I b c) Q =
   (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
        (I s \<and> bval b s \<longrightarrow> pre c I s) \<and>
        vc c I s)"

 text{* Strip annotations: *}
 
 fun strip :: "acom \<Rightarrow> com" where
 "strip ASKIP = SKIP" |
 "strip (Aassign x a) = (x::=a)" |
-"strip (Asemi c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
+"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"
 

 subsection "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 Asemi thus ?case by simp metis
+  case Aseq thus ?case by simp metis
 qed simp_all
 
 lemma vc_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
 proof(induction c arbitrary: P P')
-  case Asemi thus ?case by simp (metis pre_mono)
+  case Aseq thus ?case by simp (metis pre_mono)
 qed simp_all
 
 lemma vc_complete:
  "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. strip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
   (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")

 next
   case (Assign P a x)
   show ?case (is "\<exists>ac. ?C ac")
   proof show "?C(Aassign x a)" by simp qed
 next
-  case (Semi P c1 Q c2 R)
-  from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
-  from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
+  case (Seq P c1 Q c2 R)
+  from Seq.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
+  from Seq.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   show ?case (is "\<exists>ac. ?C ac")
   proof
-    show "?C(Asemi ac1 ac2)"
+    show "?C(Aseq ac1 ac2)"
       using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
   qed
 next
   case (If P b c1 Q c2)
   from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"

 subsection "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 (Asemi c\<^isub>1 c\<^isub>2) Q =
+"vcpre (Aseq c\<^isub>1 c\<^isub>2) Q =
   (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
        (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2
    in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |
 "vcpre (Aif b c\<^isub>1 c\<^isub>2) Q =
   (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;