equal
deleted
inserted
replaced
37 |
37 |
38 lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X" |
38 lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X" |
39 by(auto simp add:L_gen_kill) |
39 by(auto simp add:L_gen_kill) |
40 |
40 |
41 lemma L_While_lpfp: |
41 lemma L_While_lpfp: |
42 "\<lbrakk> vars b \<union> X \<subseteq> P; L c P \<subseteq> P \<rbrakk> \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P" |
42 "vars b \<union> X \<union> L c P \<subseteq> P \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P" |
43 by(simp add: L_gen_kill) |
43 by(simp add: L_gen_kill) |
44 |
44 |
45 |
45 |
46 subsection "Soundness" |
46 subsection "Soundness" |
47 |
47 |