# HG changeset patch
# User nipkow
# Date 1346680241 -7200
# Node ID 8ab9fb2483a909075c88d829fafcc4838b1ca5fe
# Parent  7b6beb7e99c1c3620e37b9cf495fd08aaeb9f5e7# Parent  7df19036392e97ee018db36f51c5c128e16a09bb
merged

diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/ACom.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -13,49 +13,49 @@
   SKIP 'a                           ("SKIP {_}" 61) |
   Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   Seq "('a acom)" "('a acom)"       ("_;//_"  [60, 61] 60) |
-  If bexp "('a acom)" "('a acom)" 'a
-    ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
-  While 'a bexp "('a acom)" 'a
-    ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
+  If bexp 'a "('a acom)" 'a "('a acom)" 'a
+    ("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})"  [0, 0, 0, 61, 0, 0] 61) |
+  While 'a bexp 'a "('a acom)" 'a
+    ("({_}//WHILE _/ DO ({_}/ _)//{_})"  [0, 0, 0, 61, 0] 61)
 
 fun post :: "'a acom \<Rightarrow>'a" where
 "post (SKIP {P}) = P" |
 "post (x ::= e {P}) = P" |
 "post (c1; c2) = post c2" |
-"post (IF b THEN c1 ELSE c2 {P}) = P" |
-"post ({Inv} WHILE b DO c {P}) = P"
+"post (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = P" |
+"post ({Inv} WHILE b DO {Pc} c {P}) = P"
 
 fun strip :: "'a acom \<Rightarrow> com" where
 "strip (SKIP {P}) = com.SKIP" |
 "strip (x ::= e {P}) = (x ::= e)" |
 "strip (c1;c2) = (strip c1; strip c2)" |
-"strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
-"strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)"
+"strip (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
+"strip ({Inv} WHILE b DO {Pc} c {P}) = (WHILE b DO strip c)"
 
 fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
 "anno a com.SKIP = SKIP {a}" |
 "anno a (x ::= e) = (x ::= e {a})" |
 "anno a (c1;c2) = (anno a c1; anno a c2)" |
 "anno a (IF b THEN c1 ELSE c2) =
-  (IF b THEN anno a c1 ELSE anno a c2 {a})" |
+  (IF b THEN {a} anno a c1 ELSE {a} anno a c2 {a})" |
 "anno a (WHILE b DO c) =
-  ({a} WHILE b DO anno a c {a})"
+  ({a} WHILE b DO {a} anno a c {a})"
 
 fun annos :: "'a acom \<Rightarrow> 'a list" where
 "annos (SKIP {a}) = [a]" |
 "annos (x::=e {a}) = [a]" |
 "annos (C1;C2) = annos C1 @ annos C2" |
-"annos (IF b THEN C1 ELSE C2 {a}) = a #  annos C1 @ annos C2" |
-"annos ({i} WHILE b DO C {a}) = i # a # annos C"
+"annos (IF b THEN {a1} C1 ELSE {a2} C2 {a}) = a1 # a2 #a #  annos C1 @ annos C2" |
+"annos ({i} WHILE b DO {ac} C {a}) = i # ac # a # annos C"
 
 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
 "map_acom f (SKIP {P}) = SKIP {f P}" |
 "map_acom f (x ::= e {P}) = (x ::= e {f P})" |
 "map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
-"map_acom f (IF b THEN c1 ELSE c2 {P}) =
-  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" |
-"map_acom f ({Inv} WHILE b DO c {P}) =
-  ({f Inv} WHILE b DO map_acom f c {f P})"
+"map_acom f (IF b THEN {p1} c1 ELSE {p2} c2 {P}) =
+  (IF b THEN {f p1} map_acom f c1 ELSE {f p2} map_acom f c2 {f P})" |
+"map_acom f ({Inv} WHILE b DO {p} c {P}) =
+  ({f Inv} WHILE b DO {f p} map_acom f c {f P})"
 
 
 lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
@@ -78,13 +78,14 @@
 by (cases c) auto
 
 lemma map_acom_If:
- "map_acom f c = IF b THEN c1' ELSE c2' {S'} \<longleftrightarrow>
- (\<exists>S c1 c2. c = IF b THEN c1 ELSE c2 {S} \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2' \<and> S' = f S)"
+ "map_acom f c = IF b THEN {p1'} c1' ELSE {p2'} c2' {S'} \<longleftrightarrow>
+ (\<exists>S p1 p2 c1 c2. c = IF b THEN {p1} c1 ELSE {p2} c2 {S} \<and>
+     map_acom f c1 = c1' \<and> map_acom f c2 = c2' \<and> p1' = f p1 \<and> p2' = f p2 \<and> S' = f S)"
 by (cases c) auto
 
 lemma map_acom_While:
- "map_acom f w = {I'} WHILE b DO c' {P'} \<longleftrightarrow>
- (\<exists>I P c. w = {I} WHILE b DO c {P} \<and> map_acom f c = c' \<and> I' = f I \<and> P' = f P)"
+ "map_acom f w = {I'} WHILE b DO {p'} c' {P'} \<longleftrightarrow>
+ (\<exists>I p P c. w = {I} WHILE b DO {p} c {P} \<and> map_acom f c = c' \<and> I' = f I \<and> p' = f p \<and> P' = f P)"
 by (cases w) auto
 
 
@@ -92,27 +93,26 @@
 by(induct c) simp_all
 
 lemma strip_eq_SKIP:
-  "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
-by (cases c) simp_all
+  "strip C = com.SKIP \<longleftrightarrow> (EX P. C = SKIP {P})"
+by (cases C) simp_all
 
 lemma strip_eq_Assign:
-  "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
-by (cases c) simp_all
+  "strip C = x::=e \<longleftrightarrow> (EX P. C = x::=e {P})"
+by (cases C) simp_all
 
 lemma strip_eq_Seq:
-  "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
-by (cases c) simp_all
+  "strip C = c1;c2 \<longleftrightarrow> (EX C1 C2. C = C1;C2 & strip C1 = c1 & strip C2 = c2)"
+by (cases C) simp_all
 
 lemma strip_eq_If:
-  "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow>
-  (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)"
-by (cases c) simp_all
+  "strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow>
+  (EX p1 p2 C1 C2 P. C = IF b THEN {p1} C1 ELSE {p2} C2 {P} & strip C1 = c1 & strip C2 = c2)"
+by (cases C) simp_all
 
 lemma strip_eq_While:
-  "strip c = WHILE b DO c1 \<longleftrightarrow>
-  (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)"
-by (cases c) simp_all
-
+  "strip C = WHILE b DO c1 \<longleftrightarrow>
+  (EX I p C1 P. C = {I} WHILE b DO {p} C1 {P} & strip C1 = c1)"
+by (cases C) simp_all
 
 lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}"
 by(induction C)(auto)
@@ -124,5 +124,4 @@
 
 lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
 
-
 end
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -79,10 +79,10 @@
 "le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
 "le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
 "le_acom (C1;C2) (D1;D2) = (C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)" |
-"le_acom (IF b THEN C1 ELSE C2 {S}) (IF b' THEN D1 ELSE D2 {S'}) =
-  (b=b' \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" |
-"le_acom ({I} WHILE b DO C {P}) ({I'} WHILE b' DO C' {P'}) =
-  (b=b' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')" |
+"le_acom (IF b THEN {p1} C1 ELSE {p2} C2 {S}) (IF b' THEN {q1} D1 ELSE {q2} D2 {S'}) =
+  (b=b' \<and> p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" |
+"le_acom ({I} WHILE b DO {p} C {P}) ({I'} WHILE b' DO {p'} C' {P'}) =
+  (b=b' \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')" |
 "le_acom _ _ = False"
 
 lemma [simp]: "SKIP {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = SKIP {S'} \<and> S \<sqsubseteq> S')"
@@ -94,12 +94,13 @@
 lemma [simp]: "C1;C2 \<sqsubseteq> C \<longleftrightarrow> (\<exists>D1 D2. C = D1;D2 \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)"
 by (cases C) auto
 
-lemma [simp]: "IF b THEN C1 ELSE C2 {S} \<sqsubseteq> C \<longleftrightarrow>
-  (\<exists>D1 D2 S'. C = IF b THEN D1 ELSE D2 {S'} \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')"
+lemma [simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<sqsubseteq> C \<longleftrightarrow>
+  (\<exists>q1 q2 D1 D2 S'. C = IF b THEN {q1} D1 ELSE {q2} D2 {S'} \<and>
+     p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')"
 by (cases C) auto
 
-lemma [simp]: "{I} WHILE b DO C {P} \<sqsubseteq> W \<longleftrightarrow>
-  (\<exists>I' C' P'. W = {I'} WHILE b DO C' {P'} \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')"
+lemma [simp]: "{I} WHILE b DO {p} C {P} \<sqsubseteq> W \<longleftrightarrow>
+  (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')"
 by (cases W) auto
 
 instance
@@ -274,10 +275,10 @@
 "step' S (x ::= e {P}) =
   x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" |
 "step' S (C1; C2) = step' S C1; step' (post C1) C2" |
-"step' S (IF b THEN C1 ELSE C2 {P}) =
-   IF b THEN step' S C1 ELSE step' S C2 {post C1 \<squnion> post C2}" |
-"step' S ({Inv} WHILE b DO C {P}) =
-  {S \<squnion> post C} WHILE b DO (step' Inv C) {Inv}"
+"step' S (IF b THEN {p1} C1 ELSE {p2} C2 {P}) =
+   IF b THEN {S} step' p1 C1 ELSE {S} step' p2 C2 {post C1 \<squnion> post C2}" |
+"step' S ({I} WHILE b DO {p} C {P}) =
+  {S \<squnion> post C} WHILE b DO {I} step' p C {I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI = lpfp (step' \<top>)"
@@ -335,10 +336,10 @@
   case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     by (metis le_post post_map_acom)
 next
-  case (If b C1 C2 P)
-  then obtain D1 D2 P' where
-      "C' = IF b THEN D1 ELSE D2 {P'}"
-      "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1" "C2 \<le> \<gamma>\<^isub>c D2"
+  case (If b p1 C1 p2 C2 P)
+  then obtain q1 q2 D1 D2 P' where
+      "C' = IF b THEN {q1} D1 ELSE {q2} D2 {P'}"
+      "p1 \<subseteq> \<gamma>\<^isub>o q1" "p2 \<subseteq> \<gamma>\<^isub>o q2" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1" "C2 \<le> \<gamma>\<^isub>c D2"
     by (fastforce simp: If_le map_acom_If)
   moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)"
     by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c D1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
@@ -346,15 +347,16 @@
     by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c D2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
   ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` by (simp add: If.IH subset_iff)
 next
-  case (While I b C1 P)
-  then obtain D1 I' P' where
-    "C' = {I'} WHILE b DO D1 {P'}"
-    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1"
+  case (While I b p1 C1 P)
+  then obtain D1 I' p1' P' where
+    "C' = {I'} WHILE b DO {p1'} D1 {P'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "p1 \<subseteq> \<gamma>\<^isub>o p1'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1"
     by (fastforce simp: map_acom_While While_le)
   moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post D1)"
     using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c D1`, simplified]
     by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
   ultimately show ?case by (simp add: While.IH subset_iff)
+
 qed
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -22,10 +22,10 @@
 lemma wt_acom_simps[simp]: "wt (SKIP {P}) X \<longleftrightarrow> wt P X"
   "wt (x ::= e {P}) X \<longleftrightarrow> x : X \<and> vars e \<subseteq> X \<and> wt P X"
   "wt (C1;C2) X \<longleftrightarrow> wt C1 X \<and> wt C2 X"
-  "wt (IF b THEN C1 ELSE C2 {P}) X \<longleftrightarrow>
-   vars b \<subseteq> X \<and> wt C1 X \<and> wt C2 X \<and> wt P X"
-  "wt ({I} WHILE b DO C {P}) X \<longleftrightarrow>
-   wt I X \<and> vars b \<subseteq> X \<and> wt C X \<and> wt P X"
+  "wt (IF b THEN {p1} C1 ELSE {p2} C2 {P}) X \<longleftrightarrow>
+   vars b \<subseteq> X \<and> wt C1 X \<and> wt C2 X \<and> wt p1 X \<and> wt p2 X \<and> wt P X"
+  "wt ({I} WHILE b DO {p} C {P}) X \<longleftrightarrow>
+   wt I X \<and> vars b \<subseteq> X \<and> wt p X \<and> wt C X \<and> wt P X"
 by(auto simp add: wt_acom_def)
 
 lemma wt_post[simp]: "wt c  X \<Longrightarrow> wt (post c) X"
@@ -68,10 +68,10 @@
 "step' S (x ::= e {P}) =
   x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
 "step' S (C1; C2) = step' S C1; step' (post C1) C2" |
-"step' S (IF b THEN C1 ELSE C2 {P}) =
-  (IF b THEN step' S C1 ELSE step' S C2 {post C1 \<squnion> post C2})" |
-"step' S ({Inv} WHILE b DO C {P}) =
-   {S \<squnion> post C} WHILE b DO step' Inv C {Inv}"
+"step' S (IF b THEN {p1} C1 ELSE {p2} C2 {P}) =
+  (IF b THEN {S} step' p1 C1 ELSE {S} step' p2 C2 {post C1 \<squnion> post C2})" |
+"step' S ({I} WHILE b DO {p} C {P}) =
+   {S \<squnion> post C} WHILE b DO {I} step' p C {I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = lpfp (step' (top c)) c"
@@ -99,12 +99,12 @@
   case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     by (metis le_post post_map_acom wt_post)
 next
-  case (If b C1 C2 P)
-  then obtain C1' C2' P' where
-      "C' = IF b THEN C1' ELSE C2' {P'}"
-      "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'"
+  case (If b p1 C1 p2 C2 P)
+  then obtain p1' p2' C1' C2' P' where
+      "C' = IF b THEN {p1'} C1' ELSE {p2'} C2' {P'}"
+      "p1 \<subseteq> \<gamma>\<^isub>o p1'" "p2 \<subseteq> \<gamma>\<^isub>o p2'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'"
     by (fastforce simp: If_le map_acom_If)
-  moreover from this(1) `wt C' X` have wt: "wt C1' X" "wt C2' X"
+  moreover from this(1) `wt C' X` have wt: "wt C1' X" "wt C2' X" "wt p1' X" "wt p2' X"
     by simp_all
   moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
     by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c C1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom wt wt_post)
@@ -113,13 +113,13 @@
   ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` `wt S' X`
     by (simp add: If.IH subset_iff)
 next
-  case (While I b C1 P)
-  then obtain C1' I' P' where
-    "C' = {I'} WHILE b DO C1' {P'}"
-    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'"
+  case (While I b p1 C1 P)
+  then obtain C1' I' p1' P' where
+    "C' = {I'} WHILE b DO {p1'} C1' {P'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "p1 \<subseteq> \<gamma>\<^isub>o p1'" "C1 \<le> \<gamma>\<^isub>c C1'" "P \<subseteq> \<gamma>\<^isub>o P'" 
     by (fastforce simp: map_acom_While While_le)
   moreover from this(1) `wt C' X`
-  have wt: "wt C1' X" "wt I' X" by simp_all
+  have wt: "wt C1' X" "wt I' X" "wt p1' X" by simp_all
   moreover note compat = `wt S' X` wt_post[OF wt(1)]
   moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
     using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c C1'`, simplified]
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -159,13 +159,13 @@
 "step' S (x ::= e {P}) =
   x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
 "step' S (C1; C2) = step' S C1; step' (post C1) C2" |
-"step' S (IF b THEN C1 ELSE C2 {P}) =
-  (let D1 = step' (bfilter b True S) C1; D2 = step' (bfilter b False S) C2
-   in IF b THEN D1 ELSE D2 {post C1 \<squnion> post C2})" |
-"step' S ({Inv} WHILE b DO C {P}) =
+"step' S (IF b THEN {p1} C1 ELSE {p2} C2 {P}) =
+  (let p1' = bfilter b True S; C1' = step' p1 C1; p2' = bfilter b False S; C2' = step' p2 C2
+   in IF b THEN {p1'} C1' ELSE {p2'} C2' {post C1 \<squnion> post C2})" |
+"step' S ({I} WHILE b DO {p} C {P}) =
    {S \<squnion> post C}
-   WHILE b DO step' (bfilter b True Inv) C
-   {bfilter b False Inv}"
+   WHILE b DO {bfilter b True I} step' p C
+   {bfilter b False I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = lpfp (step' \<top>\<^bsub>c\<^esub>) c"
@@ -192,12 +192,12 @@
   case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     by (metis le_post post_map_acom wt_post)
 next
-  case (If b C1 C2 P)
-  then obtain C1' C2' P' where
-      "C' = IF b THEN C1' ELSE C2' {P'}"
-      "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'"
+  case (If b p1 C1 p2 C2 P)
+  then obtain p1' C1' p2' C2' P' where
+      "C' = IF b THEN {p1'} C1' ELSE {p2'} C2' {P'}"
+      "p1 \<subseteq> \<gamma>\<^isub>o p1'" "p2 \<subseteq> \<gamma>\<^isub>o p2'"  "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'" "P \<subseteq> \<gamma>\<^isub>o P'" 
     by (fastforce simp: If_le map_acom_If)
-  moreover from this(1) `wt C' X` have wt: "wt C1' X" "wt C2' X"
+  moreover from this(1) `wt C' X` have wt: "wt C1' X" "wt C2' X" "wt p1' X" "wt p2' X"
     and "vars b \<subseteq> X" by simp_all
   moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
     by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c C1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom wt_post wt)
@@ -207,13 +207,13 @@
   ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'`
     by (simp add: If.IH subset_iff bfilter_sound[OF vars] wt_bfilter[OF vars])
 next
-  case (While I b C1 P)
-  then obtain C1' I' P' where
-    "C' = {I'} WHILE b DO C1' {P'}"
-    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'"
+  case (While I b p C1 P)
+  then obtain C1' I' p' P' where
+    "C' = {I'} WHILE b DO {p'} C1' {P'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "p \<subseteq> \<gamma>\<^isub>o p'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'"
     by (fastforce simp: map_acom_While While_le)
   moreover from this(1) `wt C' X`
-  have wt: "wt C1' X" "wt I' X" and "vars b \<subseteq> X" by simp_all
+  have wt: "wt C1' X" "wt I' X" "wt p' X" and "vars b \<subseteq> X" by simp_all
   moreover note compat = `wt S' X` wt_post[OF wt(1)]
   moreover note vars = `wt I' X` `vars b \<subseteq> X`
   moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -171,10 +171,10 @@
 "map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
 "map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
 "map2_acom f (C1;C2) (D1;D2) = (map2_acom f C1 D1; map2_acom f C2 D2)" |
-"map2_acom f (IF b THEN C1 ELSE C2 {a1}) (IF b' THEN D1 ELSE D2 {a2}) =
-  (IF b THEN map2_acom f C1 D1 ELSE map2_acom f C2 D2 {f a1 a2})" |
-"map2_acom f ({a1} WHILE b DO C {a2}) ({a3} WHILE b' DO C' {a4}) =
-  ({f a1 a3} WHILE b DO map2_acom f C C' {f a2 a4})"
+"map2_acom f (IF b THEN {p1} C1 ELSE {p2} C2 {a1}) (IF b' THEN {q1} D1 ELSE {q2} D2 {a2}) =
+  (IF b THEN {f p1 q1} map2_acom f C1 D1 ELSE {f p2 q2} map2_acom f C2 D2 {f a1 a2})" |
+"map2_acom f ({a1} WHILE b DO {p} C {a2}) ({a3} WHILE b' DO {p'} C' {a4}) =
+  ({f a1 a3} WHILE b DO {f p p'} map2_acom f C C' {f a2 a4})"
 
 instantiation acom :: (WN_Wt)WN_Wt
 begin
@@ -515,7 +515,7 @@
 
 
 lemma annos_narrow_acom[simp]: "strip C2 = strip (C1::'a::WN_Wt acom) \<Longrightarrow>
-  annos(C1 \<triangle> C2) = map (%(x,y).x\<triangle>y) (zip (annos C1) (annos C2))"
+  annos(C1 \<triangle> C2) = map (\<lambda>(x,y).x\<triangle>y) (zip (annos C1) (annos C2))"
 by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" C1 C2 rule: map2_acom.induct)
   (simp_all add: narrow_acom_def size_annos_same2)
 
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -0,0 +1,128 @@
+(* Author: Tobias Nipkow *)
+
+theory ACom_ITP
+imports "../Com"
+begin
+
+(* is there a better place? *)
+definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
+
+subsection "Annotated Commands"
+
+datatype 'a acom =
+  SKIP 'a                           ("SKIP {_}" 61) |
+  Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
+  Seq "('a acom)" "('a acom)"       ("_;//_"  [60, 61] 60) |
+  If bexp "('a acom)" "('a acom)" 'a
+    ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
+  While 'a bexp "('a acom)" 'a
+    ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
+
+fun post :: "'a acom \<Rightarrow>'a" where
+"post (SKIP {P}) = P" |
+"post (x ::= e {P}) = P" |
+"post (c1; c2) = post c2" |
+"post (IF b THEN c1 ELSE c2 {P}) = P" |
+"post ({Inv} WHILE b DO c {P}) = P"
+
+fun strip :: "'a acom \<Rightarrow> com" where
+"strip (SKIP {P}) = com.SKIP" |
+"strip (x ::= e {P}) = (x ::= e)" |
+"strip (c1;c2) = (strip c1; strip c2)" |
+"strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
+"strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)"
+
+fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
+"anno a com.SKIP = SKIP {a}" |
+"anno a (x ::= e) = (x ::= e {a})" |
+"anno a (c1;c2) = (anno a c1; anno a c2)" |
+"anno a (IF b THEN c1 ELSE c2) =
+  (IF b THEN anno a c1 ELSE anno a c2 {a})" |
+"anno a (WHILE b DO c) =
+  ({a} WHILE b DO anno a c {a})"
+
+fun annos :: "'a acom \<Rightarrow> 'a list" where
+"annos (SKIP {a}) = [a]" |
+"annos (x::=e {a}) = [a]" |
+"annos (C1;C2) = annos C1 @ annos C2" |
+"annos (IF b THEN C1 ELSE C2 {a}) = a #  annos C1 @ annos C2" |
+"annos ({i} WHILE b DO C {a}) = i # a # annos C"
+
+fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
+"map_acom f (SKIP {P}) = SKIP {f P}" |
+"map_acom f (x ::= e {P}) = (x ::= e {f P})" |
+"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
+"map_acom f (IF b THEN c1 ELSE c2 {P}) =
+  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" |
+"map_acom f ({Inv} WHILE b DO c {P}) =
+  ({f Inv} WHILE b DO map_acom f c {f P})"
+
+
+lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
+by (induction c) simp_all
+
+lemma strip_acom[simp]: "strip (map_acom f c) = strip c"
+by (induction c) auto
+
+lemma map_acom_SKIP:
+ "map_acom f c = SKIP {S'} \<longleftrightarrow> (\<exists>S. c = SKIP {S} \<and> S' = f S)"
+by (cases c) auto
+
+lemma map_acom_Assign:
+ "map_acom f c = x ::= e {S'} \<longleftrightarrow> (\<exists>S. c = x::=e {S} \<and> S' = f S)"
+by (cases c) auto
+
+lemma map_acom_Seq:
+ "map_acom f c = c1';c2' \<longleftrightarrow>
+ (\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')"
+by (cases c) auto
+
+lemma map_acom_If:
+ "map_acom f c = IF b THEN c1' ELSE c2' {S'} \<longleftrightarrow>
+ (\<exists>S c1 c2. c = IF b THEN c1 ELSE c2 {S} \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2' \<and> S' = f S)"
+by (cases c) auto
+
+lemma map_acom_While:
+ "map_acom f w = {I'} WHILE b DO c' {P'} \<longleftrightarrow>
+ (\<exists>I P c. w = {I} WHILE b DO c {P} \<and> map_acom f c = c' \<and> I' = f I \<and> P' = f P)"
+by (cases w) auto
+
+
+lemma strip_anno[simp]: "strip (anno a c) = c"
+by(induct c) simp_all
+
+lemma strip_eq_SKIP:
+  "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Assign:
+  "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Seq:
+  "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
+by (cases c) simp_all
+
+lemma strip_eq_If:
+  "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow>
+  (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)"
+by (cases c) simp_all
+
+lemma strip_eq_While:
+  "strip c = WHILE b DO c1 \<longleftrightarrow>
+  (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)"
+by (cases c) simp_all
+
+
+lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}"
+by(induction C)(auto)
+
+lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
+apply(induct C2 arbitrary: C1)
+apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While)
+done
+
+lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
+
+
+end
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -1,5 +1,5 @@
 theory Collecting_ITP
-imports Complete_Lattice_ix "../ACom"
+imports Complete_Lattice_ix "ACom_ITP"
 begin
 
 subsection "Collecting Semantics of Commands"
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Abs_Int_Tests.thy
--- a/src/HOL/IMP/Abs_Int_Tests.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -1,5 +1,5 @@
 theory Abs_Int_Tests
-imports ACom
+imports Com
 begin
 
 subsection "Test Programs"
diff -r 7b6beb7e99c1 -r 8ab9fb2483a9 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Mon Sep 03 13:19:52 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy	Mon Sep 03 15:50:41 2012 +0200
@@ -18,10 +18,10 @@
 "(SKIP {S}) \<le> (SKIP {S'}) = (S \<le> S')" |
 "(x ::= e {S}) \<le> (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
 "(c1;c2) \<le> (c1';c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
-"(IF b THEN c1 ELSE c2 {S}) \<le> (IF b' THEN c1' ELSE c2' {S'}) =
-  (b=b' \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')" |
-"({Inv} WHILE b DO c {P}) \<le> ({Inv'} WHILE b' DO c' {P'}) =
-  (b=b' \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')" |
+"(IF b THEN {p1} C1 ELSE {p2} C2 {S}) \<le> (IF b' THEN {p1'} C1' ELSE {p2'} C2' {S'}) =
+  (b=b' \<and> p1 \<le> p1' \<and> C1 \<le> C1' \<and> p2 \<le> p2' \<and> C2 \<le> C2' \<and> S \<le> S')" |
+"({I} WHILE b DO {p} C {P}) \<le> ({I'} WHILE b' DO {p'} C' {P'}) =
+  (b=b' \<and> C \<le> C' \<and> I \<le> I' \<and> p \<le> p' \<and> P \<le> P')" |
 "less_eq_acom _ _ = False"
 
 lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
@@ -30,16 +30,17 @@
 lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
 by (cases c) auto
 
-lemma Seq_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
-by (cases c) auto
+lemma Seq_le: "C1;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
+by (cases C) auto
 
-lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
-  (\<exists>c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')"
-by (cases c) auto
+lemma If_le: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<le> C \<longleftrightarrow>
+  (\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and>
+     p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')"
+by (cases C) auto
 
-lemma While_le: "{Inv} WHILE b DO c {P} \<le> w \<longleftrightarrow>
-  (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')"
-by (cases w) auto
+lemma While_le: "{I} WHILE b DO {p} C {P} \<le> W \<longleftrightarrow>
+  (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')"
+by (cases W) auto
 
 definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
 "less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
@@ -64,16 +65,22 @@
 end
 
 fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
-"sub\<^isub>1(c1;c2) = c1" |
-"sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1" |
-"sub\<^isub>1({I} WHILE b DO c {P}) = c"
+"sub\<^isub>1(C1;C2) = C1" |
+"sub\<^isub>1(IF b THEN {p1} C1 ELSE {p2} C2 {S}) = C1" |
+"sub\<^isub>1({I} WHILE b DO {p} C {P}) = C"
 
 fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
-"sub\<^isub>2(c1;c2) = c2" |
-"sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2"
+"sub\<^isub>2(C1;C2) = C2" |
+"sub\<^isub>2(IF b THEN {p1} C1 ELSE {p2} C2 {S}) = C2"
 
-fun invar :: "'a acom \<Rightarrow> 'a" where
-"invar({I} WHILE b DO c {P}) = I"
+fun anno\<^isub>1 :: "'a acom \<Rightarrow> 'a" where
+"anno\<^isub>1(IF b THEN {p1} C1 ELSE {p2} C2 {S}) = p1" |
+"anno\<^isub>1({I} WHILE b DO {p} C {P}) = I"
+
+fun anno\<^isub>2 :: "'a acom \<Rightarrow> 'a" where
+"anno\<^isub>2(IF b THEN {p1} C1 ELSE {p2} C2 {S}) = p2" |
+"anno\<^isub>2({I} WHILE b DO {p} C {P}) = p"
+
 
 fun lift :: "('a set \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom"
 where
@@ -82,11 +89,11 @@
 "lift F (c1;c2) M =
   lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
 "lift F (IF b THEN c1 ELSE c2) M =
-  IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M)
+  IF b THEN {F (anno\<^isub>1 ` M)} lift F c1 (sub\<^isub>1 ` M) ELSE {F (anno\<^isub>2 ` M)} lift F c2 (sub\<^isub>2 ` M)
   {F (post ` M)}" |
 "lift F (WHILE b DO c) M =
- {F (invar ` M)}
- WHILE b DO lift F c (sub\<^isub>1 ` M)
+ {F (anno\<^isub>1 ` M)}
+ WHILE b DO {F (anno\<^isub>2 ` M)} lift F c (sub\<^isub>1 ` M)
  {F (post ` M)}"
 
 interpretation Complete_Lattice "{C. strip C = c}" "lift Inter c" for c
@@ -137,12 +144,12 @@
 "step S (SKIP {P}) = (SKIP {S})" |
 "step S (x ::= e {P}) =
   (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
-"step S (c1; c2) = step S c1; step (post c1) c2" |
-"step S (IF b THEN c1 ELSE c2 {P}) =
-   IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2
-   {post c1 \<union> post c2}" |
-"step S ({Inv} WHILE b DO c {P}) =
-  {S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
+"step S (C1; C2) = step S C1; step (post C1) C2" |
+"step S (IF b THEN {P1} C1 ELSE {P2} C2 {P}) =
+   IF b THEN {{s:S. bval b s}} step P1 C1 ELSE {{s:S. \<not> bval b s}} step P2 C2
+   {post C1 \<union> post C2}" |
+"step S ({I} WHILE b DO {P} C {P'}) =
+  {S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}"
 
 definition CS :: "com \<Rightarrow> state set acom" where
 "CS c = lfp c (step UNIV)"
@@ -161,8 +168,8 @@
 lemma mono_step: "mono (step S)"
 by(blast intro: monoI mono2_step)
 
-lemma strip_step: "strip(step S c) = strip c"
-by (induction c arbitrary: S) auto
+lemma strip_step: "strip(step S C) = strip C"
+by (induction C arbitrary: S) auto
 
 lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
 apply(rule lfp_unfold[OF _  mono_step])