# HG changeset patch
# User paulson
# Date 1080809672 -7200
# Node ID 7a3d80e276d412c0ff49993661e37f3c427647b7
# Parent  255ad604e08e4c8c9be0039ec9d85f47289a02a8
new type class abelian_group

diff -r 255ad604e08e -r 7a3d80e276d4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Mar 31 16:10:53 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Apr 01 10:54:32 2004 +0200
@@ -9,65 +9,6 @@
 
 theory Finite_Set = Divides + Power + Inductive:
 
-subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
-
-axclass plus_ac0 < plus, zero
-  commute:     "x + y = y + x"
-  assoc:       "(x + y) + z = x + (y + z)"
-  zero [simp]: "0 + x = x"
-
-lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
-apply (rule plus_ac0.commute [THEN trans])
-apply (rule plus_ac0.assoc [THEN trans])
-apply (rule plus_ac0.commute [THEN arg_cong])
-done
-
-lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
-apply (rule plus_ac0.commute [THEN trans])
-apply (rule plus_ac0.zero)
-done
-
-lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
-                  plus_ac0.zero plus_ac0_zero_right
-
-instance almost_semiring < plus_ac0
-proof qed (rule add_commute add_assoc almost_semiring.add_0)+
-
-axclass times_ac1 < times, one
-  commute:     "x * y = y * x"
-  assoc:       "(x * y) * z = x * (y * z)"
-  one [simp]:  "1 * x = x"
-
-theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
-  y * (x * z)"
-proof -
-  have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
-    by (rule times_ac1.assoc [THEN sym])
-  also have "x * y = y * x"
-    by (rule times_ac1.commute)
-  also have "(y * x) * z = y * (x * z)"
-    by (rule times_ac1.assoc)
-  finally show ?thesis .
-qed
-
-theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"
-proof -
-  have "x * 1 = 1 * x"
-    by (rule times_ac1.commute)
-  also have "... = x"
-    by (rule times_ac1.one)
-  finally show ?thesis .
-qed
-
-instance almost_semiring < times_ac1
-  apply intro_classes
-  apply (rule mult_commute)
-  apply (rule mult_assoc, simp)
-  done
-
-theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute
-  times_ac1.one times_ac1_one_right
-
 subsection {* Collection of finite sets *}
 
 consts Finites :: "'a set set"
@@ -957,9 +898,7 @@
 lemma setsum_Un_ring: "finite A ==> finite B ==>
     (setsum f (A Un B) :: 'a :: ring) =
       setsum f A + setsum f B - setsum f (A Int B)"
-  apply (subst setsum_Un_Int [symmetric], auto)
-  apply (simp add: compare_rls)
-  done
+  by (subst setsum_Un_Int [symmetric], auto)
 
 lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
     (if a:A then setsum f A - f a else setsum f A)"
diff -r 255ad604e08e -r 7a3d80e276d4 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed Mar 31 16:10:53 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Apr 01 10:54:32 2004 +0200
@@ -14,11 +14,66 @@
 
 subsection {* Abstract algebraic structures *}
 
-text{*This class underlies both @{text semiring} and @{text ring}*}
-axclass almost_semiring \<subseteq> zero, one, plus, times
+subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
+
+axclass plus_ac0 \<subseteq> plus, zero
+  commute:     "x + y = y + x"
+  assoc:       "(x + y) + z = x + (y + z)"
+  zero [simp]: "0 + x = x"
+
+lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.assoc [THEN trans])
+apply (rule plus_ac0.commute [THEN arg_cong])
+done
+
+lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.zero)
+done
+
+lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
+                  plus_ac0.zero plus_ac0_zero_right
+
+axclass times_ac1 \<subseteq> times, one
+  commute:     "x * y = y * x"
+  assoc:       "(x * y) * z = x * (y * z)"
+  one [simp]:  "1 * x = x"
+
+theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
+  y * (x * z)"
+proof -
+  have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
+    by (rule times_ac1.assoc [THEN sym])
+  also have "x * y = y * x"
+    by (rule times_ac1.commute)
+  also have "(y * x) * z = y * (x * z)"
+    by (rule times_ac1.assoc)
+  finally show ?thesis .
+qed
+
+theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"
+proof -
+  have "x * 1 = 1 * x"
+    by (rule times_ac1.commute)
+  also have "... = x"
+    by (rule times_ac1.one)
+  finally show ?thesis .
+qed
+
+theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute
+  times_ac1.one times_ac1_one_right
+
+
+text{*This class is the same as @{text plus_ac0}, while using the same axiom
+names as the other axclasses.*}
+axclass abelian_semigroup \<subseteq> zero, plus
   add_assoc: "(a + b) + c = a + (b + c)"
   add_commute: "a + b = b + a"
   add_0 [simp]: "0 + a = a"
+
+text{*This class underlies both @{text semiring} and @{text ring}*}
+axclass almost_semiring \<subseteq> abelian_semigroup, one, times
   mult_assoc: "(a * b) * c = a * (b * c)"
   mult_commute: "a * b = b * a"
   mult_1 [simp]: "1 * a = a"
@@ -26,15 +81,34 @@
   left_distrib: "(a + b) * c = a * c + b * c"
   zero_neq_one [simp]: "0 \<noteq> 1"
 
+
 axclass semiring \<subseteq> almost_semiring
   add_left_imp_eq: "a + b = a + c ==> b=c"
     --{*This axiom is needed for semirings only: for rings, etc., it is
         redundant. Including it allows many more of the following results
         to be proved for semirings too.*}
 
-axclass ring \<subseteq> almost_semiring, minus
-  left_minus [simp]: "- a + a = 0"
-  diff_minus: "a - b = a + (-b)"
+instance abelian_semigroup \<subseteq> plus_ac0
+proof
+  fix x y z :: 'a
+  show "x + y = y + x" by (rule add_commute)
+  show "x + y + z = x + (y + z)" by (rule add_assoc)
+  show "0+x = x" by (rule add_0)
+qed
+
+instance almost_semiring \<subseteq> times_ac1
+proof
+  fix x y z :: 'a
+  show "x * y = y * x" by (rule mult_commute)
+  show "x * y * z = x * (y * z)" by (rule mult_assoc)
+  show "1*x = x" by simp
+qed
+
+axclass abelian_group \<subseteq> abelian_semigroup, minus
+   left_minus [simp]: "-a + a = 0"
+   diff_minus: "a - b = a + -b"
+
+axclass ring \<subseteq> almost_semiring, abelian_group
 
 text{*Proving axiom @{text add_left_imp_eq} makes all @{text semiring}
       theorems available to members of @{term ring} *}
@@ -69,26 +143,26 @@
 
 subsection {* Derived Rules for Addition *}
 
-lemma add_0_right [simp]: "a + 0 = (a::'a::almost_semiring)"
+lemma add_0_right [simp]: "a + 0 = (a::'a::plus_ac0)"
 proof -
-  have "a + 0 = 0 + a" by (simp only: add_commute)
+  have "a + 0 = 0 + a" by (rule plus_ac0.commute)
   also have "... = a" by simp
   finally show ?thesis .
 qed
 
-lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::almost_semiring))"
-  by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
+lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::plus_ac0))"
+  by (rule mk_left_commute [of "op +", OF plus_ac0.assoc plus_ac0.commute])
 
 theorems add_ac = add_assoc add_commute add_left_commute
 
-lemma right_minus [simp]: "a + -(a::'a::ring) = 0"
+lemma right_minus [simp]: "a + -(a::'a::abelian_group) = 0"
 proof -
   have "a + -a = -a + a" by (simp add: add_ac)
   also have "... = 0" by simp
   finally show ?thesis .
 qed
 
-lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))"
+lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::abelian_group))"
 proof
   have "a = a - b + b" by (simp add: diff_minus add_ac)
   also assume "a - b = 0"
@@ -106,33 +180,32 @@
      "(b + a = c + a) = (b = (c::'a::semiring))"
   by (simp add: add_commute)
 
-lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
-proof (rule add_left_cancel [of "-a", THEN iffD1])
-  show "(-a + -(-a) = -a + a)"
-  by simp
-qed
+lemma minus_minus [simp]: "- (- (a::'a::abelian_group)) = a" 
+apply (rule right_minus_eq [THEN iffD1]) 
+apply (simp add: diff_minus) 
+done
 
-lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
+lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::abelian_group)"
 apply (rule right_minus_eq [THEN iffD1, symmetric])
 apply (simp add: diff_minus add_commute) 
 done
 
-lemma minus_zero [simp]: "- 0 = (0::'a::ring)"
+lemma minus_zero [simp]: "- 0 = (0::'a::abelian_group)"
 by (simp add: equals_zero_I)
 
-lemma diff_self [simp]: "a - (a::'a::ring) = 0"
+lemma diff_self [simp]: "a - (a::'a::abelian_group) = 0"
   by (simp add: diff_minus)
 
-lemma diff_0 [simp]: "(0::'a::ring) - a = -a"
+lemma diff_0 [simp]: "(0::'a::abelian_group) - a = -a"
 by (simp add: diff_minus)
 
-lemma diff_0_right [simp]: "a - (0::'a::ring) = a" 
+lemma diff_0_right [simp]: "a - (0::'a::abelian_group) = a" 
 by (simp add: diff_minus)
 
-lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ring)"
+lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::abelian_group)"
 by (simp add: diff_minus)
 
-lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" 
+lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::abelian_group))" 
 proof 
   assume "- a = - b"
   hence "- (- a) = - (- b)"
@@ -143,21 +216,33 @@
   thus "-a = -b" by simp
 qed
 
-lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
+lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::abelian_group))"
+by (subst neg_equal_iff_equal [symmetric], simp)
+
+lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::abelian_group))"
 by (subst neg_equal_iff_equal [symmetric], simp)
 
-lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))"
-by (subst neg_equal_iff_equal [symmetric], simp)
+lemma add_minus_self [simp]: "a + b - b = (a::'a::abelian_group)"; 
+  by (simp add: diff_minus add_assoc)
+
+lemma add_minus_self_left [simp]:  "a + (b - a)  = (b::'a::abelian_group)";
+by (simp add: diff_minus add_left_commute [of a]) 
+
+lemma add_minus_self_right  [simp]:  "a + b - a  = (b::'a::abelian_group)";
+by (simp add: diff_minus add_left_commute [of a] add_assoc) 
+
+lemma minus_add_self [simp]: "a - b + b = (a::'a::abelian_group)"; 
+by (simp add: diff_minus add_assoc) 
 
 text{*The next two equations can make the simplifier loop!*}
 
-lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))"
+lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::abelian_group))"
 proof -
   have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
   thus ?thesis by (simp add: eq_commute)
 qed
 
-lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)"
+lemma minus_equation_iff: "(- a = b) = (- (b::'a::abelian_group) = a)"
 proof -
   have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
   thus ?thesis by (simp add: eq_commute)
@@ -206,9 +291,9 @@
      "a*e + (b*e + c) = (a+b)*e + (c::'a::almost_semiring)"
 by (simp add: left_distrib add_ac)
 
-lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
+lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::abelian_group)"
 apply (rule equals_zero_I)
-apply (simp add: add_ac) 
+apply (simp add: plus_ac0) 
 done
 
 lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
@@ -388,23 +473,23 @@
 
 subsection{*Subtraction Laws*}
 
-lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ring)"
-by (simp add: diff_minus add_ac)
+lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::abelian_group)"
+by (simp add: diff_minus plus_ac0)
 
-lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ring)"
-by (simp add: diff_minus add_ac)
+lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::abelian_group)"
+by (simp add: diff_minus plus_ac0)
 
-lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ring))"
+lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::abelian_group))"
 by (auto simp add: diff_minus add_assoc)
 
-lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ring) = c)"
+lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::abelian_group) = c)"
 by (auto simp add: diff_minus add_assoc)
 
-lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ring))"
-by (simp add: diff_minus add_ac)
+lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::abelian_group))"
+by (simp add: diff_minus plus_ac0)
 
-lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ring)"
-by (simp add: diff_minus add_ac)
+lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::abelian_group)"
+by (simp add: diff_minus plus_ac0)
 
 text{*Further subtraction laws for ordered rings*}
 
@@ -446,7 +531,7 @@
 
 subsection{*Lemmas for the @{text cancel_numerals} simproc*}
 
-lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ring))"
+lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::abelian_group))"
 by (simp add: compare_rls)
 
 lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::ordered_ring))"