# HG changeset patch
# User nipkow
# Date 1369722575 -7200
# Node ID 014d6b3f5792d74719e5b6ba8886dc4cc4477a16
# Parent  fce4a365f2804b327ee072fb0f8b52f33842ae42
tuned

diff -r fce4a365f280 -r 014d6b3f5792 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Mon May 27 22:32:28 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue May 28 08:29:35 2013 +0200
@@ -63,26 +63,23 @@
   show ?case
   proof(rule hoare.If)
     show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}"
-    proof(rule strengthen_pre[OF _ If(1)])
+    proof(rule strengthen_pre[OF _ If.IH(1)])
       show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto
     qed
     show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}"
-    proof(rule strengthen_pre[OF _ If(2)])
+    proof(rule strengthen_pre[OF _ If.IH(2)])
       show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto
     qed
   qed
 next
   case (While b c)
   let ?w = "WHILE b DO c"
-  have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}"
-  proof(rule hoare.While)
+  show "\<turnstile> {wp ?w Q} ?w {Q}"
+  proof(rule While')
     show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
-    proof(rule strengthen_pre[OF _ While(1)])
+    proof(rule strengthen_pre[OF _ While.IH])
       show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
     qed
-  qed
-  thus ?case
-  proof(rule weaken_post)
     show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
   qed
 qed auto
diff -r fce4a365f280 -r 014d6b3f5792 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Mon May 27 22:32:28 2013 +0200
+++ b/src/HOL/IMP/VC.thy	Tue May 28 08:29:35 2013 +0200
@@ -8,7 +8,7 @@
 invariants. *}
 
 datatype acom =
-  ASKIP |
+  Askip                  ("SKIP") |
   Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
   Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
   Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
@@ -17,7 +17,7 @@
 text{* Weakest precondition from annotated commands: *}
 
 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
-"pre ASKIP Q = Q" |
+"pre Askip Q = Q" |
 "pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
 "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 =
@@ -28,7 +28,7 @@
 text{* Verification condition: *}
 
 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
-"vc ASKIP Q = (\<lambda>s. True)" |
+"vc Askip Q = (\<lambda>s. True)" |
 "vc (Aassign x a) Q = (\<lambda>s. True)" |
 "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)" |
@@ -40,7 +40,7 @@
 text{* Strip annotations: *}
 
 fun strip :: "acom \<Rightarrow> com" where
-"strip ASKIP = SKIP" |
+"strip Askip = com.SKIP" |
 "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)" |
@@ -88,7 +88,7 @@
 proof (induction rule: hoare.induct)
   case Skip
   show ?case (is "\<exists>ac. ?C ac")
-  proof show "?C ASKIP" by simp qed
+  proof show "?C Askip" by simp qed
 next
   case (Assign P a x)
   show ?case (is "\<exists>ac. ?C ac")
@@ -125,7 +125,7 @@
 text{* An Optimization: *}
 
 fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
-"vcpre ASKIP Q = (\<lambda>s. True, Q)" |
+"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 =
   (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;