# HG changeset patch
# User nipkow
# Date 1353708458 -3600
# Node ID c6626861c31afacbc4b4816eb491bd2b8bfde228
# Parent  ad52ddd35c3acc2d80d8dc32cd6f25a88637db6f
moved lemma

diff -r ad52ddd35c3a -r c6626861c31a src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Fri Nov 23 18:28:00 2012 +0100
+++ b/src/HOL/IMP/Live_True.thy	Fri Nov 23 23:07:38 2012 +0100
@@ -125,13 +125,6 @@
 lemma cfinite[simp]: "finite(vars(c::com))"
 by (induction c) auto
 
-text{* Some code generation magic: executing @{const lfp} *}
-
-(* FIXME mv into Library *)
-lemma lfp_while:
-  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
-  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
-unfolding while_def using assms by (rule lfp_the_while_option) blast
 
 text{* Make @{const L} executable by replacing @{const lfp} with the @{const
 while} combinator from theory @{theory While_Combinator}. The @{const while}
@@ -161,10 +154,11 @@
    in while (\<lambda>A. f A \<noteq> A) f {})"
 by(simp add: L_While del: L.simps(5))
 
-text{* Replace the equation for L WHILE by the executable @{thm[source] L_While_set}: *}
+text{* Replace the equation for @{text "L (WHILE \<dots>)"} by the executable @{thm[source] L_While_set}: *}
 lemmas [code] = L.simps(1-4) L_While_set
 text{* Sorry, this syntax is odd. *}
 
+text{* A test: *}
 lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x''; ''x'' ::= V ''z''
   in L (WHILE b DO c) {''y''}) = {''x'', ''y'', ''z''}"
 by eval
diff -r ad52ddd35c3a -r c6626861c31a src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Nov 23 18:28:00 2012 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Fri Nov 23 23:07:38 2012 +0100
@@ -169,4 +169,9 @@
   show ?thesis by auto
 qed
 
+lemma lfp_while:
+  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
+  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
+unfolding while_def using assms by (rule lfp_the_while_option) blast
+
 end