# HG changeset patch
# User nipkow
# Date 1363774591 -3600
# Node ID 6cd801fabb34bf5934fa0e115830c52aec726621
# Parent  fa84494bf3a0219408c489e45504de31b53437ef
tuned

diff -r fa84494bf3a0 -r 6cd801fabb34 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Tue Mar 19 21:35:15 2013 +0100
+++ b/src/HOL/IMP/Live_True.thy	Wed Mar 20 11:16:31 2013 +0100
@@ -133,8 +133,8 @@
 and is thus executable. *}
 
 lemma L_While: fixes b c X
-assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A"
-shows "L (WHILE b DO c) X = while (\<lambda>A. f A \<noteq> A) f {}" (is "_ = ?r")
+assumes "finite X" defines "f == \<lambda>Y. vars b \<union> X \<union> L c Y"
+shows "L (WHILE b DO c) X = while (\<lambda>Y. f Y \<noteq> Y) f {}" (is "_ = ?r")
 proof -
   let ?V = "vars b \<union> vars c \<union> X"
   have "lfp f = ?r"
@@ -149,10 +149,15 @@
   thus ?thesis by (simp add: f_def)
 qed
 
+lemma L_While_let: "finite X \<Longrightarrow> L (WHILE b DO c) X =
+  (let f = (\<lambda>Y. vars b \<union> X \<union> L c Y)
+   in while (\<lambda>Y. f Y \<noteq> Y) f {})"
+by(simp add: L_While del: L.simps(5))
+
 lemma L_While_set: "L (WHILE b DO c) (set xs) =
-  (let f = (\<lambda>A. vars b \<union> set xs \<union> L c A)
-   in while (\<lambda>A. f A \<noteq> A) f {})"
-by(simp add: L_While del: L.simps(5))
+  (let f = (\<lambda>Y. vars b \<union> set xs \<union> L c Y)
+   in while (\<lambda>Y. f Y \<noteq> Y) f {})"
+by(rule L_While_let, simp)
 
 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