--- 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 +\<natural> xs = xs"
+lemma convex_plus_absorb [simp]: "xs +\<natural> 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 +\<natural>"
- proof qed (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
+lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
+by (rule mk_left_commute
+ [of "op +\<natural>", OF convex_plus_assoc convex_plus_commute])
-lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
-by (rule aci_convex_plus.mult_left_commute)
+lemma convex_plus_left_absorb [simp]: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
+by (simp only: convex_plus_assoc [symmetric] convex_plus_absorb)
-lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> 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}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> 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]:
--- 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 +\<flat> xs = xs"
+lemma lower_plus_absorb [simp]: "xs +\<flat> 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 +\<flat>"
- proof qed (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
+lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
+by (rule mk_left_commute [of "op +\<flat>", OF lower_plus_assoc lower_plus_commute])
-lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
-by (rule aci_lower_plus.mult_left_commute)
+lemma lower_plus_left_absorb [simp]: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
+by (simp only: lower_plus_assoc [symmetric] lower_plus_absorb)
-lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> 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 \<sqsubseteq> xs +\<flat> 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 \<Rightarrow> 'b::po"
- assumes f: "\<And>x y. f x \<sqsubseteq> f y \<longleftrightarrow> x \<sqsubseteq> y"
- shows "f x = f y \<longleftrightarrow> x = y"
-unfolding po_eq_conv by (simp add: f)
-
lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
-by (rule lower_unit_less_iff [THEN fooble])
+by (simp add: po_eq_conv)
lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
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]:
--- 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 +\<sharp> xs = xs"
+lemma upper_plus_absorb [simp]: "xs +\<sharp> 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 +\<sharp>"
- proof qed (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
+lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
+by (rule mk_left_commute [of "op +\<sharp>", OF upper_plus_assoc upper_plus_commute])
-lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
-by (rule aci_upper_plus.mult_left_commute)
+lemma upper_plus_left_absorb [simp]: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
+by (simp only: upper_plus_assoc [symmetric] upper_plus_absorb)
-lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> 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 +\<sharp> ys \<sqsubseteq> 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]: