--- 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)
--- 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 *}
--- 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)
--- 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
--- 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
--- 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 =
--- 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 =
--- 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 =