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.
--- 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)
--- 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);
--- 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})"
--- 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";
--- 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
--- 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";
--- 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
--- 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";
--- 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);
--- 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);
--- 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
--- 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]
--- 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
--- 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);
--- 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
--- 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";
--- 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
--- 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";
--- 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