HOL-Algebra partially ported to Isar.
--- a/NEWS Wed Nov 27 17:25:41 2002 +0100
+++ b/NEWS Thu Nov 28 10:50:42 2002 +0100
@@ -6,6 +6,9 @@
*** General ***
+* Provers/linorder: New generic prover for transitivity reasoning over
+linear orders. Note: this prover is not efficient!
+
* Provers/simplifier:
- Completely reimplemented Asm_full_simp_tac:
@@ -87,6 +90,10 @@
*** HOL ***
+* New tactic "trans_tac" and method "trans" instantiate
+Provers/linorder.ML for axclasses "order" and "linorder" (predicates
+"<=", "<" and "=").
+
* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main
HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
--- a/src/HOL/Algebra/abstract/Factor.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/Factor.ML Thu Nov 28 10:50:42 2002 +0100
@@ -4,29 +4,29 @@
Author: Clemens Ballarin, started 25 November 1997
*)
-goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
+Goalw [thm "assoc_def"] "!! c::'a::factorial. \
\ [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b";
-by (ftac factorial_prime 1);
-by (rewrite_goals_tac [irred_def, prime_def]);
+by (ftac (thm "factorial_prime") 1);
+by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]);
by (Blast_tac 1);
qed "irred_dvd_lemma";
-goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
-\ [| irred c; a dvd <1> |] ==> \
+Goalw [thm "assoc_def"] "!! c::'a::factorial. \
+\ [| irred c; a dvd 1 |] ==> \
\ (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
\ (EX d. c assoc d & d : set factors)";
by (induct_tac "factors" 1);
(* Base case: c dvd a contradicts irred c *)
-by (full_simp_tac (simpset() addsimps [irred_def]) 1);
+by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
(* Induction step *)
-by (ftac factorial_prime 1);
-by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1);
+by (ftac (thm "factorial_prime") 1);
+by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
by (Blast_tac 1);
qed "irred_dvd_list_lemma";
-goal Ring.thy "!! c::'a::factorial. \
-\ [| irred c; ALL b : set factors. irred b; a dvd <1>; \
+Goal "!! c::'a::factorial. \
+\ [| irred c; ALL b : set factors. irred b; a dvd 1; \
\ c dvd foldr op* factors a |] ==> \
\ EX d. c assoc d & d : set factors";
by (rtac (irred_dvd_list_lemma RS mp) 1);
--- a/src/HOL/Algebra/abstract/Factor.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/Factor.thy Thu Nov 28 10:50:42 2002 +0100
@@ -7,12 +7,12 @@
Factor = Ring +
consts
- Factorisation :: ['a::ringS, 'a list, 'a] => bool
+ Factorisation :: ['a::ring, 'a list, 'a] => bool
(* factorisation of x into a list of irred factors and a unit u *)
defs
Factorisation_def "Factorisation x factors u ==
x = foldr op* factors u &
- (ALL a : set factors. irred a) & u dvd <1>"
+ (ALL a : set factors. irred a) & u dvd 1"
end
--- a/src/HOL/Algebra/abstract/Ideal.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/Ideal.ML Thu Nov 28 10:50:42 2002 +0100
@@ -51,7 +51,11 @@
Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}";
by (rtac is_idealI 1);
-by Auto_tac;
+(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *)
+by (Clarify_tac 1);
+by (Clarify_tac 2);
+by (Clarify_tac 3);
+by (Clarify_tac 4);
by (res_inst_tac [("x", "u+ua")] exI 1);
by (res_inst_tac [("x", "v+va")] exI 1);
by (res_inst_tac [("x", "-u")] exI 2);
@@ -60,7 +64,7 @@
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));
+by (REPEAT (Simp_tac 1));
qed "is_ideal_2";
(* ideal_of *)
@@ -73,9 +77,10 @@
by Auto_tac;
qed "generator_in_ideal";
-Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV";
-by (force_tac (claset() addDs [is_ideal_mult], simpset()) 1);
- (* loops if is_ideal_mult is added as non-safe rule *)
+Goalw [ideal_of_def] "ideal_of {1::'a::ring} = UNIV";
+by (force_tac (claset() addDs [is_ideal_mult],
+ simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1);
+ (* FIXME: Zumkeller's order raises Domain exn *)
qed "ideal_of_one_eq";
Goalw [ideal_of_def] "ideal_of {} = {0::'a::ring}";
@@ -101,11 +106,13 @@
by (rtac subsetI 1);
by (dtac InterD 1);
by (assume_tac 2);
-by (auto_tac (claset() addIs [is_ideal_2], simpset()));
-by (res_inst_tac [("x", "<1>")] exI 1);
+by (auto_tac (claset() addIs [is_ideal_2],
+ simpset() delsimprocs [ring_simproc]));
+(* FIXME: Zumkeller's order *)
+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", "<1>")] exI 2);
+by (res_inst_tac [("x", "1")] exI 2);
by (Simp_tac 1);
by (Simp_tac 1);
qed "ideal_of_2_structure";
@@ -204,18 +211,18 @@
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", "<1>")] exI 1);
+by (res_inst_tac [("x", "1")] exI 1);
by (Simp_tac 1);
qed "not_dvd_psubideal";
-Goalw [irred_def]
+Goalw [thm "irred_def"]
"[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I";
by (dtac is_pidealD 1);
by (etac exE 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x", "aa")] allE 1);
by (Clarify_tac 1);
-by (dres_inst_tac [("a", "<1>")] dvd_imp_subideal 1);
+by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1);
by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq]));
qed "irred_imp_max_ideal";
@@ -271,20 +278,21 @@
(* Primeness condition *)
-Goalw [prime_def] "irred a ==> prime (a::'a::pid)";
+Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)";
by (rtac conjI 1);
by (rtac conjI 2);
by (Clarify_tac 3);
-by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "<1>")]
+by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")]
irred_imp_max_ideal 3);
by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax],
- simpset() addsimps [irred_def, not_dvd_psubideal, pid_ax]));
+ simpset() addsimps [thm "irred_def", not_dvd_psubideal, pid_ax]));
by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
by (Clarify_tac 1);
by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
by (full_simp_tac (simpset() addsimps [r_distr]) 1);
-by (etac ssubst 1);
-by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]) 1);
+by (etac subst 1);
+by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]
+ delsimprocs [ring_simproc]) 1);
qed "pid_irred_imp_prime";
(* Fields are Pid *)
@@ -294,7 +302,7 @@
by (Simp_tac 1);
by (rtac subset_trans 1);
by (rtac dvd_imp_subideal 2);
-by (rtac field_ax 2);
+by (rtac (thm "field_ax") 2);
by (assume_tac 2);
by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
qed "field_pideal_univ";
--- a/src/HOL/Algebra/abstract/Ideal.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/Ideal.thy Thu Nov 28 10:50:42 2002 +0100
@@ -7,9 +7,9 @@
Ideal = Ring +
consts
- ideal_of :: ('a::ringS) set => 'a set
- is_ideal :: ('a::ringS) set => bool
- is_pideal :: ('a::ringS) set => bool
+ ideal_of :: ('a::ring) set => 'a set
+ is_ideal :: ('a::ring) set => bool
+ is_pideal :: ('a::ring) set => bool
defs
is_ideal_def "is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
--- a/src/HOL/Algebra/abstract/NatSum.ML Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,215 +0,0 @@
-(*
- Sums with naturals as index domain
- $Id$
- Author: Clemens Ballarin, started 12 December 1996
-*)
-
-section "Basic Properties";
-
-Goal "setsum f {..0::nat} = (f 0::'a::ring)";
-by (Asm_simp_tac 1);
-qed "SUM_0";
-
-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
- "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);
-(* Induction step *)
-by (asm_full_simp_tac (simpset() addsimps [a_assoc]) 1);
-qed "SUM_Suc2";
-
-(* Congruence rules *)
-
-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));
-Addcongs [SUM_cong];
-
-(* Results needed for the development of polynomials *)
-
-section "Ring Properties";
-
-Goal "setsum (%i. 0) {..n::nat} = (0::'a::ring)";
-by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "SUM_zero";
-
-Addsimps [SUM_zero];
-
-Goal
- "!!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);
-(* Induction step *)
-by (asm_simp_tac (simpset() addsimps a_ac) 1);
-qed "SUM_add";
-
-Goal
- "!!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);
-(* Induction step *)
-by (asm_simp_tac (simpset() addsimps [l_distr]) 1);
-qed "SUM_ldistr";
-
-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);
-(* Induction step *)
-by (asm_simp_tac (simpset() addsimps [r_distr]) 1);
-qed "SUM_rdistr";
-
-section "Results for the Construction of Polynomials";
-
-Goal
- "!!a::nat=>'a::ring. k <= n --> \
-\ 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);
-(* Induction step *)
-by (rtac impI 1);
-by (etac impE 1);
-by (arith_tac 1);
-by (asm_simp_tac
- (simpset() addsimps a_ac@
- [Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1);
-by (asm_simp_tac (simpset() addsimps a_ac@ [SUM_ldistr, m_assoc]) 1);
-qed_spec_mp "poly_assoc_lemma1";
-
-Goal
- "!!a::nat=>'a::ring. \
-\ 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 --> \
-\ 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 *)
-by (Simp_tac 1);
-(* Induction step *)
-by (stac SUM_Suc2 1);
-by (asm_simp_tac (simpset() addsimps [a_comm]) 1);
-qed "poly_comm_lemma1";
-
-Goal
- "!!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";
-
-section "Changing the Range of Summation";
-
-Goal
- "!! f::(nat=>'a::ring). \
-\ 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);
-(* Induction step *)
-by (Asm_simp_tac 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("f", "f")] arg_cong 1);
-by (arith_tac 1);
-qed "SUM_if_singleton";
-
-Goal
- "!! f::(nat=>'a::ring). \
-\ 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);
-(* Induction step *)
-by (case_tac "m <= n" 1);
-by Auto_tac;
-by (subgoal_tac "m = Suc n" 1);
-by (Asm_simp_tac 1);
-by (fast_arith_tac 1);
-val SUM_shrink_lemma = result();
-
-Goal
- "!! f::(nat=>'a::ring). \
-\ [| 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 (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) --> \
-\ setsum (%i. f (i+m)) {..d} = setsum f {..m+d}";
-by (induct_tac "d" 1);
-(* Base case *)
-by (induct_tac "m" 1);
-by (Simp_tac 1);
-by (Force_tac 1);
-(* Induction step *)
-by (asm_simp_tac (simpset() addsimps add_ac) 1);
-val SUM_shrink_below_lemma = result();
-
-Goal
- "!! f::(nat=>'a::ring). \
-\ [| 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";
-
-section "Result for the Univeral Property of Polynomials";
-
-Goal
- "!!f::nat=>'a::ring. j <= n + m --> \
-\ 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);
-(* Induction step *)
-by (simp_tac (simpset() addsimps [Suc_diff_le, SUM_add]) 1);
-by (asm_simp_tac (simpset() addsimps a_ac) 1);
-val DiagSum_lemma = result();
-
-Goal
- "!!f::nat=>'a::ring. \
-\ 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 Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*
- Sums with naturals as index domain
- $Id$
- Author: Clemens Ballarin, started 12 December 1996
-*)
-
-NatSum = Ring +
-
-instance
- ring < plus_ac0 (a_assoc, a_comm, l_zero)
-
-end
--- a/src/HOL/Algebra/abstract/Ring.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/Ring.ML Thu Nov 28 10:50:42 2002 +0100
@@ -4,6 +4,7 @@
Author: Clemens Ballarin, started 9 December 1996
*)
+(*
val a_assoc = thm "plus_ac0.assoc";
val l_zero = thm "plus_ac0.zero";
val a_comm = thm "plus_ac0.commute";
@@ -78,7 +79,7 @@
val m_ac = [m_assoc, m_comm, m_lcomm];
-Goal "!!a::'a::ring. a * <1> = a";
+Goal "!!a::'a::ring. a * 1 = a";
by (rtac (m_comm RS trans) 1);
by (rtac l_one 1);
qed "r_one";
@@ -161,19 +162,21 @@
Goal "!!a::'a::ring. (a = b) = (a -- b = 0)";
*)
+*)
+
(* Power *)
-Goal "!!a::'a::ring. a ^ 0 = <1>";
-by (simp_tac (simpset() addsimps [power_ax]) 1);
+Goal "!!a::'a::ring. a ^ 0 = 1";
+by (simp_tac (simpset() addsimps [power_def]) 1);
qed "power_0";
Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
-by (simp_tac (simpset() addsimps [power_ax]) 1);
+by (simp_tac (simpset() addsimps [power_def]) 1);
qed "power_Suc";
Addsimps [power_0, power_Suc];
-Goal "<1> ^ n = (<1>::'a::ring)";
+Goal "1 ^ n = (1::'a::ring)";
by (induct_tac "n" 1);
by Auto_tac;
qed "power_one";
@@ -189,7 +192,7 @@
Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
by (induct_tac "m" 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps m_ac) 1);
+by (Asm_simp_tac 1);
qed "power_mult";
(* Divisibility *)
@@ -205,26 +208,26 @@
qed "dvd_zero_left";
Goalw [dvd_def] "!! a::'a::ring. a dvd a";
-by (res_inst_tac [("x", "<1>")] exI 1);
+by (res_inst_tac [("x", "1")] exI 1);
by (Simp_tac 1);
qed "dvd_refl_ring";
Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
by (Step_tac 1);
by (res_inst_tac [("x", "k * ka")] exI 1);
-by (simp_tac (simpset() addsimps m_ac) 1);
+by (Asm_simp_tac 1);
qed "dvd_trans_ring";
Addsimps [dvd_zero_right, dvd_refl_ring];
Goalw [dvd_def]
- "!!a::'a::ring. [| a dvd <1>; b dvd <1> |] ==> a * b dvd <1>";
+ "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1";
by (Clarify_tac 1);
by (res_inst_tac [("x", "k * ka")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
+by (Asm_full_simp_tac 1);
qed "unit_mult";
-Goal "!!a::'a::ring. a dvd <1> ==> a^n dvd <1>";
+Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1";
by (induct_tac "n" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);
@@ -248,14 +251,14 @@
"!! a::'a::ring. a dvd b ==> a dvd c*b";
by (Clarify_tac 1);
by (res_inst_tac [("x", "c * k")] exI 1);
-by (simp_tac (simpset() addsimps m_ac) 1);
+by (Simp_tac 1);
qed "dvd_l_mult_right";
Goalw [dvd_def]
"!! a::'a::ring. a dvd b ==> a dvd b*c";
by (Clarify_tac 1);
by (res_inst_tac [("x", "k * c")] exI 1);
-by (simp_tac (simpset() addsimps m_ac) 1);
+by (Simp_tac 1);
qed "dvd_r_mult_right";
Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];
@@ -264,34 +267,37 @@
section "inverse";
-Goal "!! a::'a::ring. [| a * x = <1>; a * y = <1> |] ==> x = y";
+Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y";
by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);
-by (simp_tac (simpset() addsimps m_ac) 1);
+by (Simp_tac 1);
by Auto_tac;
qed "inverse_unique";
-Goal "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
-by (asm_full_simp_tac (simpset () addsimps [inverse_ax, dvd_def]) 1);
+Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1";
+by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def]) 1);
by (Clarify_tac 1);
-by (rtac someI 1);
-by (rtac sym 1);
-by (assume_tac 1);
+by (rtac theI 1);
+by (atac 1);
+by (rtac inverse_unique 1);
+by (atac 1);
+by (atac 1);
qed "r_inverse_ring";
-Goal "!! a::'a::ring. a dvd <1> ==> inverse a * a= <1>";
-by (asm_simp_tac (simpset() addsimps r_inverse_ring::m_ac) 1);
+Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1";
+by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
qed "l_inverse_ring";
(* Integral domain *)
+(*
section "Integral domains";
-Goal "0 ~= (<1>::'a::domain)";
+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";
+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";
@@ -312,16 +318,16 @@
Addsimps [not_integral, one_not_zero, zero_not_one];
-Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = <1>";
-by (res_inst_tac [("a", "- <1>")] a_lcancel 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);
by (assume_tac 2);
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>";
-by (res_inst_tac [("a", "- <1>")] a_rcancel 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);
by (assume_tac 2);
@@ -340,7 +346,7 @@
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);
+by (Asm_full_simp_tac 1);
qed "m_rcancel";
Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)";
@@ -352,23 +358,28 @@
qed "m_rcancel_eq";
Addsimps [m_lcancel_eq, m_rcancel_eq];
+*)
(* Fields *)
section "Fields";
-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]));
+Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)";
+by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left],
+ simpset() addsimps [thm "field_one_not_zero"]));
qed "field_unit";
+(* required for instantiation of field < domain in file Field.thy *)
+
Addsimps [field_unit];
-Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = <1>";
+val field_one_not_zero = thm "field_one_not_zero";
+
+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";
@@ -380,12 +391,13 @@
by (Step_tac 1);
by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
by (rtac refl 3);
-by (simp_tac (simpset() addsimps m_ac) 2);
+by (Simp_tac 2);
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);
+Goalw [thm "prime_def", thm "irred_def"]
+ "!! a::'a::field. irred a ==> prime a";
+by (blast_tac (claset() addIs [thm "field_ax"]) 1);
qed "field_fact_prime";
--- a/src/HOL/Algebra/abstract/Ring.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/Ring.thy Thu Nov 28 10:50:42 2002 +0100
@@ -1,89 +1,86 @@
(*
- Abstract class ring (commutative, with 1)
- $Id$
- Author: Clemens Ballarin, started 9 December 1996
+ Title: The algebraic hierarchy of rings as axiomatic classes
+ Id: $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+ Copyright: Clemens Ballarin
*)
-Ring = Main +
+header {* The algebraic hierarchy of rings as axiomatic classes *}
-(* Syntactic class ring *)
+theory Ring = Main
+files ("order.ML"):
-axclass
- ringS < zero, plus, minus, times, power, inverse
+section {* Constants *}
+
+text {* Most constants are already declared by HOL. *}
consts
- (* Basic rings *)
- "<1>" :: 'a::ringS ("<1>")
- "--" :: ['a, 'a] => 'a::ringS (infixl 65)
+ assoc :: "['a::times, 'a] => bool" (infixl 50)
+ irred :: "'a::{zero, one, times} => bool"
+ prime :: "'a::{zero, one, times} => bool"
+
+section {* Axioms *}
+
+subsection {* Ring axioms *}
+
+axclass ring < zero, one, plus, minus, times, inverse, power
+
+ a_assoc: "(a + b) + c = a + (b + c)"
+ l_zero: "0 + a = a"
+ l_neg: "(-a) + a = 0"
+ a_comm: "a + b = b + a"
+
+ m_assoc: "(a * b) * c = a * (b * c)"
+ l_one: "1 * a = a"
- (* Divisibility *)
- assoc :: ['a::times, 'a] => bool (infixl 50)
- irred :: 'a::ringS => bool
- prime :: 'a::ringS => bool
+ l_distr: "(a + b) * c = a * c + b * c"
+
+ m_comm: "a * b = b * a"
+
+ -- {* Definition of derived operations *}
-translations
- "a -- b" == "a + (-b)"
+ minus_def: "a - b = a + (-b)"
+ inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
+ divide_def: "a / b = a * inverse b"
+ power_def: "a ^ n = nat_rec 1 (%u b. b * a) n"
-(* Class ring and ring axioms *)
+defs
+ assoc_def: "a assoc b == a dvd b & b dvd a"
+ 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
+ & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
+
+subsection {* Integral domains *}
axclass
- ring < ringS, plus_ac0
-
-(*a_assoc "(a + b) + c = a + (b + c)"*)
-(*l_zero "0 + a = a"*)
- l_neg "(-a) + a = 0"
-(*a_comm "a + b = b + a"*)
-
- m_assoc "(a * b) * c = a * (b * c)"
- l_one "<1> * a = a"
-
- l_distr "(a + b) * c = a * c + b * c"
-
- m_comm "a * b = b * a"
+ "domain" < ring
- (* Definition of derived operations *)
-
- 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"
+ one_not_zero: "1 ~= 0"
+ integral: "a * b = 0 ==> a = 0 | b = 0"
-defs
- assoc_def "a assoc b == a dvd b & b dvd a"
- 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>
- & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
-
-(* Integral domains *)
+subsection {* Factorial domains *}
axclass
- domain < ring
-
- one_not_zero "<1> ~= 0"
- integral "a * b = 0 ==> a = 0 | b = 0"
-
-(* Factorial domains *)
-
-axclass
- factorial < domain
+ factorial < "domain"
(*
Proper definition using divisor chain condition currently not supported.
- factorial_divisor "wf {(a, b). a dvd b & ~ (b dvd a)}"
+ factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}"
*)
- factorial_divisor "True"
- factorial_prime "irred a ==> prime a"
+ factorial_divisor: "True"
+ factorial_prime: "irred a ==> prime a"
-(* Euclidean domains *)
+subsection {* Euclidean domains *}
(*
axclass
- euclidean < domain
+ 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.
+ Nothing has been proved about Euclidean domains, yet.
Design question:
Fix quo, rem and e_size as constants that are axiomatised with
euclidean_ax?
@@ -95,14 +92,147 @@
definitions of quo and rem.
*)
-(* Fields *)
+subsection {* Fields *}
axclass
field < ring
- 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>"
+ 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"
+
+section {* Basic facts *}
+
+subsection {* Normaliser for rings *}
+
+use "order.ML"
+
+method_setup ring =
+ {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
+ {* computes distributive normal form in rings *}
+
+
+subsection {* Rings and the summation operator *}
+
+(* Basic facts --- move to HOL!!! *)
+
+lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
+by simp
+
+lemma natsum_Suc [simp]:
+ "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
+by (simp add: atMost_Suc)
+
+lemma natsum_Suc2:
+ "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case Suc thus ?case by (simp add: assoc)
+qed
+
+lemma natsum_cong [cong]:
+ "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
+ setsum f {..j} = setsum g {..k}"
+by (induct j) auto
+
+lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
+by (induct n) simp_all
+
+lemma natsum_add [simp]:
+ "!!f::nat=>'a::plus_ac0.
+ setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
+by (induct n) (simp_all add: plus_ac0)
+
+(* Facts specific to rings *)
+
+instance ring < plus_ac0
+proof
+ fix x y z
+ show "(x::'a::ring) + y = y + x" by (rule a_comm)
+ show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
+ show "0 + (x::'a::ring) = x" by (rule l_zero)
+qed
+
+ML {*
+ local
+ val lhss =
+ [read_cterm (sign_of (the_context ()))
+ ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
+ read_cterm (sign_of (the_context ()))
+ ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
+ read_cterm (sign_of (the_context ()))
+ ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
+ read_cterm (sign_of (the_context ()))
+ ("- ?t::'a::ring", TVar (("'z", 0), []))
+ ];
+ fun proc sg _ t =
+ let val rew = Tactic.prove sg [] []
+ (HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
+ (fn _ => simp_tac ring_ss 1)
+ |> mk_meta_eq;
+ val (t', u) = Logic.dest_equals (Thm.prop_of rew);
+ in if t' aconv u
+ then None
+ else Some rew
+ end;
+ in
+ val ring_simproc = mk_simproc "ring" lhss proc;
+ end;
+*}
+
+ML_setup {* Addsimprocs [ring_simproc] *}
+
+lemma natsum_ldistr:
+ "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
+by (induct n) simp_all
+
+lemma natsum_rdistr:
+ "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
+by (induct n) simp_all
+
+subsection {* Integral Domains *}
+
+declare one_not_zero [simp]
+
+lemma zero_not_one [simp]:
+ "0 ~= (1::'a::domain)"
+by (rule not_sym) simp
+
+lemma integral_iff: (* not by default a simp rule! *)
+ "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
+proof
+ assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
+next
+ assume "a = 0 | b = 0" then show "a * b = 0" by auto
+qed
+
+(*
+lemma "(a::'a::ring) - (a - b) = b" apply simp
+simproc seems to fail on this example
+*)
+
+lemma bug: "(b::'a::ring) - (b - a) = a" by simp
+ (* simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" *)
+
+lemma m_lcancel:
+ assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
+proof
+ assume eq: "a * b = a * c"
+ then have "a * (b - c) = 0" by simp
+ then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
+ with prem have "b - c = 0" by auto
+ then have "b = b - (b - c)" by simp
+ also have "b - (b - c) = c" by (rule bug)
+ finally show "b = c" .
+next
+ assume "b = c" then show "a * b = a * c" by simp
+qed
+
+lemma m_rcancel:
+ "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
+by (simp add: m_lcancel)
end
--- a/src/HOL/Algebra/abstract/RingHomo.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/RingHomo.ML Thu Nov 28 10:50:42 2002 +0100
@@ -8,7 +8,7 @@
Goalw [homo_def]
"!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \
-\ f <1> = <1> |] ==> homo f";
+\ f 1 = 1 |] ==> homo f";
by Auto_tac;
qed "homoI";
@@ -20,7 +20,7 @@
by (Fast_tac 1);
qed "homo_mult";
-Goalw [homo_def] "!! f. homo f ==> f <1> = <1>";
+Goalw [homo_def] "!! f. homo f ==> f 1 = 1";
by (Fast_tac 1);
qed "homo_one";
@@ -41,7 +41,7 @@
by (dtac homo_one 1);
by (Asm_simp_tac 1);
by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1);
-by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
qed "homo_power";
Goal
--- a/src/HOL/Algebra/abstract/RingHomo.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/abstract/RingHomo.thy Thu Nov 28 10:50:42 2002 +0100
@@ -4,14 +4,14 @@
Author: Clemens Ballarin, started 15 April 1997
*)
-RingHomo = NatSum +
+RingHomo = Ring +
consts
- homo :: ('a::ringS => 'b::ringS) => bool
+ homo :: ('a::ring => 'b::ring) => bool
defs
homo_def "homo f == (ALL a b. f (a + b) = f a + f b &
f (a * b) = f a * f b) &
- f <1> = <1>"
+ f 1 = 1"
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/order.ML Thu Nov 28 10:50:42 2002 +0100
@@ -0,0 +1,250 @@
+(*
+ Title: Term order, needed for normal forms in rings
+ Id: $Id$
+ Author: Clemens Ballarin and Roland Zumkeller
+ Copyright: TU Muenchen
+*)
+
+local
+
+(*
+An order is a value of type
+ ('a -> bool, 'a * 'a -> bool).
+
+The two parts are:
+ 1) a unary predicate denoting the order's domain
+ 2) a binary predicate with the semanitcs "greater than"
+
+If (d, ord) is an order then ord (a,b) is defined if both d a and d b.
+*)
+
+(*
+Combines two orders with disjoint domains and returns
+another one.
+When the compared values are from the same domain, the corresponding
+order is used. If not the ones from the first domain are considerer
+greater. (If a value is in neither of the two domains, exception
+"Domain" is raised.)
+*)
+
+fun combineOrd ((d1, ord1), (d2, ord2)) =
+ (fn x => d1 x orelse d2 x,
+ fn (a, b) =>
+ if d1 a andalso d1 b then ord1 (a, b) else
+ if d1 a andalso d2 b then true else
+ if d2 a andalso d2 b then ord2 (a, b) else
+ if d2 a andalso d1 b then false else raise Domain)
+
+
+(* Counts the number of function applications + 1. *)
+(* ### is there a standard Isabelle function for this? *)
+
+fun tsize (a $ b) = tsize a + tsize b
+ | tsize _ = 1;
+
+(* foldl on non-empty lists *)
+
+fun foldl2 f (x::xs) = foldl f (x,xs)
+
+
+(* Compares two terms, ignoring type information. *)
+infix e;
+fun Const (s1, _) e Const (s2, _) = s1 = s2
+ | Free (s1, _) e Free (s2, _) = s1 = s2
+ | Var (ix1, _) e Var (ix2, _) = ix1 = ix2
+ | Bound i1 e Bound i2 = i1 = i2
+ | Abs (s1, _, t1) e Abs (s2, _, t2) = s1 = s2 andalso t1 = t2
+ | (s1 $ s2) e (t1 $ t2) = s1 = t1 andalso s2 = t2
+ | _ e _ = false
+
+
+
+(* Curried lexicographich path order induced by an order on function symbols.
+Its feature include:
+- compatibility with Epsilon-operations
+- closure under substitutions
+- well-foundedness
+- subterm-property
+- termination
+- defined on all terms (not only on ground terms)
+- linearity
+
+The order ignores types.
+*)
+
+infix g;
+fun clpo (d, ord) (s,t) =
+ let val (op g) = clpo (d, ord) in
+ (s <> t) andalso
+ if tsize s < tsize t then not (t g s) else
+ (* improves performance. allowed because clpo is total. *)
+ #2 (foldl2 combineOrd [
+ (fn _ $ _ => true | Abs _ => true | _ => false,
+ fn (Abs (_, _, s'), t) => s' e t orelse s' g t orelse
+ (case t of
+ Abs (_, _, t') => s' g t'
+ | t1 $ t2 => s g t1 andalso s g t2
+ )
+ | (s1 $ s2, t) => s1 e t orelse s2 e t orelse
+ s1 g t orelse s2 g t orelse
+ (case t of
+ t1 $ t2 => (s1 e t1 andalso s2 g t2) orelse
+ (s1 g t1 andalso s g t2)
+ | _ => false
+ )
+ ),
+ (fn Free _ => true | _ => false, fn (Free (a,_), Free (b,_)) => a > b),
+ (fn Bound _ => true | _ => false, fn (Bound a, Bound b) => a > b),
+ (fn Const (c, _) => not (d c) | _ => false, fn (Const (a, _), Const (b, _)) => a > b),
+ (fn Const (c, _) => d c | _ => false, fn (Const (a, _), Const (b, _)) => ord (a,b))
+ ]) (s,t)
+ end;
+
+(*
+Open Issues:
+- scheme variables have to be ordered (should be simple)
+*)
+
+(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
+
+(* Returns the position of an element in a list. If the
+element doesn't occur in the list, a MatchException is raised. *)
+fun pos (x::xs) i = if x = i then 0 else 1 + pos xs i;
+
+(* Generates a finite linear order from a list.
+[a, b, c] results in the order "a > b > c". *)
+fun linOrd l = fn (a,b) => pos l a < pos l b;
+
+(* Determines whether an element is contained in a list. *)
+fun contains (x::xs) i = (x = i) orelse (contains xs i) |
+ contains [] i = false;
+
+in
+
+(* Term order for commutative rings *)
+
+fun termless_ring (a, b) =
+ let
+ val S = ["op *", "op -", "uminus", "op +", "0"];
+ (* Order (decending from left to right) on the constant symbols *)
+ val baseOrd = (contains S, linOrd S);
+ in clpo baseOrd (b, a)
+ end;
+
+(*** Rewrite rules ***)
+
+val a_assoc = thm "ring.a_assoc";
+val l_zero = thm "ring.l_zero";
+val l_neg = thm "ring.l_neg";
+val a_comm = thm "ring.a_comm";
+val m_assoc = thm "ring.m_assoc";
+val l_one = thm "ring.l_one";
+val l_distr = thm "ring.l_distr";
+val m_comm = thm "ring.m_comm";
+val minus_def = thm "ring.minus_def";
+val inverse_def = thm "ring.inverse_def";
+val divide_def = thm "ring.divide_def";
+val power_def = thm "ring.power_def";
+
+(* These are the following axioms:
+
+ a_assoc: "(a + b) + c = a + (b + c)"
+ l_zero: "0 + a = a"
+ l_neg: "(-a) + a = 0"
+ a_comm: "a + b = b + a"
+
+ m_assoc: "(a * b) * c = a * (b * c)"
+ l_one: "1 * a = a"
+
+ l_distr: "(a + b) * c = a * c + b * c"
+
+ m_comm: "a * b = b * a"
+
+ -- {* Definition of derived operations *}
+
+ minus_def: "a - b = a + (-b)"
+ inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
+ divide_def: "a / b = a * inverse b"
+ power_def: "a ^ n = nat_rec 1 (%u b. b * a) n"
+*)
+
+(* These lemmas are needed in the proofs *)
+val trans = thm "trans";
+val sym = thm "sym";
+val subst = thm "subst";
+val box_equals = thm "box_equals";
+val arg_cong = thm "arg_cong";
+(* current theory *)
+val thy = the_context ();
+
+(* derived rewrite rules *)
+val a_lcomm = prove_goal thy "(a::'a::ring)+(b+c) = b+(a+c)"
+ (fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1,
+ rtac (a_comm RS arg_cong) 1]);
+val r_zero = prove_goal thy "(a::'a::ring) + 0 = a"
+ (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
+val r_neg = prove_goal thy "(a::'a::ring) + (-a) = 0"
+ (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
+val r_neg2 = prove_goal thy "(a::'a::ring) + (-a + b) = b"
+ (fn _ => [rtac (a_assoc RS sym RS trans) 1,
+ simp_tac (simpset() addsimps [r_neg, l_zero]) 1]);
+val r_neg1 = prove_goal thy "-(a::'a::ring) + (a + b) = b"
+ (fn _ => [rtac (a_assoc RS sym RS trans) 1,
+ simp_tac (simpset() addsimps [l_neg, l_zero]) 1]);
+(* auxiliary *)
+val a_lcancel = prove_goal thy "!! a::'a::ring. a + b = a + c ==> b = c"
+ (fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2,
+ res_inst_tac [("a1", "a")] (l_neg RS subst) 1,
+ asm_simp_tac (simpset() addsimps [a_assoc]) 1]);
+val minus_add = prove_goal thy "-((a::'a::ring) + b) = (-a) + (-b)"
+ (fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1,
+ simp_tac (simpset() addsimps [r_neg, l_neg, l_zero,
+ a_assoc, a_comm, a_lcomm]) 1]);
+val minus_minus = prove_goal thy "-(-(a::'a::ring)) = a"
+ (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]);
+val minus0 = prove_goal thy "- 0 = (0::'a::ring)"
+ (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1,
+ rtac (l_zero RS sym) 1]);
+
+(* derived rules for multiplication *)
+val m_lcomm = prove_goal thy "(a::'a::ring)*(b*c) = b*(a*c)"
+ (fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1,
+ rtac (m_comm RS arg_cong) 1]);
+val r_one = prove_goal thy "(a::'a::ring) * 1 = a"
+ (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
+val r_distr = prove_goal thy "(a::'a::ring) * (b + c) = a * b + a * c"
+ (fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1,
+ simp_tac (simpset() addsimps [m_comm]) 1]);
+(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
+val l_null = prove_goal thy "0 * (a::'a::ring) = 0"
+ (fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1,
+ simp_tac (simpset() addsimps [r_zero]) 1]);
+val r_null = prove_goal thy "(a::'a::ring) * 0 = 0"
+ (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
+val l_minus = prove_goal thy "(-(a::'a::ring)) * b = - (a * b)"
+ (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
+ rtac (l_distr RS sym RS trans) 1,
+ simp_tac (simpset() addsimps [l_null, r_neg]) 1]);
+val r_minus = prove_goal thy "(a::'a::ring) * (-b) = - (a * b)"
+ (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
+ rtac (r_distr RS sym RS trans) 1,
+ simp_tac (simpset() addsimps [r_null, r_neg]) 1]);
+
+val ring_ss = HOL_basic_ss settermless termless_ring addsimps
+ [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
+ r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
+ a_lcomm, m_lcomm, r_distr, l_null, r_null, l_minus, r_minus];
+
+val x = bind_thms ("ring_simps", [l_zero, r_zero, l_neg, r_neg,
+ minus_minus, minus0,
+ l_one, r_one, l_null, r_null, l_minus, r_minus]);
+
+(* note: r_one added to ring_simp but not ring_ss *)
+
+(* note: not added (and not proved):
+ a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one,
+ m_lcancel_eq, m_rcancel_eq,
+ thms involving dvd, integral domains, fields
+*)
+
+end;
\ No newline at end of file
--- a/src/HOL/Algebra/poly/Degree.ML Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,358 +0,0 @@
-(*
- Degree of polynomials
- $Id$
- written by Clemens Ballarin, started 22 January 1997
-*)
-
-(* Relating degree and bound *)
-
-Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
-by (force_tac (claset() addDs [inst "m" "n" boundD],
- simpset()) 1);
-qed "below_bound";
-
-goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
-by (rtac exE 1);
-by (rtac LeastI 2);
-by (assume_tac 2);
-by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
-by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
-qed "Least_is_bound";
-
-Goalw [coeff_def, deg_def]
- "!! 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";
-by (case_tac "n = 0" 1);
-(* Case n=0 *)
-by (Asm_simp_tac 1);
-(* Case n~=0 *)
-by (rotate_tac 1 1);
-by (Asm_full_simp_tac 1);
-by (rtac below_bound 1);
-by (assume_tac 2);
-by (rtac Least_is_bound 1);
-qed "deg_belowI";
-
-Goalw [coeff_def, deg_def]
- "deg p < m ==> coeff m p = 0";
-by (rtac exE 1); (* create !! x. *)
-by (rtac boundD 2);
-by (assume_tac 3);
-by (rtac LeastI 2);
-by (assume_tac 2);
-by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
-by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
-qed "deg_aboveD";
-
-Goalw [deg_def]
- "deg p = Suc y ==> ~ bound y (Rep_UP p)";
-by (rtac not_less_Least 1);
-by (Asm_simp_tac 1);
-val lemma1 = result();
-
-Goalw [deg_def, coeff_def]
- "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);
-by (subgoal_tac "bound y (Rep_UP p)" 1);
-(* prove subgoal *)
-by (rtac boundI 2);
-by (case_tac "Suc y < m" 2);
-(* first case *)
-by (rtac boundD 2);
-by (assume_tac 2);
-by (Asm_simp_tac 2);
-(* second case *)
-by (dtac leI 2);
-by (dtac Suc_leI 2);
-by (dtac le_anti_sym 2);
-by (assume_tac 2);
-by (Asm_full_simp_tac 2);
-(* end prove subgoal *)
-by (fold_goals_tac [deg_def]);
-by (dtac lemma1 1);
-by (etac notE 1);
-by (assume_tac 1);
-val lemma2 = result();
-
-Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
-by (rtac lemma2 1);
-by (Full_simp_tac 1);
-by (dtac Suc_pred 1);
-by (rtac sym 1);
-by (Asm_simp_tac 1);
-qed "deg_lcoeff";
-
-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);
-by (rtac up_eqI 1);
-by (case_tac "n=0" 1);
-by (rotate_tac ~2 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-qed "nonzero_lcoeff";
-
-Goal "(deg p <= n) = bound n (Rep_UP p)";
-by (rtac iffI 1);
-(* ==> *)
-by (rtac boundI 1);
-by (fold_goals_tac [coeff_def]);
-by (rtac deg_aboveD 1);
-by (fast_arith_tac 1);
-(* <== *)
-by (rtac deg_aboveI 1);
-by (rewtac coeff_def);
-by (Fast_tac 1);
-qed "deg_above_is_bound";
-
-(* Lemmas on the degree function *)
-
-Goalw [max_def]
- "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
-by (case_tac "deg p <= deg q" 1);
-(* case deg p <= deg q *)
-by (rtac deg_aboveI 1);
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (dtac le_less_trans 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-(* case deg p > deg q *)
-by (rtac deg_aboveI 1);
-by (Asm_simp_tac 1);
-by (dtac not_leE 1);
-by (strip_tac 1);
-by (dtac less_trans 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-qed "deg_add";
-
-Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
-by (rtac order_antisym 1);
-by (rtac le_trans 1);
-by (rtac deg_add 1);
-by (Asm_simp_tac 1);
-by (rtac deg_belowI 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
-qed "deg_add_equal";
-
-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 (rtac deg_monom_ring 1);
-(* >= *)
-by (asm_simp_tac
- (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
-qed "deg_monom";
-
-Goal "!! a::'a::ring. deg (const a) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-by (rtac deg_belowI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-qed "deg_const";
-
-Goal "deg (0::'a::ringS up) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (Simp_tac 1);
-by (rtac deg_belowI 1);
-by (Simp_tac 1);
-qed "deg_zero";
-
-Goal "deg (<1>::'a::ring up) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-by (rtac deg_belowI 1);
-by (Simp_tac 1);
-qed "deg_one";
-
-Goal "!!p::('a::ring) up. deg (-p) = deg p";
-by (rtac le_anti_sym 1);
-(* <= *)
-by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
-by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
-qed "deg_uminus";
-
-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);
-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)";
-by (rtac le_anti_sym 1);
-by (rtac deg_smult_ring 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";
-by (simp_tac (simpset() addsimps [coeff_def]) 1);
-by (rtac bound_mult_zero 1);
-by (assume_tac 3);
-by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
-by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
-qed "deg_above_mult_zero";
-
-Goal
- "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
-by (rtac deg_aboveI 1);
-by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
-qed "deg_mult_ring";
-
-goal Main.thy
- "!!k::nat. k < n ==> m < n + m - k";
-by (arith_tac 1);
-qed "less_add_diff";
-
-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);
-qed "deg_below2I";
-
-Goal
- "!! p::'a::domain up. \
-\ [| 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) *)
-by (rtac deg_below2I 1);
-by (Simp_tac 1);
-(*
-by (rtac conjI 1);
-by (rtac impI 1);
-*)
-by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
-by (rtac le_add1 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
-by (rtac le_refl 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
-(*
-by (rtac impI 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
-by (rtac le_add1 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
-by (rtac le_refl 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
-*)
-qed "deg_mult";
-
-Addsimps [deg_smult, deg_mult];
-
-(* Representation theorems about polynomials *)
-
-goal PolyRing.thy
- "!! 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 ==> 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],
- simpset()));
-qed "bound_SUM_if";
-
-Goal
- "!! 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);
-by (res_inst_tac [("x", "na")] bound_SUM_if 2);
-by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
-by (rtac SUM_cong 1);
-by (rtac refl 1);
-by (Asm_simp_tac 1);
-qed "up_repr";
-
-Goal
- "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
-\ 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 (setsum (%i. coeff i p *s monom i) {..n}) |] \
-\ ==> P p";
-by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
-qed "up_repr2D";
-
-(*
-Goal
- "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
-\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
-\ = (coeff k f = coeff k g)
-...
-qed "up_unique";
-*)
-
-(* Polynomials over integral domains are again integral domains *)
-
-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 (force_tac (claset() addIs [up_eqI], simpset()) 1);
-by (rtac integral 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";
-by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
-by (dtac up_integral 1);
-by Auto_tac;
-by (rtac (const_inj RS injD) 1);
-by (Simp_tac 1);
-qed "smult_integral";
-
-(* Divisibility and degree *)
-
-Goalw [dvd_def]
- "!! 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 (Asm_simp_tac 1);
-by (dtac r_nullD 1);
-by (asm_simp_tac (simpset() addsimps [le_add1]) 1);
-qed "dvd_imp_deg";
--- a/src/HOL/Algebra/poly/Degree.thy Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*
- Degree of polynomials
- $Id$
- written by Clemens Ballarin, started 22. 1. 1997
-*)
-
-Degree = PolyRing +
-
-consts
- deg :: ('a::ringS) up => nat
-
-defs
- deg_def "deg p == LEAST n. bound n (Rep_UP p)"
-
-end
--- a/src/HOL/Algebra/poly/LongDiv.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML Thu Nov 28 10:50:42 2002 +0100
@@ -4,10 +4,55 @@
Author: Clemens Ballarin, started 23 June 1999
*)
+(* legacy bindings and theorems *)
+
+val deg_aboveI = thm "deg_aboveI";
+val smult_l_minus = thm "smult_l_minus";
+val deg_monom_ring = thm "deg_monom_ring";
+val deg_smult_ring = thm "deg_smult_ring";
+val smult_l_distr = thm "smult_l_distr";
+val smult_r_distr = thm "smult_r_distr";
+val smult_r_minus = thm "smult_r_minus";
+val smult_assoc2 = thm "smult_assoc2";
+val smult_assoc1 = thm "smult_assoc1";
+val monom_mult_smult = thm "monom_mult_smult";
+val field_ax = thm "field_ax";
+val lcoeff_nonzero = thm "lcoeff_nonzero";
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ (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);
+by (Simp_tac 1);
+by (Force_tac 1);
+(* Induction step *)
+by (asm_simp_tac (simpset() addsimps add_ac) 1);
+val SUM_shrink_below_lemma = result();
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ [| 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";
+
+Goal
+ "!! p::'a::ring up. \
+\ [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |] \
+\ ==> P p";
+by (asm_full_simp_tac (simpset() addsimps [thm "up_repr_le"]) 1);
+qed "up_repr2D";
+
+(* Start of LongDiv *)
+
Goal
"!!p::('a::ring up). \
\ [| deg p <= deg r; deg q <= deg r; \
-\ coeff (deg r) p = - (coeff (deg r) q); deg r ~= 0 |] ==> \
+\ coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==> \
\ deg (p + q) < deg r";
by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1);
by (arith_tac 2);
@@ -25,7 +70,7 @@
Goal
"!!p::('a::ring up). \
\ [| deg p <= deg r; deg q <= deg r; \
-\ p ~= -q; coeff (deg r) p = - (coeff (deg r) q) |] ==> \
+\ p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==> \
\ deg (p + q) < deg r";
by (rtac deg_lcoeff_cancel 1);
by (REPEAT (atac 1));
@@ -51,7 +96,7 @@
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 (dres_inst_tac [("x", "lcoeff g *s x - (monom (lcoeff x) (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);
@@ -71,14 +116,35 @@
by (rtac le_trans 1);
by (rtac deg_mult_ring 1);
by (rtac le_trans 1);
+(**)
+ by (rtac add_le_mono 1); by (rtac le_refl 1);
+ (* term order forces to use this instead of add_le_mono1 *)
+ by (rtac deg_monom_ring 1);
+ by (Asm_simp_tac 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 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);
+(**)
+ (* This change is probably caused by application of commutativity *)
+by (res_inst_tac [("m", "deg g"), ("n", "deg x")] SUM_extend 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+by (arith_tac 1);
+by (res_inst_tac [("m", "deg g"), ("n", "deg g")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (Asm_simp_tac 1);
+by (arith_tac 1);
+by (Simp_tac 1);
+(**)
+(*
by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym]) 1);
@@ -87,14 +153,19 @@
by (rtac le_refl 1);
by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
by (asm_simp_tac (simpset() addsimps [diff_diff_right, leI, m_comm]) 1);
+*)
(* end of subproof deg f1 < deg f *)
by (etac exE 1);
-by (res_inst_tac [("x", "((%(q,r,k). ((lcoeff g ^ k * lcoeff x) *s monom (deg x - deg g) + q)) xa, (%(q,r,k). r) xa, (%(q,r,k). Suc k) xa)")] exI 1);
+by (res_inst_tac [("x", "((%(q,r,k). (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (%(q,r,k). r) xa, (%(q,r,k). Suc k) xa)")] exI 1);
by (Clarify_tac 1);
by (dtac sym 1);
-by (simp_tac (simpset() addsimps [l_distr, a_assoc]) 1);
-by (Asm_simp_tac 1);
-by (simp_tac (simpset() addsimps a_ac@[smult_l_distr, smult_r_distr, smult_r_minus, smult_assoc2, smult_assoc1]) 1);
+by (simp_tac (simpset() addsimps [l_distr, a_assoc]
+ delsimprocs [ring_simproc]) 1);
+by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1);
+by (simp_tac (simpset() addsimps [minus_def, smult_r_distr, smult_r_minus,
+ monom_mult_smult, smult_assoc1, smult_assoc2]
+ delsimprocs [ring_simproc]) 1);
+by (Simp_tac 1);
qed "long_div_eucl_size";
Goal
@@ -102,8 +173,9 @@
\ Ex (% (q, r, k). \
\ (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;
+ (simplify (simpset() addsimps [eucl_size_def]
+ delsimprocs [ring_simproc]) long_div_eucl_size) 1);
+by (auto_tac (claset(), simpset() delsimprocs [ring_simproc]));
by (case_tac "aa = 0" 1);
by (Blast_tac 1);
(* case "aa ~= 0 *)
@@ -111,18 +183,20 @@
by Auto_tac;
qed "long_div_ring";
+(* Next one fails *)
Goal
- "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd <1> |] ==> \
+ "!!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, \
\ (%(q,r,k). inverse(lcoeff g ^k) *s r) x)")] exI 1);
by (Clarify_tac 1);
-by (Simp_tac 1);
+(* by (Simp_tac 1); *)
by (rtac conjI 1);
by (dtac sym 1);
-by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]) 1);
+by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]
+ delsimprocs [ring_simproc]) 1);
by (asm_simp_tac (simpset() addsimps [l_inverse_ring, unit_power, smult_assoc1 RS sym]) 1);
(* degree property *)
by (etac disjE 1);
@@ -138,14 +212,28 @@
\ 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);
+by (asm_simp_tac (simpset() addsimps [lcoeff_def, lcoeff_nonzero, field_ax]) 1);
qed "long_div_theorem";
+Goal "- (0::'a::ring) = 0";
+by (Simp_tac 1);
+val uminus_zero = result();
+
+Goal "!!a::'a::ring. a - b = 0 ==> a = b";
+br trans 1;
+by (res_inst_tac [("b", "a")] (thm "bug") 2);
+by (Asm_simp_tac 1);
+val diff_zero_imp_eq = result();
+
+Goal "!!a::'a::ring. a = b ==> a + (-b) = 0";
+by (Asm_simp_tac 1);
+val eq_imp_diff_zero = result();
+
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";
-by (subgoal_tac "(q1 -- q2) * g = r2 -- r1" 1); (* 1 *)
+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);
@@ -154,18 +242,23 @@
(* r1 = 0 *)
by (etac disjE 1);
(* r2 = 0 *)
-by (force_tac (claset() addDs [integral], simpset()) 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [thm "integral_iff", minus_def, l_zero, uminus_zero]
+ delsimprocs [ring_simproc]) 1);
(* r2 ~= 0 *)
-by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
-by (Force_tac 1);
+by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero]
+ delsimprocs [ring_simproc]) 1);
(* r1 ~=0 *)
by (etac disjE 1);
(* r2 = 0 *)
-by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
-by (Force_tac 1);
+by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero]
+ delsimprocs [ring_simproc]) 1);
(* r2 ~= 0 *)
-by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
-by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [minus_def]
+ delsimprocs [ring_simproc]) 1);
by (dtac (order_eq_refl RS add_leD2) 1);
by (dtac leD 1);
by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1);
@@ -174,7 +267,7 @@
by (rtac diff_zero_imp_eq 1);
by (hyp_subst_tac 1);
by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1);
-by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1);
+by (Asm_full_simp_tac 1);
qed "long_div_quo_unique";
Goal
@@ -183,7 +276,11 @@
\ 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);
+by (res_inst_tac [("a", "q2 * g + r1 - q2 * g"), ("b", "q2 * g + r2 - q2 * g")]
+ box_equals 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
by (rtac long_div_quo_unique 1);
by (REPEAT (atac 1));
qed "long_div_rem_unique";
--- a/src/HOL/Algebra/poly/LongDiv.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy Thu Nov 28 10:50:42 2002 +0100
@@ -7,11 +7,11 @@
LongDiv = PolyHomo +
consts
- lcoeff :: "'a::ringS up => 'a"
- eucl_size :: 'a::ringS => nat
+ lcoeff :: "'a::ring up => 'a"
+ eucl_size :: 'a::ring => nat
defs
- lcoeff_def "lcoeff p == coeff (deg p) p"
+ lcoeff_def "lcoeff p == coeff p (deg p)"
eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1"
end
--- a/src/HOL/Algebra/poly/PolyHomo.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.ML Thu Nov 28 10:50:42 2002 +0100
@@ -4,8 +4,85 @@
Author: Clemens Ballarin, started 16 April 1997
*)
+(* Summation result for tactic-style proofs *)
+
+val natsum_add = thm "natsum_add";
+val natsum_ldistr = thm "natsum_ldistr";
+val natsum_rdistr = thm "natsum_rdistr";
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ 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);
+(* Induction step *)
+by (case_tac "m <= n" 1);
+by Auto_tac;
+by (subgoal_tac "m = Suc n" 1);
+by (Asm_simp_tac 1);
+by (fast_arith_tac 1);
+val SUM_shrink_lemma = result();
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ [| 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 (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. j <= n + m --> \
+\ 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);
+(* Induction step *)
+by (simp_tac (simpset() addsimps [Suc_diff_le, natsum_add]) 1);
+(*
+by (asm_simp_tac (simpset() addsimps a_ac) 1);
+*)
+by (Asm_simp_tac 1);
+val DiagSum_lemma = result();
+
+Goal
+ "!!f::nat=>'a::ring. \
+\ 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";
+
+Goal
+ "!! f::nat=>'a::ring. [| bound n f; bound 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 [natsum_ldistr, DiagSum]) 1);
+(* SUM_rdistr must be applied after SUM_ldistr ! *)
+by (simp_tac (simpset() addsimps [natsum_rdistr]) 1);
+by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
+by (rtac le_add1 1);
+by (Force_tac 1);
+by (rtac (thm "natsum_cong") 1);
+by (rtac refl 1);
+by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
+by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
+by Auto_tac;
+qed "CauchySum";
+
(* Ring homomorphisms and polynomials *)
-
+(*
Goal "homo (const::'a::ring=>'a up)";
by (auto_tac (claset() addSIs [homoI], simpset()));
qed "const_homo";
@@ -19,6 +96,15 @@
qed "homo_smult";
Addsimps [homo_smult];
+*)
+
+val deg_add = thm "deg_add";
+val deg_mult_ring = thm "deg_mult_ring";
+val deg_aboveD = thm "deg_aboveD";
+val coeff_add = thm "coeff_add";
+val coeff_mult = thm "coeff_mult";
+val boundI = thm "boundI";
+val monom_mult_is_smult = thm "monom_mult_is_smult";
(* Evaluation homomorphism *)
@@ -42,7 +128,7 @@
by (rtac le_maxI2 1);
by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
(* actual homom property + *)
-by (asm_simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
+by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1);
(* * commutes *)
by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")]
@@ -53,34 +139,33 @@
by (rtac CauchySum 2);
by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
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 *)
+(* getting a^i and a^(k-i) together is difficult, so we do it manually *)
by (res_inst_tac [("s",
" setsum \
\ (%k. setsum \
-\ (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \
+\ (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * \
\ (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);
-by (simp_tac (simpset() addsimps m_ac) 1);
-(* <1> commutes *)
+ addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1);
+by (Simp_tac 1);
+(* 1 commutes *)
by (Asm_simp_tac 1);
qed "EVAL2_homo";
Goalw [EVAL2_def]
- "!! phi::'a::ring=>'b::ring. EVAL2 phi a (const b) = phi b";
+ "!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b";
by (Simp_tac 1);
qed "EVAL2_const";
Goalw [EVAL2_def]
- "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a";
-(* Must be able to distinguish 0 from <1>, hence 'a::domain *)
+ "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 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::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
+ "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n";
by (Simp_tac 1);
by (case_tac "n" 1);
by Auto_tac;
@@ -89,19 +174,35 @@
Goal
"!! phi::'a::ring=>'b::ring. \
\ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p";
-by (asm_simp_tac
- (simpset() addsimps [const_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
+by (asm_simp_tac (simpset()
+ addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
qed "EVAL2_smult";
+val up_eqI = thm "up_eqI";
+
+Goal "monom (a::'a::ring) n = monom a 0 * monom 1 n";
+by (simp_tac (simpset() addsimps [monom_mult_is_smult]) 1);
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+qed "monom_decomp";
+
+Goal
+ "!! phi::'a::domain=>'b::ring. \
+\ homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n";
+by (stac monom_decomp 1);
+by (asm_simp_tac (simpset()
+ addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1);
+qed "EVAL2_monom_n";
+
Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)";
-by (asm_simp_tac (simpset() addsimps [EVAL2_homo, id_homo]) 1);
+by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1);
qed "EVAL_homo";
-Goalw [EVAL_def] "!! a::'a::ring. EVAL a (const b) = b";
+Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom b 0) = b";
by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
qed "EVAL_const";
-Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom n) = a ^ n";
+Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n";
by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
qed "EVAL_monom";
@@ -109,19 +210,23 @@
by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
qed "EVAL_smult";
+Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n";
+by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1);
+qed "EVAL_monom_n";
+
(* Examples *)
Goal
"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);
+ addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1);
result();
Goal
"EVAL (y::'a::domain) \
-\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
+\ (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \
\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
by (asm_simp_tac (simpset() delsimps [power_Suc]
- addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
+ addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1);
result();
--- a/src/HOL/Algebra/poly/PolyHomo.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy Thu Nov 28 10:50:42 2002 +0100
@@ -4,20 +4,15 @@
Author: Clemens Ballarin, started 15 April 1997
*)
-PolyHomo = Degree +
-
-(* Instantiate result from Degree.ML *)
-
-instance
- up :: (domain) domain (up_one_not_zero, up_integral)
+PolyHomo = UnivPoly +
consts
- EVAL2 :: "('a::ring => 'b) => 'b => 'a up => 'b::ring"
- EVAL :: "'a::ring => 'a up => 'a"
+ EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
+ EVAL :: "['a::ring, 'a up] => 'a"
defs
EVAL2_def "EVAL2 phi a p ==
- setsum (%i. phi (coeff i p) * a ^ i) {..deg p}"
+ setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
EVAL_def "EVAL == EVAL2 (%x. x)"
end
--- a/src/HOL/Algebra/poly/PolyRing.ML Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*
- Instantiate polynomials to form a ring and prove further properties
- $Id$
- Author: Clemens Ballarin, started 22 January 1997
-*)
-
-(* Properties of *s:
- Polynomials form a module *)
-
-goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p";
-by (rtac up_eqI 1);
-by (simp_tac (simpset() addsimps [l_distr]) 1);
-qed "smult_l_distr";
-
-goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q";
-by (rtac up_eqI 1);
-by (simp_tac (simpset() addsimps [r_distr]) 1);
-qed "smult_r_distr";
-
-goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)";
-by (rtac up_eqI 1);
-by (simp_tac (simpset() addsimps [m_assoc]) 1);
-qed "smult_assoc1";
-
-goal UnivPoly.thy "(<1>::'a::ring) *s p = p";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-qed "smult_one";
-
-(* Polynomials form an algebra *)
-
-goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)";
-by (rtac up_eqI 1);
-by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1);
-qed "smult_assoc2";
-
-(* the following can be derived from the above ones,
- for generality reasons, it is therefore done *)
-
-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";
-by (rtac a_lcancel 1);
-by (rtac (smult_r_distr RS sym RS trans) 1);
-by (Simp_tac 1);
-qed "smult_r_null";
-
-Goal "!!a::'a::ring. (-a) *s p = - (a *s p)";
-by (rtac a_lcancel 1);
-by (rtac (r_neg RS sym RSN (2, trans)) 1);
-by (rtac (smult_l_distr RS sym RS trans) 1);
-by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1);
-qed "smult_l_minus";
-
-Goal "!!a::'a::ring. a *s (-p) = - (a *s p)";
-by (rtac a_lcancel 1);
-by (rtac (r_neg RS sym RSN (2, trans)) 1);
-by (rtac (smult_r_distr RS sym RS trans) 1);
-by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1);
-qed "smult_r_minus";
-
-val smult_minus = [smult_l_minus, smult_r_minus];
-
-Addsimps [smult_one, smult_l_null, smult_r_null];
--- a/src/HOL/Algebra/poly/PolyRing.thy Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*
- Instantiate polynomials to form a ring and prove further properties
- $Id$
- Author: Clemens Ballarin, started 20 January 1997
-*)
-
-PolyRing = UnivPoly +
-
-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_inverse_def, up_divide_def, up_power_def) {| ALLGOALS (rtac refl) |}
-
-end
--- a/src/HOL/Algebra/poly/ProtoPoly.ML Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*
- Prepearing definitions for polynomials
- $Id$
- Author: Clemens Ballarin, started 9 December 1996
-*)
-
-(* Rules for bound *)
-
-val prem = goalw ProtoPoly.thy [bound_def]
- "[| !! 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";
-by (Fast_tac 1);
-qed "boundD";
-
-Goalw [bound_def]
- "!! f. [| bound n f; n <= m |] ==> bound m f";
-by (fast_tac (set_cs addIs [le_less_trans]) 1);
-(* Need set_cs, otherwise starts reasoning about naturals *)
-qed "le_bound";
-
-AddSIs [boundI];
-AddDs [boundD];
-
-Goal "(%x. 0) : {f. EX n. bound n f}";
-by (Blast_tac 1);
-qed "UP_witness";
--- a/src/HOL/Algebra/poly/ProtoPoly.thy Wed Nov 27 17:25:41 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*
- Prepearing definitions for polynomials
- $Id$
- Author: Clemens Ballarin, started 9 December 1996
-*)
-
-ProtoPoly = Abstract +
-
-consts
- bound :: [nat, nat => 'a::ringS] => bool
-
-defs
- bound_def "bound n f == ALL i. n<i --> f i = 0"
-
-end
--- a/src/HOL/Algebra/poly/UnivPoly.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly.ML Thu Nov 28 10:50:42 2002 +0100
@@ -1,242 +1,359 @@
(*
- Univariate Polynomials
+ Degree of polynomials
$Id$
- Author: Clemens Ballarin, started 9 December 1996
-TODO: monom is *mono*morphism (probably induction needed)
+ written by Clemens Ballarin, started 22 January 1997
*)
-(* Closure of UP under +, *s, monom, const and * *)
+(*
+(* Relating degree and bound *)
+
+Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
+by (force_tac (claset() addDs [inst "m" "n" boundD],
+ simpset()) 1);
+qed "below_bound";
+
+goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
+by (rtac exE 1);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "Least_is_bound";
+
+Goalw [coeff_def, deg_def]
+ "!! 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";
+by (case_tac "n = 0" 1);
+(* Case n=0 *)
+by (Asm_simp_tac 1);
+(* Case n~=0 *)
+by (rotate_tac 1 1);
+by (Asm_full_simp_tac 1);
+by (rtac below_bound 1);
+by (assume_tac 2);
+by (rtac Least_is_bound 1);
+qed "deg_belowI";
+
+Goalw [coeff_def, deg_def]
+ "deg p < m ==> coeff m p = 0";
+by (rtac exE 1); (* create !! x. *)
+by (rtac boundD 2);
+by (assume_tac 3);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "deg_aboveD";
+
+Goalw [deg_def]
+ "deg p = Suc y ==> ~ bound y (Rep_UP p)";
+by (rtac not_less_Least 1);
+by (Asm_simp_tac 1);
+val lemma1 = result();
+
+Goalw [deg_def, coeff_def]
+ "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);
+by (subgoal_tac "bound y (Rep_UP p)" 1);
+(* prove subgoal *)
+by (rtac boundI 2);
+by (case_tac "Suc y < m" 2);
+(* first case *)
+by (rtac boundD 2);
+by (assume_tac 2);
+by (Asm_simp_tac 2);
+(* second case *)
+by (dtac leI 2);
+by (dtac Suc_leI 2);
+by (dtac le_anti_sym 2);
+by (assume_tac 2);
+by (Asm_full_simp_tac 2);
+(* end prove subgoal *)
+by (fold_goals_tac [deg_def]);
+by (dtac lemma1 1);
+by (etac notE 1);
+by (assume_tac 1);
+val lemma2 = result();
+
+Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
+by (rtac lemma2 1);
+by (Full_simp_tac 1);
+by (dtac Suc_pred 1);
+by (rtac sym 1);
+by (Asm_simp_tac 1);
+qed "deg_lcoeff";
-Goalw [UP_def]
- "[| f : UP; g : UP |] ==> (%n. (f n + g n::'a::ring)) : UP";
-by Auto_tac;
-(* instantiate bound for the sum and do case split *)
-by (res_inst_tac [("x", "if n<=na then na else n")] exI 1);
-by Auto_tac;
-(* first case, bound of g higher *)
-by (dtac le_bound 1 THEN assume_tac 1);
-by (Force_tac 1);
-(* second case is identical,
- apart from we have to massage the inequality *)
-by (dtac (not_leE RS less_imp_le) 1);
-by (dtac le_bound 1 THEN assume_tac 1);
-by (Force_tac 1);
-qed "UP_closed_add";
+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);
+by (rtac up_eqI 1);
+by (case_tac "n=0" 1);
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "nonzero_lcoeff";
+
+Goal "(deg p <= n) = bound n (Rep_UP p)";
+by (rtac iffI 1);
+(* ==> *)
+by (rtac boundI 1);
+by (fold_goals_tac [coeff_def]);
+by (rtac deg_aboveD 1);
+by (fast_arith_tac 1);
+(* <== *)
+by (rtac deg_aboveI 1);
+by (rewtac coeff_def);
+by (Fast_tac 1);
+qed "deg_above_is_bound";
+
+(* Lemmas on the degree function *)
+
+Goalw [max_def]
+ "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
+by (case_tac "deg p <= deg q" 1);
+(* case deg p <= deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (dtac le_less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+(* case deg p > deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (dtac not_leE 1);
+by (strip_tac 1);
+by (dtac less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "deg_add";
-Goalw [UP_def]
- "f : UP ==> (%n. (a * f n::'a::ring)) : UP";
-by (Force_tac 1);
-qed "UP_closed_smult";
+Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
+by (rtac order_antisym 1);
+by (rtac le_trans 1);
+by (rtac deg_add 1);
+by (Asm_simp_tac 1);
+by (rtac deg_belowI 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
+qed "deg_add_equal";
+
+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 (rtac deg_monom_ring 1);
+(* >= *)
+by (asm_simp_tac
+ (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
+qed "deg_monom";
-Goalw [UP_def]
- "(%n. if m = n then <1> else 0) : UP";
-by Auto_tac;
-qed "UP_closed_monom";
+Goal "!! a::'a::ring. deg (const a) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+qed "deg_const";
+
+Goal "deg (0::'a::ringS up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (Simp_tac 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_zero";
-Goalw [UP_def] "(%n. if n = 0 then a else 0) : UP";
-by Auto_tac;
-qed "UP_closed_const";
+Goal "deg (<1>::'a::ring up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_one";
+
+Goal "!!p::('a::ring) up. deg (-p) = deg p";
+by (rtac le_anti_sym 1);
+(* <= *)
+by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
+by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
+qed "deg_uminus";
+
+Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
Goal
- "!! f::nat=>'a::ring. \
-\ [| 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 *)
-by (Force_tac 1);
-(* Second case, we have to derive m < k-i *)
-by (subgoal_tac "m < k-i" 1);
-by (arith_tac 2);
-by (Force_tac 1);
-qed "bound_mult_zero";
+ "!! 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";
-Goalw [UP_def]
- "[| f : UP; g : 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);
-by (Step_tac 1);
-(* Show that the sum is 0 *)
-by (asm_simp_tac (simpset() addsimps [bound_mult_zero]) 1);
-qed "UP_closed_mult";
+Goal
+ "!! 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 (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
+qed "deg_smult";
-(* %x. 0 represents a polynomial *)
-
-Goalw [UP_def] "(%x. 0) : UP";
-by (Fast_tac 1);
-qed "UP_zero";
-
-(* Effect of +, *s, monom, * and the other operations on the coefficients *)
+Goal
+ "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
+\ 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);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+qed "deg_above_mult_zero";
-Goalw [coeff_def, up_add_def]
- "coeff n (p+q) = (coeff n p + coeff n q::'a::ring)";
-by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_add, Rep_UP]) 1);
-qed "coeff_add";
+Goal
+ "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
+by (rtac deg_aboveI 1);
+by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
+qed "deg_mult_ring";
-Goalw [coeff_def, up_smult_def]
- "!!a::'a::ring. coeff n (a *s p) = a * coeff n p";
-by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_smult, Rep_UP]) 1);
-qed "coeff_smult";
+goal Main.thy
+ "!!k::nat. k < n ==> m < n + m - k";
+by (arith_tac 1);
+qed "less_add_diff";
-Goalw [coeff_def, monom_def]
- "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";
+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);
+qed "deg_below2I";
-Goalw [coeff_def, const_def]
- "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) = (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";
-by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_zero, Rep_UP]) 1);
-qed "coeff_zero";
-
-Addsimps [coeff_add, coeff_smult, coeff_monom, coeff_const,
- coeff_mult, coeff_zero];
-
-Goalw [up_one_def]
- "coeff n <1> = (if n=0 then <1> else 0)";
+Goal
+ "!! p::'a::domain up. \
+\ [| 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) *)
+by (rtac deg_below2I 1);
by (Simp_tac 1);
-qed "coeff_one";
+(*
+by (rtac conjI 1);
+by (rtac impI 1);
+*)
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+(*
+by (rtac impI 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+*)
+qed "deg_mult";
-Goalw [up_uminus_def] "coeff n (-p) = (-coeff n p::'a::ring)";
-by (simp_tac (simpset() addsimps m_minus) 1);
-qed "coeff_uminus";
+Addsimps [deg_smult, deg_mult];
+
+(* Representation theorems about polynomials *)
-Addsimps [coeff_one, coeff_uminus];
-
-(* Polynomials form a ring *)
+goal PolyRing.thy
+ "!! 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";
-val prems = Goalw [coeff_def]
- "(!! n. coeff n p = coeff n q) ==> p = q";
-by (res_inst_tac [("t", "p")] (Rep_UP_inverse RS subst) 1);
-by (res_inst_tac [("t", "q")] (Rep_UP_inverse RS subst) 1);
-by (asm_simp_tac (simpset() addsimps prems) 1);
-qed "up_eqI";
+goal UnivPoly.thy
+ "!! f::(nat=>'a::ring). \
+\ 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],
+ simpset()));
+qed "bound_SUM_if";
-Goalw [coeff_def]
- "coeff n p ~= coeff n q ==> p ~= q";
-by Auto_tac;
-qed "up_neqI";
-
-Goal "!! a::('a::ring) up. (a + b) + c = a + (b + c)";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-by (rtac a_assoc 1);
-qed "up_a_assoc";
-
-Goal "!! a::('a::ring) up. 0 + a = a";
+Goal
+ "!! 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 1);
-qed "up_l_zero";
-
-Goal "!! a::('a::ring) up. (-a) + a = 0";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-qed "up_l_neg";
-
-Goal "!! a::('a::ring) up. a + b = b + a";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-by (rtac a_comm 1);
-qed "up_a_comm";
-
-Goal "!! a::('a::ring) up. (a * b) * c = a * (b * c)";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-by (rtac poly_assoc_lemma 1);
-qed "up_m_assoc";
-
-Goal "!! a::('a::ring) up. <1> * a = a";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-by (case_tac "n" 1);
-(* 0 case *)
-by (Asm_simp_tac 1);
-(* Suc case *)
-by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
-qed "up_l_one";
-
-Goal "!! a::('a::ring) up. (a + b) * c = a * c + b * c";
-by (rtac up_eqI 1);
-by (simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
-qed "up_l_distr";
-
-Goal "!! a::('a::ring) up. a * b = b * a";
-by (rtac up_eqI 1);
-by (cut_inst_tac [("a", "%i. coeff i a"), ("b", "%i. coeff i b")]
- poly_comm_lemma 1);
-by (asm_full_simp_tac (simpset() addsimps [m_comm]) 1);
-qed "up_m_comm";
-
-(* Further algebraic rules *)
-
-Goal "!! a::'a::ring. const a * p = a *s p";
-by (rtac up_eqI 1);
-by (case_tac "n" 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
-qed "const_mult_is_smult";
-
-Goal "!! a::'a::ring. const (a + b) = const a + const b";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-qed "const_add";
-
-Goal "!! a::'a::ring. const (a * b) = const a * const b";
-by (simp_tac (simpset() addsimps [const_mult_is_smult]) 1);
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-qed "const_mult";
-
-Goal "const (<1>::'a::ring) = <1>";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-qed "const_one";
-
-Goal "const (0::'a::ring) = 0";
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-qed "const_zero";
-
-Addsimps [const_add, const_mult, const_one, const_zero];
-
-Goalw [inj_on_def, UNIV_def, const_def] "inj const";
-by (Simp_tac 1);
-by (strip_tac 1);
-by (dres_inst_tac [("f", "Rep_UP")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const,
- expand_fun_eq]) 1);
-by (dres_inst_tac [("x", "0")] spec 1);
-by (Full_simp_tac 1);
-qed "const_inj";
-
-(*Lemma used in PolyHomo*)
-Goal
- "!! f::nat=>'a::ring. [| bound n f; bound 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);
-by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
-by (rtac le_add1 1);
-by (Force_tac 1);
+by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
+by (rtac trans 1);
+by (res_inst_tac [("x", "na")] bound_SUM_if 2);
+by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
by (rtac SUM_cong 1);
by (rtac refl 1);
-by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
-by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
-by Auto_tac;
-qed "CauchySum";
+by (Asm_simp_tac 1);
+qed "up_repr";
+
+Goal
+ "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
+\ 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 (setsum (%i. coeff i p *s monom i) {..n}) |] \
+\ ==> P p";
+by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
+qed "up_repr2D";
+
+(*
+Goal
+ "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
+\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
+\ = (coeff k f = coeff k g)
+...
+qed "up_unique";
+*)
+
+(* Polynomials over integral domains are again integral domains *)
-Goal "<1> ~= (0::('a::domain) up)";
-by (res_inst_tac [("n", "0")] up_neqI 1);
+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 (force_tac (claset() addIs [up_eqI], simpset()) 1);
+by (rtac integral 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";
+by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
+by (dtac up_integral 1);
+by Auto_tac;
+by (rtac (const_inj RS injD) 1);
by (Simp_tac 1);
-qed "up_one_not_zero";
+qed "smult_integral";
+*)
+
+(* Divisibility and degree *)
+
+Goalw [dvd_def]
+ "!! 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 "k = 0" 2);
+by Auto_tac;
+qed "dvd_imp_deg";
--- a/src/HOL/Algebra/poly/UnivPoly.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly.thy Thu Nov 28 10:50:42 2002 +0100
@@ -1,44 +1,748 @@
(*
- Univariate Polynomials
- $Id$
- Author: Clemens Ballarin, started 9 December 1996
+ Title: Univariate Polynomials
+ Id: $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+ Copyright: Clemens Ballarin
+*)
+
+header {* Univariate Polynomials *}
+
+theory UnivPoly = Abstract:
+
+(* already proved in Finite_Set.thy
+
+lemma setsum_cong:
+ "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
+proof -
+ assume prems: "A = B" "!!i. i : B ==> f i = g i"
+ show ?thesis
+ proof (cases "finite B")
+ case True
+ then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
+ setsum f A = setsum g B"
+ proof induct
+ case empty thus ?case by simp
+ next
+ case insert thus ?case by simp
+ qed
+ with prems show ?thesis by simp
+ next
+ case False with prems show ?thesis by (simp add: setsum_def)
+ qed
+qed
*)
-UnivPoly = ProtoPoly +
+(* Instruct simplifier to simplify assumptions introduced by congs.
+ This makes setsum_cong more convenient to use, because assumptions
+ like i:{m..n} get simplified (to m <= i & i <= n). *)
+
+ML_setup {*
+
+Addcongs [thm "setsum_cong"];
+Context.>> (fn thy => (simpset_ref_of thy :=
+ simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+
+section {* Definition of type up *}
+
+constdefs
+ bound :: "[nat, nat => 'a::zero] => bool"
+ "bound n f == (ALL i. n < i --> f i = 0)"
+
+lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
+proof (unfold bound_def)
+qed fast
+
+lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
+proof (unfold bound_def)
+qed fast
+
+lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
+proof (unfold bound_def)
+qed fast
+
+lemma bound_below:
+ assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
+proof (rule classical)
+ assume "~ ?thesis"
+ then have "m < n" by arith
+ with bound have "f n = 0" ..
+ with nonzero show ?thesis by contradiction
+qed
typedef (UP)
- ('a) up = "{f :: nat => 'a::ringS. EX n. bound n f}" (UP_witness)
+ ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
+by (rule+) (* Question: what does trace_rule show??? *)
-instance
- up :: (ringS) ringS
+section {* Constants *}
consts
- coeff :: [nat, 'a up] => 'a::ringS
- "*s" :: ['a::ringS, 'a up] => 'a up (infixl 70)
- monom :: nat => ('a::ringS) up
- const :: 'a::ringS => 'a up
+ coeff :: "['a up, nat] => ('a::zero)"
+ monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70)
+ "*s" :: "['a::{zero, times}, 'a up] => 'a up" (infixl 70)
+
+defs
+ coeff_def: "coeff p n == Rep_UP p n"
+ monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
+ smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
- "*X^" :: ['a, nat] => 'a up ("(3_*X^/_)" [71, 71] 70)
+lemma coeff_bound_ex: "EX n. bound n (coeff p)"
+proof -
+ have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+ then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
+ then show ?thesis ..
+qed
+
+lemma bound_coeff_obtain:
+ assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
+proof -
+ have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+ then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
+ with prem show P .
+qed
-translations
- "a *X^ n" == "a *s monom n"
- (* this translation is only nice for non-nested polynomials *)
+text {* Ring operations *}
+
+instance up :: (zero) zero ..
+instance up :: (one) one ..
+instance up :: (plus) plus ..
+instance up :: (minus) minus ..
+instance up :: (times) times ..
+instance up :: (inverse) inverse ..
+instance up :: (power) power ..
defs
- 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::nat. setsum
+ up_add_def: "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
+ 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 == monom 0 0"
+ up_one_def: "1 == monom 1 0"
+ up_uminus_def:"- p == (- 1) *s p"
+ (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
+ (* note: - 1 is different from -1; latter is of class number *)
+
+ up_minus_def: "(a::'a::{plus, minus} up) - b == a + (-b)"
+ up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) ==
+ (if a dvd 1 then THE x. a*x = 1 else 0)"
+ up_divide_def: "(a::'a::{times, inverse} up) / b == a * inverse b"
+ up_power_def: "(a::'a::{one, times, power} up) ^ n ==
+ nat_rec 1 (%u b. b * a) n"
+
+subsection {* Effect of operations on coefficients *}
+
+lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
+proof -
+ have "(%n. if n = m then a else 0) : UP"
+ using UP_def by force
+ from this show ?thesis
+ by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_zero [simp]: "coeff 0 n = 0"
+proof (unfold up_zero_def)
+qed simp
+
+lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
+proof (unfold up_one_def)
+qed simp
+
+lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
+proof -
+ have "!!f. f : UP ==> (%n. a * f n) : UP"
+ by (unfold UP_def) (force simp add: ring_simps)
+ (* this force step is slow *)
+ then show ?thesis
+ by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
+proof -
+ {
+ fix f g
+ assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
+ have "(%i. f i + g i) : UP"
+ proof -
+ from fup obtain n where boundn: "bound n f"
+ by (unfold UP_def) fast
+ from gup obtain m where boundm: "bound m g"
+ by (unfold UP_def) fast
+ have "bound (max n m) (%i. (f i + g i))"
+ proof
+ fix i
+ assume "max n m < i"
+ with boundn and boundm show "f i + g i = 0"
+ by (fastsimp simp add: ring_simps)
+ qed
+ then show "(%i. (f i + g i)) : UP"
+ by (unfold UP_def) fast
+ qed
+ }
+ then show ?thesis
+ by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_mult [simp]:
+ "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
+proof -
+ {
+ fix f g
+ assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
+ have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
+ proof -
+ from fup obtain n where "bound n f"
+ by (unfold UP_def) fast
+ from gup obtain m where "bound m g"
+ by (unfold UP_def) fast
+ have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
+ proof
+ fix k
+ assume bound: "n + m < k"
+ {
+ fix i
+ have "f i * g (k-i) = 0"
+ proof cases
+ assume "n < i"
+ show ?thesis by (auto! simp add: ring_simps)
+ next
+ assume "~ (n < i)"
+ with bound have "m < k-i" by arith
+ then show ?thesis by (auto! simp add: ring_simps)
+ qed
+ }
+ then show "setsum (%i. f i * g (k-i)) {..k} = 0"
+ by (simp add: ring_simps)
+ qed
+ then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
+ by (unfold UP_def) fast
+ qed
+ }
+ then show ?thesis
+ by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
+by (unfold up_uminus_def) (simp add: ring_simps)
+
+(* Other lemmas *)
+
+lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
+proof -
+ have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
+ also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
+ also have "... = q" by (simp add: Rep_UP_inverse)
+ finally show ?thesis .
+qed
+
+(* ML_setup {* Addsimprocs [ring_simproc] *} *)
+
+instance up :: (ring) ring
+proof
+ fix p q r :: "'a::ring up"
+ fix n
+ show "(p + q) + r = p + (q + r)"
+ by (rule up_eqI) simp
+ show "0 + p = p"
+ by (rule up_eqI) simp
+ show "(-p) + p = 0"
+ by (rule up_eqI) simp
+ show "p + q = q + p"
+ by (rule up_eqI) simp
+ show "(p * q) * r = p * (q * r)"
+ proof (rule up_eqI)
+ fix n
+ {
+ fix k and a b c :: "nat=>'a::ring"
+ have "k <= n ==>
+ 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}"
+ (is "_ ==> ?eq k")
+ proof (induct k)
+ case 0 show ?case by simp
+ next
+ case (Suc k)
+ then have "k <= n" by arith
+ then have "?eq k" by (rule Suc)
+ then show ?case
+ by (simp add: Suc_diff_le natsum_ldistr)
+ qed
+ }
+ then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
+ by simp
+ qed
+ show "1 * p = p"
+ proof (rule up_eqI)
+ fix n
+ show "coeff (1 * p) n = coeff p n"
+ proof (cases n)
+ case 0 then show ?thesis by simp
+ next
+ case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
+ qed
+ qed
+ show "(p + q) * r = p * r + q * r"
+ by (rule up_eqI) simp
+ show "p * q = q * p"
+ proof (rule up_eqI)
+ fix n
+ {
+ fix k
+ fix a b :: "nat=>'a::ring"
+ have "k <= n ==>
+ setsum (%i. a i * b (n-i)) {..k} =
+ setsum (%i. a (k-i) * b (i+n-k)) {..k}"
+ (is "_ ==> ?eq k")
+ proof (induct k)
+ case 0 show ?case by simp
+ next
+ case (Suc k) then show ?case by (subst natsum_Suc2) simp
+ qed
+ }
+ then show "coeff (p * q) n = coeff (q * p) n"
+ by simp
+ qed
+
+ show "p - q = p + (-q)"
+ by (simp add: up_minus_def)
+ show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
+ by (simp add: up_inverse_def)
+ show "p / q = p * inverse q"
+ by (simp add: up_divide_def)
+ show "p ^ n = nat_rec 1 (%u b. b * p) n"
+ by (simp add: up_power_def)
+ qed
+
+(* Further properties of monom *)
+
+lemma monom_zero [simp]:
+ "monom 0 n = 0"
+ by (simp add: monom_def up_zero_def)
+
+lemma monom_mult_is_smult:
+ "monom (a::'a::ring) 0 * p = a *s p"
+proof (rule up_eqI)
+ fix k
+ show "coeff (monom a 0 * p) k = coeff (a *s p) k"
+ proof (cases k)
+ case 0 then show ?thesis by simp
+ next
+ case Suc then show ?thesis by simp
+ qed
+qed
+
+lemma monom_add [simp]:
+ "monom (a + b) n = monom (a::'a::ring) n + monom b n"
+by (rule up_eqI) simp
+
+lemma monom_mult_smult:
+ "monom (a * b) n = a *s monom (b::'a::ring) n"
+by (rule up_eqI) simp
+
+lemma monom_uminus [simp]:
+ "monom (-a) n = - monom (a::'a::ring) n"
+by (rule up_eqI) simp
+
+lemma monom_one [simp]:
+ "monom 1 0 = 1"
+by (simp add: up_one_def)
+
+lemma monom_inj:
+ "(monom a n = monom b n) = (a = b)"
+proof
+ assume "monom a n = monom b n"
+ then have "coeff (monom a n) n = coeff (monom b n) n" by simp
+ then show "a = b" by simp
+next
+ assume "a = b" then show "monom a n = monom b n" by simp
+qed
+
+(* Properties of *s:
+ Polynomials form a module *)
+
+lemma smult_l_distr:
+ "(a + b::'a::ring) *s p = a *s p + b *s p"
+by (rule up_eqI) simp
+
+lemma smult_r_distr:
+ "(a::'a::ring) *s (p + q) = a *s p + a *s q"
+by (rule up_eqI) simp
+
+lemma smult_assoc1:
+ "(a * b::'a::ring) *s p = a *s (b *s p)"
+by (rule up_eqI) simp
+
+lemma smult_one [simp]:
+ "(1::'a::ring) *s p = p"
+by (rule up_eqI) simp
+
+(* Polynomials form an algebra *)
+
+ML_setup {* Delsimprocs [ring_simproc] *}
+
+lemma smult_assoc2:
+ "(a *s p) * q = (a::'a::ring) *s (p * q)"
+by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
+(* Simproc fails. *)
+
+ML_setup {* Addsimprocs [ring_simproc] *}
+
+(* the following can be derived from the above ones,
+ for generality reasons, it is therefore done *)
+
+lemma smult_l_null [simp]:
+ "(0::'a::ring) *s p = 0"
+proof -
+ fix a
+ have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
+ also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
+ also have "... = 0" by simp
+ finally show ?thesis .
+qed
+
+lemma smult_r_null [simp]:
+ "(a::'a::ring) *s 0 = 0";
+proof -
+ fix p
+ have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
+ also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
+ also have "... = 0" by simp
+ finally show ?thesis .
+qed
+
+lemma smult_l_minus:
+ "(-a::'a::ring) *s p = - (a *s p)"
+proof -
+ have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp
+ also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
+ also have "... = -(a *s p)" by simp
+ finally show ?thesis .
+qed
+
+lemma smult_r_minus:
+ "(a::'a::ring) *s (-p) = - (a *s p)"
+proof -
+ have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
+ also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
+ also have "... = -(a *s p)" by simp
+ finally show ?thesis .
+qed
+
+section {* The degree function *}
- 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_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
+constdefs
+ deg :: "('a::zero) up => nat"
+ "deg p == LEAST n. bound n (coeff p)"
+
+lemma deg_aboveI:
+ "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
+by (unfold deg_def) (fast intro: Least_le)
+
+lemma deg_aboveD:
+ assumes prem: "deg p < m" shows "coeff p m = 0"
+proof -
+ obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
+ then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
+ then show "coeff p m = 0" by (rule boundD)
+qed
+
+lemma deg_belowI:
+ assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
+(* logically, this is a slightly stronger version of deg_aboveD *)
+proof (cases "n=0")
+ case True then show ?thesis by simp
+next
+ case False then have "coeff p n ~= 0" by (rule prem)
+ then have "~ deg p < n" by (fast dest: deg_aboveD)
+ then show ?thesis by arith
+qed
+
+lemma lcoeff_nonzero_deg:
+ assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
+proof -
+ obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
+ proof -
+ have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
+ by arith (* make public?, why does proof not work with "1" *)
+ from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
+ by (unfold deg_def) arith
+ then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
+ then have "EX m. deg p - 1 < m & coeff p m ~= 0"
+ by (unfold bound_def) fast
+ then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
+ then show ?thesis by auto
+ qed
+ with deg_belowI have "deg p = m" by fastsimp
+ with m_coeff show ?thesis by simp
+qed
+
+lemma lcoeff_nonzero_nonzero:
+ assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
+proof -
+ have "EX m. coeff p m ~= 0"
+ proof (rule classical)
+ assume "~ ?thesis"
+ then have "p = 0" by (auto intro: up_eqI)
+ with nonzero show ?thesis by contradiction
+ qed
+ then obtain m where coeff: "coeff p m ~= 0" ..
+ then have "m <= deg p" by (rule deg_belowI)
+ then have "m = 0" by (simp add: deg)
+ with coeff show ?thesis by simp
+qed
+
+lemma lcoeff_nonzero:
+ "p ~= 0 ==> coeff p (deg p) ~= 0"
+proof (cases "deg p = 0")
+ case True
+ assume "p ~= 0"
+ with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
+next
+ case False
+ assume "p ~= 0"
+ with False show ?thesis by (simp add: lcoeff_nonzero_deg)
+qed
+
+lemma deg_eqI:
+ "[| !!m. n < m ==> coeff p m = 0;
+ !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
+by (fast intro: le_anti_sym deg_aboveI deg_belowI)
+
+(* Degree and polynomial operations *)
+
+lemma deg_add [simp]:
+ "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
+proof (cases "deg p <= deg q")
+ case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD)
+next
+ case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
+qed
+
+lemma deg_monom_ring:
+ "deg (monom a n::'a::ring up) <= n"
+by (rule deg_aboveI) simp
+
+lemma deg_monom [simp]:
+ "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
+by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
+
+lemma deg_const [simp]:
+ "deg (monom (a::'a::ring) 0) = 0"
+proof (rule le_anti_sym)
+ show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
+next
+ show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
+qed
+
+lemma deg_zero [simp]:
+ "deg 0 = 0"
+proof (rule le_anti_sym)
+ show "deg 0 <= 0" by (rule deg_aboveI) simp
+next
+ show "0 <= deg 0" by (rule deg_belowI) simp
+qed
+
+lemma deg_one [simp]:
+ "deg 1 = 0"
+proof (rule le_anti_sym)
+ show "deg 1 <= 0" by (rule deg_aboveI) simp
+next
+ show "0 <= deg 1" by (rule deg_belowI) simp
+qed
+
+lemma uminus_monom:
+ "!!a::'a::ring. (-a = 0) = (a = 0)"
+proof
+ fix a::"'a::ring"
+ assume "a = 0"
+ then show "-a = 0" by simp
+next
+ fix a::"'a::ring"
+ assume "- a = 0"
+ then have "-(- a) = 0" by simp
+ then show "a = 0" by simp
+qed
+
+lemma deg_uminus [simp]:
+ "deg (-p::('a::ring) up) = deg p"
+proof (rule le_anti_sym)
+ show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
+next
+ show "deg p <= deg (- p)"
+ by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
+qed
+
+lemma deg_smult_ring:
+ "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
+proof (cases "a = 0")
+qed (simp add: deg_aboveI deg_aboveD)+
+
+lemma deg_smult [simp]:
+ "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
+proof (rule le_anti_sym)
+ show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
+next
+ show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
+ proof (cases "a = 0")
+ qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
+qed
+lemma deg_mult_ring:
+ "deg (p * q::'a::ring up) <= deg p + deg q"
+proof (rule deg_aboveI)
+ fix m
+ assume boundm: "deg p + deg q < m"
+ {
+ fix k i
+ assume boundk: "deg p + deg q < k"
+ then have "coeff p i * coeff q (k - i) = 0"
+ proof (cases "deg p < i")
+ case True then show ?thesis by (simp add: deg_aboveD)
+ next
+ case False with boundk have "deg q < k - i" by arith
+ then show ?thesis by (simp add: deg_aboveD)
+ qed
+ }
+ (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
+ proofs. *)
+ with boundm show "coeff (p * q) m = 0" by simp
+qed
+lemma deg_mult [simp]:
+ "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
+proof (rule le_anti_sym)
+ show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
+next
+ let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
+ assume nz: "p ~= 0" "q ~= 0"
+ have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
+ show "deg p + deg q <= deg (p * q)"
+ proof (rule deg_belowI, simp)
+ have "setsum ?s {.. deg p + deg q}
+ = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
+ by (simp only: ivl_disj_un_one)
+ also have "... = setsum ?s {deg p .. deg p + deg q}"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_one
+ setsum_0 deg_aboveD less_add_diff)
+ also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
+ by (simp only: ivl_disj_un_singleton)
+ also have "... = coeff p (deg p) * coeff q (deg q)"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
+ setsum_0 deg_aboveD)
+ finally have "setsum ?s {.. deg p + deg q}
+ = coeff p (deg p) * coeff q (deg q)" .
+ with nz show "setsum ?s {.. deg p + deg q} ~= 0"
+ by (simp add: integral_iff lcoeff_nonzero)
+ qed
+ qed
+
+lemma coeff_natsum:
+ "((coeff (setsum p A) k)::'a::ring) =
+ setsum (%i. coeff (p i) k) A"
+proof (cases "finite A")
+ case True then show ?thesis by induct auto
+next
+ case False then show ?thesis by (simp add: setsum_def)
+qed
+(* Instance of a more general result!!! *)
+
+(*
+lemma coeff_natsum:
+ "((coeff (setsum p {..n::nat}) k)::'a::ring) =
+ setsum (%i. coeff (p i) k) {..n}"
+by (induct n) auto
+*)
+
+lemma up_repr:
+ "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
+proof (rule up_eqI)
+ let ?s = "(%i. monom (coeff p i) i)"
+ fix k
+ show "coeff (setsum ?s {..deg p}) k = coeff p k"
+ proof (cases "k <= deg p")
+ case True
+ hence "coeff (setsum ?s {..deg p}) k =
+ coeff (setsum ?s ({..k} Un {)k..deg p})) k"
+ by (simp only: ivl_disj_un_one)
+ also from True
+ have "... = coeff (setsum ?s {..k}) k"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
+ setsum_0 coeff_natsum )
+ also
+ have "... = coeff (setsum ?s ({..k(} Un {k})) k"
+ by (simp only: ivl_disj_un_singleton)
+ also have "... = coeff p k"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
+ setsum_0 coeff_natsum deg_aboveD)
+ finally show ?thesis .
+ next
+ case False
+ hence "coeff (setsum ?s {..deg p}) k =
+ coeff (setsum ?s ({..deg p(} Un {deg p})) k"
+ by (simp only: ivl_disj_un_singleton)
+ also from False have "... = coeff p k"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
+ setsum_0 coeff_natsum deg_aboveD)
+ finally show ?thesis .
+ qed
+qed
+
+lemma up_repr_le:
+ "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
+proof -
+ let ?s = "(%i. monom (coeff p i) i)"
+ assume "deg p <= n"
+ then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
+ by (simp only: ivl_disj_un_one)
+ also have "... = setsum ?s {..deg p}"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_one
+ setsum_0 deg_aboveD)
+ also have "... = p" by (rule up_repr)
+ finally show ?thesis .
+qed
+
+instance up :: ("domain") "domain"
+proof
+ show "1 ~= (0::'a up)"
+ proof (* notI is applied here *)
+ assume "1 = (0::'a up)"
+ hence "coeff 1 0 = (coeff 0 0::'a)" by simp
+ hence "1 = (0::'a)" by simp
+ with one_not_zero show "False" by contradiction
+ qed
+next
+ fix p q :: "'a::domain up"
+ assume pq: "p * q = 0"
+ show "p = 0 | q = 0"
+ proof (rule classical)
+ assume c: "~ (p = 0 | q = 0)"
+ then have "deg p + deg q = deg (p * q)" by simp
+ also from pq have "... = 0" by simp
+ finally have "deg p + deg q = 0" .
+ then have f1: "deg p = 0 & deg q = 0" by simp
+ from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
+ by (simp only: up_repr_le)
+ also have "... = monom (coeff p 0) 0" by simp
+ finally have p: "p = monom (coeff p 0) 0" .
+ from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
+ by (simp only: up_repr_le)
+ also have "... = monom (coeff q 0) 0" by simp
+ finally have q: "q = monom (coeff q 0) 0" .
+ have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
+ also from pq have "... = 0" by simp
+ finally have "coeff p 0 * coeff q 0 = 0" .
+ then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
+ with p q show "p = 0 | q = 0" by fastsimp
+ qed
+qed
+
+lemma monom_inj_zero:
+ "(monom a n = 0) = (a = 0)"
+proof -
+ have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
+ also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
+ finally show ?thesis .
+qed
+
+lemma smult_integral:
+ "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
+by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
+
+end
\ No newline at end of file
--- a/src/HOL/Finite_Set.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Finite_Set.thy Thu Nov 28 10:50:42 2002 +0100
@@ -273,6 +273,22 @@
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
by (induct k) (simp_all add: atMost_Suc)
+lemma finite_greaterThanLessThan [iff]:
+ fixes l :: nat shows "finite {)l..u(}"
+by (simp add: greaterThanLessThan_def)
+
+lemma finite_atLeastLessThan [iff]:
+ fixes l :: nat shows "finite {l..u(}"
+by (simp add: atLeastLessThan_def)
+
+lemma finite_greaterThanAtMost [iff]:
+ fixes l :: nat shows "finite {)l..u}"
+by (simp add: greaterThanAtMost_def)
+
+lemma finite_atLeastAtMost [iff]:
+ fixes l :: nat shows "finite {l..u}"
+by (simp add: atLeastAtMost_def)
+
lemma bounded_nat_set_is_finite:
"(ALL i:N. i < (n::nat)) ==> finite N"
-- {* A bounded set of natural numbers is finite. *}
--- a/src/HOL/IsaMakefile Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/IsaMakefile Thu Nov 28 10:50:42 2002 +0100
@@ -78,7 +78,8 @@
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
$(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
- $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
+ $(SRC)/Provers/splitter.ML $(SRC)/Provers/linorder.ML \
+ $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
$(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
$(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
@@ -341,16 +342,13 @@
Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
Algebra/abstract/Field.thy \
Algebra/abstract/Ideal.ML Algebra/abstract/Ideal.thy \
- Algebra/abstract/NatSum.ML Algebra/abstract/NatSum.thy \
Algebra/abstract/PID.thy \
Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \
Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
- Algebra/poly/Degree.ML Algebra/poly/Degree.thy \
+ Algebra/abstract/order.ML \
Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
- Algebra/poly/PolyRing.ML Algebra/poly/PolyRing.thy \
Algebra/poly/Polynomial.thy \
- Algebra/poly/ProtoPoly.ML Algebra/poly/ProtoPoly.thy \
Algebra/poly/UnivPoly.ML Algebra/poly/UnivPoly.thy
@$(ISATOOL) usedir $(OUT)/HOL Algebra
--- a/src/HOL/ROOT.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/ROOT.ML Thu Nov 28 10:50:42 2002 +0100
@@ -35,6 +35,7 @@
use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
use "~~/src/Provers/Arith/extract_common_term.ML";
use "~~/src/Provers/Arith/cancel_div_mod.ML";
+use "~~/src/Provers/linorder.ML";
with_path "Integ" use_thy "Main";
--- a/src/HOL/SetInterval.ML Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/SetInterval.ML Thu Nov 28 10:50:42 2002 +0100
@@ -1,137 +1,51 @@
(* Title: HOL/SetInterval.ML
ID: $Id$
- Author: Tobias Nipkow
- Copyright 2000 TU Muenchen
-
-Set Intervals: lessThan, greaterThan, atLeast, atMost
+ Author: Clemens Ballarin
+ Copyright 2002 TU Muenchen
*)
-
-(*** lessThan ***)
-
-Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
-by (Blast_tac 1);
-qed "lessThan_iff";
-AddIffs [lessThan_iff];
-
-Goalw [lessThan_def] "lessThan (0::nat) = {}";
-by (Simp_tac 1);
-qed "lessThan_0";
-Addsimps [lessThan_0];
-
-Goalw [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
-by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
-by (Blast_tac 1);
-qed "lessThan_Suc";
-
-Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
-by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
-qed "lessThan_Suc_atMost";
-
-Goal "(UN m::nat. lessThan m) = UNIV";
-by (Blast_tac 1);
-qed "UN_lessThan_UNIV";
-
-Goalw [lessThan_def, atLeast_def]
- "!!k:: 'a::linorder. -lessThan k = atLeast k";
-by Auto_tac;
-by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
-by (blast_tac (claset() addDs [order_le_less_trans]) 1);
-qed "Compl_lessThan";
-
-Goal "!!k:: 'a::order. {k} - lessThan k = {k}";
-by Auto_tac;
-qed "single_Diff_lessThan";
-Addsimps [single_Diff_lessThan];
-
-(*** greaterThan ***)
-
-Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
-by (Blast_tac 1);
-qed "greaterThan_iff";
-AddIffs [greaterThan_iff];
-
-Goalw [greaterThan_def] "greaterThan 0 = range Suc";
-by (blast_tac (claset() addDs [gr0_conv_Suc RS iffD1]) 1);
-qed "greaterThan_0";
-Addsimps [greaterThan_0];
-
-Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
-by (auto_tac (claset() addEs [linorder_neqE], simpset()));
-qed "greaterThan_Suc";
-
-Goal "(INT m::nat. greaterThan m) = {}";
-by (Blast_tac 1);
-qed "INT_greaterThan_UNIV";
-
-Goalw [greaterThan_def, atMost_def, le_def]
- "!!k:: 'a::linorder. -greaterThan k = atMost k";
-by Auto_tac;
-by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
-by (blast_tac (claset() addDs [order_le_less_trans]) 1);
-qed "Compl_greaterThan";
+(* Legacy ML bindings *)
-Goal "!!k:: 'a::linorder. -atMost k = greaterThan k";
-by (simp_tac (simpset() addsimps [Compl_greaterThan RS sym]) 1);
-qed "Compl_atMost";
-
-Addsimps [Compl_greaterThan, Compl_atMost];
-
-(*** atLeast ***)
-
-Goalw [atLeast_def] "(i: atLeast k) = (k<=i)";
-by (Blast_tac 1);
-qed "atLeast_iff";
-AddIffs [atLeast_iff];
-
-Goalw [atLeast_def, UNIV_def] "atLeast (0::nat) = UNIV";
-by (Simp_tac 1);
-qed "atLeast_0";
-Addsimps [atLeast_0];
-
-Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
-by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
-by (simp_tac (simpset() addsimps [order_le_less]) 1);
-by (Blast_tac 1);
-qed "atLeast_Suc";
-
-Goal "(UN m::nat. atLeast m) = UNIV";
-by (Blast_tac 1);
-qed "UN_atLeast_UNIV";
-
-Goalw [lessThan_def, atLeast_def, le_def]
- "!!k:: 'a::linorder. -atLeast k = lessThan k";
-by Auto_tac;
-by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
-by (blast_tac (claset() addDs [order_le_less_trans]) 1);
-qed "Compl_atLeast";
-
-Addsimps [Compl_lessThan, Compl_atLeast];
-
-(*** atMost ***)
-
-Goalw [atMost_def] "(i: atMost k) = (i<=k)";
-by (Blast_tac 1);
-qed "atMost_iff";
-AddIffs [atMost_iff];
-
-Goalw [atMost_def] "atMost (0::nat) = {0}";
-by (Simp_tac 1);
-qed "atMost_0";
-Addsimps [atMost_0];
-
-Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
-by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
-by (Blast_tac 1);
-qed "atMost_Suc";
-
-Goal "(UN m::nat. atMost m) = UNIV";
-by (Blast_tac 1);
-qed "UN_atMost_UNIV";
-
-
-(*** Combined properties ***)
-
-Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";
-by (blast_tac (claset() addIs [order_antisym]) 1);
-qed "atMost_Int_atLeast";
+val Compl_atLeast = thm "Compl_atLeast";
+val Compl_atMost = thm "Compl_atMost";
+val Compl_greaterThan = thm "Compl_greaterThan";
+val Compl_lessThan = thm "Compl_lessThan";
+val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV";
+val UN_atLeast_UNIV = thm "UN_atLeast_UNIV";
+val UN_atMost_UNIV = thm "UN_atMost_UNIV";
+val UN_lessThan_UNIV = thm "UN_lessThan_UNIV";
+val atLeastAtMost_def = thm "atLeastAtMost_def";
+val atLeastAtMost_iff = thm "atLeastAtMost_iff";
+val atLeastLessThan_def = thm "atLeastLessThan_def";
+val atLeastLessThan_iff = thm "atLeastLessThan_iff";
+val atLeast_0 = thm "atLeast_0";
+val atLeast_Suc = thm "atLeast_Suc";
+val atLeast_def = thm "atLeast_def";
+val atLeast_iff = thm "atLeast_iff";
+val atMost_0 = thm "atMost_0";
+val atMost_Int_atLeast = thm "atMost_Int_atLeast";
+val atMost_Suc = thm "atMost_Suc";
+val atMost_def = thm "atMost_def";
+val atMost_iff = thm "atMost_iff";
+val greaterThanAtMost_def = thm "greaterThanAtMost_def";
+val greaterThanAtMost_iff = thm "greaterThanAtMost_iff";
+val greaterThanLessThan_def = thm "greaterThanLessThan_def";
+val greaterThanLessThan_iff = thm "greaterThanLessThan_iff";
+val greaterThan_0 = thm "greaterThan_0";
+val greaterThan_Suc = thm "greaterThan_Suc";
+val greaterThan_def = thm "greaterThan_def";
+val greaterThan_iff = thm "greaterThan_iff";
+val ivl_disj_int = thms "ivl_disj_int";
+val ivl_disj_int_one = thms "ivl_disj_int_one";
+val ivl_disj_int_singleton = thms "ivl_disj_int_singleton";
+val ivl_disj_int_two = thms "ivl_disj_int_two";
+val ivl_disj_un = thms "ivl_disj_un";
+val ivl_disj_un_one = thms "ivl_disj_un_one";
+val ivl_disj_un_singleton = thms "ivl_disj_un_singleton";
+val ivl_disj_un_two = thms "ivl_disj_un_two";
+val lessThan_0 = thm "lessThan_0";
+val lessThan_Suc = thm "lessThan_Suc";
+val lessThan_Suc_atMost = thm "lessThan_Suc_atMost";
+val lessThan_def = thm "lessThan_def";
+val lessThan_iff = thm "lessThan_iff";
+val single_Diff_lessThan = thm "single_Diff_lessThan";
--- a/src/HOL/SetInterval.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/SetInterval.thy Thu Nov 28 10:50:42 2002 +0100
@@ -1,12 +1,12 @@
(* Title: HOL/SetInterval.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow and Clemens Ballarin
Copyright 2000 TU Muenchen
-lessThan, greaterThan, atLeast, atMost
+lessThan, greaterThan, atLeast, atMost and two-sided intervals
*)
-SetInterval = NatArith +
+theory SetInterval = NatArith:
constdefs
lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")
@@ -21,4 +21,320 @@
atLeast :: "('a::ord) => 'a set" ("(1{_..})")
"{l..} == {x. l<=x}"
+ greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})")
+ "{)l..u(} == {)l..} Int {..u(}"
+
+ atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})")
+ "{l..u(} == {l..} Int {..u(}"
+
+ greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{')_.._})")
+ "{)l..u} == {)l..} Int {..u}"
+
+ atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})")
+ "{l..u} == {l..} Int {..u}"
+
+(* Setup of transitivity reasoner *)
+
+ML {*
+
+structure Trans_Tac = Trans_Tac_Fun (
+ struct
+ val less_reflE = thm "order_less_irrefl" RS thm "notE";
+ val le_refl = thm "order_refl";
+ val less_imp_le = thm "order_less_imp_le";
+ val not_lessI = thm "linorder_not_less" RS thm "iffD2";
+ val not_leI = thm "linorder_not_less" RS thm "iffD2";
+ val not_lessD = thm "linorder_not_less" RS thm "iffD1";
+ val not_leD = thm "linorder_not_le" RS thm "iffD1";
+ val eqI = thm "order_antisym";
+ val eqD1 = thm "order_eq_refl";
+ val eqD2 = thm "sym" RS thm "order_eq_refl";
+ val less_trans = thm "order_less_trans";
+ val less_le_trans = thm "order_less_le_trans";
+ val le_less_trans = thm "order_le_less_trans";
+ val le_trans = thm "order_trans";
+ fun decomp (Trueprop $ t) =
+ let fun dec (Const ("Not", _) $ t) = (
+ case dec t of
+ None => None
+ | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
+ | dec (Const (rel, _) $ t1 $ t2) =
+ Some (t1, implode (drop (3, explode rel)), t2)
+ | dec _ = None
+ in dec t end
+ | decomp _ = None
+ end);
+
+val trans_tac = Trans_Tac.trans_tac;
+
+*}
+
+method_setup trans =
+ {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *}
+ {* simple transitivity reasoner *}
+
+(*** lessThan ***)
+
+lemma lessThan_iff: "(i: lessThan k) = (i<k)"
+
+apply (unfold lessThan_def)
+apply blast
+done
+declare lessThan_iff [iff]
+
+lemma lessThan_0: "lessThan (0::nat) = {}"
+apply (unfold lessThan_def)
+apply (simp (no_asm))
+done
+declare lessThan_0 [simp]
+
+lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
+apply (unfold lessThan_def)
+apply (simp (no_asm) add: less_Suc_eq)
+apply blast
+done
+
+lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
+apply (unfold lessThan_def atMost_def)
+apply (simp (no_asm) add: less_Suc_eq_le)
+done
+
+lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
+apply blast
+done
+
+lemma Compl_lessThan:
+ "!!k:: 'a::linorder. -lessThan k = atLeast k"
+apply (unfold lessThan_def atLeast_def)
+apply auto
+apply (blast intro: linorder_not_less [THEN iffD1])
+apply (blast dest: order_le_less_trans)
+done
+
+lemma single_Diff_lessThan: "!!k:: 'a::order. {k} - lessThan k = {k}"
+apply auto
+done
+declare single_Diff_lessThan [simp]
+
+(*** greaterThan ***)
+
+lemma greaterThan_iff: "(i: greaterThan k) = (k<i)"
+
+apply (unfold greaterThan_def)
+apply blast
+done
+declare greaterThan_iff [iff]
+
+lemma greaterThan_0: "greaterThan 0 = range Suc"
+apply (unfold greaterThan_def)
+apply (blast dest: gr0_conv_Suc [THEN iffD1])
+done
+declare greaterThan_0 [simp]
+
+lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
+apply (unfold greaterThan_def)
+apply (auto elim: linorder_neqE)
+done
+
+lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
+apply blast
+done
+
+lemma Compl_greaterThan:
+ "!!k:: 'a::linorder. -greaterThan k = atMost k"
+apply (unfold greaterThan_def atMost_def le_def)
+apply auto
+apply (blast intro: linorder_not_less [THEN iffD1])
+apply (blast dest: order_le_less_trans)
+done
+
+lemma Compl_atMost: "!!k:: 'a::linorder. -atMost k = greaterThan k"
+apply (simp (no_asm) add: Compl_greaterThan [symmetric])
+done
+
+declare Compl_greaterThan [simp] Compl_atMost [simp]
+
+(*** atLeast ***)
+
+lemma atLeast_iff: "(i: atLeast k) = (k<=i)"
+
+apply (unfold atLeast_def)
+apply blast
+done
+declare atLeast_iff [iff]
+
+lemma atLeast_0: "atLeast (0::nat) = UNIV"
+apply (unfold atLeast_def UNIV_def)
+apply (simp (no_asm))
+done
+declare atLeast_0 [simp]
+
+lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
+apply (unfold atLeast_def)
+apply (simp (no_asm) add: Suc_le_eq)
+apply (simp (no_asm) add: order_le_less)
+apply blast
+done
+
+lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
+apply blast
+done
+
+lemma Compl_atLeast:
+ "!!k:: 'a::linorder. -atLeast k = lessThan k"
+apply (unfold lessThan_def atLeast_def le_def)
+apply auto
+apply (blast intro: linorder_not_less [THEN iffD1])
+apply (blast dest: order_le_less_trans)
+done
+
+declare Compl_lessThan [simp] Compl_atLeast [simp]
+
+(*** atMost ***)
+
+lemma atMost_iff: "(i: atMost k) = (i<=k)"
+
+apply (unfold atMost_def)
+apply blast
+done
+declare atMost_iff [iff]
+
+lemma atMost_0: "atMost (0::nat) = {0}"
+apply (unfold atMost_def)
+apply (simp (no_asm))
+done
+declare atMost_0 [simp]
+
+lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
+apply (unfold atMost_def)
+apply (simp (no_asm) add: less_Suc_eq order_le_less)
+apply blast
+done
+
+lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
+apply blast
+done
+
+
+(*** Combined properties ***)
+
+lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
+apply (blast intro: order_antisym)
+done
+
+(*** Two-sided intervals ***)
+
+(* greaterThanLessThan *)
+
+lemma greaterThanLessThan_iff [simp]:
+ "(i : {)l..u(}) = (l < i & i < u)"
+by (simp add: greaterThanLessThan_def)
+
+(* atLeastLessThan *)
+
+lemma atLeastLessThan_iff [simp]:
+ "(i : {l..u(}) = (l <= i & i < u)"
+by (simp add: atLeastLessThan_def)
+
+(* greaterThanAtMost *)
+
+lemma greaterThanAtMost_iff [simp]:
+ "(i : {)l..u}) = (l < i & i <= u)"
+by (simp add: greaterThanAtMost_def)
+
+(* atLeastAtMost *)
+
+lemma atLeastAtMost_iff [simp]:
+ "(i : {l..u}) = (l <= i & i <= u)"
+by (simp add: atLeastAtMost_def)
+
+(* The above four lemmas could be declared as iffs.
+ If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
+ seems to take forever (more than one hour). *)
+
+(*** The following lemmas are useful with the summation operator setsum ***)
+(* For examples, see Algebra/poly/UnivPoly.thy *)
+
+(** Disjoint Unions **)
+
+(* Singletons and open intervals *)
+
+lemma ivl_disj_un_singleton:
+ "{l::'a::linorder} Un {)l..} = {l..}"
+ "{..u(} Un {u::'a::linorder} = {..u}"
+ "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
+ "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
+ "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
+ "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
+by auto (elim linorder_neqE | trans+)+
+
+(* One- and two-sided intervals *)
+
+lemma ivl_disj_un_one:
+ "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
+ "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
+ "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
+ "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
+ "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
+ "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
+ "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
+ "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
+by auto trans+
+
+(* Two- and two-sided intervals *)
+
+lemma ivl_disj_un_two:
+ "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
+ "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
+ "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
+ "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
+by auto trans+
+
+lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
+
+(** Disjoint Intersections **)
+
+(* Singletons and open intervals *)
+
+lemma ivl_disj_int_singleton:
+ "{l::'a::order} Int {)l..} = {}"
+ "{..u(} Int {u} = {}"
+ "{l} Int {)l..u(} = {}"
+ "{)l..u(} Int {u} = {}"
+ "{l} Int {)l..u} = {}"
+ "{l..u(} Int {u} = {}"
+ by simp+
+
+(* One- and two-sided intervals *)
+
+lemma ivl_disj_int_one:
+ "{..l::'a::order} Int {)l..u(} = {}"
+ "{..l(} Int {l..u(} = {}"
+ "{..l} Int {)l..u} = {}"
+ "{..l(} Int {l..u} = {}"
+ "{)l..u} Int {)u..} = {}"
+ "{)l..u(} Int {u..} = {}"
+ "{l..u} Int {)u..} = {}"
+ "{l..u(} Int {u..} = {}"
+ by auto trans+
+
+(* Two- and two-sided intervals *)
+
+lemma ivl_disj_int_two:
+ "{)l::'a::order..m(} Int {m..u(} = {}"
+ "{)l..m} Int {)m..u(} = {}"
+ "{l..m(} Int {m..u(} = {}"
+ "{l..m} Int {)m..u(} = {}"
+ "{)l..m(} Int {m..u} = {}"
+ "{)l..m} Int {)m..u} = {}"
+ "{l..m(} Int {m..u} = {}"
+ "{l..m} Int {)m..u} = {}"
+ by auto trans+
+
+lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
+
end
--- a/src/Provers/README Wed Nov 27 17:25:41 2002 +0100
+++ b/src/Provers/README Thu Nov 28 10:50:42 2002 +0100
@@ -16,6 +16,7 @@
simplifier.ML fast simplifier
split_paired_all.ML turn surjective pairing into split rule
splitter.ML performs case splits for simplifier.ML
+ trans.ML transitivity reasoner for linear (total) orders
typedsimp.ML basic simplifier for explicitly typed logics
directory Arith:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/linorder.ML Thu Nov 28 10:50:42 2002 +0100
@@ -0,0 +1,214 @@
+(*
+ Title: Transitivity reasoner for linear orders
+ Id: $Id$
+ Author: Clemens Ballarin, started 8 November 2002
+ Copyright: TU Muenchen
+*)
+
+(***
+This is a very simple package for transitivity reasoning over linear orders.
+Simple means exponential time (and space) in the number of premises.
+Should be replaced by a graph-theoretic algorithm.
+
+The package provides a tactic trans_tac that uses all premises of the form
+
+ t = u, t < u, t <= u, ~(t < u) and ~(t <= u)
+
+to
+1. either derive a contradiction,
+ in which case the conclusion can be any term,
+2. or prove the conclusion, which must be of the same form as the premises.
+
+To get rid of ~= in the premises, it is advisable to use an elimination
+rule of the form
+
+ [| t ~= u; t < u ==> P; u < t ==> P |] ==> P.
+
+The package is implemented as an ML functor and thus not limited to the
+relation <= and friends. It can be instantiated to any total order ---
+for example, the divisibility relation "dvd".
+***)
+
+(*** Credits ***
+
+This package is closely based on a (no longer used) transitivity reasoner for
+the natural numbers, which was written by Tobias Nipkow.
+
+****************)
+
+signature LESS_ARITH =
+sig
+ val less_reflE: thm (* x < x ==> P *)
+ val le_refl: thm (* x <= x *)
+ val less_imp_le: thm (* x <= y ==> x < y *)
+ val not_lessI: thm (* y <= x ==> ~(x < y) *)
+ val not_leI: thm (* y < x ==> ~(x <= y) *)
+ val not_lessD: thm (* ~(x < y) ==> y <= x *)
+ val not_leD: thm (* ~(x <= y) ==> y < x *)
+ val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
+ val eqD1: thm (* x = y ==> x <= y *)
+ val eqD2: thm (* x = y ==> y <= x *)
+ val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *)
+ val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *)
+ val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *)
+ val le_trans: thm (* [| x < y; y < z |] ==> x < z *)
+ val decomp: term -> (term * string * term) option
+ (* decomp (`x Rel y') should yield (x, Rel, y)
+ where Rel is one of "<", "<=", "~<", "~<=", "=" and "~="
+ other relation symbols are ignored *)
+end;
+
+signature TRANS_TAC =
+sig
+ val trans_tac: int -> tactic
+end;
+
+functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
+struct
+
+(*** Proof objects ***)
+
+datatype proof
+ = Asm of int
+ | Thm of proof list * thm;
+
+(* Turn proof objects into theorems *)
+
+fun prove asms =
+ let fun pr (Asm i) = nth_elem (i, asms)
+ | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
+ in pr end;
+
+(*** Exceptions ***)
+
+exception Contr of proof; (* Raised when contradiction is found *)
+
+exception Cannot; (* Raised when goal cannot be proved *)
+
+(*** Internal representation of inequalities ***)
+
+datatype less
+ = Less of term * term * proof
+ | Le of term * term * proof;
+
+fun lower (Less (x, _, _)) = x
+ | lower (Le (x, _, _)) = x;
+
+fun upper (Less (_, y, _)) = y
+ | upper (Le (_, y, _)) = y;
+
+infix subsumes;
+
+fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
+ | (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y')
+ | (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
+ | _ subsumes _ = false;
+
+fun trivial (Le (x, x', _)) = (x = x')
+ | trivial _ = false;
+
+(*** Transitive closure ***)
+
+fun add new =
+ let fun adds([], news) = new::news
+ | adds(old::olds, news) = if new subsumes old then adds(olds, news)
+ else adds(olds, old::news)
+ in adds end;
+
+fun ctest (less as Less (x, x', p)) =
+ if x = x' then raise Contr (Thm ([p], Less.less_reflE))
+ else less
+ | ctest less = less;
+
+fun mktrans (Less (x, _, p), Less (_, z, q)) =
+ Less (x, z, Thm([p, q], Less.less_trans))
+ | mktrans (Less (x, _, p), Le (_, z, q)) =
+ Less (x, z, Thm([p, q], Less.less_le_trans))
+ | mktrans (Le (x, _, p), Less (_, z, q)) =
+ Less (x, z, Thm([p, q], Less.le_less_trans))
+ | mktrans (Le (x, _, p), Le (_, z, q)) =
+ Le (x, z, Thm([p, q], Less.le_trans));
+
+fun trans new olds =
+ let fun tr (news, old) =
+ if upper old = lower new then mktrans (old, new)::news
+ else if upper new = lower old then mktrans (new, old)::news
+ else news
+ in foldl tr ([], olds) end;
+
+fun close1 olds new =
+ if trivial new orelse exists (fn old => old subsumes new) olds then olds
+ else let val news = trans new olds
+ in close (add new (olds, [])) news end
+and close olds [] = olds
+ | close olds (new::news) = close (close1 olds (ctest new)) news;
+
+(*** Solving and proving goals ***)
+
+(* Recognise and solve trivial goal *)
+
+fun triv_sol (Le (x, x', _)) =
+ if x = x' then Some (Thm ([], Less.le_refl))
+ else None
+ | triv_sol _ = None;
+
+(* Solve less starting from facts *)
+
+fun solve facts less =
+ case triv_sol less of
+ None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of
+ (None, _) => raise Cannot
+ | (Some (Less (_, _, p)), Less _) => p
+ | (Some (Le (_, _, p)), Less _) =>
+ error "trans_tac/solve: internal error: le cannot subsume less"
+ | (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le)
+ | (Some (Le (_, _, p)), Le _) => p)
+ | Some prf => prf;
+
+(* Turn term t into Less or Le; n is position of t in list of assumptions *)
+
+fun mkasm (t, n) =
+ case Less.decomp t of
+ Some (x, rel, y) => (case rel of
+ "<" => [Less (x, y, Asm n)]
+ | "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
+ | "<=" => [Le (x, y, Asm n)]
+ | "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))]
+ | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)),
+ Le (x, y, Thm ([Asm n], Less.eqD1))]
+ | "~=" => []
+ | _ => error ("trans_tac/mkasm: unknown relation " ^ rel))
+ | None => [];
+
+(* Turn goal t into a pair (goals, proof) where goals is a list of
+ Le/Less-subgoals to solve, and proof the validation that proves the concl t
+ Asm ~1 is dummy (denotes a goal)
+*)
+
+fun mkconcl t =
+ case Less.decomp t of
+ Some (x, rel, y) => (case rel of
+ "<" => ([Less (x, y, Asm ~1)], Asm 0)
+ | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
+ | "<=" => ([Le (x, y, Asm ~1)], Asm 0)
+ | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
+ | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
+ Thm ([Asm 0, Asm 1], Less.eqI))
+ | _ => raise Cannot)
+ | None => raise Cannot;
+
+val trans_tac = SUBGOAL (fn (A, n) =>
+ let val Hs = Logic.strip_assums_hyp A
+ val C = Logic.strip_assums_concl A
+ val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
+ val clesss = close [] lesss
+ val (subgoals, prf) = mkconcl C
+ val prfs = map (solve clesss) subgoals
+ in METAHYPS (fn asms =>
+ let val thms = map (prove asms) prfs
+ in rtac (prove thms prf) 1 end) n
+ end
+ handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
+ | Cannot => no_tac);
+
+end;