--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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",