# HG changeset patch
# User nipkow
# Date 1325501661 -3600
# Node ID 8392c28d7868e7bc0c4c56c939bf0b8bc4e1401e
# Parent  4869f1389333a27df91e46e8537e26d6eb5069f3
tuned

diff -r 4869f1389333 -r 8392c28d7868 src/HOL/IMP/Abs_Int0.thy
--- 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])
diff -r 4869f1389333 -r 8392c28d7868 src/HOL/IMP/Abs_Int0_fun.thy
--- 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])
diff -r 4869f1389333 -r 8392c28d7868 src/HOL/IMP/Abs_Int1.thy
--- 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])
diff -r 4869f1389333 -r 8392c28d7868 src/HOL/IMP/Abs_Int2.thy
--- 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]
diff -r 4869f1389333 -r 8392c28d7868 src/HOL/IMP/Collecting.thy
--- 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
diff -r 4869f1389333 -r 8392c28d7868 src/HOL/IMP/Collecting1.thy
--- 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