# HG changeset patch
# User blanchet
# Date 1370657839 14400
# Node ID 891e128ea08cf5f53de9f676144d970df5c629e0
# Parent  40136fcb5e7a5710ebfd014797dbcdc78d1994ac# Parent  ac2fb87a12f30b571295334352c74321498da3b0
merge

diff -r 40136fcb5e7a -r 891e128ea08c src/HOL/IMP/Hoare_Total.thy
--- a/src/HOL/IMP/Hoare_Total.thy	Fri Jun 07 17:24:29 2013 +0100
+++ b/src/HOL/IMP/Hoare_Total.thy	Fri Jun 07 22:17:19 2013 -0400
@@ -32,7 +32,7 @@
 
 While:
   "(\<And>n::nat.
-    \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'. T s n' \<and> n' < n)})
+    \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'<n. T s n')})
    \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"  |
 
 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
@@ -177,7 +177,7 @@
     unfolding wpt_def by (metis WHILE_Its)
   moreover
   { fix n
-    let ?R = "\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)"
+    let ?R = "\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
     { fix s t assume "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t"
       from `bval b s` and `(?w, s) \<Rightarrow> t` obtain s' where
         "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto
diff -r 40136fcb5e7a -r 891e128ea08c src/HOL/IMP/VCG.thy
--- a/src/HOL/IMP/VCG.thy	Fri Jun 07 17:24:29 2013 +0100
+++ b/src/HOL/IMP/VCG.thy	Fri Jun 07 22:17:19 2013 -0400
@@ -20,104 +20,104 @@
 fun strip :: "acom \<Rightarrow> com" where
 "strip SKIP = com.SKIP" |
 "strip (x ::= a) = (x ::= a)" |
-"strip (c\<^isub>1;; c\<^isub>2) = (strip c\<^isub>1;; strip c\<^isub>2)" |
-"strip (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
-"strip ({_} WHILE b DO c) = (WHILE b DO strip c)"
+"strip (C\<^isub>1;; C\<^isub>2) = (strip C\<^isub>1;; strip C\<^isub>2)" |
+"strip (IF b THEN C\<^isub>1 ELSE C\<^isub>2) = (IF b THEN strip C\<^isub>1 ELSE strip C\<^isub>2)" |
+"strip ({_} WHILE b DO C) = (WHILE b DO strip C)"
 
 text{* Weakest precondition from annotated commands: *}
 
 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\<^isub>1;; c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
-"pre (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
-  (\<lambda>s. if bval b s then pre c\<^isub>1 Q s else pre c\<^isub>2 Q s)" |
-"pre ({I} WHILE b DO c) Q = I"
+"pre (C\<^isub>1;; C\<^isub>2) Q = pre C\<^isub>1 (pre C\<^isub>2 Q)" |
+"pre (IF b THEN C\<^isub>1 ELSE C\<^isub>2) Q =
+  (\<lambda>s. if bval b s then pre C\<^isub>1 Q s else pre C\<^isub>2 Q s)" |
+"pre ({I} WHILE b DO C) Q = I"
 
 text{* Verification condition: *}
 
 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
 "vc SKIP Q = (\<lambda>s. True)" |
 "vc (x ::= a) Q = (\<lambda>s. True)" |
-"vc (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 (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" |
-"vc ({I} WHILE b DO c) Q =
+"vc (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 (IF b THEN C\<^isub>1 ELSE C\<^isub>2) Q = (\<lambda>s. vc C\<^isub>1 Q s \<and> vc C\<^isub>2 Q s)" |
+"vc ({I} WHILE b DO 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)"
+       (I s \<and> bval b s \<longrightarrow> pre C I s) \<and>
+       vc C I s)"
 
 
 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)
+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
   proof(simp, rule While')
-    from `\<forall>s. vc (Awhile I b c) Q s`
-    have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
-         pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
-    have "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc])
-    with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip c {I}"
+    from `\<forall>s. vc (Awhile I b C) Q s`
+    have vc: "\<forall>s. vc C I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
+         pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre C I s" by simp_all
+    have "\<turnstile> {pre C I} strip C {I}" by(rule Awhile.IH[OF vc])
+    with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}"
       by(rule strengthen_pre)
     show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
   qed
 qed (auto intro: hoare.conseq)
 
 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}"
+  "\<lbrakk> \<forall>s. vc C Q s; \<forall>s. P s \<longrightarrow> pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}"
 by (metis strengthen_pre vc_sound)
 
 
 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)
+  "\<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
 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')
+  "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc C P s \<Longrightarrow> vc C P' s"
+proof(induction C arbitrary: P P')
   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'")
+ "\<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")
 proof (induction rule: hoare.induct)
   case Skip
-  show ?case (is "\<exists>ac. ?C ac")
+  show ?case (is "\<exists>C. ?C C")
   proof show "?C Askip" by simp qed
 next
   case (Assign P a x)
-  show ?case (is "\<exists>ac. ?C ac")
+  show ?case (is "\<exists>C. ?C C")
   proof show "?C(Aassign x a)" by simp qed
 next
   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")
+  from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast
+  from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast
+  show ?case (is "\<exists>C. ?C C")
   proof
-    show "?C(Aseq ac1 ac2)"
+    show "?C(Aseq C1 C2)"
       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"
+  from If.IH obtain C1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q C1"
     by blast
-  from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
+  from If.IH obtain C2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q C2"
     by blast
-  show ?case (is "\<exists>ac. ?C ac")
+  show ?case (is "\<exists>C. ?C C")
   proof
-    show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp
+    show "?C(Aif b C1 C2)" using ih1 ih2 by simp
   qed
 next
   case (While P b c)
-  from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
-  show ?case (is "\<exists>ac. ?C ac")
-  proof show "?C(Awhile P b ac)" using ih by simp qed
+  from While.IH obtain C where ih: "?G (\<lambda>s. P s \<and> bval b s) c P C" by blast
+  show ?case (is "\<exists>C. ?C C")
+  proof show "?C(Awhile P b C)" using ih by simp qed
 next
   case conseq thus ?case by(fast elim!: pre_mono vc_mono)
 qed