--- a/src/HOL/IMP/Abs_Int0.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Sun Mar 10 18:29:10 2013 +0100
@@ -6,16 +6,10 @@
subsection "Orderings"
-notation
- Orderings.bot ("\<bottom>") and
- Orderings.top ("\<top>")
-
declare order_trans[trans]
-class join = order +
-fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
-
-class semilattice = join + top +
+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"
@@ -23,17 +17,15 @@
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"
-by (metis join_ge1 join_ge2 order_trans)
-
-end
+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)
-instantiation "fun" :: (type, semilattice) semilattice
-begin
-
-definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+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)
@@ -43,7 +35,7 @@
qed (simp_all add: le_fun_def)
end
-
+*)
instantiation option :: (order)order
begin
@@ -73,15 +65,15 @@
end
-instantiation option :: (join)join
+instantiation option :: (sup)sup
begin
-fun join_option where
+fun sup_option where
"Some x \<squnion> Some y = Some(x \<squnion> y)" |
"None \<squnion> y = y" |
"x \<squnion> None = x"
-lemma join_None2[simp]: "x \<squnion> None = x"
+lemma sup_None2[simp]: "x \<squnion> None = x"
by (cases x) simp_all
instance ..
@@ -94,13 +86,13 @@
definition top_option where "\<top> = Some \<top>"
instance proof
- case goal1 show ?case by(cases a, simp_all add: top_option_def)
+ case goal4 show ?case by(cases a, simp_all add: top_option_def)
next
- case goal2 thus ?case by(cases x, simp, cases y, simp_all)
+ case goal1 thus ?case by(cases x, simp, cases y, simp_all)
next
- case goal3 thus ?case by(cases y, simp, cases x, simp_all)
+ case goal2 thus ?case by(cases y, simp, cases x, simp_all)
next
- case goal4 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+ case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
qed
end
@@ -186,17 +178,25 @@
"aval' (V x) S = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av 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(S(x := aval' e S))}" |
-"step' S (C1; C2) = step' S C1; step' (post C1) C2" |
-"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+(* Interpretation would be nicer but is impossible *)
+definition "step' = 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}" |
-"step' S ({I} WHILE b DO {P} C {Q}) =
+ {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)"
--- a/src/HOL/IMP/Abs_Int1.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Sun Mar 10 18:29:10 2013 +0100
@@ -60,15 +60,25 @@
locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
begin
-fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av 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 {P1} C1 ELSE {P2} C2 {Q}) =
- (IF b THEN {S} step' P1 C1 ELSE {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 {I} step' P C {I}"
+(* Interpretation would be nicer but is impossible *)
+definition "step' = 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)"
@@ -95,7 +105,7 @@
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 join_ge1 join_ge2)
+ 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)
@@ -133,9 +143,9 @@
subsubsection "Monotonicity"
-lemma le_join_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow>
+lemma le_sup_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow>
x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
-by (metis join_ge1 join_ge2 order_trans)
+by (metis sup_ge1 sup_ge2 order_trans)
locale Abs_Int_mono = Abs_Int +
assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
@@ -149,7 +159,7 @@
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_join_disj le_join_disj[OF post_in_L post_in_L]
+ le_sup_disj le_sup_disj[OF post_in_L post_in_L]
split: option.split)
done
--- a/src/HOL/IMP/Abs_Int1_const.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Sun Mar 10 18:29:10 2013 +0100
@@ -30,7 +30,7 @@
definition "a < (b::const) = (a \<le> b & ~ b \<le> a)"
-fun join_const where
+fun sup_const where
"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
"_ \<squnion> _ = Any"
@@ -48,11 +48,11 @@
next
case goal6 thus ?case by(cases x, cases y, simp_all)
next
- case goal7 thus ?case by(cases y, cases x, simp_all)
+ case goal5 thus ?case by(cases y, cases x, simp_all)
next
- case goal8 thus ?case by(cases z, cases y, cases x, simp_all)
+ case goal7 thus ?case by(cases z, cases y, cases x, simp_all)
next
- case goal5 thus ?case by(simp add: top_const_def)
+ case goal8 thus ?case by(simp add: top_const_def)
qed
end
--- a/src/HOL/IMP/Abs_Int1_parity.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Sun Mar 10 18:29:10 2013 +0100
@@ -52,7 +52,7 @@
instantiation parity :: semilattice
begin
-definition join_parity where
+definition sup_parity where
"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)"
definition top_parity where
@@ -66,13 +66,13 @@
instance
proof
- case goal1 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
+ case goal1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
- case goal2 (*join1*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
+ case goal2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
- case goal3 (*join2*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
+ case goal3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
- case goal4 (*join least*) thus ?case by(auto simp: less_eq_parity_def join_parity_def)
+ case goal4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
qed
end
@@ -165,7 +165,7 @@
qed
definition m_parity :: "parity \<Rightarrow> nat" where
-"m_parity x = (if x=Either then 0 else 1)"
+"m_parity x = (if x = Either then 0 else 1)"
interpretation Abs_Int_measure
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
--- a/src/HOL/IMP/Abs_Int2.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Sun Mar 10 18:29:10 2013 +0100
@@ -26,17 +26,7 @@
subsection "Backward Analysis of Expressions"
-class lattice = semilattice + bot +
-fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
-assumes meet_le1 [simp]: "x \<sqinter> y \<le> x"
-and meet_le2 [simp]: "x \<sqinter> y \<le> y"
-and meet_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
-begin
-
-lemma mono_meet: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> x \<sqinter> y \<le> x' \<sqinter> y'"
-by (metis meet_greatest meet_le1 meet_le2 order_trans)
-
-end
+class lattice = semilattice + semilattice_inf + bot
locale Val_abs1_gamma =
Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set" +
@@ -49,7 +39,8 @@
by (metis IntI inter_gamma_subset_gamma_meet set_mp)
lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
-by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2)
+by(rule equalityI[OF _ inter_gamma_subset_gamma_meet])
+ (metis inf_le1 inf_le2 le_inf_iff mono_gamma)
end
@@ -71,9 +62,9 @@
Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set"
begin
-lemma in_gamma_join_UpI:
+lemma in_gamma_sup_UpI:
"S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
-by (metis (hide_lams, no_types) semilatticeL_class.join_ge1 semilatticeL_class.join_ge2 mono_gamma_o subsetD)
+by (metis (hide_lams, no_types) semilatticeL_class.sup_ge1 semilatticeL_class.sup_ge2 mono_gamma_o subsetD)
fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
"aval'' e None = \<bottom>" |
@@ -98,7 +89,7 @@
program point is unreachable. But then the abstract state should collapse to
@{const None}. Put differently, we maintain the invariant that in an abstract
state of the form @{term"Some s"}, all variables are mapped to non-@{const
-bot} values. Otherwise the (pointwise) join of two abstract states, one of
+bot} values. Otherwise the (pointwise) sup of two abstract states, one of
which contains @{const bot} values, may produce too large a result, thus
making the analysis less precise. *}
@@ -148,27 +139,35 @@
case (Not b) thus ?case by simp
next
case (And b1 b2) thus ?case
- by simp (metis And(1) And(2) bfilter_in_L in_gamma_join_UpI)
+ by simp (metis And(1) And(2) bfilter_in_L in_gamma_sup_UpI)
next
case (Less e1 e2) thus ?case
by(auto split: prod.split)
(metis (lifting) afilter_in_L afilter_sound aval''_sound filter_less')
qed
+(* Interpretation would be nicer but is impossible *)
+definition "step' = 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)"
-fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av 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 {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})" |
-"step' S ({I} WHILE b DO {p} C {Q}) =
+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)"
@@ -194,7 +193,7 @@
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 join_ge1 join_ge2)
+ 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
@@ -259,10 +258,10 @@
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 mono_meet split: option.splits prod.splits)
+apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
apply (metis mono_gamma subsetD)
-apply(drule (2) mono_fun_L)
-apply (metis mono_meet le_bot)
+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
@@ -272,7 +271,7 @@
apply(simp)
apply(simp)
apply simp
-apply(metis join_least order_trans[OF _ join_ge1] order_trans[OF _ join_ge2] bfilter_in_L)
+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
@@ -281,7 +280,7 @@
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_join_disj le_join_disj[OF post_in_L post_in_L] bfilter_in_L
+ le_sup_disj le_sup_disj[OF post_in_L post_in_L] bfilter_in_L
split: option.split)
done
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Sun Mar 10 18:29:10 2013 +0100
@@ -87,12 +87,12 @@
definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))"
-definition join_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
-"join_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
+definition sup_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"sup_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
else let (l1,h1) = p1; (l2,h2) = p2 in (min l1 l2, max h1 h2))"
-lift_definition join_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is join_rep
-by(auto simp: eq_ivl_iff join_rep_def)
+lift_definition sup_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is sup_rep
+by(auto simp: eq_ivl_iff sup_rep_def)
lift_definition top_ivl :: ivl is "(Minf,Pinf)"
by(auto simp: eq_ivl_def)
@@ -111,13 +111,13 @@
next
case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
next
- case goal6 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
+ case goal5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
next
- case goal7 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
+ case goal6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
next
- case goal8 thus ?case by transfer (auto simp add: le_rep_def join_rep_def)
+ case goal7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def)
next
- case goal5 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
+ case goal8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
qed
end
@@ -144,29 +144,29 @@
instantiation ivl :: lattice
begin
-definition meet_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
-"meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
+definition inf_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"inf_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
-lemma \<gamma>_meet_rep: "\<gamma>_rep(meet_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
-by(auto simp:meet_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
+lemma \<gamma>_inf_rep: "\<gamma>_rep(inf_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
+by(auto simp:inf_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
-lift_definition meet_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is meet_rep
-by(auto simp: \<gamma>_meet_rep eq_ivl_def)
+lift_definition inf_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is inf_rep
+by(auto simp: \<gamma>_inf_rep eq_ivl_def)
definition "\<bottom> = empty_ivl"
instance
proof
+ case goal1 thus ?case
+ unfolding inf_rep_def by transfer (auto simp: le_iff_subset \<gamma>_inf_rep)
+next
case goal2 thus ?case
- unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
+ unfolding inf_rep_def by transfer (auto simp: le_iff_subset \<gamma>_inf_rep)
next
case goal3 thus ?case
- unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
+ unfolding inf_rep_def by transfer (auto simp: le_iff_subset \<gamma>_inf_rep)
next
- case goal4 thus ?case
- unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
-next
- case goal1 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
+ case goal4 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
qed
end
@@ -180,13 +180,13 @@
if [l2\<dots>h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)"
unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty)
-lemma join_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] =
+lemma sup_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] =
(if [l1\<dots>h1] = \<bottom> then [l2\<dots>h2] else
if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])"
-unfolding bot_ivl_def by transfer (simp add: join_rep_def eq_ivl_empty)
+unfolding bot_ivl_def by transfer (simp add: sup_rep_def eq_ivl_empty)
-lemma meet_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
-by transfer (simp add: meet_rep_def)
+lemma inf_ivl_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
+by transfer (simp add: inf_rep_def)
instantiation ivl :: plus
@@ -300,7 +300,7 @@
defines aval_ivl is aval'
proof
case goal1 show ?case
- by transfer (auto simp add:meet_rep_def \<gamma>_rep_cases split: prod.split extended.split)
+ by transfer (auto simp add:inf_rep_def \<gamma>_rep_cases split: prod.split extended.split)
next
case goal2 show ?case unfolding bot_ivl_def by transfer simp
qed
@@ -308,16 +308,16 @@
lemma \<gamma>_plus_rep: "i1 : \<gamma>_rep p1 \<Longrightarrow> i2 : \<gamma>_rep p2 \<Longrightarrow> i1+i2 \<in> \<gamma>_rep(plus_rep p1 p2)"
by(auto simp: plus_rep_def plus_rep_plus split: prod.splits)
-lemma non_empty_meet: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow>
- \<not> is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))"
-by (auto simp add: \<gamma>_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv)
+lemma non_empty_inf: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow>
+ \<not> is_empty_rep (inf_rep a1 (plus_rep a (uminus_rep a2)))"
+by (auto simp add: \<gamma>_inf_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv)
(metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_minus)
-lemma filter_plus: "\<lbrakk>eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and>
- eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2;
+lemma filter_plus: "\<lbrakk>eq_ivl (inf_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and>
+ eq_ivl (inf_rep a2 (plus_rep a (uminus_rep a1))) b2;
n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a\<rbrakk>
\<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2"
-by (auto simp: eq_ivl_iff \<gamma>_meet_rep non_empty_meet add_ac)
+by (auto simp: eq_ivl_iff \<gamma>_inf_rep non_empty_inf add_ac)
(metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_def add_commute)+
interpretation Val_abs1
@@ -352,8 +352,8 @@
text{* Monotonicity: *}
-lemma mono_meet_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (meet_rep p1 q1) (meet_rep p2 q2)"
-by(auto simp add: le_iff_subset \<gamma>_meet_rep)
+lemma mono_inf_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (inf_rep p1 q1) (inf_rep p2 q2)"
+by(auto simp add: le_iff_subset \<gamma>_inf_rep)
lemma mono_plus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (plus_rep p1 q1) (plus_rep p2 q2)"
apply(auto simp: plus_rep_def le_iff_subset split: if_splits)
@@ -371,7 +371,7 @@
case goal1 thus ?case by transfer (rule mono_plus_rep)
next
case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def
- by transfer (auto simp: mono_meet_rep mono_plus_rep mono_minus_rep)
+ by transfer (auto simp: mono_inf_rep mono_plus_rep mono_minus_rep)
next
case goal3 thus ?case unfolding less_eq_prod_def
apply transfer
--- a/src/HOL/IMP/Abs_Int_init.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_init.thy Sun Mar 10 18:29:10 2013 +0100
@@ -1,6 +1,5 @@
theory Abs_Int_init
-imports "~~/src/HOL/ex/Interpretation_with_Defs"
- "~~/src/HOL/Library/While_Combinator"
+imports "~~/src/HOL/Library/While_Combinator"
Vars Collecting Abs_Int_Tests
begin
--- a/src/HOL/IMP/Abs_State.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_State.thy Sun Mar 10 18:29:10 2013 +0100
@@ -59,14 +59,14 @@
end
-class semilatticeL = join + L +
+class semilatticeL = order + sup + L +
fixes Top :: "vname set \<Rightarrow> 'a"
-assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<le> x \<squnion> y"
-and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<le> x \<squnion> y"
-and join_least[simp]: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
+assumes sup_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<le> x \<squnion> y"
+and sup_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<le> x \<squnion> y"
+and sup_least[simp]: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
and Top[simp]: "x \<in> L X \<Longrightarrow> x \<le> Top X"
and Top_in_L[simp]: "Top X \<in> L X"
-and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
+and sup_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
notation (input) Top ("\<top>\<^bsub>_\<^esub>")
notation (latex output) Top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
@@ -171,10 +171,10 @@
end
-instantiation st :: (join) join
+instantiation st :: (sup) sup
begin
-definition join_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
+definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
"F \<squnion> (G::'a st) = St (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
instance ..
@@ -197,7 +197,7 @@
definition Top_st :: "vname set \<Rightarrow> 'a st" where "Top(X) = St (\<lambda>x. \<top>) X"
instance
-proof qed(auto simp add: less_eq_st_def join_st_def Top_st_def L_st_def)
+proof qed(auto simp add: less_eq_st_def sup_st_def Top_st_def L_st_def)
end
--- a/src/HOL/IMP/Collecting.thy Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Collecting.thy Sun Mar 10 18:29:10 2013 +0100
@@ -1,7 +1,35 @@
theory Collecting
imports Complete_Lattice Big_Step ACom
+ "~~/src/HOL/ex/Interpretation_with_Defs"
begin
+subsection "The generic Step function"
+
+notation
+ sup (infixl "\<squnion>" 65) and
+ inf (infixl "\<sqinter>" 70) and
+ 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 :: "'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}"
+
+end
+
+
subsection "Collecting Semantics of Commands"
subsubsection "Annotated commands as a complete lattice"
@@ -141,16 +169,11 @@
subsubsection "Collecting semantics"
-fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
-"step S (SKIP {Q}) = (SKIP {S})" |
-"step S (x ::= e {Q}) =
- x ::= e {{s(x := aval e s) |s. s : 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 {{s:S. bval b s}} step P1 C1 ELSE {{s:S. \<not> bval b s}} step P2 C2
- {post C1 \<union> post C2}" |
-"step S ({I} WHILE b DO {P} C {Q}) =
- {S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}"
+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 CS :: "com \<Rightarrow> state set acom" where
"CS c = lfp c (step UNIV)"