# HG changeset patch
# User nipkow
# Date 1353708478 -3600
# Node ID bc3c4c89d5c95243c257018d5c257795b626ed62
# Parent  978200ae84736498decdf460ff95f0c36b64f33f# Parent  c6626861c31afacbc4b4816eb491bd2b8bfde228
merged

diff -r 978200ae8473 -r bc3c4c89d5c9 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Fri Nov 23 22:16:52 2012 +0100
+++ b/src/HOL/IMP/Live_True.thy	Fri Nov 23 23:07:58 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 978200ae8473 -r bc3c4c89d5c9 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Nov 23 22:16:52 2012 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Fri Nov 23 23:07:58 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