--- a/src/HOL/IMP/Live.thy Wed Mar 20 15:35:35 2013 +0100
+++ b/src/HOL/IMP/Live.thy Thu Mar 21 10:05:03 2013 +0100
@@ -42,6 +42,14 @@
"vars b \<union> X \<union> L c P \<subseteq> P \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
by(simp add: L_gen_kill)
+lemma L_While_vars: "vars b \<subseteq> L (WHILE b DO c) X"
+by auto
+
+lemma L_While_X: "X \<subseteq> L (WHILE b DO c) X"
+by auto
+
+text{* Disable L WHILE equation and reason only with L WHILE constraints *}
+declare L.simps(5)[simp del]
subsection "Soundness"
@@ -78,14 +86,15 @@
thus ?case using `~bval b t` by auto
next
case (WhileFalse b s c)
- hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
- thus ?case using WhileFalse.prems by auto
+ hence "~ bval b t"
+ by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+ thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse set_mp)
next
case (WhileTrue b s1 c s2 s3 X t1)
let ?w = "WHILE b DO c"
from `bval b s1` WhileTrue.prems have "bval b t1"
- by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
- have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
+ by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+ have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
by (blast)
from WhileTrue.IH(1)[OF this] obtain t2 where
"(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
@@ -103,7 +112,7 @@
"bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" |
"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
"bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
-"bury (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
+"bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)"
text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the
proof would be very similar. However, we phrase it as a semantics
@@ -142,13 +151,14 @@
thus ?case using `~bval b t` by auto
next
case (WhileFalse b s c)
- hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
- thus ?case using WhileFalse.prems by auto
+ hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+ thus ?case
+ by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse set_mp)
next
case (WhileTrue b s1 c s2 s3 X t1)
let ?w = "WHILE b DO c"
from `bval b s1` WhileTrue.prems have "bval b t1"
- by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+ by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
have "s1 = t1 on L c (L ?w X)"
using L_While_pfp WhileTrue.prems by blast
from WhileTrue.IH(1)[OF this] obtain t2 where
@@ -182,7 +192,7 @@
by (cases c) auto
lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
- (EX c'. c = WHILE b DO c' & bc' = bury c' (vars b \<union> X \<union> L c X))"
+ (EX c'. c = WHILE b DO c' & bc' = bury c' (L (WHILE b DO c') X))"
by (cases c) auto
theorem bury_sound2:
@@ -226,24 +236,25 @@
thus ?case using c `~bval b t` by auto
next
case (WhileFalse b s c)
- hence "~ bval b t" by (auto simp: ball_Un dest: bval_eq_if_eq_on_vars)
- thus ?case using WhileFalse by auto
+ hence "~ bval b t"
+ by auto (metis L_While_vars bval_eq_if_eq_on_vars set_rev_mp)
+ thus ?case using WhileFalse
+ by auto (metis L_While_X big_step.WhileFalse set_mp)
next
- case (WhileTrue b s1 bc' s2 s3 c X t1)
- then obtain c' where c: "c = WHILE b DO c'"
- and bc': "bc' = bury c' (vars b \<union> X \<union> L c' X)" by auto
- let ?w = "WHILE b DO c'"
- from `bval b s1` WhileTrue.prems c have "bval b t1"
- by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+ case (WhileTrue b s1 bc' s2 s3 w X t1)
+ then obtain c' where w: "w = WHILE b DO c'"
+ and bc': "bc' = bury c' (L (WHILE b DO c') X)" by auto
+ from `bval b s1` WhileTrue.prems w have "bval b t1"
+ by auto (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
note IH = WhileTrue.hyps(3,5)
- have "s1 = t1 on L c' (L ?w X)"
- using L_While_pfp WhileTrue.prems c by blast
- with IH(1)[OF bc', of t1] obtain t2 where
- "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
- from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
- where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
+ have "s1 = t1 on L c' (L w X)"
+ using L_While_pfp WhileTrue.prems w by blast
+ with IH(1)[OF bc', of t1] w obtain t2 where
+ "(c', t1) \<Rightarrow> t2" "s2 = t2 on L w X" by auto
+ from IH(2)[OF WhileTrue.hyps(6), of t2] w this(2) obtain t3
+ where "(w,t2) \<Rightarrow> t3" "s3 = t3 on X"
by auto
- with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
+ with `bval b t1` `(c', t1) \<Rightarrow> t2` w show ?case by auto
qed
corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
--- a/src/HOL/IMP/Live_True.thy Wed Mar 20 15:35:35 2013 +0100
+++ b/src/HOL/IMP/Live_True.thy Thu Mar 21 10:05:03 2013 +0100
@@ -37,6 +37,18 @@
"L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)"
by(metis lfp_unfold[OF mono_union_L] L.simps(5))
+lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
+using L_While_unfold by blast
+
+lemma L_While_vars: "vars b \<subseteq> L (WHILE b DO c) X"
+using L_While_unfold by blast
+
+lemma L_While_X: "X \<subseteq> L (WHILE b DO c) X"
+using L_While_unfold by blast
+
+text{* Disable L WHILE equation and reason only with L WHILE constraints *}
+declare L.simps(5)[simp del]
+
subsection "Soundness"
@@ -74,14 +86,14 @@
next
case (WhileFalse b s c)
hence "~ bval b t"
- by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars)
- thus ?case using WhileFalse.prems L_While_unfold[of b c X] by auto
+ by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+ thus ?case using WhileFalse.prems L_While_X[of X b c] by auto
next
case (WhileTrue b s1 c s2 s3 X t1)
let ?w = "WHILE b DO c"
from `bval b s1` WhileTrue.prems have "bval b t1"
- by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars)
- have "s1 = t1 on L c (L ?w X)" using L_While_unfold WhileTrue.prems
+ by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+ have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
by (blast)
from WhileTrue.IH(1)[OF this] obtain t2 where
"(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
@@ -90,6 +102,8 @@
with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
qed
+(*declare L.simps(5)[simp]*)
+
subsection "Executability"
@@ -113,7 +127,7 @@
have "lfp(\<lambda>Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> vars c \<union> X"
using While.IH[of "vars b \<union> vars c \<union> X"]
by (auto intro!: lfp_lowerbound)
- thus ?case by simp
+ thus ?case by (simp add: L.simps(5))
qed auto
lemma afinite[simp]: "finite(vars(a::aexp))"
@@ -146,13 +160,13 @@
next
show "finite ?V" using `finite X` by simp
qed
- thus ?thesis by (simp add: f_def)
+ thus ?thesis by (simp add: f_def L.simps(5))
qed
lemma L_While_let: "finite X \<Longrightarrow> L (WHILE b DO c) X =
(let f = (\<lambda>Y. vars b \<union> X \<union> L c Y)
in while (\<lambda>Y. f Y \<noteq> Y) f {})"
-by(simp add: L_While del: L.simps(5))
+by(simp add: L_While)
lemma L_While_set: "L (WHILE b DO c) (set xs) =
(let f = (\<lambda>Y. vars b \<union> set xs \<union> L c Y)
@@ -206,7 +220,7 @@
let ?f = "\<lambda>A. vars b \<union> X \<union> L c A"
let ?fb = "\<lambda>A. vars b \<union> X \<union> Lb c A"
show ?case
- proof (simp, rule lfp_subset_iter[OF mono_union_L])
+ proof (simp add: L.simps(5), rule lfp_subset_iter[OF mono_union_L])
show "!!X. ?f X \<subseteq> ?fb X" using While.IH by blast
show "lfp ?f \<subseteq> vars b \<union> vars c \<union> X"
by (metis (full_types) L.simps(5) L_subset_vars vars_com.simps(5))