# HG changeset patch
# User nipkow
# Date 1323177504 -3600
# Node ID a7046524409699734b443edd6d84cd2d0865d660
# Parent  5d35cb2c0f02f7edc160021d7c8409d8f04e7201
added lemmas

diff -r 5d35cb2c0f02 -r a70465244096 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Mon Dec 05 22:29:43 2011 +0100
+++ b/src/HOL/IMP/Live.thy	Tue Dec 06 14:18:24 2011 +0100
@@ -35,9 +35,13 @@
 lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
 by(induct c arbitrary:X) auto
 
-lemma L_While_subset: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
+lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
 by(auto simp add:L_gen_kill)
 
+lemma L_While_lpfp:
+  "\<lbrakk> vars b \<union> X \<subseteq> P; L c P \<subseteq> P \<rbrakk> \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
+by(simp add: L_gen_kill)
+
 
 subsection "Soundness"
 
@@ -81,7 +85,7 @@
   let ?w = "WHILE b DO c"
   from `bval b s1` WhileTrue.prems have "bval b t1"
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
-  have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
+  have "s1 = t1 on L c (L ?w X)" using  L_While_pfp WhileTrue.prems
     by (blast)
   from WhileTrue.IH(1)[OF this] obtain t2 where
     "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
@@ -146,7 +150,7 @@
   from `bval b s1` WhileTrue.prems have "bval b t1"
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   have "s1 = t1 on L c (L ?w X)"
-    using L_While_subset WhileTrue.prems by blast
+    using L_While_pfp WhileTrue.prems by blast
   from WhileTrue.IH(1)[OF this] obtain t2 where
     "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
   from WhileTrue.IH(2)[OF this(2)] obtain t3
@@ -233,7 +237,7 @@
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   note IH = WhileTrue.hyps(3,5)
   have "s1 = t1 on L c' (L ?w X)"
-    using L_While_subset WhileTrue.prems c by blast
+    using L_While_pfp WhileTrue.prems c by blast
   with IH(1)[OF bc', of t1] obtain t2 where
     "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
   from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3