# HG changeset patch
# User nipkow
# Date 1322397112 -3600
# Node ID a49f9428aba45588639666605c6753d0c23dcae4
# Parent  8634b4e61b88ef3abe7269b889646fcc3a31f23c
simplified Collecting1 and renamed: step -> step', step_cs -> step

diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -25,22 +25,22 @@
 locale Abs_Int = Val_abs
 begin
 
-fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
-"step S (SKIP {P}) = (SKIP {S})" |
-"step S (x ::= e {P}) =
+fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
+"step' S (SKIP {P}) = (SKIP {S})" |
+"step' S (x ::= e {P}) =
   x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
-"step S (c1; c2) = step S c1; step (post c1) c2" |
-"step S (IF b THEN c1 ELSE c2 {P}) =
-  (let c1' = step S c1; c2' = step S c2
+"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
+"step' S (IF b THEN c1 ELSE c2 {P}) =
+  (let c1' = step' S c1; c2' = step' S c2
    in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
-"step S ({Inv} WHILE b DO c {P}) =
-   {S \<squnion> post c} WHILE b DO step Inv c {Inv}"
+"step' S ({Inv} WHILE b DO c {P}) =
+   {S \<squnion> post c} WHILE b DO step' Inv c {Inv}"
 
 definition AI :: "com \<Rightarrow> 'a st option acom option" where
-"AI = lpfp\<^isub>c (step \<top>)"
+"AI = lpfp\<^isub>c (step' \<top>)"
 
 
-lemma strip_step[simp]: "strip(step S c) = strip c"
+lemma strip_step'[simp]: "strip(step' S c) = strip c"
 by(induct c arbitrary: S) (simp_all add: Let_def)
 
 
@@ -55,7 +55,7 @@
 
 lemma step_preserves_le2:
   "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
-   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
+   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
 proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
     by(auto simp:strip_eq_SKIP)
@@ -93,24 +93,24 @@
 
 lemma step_preserves_le:
   "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
-   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
+   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa 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'"
 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])
-  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c"
+  assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
+  have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
+  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
-  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[OF 3])
-    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_rep_c order_trans)
 qed
 
@@ -129,7 +129,7 @@
 lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
 by(auto simp add: le_st_def lookup_def update_def)
 
-lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
+lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
 apply(induction c arbitrary: S S')
 apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
 done
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -68,7 +68,7 @@
 
 interpretation Abs_Int rep_cval Const plus_cval
 defines AI_const is AI
-and step_const is step
+and step_const is step'
 proof qed
 
 
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -253,22 +253,22 @@
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
+fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
  where
-"step S (SKIP {P}) = (SKIP {S})" |
-"step S (x ::= e {P}) =
+"step' S (SKIP {P}) = (SKIP {S})" |
+"step' S (x ::= e {P}) =
   x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" |
-"step S (c1; c2) = step S c1; step (post c1) c2" |
-"step S (IF b THEN c1 ELSE c2 {P}) =
-   IF b THEN step S c1 ELSE step S c2 {post c1 \<squnion> post c2}" |
-"step S ({Inv} WHILE b DO c {P}) =
-  {S \<squnion> post c} WHILE b DO (step Inv c) {Inv}"
+"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
+"step' S (IF b THEN c1 ELSE c2 {P}) =
+   IF b THEN step' S c1 ELSE step' S c2 {post c1 \<squnion> post c2}" |
+"step' S ({Inv} WHILE b DO c {P}) =
+  {S \<squnion> post c} WHILE b DO (step' Inv c) {Inv}"
 
 definition AI :: "com \<Rightarrow> 'a st option acom option" where
-"AI = lpfp\<^isub>c (step \<top>)"
+"AI = lpfp\<^isub>c (step' \<top>)"
 
 
-lemma strip_step[simp]: "strip(step S c) = strip c"
+lemma strip_step'[simp]: "strip(step' S c) = strip c"
 by(induct c arbitrary: S) (simp_all add: Let_def)
 
 
@@ -310,7 +310,7 @@
 
 lemma step_preserves_le2:
   "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
-   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
+   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
 proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
     by(auto simp:strip_eq_SKIP)
@@ -348,24 +348,24 @@
 
 lemma step_preserves_le:
   "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
-   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
+   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa 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'"
 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])
-  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c"
+  assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
+  have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
+  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
-  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[OF 3])
-    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_rep_c order_trans)
 qed
 
@@ -384,7 +384,7 @@
 lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
 by(simp add: le_fun_def)
 
-lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
+lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
 apply(induction c arbitrary: S S')
 apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
 done
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -139,24 +139,24 @@
 qed
 
 
-fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
+fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
  where
-"step S (SKIP {P}) = (SKIP {S})" |
-"step S (x ::= e {P}) =
+"step' S (SKIP {P}) = (SKIP {S})" |
+"step' S (x ::= e {P}) =
   x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
-"step S (c1; c2) = step S c1; step (post c1) c2" |
-"step S (IF b THEN c1 ELSE c2 {P}) =
-  (let c1' = step (bfilter b True S) c1; c2' = step (bfilter b False S) c2
+"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
+"step' S (IF b THEN c1 ELSE c2 {P}) =
+  (let c1' = step' (bfilter b True S) c1; c2' = step' (bfilter b False S) c2
    in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
-"step S ({Inv} WHILE b DO c {P}) =
+"step' S ({Inv} WHILE b DO c {P}) =
    {S \<squnion> post c}
-   WHILE b DO step (bfilter b True Inv) c
+   WHILE b DO step' (bfilter b True Inv) c
    {bfilter b False Inv}"
 
 definition AI :: "com \<Rightarrow> 'a st option acom option" where
-"AI = lpfp\<^isub>c (step \<top>)"
+"AI = lpfp\<^isub>c (step' \<top>)"
 
-lemma strip_step[simp]: "strip(step S c) = strip c"
+lemma strip_step'[simp]: "strip(step' S c) = strip c"
 by(induct c arbitrary: S) (simp_all add: Let_def)
 
 
@@ -169,7 +169,7 @@
 
 lemma step_preserves_le2:
   "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
-   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
+   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
 proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
     by(auto simp:strip_eq_SKIP)
@@ -208,24 +208,24 @@
 
 lemma step_preserves_le:
   "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
-   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
+   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa 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'"
 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])
-  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c"
+  assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
+  have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
+  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
-  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[OF 3])
-    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_rep_c order_trans)
 qed
 
@@ -272,14 +272,14 @@
 lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
 by (induction c c' rule: le_acom.induct) simp_all
 
-lemma mono_step_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
+lemma mono_step'_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
 apply(induction c c' arbitrary: S S' rule: le_acom.induct)
 apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
   split: option.split)
 done
 
-lemma mono_step: "mono (step S)"
-by(simp add: mono_def mono_step_aux[OF le_refl])
+lemma mono_step': "mono (step' S)"
+by(simp add: mono_def mono_step'_aux[OF le_refl])
 
 end
 
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Abs_Int1_ivl.thy
--- a/src/HOL/IMP/Abs_Int1_ivl.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -207,7 +207,7 @@
   Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
-and step_ivl is step
+and step_ivl is step'
 and AI_ivl is AI
 and aval_ivl' is aval''
 proof qed
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -184,23 +184,23 @@
 begin
 
 definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
-"AI_WN = pfp_WN (step \<top>)"
+"AI_WN = pfp_WN (step' \<top>)"
 
 lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV 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]
-  have 2: "step \<top> c' \<sqsubseteq> c'" .
-  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
-  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  assume 1: "pfp_WN (step' \<top>) c = Some c'"
+  from pfp_WN_pfp[OF allI[OF strip_step'] mono_step' 1]
+  have 2: "step' \<top> c' \<sqsubseteq> c'" .
+  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[OF 3])
-    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
-      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_rep_c order_trans)
 qed
 
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Collecting.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -138,21 +138,21 @@
 
 subsubsection "Collecting semantics"
 
-fun step_cs :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
-"step_cs S (SKIP {P}) = (SKIP {S})" |
-"step_cs S (x ::= e {P}) =
+fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
+"step S (SKIP {P}) = (SKIP {S})" |
+"step S (x ::= e {P}) =
   (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
-"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
-"step_cs S (IF b THEN c1 ELSE c2 {P}) =
-   IF b THEN step_cs {s:S. bval b s} c1 ELSE step_cs {s:S. \<not> bval b s} c2
+"step S (c1; c2) = step S c1; step (post c1) c2" |
+"step S (IF b THEN c1 ELSE c2 {P}) =
+   IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2
    {post c1 \<union> post c2}" |
-"step_cs S ({Inv} WHILE b DO c {P}) =
-  {S \<union> post c} WHILE b DO (step_cs {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
+"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 c (step_cs S)"
+"CS S c = lfp c (step S)"
 
-lemma mono_step_cs_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step_cs S x \<le> step_cs T y"
+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)
   case 2 thus ?case by fastforce
 next
@@ -163,15 +163,15 @@
   case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
 qed auto
 
-lemma mono_step_cs: "mono (step_cs S)"
-by(blast intro: monoI mono_step_cs_aux)
+lemma mono_step: "mono (step S)"
+by(blast intro: monoI mono_step_aux)
 
-lemma strip_step_cs: "strip(step_cs S c) = strip c"
+lemma strip_step: "strip(step S c) = strip c"
 by (induction c arbitrary: S) auto
 
-lemmas lfp_cs_unfold = lfp_unfold[OF strip_step_cs mono_step_cs]
+lemmas lfp_cs_unfold = lfp_unfold[OF strip_step mono_step]
 
-lemma CS_unfold: "CS S c = step_cs S (CS S c)"
+lemma CS_unfold: "CS S c = step S (CS S c)"
 by (metis CS_def lfp_cs_unfold)
 
 lemma strip_CS[simp]: "strip(CS S c) = c"
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Collecting1.thy
--- a/src/HOL/IMP/Collecting1.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Collecting1.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -5,221 +5,40 @@
 subsection "A small step semantics on annotated commands"
 
 text{* The idea: the state is propagated through the annotated command as an
-annotation @{term "Some s"}, all other annotations are @{const None}. *}
-
-fun join :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" where
-"join None x = x" |
-"join x None = x"
-
-definition bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> state option \<Rightarrow> state option" where
-"bfilter b r so =
-  (case so of None \<Rightarrow> None | Some s \<Rightarrow> if bval b s = r then Some s else None)"
-
-lemma bfilter_None[simp]: "bfilter b r None = None"
-by(simp add: bfilter_def split: option.split)
-
-fun step1 :: "state option \<Rightarrow> state option acom \<Rightarrow> state option acom" where
-"step1 so (SKIP {P}) = SKIP {so}" |
-"step1 so (x::=e {P}) =
-  x ::= e {case so of None \<Rightarrow> None | Some s \<Rightarrow> Some(s(x := aval e s))}" |
-"step1 so (c1;c2) = step1 so c1; step1 (post c1) c2" |
-"step1 so (IF b THEN c1 ELSE c2 {P}) =
-  IF b THEN step1 (bfilter b True so) c1
-  ELSE step1 (bfilter b False so) c2
-  {join (post c1) (post c2)}" |
-"step1 so ({I} WHILE b DO c {P}) =
-  {join so (post c)}
-  WHILE b DO step1 (bfilter b True I) c
-  {bfilter b False I}"
-
-definition "show_acom xs = map_acom (Option.map (show_state xs))"
-
-definition
- "p1 = ''x'' ::= N 2; IF Less (V ''x'') (N 3) THEN ''x'' ::= N 1 ELSE com.SKIP"
-
-definition "p2 =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
-
-value "show_acom [''x'']
- (((step1 None)^^6) (step1 (Some <>) (anno None p2)))"
-
-subsubsection "Relating the small step and the collecting semantics"
-
-hide_const (open) set
-
-abbreviation set :: "'a option acom \<Rightarrow> 'a set acom" where
-"set == map_acom Option.set"
-
-definition some :: "'a option \<Rightarrow> nat" where
-"some opt = (case opt of Some x \<Rightarrow> 1 | None \<Rightarrow> 0)"
-
-lemma some[simp]: "some None = 0 \<and> some (Some x) = 1"
-by(simp add: some_def split:option.split)
-
-fun somes :: "'a option acom \<Rightarrow> nat" where
-"somes(SKIP {p}) = some p" |
-"somes(x::=e {p}) = some p" |
-"somes(c1;c2) = somes c1 + somes c2" |
-"somes(IF b THEN c1 ELSE c2 {p}) = somes c1 + somes c2 + some p" |
-"somes({i} WHILE b DO c {p}) = some i + somes c + some p"
-
-lemma some_anno_None: "somes(anno None c) = 0"
-by(induction c) auto
-
-lemma some_post: "some(post co) \<le> somes co"
-by(induction co) auto
-
-lemma some_join:
-  "some so1 + some so2 \<le> 1 \<Longrightarrow> some(join so1 so2) = some so1 + some so2"
-by(simp add: some_def split: option.splits)
+annotation @{term "{s}"}, all other annotations are @{term "{}"}. It is easy
+to show that this semantics approximates the collecting semantics. *}
 
-lemma somes_step1: "some so + somes co \<le> 1 \<Longrightarrow>
- somes(step1 so co) + some(post co) = some so + somes co"
-proof(induction co arbitrary: so)
-  case SKIP thus ?case by simp
-next
-  case Assign thus ?case by (simp split:option.split)
-next
-  case (Semi co1 _)
-  from Semi.prems Semi.IH(1)[of so] Semi.IH(2)[of "post co1"]
-  show ?case by simp
-next
-  case (If b)
-  from If.prems If.IH(1)[of "bfilter b True so"]
-       If.prems If.IH(2)[of "bfilter b False so"]
-  show ?case
-    by (auto simp: bfilter_def some_join split:option.split)
-next
-  case (While i b c p)
-  from While.prems While.IH[of "bfilter b True i"]
-  show ?case
-    by(auto simp: bfilter_def some_join split:option.split)
-qed
-
-lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
-by(induction c) auto
-
-lemma join_eq_Some: "some so1 + some so2 \<le> 1 \<Longrightarrow>
-  join so1 so2 = Some s =
- (so1 = Some s & so2 = None | so1 = None & so2 = Some s)"
-apply(cases so1) apply simp
-apply(cases so2) apply auto
-done
-
-lemma set_bfilter:
-  "Option.set (bfilter b r so) = {s : Option.set so. bval b s = r}"
-by(auto simp: bfilter_def split: option.splits)
-
-lemma set_join:  "some so1 + some so2 \<le> 1 \<Longrightarrow>
-  Option.set (join so1 so2) = Option.set so1 \<union> Option.set so2"
-apply(cases so1) apply simp
-apply(cases so2) apply auto
-done
-
-lemma add_le1_iff: "m + n \<le> (Suc 0) \<longleftrightarrow> (m=0 \<and> n\<le>1 | m\<le>1 & n=0)"
-by arith
+lemma step_preserves_le:
+  "\<lbrakk> step S cs = cs; S' \<subseteq> S; cs' \<le> cs \<rbrakk> \<Longrightarrow>
+   step S' cs' \<le> cs"
+by (metis mono_step_aux)
 
-lemma some_0_iff: "some opt = 0 \<longleftrightarrow> opt = None"
-by(auto simp add: some_def split: option.splits)
-
-lemma some_le1[simp]: "some x \<le> Suc 0"
-by(auto simp add: some_def split: option.splits)
-
-lemma step1_preserves_le:
-  "\<lbrakk> step_cs S cs = cs; Option.set so \<subseteq> S; set co \<le> cs;
-    somes co + some so \<le> 1 \<rbrakk> \<Longrightarrow>
-  set(step1 so co) \<le> cs"
-proof(induction co arbitrary: S cs so)
-  case SKIP thus ?case by (clarsimp simp: SKIP_le)
-next
-  case Assign thus ?case by (fastforce simp: Assign_le split: option.splits)
-next
-  case (Semi co1 co2)
-  from Semi.prems show ?case using some_post[of co1]
-    by (fastforce simp add: Semi_le add_le1_iff Semi.IH dest: le_post)
-next
-  case (If _ co1 co2)
-  from If.prems show ?case
-    using some_post[of co1] some_post[of co2]
-    by (fastforce simp: If_le add_le1_iff some_0_iff set_bfilter subset_iff
-      join_eq_Some If.IH dest: le_post)
-next
-  case (While _ _ co)
-  from While.prems show ?case
-    using some_post[of co]
-    by (fastforce simp: While_le set_bfilter subset_iff join_eq_Some
-      add_le1_iff some_0_iff While.IH dest: le_post)
-qed
-
-lemma step1_None_preserves_le:
-  "\<lbrakk> step_cs S cs = cs; set co \<le> cs; somes co \<le> 1 \<rbrakk> \<Longrightarrow>
-  set(step1 None co) \<le> cs"
-by(auto dest: step1_preserves_le[of _ _ None])
-
-lemma step1_Some_preserves_le:
-  "\<lbrakk> step_cs S cs = cs; s : S; set co \<le> cs; somes co = 0 \<rbrakk> \<Longrightarrow>
-  set(step1 (Some s) co) \<le> cs"
-by(auto dest: step1_preserves_le[of _ _ "Some s"])
-
-lemma steps_None_preserves_le: assumes "step_cs S cs = cs"
-shows "set co \<le> cs \<Longrightarrow> somes co \<le> 1 \<Longrightarrow> set ((step1 None ^^ n) co) \<le> cs"
-proof(induction n arbitrary: co)
+lemma steps_empty_preserves_le: assumes "step S cs = cs"
+shows "cs' \<le> cs \<Longrightarrow> (step {} ^^ n) cs' \<le> cs"
+proof(induction n arbitrary: cs')
   case 0 thus ?case by simp
 next
   case (Suc n) thus ?case
-    using somes_step1[of None co] step1_None_preserves_le[OF assms Suc.prems]
-    by(simp add:funpow_swap1 Suc.IH)
+    using Suc.IH[OF step_preserves_le[OF assms empty_subsetI Suc.prems]]
+    by(simp add:funpow_swap1)
 qed
 
 
-definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state option acom" where
-"steps s c n = ((step1 None)^^n) (step1 (Some s) (anno None c))"
+definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state set acom" where
+"steps s c n = ((step {})^^n) (step {s} (anno {} c))"
 
-lemma steps_approx_fix_step_cs: assumes "step_cs S cs = cs" and "s:S"
-shows "set (steps s (strip cs) n) \<le> cs"
+lemma steps_approx_fix_step: assumes "step S cs = cs" and "s:S"
+shows "steps s (strip cs) n \<le> cs"
 proof-
-  { fix c have "somes (anno None c) = 0" by(induction c) auto }
-  note somes_None = this
-  let ?cNone = "anno None (strip cs)"
-  have "set ?cNone \<le> cs" by(induction cs) auto
-  from step1_Some_preserves_le[OF assms this somes_None]
-  have 1: "set(step1 (Some s) ?cNone) \<le> cs" .
-  have 2: "somes (step1 (Some s) ?cNone) \<le> 1"
-    using some_post somes_step1[of "Some s" ?cNone]
-    by (simp add:some_anno_None[of "strip cs"])
-  from steps_None_preserves_le[OF assms(1) 1 2]
+  let ?bot = "anno {} (strip cs)"
+  have "?bot \<le> cs" by(induction cs) auto
+  from step_preserves_le[OF assms(1)_ this, of "{s}"] `s:S`
+  have 1: "step {s} ?bot \<le> cs" by simp
+  from steps_empty_preserves_le[OF assms(1) 1]
   show ?thesis by(simp add: steps_def)
 qed
 
-theorem steps_approx_CS: "s:S \<Longrightarrow> set (steps s c n) \<le> CS S c"
-by (metis CS_unfold steps_approx_fix_step_cs strip_CS)
-
-lemma While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
-by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
-
-lemma step_cs_complete:
-  "\<lbrakk> step_cs S c = c; (strip c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post c"
-proof(induction c arbitrary: S s t)
-  case (While Inv b c P)
-  from While.prems have inv: "step_cs {s:Inv. bval b s} c = c"
-    and "post c \<subseteq> Inv" and "S \<subseteq> Inv" and "{s:Inv. \<not> bval b s} \<subseteq> P"  by(auto)
-  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s : Inv \<Longrightarrow> t : Inv"
-    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by simp
-    next
-      case (WhileTrue s1 s2 s3)
-      from WhileTrue.hyps(5) While.IH[OF inv `(strip c, s1) \<Rightarrow> s2`]
-        `s1 : Inv` `post c \<subseteq> Inv` `bval b s1`
-      show ?case by auto
-    qed
-  } note Inv = this
-  from  While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
-    by(auto dest: While_final_False)
-  from Inv[OF this(1)] `s : S` `S \<subseteq> Inv` have "t : Inv" by blast
-  with `{s:Inv. \<not> bval b s} \<subseteq> P` show ?case using `\<not> bval b t` by auto
-qed auto
-
-theorem CS_complete: "\<lbrakk> (c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post(CS S c)"
-by (metis CS_unfold step_cs_complete strip_CS)
+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)
 
 end
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/Collecting_list.thy
--- a/src/HOL/IMP/Collecting_list.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Collecting_list.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -4,22 +4,28 @@
 
 subsection "Executable Collecting Semantics on lists"
 
-fun step_cs :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where
-"step_cs S (SKIP {P}) = (SKIP {S})" |
-"step_cs S (x ::= e {P}) =
+fun step :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where
+"step S (SKIP {P}) = (SKIP {S})" |
+"step S (x ::= e {P}) =
   (x ::= e {[s(x := aval e s). s \<leftarrow> S]})" |
-"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
-"step_cs S (IF b THEN c1 ELSE c2 {P}) =
-   IF b THEN step_cs [s \<leftarrow> S. bval b s] c1 ELSE step_cs [s\<leftarrow>S. \<not> bval b s] c2
+"step S (c1; c2) = step S c1; step (post c1) c2" |
+"step S (IF b THEN c1 ELSE c2 {P}) =
+   IF b THEN step [s \<leftarrow> S. bval b s] c1 ELSE step [s\<leftarrow>S. \<not> bval b s] c2
    {post c1 @ post c2}" |
-"step_cs S ({Inv} WHILE b DO c {P}) =
-  {S @ post c} WHILE b DO (step_cs [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
+"step S ({Inv} WHILE b DO c {P}) =
+  {S @ post c} WHILE b DO (step [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
 
 definition "c = WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
 definition "c0 = anno [] c"
 
 definition "show_acom xs = map_acom (map (show_state xs))"
 
-value "show_acom [''x''] (((step_cs [<>]) ^^ 6) c0)"
+text{* Collecting semantics: *}
+
+value "show_acom [''x''] (((step [<>]) ^^ 6) c0)"
+
+text{* Small step semantics: *}
+
+value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))"
 
 end
diff -r 8634b4e61b88 -r a49f9428aba4 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/ROOT.ML	Sun Nov 27 13:31:52 2011 +0100
@@ -19,6 +19,8 @@
  "VC",
  "HoareT",
  "Abs_Int2",
+ "Collecting1",
+ "Collecting_list",
  "Abs_Int_Den/Abs_Int_den2",
  "Procs_Dyn_Vars_Dyn",
  "Procs_Stat_Vars_Dyn",