src/HOL/Library/While_Combinator.thy
changeset 50180 c6626861c31a
parent 50008 eb7f574d0303
child 50577 cfbad2d08412
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Nov 23 18:28:00 2012 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Nov 23 23:07:38 2012 +0100
     1.3 @@ -169,4 +169,9 @@
     1.4    show ?thesis by auto
     1.5  qed
     1.6  
     1.7 +lemma lfp_while:
     1.8 +  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
     1.9 +  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
    1.10 +unfolding while_def using assms by (rule lfp_the_while_option) blast
    1.11 +
    1.12  end