--- a/src/HOL/IMP/Live_True.thy Fri Jul 13 08:45:09 2012 +0200
+++ b/src/HOL/IMP/Live_True.thy Sat Jul 14 16:35:58 2012 +0200
@@ -123,55 +123,6 @@
lemma cfinite[simp]: "finite(vars(c::com))"
by (induction c) auto
-(* move to Inductive; call Kleene? *)
-lemma lfp_finite_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"
-shows "lfp f = (f^^k) bot"
-proof(rule antisym)
- show "lfp f \<le> (f^^k) bot"
- proof(rule lfp_lowerbound)
- show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp
- qed
-next
- show "(f^^k) bot \<le> lfp f"
- proof(induction k)
- case 0 show ?case by simp
- next
- case Suc
- from monoD[OF assms(1) Suc] lfp_unfold[OF assms(1)]
- show ?case by simp
- qed
-qed
-
-(* move to While_Combinator *)
-lemma while_option_stop2:
- "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
-apply(simp add: while_option_def split: if_splits)
-by (metis (lifting) LeastI_ex)
-(* move to While_Combinator *)
-lemma while_option_finite_subset_Some: fixes C :: "'a set"
- assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
- shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
-proof(rule measure_while_option_Some[where
- f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
- fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
- show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
- (is "?L \<and> ?R")
- proof
- show ?L by(metis A(1) assms(2) monoD[OF `mono f`])
- show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
- qed
-qed simp
-(* move to While_Combinator *)
-lemma lfp_eq_while_option:
- assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
- shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
-proof-
- obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
- using while_option_finite_subset_Some[OF assms] by blast
- with while_option_stop2[OF this] lfp_finite_iter[OF assms(1)]
- show ?thesis by auto
-qed
-
text{* For code generation: *}
lemma L_While: fixes b c X
assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A"
@@ -179,7 +130,7 @@
proof -
let ?V = "vars b \<union> vars c \<union> X"
have "lfp f = ?r"
- proof(rule lfp_eq_while_option[where C = "?V"])
+ proof(rule lfp_the_while_option[where C = "?V"])
show "mono f" by(simp add: f_def mono_union_L)
next
fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V"