# 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 \ C \ f X \ C" and "finite C" - shows "lfp f = while (\A. f A \ 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 (\A. f A \ 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 \)"} 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 \ C \ f X \ C" and "finite C" + shows "lfp f = while (\A. f A \ A) f {}" +unfolding while_def using assms by (rule lfp_the_while_option) blast + end