--- a/src/HOL/IMP/Abs_Int0.thy Mon Jan 02 11:33:50 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Mon Jan 02 11:54:21 2012 +0100
@@ -91,7 +91,7 @@
ultimately show ?case by (simp add: While.IH subset_iff)
qed
-lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
proof(simp add: CS_def AI_def)
assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
--- a/src/HOL/IMP/Abs_Int0_fun.thy Mon Jan 02 11:33:50 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Mon Jan 02 11:54:21 2012 +0100
@@ -342,7 +342,7 @@
ultimately show ?case by (simp add: While.IH subset_iff)
qed
-lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
proof(simp add: CS_def AI_def)
assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
--- a/src/HOL/IMP/Abs_Int1.thy Mon Jan 02 11:33:50 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Mon Jan 02 11:54:21 2012 +0100
@@ -203,7 +203,7 @@
ultimately show ?case by (simp add: While.IH subset_iff bfilter_sound)
qed
-lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
proof(simp add: CS_def AI_def)
assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
--- a/src/HOL/IMP/Abs_Int2.thy Mon Jan 02 11:33:50 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Mon Jan 02 11:54:21 2012 +0100
@@ -187,7 +187,7 @@
definition AI_WN :: "com \<Rightarrow> 'av st option acom option" where
"AI_WN = pfp_WN (step' \<top>)"
-lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
proof(simp add: CS_def AI_WN_def)
assume 1: "pfp_WN (step' \<top>) c = Some c'"
from pfp_WN_pfp[OF allI[OF strip_step'] mono_step' 1]
--- a/src/HOL/IMP/Collecting.thy Mon Jan 02 11:33:50 2012 +0100
+++ b/src/HOL/IMP/Collecting.thy Mon Jan 02 11:54:21 2012 +0100
@@ -149,8 +149,8 @@
"step S ({Inv} WHILE b DO c {P}) =
{S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
-definition CS :: "state set \<Rightarrow> com \<Rightarrow> state set acom" where
-"CS S c = lfp (step S) c"
+definition CS :: "com \<Rightarrow> state set acom" where
+"CS c = lfp (step UNIV) c"
lemma mono_step_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step S x \<le> step T y"
proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
@@ -174,10 +174,10 @@
apply(simp add: strip_step)
done
-lemma CS_unfold: "CS S c = step S (CS S c)"
+lemma CS_unfold: "CS c = step UNIV (CS c)"
by (metis CS_def lfp_cs_unfold)
-lemma strip_CS[simp]: "strip(CS S c) = c"
+lemma strip_CS[simp]: "strip(CS c) = c"
by(simp add: CS_def index_lfp[simplified])
end
--- a/src/HOL/IMP/Collecting1.thy Mon Jan 02 11:33:50 2012 +0100
+++ b/src/HOL/IMP/Collecting1.thy Mon Jan 02 11:54:21 2012 +0100
@@ -38,7 +38,7 @@
show ?thesis by(simp add: steps_def)
qed
-theorem steps_approx_CS: "s:S \<Longrightarrow> steps s c n \<le> CS S c"
-by (metis CS_unfold steps_approx_fix_step strip_CS)
+theorem steps_approx_CS: "steps s c n \<le> CS c"
+by (metis CS_unfold UNIV_I steps_approx_fix_step strip_CS)
end