diff -r 033cb3a668b9 -r 9c232d370244 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Dec 13 16:14:41 2011 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Tue Dec 13 16:53:28 2011 +0100
@@ -52,16 +52,13 @@
   ultimately show ?thesis unfolding while_option_def by auto 
 qed
 
-lemma while_option_stop:
-assumes "while_option b c s = Some t"
-shows "~ b t"
-proof -
-  from assms have ex: "\<exists>k. ~ b ((c ^^ k) s)"
-  and t: "t = (c ^^ (LEAST k. ~ b ((c ^^ k) s))) s"
-    by (auto simp: while_option_def split: if_splits)
-  from LeastI_ex[OF ex]
-  show "~ b t" unfolding t .
-qed
+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 (lam_lifting) LeastI_ex)
+
+lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t"
+by(metis while_option_stop2)
 
 theorem while_option_rule:
 assumes step: "!!s. P s ==> b s ==> P (c s)"
@@ -145,4 +142,31 @@
   \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
 
+text{* Kleene iteration starting from the empty set and assuming some finite
+bounding set: *}
+
+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
+
+lemma lfp_the_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_Kleene_iter[OF assms(1)]
+  show ?thesis by auto
+qed
+
 end