# HG changeset patch # User nipkow # Date 1362936550 -3600 # Node ID 8a9f0503b1c01d956bc3da13fea4cde1bd8e5649 # Parent 1f5497c8ce8c3cb30724ed618e9ac4662916e9a7 factored out Step diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int0.thy --- 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 ("\") and - Orderings.top ("\") - declare order_trans[trans] -class join = order + -fixes join :: "'a \ 'a \ 'a" (infixl "\" 65) - -class semilattice = join + top + +class semilattice = semilattice_sup + top +(* + assumes join_ge1 [simp]: "x \ x \ y" and join_ge2 [simp]: "y \ x \ y" and join_least: "x \ z \ y \ z \ x \ y \ z" @@ -23,17 +17,15 @@ lemma join_le_iff[simp]: "x \ y \ z \ x \ z \ y \ z" by (metis join_ge1 join_ge2 join_least order_trans) +*) -lemma le_join_disj: "x \ y \ x \ z \ x \ y \ z" -by (metis join_ge1 join_ge2 order_trans) - -end +lemma le_join_disj: "x \ y \ x \ z \ x \ y \ (z::'a::semilattice_sup)" +by (metis sup_ge1 sup_ge2 order_trans) -instantiation "fun" :: (type, semilattice) semilattice -begin - -definition "f \ g = (\x. f x \ g x)" +instance "fun" :: (type, semilattice) semilattice .. +(* +definition top_fun where "top_fun = (\x. \)" lemma join_apply[simp]: "(f \ g) x = f x \ 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 \ Some y = Some(x \ y)" | "None \ y = y" | "x \ None = x" -lemma join_None2[simp]: "x \ None = x" +lemma sup_None2[simp]: "x \ None = x" by (cases x) simp_all instance .. @@ -94,13 +86,13 @@ definition top_option where "\ = Some \" 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 \ 'av st option acom \ 'av st option acom" - where -"step' S (SKIP {P}) = (SKIP {S})" | -"step' S (x ::= e {P}) = - x ::= e {case S of None \ None | Some S \ 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 + (\x e S. case S of None \ None | Some S \ Some(S(x := aval' e S))) + (\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 \ None | Some S \ 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 \ post C2}" | -"step' S ({I} WHILE b DO {P} C {Q}) = + {post C1 \ post C2}" +by(simp add: step'_def Step.Step.simps) +lemma [simp]: "step' S ({I} WHILE b DO {P} C {Q}) = {S \ post C} WHILE b DO {I} step' P C {I}" +by(simp add: step'_def Step.Step.simps) definition AI :: "com \ 'av st option acom option" where "AI c = pfp (step' \) (bot c)" diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int1.thy --- 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 \=\ for \ :: "'av::semilattice \ val set" begin -fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" where -"step' S (SKIP {P}) = (SKIP {S})" | -"step' S (x ::= e {P}) = - x ::= e {case S of None \ None | Some S \ 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 \ post C2})" | -"step' S ({I} WHILE b DO {P} C {Q}) = - {S \ post C} WHILE b DO {I} step' P C {I}" +(* Interpretation would be nicer but is impossible *) +definition "step' = Step.Step + (\x e S. case S of None \ None | Some S \ Some(update S x (aval' e S))) + (\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 \ None | Some S \ 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 \ post C2}" +by(simp add: step'_def Step.Step.simps) +lemma [code,simp]: "step' S ({I} WHILE b DO {P} C {Q}) = + {S \ post C} WHILE b DO {I} step' P C {I}" +by(simp add: step'_def Step.Step.simps) definition AI :: "com \ '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 \ post C1 \ post C2 \ post C2 \ post C1 \ 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 \ L X \ (z::_::semilatticeL) \ L X \ +lemma le_sup_disj: "y \ L X \ (z::_::semilatticeL) \ L X \ x \ y \ x \ z \ x \ y \ 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 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" @@ -149,7 +159,7 @@ S1 \ S2 \ C1 \ C2 \ step' S1 C1 \ 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 diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int1_const.thy --- 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 \ b & ~ b \ a)" -fun join_const where +fun sup_const where "Const m \ Const n = (if n=m then Const m else Any)" | "_ \ _ = 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 diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int1_parity.thy --- 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 \ y = (if x \ y then y else if y \ 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 \ 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 \ = \_parity and num' = num_parity and plus' = plus_parity diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int2.thy --- 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 \ 'a \ 'a" (infixl "\" 65) -assumes meet_le1 [simp]: "x \ y \ x" -and meet_le2 [simp]: "x \ y \ y" -and meet_greatest: "x \ y \ x \ z \ x \ y \ z" -begin - -lemma mono_meet: "x \ x' \ y \ y' \ x \ y \ x' \ y'" -by (metis meet_greatest meet_le1 meet_le2 order_trans) - -end +class lattice = semilattice + semilattice_inf + bot locale Val_abs1_gamma = Gamma where \ = \ for \ :: "'av::lattice \ val set" + @@ -49,7 +39,8 @@ by (metis IntI inter_gamma_subset_gamma_meet set_mp) lemma gamma_meet[simp]: "\(a1 \ a2) = \ a1 \ \ 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 \ = \ for \ :: "'av::lattice \ val set" begin -lemma in_gamma_join_UpI: +lemma in_gamma_sup_UpI: "S1 \ L X \ S2 \ L X \ s : \\<^isub>o S1 \ s : \\<^isub>o S2 \ s : \\<^isub>o(S1 \ 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 \ 'av st option \ 'av" where "aval'' e None = \" | @@ -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 + (\x e S. case S of None \ None | Some S \ Some(update S x (aval' e S))) + (\b S. bfilter b True S)" -fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" - where -"step' S (SKIP {P}) = (SKIP {S})" | -"step' S (x ::= e {P}) = - x ::= e {case S of None \ None | Some S \ 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 \ 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 \ None | Some S \ 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 \ post C2})" +by(simp add: step'_def Step.Step.simps) +lemma [code,simp]: "step' S ({I} WHILE b DO {p} C {Q}) = {S \ 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 \ 'av st option acom option" where "AI c = pfp (step' \\<^bsub>vars c\<^esub>) (bot c)" @@ -194,7 +193,7 @@ next case (If b _ C1 _ C2) hence 0: "post C1 \ post C1 \ post C2 \ post C2 \ post C1 \ 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 \ X" using If.prems by simp note vars = `S \ L X` `vars b \ X` show ?case using If 0 @@ -259,10 +258,10 @@ lemma mono_afilter: "S1 \ L X \ S2 \ L X \ vars e \ X \ r1 \ r2 \ S1 \ S2 \ afilter e r1 S1 \ 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 \ S2 \ C1 \ C2 \ step' S1 C1 \ 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 diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int2_ivl.thy --- 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 \ i2 \ \ i2 \ (i1::ivl))" -definition join_rep :: "eint2 \ eint2 \ 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 \ eint2 \ 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 \ ivl \ ivl" is join_rep -by(auto simp: eq_ivl_iff join_rep_def) +lift_definition sup_ivl :: "ivl \ ivl \ 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 \ eint2 \ eint2" where -"meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))" +definition inf_rep :: "eint2 \ eint2 \ eint2" where +"inf_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))" -lemma \_meet_rep: "\_rep(meet_rep p1 p2) = \_rep p1 \ \_rep p2" -by(auto simp:meet_rep_def \_rep_cases split: prod.splits extended.splits) +lemma \_inf_rep: "\_rep(inf_rep p1 p2) = \_rep p1 \ \_rep p2" +by(auto simp:inf_rep_def \_rep_cases split: prod.splits extended.splits) -lift_definition meet_ivl :: "ivl \ ivl \ ivl" is meet_rep -by(auto simp: \_meet_rep eq_ivl_def) +lift_definition inf_ivl :: "ivl \ ivl \ ivl" is inf_rep +by(auto simp: \_inf_rep eq_ivl_def) definition "\ = empty_ivl" instance proof + case goal1 thus ?case + unfolding inf_rep_def by transfer (auto simp: le_iff_subset \_inf_rep) +next case goal2 thus ?case - unfolding meet_rep_def by transfer (auto simp: le_iff_subset \_meet_rep) + unfolding inf_rep_def by transfer (auto simp: le_iff_subset \_inf_rep) next case goal3 thus ?case - unfolding meet_rep_def by transfer (auto simp: le_iff_subset \_meet_rep) + unfolding inf_rep_def by transfer (auto simp: le_iff_subset \_inf_rep) next - case goal4 thus ?case - unfolding meet_rep_def by transfer (auto simp: le_iff_subset \_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\h2] = \ then False else l1 \ l2 & h1 \ h2)" unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty) -lemma join_ivl_nice: "[l1\h1] \ [l2\h2] = +lemma sup_ivl_nice: "[l1\h1] \ [l2\h2] = (if [l1\h1] = \ then [l2\h2] else if [l2\h2] = \ then [l1\h1] else [min l1 l2\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\h1] \ [l2\h2] = [max l1 l2\min h1 h2]" -by transfer (simp add: meet_rep_def) +lemma inf_ivl_nice: "[l1\h1] \ [l2\h2] = [max l1 l2\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 \_rep_cases split: prod.split extended.split) + by transfer (auto simp add:inf_rep_def \_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 \_plus_rep: "i1 : \_rep p1 \ i2 : \_rep p2 \ i1+i2 \ \_rep(plus_rep p1 p2)" by(auto simp: plus_rep_def plus_rep_plus split: prod.splits) -lemma non_empty_meet: "\n1 \ \_rep a1; n2 \ \_rep a2; n1 + n2 \ \_rep a \ \ - \ is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))" -by (auto simp add: \_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv) +lemma non_empty_inf: "\n1 \ \_rep a1; n2 \ \_rep a2; n1 + n2 \ \_rep a \ \ + \ is_empty_rep (inf_rep a1 (plus_rep a (uminus_rep a2)))" +by (auto simp add: \_inf_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv) (metis \_plus_rep \_uminus_rep add_diff_cancel diff_minus) -lemma filter_plus: "\eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \ - eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2; +lemma filter_plus: "\eq_ivl (inf_rep a1 (plus_rep a (uminus_rep a2))) b1 \ + eq_ivl (inf_rep a2 (plus_rep a (uminus_rep a1))) b2; n1 \ \_rep a1; n2 \ \_rep a2; n1 + n2 \ \_rep a\ \ n1 \ \_rep b1 \ n2 \ \_rep b2" -by (auto simp: eq_ivl_iff \_meet_rep non_empty_meet add_ac) +by (auto simp: eq_ivl_iff \_inf_rep non_empty_inf add_ac) (metis \_plus_rep \_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 \ le_rep q1 q2 \ le_rep (meet_rep p1 q1) (meet_rep p2 q2)" -by(auto simp add: le_iff_subset \_meet_rep) +lemma mono_inf_rep: "le_rep p1 p2 \ le_rep q1 q2 \ le_rep (inf_rep p1 q1) (inf_rep p2 q2)" +by(auto simp add: le_iff_subset \_inf_rep) lemma mono_plus_rep: "le_rep p1 p2 \ le_rep q1 q2 \ 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 diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_Int_init.thy --- 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 diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Abs_State.thy --- 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 \ 'a" -assumes join_ge1 [simp]: "x \ L X \ y \ L X \ x \ x \ y" -and join_ge2 [simp]: "x \ L X \ y \ L X \ y \ x \ y" -and join_least[simp]: "x \ z \ y \ z \ x \ y \ z" +assumes sup_ge1 [simp]: "x \ L X \ y \ L X \ x \ x \ y" +and sup_ge2 [simp]: "x \ L X \ y \ L X \ y \ x \ y" +and sup_least[simp]: "x \ z \ y \ z \ x \ y \ z" and Top[simp]: "x \ L X \ x \ Top X" and Top_in_L[simp]: "Top X \ L X" -and join_in_L[simp]: "x \ L X \ y \ L X \ x \ y \ L X" +and sup_in_L[simp]: "x \ L X \ y \ L X \ x \ y \ L X" notation (input) Top ("\\<^bsub>_\<^esub>") notation (latex output) 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 \ 'a st \ 'a st" where +definition sup_st :: "'a st \ 'a st \ 'a st" where "F \ (G::'a st) = St (\x. fun F x \ fun G x) (dom F)" instance .. @@ -197,7 +197,7 @@ definition Top_st :: "vname set \ 'a st" where "Top(X) = St (\x. \) 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 diff -r 1f5497c8ce8c -r 8a9f0503b1c0 src/HOL/IMP/Collecting.thy --- 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 "\" 65) and + inf (infixl "\