# HG changeset patch
# User nipkow
# Date 1342276558 -7200
# Node ID 5fa4fc4d721aff458975846f00192fa8eed86d3b
# Parent  968602739b543137689bc6c041a39f15aaca57ea
removed superfluous lemmas

diff -r 968602739b54 -r 5fa4fc4d721a src/HOL/IMP/Live_True.thy
--- 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"