# HG changeset patch
# User haftmann
# Date 1264675723 -3600
# Node ID ae634fad947e3a8c67340d058edafac070ef632f
# Parent  cc1d4c3ca9db4df7a38e390bfc4af4e4e9cec612
dropped mk_left_commute; use interpretation of locale abel_semigroup instead

diff -r cc1d4c3ca9db -r ae634fad947e src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/GCD.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -302,28 +302,22 @@
 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
 
-lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
-  by (rule dvd_antisym, auto)
-
-lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
-  by (auto simp add: gcd_int_def gcd_commute_nat)
+interpretation gcd_nat!: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
+proof
+qed (auto intro: dvd_antisym dvd_trans)
 
-lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
-  apply (rule dvd_antisym)
-  apply (blast intro: dvd_trans)+
-done
+interpretation gcd_int!: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
+proof
+qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
 
-lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
-  by (auto simp add: gcd_int_def gcd_assoc_nat)
-
-lemmas gcd_left_commute_nat =
-  mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
-
-lemmas gcd_left_commute_int =
-  mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
+lemmas gcd_assoc_nat = gcd_nat.assoc
+lemmas gcd_commute_nat = gcd_nat.commute
+lemmas gcd_left_commute_nat = gcd_nat.left_commute
+lemmas gcd_assoc_int = gcd_int.assoc
+lemmas gcd_commute_int = gcd_int.commute
+lemmas gcd_left_commute_int = gcd_int.left_commute
 
 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
-  -- {* gcd is an AC-operator *}
 
 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
 
@@ -1250,13 +1244,6 @@
 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
   unfolding lcm_int_def by simp
 
-lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
-  unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
-
-lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
-  unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
-
-
 lemma lcm_pos_nat:
   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
@@ -1344,10 +1331,10 @@
 done
 
 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
-  by (subst lcm_commute_nat, rule lcm_dvd1_nat)
+  using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def times.commute gcd_nat.commute)
 
 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
-  by (subst lcm_commute_int, rule lcm_dvd1_int)
+  using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def times.commute gcd_nat.commute)
 
 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
 by(metis lcm_dvd1_nat dvd_trans)
@@ -1369,6 +1356,34 @@
     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   by (auto intro: dvd_antisym [transferred] lcm_least_int)
 
+interpretation lcm_nat!: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+proof
+  fix n m p :: nat
+  show "lcm (lcm n m) p = lcm n (lcm m p)"
+    by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
+  show "lcm m n = lcm n m"
+    by (simp add: lcm_nat_def gcd_commute_nat ring_simps)
+qed
+
+interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
+proof
+  fix n m p :: int
+  show "lcm (lcm n m) p = lcm n (lcm m p)"
+    by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
+  show "lcm m n = lcm n m"
+    by (simp add: lcm_int_def lcm_nat.commute)
+qed
+
+lemmas lcm_assoc_nat = lcm_nat.assoc
+lemmas lcm_commute_nat = lcm_nat.commute
+lemmas lcm_left_commute_nat = lcm_nat.left_commute
+lemmas lcm_assoc_int = lcm_int.assoc
+lemmas lcm_commute_int = lcm_int.commute
+lemmas lcm_left_commute_int = lcm_int.left_commute
+
+lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
+lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
+
 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   apply (rule sym)
   apply (subst lcm_unique_nat [symmetric])
@@ -1399,18 +1414,6 @@
 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
 
-lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
-by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
-
-lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
-by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
-
-lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
-lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
-
-lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
-lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
-
 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
 proof qed (auto simp add: gcd_ac_nat)
 
diff -r cc1d4c3ca9db -r ae634fad947e src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/Lattices.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -112,48 +112,73 @@
 
 subsubsection {* Equational laws *}
 
+sublocale lower_semilattice < inf!: semilattice inf
+proof
+  fix a b c
+  show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
+    by (rule antisym) (auto intro: le_infI1 le_infI2)
+  show "a \<sqinter> b = b \<sqinter> a"
+    by (rule antisym) auto
+  show "a \<sqinter> a = a"
+    by (rule antisym) auto
+qed
+
 context lower_semilattice
 begin
 
-lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
-  by (rule antisym) auto
+lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+  by (fact inf.assoc)
 
-lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
-  by (rule antisym) (auto intro: le_infI1 le_infI2)
+lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
+  by (fact inf.commute)
 
-lemma inf_idem[simp]: "x \<sqinter> x = x"
-  by (rule antisym) auto
+lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
+  by (fact inf.left_commute)
 
-lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
-  by (rule antisym) (auto intro: le_infI2)
+lemma inf_idem: "x \<sqinter> x = x"
+  by (fact inf.idem)
+
+lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+  by (fact inf.left_idem)
 
 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   by (rule antisym) auto
 
 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   by (rule antisym) auto
-
-lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
-  by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
-  
+ 
 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
 
 end
 
+sublocale upper_semilattice < sup!: semilattice sup
+proof
+  fix a b c
+  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
+    by (rule antisym) (auto intro: le_supI1 le_supI2)
+  show "a \<squnion> b = b \<squnion> a"
+    by (rule antisym) auto
+  show "a \<squnion> a = a"
+    by (rule antisym) auto
+qed
+
 context upper_semilattice
 begin
 
-lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
-  by (rule antisym) auto
+lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+  by (fact sup.assoc)
 
-lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
-  by (rule antisym) (auto intro: le_supI1 le_supI2)
+lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
+  by (fact sup.commute)
 
-lemma sup_idem[simp]: "x \<squnion> x = x"
-  by (rule antisym) auto
+lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
+  by (fact sup.left_commute)
 
-lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
-  by (rule antisym) (auto intro: le_supI2)
+lemma sup_idem: "x \<squnion> x = x"
+  by (fact sup.idem)
+
+lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
+  by (fact sup.left_idem)
 
 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   by (rule antisym) auto
@@ -161,9 +186,6 @@
 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   by (rule antisym) auto
 
-lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
-  by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
-
 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
 
 end
@@ -514,11 +536,12 @@
 lemmas le_maxI1 = min_max.sup_ge1
 lemmas le_maxI2 = min_max.sup_ge2
  
-lemmas max_ac = min_max.sup_assoc min_max.sup_commute
-  mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
+lemmas min_ac = min_max.inf_assoc min_max.inf_commute
+  min_max.inf.left_commute
 
-lemmas min_ac = min_max.inf_assoc min_max.inf_commute
-  mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
+lemmas max_ac = min_max.sup_assoc min_max.sup_commute
+  min_max.sup.left_commute
+
 
 
 subsection {* Bool as lattice *}
diff -r cc1d4c3ca9db -r ae634fad947e src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -24,15 +24,22 @@
   assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
   assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
   assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
+
+sublocale boolean < conj!: abel_semigroup conj proof
+qed (fact conj_assoc conj_commute)+
+
+sublocale boolean < disj!: abel_semigroup disj proof
+qed (fact disj_assoc disj_commute)+
+
+context boolean
 begin
 
-lemmas disj_ac =
-  disj_assoc disj_commute
-  mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute]
+lemmas conj_left_commute = conj.left_commute
 
-lemmas conj_ac =
-  conj_assoc conj_commute
-  mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute]
+lemmas disj_left_commute = disj.left_commute
+
+lemmas conj_ac = conj.assoc conj.commute conj.left_commute
+lemmas disj_ac = disj.assoc disj.commute disj.left_commute
 
 lemma dual: "boolean disj conj compl one zero"
 apply (rule boolean.intro)
@@ -178,18 +185,9 @@
 locale boolean_xor = boolean +
   fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
   assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
-begin
 
-lemma xor_def2:
-  "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
-by (simp only: xor_def conj_disj_distribs
-               disj_ac conj_ac conj_cancel_right disj_zero_left)
-
-lemma xor_commute: "x \<oplus> y = y \<oplus> x"
-by (simp only: xor_def conj_commute disj_commute)
-
-lemma xor_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-proof -
+sublocale boolean_xor < xor!: abel_semigroup xor proof
+  fix x y z :: 'a
   let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
             (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
   have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
@@ -199,11 +197,23 @@
     apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
     apply (simp only: conj_disj_distribs conj_ac disj_ac)
     done
+  show "x \<oplus> y = y \<oplus> x"
+    by (simp only: xor_def conj_commute disj_commute)
 qed
 
-lemmas xor_ac =
-  xor_assoc xor_commute
-  mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute]
+context boolean_xor
+begin
+
+lemmas xor_assoc = xor.assoc
+lemmas xor_commute = xor.commute
+lemmas xor_left_commute = xor.left_commute
+
+lemmas xor_ac = xor.assoc xor.commute xor.left_commute
+
+lemma xor_def2:
+  "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
+by (simp only: xor_def conj_disj_distribs
+               disj_ac conj_ac conj_cancel_right disj_zero_left)
 
 lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
 by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
diff -r cc1d4c3ca9db -r ae634fad947e src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -1200,14 +1200,18 @@
     by (rule poly_dvd_antisym)
 qed
 
-lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
-by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+interpretation poly_gcd!: abel_semigroup poly_gcd
+proof
+  fix x y z :: "'a poly"
+  show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
+    by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
+  show "poly_gcd x y = poly_gcd y x"
+    by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+qed
 
-lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
-by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
-
-lemmas poly_gcd_left_commute =
-  mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
+lemmas poly_gcd_assoc = poly_gcd.assoc
+lemmas poly_gcd_commute = poly_gcd.commute
+lemmas poly_gcd_left_commute = poly_gcd.left_commute
 
 lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
 
diff -r cc1d4c3ca9db -r ae634fad947e src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/OrderedGroup.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -23,8 +23,7 @@
 *}
 
 ML {*
-structure Algebra_Simps = Named_Thms
-(
+structure Algebra_Simps = Named_Thms(
   val name = "algebra_simps"
   val description = "algebra simplification rules"
 )
@@ -44,14 +43,21 @@
 subsection {* Semigroups and Monoids *}
 
 class semigroup_add = plus +
-  assumes add_assoc[algebra_simps]: "(a + b) + c = a + (b + c)"
+  assumes add_assoc [algebra_simps]: "(a + b) + c = a + (b + c)"
+
+sublocale semigroup_add < plus!: semigroup plus proof
+qed (fact add_assoc)
 
 class ab_semigroup_add = semigroup_add +
-  assumes add_commute[algebra_simps]: "a + b = b + a"
+  assumes add_commute [algebra_simps]: "a + b = b + a"
+
+sublocale ab_semigroup_add < plus!: abel_semigroup plus proof
+qed (fact add_commute)
+
+context ab_semigroup_add
 begin
 
-lemma add_left_commute[algebra_simps]: "a + (b + c) = b + (a + c)"
-by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
+lemmas add_left_commute [algebra_simps] = plus.left_commute
 
 theorems add_ac = add_assoc add_commute add_left_commute
 
@@ -60,14 +66,21 @@
 theorems add_ac = add_assoc add_commute add_left_commute
 
 class semigroup_mult = times +
-  assumes mult_assoc[algebra_simps]: "(a * b) * c = a * (b * c)"
+  assumes mult_assoc [algebra_simps]: "(a * b) * c = a * (b * c)"
+
+sublocale semigroup_mult < times!: semigroup times proof
+qed (fact mult_assoc)
 
 class ab_semigroup_mult = semigroup_mult +
-  assumes mult_commute[algebra_simps]: "a * b = b * a"
+  assumes mult_commute [algebra_simps]: "a * b = b * a"
+
+sublocale ab_semigroup_mult < times!: abel_semigroup times proof
+qed (fact mult_commute)
+
+context ab_semigroup_mult
 begin
 
-lemma mult_left_commute[algebra_simps]: "a * (b * c) = b * (a * c)"
-by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
+lemmas mult_left_commute [algebra_simps] = times.left_commute
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
@@ -76,11 +89,15 @@
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
 class ab_semigroup_idem_mult = ab_semigroup_mult +
-  assumes mult_idem[simp]: "x * x = x"
+  assumes mult_idem: "x * x = x"
+
+sublocale ab_semigroup_idem_mult < times!: semilattice times proof
+qed (fact mult_idem)
+
+context ab_semigroup_idem_mult
 begin
 
-lemma mult_left_idem[simp]: "x * (x * y) = x * y"
-  unfolding mult_assoc [symmetric, of x] mult_idem ..
+lemmas mult_left_idem = times.left_idem
 
 end
 
@@ -1370,8 +1387,8 @@
 (* term order for abelian groups *)
 
 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
-      [@{const_name HOL.zero}, @{const_name HOL.plus},
-        @{const_name HOL.uminus}, @{const_name HOL.minus}]
+      [@{const_name Algebras.zero}, @{const_name Algebras.plus},
+        @{const_name Algebras.uminus}, @{const_name Algebras.minus}]
   | agrp_ord _ = ~1;
 
 fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
@@ -1380,9 +1397,9 @@
   val ac1 = mk_meta_eq @{thm add_assoc};
   val ac2 = mk_meta_eq @{thm add_commute};
   val ac3 = mk_meta_eq @{thm add_left_commute};
-  fun solve_add_ac thy _ (_ $ (Const (@{const_name HOL.plus},_) $ _ $ _) $ _) =
+  fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) =
         SOME ac1
-    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name HOL.plus},_) $ y $ z)) =
+    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) =
         if termless_agrp (y, x) then SOME ac3 else NONE
     | solve_add_ac thy _ (_ $ x $ y) =
         if termless_agrp (y, x) then SOME ac2 else NONE
diff -r cc1d4c3ca9db -r ae634fad947e src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -279,29 +279,28 @@
   "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
 
-lemma convex_plus_assoc:
-  "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
-apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
-apply (rule_tac x=zs in convex_pd.principal_induct, simp)
-apply (simp add: PDPlus_assoc)
-done
-
-lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
-apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
+interpretation convex_add!: semilattice convex_add proof
+  fix xs ys zs :: "'a convex_pd"
+  show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
+    apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
+    apply (rule_tac x=zs in convex_pd.principal_induct, simp)
+    apply (simp add: PDPlus_assoc)
+    done
+  show "xs +\<natural> ys = ys +\<natural> xs"
+    apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
+    apply (simp add: PDPlus_commute)
+    done
+  show "xs +\<natural> xs = xs"
+    apply (induct xs rule: convex_pd.principal_induct, simp)
+    apply (simp add: PDPlus_absorb)
+    done
+qed
 
-lemma convex_plus_absorb [simp]: "xs +\<natural> xs = xs"
-apply (induct xs rule: convex_pd.principal_induct, simp)
-apply (simp add: PDPlus_absorb)
-done
-
-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_absorb [simp]: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
-by (simp only: convex_plus_assoc [symmetric] convex_plus_absorb)
+lemmas convex_plus_assoc = convex_add.assoc
+lemmas convex_plus_commute = convex_add.commute
+lemmas convex_plus_absorb = convex_add.idem
+lemmas convex_plus_left_commute = convex_add.left_commute
+lemmas convex_plus_left_absorb = convex_add.left_idem
 
 text {* Useful for @{text "simp add: convex_plus_ac"} *}
 lemmas convex_plus_ac =
diff -r cc1d4c3ca9db -r ae634fad947e src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOLCF/LowerPD.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -234,27 +234,28 @@
   "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
 by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
 
-lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
-apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
-apply (rule_tac x=zs in lower_pd.principal_induct, simp)
-apply (simp add: PDPlus_assoc)
-done
-
-lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
-apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
+interpretation lower_add!: semilattice lower_add proof
+  fix xs ys zs :: "'a lower_pd"
+  show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
+    apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
+    apply (rule_tac x=zs in lower_pd.principal_induct, simp)
+    apply (simp add: PDPlus_assoc)
+    done
+  show "xs +\<flat> ys = ys +\<flat> xs"
+    apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
+    apply (simp add: PDPlus_commute)
+    done
+  show "xs +\<flat> xs = xs"
+    apply (induct xs rule: lower_pd.principal_induct, simp)
+    apply (simp add: PDPlus_absorb)
+    done
+qed
 
-lemma lower_plus_absorb [simp]: "xs +\<flat> xs = xs"
-apply (induct xs rule: lower_pd.principal_induct, simp)
-apply (simp add: PDPlus_absorb)
-done
-
-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_absorb [simp]: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
-by (simp only: lower_plus_assoc [symmetric] lower_plus_absorb)
+lemmas lower_plus_assoc = lower_add.assoc
+lemmas lower_plus_commute = lower_add.commute
+lemmas lower_plus_absorb = lower_add.idem
+lemmas lower_plus_left_commute = lower_add.left_commute
+lemmas lower_plus_left_absorb = lower_add.left_idem
 
 text {* Useful for @{text "simp add: lower_plus_ac"} *}
 lemmas lower_plus_ac =
diff -r cc1d4c3ca9db -r ae634fad947e src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOLCF/UpperPD.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -232,27 +232,28 @@
   "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
 by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
 
-lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
-apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
-apply (rule_tac x=zs in upper_pd.principal_induct, simp)
-apply (simp add: PDPlus_assoc)
-done
-
-lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
-apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
+interpretation upper_add!: semilattice upper_add proof
+  fix xs ys zs :: "'a upper_pd"
+  show "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
+    apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
+    apply (rule_tac x=zs in upper_pd.principal_induct, simp)
+    apply (simp add: PDPlus_assoc)
+    done
+  show "xs +\<sharp> ys = ys +\<sharp> xs"
+    apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
+    apply (simp add: PDPlus_commute)
+    done
+  show "xs +\<sharp> xs = xs"
+    apply (induct xs rule: upper_pd.principal_induct, simp)
+    apply (simp add: PDPlus_absorb)
+    done
+qed
 
-lemma upper_plus_absorb [simp]: "xs +\<sharp> xs = xs"
-apply (induct xs rule: upper_pd.principal_induct, simp)
-apply (simp add: PDPlus_absorb)
-done
-
-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_absorb [simp]: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
-by (simp only: upper_plus_assoc [symmetric] upper_plus_absorb)
+lemmas upper_plus_assoc = upper_add.assoc
+lemmas upper_plus_commute = upper_add.commute
+lemmas upper_plus_absorb = upper_add.idem
+lemmas upper_plus_left_commute = upper_add.left_commute
+lemmas upper_plus_left_absorb = upper_add.left_idem
 
 text {* Useful for @{text "simp add: upper_plus_ac"} *}
 lemmas upper_plus_ac =