Now that 0 is overloaded, constant "zero" and its type class "zero" are
no longer needed. Also IntRingDefs is redundant
--- 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);
--- 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 *)
--- 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)
--- 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";
--- 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
--- 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);
--- 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);