merged
authornipkow
Sun Nov 27 13:32:20 2011 +0100 (2011-11-27)
changeset 45656003a01272d28
parent 45646 02afa20cf397
parent 45655 a49f9428aba4
child 45657 862d68ee10f3
merged
     1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Sun Nov 27 13:12:42 2011 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Sun Nov 27 13:32:20 2011 +0100
     1.3 @@ -25,22 +25,22 @@
     1.4  locale Abs_Int = Val_abs
     1.5  begin
     1.6  
     1.7 -fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
     1.8 -"step S (SKIP {P}) = (SKIP {S})" |
     1.9 -"step S (x ::= e {P}) =
    1.10 +fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
    1.11 +"step' S (SKIP {P}) = (SKIP {S})" |
    1.12 +"step' S (x ::= e {P}) =
    1.13    x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
    1.14 -"step S (c1; c2) = step S c1; step (post c1) c2" |
    1.15 -"step S (IF b THEN c1 ELSE c2 {P}) =
    1.16 -  (let c1' = step S c1; c2' = step S c2
    1.17 +"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
    1.18 +"step' S (IF b THEN c1 ELSE c2 {P}) =
    1.19 +  (let c1' = step' S c1; c2' = step' S c2
    1.20     in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
    1.21 -"step S ({Inv} WHILE b DO c {P}) =
    1.22 -   {S \<squnion> post c} WHILE b DO step Inv c {Inv}"
    1.23 +"step' S ({Inv} WHILE b DO c {P}) =
    1.24 +   {S \<squnion> post c} WHILE b DO step' Inv c {Inv}"
    1.25  
    1.26  definition AI :: "com \<Rightarrow> 'a st option acom option" where
    1.27 -"AI = lpfp\<^isub>c (step \<top>)"
    1.28 +"AI = lpfp\<^isub>c (step' \<top>)"
    1.29  
    1.30  
    1.31 -lemma strip_step[simp]: "strip(step S c) = strip c"
    1.32 +lemma strip_step'[simp]: "strip(step' S c) = strip c"
    1.33  by(induct c arbitrary: S) (simp_all add: Let_def)
    1.34  
    1.35  
    1.36 @@ -55,7 +55,7 @@
    1.37  
    1.38  lemma step_preserves_le2:
    1.39    "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
    1.40 -   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
    1.41 +   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
    1.42  proof(induction c arbitrary: cs ca S sa)
    1.43    case SKIP thus ?case
    1.44      by(auto simp:strip_eq_SKIP)
    1.45 @@ -93,24 +93,24 @@
    1.46  
    1.47  lemma step_preserves_le:
    1.48    "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
    1.49 -   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
    1.50 +   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
    1.51  by (metis le_strip step_preserves_le2 strip_acom)
    1.52  
    1.53  lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
    1.54  proof(simp add: CS_def AI_def)
    1.55 -  assume 1: "lpfp\<^isub>c (step \<top>) c = Some c'"
    1.56 -  have 2: "step \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
    1.57 -  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c"
    1.58 +  assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
    1.59 +  have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
    1.60 +  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
    1.61      by(simp add: strip_lpfpc[OF _ 1])
    1.62 -  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
    1.63 +  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    1.64    proof(rule lfp_lowerbound[OF 3])
    1.65 -    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
    1.66 +    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    1.67      proof(rule step_preserves_le[OF _ _ 3])
    1.68        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
    1.69 -      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    1.70 +      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    1.71      qed
    1.72    qed
    1.73 -  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
    1.74 +  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
    1.75      by (blast intro: mono_rep_c order_trans)
    1.76  qed
    1.77  
    1.78 @@ -129,7 +129,7 @@
    1.79  lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
    1.80  by(auto simp add: le_st_def lookup_def update_def)
    1.81  
    1.82 -lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
    1.83 +lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
    1.84  apply(induction c arbitrary: S S')
    1.85  apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
    1.86  done
     2.1 --- a/src/HOL/IMP/Abs_Int0_const.thy	Sun Nov 27 13:12:42 2011 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int0_const.thy	Sun Nov 27 13:32:20 2011 +0100
     2.3 @@ -68,7 +68,7 @@
     2.4  
     2.5  interpretation Abs_Int rep_cval Const plus_cval
     2.6  defines AI_const is AI
     2.7 -and step_const is step
     2.8 +and step_const is step'
     2.9  proof qed
    2.10  
    2.11  
     3.1 --- a/src/HOL/IMP/Abs_Int0_fun.thy	Sun Nov 27 13:12:42 2011 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int0_fun.thy	Sun Nov 27 13:32:20 2011 +0100
     3.3 @@ -253,22 +253,22 @@
     3.4  "aval' (V x) S = S x" |
     3.5  "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
     3.6  
     3.7 -fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
     3.8 +fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
     3.9   where
    3.10 -"step S (SKIP {P}) = (SKIP {S})" |
    3.11 -"step S (x ::= e {P}) =
    3.12 +"step' S (SKIP {P}) = (SKIP {S})" |
    3.13 +"step' S (x ::= e {P}) =
    3.14    x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" |
    3.15 -"step S (c1; c2) = step S c1; step (post c1) c2" |
    3.16 -"step S (IF b THEN c1 ELSE c2 {P}) =
    3.17 -   IF b THEN step S c1 ELSE step S c2 {post c1 \<squnion> post c2}" |
    3.18 -"step S ({Inv} WHILE b DO c {P}) =
    3.19 -  {S \<squnion> post c} WHILE b DO (step Inv c) {Inv}"
    3.20 +"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
    3.21 +"step' S (IF b THEN c1 ELSE c2 {P}) =
    3.22 +   IF b THEN step' S c1 ELSE step' S c2 {post c1 \<squnion> post c2}" |
    3.23 +"step' S ({Inv} WHILE b DO c {P}) =
    3.24 +  {S \<squnion> post c} WHILE b DO (step' Inv c) {Inv}"
    3.25  
    3.26  definition AI :: "com \<Rightarrow> 'a st option acom option" where
    3.27 -"AI = lpfp\<^isub>c (step \<top>)"
    3.28 +"AI = lpfp\<^isub>c (step' \<top>)"
    3.29  
    3.30  
    3.31 -lemma strip_step[simp]: "strip(step S c) = strip c"
    3.32 +lemma strip_step'[simp]: "strip(step' S c) = strip c"
    3.33  by(induct c arbitrary: S) (simp_all add: Let_def)
    3.34  
    3.35  
    3.36 @@ -310,7 +310,7 @@
    3.37  
    3.38  lemma step_preserves_le2:
    3.39    "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
    3.40 -   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
    3.41 +   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
    3.42  proof(induction c arbitrary: cs ca S sa)
    3.43    case SKIP thus ?case
    3.44      by(auto simp:strip_eq_SKIP)
    3.45 @@ -348,24 +348,24 @@
    3.46  
    3.47  lemma step_preserves_le:
    3.48    "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
    3.49 -   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
    3.50 +   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
    3.51  by (metis le_strip step_preserves_le2 strip_acom)
    3.52  
    3.53  lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
    3.54  proof(simp add: CS_def AI_def)
    3.55 -  assume 1: "lpfp\<^isub>c (step \<top>) c = Some c'"
    3.56 -  have 2: "step \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
    3.57 -  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c"
    3.58 +  assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
    3.59 +  have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
    3.60 +  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
    3.61      by(simp add: strip_lpfpc[OF _ 1])
    3.62 -  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
    3.63 +  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    3.64    proof(rule lfp_lowerbound[OF 3])
    3.65 -    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
    3.66 +    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    3.67      proof(rule step_preserves_le[OF _ _ 3])
    3.68        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
    3.69 -      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    3.70 +      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    3.71      qed
    3.72    qed
    3.73 -  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
    3.74 +  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
    3.75      by (blast intro: mono_rep_c order_trans)
    3.76  qed
    3.77  
    3.78 @@ -384,7 +384,7 @@
    3.79  lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
    3.80  by(simp add: le_fun_def)
    3.81  
    3.82 -lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
    3.83 +lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
    3.84  apply(induction c arbitrary: S S')
    3.85  apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
    3.86  done
     4.1 --- a/src/HOL/IMP/Abs_Int1.thy	Sun Nov 27 13:12:42 2011 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Sun Nov 27 13:32:20 2011 +0100
     4.3 @@ -139,24 +139,24 @@
     4.4  qed
     4.5  
     4.6  
     4.7 -fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
     4.8 +fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
     4.9   where
    4.10 -"step S (SKIP {P}) = (SKIP {S})" |
    4.11 -"step S (x ::= e {P}) =
    4.12 +"step' S (SKIP {P}) = (SKIP {S})" |
    4.13 +"step' S (x ::= e {P}) =
    4.14    x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
    4.15 -"step S (c1; c2) = step S c1; step (post c1) c2" |
    4.16 -"step S (IF b THEN c1 ELSE c2 {P}) =
    4.17 -  (let c1' = step (bfilter b True S) c1; c2' = step (bfilter b False S) c2
    4.18 +"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
    4.19 +"step' S (IF b THEN c1 ELSE c2 {P}) =
    4.20 +  (let c1' = step' (bfilter b True S) c1; c2' = step' (bfilter b False S) c2
    4.21     in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
    4.22 -"step S ({Inv} WHILE b DO c {P}) =
    4.23 +"step' S ({Inv} WHILE b DO c {P}) =
    4.24     {S \<squnion> post c}
    4.25 -   WHILE b DO step (bfilter b True Inv) c
    4.26 +   WHILE b DO step' (bfilter b True Inv) c
    4.27     {bfilter b False Inv}"
    4.28  
    4.29  definition AI :: "com \<Rightarrow> 'a st option acom option" where
    4.30 -"AI = lpfp\<^isub>c (step \<top>)"
    4.31 +"AI = lpfp\<^isub>c (step' \<top>)"
    4.32  
    4.33 -lemma strip_step[simp]: "strip(step S c) = strip c"
    4.34 +lemma strip_step'[simp]: "strip(step' S c) = strip c"
    4.35  by(induct c arbitrary: S) (simp_all add: Let_def)
    4.36  
    4.37  
    4.38 @@ -169,7 +169,7 @@
    4.39  
    4.40  lemma step_preserves_le2:
    4.41    "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
    4.42 -   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
    4.43 +   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' sa ca)"
    4.44  proof(induction c arbitrary: cs ca S sa)
    4.45    case SKIP thus ?case
    4.46      by(auto simp:strip_eq_SKIP)
    4.47 @@ -208,24 +208,24 @@
    4.48  
    4.49  lemma step_preserves_le:
    4.50    "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
    4.51 -   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
    4.52 +   \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c(step' sa ca)"
    4.53  by (metis le_strip step_preserves_le2 strip_acom)
    4.54  
    4.55  lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
    4.56  proof(simp add: CS_def AI_def)
    4.57 -  assume 1: "lpfp\<^isub>c (step \<top>) c = Some c'"
    4.58 -  have 2: "step \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
    4.59 -  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c"
    4.60 +  assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
    4.61 +  have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
    4.62 +  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
    4.63      by(simp add: strip_lpfpc[OF _ 1])
    4.64 -  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
    4.65 +  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    4.66    proof(rule lfp_lowerbound[OF 3])
    4.67 -    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
    4.68 +    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    4.69      proof(rule step_preserves_le[OF _ _ 3])
    4.70        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
    4.71 -      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    4.72 +      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    4.73      qed
    4.74    qed
    4.75 -  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
    4.76 +  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
    4.77      by (blast intro: mono_rep_c order_trans)
    4.78  qed
    4.79  
    4.80 @@ -272,14 +272,14 @@
    4.81  lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
    4.82  by (induction c c' rule: le_acom.induct) simp_all
    4.83  
    4.84 -lemma mono_step_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
    4.85 +lemma mono_step'_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
    4.86  apply(induction c c' arbitrary: S S' rule: le_acom.induct)
    4.87  apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
    4.88    split: option.split)
    4.89  done
    4.90  
    4.91 -lemma mono_step: "mono (step S)"
    4.92 -by(simp add: mono_def mono_step_aux[OF le_refl])
    4.93 +lemma mono_step': "mono (step' S)"
    4.94 +by(simp add: mono_def mono_step'_aux[OF le_refl])
    4.95  
    4.96  end
    4.97  
     5.1 --- a/src/HOL/IMP/Abs_Int1_ivl.thy	Sun Nov 27 13:12:42 2011 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Sun Nov 27 13:32:20 2011 +0100
     5.3 @@ -207,7 +207,7 @@
     5.4    Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
     5.5  defines afilter_ivl is afilter
     5.6  and bfilter_ivl is bfilter
     5.7 -and step_ivl is step
     5.8 +and step_ivl is step'
     5.9  and AI_ivl is AI
    5.10  and aval_ivl' is aval''
    5.11  proof qed
     6.1 --- a/src/HOL/IMP/Abs_Int2.thy	Sun Nov 27 13:12:42 2011 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Sun Nov 27 13:32:20 2011 +0100
     6.3 @@ -184,23 +184,23 @@
     6.4  begin
     6.5  
     6.6  definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
     6.7 -"AI_WN = pfp_WN (step \<top>)"
     6.8 +"AI_WN = pfp_WN (step' \<top>)"
     6.9  
    6.10  lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
    6.11  proof(simp add: CS_def AI_WN_def)
    6.12 -  assume 1: "pfp_WN (step \<top>) c = Some c'"
    6.13 -  from pfp_WN_pfp[OF allI[OF strip_step] mono_step 1]
    6.14 -  have 2: "step \<top> c' \<sqsubseteq> c'" .
    6.15 -  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
    6.16 -  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
    6.17 +  assume 1: "pfp_WN (step' \<top>) c = Some c'"
    6.18 +  from pfp_WN_pfp[OF allI[OF strip_step'] mono_step' 1]
    6.19 +  have 2: "step' \<top> c' \<sqsubseteq> c'" .
    6.20 +  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
    6.21 +  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    6.22    proof(rule lfp_lowerbound[OF 3])
    6.23 -    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
    6.24 +    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    6.25      proof(rule step_preserves_le[OF _ _ 3])
    6.26        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
    6.27 -      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    6.28 +      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
    6.29      qed
    6.30    qed
    6.31 -  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
    6.32 +  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
    6.33      by (blast intro: mono_rep_c order_trans)
    6.34  qed
    6.35  
     7.1 --- a/src/HOL/IMP/Collecting.thy	Sun Nov 27 13:12:42 2011 +0100
     7.2 +++ b/src/HOL/IMP/Collecting.thy	Sun Nov 27 13:32:20 2011 +0100
     7.3 @@ -138,21 +138,21 @@
     7.4  
     7.5  subsubsection "Collecting semantics"
     7.6  
     7.7 -fun step_cs :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
     7.8 -"step_cs S (SKIP {P}) = (SKIP {S})" |
     7.9 -"step_cs S (x ::= e {P}) =
    7.10 +fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
    7.11 +"step S (SKIP {P}) = (SKIP {S})" |
    7.12 +"step S (x ::= e {P}) =
    7.13    (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
    7.14 -"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
    7.15 -"step_cs S (IF b THEN c1 ELSE c2 {P}) =
    7.16 -   IF b THEN step_cs {s:S. bval b s} c1 ELSE step_cs {s:S. \<not> bval b s} c2
    7.17 +"step S (c1; c2) = step S c1; step (post c1) c2" |
    7.18 +"step S (IF b THEN c1 ELSE c2 {P}) =
    7.19 +   IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2
    7.20     {post c1 \<union> post c2}" |
    7.21 -"step_cs S ({Inv} WHILE b DO c {P}) =
    7.22 -  {S \<union> post c} WHILE b DO (step_cs {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
    7.23 +"step S ({Inv} WHILE b DO c {P}) =
    7.24 +  {S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
    7.25  
    7.26  definition CS :: "state set \<Rightarrow> com \<Rightarrow> state set acom" where
    7.27 -"CS S c = lfp c (step_cs S)"
    7.28 +"CS S c = lfp c (step S)"
    7.29  
    7.30 -lemma mono_step_cs_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step_cs S x \<le> step_cs T y"
    7.31 +lemma mono_step_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step S x \<le> step T y"
    7.32  proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
    7.33    case 2 thus ?case by fastforce
    7.34  next
    7.35 @@ -163,15 +163,15 @@
    7.36    case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
    7.37  qed auto
    7.38  
    7.39 -lemma mono_step_cs: "mono (step_cs S)"
    7.40 -by(blast intro: monoI mono_step_cs_aux)
    7.41 +lemma mono_step: "mono (step S)"
    7.42 +by(blast intro: monoI mono_step_aux)
    7.43  
    7.44 -lemma strip_step_cs: "strip(step_cs S c) = strip c"
    7.45 +lemma strip_step: "strip(step S c) = strip c"
    7.46  by (induction c arbitrary: S) auto
    7.47  
    7.48 -lemmas lfp_cs_unfold = lfp_unfold[OF strip_step_cs mono_step_cs]
    7.49 +lemmas lfp_cs_unfold = lfp_unfold[OF strip_step mono_step]
    7.50  
    7.51 -lemma CS_unfold: "CS S c = step_cs S (CS S c)"
    7.52 +lemma CS_unfold: "CS S c = step S (CS S c)"
    7.53  by (metis CS_def lfp_cs_unfold)
    7.54  
    7.55  lemma strip_CS[simp]: "strip(CS S c) = c"
     8.1 --- a/src/HOL/IMP/Collecting1.thy	Sun Nov 27 13:12:42 2011 +0100
     8.2 +++ b/src/HOL/IMP/Collecting1.thy	Sun Nov 27 13:32:20 2011 +0100
     8.3 @@ -5,221 +5,40 @@
     8.4  subsection "A small step semantics on annotated commands"
     8.5  
     8.6  text{* The idea: the state is propagated through the annotated command as an
     8.7 -annotation @{term "Some s"}, all other annotations are @{const None}. *}
     8.8 -
     8.9 -fun join :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" where
    8.10 -"join None x = x" |
    8.11 -"join x None = x"
    8.12 -
    8.13 -definition bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> state option \<Rightarrow> state option" where
    8.14 -"bfilter b r so =
    8.15 -  (case so of None \<Rightarrow> None | Some s \<Rightarrow> if bval b s = r then Some s else None)"
    8.16 -
    8.17 -lemma bfilter_None[simp]: "bfilter b r None = None"
    8.18 -by(simp add: bfilter_def split: option.split)
    8.19 -
    8.20 -fun step1 :: "state option \<Rightarrow> state option acom \<Rightarrow> state option acom" where
    8.21 -"step1 so (SKIP {P}) = SKIP {so}" |
    8.22 -"step1 so (x::=e {P}) =
    8.23 -  x ::= e {case so of None \<Rightarrow> None | Some s \<Rightarrow> Some(s(x := aval e s))}" |
    8.24 -"step1 so (c1;c2) = step1 so c1; step1 (post c1) c2" |
    8.25 -"step1 so (IF b THEN c1 ELSE c2 {P}) =
    8.26 -  IF b THEN step1 (bfilter b True so) c1
    8.27 -  ELSE step1 (bfilter b False so) c2
    8.28 -  {join (post c1) (post c2)}" |
    8.29 -"step1 so ({I} WHILE b DO c {P}) =
    8.30 -  {join so (post c)}
    8.31 -  WHILE b DO step1 (bfilter b True I) c
    8.32 -  {bfilter b False I}"
    8.33 -
    8.34 -definition "show_acom xs = map_acom (Option.map (show_state xs))"
    8.35 -
    8.36 -definition
    8.37 - "p1 = ''x'' ::= N 2; IF Less (V ''x'') (N 3) THEN ''x'' ::= N 1 ELSE com.SKIP"
    8.38 -
    8.39 -definition "p2 =
    8.40 - ''x'' ::= N 0; WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
    8.41 -
    8.42 -value "show_acom [''x'']
    8.43 - (((step1 None)^^6) (step1 (Some <>) (anno None p2)))"
    8.44 -
    8.45 -subsubsection "Relating the small step and the collecting semantics"
    8.46 -
    8.47 -hide_const (open) set
    8.48 -
    8.49 -abbreviation set :: "'a option acom \<Rightarrow> 'a set acom" where
    8.50 -"set == map_acom Option.set"
    8.51 -
    8.52 -definition some :: "'a option \<Rightarrow> nat" where
    8.53 -"some opt = (case opt of Some x \<Rightarrow> 1 | None \<Rightarrow> 0)"
    8.54 -
    8.55 -lemma some[simp]: "some None = 0 \<and> some (Some x) = 1"
    8.56 -by(simp add: some_def split:option.split)
    8.57 -
    8.58 -fun somes :: "'a option acom \<Rightarrow> nat" where
    8.59 -"somes(SKIP {p}) = some p" |
    8.60 -"somes(x::=e {p}) = some p" |
    8.61 -"somes(c1;c2) = somes c1 + somes c2" |
    8.62 -"somes(IF b THEN c1 ELSE c2 {p}) = somes c1 + somes c2 + some p" |
    8.63 -"somes({i} WHILE b DO c {p}) = some i + somes c + some p"
    8.64 -
    8.65 -lemma some_anno_None: "somes(anno None c) = 0"
    8.66 -by(induction c) auto
    8.67 -
    8.68 -lemma some_post: "some(post co) \<le> somes co"
    8.69 -by(induction co) auto
    8.70 -
    8.71 -lemma some_join:
    8.72 -  "some so1 + some so2 \<le> 1 \<Longrightarrow> some(join so1 so2) = some so1 + some so2"
    8.73 -by(simp add: some_def split: option.splits)
    8.74 +annotation @{term "{s}"}, all other annotations are @{term "{}"}. It is easy
    8.75 +to show that this semantics approximates the collecting semantics. *}
    8.76  
    8.77 -lemma somes_step1: "some so + somes co \<le> 1 \<Longrightarrow>
    8.78 - somes(step1 so co) + some(post co) = some so + somes co"
    8.79 -proof(induction co arbitrary: so)
    8.80 -  case SKIP thus ?case by simp
    8.81 -next
    8.82 -  case Assign thus ?case by (simp split:option.split)
    8.83 -next
    8.84 -  case (Semi co1 _)
    8.85 -  from Semi.prems Semi.IH(1)[of so] Semi.IH(2)[of "post co1"]
    8.86 -  show ?case by simp
    8.87 -next
    8.88 -  case (If b)
    8.89 -  from If.prems If.IH(1)[of "bfilter b True so"]
    8.90 -       If.prems If.IH(2)[of "bfilter b False so"]
    8.91 -  show ?case
    8.92 -    by (auto simp: bfilter_def some_join split:option.split)
    8.93 -next
    8.94 -  case (While i b c p)
    8.95 -  from While.prems While.IH[of "bfilter b True i"]
    8.96 -  show ?case
    8.97 -    by(auto simp: bfilter_def some_join split:option.split)
    8.98 -qed
    8.99 -
   8.100 -lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
   8.101 -by(induction c) auto
   8.102 -
   8.103 -lemma join_eq_Some: "some so1 + some so2 \<le> 1 \<Longrightarrow>
   8.104 -  join so1 so2 = Some s =
   8.105 - (so1 = Some s & so2 = None | so1 = None & so2 = Some s)"
   8.106 -apply(cases so1) apply simp
   8.107 -apply(cases so2) apply auto
   8.108 -done
   8.109 -
   8.110 -lemma set_bfilter:
   8.111 -  "Option.set (bfilter b r so) = {s : Option.set so. bval b s = r}"
   8.112 -by(auto simp: bfilter_def split: option.splits)
   8.113 -
   8.114 -lemma set_join:  "some so1 + some so2 \<le> 1 \<Longrightarrow>
   8.115 -  Option.set (join so1 so2) = Option.set so1 \<union> Option.set so2"
   8.116 -apply(cases so1) apply simp
   8.117 -apply(cases so2) apply auto
   8.118 -done
   8.119 -
   8.120 -lemma add_le1_iff: "m + n \<le> (Suc 0) \<longleftrightarrow> (m=0 \<and> n\<le>1 | m\<le>1 & n=0)"
   8.121 -by arith
   8.122 +lemma step_preserves_le:
   8.123 +  "\<lbrakk> step S cs = cs; S' \<subseteq> S; cs' \<le> cs \<rbrakk> \<Longrightarrow>
   8.124 +   step S' cs' \<le> cs"
   8.125 +by (metis mono_step_aux)
   8.126  
   8.127 -lemma some_0_iff: "some opt = 0 \<longleftrightarrow> opt = None"
   8.128 -by(auto simp add: some_def split: option.splits)
   8.129 -
   8.130 -lemma some_le1[simp]: "some x \<le> Suc 0"
   8.131 -by(auto simp add: some_def split: option.splits)
   8.132 -
   8.133 -lemma step1_preserves_le:
   8.134 -  "\<lbrakk> step_cs S cs = cs; Option.set so \<subseteq> S; set co \<le> cs;
   8.135 -    somes co + some so \<le> 1 \<rbrakk> \<Longrightarrow>
   8.136 -  set(step1 so co) \<le> cs"
   8.137 -proof(induction co arbitrary: S cs so)
   8.138 -  case SKIP thus ?case by (clarsimp simp: SKIP_le)
   8.139 -next
   8.140 -  case Assign thus ?case by (fastforce simp: Assign_le split: option.splits)
   8.141 -next
   8.142 -  case (Semi co1 co2)
   8.143 -  from Semi.prems show ?case using some_post[of co1]
   8.144 -    by (fastforce simp add: Semi_le add_le1_iff Semi.IH dest: le_post)
   8.145 -next
   8.146 -  case (If _ co1 co2)
   8.147 -  from If.prems show ?case
   8.148 -    using some_post[of co1] some_post[of co2]
   8.149 -    by (fastforce simp: If_le add_le1_iff some_0_iff set_bfilter subset_iff
   8.150 -      join_eq_Some If.IH dest: le_post)
   8.151 -next
   8.152 -  case (While _ _ co)
   8.153 -  from While.prems show ?case
   8.154 -    using some_post[of co]
   8.155 -    by (fastforce simp: While_le set_bfilter subset_iff join_eq_Some
   8.156 -      add_le1_iff some_0_iff While.IH dest: le_post)
   8.157 -qed
   8.158 -
   8.159 -lemma step1_None_preserves_le:
   8.160 -  "\<lbrakk> step_cs S cs = cs; set co \<le> cs; somes co \<le> 1 \<rbrakk> \<Longrightarrow>
   8.161 -  set(step1 None co) \<le> cs"
   8.162 -by(auto dest: step1_preserves_le[of _ _ None])
   8.163 -
   8.164 -lemma step1_Some_preserves_le:
   8.165 -  "\<lbrakk> step_cs S cs = cs; s : S; set co \<le> cs; somes co = 0 \<rbrakk> \<Longrightarrow>
   8.166 -  set(step1 (Some s) co) \<le> cs"
   8.167 -by(auto dest: step1_preserves_le[of _ _ "Some s"])
   8.168 -
   8.169 -lemma steps_None_preserves_le: assumes "step_cs S cs = cs"
   8.170 -shows "set co \<le> cs \<Longrightarrow> somes co \<le> 1 \<Longrightarrow> set ((step1 None ^^ n) co) \<le> cs"
   8.171 -proof(induction n arbitrary: co)
   8.172 +lemma steps_empty_preserves_le: assumes "step S cs = cs"
   8.173 +shows "cs' \<le> cs \<Longrightarrow> (step {} ^^ n) cs' \<le> cs"
   8.174 +proof(induction n arbitrary: cs')
   8.175    case 0 thus ?case by simp
   8.176  next
   8.177    case (Suc n) thus ?case
   8.178 -    using somes_step1[of None co] step1_None_preserves_le[OF assms Suc.prems]
   8.179 -    by(simp add:funpow_swap1 Suc.IH)
   8.180 +    using Suc.IH[OF step_preserves_le[OF assms empty_subsetI Suc.prems]]
   8.181 +    by(simp add:funpow_swap1)
   8.182  qed
   8.183  
   8.184  
   8.185 -definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state option acom" where
   8.186 -"steps s c n = ((step1 None)^^n) (step1 (Some s) (anno None c))"
   8.187 +definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state set acom" where
   8.188 +"steps s c n = ((step {})^^n) (step {s} (anno {} c))"
   8.189  
   8.190 -lemma steps_approx_fix_step_cs: assumes "step_cs S cs = cs" and "s:S"
   8.191 -shows "set (steps s (strip cs) n) \<le> cs"
   8.192 +lemma steps_approx_fix_step: assumes "step S cs = cs" and "s:S"
   8.193 +shows "steps s (strip cs) n \<le> cs"
   8.194  proof-
   8.195 -  { fix c have "somes (anno None c) = 0" by(induction c) auto }
   8.196 -  note somes_None = this
   8.197 -  let ?cNone = "anno None (strip cs)"
   8.198 -  have "set ?cNone \<le> cs" by(induction cs) auto
   8.199 -  from step1_Some_preserves_le[OF assms this somes_None]
   8.200 -  have 1: "set(step1 (Some s) ?cNone) \<le> cs" .
   8.201 -  have 2: "somes (step1 (Some s) ?cNone) \<le> 1"
   8.202 -    using some_post somes_step1[of "Some s" ?cNone]
   8.203 -    by (simp add:some_anno_None[of "strip cs"])
   8.204 -  from steps_None_preserves_le[OF assms(1) 1 2]
   8.205 +  let ?bot = "anno {} (strip cs)"
   8.206 +  have "?bot \<le> cs" by(induction cs) auto
   8.207 +  from step_preserves_le[OF assms(1)_ this, of "{s}"] `s:S`
   8.208 +  have 1: "step {s} ?bot \<le> cs" by simp
   8.209 +  from steps_empty_preserves_le[OF assms(1) 1]
   8.210    show ?thesis by(simp add: steps_def)
   8.211  qed
   8.212  
   8.213 -theorem steps_approx_CS: "s:S \<Longrightarrow> set (steps s c n) \<le> CS S c"
   8.214 -by (metis CS_unfold steps_approx_fix_step_cs strip_CS)
   8.215 -
   8.216 -lemma While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
   8.217 -by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
   8.218 -
   8.219 -lemma step_cs_complete:
   8.220 -  "\<lbrakk> step_cs S c = c; (strip c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post c"
   8.221 -proof(induction c arbitrary: S s t)
   8.222 -  case (While Inv b c P)
   8.223 -  from While.prems have inv: "step_cs {s:Inv. bval b s} c = c"
   8.224 -    and "post c \<subseteq> Inv" and "S \<subseteq> Inv" and "{s:Inv. \<not> bval b s} \<subseteq> P"  by(auto)
   8.225 -  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s : Inv \<Longrightarrow> t : Inv"
   8.226 -    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
   8.227 -      case WhileFalse thus ?case by simp
   8.228 -    next
   8.229 -      case (WhileTrue s1 s2 s3)
   8.230 -      from WhileTrue.hyps(5) While.IH[OF inv `(strip c, s1) \<Rightarrow> s2`]
   8.231 -        `s1 : Inv` `post c \<subseteq> Inv` `bval b s1`
   8.232 -      show ?case by auto
   8.233 -    qed
   8.234 -  } note Inv = this
   8.235 -  from  While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
   8.236 -    by(auto dest: While_final_False)
   8.237 -  from Inv[OF this(1)] `s : S` `S \<subseteq> Inv` have "t : Inv" by blast
   8.238 -  with `{s:Inv. \<not> bval b s} \<subseteq> P` show ?case using `\<not> bval b t` by auto
   8.239 -qed auto
   8.240 -
   8.241 -theorem CS_complete: "\<lbrakk> (c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post(CS S c)"
   8.242 -by (metis CS_unfold step_cs_complete strip_CS)
   8.243 +theorem steps_approx_CS: "s:S \<Longrightarrow> steps s c n \<le> CS S c"
   8.244 +by (metis CS_unfold steps_approx_fix_step strip_CS)
   8.245  
   8.246  end
     9.1 --- a/src/HOL/IMP/Collecting_list.thy	Sun Nov 27 13:12:42 2011 +0100
     9.2 +++ b/src/HOL/IMP/Collecting_list.thy	Sun Nov 27 13:32:20 2011 +0100
     9.3 @@ -4,22 +4,28 @@
     9.4  
     9.5  subsection "Executable Collecting Semantics on lists"
     9.6  
     9.7 -fun step_cs :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where
     9.8 -"step_cs S (SKIP {P}) = (SKIP {S})" |
     9.9 -"step_cs S (x ::= e {P}) =
    9.10 +fun step :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where
    9.11 +"step S (SKIP {P}) = (SKIP {S})" |
    9.12 +"step S (x ::= e {P}) =
    9.13    (x ::= e {[s(x := aval e s). s \<leftarrow> S]})" |
    9.14 -"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
    9.15 -"step_cs S (IF b THEN c1 ELSE c2 {P}) =
    9.16 -   IF b THEN step_cs [s \<leftarrow> S. bval b s] c1 ELSE step_cs [s\<leftarrow>S. \<not> bval b s] c2
    9.17 +"step S (c1; c2) = step S c1; step (post c1) c2" |
    9.18 +"step S (IF b THEN c1 ELSE c2 {P}) =
    9.19 +   IF b THEN step [s \<leftarrow> S. bval b s] c1 ELSE step [s\<leftarrow>S. \<not> bval b s] c2
    9.20     {post c1 @ post c2}" |
    9.21 -"step_cs S ({Inv} WHILE b DO c {P}) =
    9.22 -  {S @ post c} WHILE b DO (step_cs [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
    9.23 +"step S ({Inv} WHILE b DO c {P}) =
    9.24 +  {S @ post c} WHILE b DO (step [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
    9.25  
    9.26  definition "c = WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
    9.27  definition "c0 = anno [] c"
    9.28  
    9.29  definition "show_acom xs = map_acom (map (show_state xs))"
    9.30  
    9.31 -value "show_acom [''x''] (((step_cs [<>]) ^^ 6) c0)"
    9.32 +text{* Collecting semantics: *}
    9.33 +
    9.34 +value "show_acom [''x''] (((step [<>]) ^^ 6) c0)"
    9.35 +
    9.36 +text{* Small step semantics: *}
    9.37 +
    9.38 +value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))"
    9.39  
    9.40  end
    10.1 --- a/src/HOL/IMP/ROOT.ML	Sun Nov 27 13:12:42 2011 +0100
    10.2 +++ b/src/HOL/IMP/ROOT.ML	Sun Nov 27 13:32:20 2011 +0100
    10.3 @@ -19,6 +19,8 @@
    10.4   "VC",
    10.5   "HoareT",
    10.6   "Abs_Int2",
    10.7 + "Collecting1",
    10.8 + "Collecting_list",
    10.9   "Abs_Int_Den/Abs_Int_den2",
   10.10   "Procs_Dyn_Vars_Dyn",
   10.11   "Procs_Stat_Vars_Dyn",