dropped mk_left_commute; use interpretation of locale abel_semigroup instead
authorhaftmann
Thu Jan 28 11:48:43 2010 +0100 (2010-01-28)
changeset 34973ae634fad947e
parent 34972 cc1d4c3ca9db
child 34974 18b41bba42b5
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
src/HOL/GCD.thy
src/HOL/Lattices.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Polynomial.thy
src/HOL/OrderedGroup.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOL/GCD.thy	Wed Jan 27 14:03:08 2010 +0100
     1.2 +++ b/src/HOL/GCD.thy	Thu Jan 28 11:48:43 2010 +0100
     1.3 @@ -302,28 +302,22 @@
     1.4  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
     1.5    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
     1.6  
     1.7 -lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
     1.8 -  by (rule dvd_antisym, auto)
     1.9 -
    1.10 -lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
    1.11 -  by (auto simp add: gcd_int_def gcd_commute_nat)
    1.12 +interpretation gcd_nat!: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.13 +proof
    1.14 +qed (auto intro: dvd_antisym dvd_trans)
    1.15  
    1.16 -lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
    1.17 -  apply (rule dvd_antisym)
    1.18 -  apply (blast intro: dvd_trans)+
    1.19 -done
    1.20 +interpretation gcd_int!: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.21 +proof
    1.22 +qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
    1.23  
    1.24 -lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
    1.25 -  by (auto simp add: gcd_int_def gcd_assoc_nat)
    1.26 -
    1.27 -lemmas gcd_left_commute_nat =
    1.28 -  mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
    1.29 -
    1.30 -lemmas gcd_left_commute_int =
    1.31 -  mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
    1.32 +lemmas gcd_assoc_nat = gcd_nat.assoc
    1.33 +lemmas gcd_commute_nat = gcd_nat.commute
    1.34 +lemmas gcd_left_commute_nat = gcd_nat.left_commute
    1.35 +lemmas gcd_assoc_int = gcd_int.assoc
    1.36 +lemmas gcd_commute_int = gcd_int.commute
    1.37 +lemmas gcd_left_commute_int = gcd_int.left_commute
    1.38  
    1.39  lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
    1.40 -  -- {* gcd is an AC-operator *}
    1.41  
    1.42  lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
    1.43  
    1.44 @@ -1250,13 +1244,6 @@
    1.45  lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
    1.46    unfolding lcm_int_def by simp
    1.47  
    1.48 -lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
    1.49 -  unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
    1.50 -
    1.51 -lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
    1.52 -  unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
    1.53 -
    1.54 -
    1.55  lemma lcm_pos_nat:
    1.56    "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
    1.57  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
    1.58 @@ -1344,10 +1331,10 @@
    1.59  done
    1.60  
    1.61  lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
    1.62 -  by (subst lcm_commute_nat, rule lcm_dvd1_nat)
    1.63 +  using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def times.commute gcd_nat.commute)
    1.64  
    1.65  lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
    1.66 -  by (subst lcm_commute_int, rule lcm_dvd1_int)
    1.67 +  using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def times.commute gcd_nat.commute)
    1.68  
    1.69  lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
    1.70  by(metis lcm_dvd1_nat dvd_trans)
    1.71 @@ -1369,6 +1356,34 @@
    1.72      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    1.73    by (auto intro: dvd_antisym [transferred] lcm_least_int)
    1.74  
    1.75 +interpretation lcm_nat!: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.76 +proof
    1.77 +  fix n m p :: nat
    1.78 +  show "lcm (lcm n m) p = lcm n (lcm m p)"
    1.79 +    by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
    1.80 +  show "lcm m n = lcm n m"
    1.81 +    by (simp add: lcm_nat_def gcd_commute_nat ring_simps)
    1.82 +qed
    1.83 +
    1.84 +interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
    1.85 +proof
    1.86 +  fix n m p :: int
    1.87 +  show "lcm (lcm n m) p = lcm n (lcm m p)"
    1.88 +    by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
    1.89 +  show "lcm m n = lcm n m"
    1.90 +    by (simp add: lcm_int_def lcm_nat.commute)
    1.91 +qed
    1.92 +
    1.93 +lemmas lcm_assoc_nat = lcm_nat.assoc
    1.94 +lemmas lcm_commute_nat = lcm_nat.commute
    1.95 +lemmas lcm_left_commute_nat = lcm_nat.left_commute
    1.96 +lemmas lcm_assoc_int = lcm_int.assoc
    1.97 +lemmas lcm_commute_int = lcm_int.commute
    1.98 +lemmas lcm_left_commute_int = lcm_int.left_commute
    1.99 +
   1.100 +lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   1.101 +lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   1.102 +
   1.103  lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   1.104    apply (rule sym)
   1.105    apply (subst lcm_unique_nat [symmetric])
   1.106 @@ -1399,18 +1414,6 @@
   1.107  lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
   1.108  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
   1.109  
   1.110 -lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
   1.111 -by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
   1.112 -
   1.113 -lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
   1.114 -by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
   1.115 -
   1.116 -lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
   1.117 -lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
   1.118 -
   1.119 -lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   1.120 -lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   1.121 -
   1.122  lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.123  proof qed (auto simp add: gcd_ac_nat)
   1.124  
     2.1 --- a/src/HOL/Lattices.thy	Wed Jan 27 14:03:08 2010 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Thu Jan 28 11:48:43 2010 +0100
     2.3 @@ -112,48 +112,73 @@
     2.4  
     2.5  subsubsection {* Equational laws *}
     2.6  
     2.7 +sublocale lower_semilattice < inf!: semilattice inf
     2.8 +proof
     2.9 +  fix a b c
    2.10 +  show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
    2.11 +    by (rule antisym) (auto intro: le_infI1 le_infI2)
    2.12 +  show "a \<sqinter> b = b \<sqinter> a"
    2.13 +    by (rule antisym) auto
    2.14 +  show "a \<sqinter> a = a"
    2.15 +    by (rule antisym) auto
    2.16 +qed
    2.17 +
    2.18  context lower_semilattice
    2.19  begin
    2.20  
    2.21 -lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
    2.22 -  by (rule antisym) auto
    2.23 +lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    2.24 +  by (fact inf.assoc)
    2.25  
    2.26 -lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    2.27 -  by (rule antisym) (auto intro: le_infI1 le_infI2)
    2.28 +lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
    2.29 +  by (fact inf.commute)
    2.30  
    2.31 -lemma inf_idem[simp]: "x \<sqinter> x = x"
    2.32 -  by (rule antisym) auto
    2.33 +lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
    2.34 +  by (fact inf.left_commute)
    2.35  
    2.36 -lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    2.37 -  by (rule antisym) (auto intro: le_infI2)
    2.38 +lemma inf_idem: "x \<sqinter> x = x"
    2.39 +  by (fact inf.idem)
    2.40 +
    2.41 +lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    2.42 +  by (fact inf.left_idem)
    2.43  
    2.44  lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    2.45    by (rule antisym) auto
    2.46  
    2.47  lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    2.48    by (rule antisym) auto
    2.49 -
    2.50 -lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
    2.51 -  by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
    2.52 -  
    2.53 + 
    2.54  lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
    2.55  
    2.56  end
    2.57  
    2.58 +sublocale upper_semilattice < sup!: semilattice sup
    2.59 +proof
    2.60 +  fix a b c
    2.61 +  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
    2.62 +    by (rule antisym) (auto intro: le_supI1 le_supI2)
    2.63 +  show "a \<squnion> b = b \<squnion> a"
    2.64 +    by (rule antisym) auto
    2.65 +  show "a \<squnion> a = a"
    2.66 +    by (rule antisym) auto
    2.67 +qed
    2.68 +
    2.69  context upper_semilattice
    2.70  begin
    2.71  
    2.72 -lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
    2.73 -  by (rule antisym) auto
    2.74 +lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    2.75 +  by (fact sup.assoc)
    2.76  
    2.77 -lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    2.78 -  by (rule antisym) (auto intro: le_supI1 le_supI2)
    2.79 +lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
    2.80 +  by (fact sup.commute)
    2.81  
    2.82 -lemma sup_idem[simp]: "x \<squnion> x = x"
    2.83 -  by (rule antisym) auto
    2.84 +lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    2.85 +  by (fact sup.left_commute)
    2.86  
    2.87 -lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    2.88 -  by (rule antisym) (auto intro: le_supI2)
    2.89 +lemma sup_idem: "x \<squnion> x = x"
    2.90 +  by (fact sup.idem)
    2.91 +
    2.92 +lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    2.93 +  by (fact sup.left_idem)
    2.94  
    2.95  lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    2.96    by (rule antisym) auto
    2.97 @@ -161,9 +186,6 @@
    2.98  lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    2.99    by (rule antisym) auto
   2.100  
   2.101 -lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   2.102 -  by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
   2.103 -
   2.104  lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
   2.105  
   2.106  end
   2.107 @@ -514,11 +536,12 @@
   2.108  lemmas le_maxI1 = min_max.sup_ge1
   2.109  lemmas le_maxI2 = min_max.sup_ge2
   2.110   
   2.111 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   2.112 -  mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
   2.113 +lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   2.114 +  min_max.inf.left_commute
   2.115  
   2.116 -lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   2.117 -  mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
   2.118 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   2.119 +  min_max.sup.left_commute
   2.120 +
   2.121  
   2.122  
   2.123  subsection {* Bool as lattice *}
     3.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Wed Jan 27 14:03:08 2010 +0100
     3.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Jan 28 11:48:43 2010 +0100
     3.3 @@ -24,15 +24,22 @@
     3.4    assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
     3.5    assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
     3.6    assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
     3.7 +
     3.8 +sublocale boolean < conj!: abel_semigroup conj proof
     3.9 +qed (fact conj_assoc conj_commute)+
    3.10 +
    3.11 +sublocale boolean < disj!: abel_semigroup disj proof
    3.12 +qed (fact disj_assoc disj_commute)+
    3.13 +
    3.14 +context boolean
    3.15  begin
    3.16  
    3.17 -lemmas disj_ac =
    3.18 -  disj_assoc disj_commute
    3.19 -  mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute]
    3.20 +lemmas conj_left_commute = conj.left_commute
    3.21  
    3.22 -lemmas conj_ac =
    3.23 -  conj_assoc conj_commute
    3.24 -  mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute]
    3.25 +lemmas disj_left_commute = disj.left_commute
    3.26 +
    3.27 +lemmas conj_ac = conj.assoc conj.commute conj.left_commute
    3.28 +lemmas disj_ac = disj.assoc disj.commute disj.left_commute
    3.29  
    3.30  lemma dual: "boolean disj conj compl one zero"
    3.31  apply (rule boolean.intro)
    3.32 @@ -178,18 +185,9 @@
    3.33  locale boolean_xor = boolean +
    3.34    fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
    3.35    assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
    3.36 -begin
    3.37  
    3.38 -lemma xor_def2:
    3.39 -  "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
    3.40 -by (simp only: xor_def conj_disj_distribs
    3.41 -               disj_ac conj_ac conj_cancel_right disj_zero_left)
    3.42 -
    3.43 -lemma xor_commute: "x \<oplus> y = y \<oplus> x"
    3.44 -by (simp only: xor_def conj_commute disj_commute)
    3.45 -
    3.46 -lemma xor_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    3.47 -proof -
    3.48 +sublocale boolean_xor < xor!: abel_semigroup xor proof
    3.49 +  fix x y z :: 'a
    3.50    let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
    3.51              (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
    3.52    have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
    3.53 @@ -199,11 +197,23 @@
    3.54      apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
    3.55      apply (simp only: conj_disj_distribs conj_ac disj_ac)
    3.56      done
    3.57 +  show "x \<oplus> y = y \<oplus> x"
    3.58 +    by (simp only: xor_def conj_commute disj_commute)
    3.59  qed
    3.60  
    3.61 -lemmas xor_ac =
    3.62 -  xor_assoc xor_commute
    3.63 -  mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute]
    3.64 +context boolean_xor
    3.65 +begin
    3.66 +
    3.67 +lemmas xor_assoc = xor.assoc
    3.68 +lemmas xor_commute = xor.commute
    3.69 +lemmas xor_left_commute = xor.left_commute
    3.70 +
    3.71 +lemmas xor_ac = xor.assoc xor.commute xor.left_commute
    3.72 +
    3.73 +lemma xor_def2:
    3.74 +  "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
    3.75 +by (simp only: xor_def conj_disj_distribs
    3.76 +               disj_ac conj_ac conj_cancel_right disj_zero_left)
    3.77  
    3.78  lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
    3.79  by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
     4.1 --- a/src/HOL/Library/Polynomial.thy	Wed Jan 27 14:03:08 2010 +0100
     4.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Jan 28 11:48:43 2010 +0100
     4.3 @@ -1200,14 +1200,18 @@
     4.4      by (rule poly_dvd_antisym)
     4.5  qed
     4.6  
     4.7 -lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
     4.8 -by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
     4.9 +interpretation poly_gcd!: abel_semigroup poly_gcd
    4.10 +proof
    4.11 +  fix x y z :: "'a poly"
    4.12 +  show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
    4.13 +    by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
    4.14 +  show "poly_gcd x y = poly_gcd y x"
    4.15 +    by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
    4.16 +qed
    4.17  
    4.18 -lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
    4.19 -by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
    4.20 -
    4.21 -lemmas poly_gcd_left_commute =
    4.22 -  mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
    4.23 +lemmas poly_gcd_assoc = poly_gcd.assoc
    4.24 +lemmas poly_gcd_commute = poly_gcd.commute
    4.25 +lemmas poly_gcd_left_commute = poly_gcd.left_commute
    4.26  
    4.27  lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
    4.28  
     5.1 --- a/src/HOL/OrderedGroup.thy	Wed Jan 27 14:03:08 2010 +0100
     5.2 +++ b/src/HOL/OrderedGroup.thy	Thu Jan 28 11:48:43 2010 +0100
     5.3 @@ -23,8 +23,7 @@
     5.4  *}
     5.5  
     5.6  ML {*
     5.7 -structure Algebra_Simps = Named_Thms
     5.8 -(
     5.9 +structure Algebra_Simps = Named_Thms(
    5.10    val name = "algebra_simps"
    5.11    val description = "algebra simplification rules"
    5.12  )
    5.13 @@ -44,14 +43,21 @@
    5.14  subsection {* Semigroups and Monoids *}
    5.15  
    5.16  class semigroup_add = plus +
    5.17 -  assumes add_assoc[algebra_simps]: "(a + b) + c = a + (b + c)"
    5.18 +  assumes add_assoc [algebra_simps]: "(a + b) + c = a + (b + c)"
    5.19 +
    5.20 +sublocale semigroup_add < plus!: semigroup plus proof
    5.21 +qed (fact add_assoc)
    5.22  
    5.23  class ab_semigroup_add = semigroup_add +
    5.24 -  assumes add_commute[algebra_simps]: "a + b = b + a"
    5.25 +  assumes add_commute [algebra_simps]: "a + b = b + a"
    5.26 +
    5.27 +sublocale ab_semigroup_add < plus!: abel_semigroup plus proof
    5.28 +qed (fact add_commute)
    5.29 +
    5.30 +context ab_semigroup_add
    5.31  begin
    5.32  
    5.33 -lemma add_left_commute[algebra_simps]: "a + (b + c) = b + (a + c)"
    5.34 -by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
    5.35 +lemmas add_left_commute [algebra_simps] = plus.left_commute
    5.36  
    5.37  theorems add_ac = add_assoc add_commute add_left_commute
    5.38  
    5.39 @@ -60,14 +66,21 @@
    5.40  theorems add_ac = add_assoc add_commute add_left_commute
    5.41  
    5.42  class semigroup_mult = times +
    5.43 -  assumes mult_assoc[algebra_simps]: "(a * b) * c = a * (b * c)"
    5.44 +  assumes mult_assoc [algebra_simps]: "(a * b) * c = a * (b * c)"
    5.45 +
    5.46 +sublocale semigroup_mult < times!: semigroup times proof
    5.47 +qed (fact mult_assoc)
    5.48  
    5.49  class ab_semigroup_mult = semigroup_mult +
    5.50 -  assumes mult_commute[algebra_simps]: "a * b = b * a"
    5.51 +  assumes mult_commute [algebra_simps]: "a * b = b * a"
    5.52 +
    5.53 +sublocale ab_semigroup_mult < times!: abel_semigroup times proof
    5.54 +qed (fact mult_commute)
    5.55 +
    5.56 +context ab_semigroup_mult
    5.57  begin
    5.58  
    5.59 -lemma mult_left_commute[algebra_simps]: "a * (b * c) = b * (a * c)"
    5.60 -by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
    5.61 +lemmas mult_left_commute [algebra_simps] = times.left_commute
    5.62  
    5.63  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    5.64  
    5.65 @@ -76,11 +89,15 @@
    5.66  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    5.67  
    5.68  class ab_semigroup_idem_mult = ab_semigroup_mult +
    5.69 -  assumes mult_idem[simp]: "x * x = x"
    5.70 +  assumes mult_idem: "x * x = x"
    5.71 +
    5.72 +sublocale ab_semigroup_idem_mult < times!: semilattice times proof
    5.73 +qed (fact mult_idem)
    5.74 +
    5.75 +context ab_semigroup_idem_mult
    5.76  begin
    5.77  
    5.78 -lemma mult_left_idem[simp]: "x * (x * y) = x * y"
    5.79 -  unfolding mult_assoc [symmetric, of x] mult_idem ..
    5.80 +lemmas mult_left_idem = times.left_idem
    5.81  
    5.82  end
    5.83  
    5.84 @@ -1370,8 +1387,8 @@
    5.85  (* term order for abelian groups *)
    5.86  
    5.87  fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
    5.88 -      [@{const_name HOL.zero}, @{const_name HOL.plus},
    5.89 -        @{const_name HOL.uminus}, @{const_name HOL.minus}]
    5.90 +      [@{const_name Algebras.zero}, @{const_name Algebras.plus},
    5.91 +        @{const_name Algebras.uminus}, @{const_name Algebras.minus}]
    5.92    | agrp_ord _ = ~1;
    5.93  
    5.94  fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
    5.95 @@ -1380,9 +1397,9 @@
    5.96    val ac1 = mk_meta_eq @{thm add_assoc};
    5.97    val ac2 = mk_meta_eq @{thm add_commute};
    5.98    val ac3 = mk_meta_eq @{thm add_left_commute};
    5.99 -  fun solve_add_ac thy _ (_ $ (Const (@{const_name HOL.plus},_) $ _ $ _) $ _) =
   5.100 +  fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) =
   5.101          SOME ac1
   5.102 -    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name HOL.plus},_) $ y $ z)) =
   5.103 +    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) =
   5.104          if termless_agrp (y, x) then SOME ac3 else NONE
   5.105      | solve_add_ac thy _ (_ $ x $ y) =
   5.106          if termless_agrp (y, x) then SOME ac2 else NONE
     6.1 --- a/src/HOLCF/ConvexPD.thy	Wed Jan 27 14:03:08 2010 +0100
     6.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Jan 28 11:48:43 2010 +0100
     6.3 @@ -279,29 +279,28 @@
     6.4    "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
     6.5  by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
     6.6  
     6.7 -lemma convex_plus_assoc:
     6.8 -  "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
     6.9 -apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
    6.10 -apply (rule_tac x=zs in convex_pd.principal_induct, simp)
    6.11 -apply (simp add: PDPlus_assoc)
    6.12 -done
    6.13 -
    6.14 -lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
    6.15 -apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
    6.16 -apply (simp add: PDPlus_commute)
    6.17 -done
    6.18 +interpretation convex_add!: semilattice convex_add proof
    6.19 +  fix xs ys zs :: "'a convex_pd"
    6.20 +  show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
    6.21 +    apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
    6.22 +    apply (rule_tac x=zs in convex_pd.principal_induct, simp)
    6.23 +    apply (simp add: PDPlus_assoc)
    6.24 +    done
    6.25 +  show "xs +\<natural> ys = ys +\<natural> xs"
    6.26 +    apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
    6.27 +    apply (simp add: PDPlus_commute)
    6.28 +    done
    6.29 +  show "xs +\<natural> xs = xs"
    6.30 +    apply (induct xs rule: convex_pd.principal_induct, simp)
    6.31 +    apply (simp add: PDPlus_absorb)
    6.32 +    done
    6.33 +qed
    6.34  
    6.35 -lemma convex_plus_absorb [simp]: "xs +\<natural> xs = xs"
    6.36 -apply (induct xs rule: convex_pd.principal_induct, simp)
    6.37 -apply (simp add: PDPlus_absorb)
    6.38 -done
    6.39 -
    6.40 -lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
    6.41 -by (rule mk_left_commute
    6.42 -    [of "op +\<natural>", OF convex_plus_assoc convex_plus_commute])
    6.43 -
    6.44 -lemma convex_plus_left_absorb [simp]: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
    6.45 -by (simp only: convex_plus_assoc [symmetric] convex_plus_absorb)
    6.46 +lemmas convex_plus_assoc = convex_add.assoc
    6.47 +lemmas convex_plus_commute = convex_add.commute
    6.48 +lemmas convex_plus_absorb = convex_add.idem
    6.49 +lemmas convex_plus_left_commute = convex_add.left_commute
    6.50 +lemmas convex_plus_left_absorb = convex_add.left_idem
    6.51  
    6.52  text {* Useful for @{text "simp add: convex_plus_ac"} *}
    6.53  lemmas convex_plus_ac =
     7.1 --- a/src/HOLCF/LowerPD.thy	Wed Jan 27 14:03:08 2010 +0100
     7.2 +++ b/src/HOLCF/LowerPD.thy	Thu Jan 28 11:48:43 2010 +0100
     7.3 @@ -234,27 +234,28 @@
     7.4    "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
     7.5  by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
     7.6  
     7.7 -lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
     7.8 -apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
     7.9 -apply (rule_tac x=zs in lower_pd.principal_induct, simp)
    7.10 -apply (simp add: PDPlus_assoc)
    7.11 -done
    7.12 -
    7.13 -lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
    7.14 -apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    7.15 -apply (simp add: PDPlus_commute)
    7.16 -done
    7.17 +interpretation lower_add!: semilattice lower_add proof
    7.18 +  fix xs ys zs :: "'a lower_pd"
    7.19 +  show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
    7.20 +    apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
    7.21 +    apply (rule_tac x=zs in lower_pd.principal_induct, simp)
    7.22 +    apply (simp add: PDPlus_assoc)
    7.23 +    done
    7.24 +  show "xs +\<flat> ys = ys +\<flat> xs"
    7.25 +    apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    7.26 +    apply (simp add: PDPlus_commute)
    7.27 +    done
    7.28 +  show "xs +\<flat> xs = xs"
    7.29 +    apply (induct xs rule: lower_pd.principal_induct, simp)
    7.30 +    apply (simp add: PDPlus_absorb)
    7.31 +    done
    7.32 +qed
    7.33  
    7.34 -lemma lower_plus_absorb [simp]: "xs +\<flat> xs = xs"
    7.35 -apply (induct xs rule: lower_pd.principal_induct, simp)
    7.36 -apply (simp add: PDPlus_absorb)
    7.37 -done
    7.38 -
    7.39 -lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
    7.40 -by (rule mk_left_commute [of "op +\<flat>", OF lower_plus_assoc lower_plus_commute])
    7.41 -
    7.42 -lemma lower_plus_left_absorb [simp]: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
    7.43 -by (simp only: lower_plus_assoc [symmetric] lower_plus_absorb)
    7.44 +lemmas lower_plus_assoc = lower_add.assoc
    7.45 +lemmas lower_plus_commute = lower_add.commute
    7.46 +lemmas lower_plus_absorb = lower_add.idem
    7.47 +lemmas lower_plus_left_commute = lower_add.left_commute
    7.48 +lemmas lower_plus_left_absorb = lower_add.left_idem
    7.49  
    7.50  text {* Useful for @{text "simp add: lower_plus_ac"} *}
    7.51  lemmas lower_plus_ac =
     8.1 --- a/src/HOLCF/UpperPD.thy	Wed Jan 27 14:03:08 2010 +0100
     8.2 +++ b/src/HOLCF/UpperPD.thy	Thu Jan 28 11:48:43 2010 +0100
     8.3 @@ -232,27 +232,28 @@
     8.4    "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
     8.5  by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
     8.6  
     8.7 -lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
     8.8 -apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
     8.9 -apply (rule_tac x=zs in upper_pd.principal_induct, simp)
    8.10 -apply (simp add: PDPlus_assoc)
    8.11 -done
    8.12 -
    8.13 -lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
    8.14 -apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    8.15 -apply (simp add: PDPlus_commute)
    8.16 -done
    8.17 +interpretation upper_add!: semilattice upper_add proof
    8.18 +  fix xs ys zs :: "'a upper_pd"
    8.19 +  show "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
    8.20 +    apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
    8.21 +    apply (rule_tac x=zs in upper_pd.principal_induct, simp)
    8.22 +    apply (simp add: PDPlus_assoc)
    8.23 +    done
    8.24 +  show "xs +\<sharp> ys = ys +\<sharp> xs"
    8.25 +    apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    8.26 +    apply (simp add: PDPlus_commute)
    8.27 +    done
    8.28 +  show "xs +\<sharp> xs = xs"
    8.29 +    apply (induct xs rule: upper_pd.principal_induct, simp)
    8.30 +    apply (simp add: PDPlus_absorb)
    8.31 +    done
    8.32 +qed
    8.33  
    8.34 -lemma upper_plus_absorb [simp]: "xs +\<sharp> xs = xs"
    8.35 -apply (induct xs rule: upper_pd.principal_induct, simp)
    8.36 -apply (simp add: PDPlus_absorb)
    8.37 -done
    8.38 -
    8.39 -lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
    8.40 -by (rule mk_left_commute [of "op +\<sharp>", OF upper_plus_assoc upper_plus_commute])
    8.41 -
    8.42 -lemma upper_plus_left_absorb [simp]: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
    8.43 -by (simp only: upper_plus_assoc [symmetric] upper_plus_absorb)
    8.44 +lemmas upper_plus_assoc = upper_add.assoc
    8.45 +lemmas upper_plus_commute = upper_add.commute
    8.46 +lemmas upper_plus_absorb = upper_add.idem
    8.47 +lemmas upper_plus_left_commute = upper_add.left_commute
    8.48 +lemmas upper_plus_left_absorb = upper_add.left_idem
    8.49  
    8.50  text {* Useful for @{text "simp add: upper_plus_ac"} *}
    8.51  lemmas upper_plus_ac =