--- a/src/HOL/IMP/Abs_Int0.thy Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Mon Mar 11 12:27:31 2013 +0100
@@ -9,33 +9,9 @@
declare order_trans[trans]
class semilattice = semilattice_sup + top
-(* +
-assumes join_ge1 [simp]: "x \<le> x \<squnion> y"
-and join_ge2 [simp]: "y \<le> x \<squnion> y"
-and join_least: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
-begin
-
-lemma join_le_iff[simp]: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
-by (metis join_ge1 join_ge2 join_least order_trans)
-*)
-
-lemma le_join_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> (z::'a::semilattice_sup)"
-by (metis sup_ge1 sup_ge2 order_trans)
instance "fun" :: (type, semilattice) semilattice ..
-(*
-definition top_fun where "top_fun = (\<lambda>x. \<top>)"
-
-lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
-by (simp add: join_fun_def)
-
-instance
-proof
-qed (simp_all add: le_fun_def)
-
-end
-*)
instantiation option :: (order)order
begin
@@ -97,6 +73,9 @@
end
+lemma [simp]: "(Some x < Some y) = (x < y)"
+by(auto simp: less_le)
+
instantiation option :: (order)bot
begin
@@ -178,34 +157,14 @@
"aval' (V x) S = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-(* Interpretation would be nicer but is impossible *)
-definition "step' = Step.Step
+definition "step' = Step
(\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))
(\<lambda>b S. S)"
-lemma [simp]: "step' S (SKIP {P}) = (SKIP {S})"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (x ::= e {P}) =
- x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
- IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
- {post C1 \<squnion> post C2}"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S ({I} WHILE b DO {P} C {Q}) =
- {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
-by(simp add: step'_def Step.Step.simps)
-
definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI c = pfp (step' \<top>) (bot c)"
-lemma strip_step'[simp]: "strip(step' S C) = strip C"
-by(induct C arbitrary: S) (simp_all add: Let_def)
-
-
abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
where "\<gamma>\<^isub>s == \<gamma>_fun \<gamma>"
@@ -236,23 +195,18 @@
lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
-lemma in_gamma_update:
- "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
+lemma in_gamma_update: "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
by(simp add: \<gamma>_fun_def)
+lemma gamma_Step_subcomm:
+ assumes "!!x e S. f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)" "!!b S. g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
+ shows "Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
+proof(induction C arbitrary: S)
+qed (auto simp: mono_gamma_o assms)
+
lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
-proof(induction C arbitrary: S)
- case SKIP thus ?case by auto
-next
- case Assign thus ?case
- by (fastforce intro: aval'_sound in_gamma_update split: option.splits)
-next
- case Seq thus ?case by auto
-next
- case If thus ?case by (auto simp: mono_gamma_o)
-next
- case While thus ?case by (auto simp: mono_gamma_o)
-qed
+unfolding step_def step'_def
+by(rule gamma_Step_subcomm) (auto simp: aval'_sound in_gamma_update split: option.splits)
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
@@ -263,7 +217,7 @@
show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
qed
- have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+ have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
@@ -288,10 +242,8 @@
by(simp add: le_fun_def)
lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
- split: option.split)
-done
+unfolding step'_def
+by(rule mono2_Step) (auto simp: mono_update mono_aval' split: option.split)
end
--- a/src/HOL/IMP/Abs_Int1.thy Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Mon Mar 11 12:27:31 2013 +0100
@@ -37,8 +37,7 @@
subsection "Computable Abstract Interpretation"
-text{* Abstract interpretation over type @{text st} instead of
-functions. *}
+text{* Abstract interpretation over type @{text st} instead of functions. *}
context Gamma
begin
@@ -51,8 +50,29 @@
lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> vars a \<subseteq> dom S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
by (induction a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def)
+lemma gamma_Step_subcomm: fixes C1 C2 :: "'a::semilattice_sup acom"
+ assumes "!!x e S. x : X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> S \<in> L X \<Longrightarrow> f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)"
+ "!!b S. S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
+ shows "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
+proof(induction C arbitrary: S)
+qed (auto simp: assms intro!: mono_gamma_o post_in_L sup_ge1 sup_ge2)
+
+lemma in_gamma_update: "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
+by(simp add: \<gamma>_st_def)
+
end
+
+lemma Step_in_L: fixes C :: "'a::semilatticeL acom"
+assumes "!!x e S. \<lbrakk>S \<in> L X; x \<in> X; vars e \<subseteq> X\<rbrakk> \<Longrightarrow> f x e S \<in> L X"
+ "!!b S. S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> g b S \<in> L X"
+shows"\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> Step f g S C \<in> L X"
+proof(induction C arbitrary: S)
+ case Assign thus ?case
+ by(auto simp: L_st_def assms split: option.splits)
+qed (auto simp: assms)
+
+
text{* The for-clause (here and elsewhere) only serves the purpose of fixing
the name of the type parameter @{typ 'av} which would otherwise be renamed to
@{typ 'a}. *}
@@ -60,63 +80,28 @@
locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
begin
-(* Interpretation would be nicer but is impossible *)
-definition "step' = Step.Step
+definition "step' = Step
(\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
(\<lambda>b S. S)"
-lemma [code,simp]: "step' S (SKIP {P}) = (SKIP {S})"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (x ::= e {P}) =
- x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
- IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
- {post C1 \<squnion> post C2}"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S ({I} WHILE b DO {P} C {Q}) =
- {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
-by(simp add: step'_def Step.Step.simps)
-
definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI c = pfp (step' (Top(vars c))) (bot c)"
lemma strip_step'[simp]: "strip(step' S C) = strip C"
-by(induct C arbitrary: S) (simp_all add: Let_def)
+by(simp add: step'_def)
text{* Soundness: *}
-lemma in_gamma_update:
- "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
-by(simp add: \<gamma>_st_def)
+lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
+unfolding step_def step'_def
+by(rule gamma_Step_subcomm)
+ (auto simp: L_st_def intro!: aval'_sound in_gamma_update split: option.splits)
-lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
-proof(induction C arbitrary: S)
- case SKIP thus ?case by auto
-next
- case Assign thus ?case
- by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
-next
- case Seq thus ?case by auto
-next
- case (If b p1 C1 p2 C2 P)
- hence "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
- by(simp, metis post_in_L sup_ge1 sup_ge2)
- thus ?case using If by (auto simp: mono_gamma_o)
-next
- case While thus ?case by (auto simp: mono_gamma_o)
-qed
-
-lemma step'_in_L[simp]:
- "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> (step' S C) \<in> L X"
-proof(induction C arbitrary: S)
- case Assign thus ?case
- by(auto simp: L_st_def split: option.splits)
-qed auto
+lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
+unfolding step'_def
+by(rule Step_in_L)(auto simp: L_st_def step'_def split: option.splits)
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
@@ -132,7 +117,7 @@
show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
by(rule mono_gamma_c[OF pfp'])
qed
- have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+ have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
@@ -147,6 +132,15 @@
x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
by (metis sup_ge1 sup_ge2 order_trans)
+theorem mono2_Step: fixes C1 :: "'a::semilatticeL acom"
+ assumes "!!x e S1 S2. \<lbrakk>S1 \<in> L X; S2 \<in> L X; x \<in> X; vars e \<subseteq> X; S1 \<le> S2\<rbrakk> \<Longrightarrow> f x e S1 \<le> f x e S2"
+ "!!b S1 S2. S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
+ shows "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
+ S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
+by(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
+ (auto simp: mono_post assms le_sup_disj le_sup_disj[OF post_in_L post_in_L])
+
+
locale Abs_Int_mono = Abs_Int +
assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
begin
@@ -157,11 +151,8 @@
theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-apply (auto simp: Let_def mono_aval' mono_post
- le_sup_disj le_sup_disj[OF post_in_L post_in_L]
- split: option.split)
-done
+unfolding step'_def
+by(rule mono2_Step) (auto simp: mono_aval' split: option.split)
lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'"
@@ -173,14 +164,14 @@
and "\<forall>C. C \<in> L(vars c)\<inter>{C. strip C = c} \<longrightarrow> f C \<in> L(vars c)\<inter>{C. strip C = c}"
and "f C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
shows "C \<le> C'"
-apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
-by (simp_all add: assms(4,5) bot_least)
+by(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
+ (simp_all add: assms(4,5) bot_least)
lemma AI_least_pfp: assumes "AI c = Some C"
and "step' (Top(vars c)) C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)"
shows "C \<le> C'"
-apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
-by (simp_all add: mono_step'_top)
+by(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
+ (simp_all add: mono_step'_top)
end
--- a/src/HOL/IMP/Abs_Int2.thy Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Mon Mar 11 12:27:31 2013 +0100
@@ -30,16 +30,16 @@
locale Val_abs1_gamma =
Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set" +
-assumes inter_gamma_subset_gamma_meet:
+assumes inter_gamma_subset_gamma_inf:
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
and gamma_bot[simp]: "\<gamma> \<bottom> = {}"
begin
-lemma in_gamma_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
-by (metis IntI inter_gamma_subset_gamma_meet set_mp)
+lemma in_gamma_inf: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
+by (metis IntI inter_gamma_subset_gamma_inf set_mp)
-lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
-by(rule equalityI[OF _ inter_gamma_subset_gamma_meet])
+lemma gamma_inf[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
(metis inf_le1 inf_le2 le_inf_iff mono_gamma)
end
@@ -121,7 +121,7 @@
moreover have "s x : \<gamma> a" using V by simp
ultimately show ?case using V(3)
by(simp add: Let_def \<gamma>_st_def)
- (metis mono_gamma emptyE in_gamma_meet gamma_bot subset_empty)
+ (metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
next
case (Plus e1 e2) thus ?case
using filter_plus'[OF _ aval''_sound[OF Plus.prems(3)] aval''_sound[OF Plus.prems(3)]]
@@ -146,69 +146,27 @@
(metis (lifting) afilter_in_L afilter_sound aval''_sound filter_less')
qed
-(* Interpretation would be nicer but is impossible *)
-definition "step' = Step.Step
+definition "step' = Step
(\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
(\<lambda>b S. bfilter b True S)"
-lemma [code,simp]: "step' S (SKIP {P}) = (SKIP {S})"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (x ::= e {P}) =
- x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
- (let P1' = bfilter b True S; C1' = step' P1 C1;
- P2' = bfilter b False S; C2' = step' P2 C2
- in IF b THEN {P1'} C1' ELSE {P2'} C2' {post C1 \<squnion> post C2})"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S ({I} WHILE b DO {p} C {Q}) =
- {S \<squnion> post C}
- WHILE b DO {bfilter b True I} step' p C
- {bfilter b False I}"
-by(simp add: step'_def Step.Step.simps)
-
definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI c = pfp (step' \<top>\<^bsub>vars c\<^esub>) (bot c)"
lemma strip_step'[simp]: "strip(step' S c) = strip c"
-by(induct c arbitrary: S) (simp_all add: Let_def)
+by(simp add: step'_def)
subsubsection "Soundness"
-lemma in_gamma_update:
- "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
-by(simp add: \<gamma>_st_def)
-
lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
-proof(induction C arbitrary: S)
- case SKIP thus ?case by auto
-next
- case Assign thus ?case
- by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
-next
- case Seq thus ?case by auto
-next
- case (If b _ C1 _ C2)
- hence 0: "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
- by(simp, metis post_in_L sup_ge1 sup_ge2)
- have "vars b \<subseteq> X" using If.prems by simp
- note vars = `S \<in> L X` `vars b \<subseteq> X`
- show ?case using If 0
- by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
-next
- case (While I b)
- hence vars: "I \<in> L X" "vars b \<subseteq> X" by simp_all
- thus ?case using While
- by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
-qed
+unfolding step_def step'_def
+by(rule gamma_Step_subcomm)
+ (auto simp: L_st_def intro!: aval'_sound bfilter_sound in_gamma_update split: option.splits)
lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
-proof(induction C arbitrary: S)
- case Assign thus ?case by(auto simp add: L_option_def L_st_def split: option.splits)
-qed (auto simp add: bfilter_in_L)
+unfolding step'_def
+by(rule Step_in_L)(auto simp: bfilter_in_L L_st_def step'_def split: option.splits)
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
@@ -258,31 +216,28 @@
lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
apply(induction e arbitrary: r1 r2 S1 S2)
-apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
-apply (metis mono_gamma subsetD)
-apply (metis inf_mono le_bot mono_fun_L)
-apply (metis inf_mono mono_fun_L mono_update)
+ apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
+ apply (metis mono_gamma subsetD)
+ apply (metis inf_mono le_bot mono_fun_L)
+ apply (metis inf_mono mono_fun_L mono_update)
apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
done
lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
apply(induction b arbitrary: bv S1 S2)
-apply(simp)
-apply(simp)
-apply simp
-apply(metis sup_least order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2] bfilter_in_L)
+ apply(simp)
+ apply(simp)
+ apply simp
+ apply(metis sup_least order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2] bfilter_in_L)
apply (simp split: prod.splits)
apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
done
theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
- le_sup_disj le_sup_disj[OF post_in_L post_in_L] bfilter_in_L
- split: option.split)
-done
+unfolding step'_def
+by(rule mono2_Step) (auto simp: mono_aval' mono_bfilter split: option.split)
lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
C1 \<le> C2 \<Longrightarrow> step' (Top X) C1 \<le> step' (Top X) C2"
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Mon Mar 11 12:27:31 2013 +0100
@@ -1,9 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int2_ivl
-imports "~~/src/HOL/Library/Quotient_List"
- "~~/src/HOL/Library/Extended"
- Abs_Int2
+imports Abs_Int2
begin
subsection "Interval Analysis"
--- a/src/HOL/IMP/Abs_Int3.thy Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Mon Mar 11 12:27:31 2013 +0100
@@ -350,7 +350,7 @@
lemma strip_pfp_wn:
"\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C"
by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
- (metis (no_types) narrow_acom_def strip_iter_widen strip_map2_acom strip_while)
+ (metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
locale Abs_Int2 = Abs_Int1_mono
@@ -478,17 +478,17 @@
"C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
-prefer 2 apply (simp add: size_annos_same2)
+ prefer 2 apply (simp add: size_annos_same2)
apply (auto)
apply(rule setsum_strict_mono_ex1)
-apply simp
-apply (clarsimp)
-apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
+ apply simp
+ apply (clarsimp)
+ apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
apply(auto simp: le_iff_le_annos listrel_iff_nth)
apply(rule_tac x=i in bexI)
-prefer 2 apply simp
+ prefer 2 apply simp
apply(rule m_o_widen)
-apply (simp add: finite_cvars)+
+ apply (simp add: finite_cvars)+
done
@@ -525,10 +525,6 @@
definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
"n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
-(* FIXME mv *)
-lemma [simp]: "(Some x < Some y) = (x < y)"
-by(auto simp: less_le)
-
lemma n_o_narrow:
"S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
\<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
@@ -689,7 +685,7 @@
apply(erule iter_widen_pfp)
done
-(*unused_thms Abs_Int_init -*)
+(*unused_thms Abs_Int_init - *)
subsubsection "Counterexamples"
--- a/src/HOL/IMP/Abs_Int_init.thy Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_init.thy Mon Mar 11 12:27:31 2013 +0100
@@ -1,8 +1,10 @@
theory Abs_Int_init
imports "~~/src/HOL/Library/While_Combinator"
+ "~~/src/HOL/Library/Quotient_List"
+ "~~/src/HOL/Library/Extended"
Vars Collecting Abs_Int_Tests
begin
-hide_const (open) top bot dom --"to avoid qualified names"
+hide_const (open) top bot dom --"to avoid qualified names"
end
--- a/src/HOL/IMP/Collecting.thy Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Collecting.thy Mon Mar 11 12:27:31 2013 +0100
@@ -11,23 +11,26 @@
bot ("\<bottom>") and
top ("\<top>")
-locale Step =
-fixes step_assign :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
-and step_cond :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a"
-begin
+fun Step :: "(vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup) \<Rightarrow> (bexp \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"Step f g S (SKIP {Q}) = (SKIP {S})" |
+"Step f g S (x ::= e {Q}) =
+ x ::= e {f x e S}" |
+"Step f g S (C1; C2) = Step f g S C1; Step f g (post C1) C2" |
+"Step f g S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+ IF b THEN {g b S} Step f g P1 C1 ELSE {g (Not b) S} Step f g P2 C2
+ {post C1 \<squnion> post C2}" |
+"Step f g S ({I} WHILE b DO {P} C {Q}) =
+ {S \<squnion> post C} WHILE b DO {g b I} Step f g P C {g (Not b) I}"
-fun Step :: "'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
-"Step S (SKIP {Q}) = (SKIP {S})" |
-"Step S (x ::= e {Q}) =
- x ::= e {step_assign x e S}" |
-"Step S (C1; C2) = Step S C1; Step (post C1) C2" |
-"Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
- IF b THEN {step_cond b S} Step P1 C1 ELSE {step_cond (Not b) S} Step P2 C2
- {post C1 \<squnion> post C2}" |
-"Step S ({I} WHILE b DO {P} C {Q}) =
- {S \<squnion> post C} WHILE b DO {step_cond b I} Step P C {step_cond (Not b) I}"
+(* Could hide f and g like this:
+consts fa :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
+ fb :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
+abbreviation "STEP == Step fa fb"
+thm Step.simps[where f = fa and g = fb]
+*)
-end
+lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
+by(induct C arbitrary: S) auto
subsection "Collecting Semantics of Commands"
@@ -169,31 +172,35 @@
subsubsection "Collecting semantics"
-interpretation Step
-where step_assign = "\<lambda>x e S. {s(x := aval e s) |s. s : S}"
-and step_cond = "\<lambda>b S. {s:S. bval b s}"
-defines step is Step
-.
+definition "step = Step (\<lambda>x e S. {s(x := aval e s) |s. s : S}) (\<lambda>b S. {s:S. bval b s})"
definition CS :: "com \<Rightarrow> state set acom" where
"CS c = lfp c (step UNIV)"
-lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2"
-proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
- case 2 thus ?case by fastforce
+lemma mono2_Step: fixes C1 C2 :: "'a::semilattice_sup acom"
+ assumes "!!x e S1 S2. S1 \<le> S2 \<Longrightarrow> f x e S1 \<le> f x e S2"
+ "!!b S1 S2. S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
+ shows "C1 \<le> C2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
+proof(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
+ case 2 thus ?case by (fastforce simp: assms(1))
next
case 3 thus ?case by(simp add: le_post)
next
- case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+
+ case 4 thus ?case
+ by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2)
next
- case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
+ case 5 thus ?case
+ by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2)
qed auto
+lemma mono2_step: "C1 \<le> C2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 C1 \<le> step S2 C2"
+unfolding step_def by(rule mono2_Step) auto
+
lemma mono_step: "mono (step S)"
by(blast intro: monoI mono2_step)
lemma strip_step: "strip(step S C) = strip C"
-by (induction C arbitrary: S) auto
+by (induction C arbitrary: S) (auto simp: step_def)
lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
apply(rule lfp_unfold[OF _ mono_step])
@@ -224,23 +231,24 @@
lemma big_step_post_step:
"\<lbrakk> (c, s) \<Rightarrow> t; strip C = c; s \<in> S; step S C \<le> C \<rbrakk> \<Longrightarrow> t \<in> post C"
proof(induction arbitrary: C S rule: big_step_induct)
- case Skip thus ?case by(auto simp: strip_eq_SKIP)
+ case Skip thus ?case by(auto simp: strip_eq_SKIP step_def)
next
- case Assign thus ?case by(fastforce simp: strip_eq_Assign)
+ case Assign thus ?case by(fastforce simp: strip_eq_Assign step_def)
next
- case Seq thus ?case by(fastforce simp: strip_eq_Seq)
+ case Seq thus ?case by(fastforce simp: strip_eq_Seq step_def)
next
- case IfTrue thus ?case apply(auto simp: strip_eq_If)
- by (metis (lifting) mem_Collect_eq set_mp)
+ case IfTrue thus ?case apply(auto simp: strip_eq_If step_def)
+ by (metis (lifting,full_types) mem_Collect_eq set_mp)
next
- case IfFalse thus ?case apply(auto simp: strip_eq_If)
- by (metis (lifting) mem_Collect_eq set_mp)
+ case IfFalse thus ?case apply(auto simp: strip_eq_If step_def)
+ by (metis (lifting,full_types) mem_Collect_eq set_mp)
next
case (WhileTrue b s1 c' s2 s3)
from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
by(auto simp: strip_eq_While)
from WhileTrue.prems(3) `C = _`
- have "step P C' \<le> C'" "{s \<in> I. bval b s} \<le> P" "S \<le> I" "step (post C') C \<le> C" by auto
+ have "step P C' \<le> C'" "{s \<in> I. bval b s} \<le> P" "S \<le> I" "step (post C') C \<le> C"
+ by (auto simp: step_def)
have "step {s \<in> I. bval b s} C' \<le> C'"
by (rule order_trans[OF mono2_step[OF order_refl `{s \<in> I. bval b s} \<le> P`] `step P C' \<le> C'`])
have "s1: {s:I. bval b s}" using `s1 \<in> S` `S \<subseteq> I` `bval b s1` by auto
@@ -248,7 +256,7 @@
from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' `step (post C') C \<le> C`]
show ?case .
next
- case (WhileFalse b s1 c') thus ?case by (force simp: strip_eq_While)
+ case (WhileFalse b s1 c') thus ?case by (force simp: strip_eq_While step_def)
qed
lemma big_step_lfp: "\<lbrakk> (c,s) \<Rightarrow> t; s \<in> S \<rbrakk> \<Longrightarrow> t \<in> post(lfp c (step S))"