--- a/src/HOL/IMP/Abs_Int0.thy Sun Jan 01 16:32:53 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Sun Jan 01 18:12:11 2012 +0100
@@ -58,9 +58,9 @@
function operating on states as functions. *}
lemma step_preserves_le2:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
- \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
-proof(induction c arbitrary: cs ca S sa)
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+ \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' S' ca)"
+proof(induction c arbitrary: cs ca S S')
case SKIP thus ?case
by(auto simp:strip_eq_SKIP)
next
@@ -89,15 +89,15 @@
"I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
"strip cs1 = c1" "strip ca1 = c1"
by (fastforce simp: strip_eq_While)
- moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (sa \<squnion> post ca1)"
- using `S \<subseteq> \<gamma>\<^isub>o sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+ moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post ca1)"
+ using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
ultimately show ?case by (simp add: While.IH subset_iff)
qed
lemma step_preserves_le:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
- \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+ \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' S' ca)"
by (metis le_strip step_preserves_le2 strip_acom)
lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"