--- 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')"