diff -r 113cee845044 -r fba08009ff3e src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Thu Jul 28 20:39:51 2016 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri Jul 29 09:49:23 2016 +0200
@@ -300,6 +300,65 @@
   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
 unfolding while_def using assms by (rule lfp_the_while_option) blast
 
+lemma wf_finite_less:
+  assumes "finite (C :: 'a::order set)"
+  shows "wf {(x, y). {x, y} \<subseteq> C \<and> x < y}"
+by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> a < b}", THEN wf_subset])
+   (fastforce simp: less_eq assms intro: psubset_card_mono)
+
+lemma wf_finite_greater:
+  assumes "finite (C :: 'a::order set)"
+  shows "wf {(x, y). {x, y} \<subseteq> C \<and> y < x}"
+by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> b < a}", THEN wf_subset])
+   (fastforce simp: less_eq assms intro: psubset_card_mono)
+
+lemma while_option_finite_increasing_Some:
+  fixes f :: "'a::order \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)" and "s \<le> f s"
+  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
+by (rule wf_rel_while_option_Some[where R="{(x, y). y < x}" and P="\<lambda>A. A \<le> f A" and s="s"])
+   (auto simp: assms monoD intro: wf_finite_greater[where C="UNIV::'a set", simplified])
+
+lemma lfp_the_while_option_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "lfp f = the (while_option (\<lambda>A. f A \<noteq> A) f bot)"
+proof -
+  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f bot = Some P"
+    using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast
+  with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
+  show ?thesis by auto
+qed
+
+lemma lfp_while_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f bot"
+unfolding while_def using assms by (rule lfp_the_while_option_lattice)
+
+lemma while_option_finite_decreasing_Some:
+  fixes f :: "'a::order \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)" and "f s \<le> s"
+  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
+by (rule wf_rel_while_option_Some[where R="{(x, y). x < y}" and P="\<lambda>A. f A \<le> A" and s="s"])
+   (auto simp add: assms monoD intro: wf_finite_less[where C="UNIV::'a set", simplified])
+
+lemma gfp_the_while_option_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "gfp f = the(while_option (\<lambda>A. f A \<noteq> A) f top)"
+proof -
+  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f top = Some P"
+    using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast
+  with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)]
+  show ?thesis by auto
+qed
+
+lemma gfp_while_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "gfp f = while (\<lambda>A. f A \<noteq> A) f top"
+unfolding while_def using assms by (rule gfp_the_while_option_lattice)
 
 text\<open>Computing the reflexive, transitive closure by iterating a successor
 function. Stops when an element is found that dos not satisfy the test.