# HG changeset patch # User huffman # Date 1235054826 28800 # Node ID b11793ea15a3caef8565e645d07226bc8279c5a5 # Parent bdf83fc2c8ba97a8122f39abea84710622b59ea0 avoid using ab_semigroup_idem_mult locale for powerdomains diff -r bdf83fc2c8ba -r b11793ea15a3 src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Thu Feb 19 05:50:26 2009 -0800 +++ b/src/HOLCF/ConvexPD.thy Thu Feb 19 06:47:06 2009 -0800 @@ -291,22 +291,26 @@ apply (simp add: PDPlus_commute) done -lemma convex_plus_absorb: "xs +\ xs = xs" +lemma convex_plus_absorb [simp]: "xs +\ xs = xs" apply (induct xs rule: convex_pd.principal_induct, simp) apply (simp add: PDPlus_absorb) done -interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\" - proof qed (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+ +lemma convex_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" +by (rule mk_left_commute + [of "op +\", OF convex_plus_assoc convex_plus_commute]) -lemma convex_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" -by (rule aci_convex_plus.mult_left_commute) +lemma convex_plus_left_absorb [simp]: "xs +\ (xs +\ ys) = xs +\ ys" +by (simp only: convex_plus_assoc [symmetric] convex_plus_absorb) -lemma convex_plus_left_absorb: "xs +\ (xs +\ ys) = xs +\ ys" -by (rule aci_convex_plus.mult_left_idem) -(* -lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem -*) +text {* Useful for @{text "simp add: convex_plus_ac"} *} +lemmas convex_plus_ac = + convex_plus_assoc convex_plus_commute convex_plus_left_commute + +text {* Useful for @{text "simp only: convex_plus_aci"} *} +lemmas convex_plus_aci = + convex_plus_ac convex_plus_absorb convex_plus_left_absorb + lemma convex_unit_less_plus_iff [simp]: "{x}\ \ ys +\ zs \ {x}\ \ ys \ {x}\ \ zs" apply (rule iffI) @@ -413,7 +417,7 @@ apply unfold_locales apply (simp add: convex_plus_assoc) apply (simp add: convex_plus_commute) -apply (simp add: convex_plus_absorb eta_cfun) +apply (simp add: eta_cfun) done lemma convex_bind_basis_simps [simp]: diff -r bdf83fc2c8ba -r b11793ea15a3 src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Thu Feb 19 05:50:26 2009 -0800 +++ b/src/HOLCF/LowerPD.thy Thu Feb 19 06:47:06 2009 -0800 @@ -245,22 +245,25 @@ apply (simp add: PDPlus_commute) done -lemma lower_plus_absorb: "xs +\ xs = xs" +lemma lower_plus_absorb [simp]: "xs +\ xs = xs" apply (induct xs rule: lower_pd.principal_induct, simp) apply (simp add: PDPlus_absorb) done -interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\" - proof qed (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+ +lemma lower_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" +by (rule mk_left_commute [of "op +\", OF lower_plus_assoc lower_plus_commute]) -lemma lower_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" -by (rule aci_lower_plus.mult_left_commute) +lemma lower_plus_left_absorb [simp]: "xs +\ (xs +\ ys) = xs +\ ys" +by (simp only: lower_plus_assoc [symmetric] lower_plus_absorb) -lemma lower_plus_left_absorb: "xs +\ (xs +\ ys) = xs +\ ys" -by (rule aci_lower_plus.mult_left_idem) -(* -lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem -*) +text {* Useful for @{text "simp add: lower_plus_ac"} *} +lemmas lower_plus_ac = + lower_plus_assoc lower_plus_commute lower_plus_left_commute + +text {* Useful for @{text "simp only: lower_plus_aci"} *} +lemmas lower_plus_aci = + lower_plus_ac lower_plus_absorb lower_plus_left_absorb + lemma lower_plus_less1: "xs \ xs +\ ys" apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp) apply (simp add: PDPlus_lower_less) @@ -315,14 +318,8 @@ lower_plus_less_iff lower_unit_less_plus_iff -lemma fooble: - fixes f :: "'a::po \ 'b::po" - assumes f: "\x y. f x \ f y \ x \ y" - shows "f x = f y \ x = y" -unfolding po_eq_conv by (simp add: f) - lemma lower_unit_eq_iff [simp]: "{x}\ = {y}\ \ x = y" -by (rule lower_unit_less_iff [THEN fooble]) +by (simp add: po_eq_conv) lemma lower_unit_strict [simp]: "{\}\ = \" unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp @@ -399,7 +396,7 @@ apply unfold_locales apply (simp add: lower_plus_assoc) apply (simp add: lower_plus_commute) -apply (simp add: lower_plus_absorb eta_cfun) +apply (simp add: eta_cfun) done lemma lower_bind_basis_simps [simp]: diff -r bdf83fc2c8ba -r b11793ea15a3 src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Thu Feb 19 05:50:26 2009 -0800 +++ b/src/HOLCF/UpperPD.thy Thu Feb 19 06:47:06 2009 -0800 @@ -243,22 +243,25 @@ apply (simp add: PDPlus_commute) done -lemma upper_plus_absorb: "xs +\ xs = xs" +lemma upper_plus_absorb [simp]: "xs +\ xs = xs" apply (induct xs rule: upper_pd.principal_induct, simp) apply (simp add: PDPlus_absorb) done -interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\" - proof qed (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+ +lemma upper_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" +by (rule mk_left_commute [of "op +\", OF upper_plus_assoc upper_plus_commute]) -lemma upper_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" -by (rule aci_upper_plus.mult_left_commute) +lemma upper_plus_left_absorb [simp]: "xs +\ (xs +\ ys) = xs +\ ys" +by (simp only: upper_plus_assoc [symmetric] upper_plus_absorb) -lemma upper_plus_left_absorb: "xs +\ (xs +\ ys) = xs +\ ys" -by (rule aci_upper_plus.mult_left_idem) -(* -lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem -*) +text {* Useful for @{text "simp add: upper_plus_ac"} *} +lemmas upper_plus_ac = + upper_plus_assoc upper_plus_commute upper_plus_left_commute + +text {* Useful for @{text "simp only: upper_plus_aci"} *} +lemmas upper_plus_aci = + upper_plus_ac upper_plus_absorb upper_plus_left_absorb + lemma upper_plus_less1: "xs +\ ys \ xs" apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp) apply (simp add: PDPlus_upper_less) @@ -388,7 +391,7 @@ apply unfold_locales apply (simp add: upper_plus_assoc) apply (simp add: upper_plus_commute) -apply (simp add: upper_plus_absorb eta_cfun) +apply (simp add: eta_cfun) done lemma upper_bind_basis_simps [simp]: