# HG changeset patch
# User nipkow
# Date 1347524928 -7200
# Node ID ce1ccb78ecdabc6af3d032cf60e9edf2eaf7de55
# Parent  bcce6988f6fa39a4caf5f6ae975d7c7c69adde9b
tuned

diff -r bcce6988f6fa -r ce1ccb78ecda src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Wed Sep 12 23:38:12 2012 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Sep 13 10:28:48 2012 +0200
@@ -275,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 {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}"
+"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+   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 {Q}) =
+  {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>)"
diff -r bcce6988f6fa -r ce1ccb78ecda src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Sep 12 23:38:12 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Sep 13 10:28:48 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 {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"
+  "wt (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X \<longleftrightarrow>
+   vars b \<subseteq> X \<and> wt C1 X \<and> wt C2 X \<and> wt P1 X \<and> wt P2 X \<and> wt Q X"
+  "wt ({I} WHILE b DO {P} C {Q}) X \<longleftrightarrow>
+   wt I X \<and> vars b \<subseteq> X \<and> wt P X \<and> wt C X \<and> wt Q 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 {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}"
+"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+  (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 {Q}) =
+   {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 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'"
+  case (If b P1 C1 P2 C2 Q)
+  then obtain P1' P2' C1' C2' Q' where
+      "C' = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'}"
+      "P1 \<subseteq> \<gamma>\<^isub>o P1'" "P2 \<subseteq> \<gamma>\<^isub>o P2'" "Q \<subseteq> \<gamma>\<^isub>o Q'" "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" "wt p1' X" "wt p2' 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 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'" 
+  case (While I b P1 C1 Q)
+  then obtain C1' I' P1' Q' where
+    "C' = {I'} WHILE b DO {P1'} C1' {Q'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "P1 \<subseteq> \<gamma>\<^isub>o P1'" "C1 \<le> \<gamma>\<^isub>c C1'" "Q \<subseteq> \<gamma>\<^isub>o Q'" 
     by (fastforce simp: map_acom_While While_le)
   moreover from this(1) `wt C' X`
-  have wt: "wt C1' X" "wt I' X" "wt p1' 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 bcce6988f6fa -r ce1ccb78ecda src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Wed Sep 12 23:38:12 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Thu Sep 13 10:28:48 2012 +0200
@@ -108,7 +108,7 @@
 
 text{* Instantiating the abstract interpretation locale requires no more
 proofs (they happened in the instatiation above) but delivers the
-instantiated abstract interpreter which we call AI: *}
+instantiated abstract interpreter which we call @{text AI_parity}: *}
 
 interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
diff -r bcce6988f6fa -r ce1ccb78ecda src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Wed Sep 12 23:38:12 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu Sep 13 10:28:48 2012 +0200
@@ -159,10 +159,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 {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}) =
+"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+  (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 {Q}) =
    {S \<squnion> post C}
    WHILE b DO {bfilter b True I} step' p C
    {bfilter b False I}"
@@ -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 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'" 
+  case (If b P1 C1 P2 C2 Q)
+  then obtain P1' C1' P2' C2' Q' where
+      "C' = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'}"
+      "P1 \<subseteq> \<gamma>\<^isub>o P1'" "P2 \<subseteq> \<gamma>\<^isub>o P2'"  "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'" "Q \<subseteq> \<gamma>\<^isub>o Q'" 
     by (fastforce simp: If_le map_acom_If)
-  moreover from this(1) `wt C' X` have wt: "wt C1' X" "wt C2' X" "wt p1' X" "wt p2' 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 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'"
+  case (While I b P C1 Q)
+  then obtain C1' I' P' Q' where
+    "C' = {I'} WHILE b DO {P'} C1' {Q'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "Q \<subseteq> \<gamma>\<^isub>o Q'" "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" "wt p' 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 bcce6988f6fa -r ce1ccb78ecda src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed Sep 12 23:38:12 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Thu Sep 13 10:28:48 2012 +0200
@@ -99,8 +99,8 @@
 
 datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set"
 
-fun "fun" where "fun (FunDom f xs) = f"
-fun dom where "dom (FunDom f xs) = xs"
+fun "fun" where "fun (FunDom f X) = f"
+fun dom where "dom (FunDom f X) = X"
 
 definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
 
diff -r bcce6988f6fa -r ce1ccb78ecda src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Wed Sep 12 23:38:12 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy	Thu Sep 13 10:28:48 2012 +0200
@@ -15,13 +15,13 @@
 begin
 
 fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
-"(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 {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')" |
+"(SKIP {P}) \<le> (SKIP {P'}) = (P \<le> P')" |
+"(x ::= e {P}) \<le> (x' ::= e' {P'}) = (x=x' \<and> e=e' \<and> P \<le> P')" |
+"(C1;C2) \<le> (C1';C2') = (C1 \<le> C1' \<and> C2 \<le> C2')" |
+"(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) \<le> (IF b' THEN {P1'} C1' ELSE {P2'} C2' {Q'}) =
+  (b=b' \<and> P1 \<le> P1' \<and> C1 \<le> C1' \<and> P2 \<le> P2' \<and> C2 \<le> C2' \<and> Q \<le> Q')" |
+"({I} WHILE b DO {P} C {Q}) \<le> ({I'} WHILE b' DO {P'} C' {Q'}) =
+  (b=b' \<and> C \<le> C' \<and> I \<le> I' \<and> P \<le> P' \<and> Q \<le> Q')" |
 "less_eq_acom _ _ = False"
 
 lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
@@ -66,20 +66,20 @@
 
 fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
 "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"
+"sub\<^isub>1(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = C1" |
+"sub\<^isub>1({I} WHILE b DO {P} C {Q}) = C"
 
 fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
 "sub\<^isub>2(C1;C2) = C2" |
-"sub\<^isub>2(IF b THEN {p1} C1 ELSE {p2} C2 {S}) = C2"
+"sub\<^isub>2(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = C2"
 
 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"
+"anno\<^isub>1(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = P1" |
+"anno\<^isub>1({I} WHILE b DO {P} C {Q}) = 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"
+"anno\<^isub>2(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = P2" |
+"anno\<^isub>2({I} WHILE b DO {P} C {Q}) = P"
 
 
 fun lift :: "('a set \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom"