--- a/src/HOL/IMP/ACom.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/ACom.thy Mon Sep 03 15:41:06 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
--- a/src/HOL/IMP/Abs_Int0.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Mon Sep 03 15:41:06 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"
--- a/src/HOL/IMP/Abs_Int1.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Mon Sep 03 15:41:06 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]
--- a/src/HOL/IMP/Abs_Int2.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Mon Sep 03 15:41:06 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')"
--- a/src/HOL/IMP/Abs_Int3.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Mon Sep 03 15:41:06 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)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Mon Sep 03 15:41:06 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
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Mon Sep 03 15:41:06 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"
--- a/src/HOL/IMP/Abs_Int_Tests.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy Mon Sep 03 15:41:06 2012 +0200
@@ -1,5 +1,5 @@
theory Abs_Int_Tests
-imports ACom
+imports Com
begin
subsection "Test Programs"
--- a/src/HOL/IMP/Collecting.thy Mon Sep 03 09:15:58 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy Mon Sep 03 15:41:06 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])