# HG changeset patch
# User ballarin
# Date 981791561 -3600
# Node ID 62c2e0af1d30d81cef1f0cec447128e1c1fa0b14
# Parent  69c1abb9a12992e4de7cd4720418790807ee93e2
Changes to HOL/Algebra:
- Axclasses consolidated (axiom one_not_zero).
- Now uses summation operator setsum; SUM has been removed.
- Priority of infix assoc changed to 50, in accordance to dvd.

diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/Field.thy
--- a/src/HOL/Algebra/abstract/Field.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/Field.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -4,10 +4,10 @@
     Author: Clemens Ballarin, started 15 November 1997
 *)
 
-Field = Factor + Ideal +
+Field = Factor + PID +
 
 instance
-  field < domain (field_integral)
+  field < domain (field_one_not_zero, field_integral)
 
 instance
   field < factorial (TrueI, field_fact_prime)
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/Ideal.ML
--- a/src/HOL/Algebra/abstract/Ideal.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -8,7 +8,7 @@
 
 Goalw [is_ideal_def]
   "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \
-\     !! a. a:I ==> - a : I; <0> : I; \
+\     !! a. a:I ==> - a : I; 0 : I; \
 \     !! a r. a:I ==> a * r : I |] ==> is_ideal I";
 by Auto_tac;
 qed "is_idealI";
@@ -21,7 +21,7 @@
 by (Fast_tac 1);
 qed "is_ideal_uminus";
 
-Goalw [is_ideal_def] "[| is_ideal I |] ==> <0> : I";
+Goalw [is_ideal_def] "[| is_ideal I |] ==> 0 : I";
 by (Fast_tac 1);
 qed "is_ideal_zero";
 
@@ -37,7 +37,7 @@
 by Auto_tac;
 qed "UNIV_is_ideal";
 
-Goalw [is_ideal_def] "is_ideal {<0>::'a::ring}";
+Goalw [is_ideal_def] "is_ideal {0::'a::ring}";
 by Auto_tac;
 qed "zero_is_ideal";
 
@@ -56,8 +56,8 @@
 by (res_inst_tac [("x", "v+va")] exI 1);
 by (res_inst_tac [("x", "-u")] exI 2);
 by (res_inst_tac [("x", "-v")] exI 2);
-by (res_inst_tac [("x", "<0>")] exI 3);
-by (res_inst_tac [("x", "<0>")] exI 3);
+by (res_inst_tac [("x", "0")] exI 3);
+by (res_inst_tac [("x", "0")] exI 3);
 by (res_inst_tac [("x", "u * r")] exI 4);
 by (res_inst_tac [("x", "v * r")] exI 4);
 by (REPEAT (simp_tac (simpset() addsimps [r_distr, l_distr, r_minus, minus_add, m_assoc]@a_ac) 1));
@@ -78,7 +78,7 @@
   (* loops if is_ideal_mult is added as non-safe rule *)
 qed "ideal_of_one_eq";
 
-Goalw [ideal_of_def] "ideal_of {} = {<0>::'a::ring}";
+Goalw [ideal_of_def] "ideal_of {} = {0::'a::ring}";
 by (rtac subset_antisym 1);
 by (rtac subsetI 1);
 by (dtac InterD 1);
@@ -103,8 +103,8 @@
 by (assume_tac 2);
 by (auto_tac (claset() addIs [is_ideal_2], simpset()));
 by (res_inst_tac [("x", "<1>")] exI 1);
-by (res_inst_tac [("x", "<0>")] exI 1);
-by (res_inst_tac [("x", "<0>")] exI 2);
+by (res_inst_tac [("x", "0")] exI 1);
+by (res_inst_tac [("x", "0")] exI 2);
 by (res_inst_tac [("x", "<1>")] exI 2);
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -114,7 +114,7 @@
 by Auto_tac;
 qed "ideal_of_mono";
 
-Goal "ideal_of {<0>::'a::ring} = {<0>}";
+Goal "ideal_of {0::'a::ring} = {0}";
 by (simp_tac (simpset() addsimps [pideal_structure]) 1);
 by (rtac subset_antisym 1);
 by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
@@ -203,7 +203,7 @@
 by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
 by (rtac in_pideal_imp_dvd 1);
 by (Asm_simp_tac 1);
-by (res_inst_tac [("x", "<0>")] exI 1);
+by (res_inst_tac [("x", "0")] exI 1);
 by (res_inst_tac [("x", "<1>")] exI 1);
 by (Simp_tac 1);
 qed "not_dvd_psubideal";
@@ -289,7 +289,7 @@
 
 (* Fields are Pid *)
 
-Goal "a ~= <0> ==> ideal_of {a::'a::field} = UNIV";
+Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV";
 by (rtac subset_antisym 1);
 by (Simp_tac 1);
 by (rtac subset_trans 1);
@@ -299,15 +299,15 @@
 by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
 qed "field_pideal_univ";
 
-Goal "[| is_ideal I; I ~= {<0>} |] ==> {<0>} < I";
+Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I";
 by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1);
 qed "proper_ideal";
 
 Goalw [is_pideal_def] "is_ideal (I::('a::field) set) ==> is_pideal I";
-by (case_tac "I = {<0>}" 1);
-by (res_inst_tac [("x", "<0>")] exI 1);
+by (case_tac "I = {0}" 1);
+by (res_inst_tac [("x", "0")] exI 1);
 by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1);
-(* case "I ~= {<0>}" *)
+(* case "I ~= {0}" *)
 by (ftac proper_ideal 1);
 by (assume_tac 1);
 by (dtac psubset_imp_ex_mem 1);
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/Ideal.thy
--- a/src/HOL/Algebra/abstract/Ideal.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ideal.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -13,7 +13,7 @@
 
 defs
   is_ideal_def	"is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
-                               (ALL a: I. - a : I) & <0> : I &
+                               (ALL a: I. - a : I) & 0 : I &
                                (ALL a: I. ALL r. a * r : I)"
   ideal_of_def	"ideal_of S == Inter {I. is_ideal I & S <= I}"
   is_pideal_def	"is_pideal I == (EX a. I = ideal_of {a})"
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/NatSum.ML
--- a/src/HOL/Algebra/abstract/NatSum.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/NatSum.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -6,18 +6,18 @@
 
 section "Basic Properties";
 
-Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";
+Goal "setsum f {..0::nat} = (f 0::'a::ring)";
 by (Asm_simp_tac 1);
 qed "SUM_0";
 
-Goalw [SUM_def]
-  "SUM (Suc n) f = (f (Suc n) + SUM n f::'a::ring)";
-by (Simp_tac 1);
+Goal "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::ring)";
+by (simp_tac (simpset() addsimps [atMost_Suc]) 1);
 qed "SUM_Suc";
 
 Addsimps [SUM_0, SUM_Suc];
 
-Goal "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";
+Goal
+  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::ring)";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
@@ -27,8 +27,8 @@
 
 (* Congruence rules *)
 
-Goal "ALL j'. j=j' --> (ALL i. i<=j' --> f i = (f' i :: 'a :: ring)) \
-\     --> SUM j f = SUM j' f'";
+Goal "ALL j'::nat. j=j' --> (ALL i. i<=j' --> f i = (f' i :: 'a :: ring)) \
+\     --> setsum f {..j} = setsum f' {..j'}";
 by (induct_tac "j" 1);
 by Auto_tac;  
 bind_thm ("SUM_cong", (impI RS allI) RSN (2, result() RS spec RS mp RS mp));
@@ -38,7 +38,7 @@
 
 section "Ring Properties";
 
-Goal "SUM n (%i. <0>) = (<0>::'a::ring)";
+Goal "setsum (%i. 0) {..n::nat} = (0::'a::ring)";
 by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -47,7 +47,8 @@
 Addsimps [SUM_zero];
 
 Goal
-  "!!f::nat=>'a::ring. SUM n (%i. f i + g i) = SUM n f + SUM n g";
+  "!!f::nat=>'a::ring. \
+\  setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
@@ -56,7 +57,7 @@
 qed "SUM_add";
 
 Goal
-  "!!a::'a::ring. SUM n f * a = SUM n (%i. f i * a)";
+  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
@@ -64,7 +65,8 @@
 by (asm_simp_tac (simpset() addsimps [l_distr]) 1);
 qed "SUM_ldistr";
 
-Goal "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";
+Goal
+  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
@@ -76,8 +78,8 @@
 
 Goal
   "!!a::nat=>'a::ring. k <= n --> \
-\  SUM k (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
-\  SUM k (%j. a j * SUM (k-j) (%i. b i * c (n-j-i)))";
+\  setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = \
+\  setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}";
 by (induct_tac "k" 1);
 (* Base case *)
 by (simp_tac (simpset() addsimps [m_assoc]) 1);
@@ -93,14 +95,15 @@
 
 Goal
   "!!a::nat=>'a::ring. \
-\  SUM n (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
-\  SUM n (%j. a j * SUM (n-j) (%i. b i * c (n-(j+i))))";
+\  setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..n} = \
+\  setsum (%j. a j * setsum (%i. b i * c (n-(j+i))) {..n-j}) {..n}";
 by (asm_simp_tac (simpset() addsimps [poly_assoc_lemma1]) 1);
 qed "poly_assoc_lemma";
 
 Goal
   "!! a::nat=>'a::ring. j <= n --> \
-\    SUM j (%i. a i * b (n-i)) = SUM j (%i. a (n-i-(n-j)) * b (i+(n-j)))";
+\    setsum (%i. a i * b (n-i)) {..j} = \
+\    setsum (%i. a (n-i-(n-j)) * b (i+(n-j))) {..j}";
 by (Simp_tac 1); 
 by (induct_tac "j" 1);
 (* Base case *)
@@ -111,7 +114,9 @@
 qed "poly_comm_lemma1";
 
 Goal
- "!!a::nat=>'a::ring. SUM n (%i. a i * b (n-i)) = SUM n (%i. a (n-i) * b i)";
+ "!!a::nat=>'a::ring. \
+\   setsum (%i. a i * b (n-i)) {..n} = \
+\   setsum (%i. a (n-i) * b i) {..n}";
 by (cut_inst_tac [("j", "n"), ("n", "n")] poly_comm_lemma1 1);
 by (Asm_full_simp_tac 1);
 qed "poly_comm_lemma";
@@ -120,7 +125,7 @@
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
+\   setsum (%i. if i = x then f i else 0) {..n} = (if x <= n then f x else 0)";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
@@ -133,8 +138,8 @@
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \
-\    SUM m f = SUM n f";
+\    m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \
+\    setsum f {..m} = setsum f {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
@@ -148,23 +153,24 @@
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM n f) |] ==> \
-\      P (SUM m f)";
+\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \
+\  ==> P (setsum f {..m})";
 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
 by (Asm_full_simp_tac 1);
 qed "SUM_shrink";
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM m f) |] ==> \
-\      P (SUM n f)";
+\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \
+\    ==> P (setsum f {..n})";
 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
 by (Asm_full_simp_tac 1);
 qed "SUM_extend";
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    (ALL i. i < m --> f i = <0>) --> SUM d (%i. f (i+m)) = SUM (m+d) f";
+\    (ALL i. i < m --> f i = 0) --> \
+\      setsum (%i. f (i+m)) {..d} = setsum f {..m+d}";
 by (induct_tac "d" 1);
 (* Base case *)
 by (induct_tac "m" 1);
@@ -176,8 +182,8 @@
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    [| m <= n; !!i. i < m ==> f i = <0>; P (SUM (n-m) (%i. f (i+m))) |] ==> \
-\    P (SUM n f)";
+\    [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
+\    ==> P (setsum f {..n})";
 by (asm_full_simp_tac 
     (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
 qed "SUM_extend_below";
@@ -186,8 +192,8 @@
 
 Goal
   "!!f::nat=>'a::ring. j <= n + m --> \
-\    SUM j (%k. SUM k (%i. f i * g (k - i))) = \
-\    SUM j (%k. SUM (j - k) (%i. f k * g i))";
+\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \
+\    setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}";
 by (induct_tac "j" 1);
 (* Base case *)
 by (Simp_tac 1);
@@ -198,8 +204,8 @@
 
 Goal
   "!!f::nat=>'a::ring. \
-\    SUM (n + m) (%k. SUM k (%i. f i * g (k - i))) = \
-\    SUM (n + m) (%k. SUM (n + m - k) (%i. f k * g i))";
+\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \
+\    setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}";
 by (rtac (DiagSum_lemma RS mp) 1);
 by (rtac le_refl 1);
 qed "DiagSum";
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/NatSum.thy
--- a/src/HOL/Algebra/abstract/NatSum.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/NatSum.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -6,10 +6,7 @@
 
 NatSum = Ring +
 
-consts
-  SUM		:: [nat, nat => 'a] => 'a::ringS
-
-defs
-  SUM_def	"SUM n f == nat_rec <0> (%m sum. f m + sum) (Suc n)"
+instance
+  ring < plus_ac0 (a_assoc, a_comm, l_zero)
 
 end
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/Ring.ML
--- a/src/HOL/Algebra/abstract/Ring.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ring.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -19,12 +19,12 @@
 
 val a_ac = [a_assoc, a_comm, a_lcomm];
 
-Goal "!!a::'a::ring. a + <0> = a";
+Goal "!!a::'a::ring. a + 0 = a";
 by (rtac (a_comm RS trans) 1);
 by (rtac l_zero 1);
 qed "r_zero";
 
-Goal "!!a::'a::ring. a + (-a) = <0>";
+Goal "!!a::'a::ring. a + (-a) = 0";
 by (rtac (a_comm RS trans) 1);
 by (rtac l_neg 1);
 qed "r_neg";
@@ -58,7 +58,7 @@
 by (rtac (l_neg RS sym) 1);
 qed "minus_minus";
 
-Goal "- <0> = (<0>::'a::ring)";
+Goal "- 0 = (0::'a::ring)";
 by (rtac a_lcancel 1);
 by (rtac (r_neg RS trans) 1);
 by (rtac (l_zero RS sym) 1);
@@ -94,13 +94,13 @@
 (* the following two proofs can be found in
    Jacobson, Basic Algebra I, pp. 88-89 *)
 
-Goal "!!a::'a::ring. <0> * a = <0>";
+Goal "!!a::'a::ring. 0 * a = 0";
 by (rtac a_lcancel 1);
 by (rtac (l_distr RS sym RS trans) 1);
 by (simp_tac (simpset() addsimps [r_zero]) 1);
 qed "l_null";
 
-Goal "!!a::'a::ring. a * <0> = <0>";
+Goal "!!a::'a::ring. a * 0 = 0";
 by (rtac (m_comm RS trans) 1);
 by (rtac l_null 1);
 qed "r_null";
@@ -121,50 +121,42 @@
 
 val m_minus = [l_minus, r_minus];
 
-(* one and zero are distinct *)
-
-Goal "<0> ~= (<1>::'a::ring)";
-by (rtac not_sym 1);
-by (rtac one_not_zero 1);
-qed "zero_not_one";
-
 Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, 
-	  l_one, r_one, l_null, r_null,
-	  one_not_zero, zero_not_one];
+	  l_one, r_one, l_null, r_null];
 
 (* further rules *)
 
-Goal "!!a::'a::ring. -a = <0> ==> a = <0>";
+Goal "!!a::'a::ring. -a = 0 ==> a = 0";
 by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1);
 by (Asm_simp_tac 1);
 qed "uminus_monom";
 
-Goal "!!a::'a::ring. a ~= <0> ==> -a ~= <0>";
+Goal "!!a::'a::ring. a ~= 0 ==> -a ~= 0";
 by (blast_tac (claset() addIs [uminus_monom]) 1); 
 qed "uminus_monom_neq";
 
-Goal "!!a::'a::ring. a * b ~= <0> ==> a ~= <0>";
+Goal "!!a::'a::ring. a * b ~= 0 ==> a ~= 0";
 by Auto_tac;  
 qed "l_nullD";
 
-Goal "!!a::'a::ring. a * b ~= <0> ==> b ~= <0>";
+Goal "!!a::'a::ring. a * b ~= 0 ==> b ~= 0";
 by Auto_tac;  
 qed "r_nullD";
 
-(* reflection between a = b and a -- b = <0> *)
+(* reflection between a = b and a -- b = 0 *)
 
-Goal "!!a::'a::ring. a = b ==> a + (-b) = <0>";
+Goal "!!a::'a::ring. a = b ==> a + (-b) = 0";
 by (Asm_simp_tac 1);
 qed "eq_imp_diff_zero";
 
-Goal "!!a::'a::ring. a + (-b) = <0> ==> a = b";
+Goal "!!a::'a::ring. a + (-b) = 0 ==> a = b";
 by (res_inst_tac [("a", "-b")] a_rcancel 1);
 by (Asm_simp_tac 1);
 qed "diff_zero_imp_eq";
 
 (* this could be a rewrite rule, but won't terminate
    ==> make it a simproc?
-Goal "!!a::'a::ring. (a = b) = (a -- b = <0>)";
+Goal "!!a::'a::ring. (a = b) = (a -- b = 0)";
 *)
 
 (* Power *)
@@ -184,7 +176,7 @@
 by Auto_tac;
 qed "power_one";
 
-Goal "!!n. n ~= 0 ==> <0> ^ n = (<0>::'a::ring)";
+Goal "!!n. n ~= 0 ==> 0 ^ n = (0::'a::ring)";
 by (etac rev_mp 1);
 by (induct_tac "n" 1);
 by Auto_tac;
@@ -201,12 +193,12 @@
 (* Divisibility *)
 section "Divisibility";
 
-Goalw [dvd_def] "!! a::'a::ring. a dvd <0>";
-by (res_inst_tac [("x", "<0>")] exI 1);
+Goalw [dvd_def] "!! a::'a::ring. a dvd 0";
+by (res_inst_tac [("x", "0")] exI 1);
 by (Simp_tac 1);
 qed "dvd_zero_right";
 
-Goalw [dvd_def] "!! a::'a::ring. <0> dvd a ==> a = <0>";
+Goalw [dvd_def] "!! a::'a::ring. 0 dvd a ==> a = 0";
 by Auto_tac;
 qed "dvd_zero_left";
 
@@ -223,10 +215,6 @@
 
 Addsimps [dvd_zero_right, dvd_refl_ring];
 
-Goal "!! a::'a::ring. a dvd <1> ==> a ~= <0>";
-by (auto_tac (claset() addDs [dvd_zero_left], simpset()));
-qed "unit_imp_nonzero";
-
 Goalw [dvd_def]
   "!!a::'a::ring. [| a dvd <1>; b dvd <1> |] ==> a * b dvd <1>";
 by (Clarify_tac 1);
@@ -296,23 +284,33 @@
 
 section "Integral domains";
 
-Goal "[| a * b = <0>; a ~= <0> |] ==> (b::'a::domain) = <0>";
+Goal "0 ~= (<1>::'a::domain)";
+by (rtac not_sym 1);
+by (rtac one_not_zero 1);
+qed "zero_not_one";
+
+Goal "!! a::'a::domain. a dvd <1> ==> a ~= 0";
+by (auto_tac (claset() addDs [dvd_zero_left],
+  simpset() addsimps [one_not_zero] ));
+qed "unit_imp_nonzero";
+
+Goal "[| a * b = 0; a ~= 0 |] ==> (b::'a::domain) = 0";
 by (dtac integral 1);
 by (Fast_tac 1);
 qed "r_integral";
 
-Goal "[| a * b = <0>; b ~= <0> |] ==> (a::'a::domain) = <0>";
+Goal "[| a * b = 0; b ~= 0 |] ==> (a::'a::domain) = 0";
 by (dtac integral 1);
 by (Fast_tac 1);
 qed "l_integral";
 
-Goal "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
+Goal "!! a::'a::domain. [| a ~= 0; b ~= 0 |] ==> a * b ~= 0";
 by (blast_tac (claset() addIs [l_integral]) 1); 
 qed "not_integral";
 
-Addsimps [not_integral];
+Addsimps [not_integral, one_not_zero, zero_not_one];
 
-Goal "!! a::'a::domain. [| a * x = x; x ~= <0> |] ==> a = <1>";
+Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = <1>";
 by (res_inst_tac [("a", "- <1>")] a_lcancel 1);
 by (Simp_tac 1);
 by (rtac l_integral 1);
@@ -320,7 +318,7 @@
 by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);
 qed "l_one_integral";
 
-Goal "!! a::'a::domain. [| x * a = x; x ~= <0> |] ==> a = <1>";
+Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = <1>";
 by (res_inst_tac [("a", "- <1>")] a_rcancel 1);
 by (Simp_tac 1);
 by (rtac r_integral 1);
@@ -330,24 +328,24 @@
 
 (* cancellation laws for multiplication *)
 
-Goal "!! a::'a::domain. [| a ~= <0>; a * b = a * c |] ==> b = c";
+Goal "!! a::'a::domain. [| a ~= 0; a * b = a * c |] ==> b = c";
 by (rtac diff_zero_imp_eq 1);
 by (dtac eq_imp_diff_zero 1);
 by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1);
 by (fast_tac (claset() addIs [l_integral]) 1);
 qed "m_lcancel";
 
-Goal "!! a::'a::domain. [| a ~= <0>; b * a = c * a |] ==> b = c";
+Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c";
 by (rtac m_lcancel 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
 qed "m_rcancel";
 
-Goal "!! a::'a::domain. a ~= <0> ==> (a * b = a * c) = (b = c)";
+Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)";
 by (auto_tac (claset() addDs [m_lcancel], simpset()));
 qed "m_lcancel_eq";
 
-Goal "!! a::'a::domain. a ~= <0> ==> (b * a = c * a) = (b = c)";
+Goal "!! a::'a::domain. a ~= 0 ==> (b * a = c * a) = (b = c)";
 by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1);
 qed "m_rcancel_eq";
 
@@ -357,25 +355,26 @@
 
 section "Fields";
 
-Goal "!! a::'a::field. (a dvd <1>) = (a ~= <0>)";
-by (blast_tac (claset() addDs [field_ax, unit_imp_nonzero]) 1);
+Goal "!! a::'a::field. (a dvd <1>) = (a ~= 0)";
+by (auto_tac (claset() addDs [field_ax, dvd_zero_left],
+  simpset() addsimps [field_one_not_zero]));
 qed "field_unit";
 
 Addsimps [field_unit];
 
-Goal "!! a::'a::field. a ~= <0> ==> a * inverse a = <1>";
+Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = <1>";
 by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
 qed "r_inverse";
 
-Goal "!! a::'a::field. a ~= <0> ==> inverse a * a= <1>";
+Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= <1>";
 by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);
 qed "l_inverse";
 
 Addsimps [l_inverse, r_inverse];
 
-(* fields are factorial domains *)
+(* fields are integral domains *)
 
-Goal "!! a::'a::field. a * b = <0> ==> a = <0> | b = <0>";
+Goal "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0";
 by (Step_tac 1);
 by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
 by (rtac refl 3);
@@ -383,6 +382,8 @@
 by Auto_tac;
 qed "field_integral";
 
+(* fields are factorial domains *)
+
 Goalw [prime_def, irred_def] "!! a::'a::field. irred a ==> prime a";
 by (blast_tac (claset() addIs [field_ax]) 1);
 qed "field_fact_prime";
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/Ring.thy
--- a/src/HOL/Algebra/abstract/Ring.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ring.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -9,16 +9,15 @@
 (* Syntactic class ring *)
 
 axclass
-  ringS < plus, minus, times, power, inverse
+  ringS < zero, plus, minus, times, power, inverse
 
 consts
   (* Basic rings *)
-  "<0>"		:: 'a::ringS				("<0>")
   "<1>"		:: 'a::ringS				("<1>")
   "--"		:: ['a, 'a] => 'a::ringS		(infixl 65)
 
   (* Divisibility *)
-  assoc		:: ['a::times, 'a] => bool		(infixl 70)
+  assoc		:: ['a::times, 'a] => bool		(infixl 50)
   irred		:: 'a::ringS => bool
   prime		:: 'a::ringS => bool
 
@@ -31,8 +30,8 @@
   ring < ringS
 
   a_assoc	"(a + b) + c = a + (b + c)"
-  l_zero	"<0> + a = a"
-  l_neg		"(-a) + a = <0>"
+  l_zero	"0 + a = a"
+  l_neg		"(-a) + a = 0"
   a_comm	"a + b = b + a"
 
   m_assoc	"(a * b) * c = a * (b * c)"
@@ -42,18 +41,17 @@
 
   m_comm	"a * b = b * a"
 
-  one_not_zero	"<1> ~= <0>"
-  		(* if <1> = <0>, then the ring has only one element! *)
+  (* Definition of derived operations *)
 
-  inverse_ax    "inverse a = (if a dvd <1> then @x. a*x = <1> else <0>)"
+  inverse_ax    "inverse a = (if a dvd <1> then @x. a*x = <1> else 0)"
   divide_ax     "a / b = a * inverse b"
   power_ax	"a ^ n = nat_rec <1> (%u b. b * a) n"
 
 defs
   assoc_def	"a assoc b == a dvd b & b dvd a"
-  irred_def	"irred a == a ~= <0> & ~ a dvd <1>
+  irred_def	"irred a == a ~= 0 & ~ a dvd <1>
                           & (ALL d. d dvd a --> d dvd <1> | a dvd d)"
-  prime_def	"prime p == p ~= <0> & ~ p dvd <1>
+  prime_def	"prime p == p ~= 0 & ~ p dvd <1>
                           & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
 
 (* Integral domains *)
@@ -61,7 +59,8 @@
 axclass
   domain < ring
 
-  integral	"a * b = <0> ==> a = <0> | b = <0>"
+  one_not_zero	"<1> ~= 0"
+  integral	"a * b = 0 ==> a = 0 | b = 0"
 
 (* Factorial domains *)
 
@@ -81,7 +80,7 @@
 axclass
   euclidean < domain
 
-  euclidean_ax	"b ~= <0> ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
+  euclidean_ax	"b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
                    a = b * q + r & e_size r < e_size b)"
 
   Nothing has been proved about euclidean domains, yet.
@@ -101,6 +100,9 @@
 axclass
   field < ring
 
-  field_ax	"a ~= <0> ==> a dvd <1>"
+  field_one_not_zero	"<1> ~= 0"
+		(* Avoid a common superclass as the first thing we will
+		   prove about fields is that they are domains. *)
+  field_ax	"a ~= 0 ==> a dvd <1>"
 
 end
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/abstract/RingHomo.ML
--- a/src/HOL/Algebra/abstract/RingHomo.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/RingHomo.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -24,8 +24,8 @@
 by (Fast_tac 1);
 qed "homo_one";
 
-Goal "!! f::('a::ring=>'b::ring). homo f ==> f <0> = <0>";
-by (res_inst_tac [("a", "f <0>")] a_lcancel 1);
+Goal "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0";
+by (res_inst_tac [("a", "f 0")] a_lcancel 1);
 by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1);
 qed "homo_zero";
 
@@ -45,11 +45,12 @@
 qed "homo_power";
 
 Goal
-  "!! f::('a::ring=>'b::ring). homo f ==> f (SUM n g) = SUM n (f o g)";
+  "!! f::('a::ring=>'b::ring). \
+\  homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}";
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1);
 by (Simp_tac 1);
-by (dres_inst_tac [("a", "g (Suc n)"), ("b", "SUM n g")] homo_add 1);
+by (dres_inst_tac [("a", "g (Suc n)"), ("b", "setsum g {..n}")] homo_add 1);
 by (Asm_simp_tac 1);
 qed "homo_SUM";
 
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/Degree.ML
--- a/src/HOL/Algebra/poly/Degree.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/Degree.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -6,7 +6,7 @@
 
 (* Relating degree and bound *)
 
-Goal "[| bound m f; f n ~= <0> |] ==> n <= m";
+Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
 by (force_tac (claset() addDs [inst "m" "n" boundD], 
                simpset()) 1); 
 qed "below_bound";
@@ -20,13 +20,13 @@
 qed "Least_is_bound";
 
 Goalw [coeff_def, deg_def]
-  "!! p. ALL m. n < m --> coeff m p = <0> ==> deg p <= n";
+  "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
 by (rtac Least_le 1);
 by (Fast_tac 1);
 qed "deg_aboveI";
 
 Goalw [coeff_def, deg_def]
-  "(n ~= 0 --> coeff n p ~= <0>) ==> n <= deg p";
+  "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
 by (case_tac "n = 0" 1);
 (* Case n=0 *)
 by (Asm_simp_tac 1);
@@ -39,7 +39,7 @@
 qed "deg_belowI";
 
 Goalw [coeff_def, deg_def]
-  "deg p < m ==> coeff m p = <0>";
+  "deg p < m ==> coeff m p = 0";
 by (rtac exE 1); (* create !! x. *)
 by (rtac boundD 2);
 by (assume_tac 3);
@@ -56,7 +56,7 @@
 val lemma1 = result();
 
 Goalw [deg_def, coeff_def]
-  "deg p = Suc y ==> coeff (deg p) p ~= <0>";
+  "deg p = Suc y ==> coeff (deg p) p ~= 0";
 by (rtac ccontr 1);
 by (dtac notnotD 1);
 by (cut_inst_tac [("p", "p")] Least_is_bound 1);
@@ -81,7 +81,7 @@
 by (assume_tac 1);
 val lemma2 = result();
 
-Goal "deg p ~= 0 ==> coeff (deg p) p ~= <0>";
+Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
 by (rtac lemma2 1);
 by (Full_simp_tac 1);
 by (dtac Suc_pred 1);
@@ -89,7 +89,7 @@
 by (Asm_simp_tac 1);
 qed "deg_lcoeff";
 
-Goal "p ~= <0> ==> coeff (deg p) p ~= <0>";
+Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
 by (etac contrapos_np 1); 
 by (case_tac "deg p = 0" 1);
 by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
@@ -144,11 +144,15 @@
 by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
 qed "deg_add_equal";
 
-Goal "deg (monom m::'a::ring up) = m";
+Goal "deg (monom m::'a::ring up) <= m";
+by (asm_simp_tac 
+  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
+qed "deg_monom_ring";
+
+Goal "deg (monom m::'a::domain up) = m";
 by (rtac le_anti_sym 1);
 (* <= *)
-by (asm_simp_tac 
-  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
+br deg_monom_ring 1;
 (* >= *)
 by (asm_simp_tac 
   (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
@@ -162,7 +166,7 @@
 by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
 qed "deg_const";
 
-Goal "deg (<0>::'a::ringS up) = 0";
+Goal "deg (0::'a::ringS up) = 0";
 by (rtac le_anti_sym 1);
 by (rtac deg_aboveI 1);
 by (Simp_tac 1);
@@ -188,22 +192,22 @@
 Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
 
 Goal
-  "!! a::'a::ring. deg (a *s p) <= (if a = <0> then 0 else deg p)";
-by (case_tac "a = <0>" 1);
+  "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
+by (case_tac "a = 0" 1);
 by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
 qed "deg_smult_ring";
 
 Goal
-  "!! a::'a::domain. deg (a *s p) = (if a = <0> then 0 else deg p)";
+  "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
 by (rtac le_anti_sym 1);
 by (rtac deg_smult_ring 1);
-by (case_tac "a = <0>" 1);
+by (case_tac "a = 0" 1);
 by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
 qed "deg_smult";
 
 Goal
   "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
-\       coeff i p * coeff (k - i) q = <0>";
+\       coeff i p * coeff (k - i) q = 0";
 by (simp_tac (simpset() addsimps [coeff_def]) 1);
 by (rtac bound_mult_zero 1);
 by (assume_tac 3);
@@ -222,7 +226,7 @@
 by (arith_tac 1);
 qed "less_add_diff";
 
-Goal "!!p. coeff n p ~= <0> ==> n <= deg p";
+Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
 (* More general than deg_belowI, and simplifies the next proof! *)
 by (rtac deg_belowI 1);
 by (Fast_tac 1);
@@ -230,7 +234,7 @@
 
 Goal
   "!! p::'a::domain up. \
-\    [| p ~= <0>; q ~= <0> |] ==> deg (p * q) = deg p + deg q";
+\    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
 by (rtac le_anti_sym 1);
 by (rtac deg_mult_ring 1);
 (* deg p + deg q <= deg (p * q) *)
@@ -264,14 +268,15 @@
 (* Representation theorems about polynomials *)
 
 goal PolyRing.thy
-  "!! p::nat=>'a::ring up. coeff k (SUM n p) = SUM n (%i. coeff k (p i))";
+  "!! p::nat=>'a::ring up. \
+\    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "coeff_SUM";
 
 goal UnivPoly.thy
   "!! f::(nat=>'a::ring). \
-\    bound n f ==> SUM n (%i. if i = x then f i else <0>) = f x";
+\    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
 by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
 by (auto_tac
     (claset() addDs [not_leE],
@@ -279,7 +284,8 @@
 qed "bound_SUM_if";
 
 Goal
-  "!! p::'a::ring up. deg p <= n ==> SUM n (%i. coeff i p *s monom i) = p";
+  "!! p::'a::ring up. deg p <= n ==> \
+\  setsum (%i. coeff i p *s monom i) {..n} = p";
 by (rtac up_eqI 1);
 by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
 by (rtac trans 1);
@@ -292,12 +298,13 @@
 
 Goal
   "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
-\  P (SUM n (%i. coeff i p *s monom i))";
+\  P (setsum (%i. coeff i p *s monom i) {..n})";
 by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
 qed "up_reprD";
 
 Goal
-  "!! p::'a::ring up. [| deg p <= n; P (SUM n (%i. coeff i p *s monom i)) |] \
+  "!! p::'a::ring up. \
+\  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
 \    ==> P p";
 by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
 qed "up_repr2D";
@@ -313,24 +320,24 @@
 
 (* Polynomials over integral domains are again integral domains *)
 
-Goal "!!p::'a::domain up. p * q = <0> ==> p = <0> | q = <0>";
+Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
 by (rtac classical 1);
 by (subgoal_tac "deg p = 0 & deg q = 0" 1);
 by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
 by (Asm_simp_tac 1);
 by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
 by (Asm_simp_tac 1);
-by (subgoal_tac "coeff 0 p = <0> | coeff 0 q = <0>" 1);
+by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
 by (force_tac (claset() addIs [up_eqI], simpset()) 1);
 by (rtac integral 1);
-by (subgoal_tac "coeff 0 (p * q) = <0>" 1);
+by (subgoal_tac "coeff 0 (p * q) = 0" 1);
 by (Asm_simp_tac 2);
 by (Full_simp_tac 1);
 by (dres_inst_tac [("f", "deg")] arg_cong 1);
 by (Asm_full_simp_tac 1);
 qed "up_integral";
 
-Goal "!! a::'a::domain. a *s p = <0> ==> a = <0> | p = <0>";
+Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
 by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
 by (dtac up_integral 1);
 by Auto_tac;
@@ -341,10 +348,10 @@
 (* Divisibility and degree *)
 
 Goalw [dvd_def]
-  "!! p::'a::domain up. [| p dvd q; q ~= <0> |] ==> deg p <= deg q";
+  "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
 by (etac exE 1);
 by (hyp_subst_tac 1);
-by (case_tac "p = <0>" 1);
+by (case_tac "p = 0" 1);
 by (Asm_simp_tac 1);
 by (dtac r_nullD 1);
 by (asm_simp_tac (simpset() addsimps [le_add1]) 1);
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/LongDiv.ML
--- a/src/HOL/Algebra/poly/LongDiv.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -39,7 +39,7 @@
 qed "deg_lcoeff_cancel2";
 
 Goal
-  "!!g::('a::ring up). g ~= <0> ==> \
+  "!!g::('a::ring up). g ~= 0 ==> \
 \    Ex (% (q, r, k). \
 \      (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))";
 by (res_inst_tac [("P", "%f. Ex (% (q, r, k). \
@@ -48,16 +48,16 @@
 (* TO DO: replace by measure_induct *)
 by (res_inst_tac [("f", "eucl_size")] wf_measure 1);
 by (case_tac "eucl_size x < eucl_size g" 1);
-by (res_inst_tac [("x", "(<0>, x, 0)")] exI 1);
+by (res_inst_tac [("x", "(0, x, 0)")] exI 1);
 by (Asm_simp_tac 1);
 (* case "eucl_size x >= eucl_size g" *)
 by (dres_inst_tac [("x", "lcoeff g *s x -- (lcoeff x *s monom (deg x - deg g)) * g")] spec 1);
 by (etac impE 1);
 by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1);
-by (case_tac "x = <0>" 1);
+by (case_tac "x = 0" 1);
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
-(* case "x ~= <0> *)
+(* case "x ~= 0 *)
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
 by (Simp_tac 1);
@@ -73,7 +73,10 @@
   by (rtac le_trans 1);
   by (rtac add_le_mono1 1);
   by (rtac deg_smult_ring 1);
-  by (asm_simp_tac (simpset() addsimps [leI]) 1);
+(*  by (asm_simp_tac (simpset() addsimps [leI]) 1); *)
+  by (Asm_simp_tac 1);
+  by (cut_inst_tac [("m", "deg x - deg g"), ("'a", "'a")] deg_monom_ring 1);
+  by (arith_tac 1);
 by (Force_tac 1);
 by (Simp_tac 1);
 by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
@@ -97,22 +100,22 @@
 qed "long_div_eucl_size";
 
 Goal
-  "!!g::('a::ring up). g ~= <0> ==> \
+  "!!g::('a::ring up). g ~= 0 ==> \
 \    Ex (% (q, r, k). \
-\      (lcoeff g)^k *s f = q * g + r & (r = <0> | deg r < deg g))";
+\      (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))";
 by (forw_inst_tac [("f", "f")]
   (simplify (simpset() addsimps [eucl_size_def]) long_div_eucl_size) 1);
 by Auto_tac;
-by (case_tac "aa = <0>" 1);
+by (case_tac "aa = 0" 1);
 by (Blast_tac 1);
-(* case "aa ~= <0> *)
+(* case "aa ~= 0 *)
 by (rotate_tac ~1 1);
 by Auto_tac;
 qed "long_div_ring";
 
 Goal
-  "!!g::('a::ring up). [| g ~= <0>; (lcoeff g) dvd <1> |] ==> \
-\    Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
+  "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd <1> |] ==> \
+\    Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
 by (forw_inst_tac [("f", "f")] long_div_ring 1);
 by (etac exE 1);
 by (res_inst_tac [("x", "((%(q,r,k). (inverse(lcoeff g ^k) *s q)) x, \
@@ -133,36 +136,36 @@
 qed "long_div_unit";
 
 Goal
-  "!!g::('a::field up). g ~= <0> ==> \
-\    Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
+  "!!g::('a::field up). g ~= 0 ==> \
+\    Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
 by (rtac long_div_unit 1);
 by (assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [lcoeff_def, nonzero_lcoeff, field_ax]) 1);
 qed "long_div_theorem";
 
 Goal
-  "!!g::('a::field up). [| g ~= <0>; \
-\    f = q1 * g + r1; (r1 = <0> | deg r1 < deg g); \
-\    f = q2 * g + r2; (r2 = <0> | deg r2 < deg g) |] ==> q1 = q2";
+  "!!g::('a::field up). [| g ~= 0; \
+\    f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \
+\    f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2";
 by (subgoal_tac "(q1 -- q2) * g = r2 -- r1" 1); (* 1 *)
 by (thin_tac "f = ?x" 1);
 by (thin_tac "f = ?x" 1);
 by (rtac diff_zero_imp_eq 1);
 by (rtac classical 1);
 by (etac disjE 1);
-(* r1 = <0> *)
+(* r1 = 0 *)
 by (etac disjE 1);
-(* r2 = <0> *)
+(* r2 = 0 *)
 by (force_tac (claset() addDs [integral], simpset()) 1);
-(* r2 ~= <0> *)
+(* r2 ~= 0 *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
 by (Force_tac 1);
-(* r1 ~=<0> *)
+(* r1 ~=0 *)
 by (etac disjE 1);
-(* r2 = <0> *)
+(* r2 = 0 *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
 by (Force_tac 1);
-(* r2 ~= <0> *)
+(* r2 ~= 0 *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
 by (Asm_full_simp_tac 1);
 by (dtac (order_eq_refl RS add_leD2) 1);
@@ -177,9 +180,9 @@
 qed "long_div_quo_unique";
 
 Goal
-  "!!g::('a::field up). [| g ~= <0>; \
-\    f = q1 * g + r1; (r1 = <0> | deg r1 < deg g); \
-\    f = q2 * g + r2; (r2 = <0> | deg r2 < deg g) |] ==> r1 = r2";
+  "!!g::('a::field up). [| g ~= 0; \
+\    f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \
+\    f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2";
 by (subgoal_tac "q1 = q2" 1);
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [a_lcancel_eq]) 1);
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -12,7 +12,7 @@
 
 defs
   lcoeff_def	"lcoeff p == coeff (deg p) p"
-  eucl_size_def "eucl_size p == if p = <0> then 0 else deg p+1"
+  eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1"
 
 end
 
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/PolyHomo.ML
--- a/src/HOL/Algebra/poly/PolyHomo.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -55,10 +55,11 @@
 by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
 (* getting a^i and a^(k-i) together is difficult, so we do is manually *)
 by (res_inst_tac [("s", 
-"        SUM (deg aa + deg b) \
-\           (%k. SUM k \
+"        setsum  \
+\           (%k. setsum \
 \                 (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \
-\                      (a ^ i * a ^ (k - i)))))")] trans 1);
+\                      (a ^ i * a ^ (k - i)))) {..k}) \
+\           {..deg aa + deg b}")] trans 1);
 by (asm_simp_tac (simpset()
     addsimps [power_mult, leD RS add_diff_inverse, SUM_ldistr]) 1);
 by (simp_tac (simpset() addsimps m_ac) 1);
@@ -72,14 +73,14 @@
 by (Simp_tac 1);
 qed "EVAL2_const";
 
-(* This is probably redundant *)
 Goalw [EVAL2_def]
-  "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a";
+  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a";
+(* Must be able to distinguish 0 from <1>, hence 'a::domain *)
 by (Asm_simp_tac 1);
 qed "EVAL2_monom1";
 
 Goalw [EVAL2_def]
-  "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
+  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
 by (Simp_tac 1);
 by (case_tac "n" 1); 
 by Auto_tac;
@@ -100,7 +101,7 @@
 by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
 qed "EVAL_const";
 
-Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom n) = a ^ n";
+Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom n) = a ^ n";
 by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
 qed "EVAL_monom";
 
@@ -111,13 +112,13 @@
 (* Examples *)
 
 Goal
-  "EVAL (x::'a::ring) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
+  "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
 by (asm_simp_tac (simpset() delsimps [power_Suc]
     addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
 result();
 
 Goal
-  "EVAL (y::'a::ring) \
+  "EVAL (y::'a::domain) \
 \    (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
 \  x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
 by (asm_simp_tac (simpset() delsimps [power_Suc]
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -9,14 +9,15 @@
 (* Instantiate result from Degree.ML *)
 
 instance
-  up :: (domain) domain (up_integral)
+  up :: (domain) domain (up_one_not_zero, up_integral)
 
 consts
   EVAL2	:: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
   EVAL	:: 'a::ringS => 'a up => 'a
 
 defs
-  EVAL2_def	"EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)"
+  EVAL2_def	"EVAL2 phi a p ==
+                 setsum (%i. phi (coeff i p) * a ^ i) {..deg p}"
   EVAL_def	"EVAL == EVAL2 (%x. x)"
 
 end
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/PolyRing.ML
--- a/src/HOL/Algebra/poly/PolyRing.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/PolyRing.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -37,13 +37,13 @@
 (* the following can be derived from the above ones,
    for generality reasons, it is therefore done *)
 
-Goal "(<0>::'a::ring) *s p = <0>";
+Goal "(0::'a::ring) *s p = 0";
 by (rtac a_lcancel 1);
 by (rtac (smult_l_distr RS sym RS trans) 1);
 by (Simp_tac 1);
 qed "smult_l_null";
 
-Goal "!!a::'a::ring. a *s <0> = <0>";
+Goal "!!a::'a::ring. a *s 0 = 0";
 by (rtac a_lcancel 1);
 by (rtac (smult_r_distr RS sym RS trans) 1);
 by (Simp_tac 1);
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/PolyRing.thy
--- a/src/HOL/Algebra/poly/PolyRing.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/PolyRing.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -9,7 +9,7 @@
 instance
   up :: (ring) ring
   (up_a_assoc, up_l_zero, up_l_neg, up_a_comm, 
-   up_m_assoc, up_l_one, up_l_distr, up_m_comm, up_one_not_zero,
+   up_m_assoc, up_l_one, up_l_distr, up_m_comm,
    up_inverse_def, up_divide_def, up_power_def) {| ALLGOALS (rtac refl) |}
 
 end
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/ProtoPoly.ML
--- a/src/HOL/Algebra/poly/ProtoPoly.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/ProtoPoly.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -7,12 +7,12 @@
 (* Rules for bound *)
 
 val prem = goalw ProtoPoly.thy [bound_def]
-  "[| !! m. n < m ==> f m = <0> |] ==> bound n f";
+  "[| !! m. n < m ==> f m = 0 |] ==> bound n f";
 by (fast_tac (claset() addIs prem) 1);
 qed "boundI";
 
 Goalw [bound_def]
-  "!! f. [| bound n f; n < m |] ==> f m = <0>";
+  "!! f. [| bound n f; n < m |] ==> f m = 0";
 by (Fast_tac 1);
 qed "boundD";
 
@@ -25,6 +25,6 @@
 AddSIs [boundI];
 AddDs [boundD];
 
-Goal "(%x. <0>) : {f. EX n. bound n f}";
+Goal "(%x. 0) : {f. EX n. bound n f}";
 by (Blast_tac 1);
 qed "UP_witness";
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/ProtoPoly.thy
--- a/src/HOL/Algebra/poly/ProtoPoly.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/ProtoPoly.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -10,6 +10,6 @@
   bound :: [nat, nat => 'a::ringS] => bool
 
 defs
-  bound_def  "bound n f == ALL i. n<i --> f i = <0>"
+  bound_def  "bound n f == ALL i. n<i --> f i = 0"
 
 end
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/UnivPoly.ML
--- a/src/HOL/Algebra/poly/UnivPoly.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -29,17 +29,17 @@
 qed "UP_closed_smult";
 
 Goalw [UP_def]
-  "(%n. if m = n then <1> else <0>) : UP";
+  "(%n. if m = n then <1> else 0) : UP";
 by Auto_tac;
 qed "UP_closed_monom";
 
-Goalw [UP_def] "(%n. if n = 0 then a else <0>) : UP";
+Goalw [UP_def] "(%n. if n = 0 then a else 0) : UP";
 by Auto_tac;
 qed "UP_closed_const";
 
 Goal
   "!! f::nat=>'a::ring. \
-\    [| bound n f; bound m g; n + m < k |] ==> f i * g (k - i) = <0>";
+\    [| bound n f; bound m g; n + m < k |] ==> f i * g (k - i) = 0";
 (* Case split: either f i or g (k - i) is zero *)
 by (case_tac "n<i" 1);
 (* First case, f i is zero *)
@@ -52,7 +52,7 @@
 
 Goalw [UP_def]
   "[| f : UP; g : UP |] ==> \
-\      (%n. (SUM n (%i. f i * g (n-i))::'a::ring)) : UP";
+\      (%n. (setsum (%i. f i * g (n-i)) {..n}::'a::ring)) : UP";
 by (Step_tac 1);
 (* Instantiate bound for the product, and remove bound in goal *)
 by (res_inst_tac [("x", "n + na")] exI 1);
@@ -61,9 +61,9 @@
 by (asm_simp_tac (simpset() addsimps [bound_mult_zero]) 1);
 qed "UP_closed_mult";
 
-(* %x. <0> represents a polynomial *)
+(* %x. 0 represents a polynomial *)
 
-Goalw [UP_def] "(%x. <0>) : UP";
+Goalw [UP_def] "(%x. 0) : UP";
 by (Fast_tac 1);
 qed "UP_zero";
 
@@ -80,21 +80,21 @@
 qed "coeff_smult";
 
 Goalw [coeff_def, monom_def]
-  "coeff n (monom m) = (if m=n then <1> else <0>)";
+  "coeff n (monom m) = (if m=n then <1> else 0)";
 by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_monom, Rep_UP]) 1);
 qed "coeff_monom";
 
 Goalw [coeff_def, const_def]
-  "coeff n (const a) = (if n=0 then a else <0>)";
+  "coeff n (const a) = (if n=0 then a else 0)";
 by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const, Rep_UP]) 1);
 qed "coeff_const";
 
 Goalw [coeff_def, up_mult_def]
-  "coeff n (p * q) = (SUM n (%i. coeff i p * coeff (n-i) q)::'a::ring)";
+  "coeff n (p * q) = (setsum (%i. coeff i p * coeff (n-i) q) {..n}::'a::ring)";
 by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_mult, Rep_UP]) 1);
 qed "coeff_mult";
 
-Goalw [coeff_def, up_zero_def] "coeff n <0> = <0>";
+Goalw [coeff_def, up_zero_def] "coeff n 0 = 0";
 by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_zero, Rep_UP]) 1);
 qed "coeff_zero";
 
@@ -102,7 +102,7 @@
 	  coeff_mult, coeff_zero];
 
 Goalw [up_one_def]
-  "coeff n <1> = (if n=0 then <1> else <0>)";
+  "coeff n <1> = (if n=0 then <1> else 0)";
 by (Simp_tac 1);
 qed "coeff_one";
 
@@ -132,12 +132,12 @@
 by (rtac a_assoc 1);
 qed "up_a_assoc";
 
-Goal "!! a::('a::ring) up. <0> + a = a";
+Goal "!! a::('a::ring) up. 0 + a = a";
 by (rtac up_eqI 1);
 by (Simp_tac 1);
 qed "up_l_zero";
 
-Goal "!! a::('a::ring) up. (-a) + a = <0>";
+Goal "!! a::('a::ring) up. (-a) + a = 0";
 by (rtac up_eqI 1);
 by (Simp_tac 1);
 qed "up_l_neg";
@@ -176,11 +176,6 @@
 by (asm_full_simp_tac (simpset() addsimps [m_comm]) 1);
 qed "up_m_comm";
 
-Goal "<1> ~= (<0>::('a::ring) up)";
-by (res_inst_tac [("n", "0")] up_neqI 1);
-by (Simp_tac 1);
-qed "up_one_not_zero";
-
 (* Further algebraic rules *)
 
 Goal "!! a::'a::ring. const a * p = a *s p";
@@ -206,7 +201,7 @@
 by (Simp_tac 1);
 qed "const_one";
 
-Goal "const (<0>::'a::ring) = <0>";
+Goal "const (0::'a::ring) = 0";
 by (rtac up_eqI 1);
 by (Simp_tac 1);
 qed "const_zero";
@@ -226,7 +221,8 @@
 (*Lemma used in PolyHomo*)
 Goal
   "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \
-\    SUM (n + m) (%k. SUM k (%i. f i * g (k-i))) = SUM n f * SUM m g";
+\    setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \
+\    setsum f {..n} * setsum g {..m}";
 by (simp_tac (simpset() addsimps [SUM_ldistr, DiagSum]) 1);
 (* SUM_rdistr must be applied after SUM_ldistr ! *)
 by (simp_tac (simpset() addsimps [SUM_rdistr]) 1);
@@ -239,3 +235,8 @@
 by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
 by Auto_tac;
 qed "CauchySum";
+
+Goal "<1> ~= (0::('a::domain) up)";
+by (res_inst_tac [("n", "0")] up_neqI 1);
+by (Simp_tac 1);
+qed "up_one_not_zero";
diff -r 69c1abb9a129 -r 62c2e0af1d30 src/HOL/Algebra/poly/UnivPoly.thy
--- a/src/HOL/Algebra/poly/UnivPoly.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -28,15 +28,15 @@
   coeff_def	"coeff n p == Rep_UP p n"
   up_add_def	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
   up_smult_def	"a *s p == Abs_UP (%n. a * Rep_UP p n)"
-  monom_def	"monom m == Abs_UP (%n. if m=n then <1> else <0>)"
-  const_def	"const a == Abs_UP (%n. if n=0 then a else <0>)"
-  up_mult_def	"p * q == Abs_UP (%n. SUM n
-		     (%i. Rep_UP p i * Rep_UP q (n-i)))"
+  monom_def	"monom m == Abs_UP (%n. if m=n then <1> else 0)"
+  const_def	"const a == Abs_UP (%n. if n=0 then a else 0)"
+  up_mult_def	"p * q == Abs_UP (%n::nat. setsum
+		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
 
-  up_zero_def	"<0> == Abs_UP (%x. <0>)"
+  up_zero_def	"0 == Abs_UP (%x. 0)"
   up_one_def	"<1> == monom 0"
   up_uminus_def	"- p == (-<1>) *s p"
-  up_inverse_def "inverse (a::'a::ringS up) == (if a dvd <1> then @x. a*x = <1> else <0>)"
+  up_inverse_def "inverse (a::'a::ringS up) == (if a dvd <1> then @x. a*x = <1> else 0)"
   up_divide_def "(a::'a::ringS up) / b == a * inverse b"
   up_power_def	"a ^ n == nat_rec (<1>::('a::ringS) up) (%u b. b * a) n"
 end