avoid using ab_semigroup_idem_mult locale for powerdomains
authorhuffman
Thu Feb 19 06:47:06 2009 -0800 (2009-02-19)
changeset 29990b11793ea15a3
parent 29989 bdf83fc2c8ba
child 29991 c60ace776315
avoid using ab_semigroup_idem_mult locale for powerdomains
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/ConvexPD.thy	Thu Feb 19 05:50:26 2009 -0800
     1.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Feb 19 06:47:06 2009 -0800
     1.3 @@ -291,22 +291,26 @@
     1.4  apply (simp add: PDPlus_commute)
     1.5  done
     1.6  
     1.7 -lemma convex_plus_absorb: "xs +\<natural> xs = xs"
     1.8 +lemma convex_plus_absorb [simp]: "xs +\<natural> xs = xs"
     1.9  apply (induct xs rule: convex_pd.principal_induct, simp)
    1.10  apply (simp add: PDPlus_absorb)
    1.11  done
    1.12  
    1.13 -interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
    1.14 -  proof qed (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
    1.15 +lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
    1.16 +by (rule mk_left_commute
    1.17 +    [of "op +\<natural>", OF convex_plus_assoc convex_plus_commute])
    1.18  
    1.19 -lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
    1.20 -by (rule aci_convex_plus.mult_left_commute)
    1.21 +lemma convex_plus_left_absorb [simp]: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
    1.22 +by (simp only: convex_plus_assoc [symmetric] convex_plus_absorb)
    1.23  
    1.24 -lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
    1.25 -by (rule aci_convex_plus.mult_left_idem)
    1.26 -(*
    1.27 -lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
    1.28 -*)
    1.29 +text {* Useful for @{text "simp add: convex_plus_ac"} *}
    1.30 +lemmas convex_plus_ac =
    1.31 +  convex_plus_assoc convex_plus_commute convex_plus_left_commute
    1.32 +
    1.33 +text {* Useful for @{text "simp only: convex_plus_aci"} *}
    1.34 +lemmas convex_plus_aci =
    1.35 +  convex_plus_ac convex_plus_absorb convex_plus_left_absorb
    1.36 +
    1.37  lemma convex_unit_less_plus_iff [simp]:
    1.38    "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
    1.39   apply (rule iffI)
    1.40 @@ -413,7 +417,7 @@
    1.41  apply unfold_locales
    1.42  apply (simp add: convex_plus_assoc)
    1.43  apply (simp add: convex_plus_commute)
    1.44 -apply (simp add: convex_plus_absorb eta_cfun)
    1.45 +apply (simp add: eta_cfun)
    1.46  done
    1.47  
    1.48  lemma convex_bind_basis_simps [simp]:
     2.1 --- a/src/HOLCF/LowerPD.thy	Thu Feb 19 05:50:26 2009 -0800
     2.2 +++ b/src/HOLCF/LowerPD.thy	Thu Feb 19 06:47:06 2009 -0800
     2.3 @@ -245,22 +245,25 @@
     2.4  apply (simp add: PDPlus_commute)
     2.5  done
     2.6  
     2.7 -lemma lower_plus_absorb: "xs +\<flat> xs = xs"
     2.8 +lemma lower_plus_absorb [simp]: "xs +\<flat> xs = xs"
     2.9  apply (induct xs rule: lower_pd.principal_induct, simp)
    2.10  apply (simp add: PDPlus_absorb)
    2.11  done
    2.12  
    2.13 -interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
    2.14 -  proof qed (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
    2.15 +lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
    2.16 +by (rule mk_left_commute [of "op +\<flat>", OF lower_plus_assoc lower_plus_commute])
    2.17  
    2.18 -lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
    2.19 -by (rule aci_lower_plus.mult_left_commute)
    2.20 +lemma lower_plus_left_absorb [simp]: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
    2.21 +by (simp only: lower_plus_assoc [symmetric] lower_plus_absorb)
    2.22  
    2.23 -lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
    2.24 -by (rule aci_lower_plus.mult_left_idem)
    2.25 -(*
    2.26 -lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
    2.27 -*)
    2.28 +text {* Useful for @{text "simp add: lower_plus_ac"} *}
    2.29 +lemmas lower_plus_ac =
    2.30 +  lower_plus_assoc lower_plus_commute lower_plus_left_commute
    2.31 +
    2.32 +text {* Useful for @{text "simp only: lower_plus_aci"} *}
    2.33 +lemmas lower_plus_aci =
    2.34 +  lower_plus_ac lower_plus_absorb lower_plus_left_absorb
    2.35 +
    2.36  lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
    2.37  apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    2.38  apply (simp add: PDPlus_lower_less)
    2.39 @@ -315,14 +318,8 @@
    2.40    lower_plus_less_iff
    2.41    lower_unit_less_plus_iff
    2.42  
    2.43 -lemma fooble:
    2.44 -  fixes f :: "'a::po \<Rightarrow> 'b::po"
    2.45 -  assumes f: "\<And>x y. f x \<sqsubseteq> f y \<longleftrightarrow> x \<sqsubseteq> y"
    2.46 -  shows "f x = f y \<longleftrightarrow> x = y"
    2.47 -unfolding po_eq_conv by (simp add: f)
    2.48 -
    2.49  lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
    2.50 -by (rule lower_unit_less_iff [THEN fooble])
    2.51 +by (simp add: po_eq_conv)
    2.52  
    2.53  lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
    2.54  unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
    2.55 @@ -399,7 +396,7 @@
    2.56  apply unfold_locales
    2.57  apply (simp add: lower_plus_assoc)
    2.58  apply (simp add: lower_plus_commute)
    2.59 -apply (simp add: lower_plus_absorb eta_cfun)
    2.60 +apply (simp add: eta_cfun)
    2.61  done
    2.62  
    2.63  lemma lower_bind_basis_simps [simp]:
     3.1 --- a/src/HOLCF/UpperPD.thy	Thu Feb 19 05:50:26 2009 -0800
     3.2 +++ b/src/HOLCF/UpperPD.thy	Thu Feb 19 06:47:06 2009 -0800
     3.3 @@ -243,22 +243,25 @@
     3.4  apply (simp add: PDPlus_commute)
     3.5  done
     3.6  
     3.7 -lemma upper_plus_absorb: "xs +\<sharp> xs = xs"
     3.8 +lemma upper_plus_absorb [simp]: "xs +\<sharp> xs = xs"
     3.9  apply (induct xs rule: upper_pd.principal_induct, simp)
    3.10  apply (simp add: PDPlus_absorb)
    3.11  done
    3.12  
    3.13 -interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
    3.14 -  proof qed (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
    3.15 +lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
    3.16 +by (rule mk_left_commute [of "op +\<sharp>", OF upper_plus_assoc upper_plus_commute])
    3.17  
    3.18 -lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
    3.19 -by (rule aci_upper_plus.mult_left_commute)
    3.20 +lemma upper_plus_left_absorb [simp]: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
    3.21 +by (simp only: upper_plus_assoc [symmetric] upper_plus_absorb)
    3.22  
    3.23 -lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
    3.24 -by (rule aci_upper_plus.mult_left_idem)
    3.25 -(*
    3.26 -lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem
    3.27 -*)
    3.28 +text {* Useful for @{text "simp add: upper_plus_ac"} *}
    3.29 +lemmas upper_plus_ac =
    3.30 +  upper_plus_assoc upper_plus_commute upper_plus_left_commute
    3.31 +
    3.32 +text {* Useful for @{text "simp only: upper_plus_aci"} *}
    3.33 +lemmas upper_plus_aci =
    3.34 +  upper_plus_ac upper_plus_absorb upper_plus_left_absorb
    3.35 +
    3.36  lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
    3.37  apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    3.38  apply (simp add: PDPlus_upper_less)
    3.39 @@ -388,7 +391,7 @@
    3.40  apply unfold_locales
    3.41  apply (simp add: upper_plus_assoc)
    3.42  apply (simp add: upper_plus_commute)
    3.43 -apply (simp add: upper_plus_absorb eta_cfun)
    3.44 +apply (simp add: eta_cfun)
    3.45  done
    3.46  
    3.47  lemma upper_bind_basis_simps [simp]: