# HG changeset patch
# User paulson
# Date 959098132 -7200
# Node ID a1c42654175776f8f33048d5784fc9c7ff548191
# Parent  548901d05a0ee88323064718b4298ed434a53966
Now that 0 is overloaded, constant "zero" and its type class "zero" are
no longer needed.  Also IntRingDefs is redundant

diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/Group.ML
--- a/src/HOL/ex/Group.ML	Tue May 23 18:06:22 2000 +0200
+++ b/src/HOL/ex/Group.ML	Tue May 23 18:08:52 2000 +0200
@@ -7,48 +7,48 @@
 (*** Groups ***)
 
 (* Derives the well-known convergent set of equations for groups
-   based on the unary inverse zero-x.
+   based on the unary inverse 0-x.
 *)
 
-Goal "!!x::'a::add_group. (zero-x)+(x+y) = y";
+Goal "!!x::'a::add_group. (0-x)+(x+y) = y";
 by (rtac trans 1);
 by (rtac (plus_assoc RS sym) 1);
 by (stac left_inv 1);
 by (rtac zeroL 1);
 qed "left_inv2";
 
-Goal "!!x::'a::add_group. (zero-(zero-x)) = x";
+Goal "!!x::'a::add_group. (0-(0-x)) = x";
 by (rtac trans 1);
-by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (res_inst_tac [("x","0-x")] left_inv2 2);
 by (stac left_inv 1);
 by (rtac (zeroR RS sym) 1);
 qed "inv_inv";
 
-Goal "zero-zero = (zero::'a::add_group)";
+Goal "0-0 = (0::'a::add_group)";
 by (rtac trans 1);
 by (rtac (zeroR RS sym) 1);
 by (rtac trans 1);
-by (res_inst_tac [("x","zero")] left_inv2 2);
+by (res_inst_tac [("x","0")] left_inv2 2);
 by (simp_tac (simpset() addsimps [zeroR]) 1);
 qed "inv_zero";
 
-Goal "!!x::'a::add_group. x+(zero-x) = zero";
+Goal "!!x::'a::add_group. x+(0-x) = 0";
 by (rtac trans 1);
-by (res_inst_tac [("x","zero-x")] left_inv 2);
+by (res_inst_tac [("x","0-x")] left_inv 2);
 by (stac inv_inv 1);
 by (rtac refl 1);
 qed "right_inv";
 
-Goal "!!x::'a::add_group. x+((zero-x)+y) = y";
+Goal "!!x::'a::add_group. x+((0-x)+y) = y";
 by (rtac trans 1);
-by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (res_inst_tac [("x","0-x")] left_inv2 2);
 by (stac inv_inv 1);
 by (rtac refl 1);
 qed "right_inv2";
 
 val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
 
-Goal "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
+Goal "!!x::'a::add_group. 0-(x+y) = (0-y)+(0-x)";
 by (rtac trans 1);
  by (rtac zeroR 2);
 by (rtac trans 1);
@@ -65,7 +65,7 @@
 by (rtac (zeroL RS sym) 1);
 qed "inv_plus";
 
-(*** convergent TRS for groups with unary inverse zero-x ***)
+(*** convergent TRS for groups with unary inverse 0-x ***)
 val group1_simps =
   [zeroL,zeroR,plus_assoc,left_inv,left_inv2,right_inv,right_inv2,inv_inv,
    inv_zero,inv_plus];
@@ -76,9 +76,9 @@
 
 (* I believe there is no convergent TRS for groups with binary `-',
    unless you have an extra unary `-' and simply define x-y = x+(-y).
-   This does not work with only a binary `-' because x-y = x+(zero-y) does
+   This does not work with only a binary `-' because x-y = x+(0-y) does
    not terminate. Hence we have a special tactic for converting all
-   occurrences of x-y into x+(zero-y):
+   occurrences of x-y into x+(0-y):
 *)
 
 local
@@ -102,12 +102,12 @@
 (* The following two equations are not used in any of the decision procedures,
    but are still very useful. They also demonstrate mk_group1_tac.
 *)
-Goal "x-x = (zero::'a::add_group)";
+Goal "x-x = (0::'a::add_group)";
 by (mk_group1_tac 1);
 by (group1_tac 1);
 qed "minus_self_zero";
 
-Goal "x-zero = (x::'a::add_group)";
+Goal "x-0 = (x::'a::add_group)";
 by (mk_group1_tac 1);
 by (group1_tac 1);
 qed "minus_zero";
@@ -122,7 +122,7 @@
 by (simp_tac (simpset() addsimps [plus_commute]) 1);
 qed "plus_commuteL";
 
-(* Convergent TRS for Abelian groups with unary inverse zero-x.
+(* Convergent TRS for Abelian groups with unary inverse 0-x.
    Requires ordered rewriting
 *)
 
@@ -182,34 +182,34 @@
    it merely decides equality.
 (* Phase 1 *)
 
-Goal "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
+Goal "!!x::'a::add_agroup. (x+(0-y))+z = (x+z)+(0-y)";
 by (Simp_tac 1);
 val lemma = result();
 bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
-Goal "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
+Goal "!!x::'a::add_agroup. x+(0-(y+z)) = (x+(0-y))+(0-z)";
 by (Simp_tac 1);
 val lemma = result();
 bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
-Goal "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
+Goal "!!x::'a::add_agroup. x+(0-(y+(0-z))) = (x+z)+(0-y)";
 by (Simp_tac 1);
 val lemma = result();
 bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
-Goal "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
+Goal "!!x::'a::add_agroup. x+(y+(0-z)) = (x+y)+(0-z)";
 by (Simp_tac 1);
 val lemma = result();
 bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
 (* Phase 2 *)
 
-Goal "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
+Goal "!!x::'a::add_agroup. (x+y)+(0-z) = x+(y+(0-z))";
 by (Simp_tac 1);
 val lemma = result();
 bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
-Goal "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
+Goal "!!x::'a::add_agroup. (x+y)+(0-x) = y";
 by (rtac (plus_assoc RS trans) 1);
 by (rtac trans 1);
  by (rtac plus_cong 1);
diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/Group.thy
--- a/src/HOL/ex/Group.thy	Tue May 23 18:06:22 2000 +0200
+++ b/src/HOL/ex/Group.thy	Tue May 23 18:08:52 2000 +0200
@@ -6,11 +6,7 @@
 A little bit of group theory leading up to rings. Hence groups are additive.
 *)
 
-Group = Set +
-
-(* 0 already used in Nat *)
-axclass  zero < term
-consts   zero :: "'a::zero"
+Group = Main +
 
 (* additive semigroups *)
 
@@ -21,20 +17,20 @@
 (* additive monoids *)
 
 axclass  add_monoid < add_semigroup, zero
-  zeroL    "zero + x = x"
-  zeroR    "x + zero = x"
+  zeroL    "0 + x = x"
+  zeroR    "x + 0 = x"
 
 (* additive groups *)
 (*
 The inverse is the binary `-'. Groups with unary and binary inverse are
-interdefinable: x-y := x+(zero-y) and -x := zero-x. The law left_inv is
-simply the translation of (-x)+x = zero. This characterizes groups already,
-provided we only allow (zero-x). Law minus_inv `defines' the general x-y in
-terms of the specific zero-y.
+interdefinable: x-y := x+(0-y) and -x := 0-x. The law left_inv is
+simply the translation of (-x)+x = 0. This characterizes groups already,
+provided we only allow (0-x). Law minus_inv `defines' the general x-y in
+terms of the specific 0-y.
 *)
 axclass  add_group < add_monoid, minus
-  left_inv  "(zero-x)+x = zero"
-  minus_inv "x-y = x + (zero-y)"
+  left_inv  "(0-x)+x = 0"
+  minus_inv "x-y = x + (0-y)"
 
 (* additive abelian groups *)
 
diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/IntRing.thy
--- a/src/HOL/ex/IntRing.thy	Tue May 23 18:06:22 2000 +0200
+++ b/src/HOL/ex/IntRing.thy	Tue May 23 18:08:52 2000 +0200
@@ -7,11 +7,11 @@
 With an application of Lagrange's lemma.
 *)
 
-IntRing = IntRingDefs + Lagrange +
+IntRing = Ring + Lagrange +
 
 instance int :: add_semigroup (zadd_assoc)
-instance int :: add_monoid (zero_int_def,zadd_int0,zadd_int0_right)
-instance int :: add_group (left_inv_int,minus_inv_int)
+instance int :: add_monoid (IntDef.Zero_def,zadd_int0,zadd_int0_right)
+instance int :: add_group {|Auto_tac|}
 instance int :: add_agroup (zadd_commute)
 instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
 instance int :: cring (zmult_commute)
diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/IntRingDefs.ML
--- a/src/HOL/ex/IntRingDefs.ML	Tue May 23 18:06:22 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title:      HOL/ex/IntRingDefs.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow and Markus Wenzel
-    Copyright   1996 TU Muenchen
-*)
-
-Goalw [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
-by (Simp_tac 1);
-qed "left_inv_int";
-
-Goalw [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
-by (Simp_tac 1);
-qed "minus_inv_int";
diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/IntRingDefs.thy
--- a/src/HOL/ex/IntRingDefs.thy	Tue May 23 18:06:22 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      HOL/ex/IntRingDefs.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow and Markus Wenzel
-    Copyright   1996 TU Muenchen
-
-Provides the basic defs and thms for showing that int is a commutative ring.
-Most of it has been defined and shown already.
-*)
-
-IntRingDefs = Main + Ring +
-
-instance int :: zero
-defs zero_int_def "zero::int == int 0"
-
-end
diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Tue May 23 18:06:22 2000 +0200
+++ b/src/HOL/ex/Primes.ML	Tue May 23 18:08:52 2000 +0200
@@ -23,7 +23,7 @@
 val prems = goal thy
      "[| !!m. P m 0;     \
 \        !!m n. [| 0<n;  P n (m mod n) |] ==> P m n  \
-\     |] ==> P m n";
+\     |] ==> P (m::nat) (n::nat)";
 by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1);
 by (case_tac "n=0" 1);
 by (asm_simp_tac (simpset() addsimps prems) 1);
diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/Ring.ML
--- a/src/HOL/ex/Ring.ML	Tue May 23 18:06:22 2000 +0200
+++ b/src/HOL/ex/Ring.ML	Tue May 23 18:08:52 2000 +0200
@@ -17,7 +17,7 @@
 
 val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
 
-Goal "!!x::'a::ring. zero*x = zero";
+Goal "!!x::'a::ring. 0*x = 0";
 by (rtac trans 1);
  by (rtac right_inv 2);
 by (rtac trans 1);
@@ -37,7 +37,7 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_zeroL";
 
-Goal "!!x::'a::ring. x*zero = zero";
+Goal "!!x::'a::ring. x*0 = 0";
 by (rtac trans 1);
  by (rtac right_inv 2);
 by (rtac trans 1);
@@ -57,7 +57,7 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_zeroR";
 
-Goal "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
+Goal "!!x::'a::ring. (0-x)*y = 0-(x*y)";
 by (rtac trans 1);
  by (rtac zeroL 2);
 by (rtac trans 1);
@@ -83,7 +83,7 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_invL";
 
-Goal "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
+Goal "!!x::'a::ring. x*(0-y) = 0-(x*y)";
 by (rtac trans 1);
  by (rtac zeroL 2);
 by (rtac trans 1);