HOL-Algebra partially ported to Isar.
authorballarin
Thu Nov 28 10:50:42 2002 +0100 (2002-11-28)
changeset 137357de9342aca7a
parent 13734 50dcee1c509e
child 13736 6ea0e7c43c4f
HOL-Algebra partially ported to Isar.
NEWS
src/HOL/Algebra/abstract/Factor.ML
src/HOL/Algebra/abstract/Factor.thy
src/HOL/Algebra/abstract/Ideal.ML
src/HOL/Algebra/abstract/Ideal.thy
src/HOL/Algebra/abstract/NatSum.ML
src/HOL/Algebra/abstract/NatSum.thy
src/HOL/Algebra/abstract/Ring.ML
src/HOL/Algebra/abstract/Ring.thy
src/HOL/Algebra/abstract/RingHomo.ML
src/HOL/Algebra/abstract/RingHomo.thy
src/HOL/Algebra/abstract/order.ML
src/HOL/Algebra/poly/Degree.ML
src/HOL/Algebra/poly/Degree.thy
src/HOL/Algebra/poly/LongDiv.ML
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Algebra/poly/PolyHomo.ML
src/HOL/Algebra/poly/PolyHomo.thy
src/HOL/Algebra/poly/PolyRing.ML
src/HOL/Algebra/poly/PolyRing.thy
src/HOL/Algebra/poly/ProtoPoly.ML
src/HOL/Algebra/poly/ProtoPoly.thy
src/HOL/Algebra/poly/UnivPoly.ML
src/HOL/Algebra/poly/UnivPoly.thy
src/HOL/Finite_Set.thy
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/SetInterval.ML
src/HOL/SetInterval.thy
src/Provers/README
src/Provers/linorder.ML
     1.1 --- a/NEWS	Wed Nov 27 17:25:41 2002 +0100
     1.2 +++ b/NEWS	Thu Nov 28 10:50:42 2002 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Provers/linorder: New generic prover for transitivity reasoning over
     1.8 +linear orders.  Note: this prover is not efficient!
     1.9 +
    1.10  * Provers/simplifier:
    1.11  
    1.12    - Completely reimplemented Asm_full_simp_tac:
    1.13 @@ -87,6 +90,10 @@
    1.14  
    1.15  *** HOL ***
    1.16  
    1.17 +* New tactic "trans_tac" and method "trans" instantiate
    1.18 +Provers/linorder.ML for axclasses "order" and "linorder" (predicates
    1.19 +"<=", "<" and "="). 
    1.20 +
    1.21  * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 
    1.22  HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
    1.23  
     2.1 --- a/src/HOL/Algebra/abstract/Factor.ML	Wed Nov 27 17:25:41 2002 +0100
     2.2 +++ b/src/HOL/Algebra/abstract/Factor.ML	Thu Nov 28 10:50:42 2002 +0100
     2.3 @@ -4,29 +4,29 @@
     2.4      Author: Clemens Ballarin, started 25 November 1997
     2.5  *)
     2.6  
     2.7 -goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
     2.8 +Goalw [thm "assoc_def"] "!! c::'a::factorial. \
     2.9  \  [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b";
    2.10 -by (ftac factorial_prime 1);
    2.11 -by (rewrite_goals_tac [irred_def, prime_def]);
    2.12 +by (ftac (thm "factorial_prime") 1);
    2.13 +by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]);
    2.14  by (Blast_tac 1);
    2.15  qed "irred_dvd_lemma";
    2.16  
    2.17 -goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
    2.18 -\  [| irred c; a dvd <1> |] ==> \
    2.19 +Goalw [thm "assoc_def"] "!! c::'a::factorial. \
    2.20 +\  [| irred c; a dvd 1 |] ==> \
    2.21  \  (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
    2.22  \  (EX d. c assoc d & d : set factors)";
    2.23  by (induct_tac "factors" 1);
    2.24  (* Base case: c dvd a contradicts irred c *)
    2.25 -by (full_simp_tac (simpset() addsimps [irred_def]) 1);
    2.26 +by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
    2.27  by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
    2.28  (* Induction step *)
    2.29 -by (ftac factorial_prime 1);
    2.30 -by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1);
    2.31 +by (ftac (thm "factorial_prime") 1);
    2.32 +by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
    2.33  by (Blast_tac 1);
    2.34  qed "irred_dvd_list_lemma";
    2.35  
    2.36 -goal Ring.thy "!! c::'a::factorial. \
    2.37 -\  [| irred c; ALL b : set factors. irred b; a dvd <1>; \
    2.38 +Goal "!! c::'a::factorial. \
    2.39 +\  [| irred c; ALL b : set factors. irred b; a dvd 1; \
    2.40  \    c dvd foldr op* factors a |] ==> \
    2.41  \  EX d. c assoc d & d : set factors";
    2.42  by (rtac (irred_dvd_list_lemma RS mp) 1);
     3.1 --- a/src/HOL/Algebra/abstract/Factor.thy	Wed Nov 27 17:25:41 2002 +0100
     3.2 +++ b/src/HOL/Algebra/abstract/Factor.thy	Thu Nov 28 10:50:42 2002 +0100
     3.3 @@ -7,12 +7,12 @@
     3.4  Factor = Ring +
     3.5  
     3.6  consts
     3.7 -  Factorisation	:: ['a::ringS, 'a list, 'a] => bool
     3.8 +  Factorisation	:: ['a::ring, 'a list, 'a] => bool
     3.9    (* factorisation of x into a list of irred factors and a unit u *)
    3.10  
    3.11  defs
    3.12    Factorisation_def	"Factorisation x factors u == 
    3.13                             x = foldr op* factors u &
    3.14 -                           (ALL a : set factors. irred a) & u dvd <1>"
    3.15 +                           (ALL a : set factors. irred a) & u dvd 1"
    3.16  
    3.17  end
     4.1 --- a/src/HOL/Algebra/abstract/Ideal.ML	Wed Nov 27 17:25:41 2002 +0100
     4.2 +++ b/src/HOL/Algebra/abstract/Ideal.ML	Thu Nov 28 10:50:42 2002 +0100
     4.3 @@ -51,7 +51,11 @@
     4.4  
     4.5  Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}";
     4.6  by (rtac is_idealI 1);
     4.7 -by Auto_tac;
     4.8 +(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *)
     4.9 +by (Clarify_tac 1);
    4.10 +by (Clarify_tac 2);
    4.11 +by (Clarify_tac 3);
    4.12 +by (Clarify_tac 4);
    4.13  by (res_inst_tac [("x", "u+ua")] exI 1);
    4.14  by (res_inst_tac [("x", "v+va")] exI 1);
    4.15  by (res_inst_tac [("x", "-u")] exI 2);
    4.16 @@ -60,7 +64,7 @@
    4.17  by (res_inst_tac [("x", "0")] exI 3);
    4.18  by (res_inst_tac [("x", "u * r")] exI 4);
    4.19  by (res_inst_tac [("x", "v * r")] exI 4);
    4.20 -by (REPEAT (simp_tac (simpset() addsimps [r_distr, l_distr, r_minus, minus_add, m_assoc]@a_ac) 1));
    4.21 +by (REPEAT (Simp_tac 1));
    4.22  qed "is_ideal_2";
    4.23  
    4.24  (* ideal_of *)
    4.25 @@ -73,9 +77,10 @@
    4.26  by Auto_tac;
    4.27  qed "generator_in_ideal";
    4.28  
    4.29 -Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV";
    4.30 -by (force_tac (claset() addDs [is_ideal_mult], simpset()) 1);
    4.31 -  (* loops if is_ideal_mult is added as non-safe rule *)
    4.32 +Goalw [ideal_of_def] "ideal_of {1::'a::ring} = UNIV";
    4.33 +by (force_tac (claset() addDs [is_ideal_mult], 
    4.34 +  simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1);
    4.35 +  (* FIXME: Zumkeller's order raises Domain exn *)
    4.36  qed "ideal_of_one_eq";
    4.37  
    4.38  Goalw [ideal_of_def] "ideal_of {} = {0::'a::ring}";
    4.39 @@ -101,11 +106,13 @@
    4.40  by (rtac subsetI 1);
    4.41  by (dtac InterD 1);
    4.42  by (assume_tac 2);
    4.43 -by (auto_tac (claset() addIs [is_ideal_2], simpset()));
    4.44 -by (res_inst_tac [("x", "<1>")] exI 1);
    4.45 +by (auto_tac (claset() addIs [is_ideal_2],
    4.46 +  simpset() delsimprocs [ring_simproc]));
    4.47 +(* FIXME: Zumkeller's order *)
    4.48 +by (res_inst_tac [("x", "1")] exI 1);
    4.49  by (res_inst_tac [("x", "0")] exI 1);
    4.50  by (res_inst_tac [("x", "0")] exI 2);
    4.51 -by (res_inst_tac [("x", "<1>")] exI 2);
    4.52 +by (res_inst_tac [("x", "1")] exI 2);
    4.53  by (Simp_tac 1);
    4.54  by (Simp_tac 1);
    4.55  qed "ideal_of_2_structure";
    4.56 @@ -204,18 +211,18 @@
    4.57  by (rtac in_pideal_imp_dvd 1);
    4.58  by (Asm_simp_tac 1);
    4.59  by (res_inst_tac [("x", "0")] exI 1);
    4.60 -by (res_inst_tac [("x", "<1>")] exI 1);
    4.61 +by (res_inst_tac [("x", "1")] exI 1);
    4.62  by (Simp_tac 1);
    4.63  qed "not_dvd_psubideal";
    4.64  
    4.65 -Goalw [irred_def]
    4.66 +Goalw [thm "irred_def"]
    4.67    "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I";
    4.68  by (dtac is_pidealD 1);
    4.69  by (etac exE 1);
    4.70  by (Clarify_tac 1);
    4.71  by (eres_inst_tac [("x", "aa")] allE 1);
    4.72  by (Clarify_tac 1);
    4.73 -by (dres_inst_tac [("a", "<1>")] dvd_imp_subideal 1);
    4.74 +by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1);
    4.75  by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq]));
    4.76  qed "irred_imp_max_ideal";
    4.77  
    4.78 @@ -271,20 +278,21 @@
    4.79  
    4.80  (* Primeness condition *)
    4.81  
    4.82 -Goalw [prime_def] "irred a ==> prime (a::'a::pid)";
    4.83 +Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)";
    4.84  by (rtac conjI 1);
    4.85  by (rtac conjI 2);
    4.86  by (Clarify_tac 3);
    4.87 -by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "<1>")]
    4.88 +by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")]
    4.89    irred_imp_max_ideal 3);
    4.90  by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax],
    4.91 -  simpset() addsimps [irred_def, not_dvd_psubideal, pid_ax]));
    4.92 +  simpset() addsimps [thm "irred_def", not_dvd_psubideal, pid_ax]));
    4.93  by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
    4.94  by (Clarify_tac 1);
    4.95  by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
    4.96  by (full_simp_tac (simpset() addsimps [r_distr]) 1);
    4.97 -by (etac ssubst 1);
    4.98 -by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]) 1);
    4.99 +by (etac subst 1);
   4.100 +by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]
   4.101 +  delsimprocs [ring_simproc]) 1);
   4.102  qed "pid_irred_imp_prime";
   4.103  
   4.104  (* Fields are Pid *)
   4.105 @@ -294,7 +302,7 @@
   4.106  by (Simp_tac 1);
   4.107  by (rtac subset_trans 1);
   4.108  by (rtac dvd_imp_subideal 2);
   4.109 -by (rtac field_ax 2);
   4.110 +by (rtac (thm "field_ax") 2);
   4.111  by (assume_tac 2);
   4.112  by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
   4.113  qed "field_pideal_univ";
     5.1 --- a/src/HOL/Algebra/abstract/Ideal.thy	Wed Nov 27 17:25:41 2002 +0100
     5.2 +++ b/src/HOL/Algebra/abstract/Ideal.thy	Thu Nov 28 10:50:42 2002 +0100
     5.3 @@ -7,9 +7,9 @@
     5.4  Ideal = Ring +
     5.5  
     5.6  consts
     5.7 -  ideal_of	:: ('a::ringS) set => 'a set
     5.8 -  is_ideal	:: ('a::ringS) set => bool
     5.9 -  is_pideal	:: ('a::ringS) set => bool
    5.10 +  ideal_of	:: ('a::ring) set => 'a set
    5.11 +  is_ideal	:: ('a::ring) set => bool
    5.12 +  is_pideal	:: ('a::ring) set => bool
    5.13  
    5.14  defs
    5.15    is_ideal_def	"is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
     6.1 --- a/src/HOL/Algebra/abstract/NatSum.ML	Wed Nov 27 17:25:41 2002 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,215 +0,0 @@
     6.4 -(*
     6.5 -    Sums with naturals as index domain
     6.6 -    $Id$
     6.7 -    Author: Clemens Ballarin, started 12 December 1996
     6.8 -*)
     6.9 -
    6.10 -section "Basic Properties";
    6.11 -
    6.12 -Goal "setsum f {..0::nat} = (f 0::'a::ring)";
    6.13 -by (Asm_simp_tac 1);
    6.14 -qed "SUM_0";
    6.15 -
    6.16 -Goal "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::ring)";
    6.17 -by (simp_tac (simpset() addsimps [atMost_Suc]) 1);
    6.18 -qed "SUM_Suc";
    6.19 -
    6.20 -Addsimps [SUM_0, SUM_Suc];
    6.21 -
    6.22 -Goal
    6.23 -  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::ring)";
    6.24 -by (induct_tac "n" 1);
    6.25 -(* Base case *)
    6.26 -by (Simp_tac 1);
    6.27 -(* Induction step *)
    6.28 -by (asm_full_simp_tac (simpset() addsimps [a_assoc]) 1);
    6.29 -qed "SUM_Suc2";
    6.30 -
    6.31 -(* Congruence rules *)
    6.32 -
    6.33 -Goal "ALL j'::nat. j=j' --> (ALL i. i<=j' --> f i = (f' i :: 'a :: ring)) \
    6.34 -\     --> setsum f {..j} = setsum f' {..j'}";
    6.35 -by (induct_tac "j" 1);
    6.36 -by Auto_tac;  
    6.37 -bind_thm ("SUM_cong", (impI RS allI) RSN (2, result() RS spec RS mp RS mp));
    6.38 -Addcongs [SUM_cong];
    6.39 -
    6.40 -(* Results needed for the development of polynomials *)
    6.41 -
    6.42 -section "Ring Properties";
    6.43 -
    6.44 -Goal "setsum (%i. 0) {..n::nat} = (0::'a::ring)";
    6.45 -by (induct_tac "n" 1);
    6.46 -by (Simp_tac 1);
    6.47 -by (Asm_simp_tac 1);
    6.48 -qed "SUM_zero";
    6.49 -
    6.50 -Addsimps [SUM_zero];
    6.51 -
    6.52 -Goal
    6.53 -  "!!f::nat=>'a::ring. \
    6.54 -\  setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}";
    6.55 -by (induct_tac "n" 1);
    6.56 -(* Base case *)
    6.57 -by (Simp_tac 1);
    6.58 -(* Induction step *)
    6.59 -by (asm_simp_tac (simpset() addsimps a_ac) 1);
    6.60 -qed "SUM_add";
    6.61 -
    6.62 -Goal
    6.63 -  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}";
    6.64 -by (induct_tac "n" 1);
    6.65 -(* Base case *)
    6.66 -by (Simp_tac 1);
    6.67 -(* Induction step *)
    6.68 -by (asm_simp_tac (simpset() addsimps [l_distr]) 1);
    6.69 -qed "SUM_ldistr";
    6.70 -
    6.71 -Goal
    6.72 -  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}";
    6.73 -by (induct_tac "n" 1);
    6.74 -(* Base case *)
    6.75 -by (Simp_tac 1);
    6.76 -(* Induction step *)
    6.77 -by (asm_simp_tac (simpset() addsimps [r_distr]) 1);
    6.78 -qed "SUM_rdistr";
    6.79 -
    6.80 -section "Results for the Construction of Polynomials";
    6.81 -
    6.82 -Goal
    6.83 -  "!!a::nat=>'a::ring. k <= n --> \
    6.84 -\  setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = \
    6.85 -\  setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}";
    6.86 -by (induct_tac "k" 1);
    6.87 -(* Base case *)
    6.88 -by (simp_tac (simpset() addsimps [m_assoc]) 1);
    6.89 -(* Induction step *)
    6.90 -by (rtac impI 1);
    6.91 -by (etac impE 1);
    6.92 -by (arith_tac 1);
    6.93 -by (asm_simp_tac
    6.94 -    (simpset() addsimps a_ac@
    6.95 -                        [Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1);
    6.96 -by (asm_simp_tac (simpset() addsimps a_ac@ [SUM_ldistr, m_assoc]) 1);
    6.97 -qed_spec_mp "poly_assoc_lemma1";
    6.98 -
    6.99 -Goal
   6.100 -  "!!a::nat=>'a::ring. \
   6.101 -\  setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..n} = \
   6.102 -\  setsum (%j. a j * setsum (%i. b i * c (n-(j+i))) {..n-j}) {..n}";
   6.103 -by (asm_simp_tac (simpset() addsimps [poly_assoc_lemma1]) 1);
   6.104 -qed "poly_assoc_lemma";
   6.105 -
   6.106 -Goal
   6.107 -  "!! a::nat=>'a::ring. j <= n --> \
   6.108 -\    setsum (%i. a i * b (n-i)) {..j} = \
   6.109 -\    setsum (%i. a (n-i-(n-j)) * b (i+(n-j))) {..j}";
   6.110 -by (Simp_tac 1); 
   6.111 -by (induct_tac "j" 1);
   6.112 -(* Base case *)
   6.113 -by (Simp_tac 1);
   6.114 -(* Induction step *)
   6.115 -by (stac SUM_Suc2 1);
   6.116 -by (asm_simp_tac (simpset() addsimps [a_comm]) 1);
   6.117 -qed "poly_comm_lemma1";
   6.118 -
   6.119 -Goal
   6.120 - "!!a::nat=>'a::ring. \
   6.121 -\   setsum (%i. a i * b (n-i)) {..n} = \
   6.122 -\   setsum (%i. a (n-i) * b i) {..n}";
   6.123 -by (cut_inst_tac [("j", "n"), ("n", "n")] poly_comm_lemma1 1);
   6.124 -by (Asm_full_simp_tac 1);
   6.125 -qed "poly_comm_lemma";
   6.126 -
   6.127 -section "Changing the Range of Summation";
   6.128 -
   6.129 -Goal
   6.130 -  "!! f::(nat=>'a::ring). \
   6.131 -\   setsum (%i. if i = x then f i else 0) {..n} = (if x <= n then f x else 0)";
   6.132 -by (induct_tac "n" 1);
   6.133 -(* Base case *)
   6.134 -by (Simp_tac 1);
   6.135 -(* Induction step *)
   6.136 -by (Asm_simp_tac 1);
   6.137 -by (Clarify_tac 1);
   6.138 -by (res_inst_tac [("f", "f")] arg_cong 1);
   6.139 -by (arith_tac 1);
   6.140 -qed "SUM_if_singleton";
   6.141 -
   6.142 -Goal
   6.143 -  "!! f::(nat=>'a::ring). \
   6.144 -\    m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \
   6.145 -\    setsum f {..m} = setsum f {..n}";
   6.146 -by (induct_tac "n" 1);
   6.147 -(* Base case *)
   6.148 -by (Simp_tac 1);
   6.149 -(* Induction step *)
   6.150 -by (case_tac "m <= n" 1);
   6.151 -by Auto_tac;
   6.152 -by (subgoal_tac "m = Suc n" 1);
   6.153 -by (Asm_simp_tac 1);
   6.154 -by (fast_arith_tac 1);
   6.155 -val SUM_shrink_lemma = result();
   6.156 -
   6.157 -Goal
   6.158 -  "!! f::(nat=>'a::ring). \
   6.159 -\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \
   6.160 -\  ==> P (setsum f {..m})";
   6.161 -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
   6.162 -by (Asm_full_simp_tac 1);
   6.163 -qed "SUM_shrink";
   6.164 -
   6.165 -Goal
   6.166 -  "!! f::(nat=>'a::ring). \
   6.167 -\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \
   6.168 -\    ==> P (setsum f {..n})";
   6.169 -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
   6.170 -by (Asm_full_simp_tac 1);
   6.171 -qed "SUM_extend";
   6.172 -
   6.173 -Goal
   6.174 -  "!! f::(nat=>'a::ring). \
   6.175 -\    (ALL i. i < m --> f i = 0) --> \
   6.176 -\      setsum (%i. f (i+m)) {..d} = setsum f {..m+d}";
   6.177 -by (induct_tac "d" 1);
   6.178 -(* Base case *)
   6.179 -by (induct_tac "m" 1);
   6.180 -by (Simp_tac 1);
   6.181 -by (Force_tac 1);
   6.182 -(* Induction step *)
   6.183 -by (asm_simp_tac (simpset() addsimps add_ac) 1);
   6.184 -val SUM_shrink_below_lemma = result();
   6.185 -
   6.186 -Goal
   6.187 -  "!! f::(nat=>'a::ring). \
   6.188 -\    [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
   6.189 -\    ==> P (setsum f {..n})";
   6.190 -by (asm_full_simp_tac 
   6.191 -    (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
   6.192 -qed "SUM_extend_below";
   6.193 -
   6.194 -section "Result for the Univeral Property of Polynomials";
   6.195 -
   6.196 -Goal
   6.197 -  "!!f::nat=>'a::ring. j <= n + m --> \
   6.198 -\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \
   6.199 -\    setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}";
   6.200 -by (induct_tac "j" 1);
   6.201 -(* Base case *)
   6.202 -by (Simp_tac 1);
   6.203 -(* Induction step *)
   6.204 -by (simp_tac (simpset() addsimps [Suc_diff_le, SUM_add]) 1);
   6.205 -by (asm_simp_tac (simpset() addsimps a_ac) 1);
   6.206 -val DiagSum_lemma = result();
   6.207 -
   6.208 -Goal
   6.209 -  "!!f::nat=>'a::ring. \
   6.210 -\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \
   6.211 -\    setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}";
   6.212 -by (rtac (DiagSum_lemma RS mp) 1);
   6.213 -by (rtac le_refl 1);
   6.214 -qed "DiagSum";
   6.215 -
   6.216 -
   6.217 -
   6.218 -
     7.1 --- a/src/HOL/Algebra/abstract/NatSum.thy	Wed Nov 27 17:25:41 2002 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,12 +0,0 @@
     7.4 -(*
     7.5 -    Sums with naturals as index domain
     7.6 -    $Id$
     7.7 -    Author: Clemens Ballarin, started 12 December 1996
     7.8 -*)
     7.9 -
    7.10 -NatSum = Ring +
    7.11 -
    7.12 -instance
    7.13 -  ring < plus_ac0 (a_assoc, a_comm, l_zero)
    7.14 -
    7.15 -end
     8.1 --- a/src/HOL/Algebra/abstract/Ring.ML	Wed Nov 27 17:25:41 2002 +0100
     8.2 +++ b/src/HOL/Algebra/abstract/Ring.ML	Thu Nov 28 10:50:42 2002 +0100
     8.3 @@ -4,6 +4,7 @@
     8.4      Author: Clemens Ballarin, started 9 December 1996
     8.5  *)
     8.6  
     8.7 +(*
     8.8  val a_assoc = thm "plus_ac0.assoc";
     8.9  val l_zero = thm "plus_ac0.zero";
    8.10  val a_comm = thm "plus_ac0.commute";
    8.11 @@ -78,7 +79,7 @@
    8.12  
    8.13  val m_ac = [m_assoc, m_comm, m_lcomm];
    8.14  
    8.15 -Goal "!!a::'a::ring. a * <1> = a";
    8.16 +Goal "!!a::'a::ring. a * 1 = a";
    8.17  by (rtac (m_comm RS trans) 1);
    8.18  by (rtac l_one 1);
    8.19  qed "r_one";
    8.20 @@ -161,19 +162,21 @@
    8.21  Goal "!!a::'a::ring. (a = b) = (a -- b = 0)";
    8.22  *)
    8.23  
    8.24 +*)
    8.25 +
    8.26  (* Power *)
    8.27  
    8.28 -Goal "!!a::'a::ring. a ^ 0 = <1>";
    8.29 -by (simp_tac (simpset() addsimps [power_ax]) 1);
    8.30 +Goal "!!a::'a::ring. a ^ 0 = 1";
    8.31 +by (simp_tac (simpset() addsimps [power_def]) 1);
    8.32  qed "power_0";
    8.33  
    8.34  Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
    8.35 -by (simp_tac (simpset() addsimps [power_ax]) 1);
    8.36 +by (simp_tac (simpset() addsimps [power_def]) 1);
    8.37  qed "power_Suc";
    8.38  
    8.39  Addsimps [power_0, power_Suc];
    8.40  
    8.41 -Goal "<1> ^ n = (<1>::'a::ring)";
    8.42 +Goal "1 ^ n = (1::'a::ring)";
    8.43  by (induct_tac "n" 1);
    8.44  by Auto_tac;
    8.45  qed "power_one";
    8.46 @@ -189,7 +192,7 @@
    8.47  Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
    8.48  by (induct_tac "m" 1);
    8.49  by (Simp_tac 1);
    8.50 -by (asm_simp_tac (simpset() addsimps m_ac) 1);
    8.51 +by (Asm_simp_tac 1);
    8.52  qed "power_mult";
    8.53  
    8.54  (* Divisibility *)
    8.55 @@ -205,26 +208,26 @@
    8.56  qed "dvd_zero_left";
    8.57  
    8.58  Goalw [dvd_def] "!! a::'a::ring. a dvd a";
    8.59 -by (res_inst_tac [("x", "<1>")] exI 1);
    8.60 +by (res_inst_tac [("x", "1")] exI 1);
    8.61  by (Simp_tac 1);
    8.62  qed "dvd_refl_ring";
    8.63  
    8.64  Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
    8.65  by (Step_tac 1);
    8.66  by (res_inst_tac [("x", "k * ka")] exI 1);
    8.67 -by (simp_tac (simpset() addsimps m_ac) 1);
    8.68 +by (Asm_simp_tac 1);
    8.69  qed "dvd_trans_ring";
    8.70  
    8.71  Addsimps [dvd_zero_right, dvd_refl_ring];
    8.72  
    8.73  Goalw [dvd_def]
    8.74 -  "!!a::'a::ring. [| a dvd <1>; b dvd <1> |] ==> a * b dvd <1>";
    8.75 +  "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1";
    8.76  by (Clarify_tac 1);
    8.77  by (res_inst_tac [("x", "k * ka")] exI 1);
    8.78 -by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
    8.79 +by (Asm_full_simp_tac 1);
    8.80  qed "unit_mult";
    8.81  
    8.82 -Goal "!!a::'a::ring. a dvd <1> ==> a^n dvd <1>";
    8.83 +Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1";
    8.84  by (induct_tac "n" 1);
    8.85  by (Simp_tac 1);
    8.86  by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);
    8.87 @@ -248,14 +251,14 @@
    8.88    "!! a::'a::ring. a dvd b ==> a dvd c*b";
    8.89  by (Clarify_tac 1);
    8.90  by (res_inst_tac [("x", "c * k")] exI 1);
    8.91 -by (simp_tac (simpset() addsimps m_ac) 1);
    8.92 +by (Simp_tac 1);
    8.93  qed "dvd_l_mult_right";
    8.94  
    8.95  Goalw [dvd_def]
    8.96    "!! a::'a::ring. a dvd b ==> a dvd b*c";
    8.97  by (Clarify_tac 1);
    8.98  by (res_inst_tac [("x", "k * c")] exI 1);
    8.99 -by (simp_tac (simpset() addsimps m_ac) 1);
   8.100 +by (Simp_tac 1);
   8.101  qed "dvd_r_mult_right";
   8.102  
   8.103  Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];
   8.104 @@ -264,34 +267,37 @@
   8.105  
   8.106  section "inverse";
   8.107  
   8.108 -Goal "!! a::'a::ring. [| a * x = <1>; a * y = <1> |] ==> x = y";
   8.109 +Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y";
   8.110  by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);
   8.111 -by (simp_tac (simpset() addsimps m_ac) 1);
   8.112 +by (Simp_tac 1);
   8.113  by Auto_tac;
   8.114  qed "inverse_unique";
   8.115  
   8.116 -Goal "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
   8.117 -by (asm_full_simp_tac (simpset () addsimps [inverse_ax, dvd_def]) 1);
   8.118 +Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1";
   8.119 +by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def]) 1);
   8.120  by (Clarify_tac 1);
   8.121 -by (rtac someI 1);
   8.122 -by (rtac sym 1);
   8.123 -by (assume_tac 1);
   8.124 +by (rtac theI 1);
   8.125 +by (atac 1);
   8.126 +by (rtac inverse_unique 1);
   8.127 +by (atac 1);
   8.128 +by (atac 1);
   8.129  qed "r_inverse_ring";
   8.130  
   8.131 -Goal "!! a::'a::ring. a dvd <1> ==> inverse a * a= <1>";
   8.132 -by (asm_simp_tac (simpset() addsimps r_inverse_ring::m_ac) 1);
   8.133 +Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1";
   8.134 +by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
   8.135  qed "l_inverse_ring";
   8.136  
   8.137  (* Integral domain *)
   8.138  
   8.139 +(*
   8.140  section "Integral domains";
   8.141  
   8.142 -Goal "0 ~= (<1>::'a::domain)";
   8.143 +Goal "0 ~= (1::'a::domain)";
   8.144  by (rtac not_sym 1);
   8.145  by (rtac one_not_zero 1);
   8.146  qed "zero_not_one";
   8.147  
   8.148 -Goal "!! a::'a::domain. a dvd <1> ==> a ~= 0";
   8.149 +Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0";
   8.150  by (auto_tac (claset() addDs [dvd_zero_left],
   8.151    simpset() addsimps [one_not_zero] ));
   8.152  qed "unit_imp_nonzero";
   8.153 @@ -312,16 +318,16 @@
   8.154  
   8.155  Addsimps [not_integral, one_not_zero, zero_not_one];
   8.156  
   8.157 -Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = <1>";
   8.158 -by (res_inst_tac [("a", "- <1>")] a_lcancel 1);
   8.159 +Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1";
   8.160 +by (res_inst_tac [("a", "- 1")] a_lcancel 1);
   8.161  by (Simp_tac 1);
   8.162  by (rtac l_integral 1);
   8.163  by (assume_tac 2);
   8.164  by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);
   8.165  qed "l_one_integral";
   8.166  
   8.167 -Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = <1>";
   8.168 -by (res_inst_tac [("a", "- <1>")] a_rcancel 1);
   8.169 +Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1";
   8.170 +by (res_inst_tac [("a", "- 1")] a_rcancel 1);
   8.171  by (Simp_tac 1);
   8.172  by (rtac r_integral 1);
   8.173  by (assume_tac 2);
   8.174 @@ -340,7 +346,7 @@
   8.175  Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c";
   8.176  by (rtac m_lcancel 1);
   8.177  by (assume_tac 1);
   8.178 -by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
   8.179 +by (Asm_full_simp_tac 1);
   8.180  qed "m_rcancel";
   8.181  
   8.182  Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)";
   8.183 @@ -352,23 +358,28 @@
   8.184  qed "m_rcancel_eq";
   8.185  
   8.186  Addsimps [m_lcancel_eq, m_rcancel_eq];
   8.187 +*)
   8.188  
   8.189  (* Fields *)
   8.190  
   8.191  section "Fields";
   8.192  
   8.193 -Goal "!! a::'a::field. (a dvd <1>) = (a ~= 0)";
   8.194 -by (auto_tac (claset() addDs [field_ax, dvd_zero_left],
   8.195 -  simpset() addsimps [field_one_not_zero]));
   8.196 +Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)";
   8.197 +by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left],
   8.198 +  simpset() addsimps [thm "field_one_not_zero"]));
   8.199  qed "field_unit";
   8.200  
   8.201 +(* required for instantiation of field < domain in file Field.thy *)
   8.202 +
   8.203  Addsimps [field_unit];
   8.204  
   8.205 -Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = <1>";
   8.206 +val field_one_not_zero = thm "field_one_not_zero";
   8.207 +
   8.208 +Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1";
   8.209  by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
   8.210  qed "r_inverse";
   8.211  
   8.212 -Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= <1>";
   8.213 +Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1";
   8.214  by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);
   8.215  qed "l_inverse";
   8.216  
   8.217 @@ -380,12 +391,13 @@
   8.218  by (Step_tac 1);
   8.219  by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
   8.220  by (rtac refl 3);
   8.221 -by (simp_tac (simpset() addsimps m_ac) 2);
   8.222 +by (Simp_tac 2);
   8.223  by Auto_tac;
   8.224  qed "field_integral";
   8.225  
   8.226  (* fields are factorial domains *)
   8.227  
   8.228 -Goalw [prime_def, irred_def] "!! a::'a::field. irred a ==> prime a";
   8.229 -by (blast_tac (claset() addIs [field_ax]) 1);
   8.230 +Goalw [thm "prime_def", thm "irred_def"]
   8.231 +  "!! a::'a::field. irred a ==> prime a";
   8.232 +by (blast_tac (claset() addIs [thm "field_ax"]) 1);
   8.233  qed "field_fact_prime";
     9.1 --- a/src/HOL/Algebra/abstract/Ring.thy	Wed Nov 27 17:25:41 2002 +0100
     9.2 +++ b/src/HOL/Algebra/abstract/Ring.thy	Thu Nov 28 10:50:42 2002 +0100
     9.3 @@ -1,89 +1,86 @@
     9.4  (*
     9.5 -    Abstract class ring (commutative, with 1)
     9.6 -    $Id$
     9.7 -    Author: Clemens Ballarin, started 9 December 1996
     9.8 +  Title:     The algebraic hierarchy of rings as axiomatic classes
     9.9 +  Id:        $Id$
    9.10 +  Author:    Clemens Ballarin, started 9 December 1996
    9.11 +  Copyright: Clemens Ballarin
    9.12  *)
    9.13  
    9.14 -Ring = Main +
    9.15 +header {* The algebraic hierarchy of rings as axiomatic classes *}
    9.16  
    9.17 -(* Syntactic class ring *)
    9.18 +theory Ring = Main
    9.19 +files ("order.ML"):
    9.20  
    9.21 -axclass
    9.22 -  ringS < zero, plus, minus, times, power, inverse
    9.23 +section {* Constants *}
    9.24 +
    9.25 +text {* Most constants are already declared by HOL. *}
    9.26  
    9.27  consts
    9.28 -  (* Basic rings *)
    9.29 -  "<1>"		:: 'a::ringS				("<1>")
    9.30 -  "--"		:: ['a, 'a] => 'a::ringS		(infixl 65)
    9.31 +  assoc         :: "['a::times, 'a] => bool"              (infixl 50)
    9.32 +  irred         :: "'a::{zero, one, times} => bool"
    9.33 +  prime         :: "'a::{zero, one, times} => bool"
    9.34 +
    9.35 +section {* Axioms *}
    9.36 +
    9.37 +subsection {* Ring axioms *}
    9.38 +
    9.39 +axclass ring < zero, one, plus, minus, times, inverse, power
    9.40 +
    9.41 +  a_assoc:      "(a + b) + c = a + (b + c)"
    9.42 +  l_zero:       "0 + a = a"
    9.43 +  l_neg:        "(-a) + a = 0"
    9.44 +  a_comm:       "a + b = b + a"
    9.45 +
    9.46 +  m_assoc:      "(a * b) * c = a * (b * c)"
    9.47 +  l_one:        "1 * a = a"
    9.48  
    9.49 -  (* Divisibility *)
    9.50 -  assoc		:: ['a::times, 'a] => bool		(infixl 50)
    9.51 -  irred		:: 'a::ringS => bool
    9.52 -  prime		:: 'a::ringS => bool
    9.53 +  l_distr:      "(a + b) * c = a * c + b * c"
    9.54 +
    9.55 +  m_comm:       "a * b = b * a"
    9.56 +
    9.57 +  -- {* Definition of derived operations *}
    9.58  
    9.59 -translations
    9.60 -  "a -- b" 	== "a + (-b)"
    9.61 +  minus_def:    "a - b = a + (-b)"
    9.62 +  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
    9.63 +  divide_def:   "a / b = a * inverse b"
    9.64 +  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
    9.65  
    9.66 -(* Class ring and ring axioms *)
    9.67 +defs
    9.68 +  assoc_def:    "a assoc b == a dvd b & b dvd a"
    9.69 +  irred_def:    "irred a == a ~= 0 & ~ a dvd 1
    9.70 +                          & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
    9.71 +  prime_def:    "prime p == p ~= 0 & ~ p dvd 1
    9.72 +                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
    9.73 +
    9.74 +subsection {* Integral domains *}
    9.75  
    9.76  axclass
    9.77 -  ring < ringS, plus_ac0
    9.78 -
    9.79 -(*a_assoc	"(a + b) + c = a + (b + c)"*)
    9.80 -(*l_zero	"0 + a = a"*)
    9.81 -  l_neg		"(-a) + a = 0"
    9.82 -(*a_comm	"a + b = b + a"*)
    9.83 -
    9.84 -  m_assoc	"(a * b) * c = a * (b * c)"
    9.85 -  l_one		"<1> * a = a"
    9.86 -
    9.87 -  l_distr	"(a + b) * c = a * c + b * c"
    9.88 -
    9.89 -  m_comm	"a * b = b * a"
    9.90 +  "domain" < ring
    9.91  
    9.92 -  (* Definition of derived operations *)
    9.93 -
    9.94 -  inverse_ax    "inverse a = (if a dvd <1> then @x. a*x = <1> else 0)"
    9.95 -  divide_ax     "a / b = a * inverse b"
    9.96 -  power_ax	"a ^ n = nat_rec <1> (%u b. b * a) n"
    9.97 +  one_not_zero: "1 ~= 0"
    9.98 +  integral:     "a * b = 0 ==> a = 0 | b = 0"
    9.99  
   9.100 -defs
   9.101 -  assoc_def	"a assoc b == a dvd b & b dvd a"
   9.102 -  irred_def	"irred a == a ~= 0 & ~ a dvd <1>
   9.103 -                          & (ALL d. d dvd a --> d dvd <1> | a dvd d)"
   9.104 -  prime_def	"prime p == p ~= 0 & ~ p dvd <1>
   9.105 -                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
   9.106 -
   9.107 -(* Integral domains *)
   9.108 +subsection {* Factorial domains *}
   9.109  
   9.110  axclass
   9.111 -  domain < ring
   9.112 -
   9.113 -  one_not_zero	"<1> ~= 0"
   9.114 -  integral	"a * b = 0 ==> a = 0 | b = 0"
   9.115 -
   9.116 -(* Factorial domains *)
   9.117 -
   9.118 -axclass
   9.119 -  factorial < domain
   9.120 +  factorial < "domain"
   9.121  
   9.122  (*
   9.123    Proper definition using divisor chain condition currently not supported.
   9.124 -  factorial_divisor	"wf {(a, b). a dvd b & ~ (b dvd a)}"
   9.125 +  factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
   9.126  *)
   9.127 -  factorial_divisor	"True"
   9.128 -  factorial_prime	"irred a ==> prime a"
   9.129 +  factorial_divisor:	"True"
   9.130 +  factorial_prime:      "irred a ==> prime a"
   9.131  
   9.132 -(* Euclidean domains *)
   9.133 +subsection {* Euclidean domains *}
   9.134  
   9.135  (*
   9.136  axclass
   9.137 -  euclidean < domain
   9.138 +  euclidean < "domain"
   9.139  
   9.140 -  euclidean_ax	"b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
   9.141 +  euclidean_ax:  "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
   9.142                     a = b * q + r & e_size r < e_size b)"
   9.143  
   9.144 -  Nothing has been proved about euclidean domains, yet.
   9.145 +  Nothing has been proved about Euclidean domains, yet.
   9.146    Design question:
   9.147      Fix quo, rem and e_size as constants that are axiomatised with
   9.148      euclidean_ax?
   9.149 @@ -95,14 +92,147 @@
   9.150          definitions of quo and rem.
   9.151  *)
   9.152  
   9.153 -(* Fields *)
   9.154 +subsection {* Fields *}
   9.155  
   9.156  axclass
   9.157    field < ring
   9.158  
   9.159 -  field_one_not_zero	"<1> ~= 0"
   9.160 -		(* Avoid a common superclass as the first thing we will
   9.161 -		   prove about fields is that they are domains. *)
   9.162 -  field_ax	"a ~= 0 ==> a dvd <1>"
   9.163 +  field_one_not_zero:    "1 ~= 0"
   9.164 +                (* Avoid a common superclass as the first thing we will
   9.165 +                   prove about fields is that they are domains. *)
   9.166 +  field_ax:        "a ~= 0 ==> a dvd 1"
   9.167 +
   9.168 +section {* Basic facts *}
   9.169 +
   9.170 +subsection {* Normaliser for rings *}
   9.171 +
   9.172 +use "order.ML"
   9.173 +
   9.174 +method_setup ring =
   9.175 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
   9.176 +  {* computes distributive normal form in rings *}
   9.177 +
   9.178 +
   9.179 +subsection {* Rings and the summation operator *}
   9.180 +
   9.181 +(* Basic facts --- move to HOL!!! *)
   9.182 +
   9.183 +lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
   9.184 +by simp
   9.185 +
   9.186 +lemma natsum_Suc [simp]:
   9.187 +  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
   9.188 +by (simp add: atMost_Suc)
   9.189 +
   9.190 +lemma natsum_Suc2:
   9.191 +  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
   9.192 +proof (induct n)
   9.193 +  case 0 show ?case by simp
   9.194 +next
   9.195 +  case Suc thus ?case by (simp add: assoc) 
   9.196 +qed
   9.197 +
   9.198 +lemma natsum_cong [cong]:
   9.199 +  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
   9.200 +        setsum f {..j} = setsum g {..k}"
   9.201 +by (induct j) auto
   9.202 +
   9.203 +lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
   9.204 +by (induct n) simp_all
   9.205 +
   9.206 +lemma natsum_add [simp]:
   9.207 +  "!!f::nat=>'a::plus_ac0.
   9.208 +   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
   9.209 +by (induct n) (simp_all add: plus_ac0)
   9.210 +
   9.211 +(* Facts specific to rings *)
   9.212 +
   9.213 +instance ring < plus_ac0
   9.214 +proof
   9.215 +  fix x y z
   9.216 +  show "(x::'a::ring) + y = y + x" by (rule a_comm)
   9.217 +  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
   9.218 +  show "0 + (x::'a::ring) = x" by (rule l_zero)
   9.219 +qed
   9.220 +
   9.221 +ML {*
   9.222 +  local
   9.223 +    val lhss = 
   9.224 +        [read_cterm (sign_of (the_context ()))
   9.225 +                    ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
   9.226 +	 read_cterm (sign_of (the_context ()))
   9.227 +                    ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
   9.228 +	 read_cterm (sign_of (the_context ()))
   9.229 +                    ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
   9.230 +	 read_cterm (sign_of (the_context ()))
   9.231 +                    ("- ?t::'a::ring", TVar (("'z", 0), []))
   9.232 +	];
   9.233 +    fun proc sg _ t = 
   9.234 +      let val rew = Tactic.prove sg [] []
   9.235 +            (HOLogic.mk_Trueprop
   9.236 +              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
   9.237 +                (fn _ => simp_tac ring_ss 1)
   9.238 +            |> mk_meta_eq;
   9.239 +          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
   9.240 +      in if t' aconv u 
   9.241 +        then None
   9.242 +        else Some rew 
   9.243 +    end;
   9.244 +  in
   9.245 +    val ring_simproc = mk_simproc "ring" lhss proc;
   9.246 +  end;
   9.247 +*}
   9.248 +
   9.249 +ML_setup {* Addsimprocs [ring_simproc] *}
   9.250 +
   9.251 +lemma natsum_ldistr:
   9.252 +  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
   9.253 +by (induct n) simp_all
   9.254 +
   9.255 +lemma natsum_rdistr:
   9.256 +  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
   9.257 +by (induct n) simp_all
   9.258 +
   9.259 +subsection {* Integral Domains *}
   9.260 +
   9.261 +declare one_not_zero [simp]
   9.262 +
   9.263 +lemma zero_not_one [simp]:
   9.264 +  "0 ~= (1::'a::domain)" 
   9.265 +by (rule not_sym) simp
   9.266 +
   9.267 +lemma integral_iff: (* not by default a simp rule! *)
   9.268 +  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
   9.269 +proof
   9.270 +  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
   9.271 +next
   9.272 +  assume "a = 0 | b = 0" then show "a * b = 0" by auto
   9.273 +qed
   9.274 +
   9.275 +(*
   9.276 +lemma "(a::'a::ring) - (a - b) = b" apply simp
   9.277 +simproc seems to fail on this example
   9.278 +*)
   9.279 +
   9.280 +lemma bug: "(b::'a::ring) - (b - a) = a" by simp
   9.281 +  (* simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" *)
   9.282 +
   9.283 +lemma m_lcancel:
   9.284 +  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
   9.285 +proof
   9.286 +  assume eq: "a * b = a * c"
   9.287 +  then have "a * (b - c) = 0" by simp
   9.288 +  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
   9.289 +  with prem have "b - c = 0" by auto 
   9.290 +  then have "b = b - (b - c)" by simp 
   9.291 +  also have "b - (b - c) = c" by (rule bug) 
   9.292 +  finally show "b = c" .
   9.293 +next
   9.294 +  assume "b = c" then show "a * b = a * c" by simp
   9.295 +qed
   9.296 +
   9.297 +lemma m_rcancel:
   9.298 +  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
   9.299 +by (simp add: m_lcancel)
   9.300  
   9.301  end
    10.1 --- a/src/HOL/Algebra/abstract/RingHomo.ML	Wed Nov 27 17:25:41 2002 +0100
    10.2 +++ b/src/HOL/Algebra/abstract/RingHomo.ML	Thu Nov 28 10:50:42 2002 +0100
    10.3 @@ -8,7 +8,7 @@
    10.4  
    10.5  Goalw [homo_def]
    10.6    "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \
    10.7 -\           f <1> = <1> |] ==> homo f";
    10.8 +\           f 1 = 1 |] ==> homo f";
    10.9  by Auto_tac;
   10.10  qed "homoI";
   10.11  
   10.12 @@ -20,7 +20,7 @@
   10.13  by (Fast_tac 1);
   10.14  qed "homo_mult";
   10.15  
   10.16 -Goalw [homo_def] "!! f. homo f ==> f <1> = <1>";
   10.17 +Goalw [homo_def] "!! f. homo f ==> f 1 = 1";
   10.18  by (Fast_tac 1);
   10.19  qed "homo_one";
   10.20  
   10.21 @@ -41,7 +41,7 @@
   10.22  by (dtac homo_one 1);
   10.23  by (Asm_simp_tac 1);
   10.24  by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1);
   10.25 -by (Asm_simp_tac 1);
   10.26 +by (Asm_full_simp_tac 1);
   10.27  qed "homo_power";
   10.28  
   10.29  Goal
    11.1 --- a/src/HOL/Algebra/abstract/RingHomo.thy	Wed Nov 27 17:25:41 2002 +0100
    11.2 +++ b/src/HOL/Algebra/abstract/RingHomo.thy	Thu Nov 28 10:50:42 2002 +0100
    11.3 @@ -4,14 +4,14 @@
    11.4      Author: Clemens Ballarin, started 15 April 1997
    11.5  *)
    11.6  
    11.7 -RingHomo = NatSum +
    11.8 +RingHomo = Ring +
    11.9  
   11.10  consts
   11.11 -  homo	:: ('a::ringS => 'b::ringS) => bool
   11.12 +  homo	:: ('a::ring => 'b::ring) => bool
   11.13  
   11.14  defs
   11.15    homo_def	"homo f == (ALL a b. f (a + b) = f a + f b &
   11.16  			      f (a * b) = f a * f b) &
   11.17 -			   f <1> = <1>"
   11.18 +			   f 1 = 1"
   11.19  
   11.20  end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Algebra/abstract/order.ML	Thu Nov 28 10:50:42 2002 +0100
    12.3 @@ -0,0 +1,250 @@
    12.4 +(*
    12.5 +  Title:     Term order, needed for normal forms in rings
    12.6 +  Id:        $Id$
    12.7 +  Author:    Clemens Ballarin and Roland Zumkeller
    12.8 +  Copyright: TU Muenchen
    12.9 +*)
   12.10 +
   12.11 +local
   12.12 +
   12.13 +(* 
   12.14 +An order is a value of type
   12.15 +  ('a -> bool, 'a * 'a -> bool).
   12.16 +
   12.17 +The two parts are:
   12.18 + 1) a unary predicate denoting the order's domain
   12.19 + 2) a binary predicate with the semanitcs "greater than"
   12.20 +
   12.21 +If (d, ord) is an order then ord (a,b) is defined if both d a and d b.
   12.22 +*)
   12.23 +
   12.24 +(*
   12.25 +Combines two orders with disjoint domains and returns
   12.26 +another one. 
   12.27 +When the compared values are from the same domain, the corresponding
   12.28 +order is used. If not the ones from the first domain are considerer
   12.29 +greater. (If a value is in neither of the two domains, exception
   12.30 +"Domain" is raised.)
   12.31 +*)
   12.32 +
   12.33 +fun combineOrd ((d1, ord1), (d2, ord2)) = 
   12.34 +  (fn x => d1 x orelse d2 x, 
   12.35 +   fn (a, b) =>
   12.36 +     if d1 a andalso d1 b then ord1 (a, b) else
   12.37 +     if d1 a andalso d2 b then true else
   12.38 +     if d2 a andalso d2 b then ord2 (a, b) else
   12.39 +     if d2 a andalso d1 b then false else raise Domain)
   12.40 +
   12.41 +
   12.42 +(* Counts the number of function applications + 1. *)
   12.43 +(* ### is there a standard Isabelle function for this? *)
   12.44 +
   12.45 +fun tsize (a $ b) = tsize a + tsize b
   12.46 +  | tsize _ = 1;
   12.47 +
   12.48 +(* foldl on non-empty lists *)
   12.49 +
   12.50 +fun foldl2 f (x::xs) = foldl f (x,xs)
   12.51 +
   12.52 +
   12.53 +(* Compares two terms, ignoring type information. *)
   12.54 +infix e;
   12.55 +fun Const (s1, _)   e Const (s2, _)   = s1 = s2
   12.56 +  | Free (s1, _)    e Free (s2, _)    = s1 = s2
   12.57 +  | Var (ix1, _)    e Var (ix2, _)    = ix1 = ix2
   12.58 +  | Bound i1        e Bound i2        = i1 = i2
   12.59 +  | Abs (s1, _, t1) e Abs (s2, _, t2) = s1 = s2 andalso t1 = t2
   12.60 +  | (s1 $ s2)       e (t1 $ t2)       = s1 = t1 andalso s2 = t2
   12.61 +  | _ e _ = false
   12.62 +
   12.63 +
   12.64 +
   12.65 +(* Curried lexicographich path order induced by an order on function symbols.
   12.66 +Its feature include:
   12.67 +- compatibility with Epsilon-operations 
   12.68 +- closure under substitutions
   12.69 +- well-foundedness
   12.70 +- subterm-property
   12.71 +- termination
   12.72 +- defined on all terms (not only on ground terms)
   12.73 +- linearity
   12.74 +
   12.75 +The order ignores types.
   12.76 +*)
   12.77 +
   12.78 +infix g;
   12.79 +fun clpo (d, ord) (s,t) = 
   12.80 +  let val (op g) = clpo (d, ord) in
   12.81 +     (s <> t) andalso
   12.82 +     if tsize s < tsize t then not (t g s) else
   12.83 +       (* improves performance. allowed because clpo is total. *)
   12.84 +     #2 (foldl2 combineOrd [
   12.85 +        (fn _ $ _ => true | Abs _ => true | _ => false, 
   12.86 +  	 fn (Abs (_, _, s'), t) => s' e t orelse s' g t orelse 
   12.87 + 				   (case t of
   12.88 + 					Abs (_, _, t') => s' g t'
   12.89 + 				      | t1 $ t2 => s g t1 andalso s g t2
   12.90 + 			           )
   12.91 +           | (s1 $ s2, t) => s1 e t orelse s2 e t orelse 
   12.92 +                             s1 g t orelse s2 g t orelse
   12.93 + 			    (case t of
   12.94 + 				 t1 $ t2 => (s1 e t1 andalso s2 g t2) orelse
   12.95 + 					    (s1 g t1 andalso s g t2)
   12.96 + 			       | _ => false
   12.97 +                             )
   12.98 +        ),
   12.99 +        (fn Free _       => true      | _ => false,   fn (Free (a,_), Free (b,_))     => a > b),
  12.100 +        (fn Bound _      => true      | _ => false,   fn (Bound a, Bound b)           => a > b),
  12.101 +        (fn Const (c, _) => not (d c) | _ => false,   fn (Const (a, _), Const (b, _)) => a > b),
  12.102 +        (fn Const (c, _) => d c       | _ => false,   fn (Const (a, _), Const (b, _)) => ord (a,b))
  12.103 +    ]) (s,t)
  12.104 +  end;
  12.105 +
  12.106 +(*
  12.107 +Open Issues: 
  12.108 +- scheme variables have to be ordered (should be simple)
  12.109 +*)
  12.110 +
  12.111 +(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
  12.112 +
  12.113 +(* Returns the position of an element in a list. If the
  12.114 +element doesn't occur in the list, a MatchException is raised. *)
  12.115 +fun pos (x::xs) i = if x = i then 0 else 1 + pos xs i;
  12.116 +
  12.117 +(* Generates a finite linear order from a list. 
  12.118 +[a, b, c] results in the order "a > b > c". *)
  12.119 +fun linOrd l = fn (a,b) => pos l a < pos l b;
  12.120 +
  12.121 +(* Determines whether an element is contained in a list. *)
  12.122 +fun contains (x::xs) i = (x = i) orelse (contains xs i) |
  12.123 +    contains [] i = false;
  12.124 +
  12.125 +in
  12.126 +
  12.127 +(* Term order for commutative rings *)
  12.128 +
  12.129 +fun termless_ring (a, b) =
  12.130 +  let
  12.131 +    val S = ["op *", "op -", "uminus", "op +", "0"];
  12.132 +    (* Order (decending from left to right) on the constant symbols *)
  12.133 +    val baseOrd = (contains S, linOrd S);
  12.134 +  in clpo baseOrd (b, a)
  12.135 +  end;
  12.136 +
  12.137 +(*** Rewrite rules ***)
  12.138 +
  12.139 +val a_assoc = thm "ring.a_assoc";
  12.140 +val l_zero = thm "ring.l_zero";
  12.141 +val l_neg = thm "ring.l_neg";
  12.142 +val a_comm = thm "ring.a_comm";
  12.143 +val m_assoc = thm "ring.m_assoc";
  12.144 +val l_one = thm "ring.l_one";
  12.145 +val l_distr = thm "ring.l_distr";
  12.146 +val m_comm = thm "ring.m_comm";
  12.147 +val minus_def = thm "ring.minus_def";
  12.148 +val inverse_def = thm "ring.inverse_def";
  12.149 +val divide_def = thm "ring.divide_def";
  12.150 +val power_def = thm "ring.power_def";
  12.151 +
  12.152 +(* These are the following axioms:
  12.153 +
  12.154 +  a_assoc:      "(a + b) + c = a + (b + c)"
  12.155 +  l_zero:       "0 + a = a"
  12.156 +  l_neg:        "(-a) + a = 0"
  12.157 +  a_comm:       "a + b = b + a"
  12.158 +
  12.159 +  m_assoc:      "(a * b) * c = a * (b * c)"
  12.160 +  l_one:        "1 * a = a"
  12.161 +
  12.162 +  l_distr:      "(a + b) * c = a * c + b * c"
  12.163 +
  12.164 +  m_comm:       "a * b = b * a"
  12.165 +
  12.166 +  -- {* Definition of derived operations *}
  12.167 +
  12.168 +  minus_def:    "a - b = a + (-b)"
  12.169 +  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
  12.170 +  divide_def:   "a / b = a * inverse b"
  12.171 +  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
  12.172 +*)
  12.173 +
  12.174 +(* These lemmas are needed in the proofs *)
  12.175 +val trans = thm "trans";
  12.176 +val sym = thm "sym";
  12.177 +val subst = thm "subst";
  12.178 +val box_equals = thm "box_equals";
  12.179 +val arg_cong = thm "arg_cong";
  12.180 +(* current theory *)
  12.181 +val thy = the_context ();
  12.182 +
  12.183 +(* derived rewrite rules *)
  12.184 +val a_lcomm = prove_goal thy "(a::'a::ring)+(b+c) = b+(a+c)"
  12.185 +  (fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1,
  12.186 +     rtac (a_comm RS arg_cong) 1]);
  12.187 +val r_zero = prove_goal thy "(a::'a::ring) + 0 = a"
  12.188 +  (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
  12.189 +val r_neg = prove_goal thy "(a::'a::ring) + (-a) = 0"
  12.190 +  (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
  12.191 +val r_neg2 = prove_goal thy "(a::'a::ring) + (-a + b) = b"
  12.192 +  (fn _ => [rtac (a_assoc RS sym RS trans) 1,
  12.193 +     simp_tac (simpset() addsimps [r_neg, l_zero]) 1]);
  12.194 +val r_neg1 = prove_goal thy "-(a::'a::ring) + (a + b) = b"
  12.195 +  (fn _ => [rtac (a_assoc RS sym RS trans) 1,
  12.196 +     simp_tac (simpset() addsimps [l_neg, l_zero]) 1]);
  12.197 +(* auxiliary *)
  12.198 +val a_lcancel = prove_goal thy "!! a::'a::ring. a + b = a + c ==> b = c"
  12.199 +  (fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2,
  12.200 +     res_inst_tac [("a1", "a")] (l_neg RS subst) 1,
  12.201 +     asm_simp_tac (simpset() addsimps [a_assoc]) 1]);
  12.202 +val minus_add = prove_goal thy "-((a::'a::ring) + b) = (-a) + (-b)"
  12.203 +  (fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1,
  12.204 +     simp_tac (simpset() addsimps [r_neg, l_neg, l_zero, 
  12.205 +                                   a_assoc, a_comm, a_lcomm]) 1]);
  12.206 +val minus_minus = prove_goal thy "-(-(a::'a::ring)) = a"
  12.207 +  (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]);
  12.208 +val minus0 = prove_goal thy "- 0 = (0::'a::ring)"
  12.209 +  (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1,
  12.210 +     rtac (l_zero RS sym) 1]);
  12.211 +
  12.212 +(* derived rules for multiplication *)
  12.213 +val m_lcomm = prove_goal thy "(a::'a::ring)*(b*c) = b*(a*c)"
  12.214 +  (fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1,
  12.215 +     rtac (m_comm RS arg_cong) 1]);
  12.216 +val r_one = prove_goal thy "(a::'a::ring) * 1 = a"
  12.217 +  (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
  12.218 +val r_distr = prove_goal thy "(a::'a::ring) * (b + c) = a * b + a * c"
  12.219 +  (fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1,
  12.220 +     simp_tac (simpset() addsimps [m_comm]) 1]);
  12.221 +(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
  12.222 +val l_null = prove_goal thy "0 * (a::'a::ring) = 0"
  12.223 +  (fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1,
  12.224 +     simp_tac (simpset() addsimps [r_zero]) 1]);
  12.225 +val r_null = prove_goal thy "(a::'a::ring) * 0 = 0"
  12.226 +  (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
  12.227 +val l_minus = prove_goal thy "(-(a::'a::ring)) * b = - (a * b)"
  12.228 +  (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
  12.229 +     rtac (l_distr RS sym RS trans) 1,
  12.230 +     simp_tac (simpset() addsimps [l_null, r_neg]) 1]);
  12.231 +val r_minus = prove_goal thy "(a::'a::ring) * (-b) = - (a * b)"
  12.232 +  (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
  12.233 +     rtac (r_distr RS sym RS trans) 1,
  12.234 +     simp_tac (simpset() addsimps [r_null, r_neg]) 1]);
  12.235 +
  12.236 +val ring_ss = HOL_basic_ss settermless termless_ring addsimps
  12.237 +  [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
  12.238 +   r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
  12.239 +   a_lcomm, m_lcomm, r_distr, l_null, r_null, l_minus, r_minus];
  12.240 +
  12.241 +val x = bind_thms ("ring_simps", [l_zero, r_zero, l_neg, r_neg,
  12.242 +  minus_minus, minus0, 
  12.243 +  l_one, r_one, l_null, r_null, l_minus, r_minus]);
  12.244 +
  12.245 +(* note: r_one added to ring_simp but not ring_ss *)
  12.246 +
  12.247 +(* note: not added (and not proved):
  12.248 +  a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one,
  12.249 +  m_lcancel_eq, m_rcancel_eq,
  12.250 +  thms involving dvd, integral domains, fields
  12.251 +*)
  12.252 +
  12.253 +end;
  12.254 \ No newline at end of file
    13.1 --- a/src/HOL/Algebra/poly/Degree.ML	Wed Nov 27 17:25:41 2002 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,358 +0,0 @@
    13.4 -(*
    13.5 -    Degree of polynomials
    13.6 -    $Id$
    13.7 -    written by Clemens Ballarin, started 22 January 1997
    13.8 -*)
    13.9 -
   13.10 -(* Relating degree and bound *)
   13.11 -
   13.12 -Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
   13.13 -by (force_tac (claset() addDs [inst "m" "n" boundD], 
   13.14 -               simpset()) 1); 
   13.15 -qed "below_bound";
   13.16 -
   13.17 -goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
   13.18 -by (rtac exE 1);
   13.19 -by (rtac LeastI 2);
   13.20 -by (assume_tac 2);
   13.21 -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
   13.22 -by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
   13.23 -qed "Least_is_bound";
   13.24 -
   13.25 -Goalw [coeff_def, deg_def]
   13.26 -  "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
   13.27 -by (rtac Least_le 1);
   13.28 -by (Fast_tac 1);
   13.29 -qed "deg_aboveI";
   13.30 -
   13.31 -Goalw [coeff_def, deg_def]
   13.32 -  "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
   13.33 -by (case_tac "n = 0" 1);
   13.34 -(* Case n=0 *)
   13.35 -by (Asm_simp_tac 1);
   13.36 -(* Case n~=0 *)
   13.37 -by (rotate_tac 1 1);
   13.38 -by (Asm_full_simp_tac 1);
   13.39 -by (rtac below_bound 1);
   13.40 -by (assume_tac 2);
   13.41 -by (rtac Least_is_bound 1);
   13.42 -qed "deg_belowI";
   13.43 -
   13.44 -Goalw [coeff_def, deg_def]
   13.45 -  "deg p < m ==> coeff m p = 0";
   13.46 -by (rtac exE 1); (* create !! x. *)
   13.47 -by (rtac boundD 2);
   13.48 -by (assume_tac 3);
   13.49 -by (rtac LeastI 2);
   13.50 -by (assume_tac 2);
   13.51 -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
   13.52 -by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
   13.53 -qed "deg_aboveD";
   13.54 -
   13.55 -Goalw [deg_def]
   13.56 -  "deg p = Suc y ==> ~ bound y (Rep_UP p)";
   13.57 -by (rtac not_less_Least 1);
   13.58 -by (Asm_simp_tac 1);
   13.59 -val lemma1 = result();
   13.60 -
   13.61 -Goalw [deg_def, coeff_def]
   13.62 -  "deg p = Suc y ==> coeff (deg p) p ~= 0";
   13.63 -by (rtac ccontr 1);
   13.64 -by (dtac notnotD 1);
   13.65 -by (cut_inst_tac [("p", "p")] Least_is_bound 1);
   13.66 -by (subgoal_tac "bound y (Rep_UP p)" 1);
   13.67 -(* prove subgoal *)
   13.68 -by (rtac boundI 2);  
   13.69 -by (case_tac "Suc y < m" 2);
   13.70 -(* first case *)
   13.71 -by (rtac boundD 2);  
   13.72 -by (assume_tac 2);
   13.73 -by (Asm_simp_tac 2);
   13.74 -(* second case *)
   13.75 -by (dtac leI 2);
   13.76 -by (dtac Suc_leI 2);
   13.77 -by (dtac le_anti_sym 2);
   13.78 -by (assume_tac 2);
   13.79 -by (Asm_full_simp_tac 2);
   13.80 -(* end prove subgoal *)
   13.81 -by (fold_goals_tac [deg_def]);
   13.82 -by (dtac lemma1 1);
   13.83 -by (etac notE 1);
   13.84 -by (assume_tac 1);
   13.85 -val lemma2 = result();
   13.86 -
   13.87 -Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
   13.88 -by (rtac lemma2 1);
   13.89 -by (Full_simp_tac 1);
   13.90 -by (dtac Suc_pred 1);
   13.91 -by (rtac sym 1);
   13.92 -by (Asm_simp_tac 1);
   13.93 -qed "deg_lcoeff";
   13.94 -
   13.95 -Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
   13.96 -by (etac contrapos_np 1); 
   13.97 -by (case_tac "deg p = 0" 1);
   13.98 -by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
   13.99 -by (rtac up_eqI 1);
  13.100 -by (case_tac "n=0" 1);
  13.101 -by (rotate_tac ~2 1);
  13.102 -by (Asm_full_simp_tac 1);
  13.103 -by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  13.104 -qed "nonzero_lcoeff";
  13.105 -
  13.106 -Goal "(deg p <= n) = bound n (Rep_UP p)";
  13.107 -by (rtac iffI 1);
  13.108 -(* ==> *)
  13.109 -by (rtac boundI 1);
  13.110 -by (fold_goals_tac [coeff_def]);
  13.111 -by (rtac deg_aboveD 1);
  13.112 -by (fast_arith_tac 1);
  13.113 -(* <== *)
  13.114 -by (rtac deg_aboveI 1);
  13.115 -by (rewtac coeff_def);
  13.116 -by (Fast_tac 1);
  13.117 -qed "deg_above_is_bound";
  13.118 -
  13.119 -(* Lemmas on the degree function *)
  13.120 -
  13.121 -Goalw [max_def]
  13.122 -  "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
  13.123 -by (case_tac "deg p <= deg q" 1);
  13.124 -(* case deg p <= deg q *)
  13.125 -by (rtac deg_aboveI 1);
  13.126 -by (Asm_simp_tac 1);
  13.127 -by (strip_tac 1);
  13.128 -by (dtac le_less_trans 1);
  13.129 -by (assume_tac 1);
  13.130 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  13.131 -(* case deg p > deg q *)
  13.132 -by (rtac deg_aboveI 1);
  13.133 -by (Asm_simp_tac 1);
  13.134 -by (dtac not_leE 1);
  13.135 -by (strip_tac 1);
  13.136 -by (dtac less_trans 1);
  13.137 -by (assume_tac 1);
  13.138 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  13.139 -qed "deg_add";
  13.140 -
  13.141 -Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
  13.142 -by (rtac order_antisym 1);
  13.143 -by (rtac le_trans 1);
  13.144 -by (rtac deg_add 1);
  13.145 -by (Asm_simp_tac 1);
  13.146 -by (rtac deg_belowI 1);
  13.147 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
  13.148 -qed "deg_add_equal";
  13.149 -
  13.150 -Goal "deg (monom m::'a::ring up) <= m";
  13.151 -by (asm_simp_tac 
  13.152 -  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
  13.153 -qed "deg_monom_ring";
  13.154 -
  13.155 -Goal "deg (monom m::'a::domain up) = m";
  13.156 -by (rtac le_anti_sym 1);
  13.157 -(* <= *)
  13.158 -by (rtac deg_monom_ring 1);
  13.159 -(* >= *)
  13.160 -by (asm_simp_tac 
  13.161 -  (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
  13.162 -qed "deg_monom";
  13.163 -
  13.164 -Goal "!! a::'a::ring. deg (const a) = 0";
  13.165 -by (rtac le_anti_sym 1);
  13.166 -by (rtac deg_aboveI 1);
  13.167 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  13.168 -by (rtac deg_belowI 1);
  13.169 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  13.170 -qed "deg_const";
  13.171 -
  13.172 -Goal "deg (0::'a::ringS up) = 0";
  13.173 -by (rtac le_anti_sym 1);
  13.174 -by (rtac deg_aboveI 1);
  13.175 -by (Simp_tac 1);
  13.176 -by (rtac deg_belowI 1);
  13.177 -by (Simp_tac 1);
  13.178 -qed "deg_zero";
  13.179 -
  13.180 -Goal "deg (<1>::'a::ring up) = 0";
  13.181 -by (rtac le_anti_sym 1);
  13.182 -by (rtac deg_aboveI 1);
  13.183 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  13.184 -by (rtac deg_belowI 1);
  13.185 -by (Simp_tac 1);
  13.186 -qed "deg_one";
  13.187 -
  13.188 -Goal "!!p::('a::ring) up. deg (-p) = deg p";
  13.189 -by (rtac le_anti_sym 1);
  13.190 -(* <= *)
  13.191 -by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
  13.192 -by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
  13.193 -qed "deg_uminus";
  13.194 -
  13.195 -Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
  13.196 -
  13.197 -Goal
  13.198 -  "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
  13.199 -by (case_tac "a = 0" 1);
  13.200 -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
  13.201 -qed "deg_smult_ring";
  13.202 -
  13.203 -Goal
  13.204 -  "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
  13.205 -by (rtac le_anti_sym 1);
  13.206 -by (rtac deg_smult_ring 1);
  13.207 -by (case_tac "a = 0" 1);
  13.208 -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
  13.209 -qed "deg_smult";
  13.210 -
  13.211 -Goal
  13.212 -  "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
  13.213 -\       coeff i p * coeff (k - i) q = 0";
  13.214 -by (simp_tac (simpset() addsimps [coeff_def]) 1);
  13.215 -by (rtac bound_mult_zero 1);
  13.216 -by (assume_tac 3);
  13.217 -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
  13.218 -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
  13.219 -qed "deg_above_mult_zero";
  13.220 -
  13.221 -Goal
  13.222 -  "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
  13.223 -by (rtac deg_aboveI 1);
  13.224 -by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
  13.225 -qed "deg_mult_ring";
  13.226 -
  13.227 -goal Main.thy 
  13.228 -  "!!k::nat. k < n ==> m < n + m - k";
  13.229 -by (arith_tac 1);
  13.230 -qed "less_add_diff";
  13.231 -
  13.232 -Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
  13.233 -(* More general than deg_belowI, and simplifies the next proof! *)
  13.234 -by (rtac deg_belowI 1);
  13.235 -by (Fast_tac 1);
  13.236 -qed "deg_below2I";
  13.237 -
  13.238 -Goal
  13.239 -  "!! p::'a::domain up. \
  13.240 -\    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
  13.241 -by (rtac le_anti_sym 1);
  13.242 -by (rtac deg_mult_ring 1);
  13.243 -(* deg p + deg q <= deg (p * q) *)
  13.244 -by (rtac deg_below2I 1);
  13.245 -by (Simp_tac 1);
  13.246 -(*
  13.247 -by (rtac conjI 1);
  13.248 -by (rtac impI 1);
  13.249 -*)
  13.250 -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
  13.251 -by (rtac le_add1 1);
  13.252 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  13.253 -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
  13.254 -by (rtac le_refl 1);
  13.255 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  13.256 -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
  13.257 -(*
  13.258 -by (rtac impI 1);
  13.259 -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
  13.260 -by (rtac le_add1 1);
  13.261 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  13.262 -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
  13.263 -by (rtac le_refl 1);
  13.264 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  13.265 -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
  13.266 -*)
  13.267 -qed "deg_mult";
  13.268 -
  13.269 -Addsimps [deg_smult, deg_mult];
  13.270 -
  13.271 -(* Representation theorems about polynomials *)
  13.272 -
  13.273 -goal PolyRing.thy
  13.274 -  "!! p::nat=>'a::ring up. \
  13.275 -\    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
  13.276 -by (induct_tac "n" 1);
  13.277 -by Auto_tac;
  13.278 -qed "coeff_SUM";
  13.279 -
  13.280 -goal UnivPoly.thy
  13.281 -  "!! f::(nat=>'a::ring). \
  13.282 -\    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
  13.283 -by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
  13.284 -by (auto_tac
  13.285 -    (claset() addDs [not_leE],
  13.286 -     simpset()));
  13.287 -qed "bound_SUM_if";
  13.288 -
  13.289 -Goal
  13.290 -  "!! p::'a::ring up. deg p <= n ==> \
  13.291 -\  setsum (%i. coeff i p *s monom i) {..n} = p";
  13.292 -by (rtac up_eqI 1);
  13.293 -by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
  13.294 -by (rtac trans 1);
  13.295 -by (res_inst_tac [("x", "na")] bound_SUM_if 2);
  13.296 -by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
  13.297 -by (rtac SUM_cong 1);
  13.298 -by (rtac refl 1);
  13.299 -by (Asm_simp_tac 1);
  13.300 -qed "up_repr";
  13.301 -
  13.302 -Goal
  13.303 -  "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
  13.304 -\  P (setsum (%i. coeff i p *s monom i) {..n})";
  13.305 -by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
  13.306 -qed "up_reprD";
  13.307 -
  13.308 -Goal
  13.309 -  "!! p::'a::ring up. \
  13.310 -\  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
  13.311 -\    ==> P p";
  13.312 -by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
  13.313 -qed "up_repr2D";
  13.314 -
  13.315 -(*
  13.316 -Goal
  13.317 -  "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
  13.318 -\    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
  13.319 -\    = (coeff k f = coeff k g)
  13.320 -...
  13.321 -qed "up_unique";
  13.322 -*)
  13.323 -
  13.324 -(* Polynomials over integral domains are again integral domains *)
  13.325 -
  13.326 -Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
  13.327 -by (rtac classical 1);
  13.328 -by (subgoal_tac "deg p = 0 & deg q = 0" 1);
  13.329 -by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
  13.330 -by (Asm_simp_tac 1);
  13.331 -by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
  13.332 -by (Asm_simp_tac 1);
  13.333 -by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
  13.334 -by (force_tac (claset() addIs [up_eqI], simpset()) 1);
  13.335 -by (rtac integral 1);
  13.336 -by (subgoal_tac "coeff 0 (p * q) = 0" 1);
  13.337 -by (Asm_simp_tac 2);
  13.338 -by (Full_simp_tac 1);
  13.339 -by (dres_inst_tac [("f", "deg")] arg_cong 1);
  13.340 -by (Asm_full_simp_tac 1);
  13.341 -qed "up_integral";
  13.342 -
  13.343 -Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
  13.344 -by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
  13.345 -by (dtac up_integral 1);
  13.346 -by Auto_tac;
  13.347 -by (rtac (const_inj RS injD) 1);
  13.348 -by (Simp_tac 1);
  13.349 -qed "smult_integral";
  13.350 -
  13.351 -(* Divisibility and degree *)
  13.352 -
  13.353 -Goalw [dvd_def]
  13.354 -  "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
  13.355 -by (etac exE 1);
  13.356 -by (hyp_subst_tac 1);
  13.357 -by (case_tac "p = 0" 1);
  13.358 -by (Asm_simp_tac 1);
  13.359 -by (dtac r_nullD 1);
  13.360 -by (asm_simp_tac (simpset() addsimps [le_add1]) 1);
  13.361 -qed "dvd_imp_deg";
    14.1 --- a/src/HOL/Algebra/poly/Degree.thy	Wed Nov 27 17:25:41 2002 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,15 +0,0 @@
    14.4 -(*
    14.5 -    Degree of polynomials
    14.6 -    $Id$
    14.7 -    written by Clemens Ballarin, started 22. 1. 1997
    14.8 -*)
    14.9 -
   14.10 -Degree = PolyRing +
   14.11 -
   14.12 -consts
   14.13 -  deg		:: ('a::ringS) up => nat
   14.14 -
   14.15 -defs
   14.16 -  deg_def	"deg p == LEAST n. bound n (Rep_UP p)"
   14.17 -
   14.18 -end
    15.1 --- a/src/HOL/Algebra/poly/LongDiv.ML	Wed Nov 27 17:25:41 2002 +0100
    15.2 +++ b/src/HOL/Algebra/poly/LongDiv.ML	Thu Nov 28 10:50:42 2002 +0100
    15.3 @@ -4,10 +4,55 @@
    15.4      Author: Clemens Ballarin, started 23 June 1999
    15.5  *)
    15.6  
    15.7 +(* legacy bindings and theorems *)
    15.8 +
    15.9 +val deg_aboveI = thm "deg_aboveI";
   15.10 +val smult_l_minus = thm "smult_l_minus";
   15.11 +val deg_monom_ring = thm "deg_monom_ring";
   15.12 +val deg_smult_ring = thm "deg_smult_ring";
   15.13 +val smult_l_distr = thm "smult_l_distr";
   15.14 +val smult_r_distr = thm "smult_r_distr";
   15.15 +val smult_r_minus = thm "smult_r_minus";
   15.16 +val smult_assoc2 = thm "smult_assoc2";
   15.17 +val smult_assoc1 = thm "smult_assoc1";
   15.18 +val monom_mult_smult = thm "monom_mult_smult";
   15.19 +val field_ax = thm "field_ax";
   15.20 +val lcoeff_nonzero = thm "lcoeff_nonzero";
   15.21 +
   15.22 +Goal
   15.23 +  "!! f::(nat=>'a::ring). \
   15.24 +\    (ALL i. i < m --> f i = 0) --> \
   15.25 +\      setsum (%i. f (i+m)) {..d} = setsum f {..m+d}";
   15.26 +by (induct_tac "d" 1);
   15.27 +(* Base case *)
   15.28 +by (induct_tac "m" 1);
   15.29 +by (Simp_tac 1);
   15.30 +by (Force_tac 1);
   15.31 +(* Induction step *)
   15.32 +by (asm_simp_tac (simpset() addsimps add_ac) 1);
   15.33 +val SUM_shrink_below_lemma = result();
   15.34 +
   15.35 +Goal
   15.36 +  "!! f::(nat=>'a::ring). \
   15.37 +\    [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
   15.38 +\    ==> P (setsum f {..n})";
   15.39 +by (asm_full_simp_tac 
   15.40 +    (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
   15.41 +qed "SUM_extend_below";
   15.42 +
   15.43 +Goal
   15.44 +  "!! p::'a::ring up. \
   15.45 +\  [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |] \
   15.46 +\    ==> P p";
   15.47 +by (asm_full_simp_tac (simpset() addsimps [thm "up_repr_le"]) 1);
   15.48 +qed "up_repr2D";
   15.49 +
   15.50 +(* Start of LongDiv *)
   15.51 +
   15.52  Goal
   15.53    "!!p::('a::ring up). \
   15.54  \    [| deg p <= deg r; deg q <= deg r; \
   15.55 -\       coeff (deg r) p = - (coeff (deg r) q); deg r ~= 0 |] ==> \
   15.56 +\       coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==> \
   15.57  \    deg (p + q) < deg r";
   15.58  by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1);
   15.59  by (arith_tac 2);
   15.60 @@ -25,7 +70,7 @@
   15.61  Goal
   15.62    "!!p::('a::ring up). \
   15.63  \    [| deg p <= deg r; deg q <= deg r; \
   15.64 -\       p ~= -q; coeff (deg r) p = - (coeff (deg r) q) |] ==> \
   15.65 +\       p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==> \
   15.66  \    deg (p + q) < deg r";
   15.67  by (rtac deg_lcoeff_cancel 1);
   15.68  by (REPEAT (atac 1));
   15.69 @@ -51,7 +96,7 @@
   15.70  by (res_inst_tac [("x", "(0, x, 0)")] exI 1);
   15.71  by (Asm_simp_tac 1);
   15.72  (* case "eucl_size x >= eucl_size g" *)
   15.73 -by (dres_inst_tac [("x", "lcoeff g *s x -- (lcoeff x *s monom (deg x - deg g)) * g")] spec 1);
   15.74 +by (dres_inst_tac [("x", "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g")] spec 1);
   15.75  by (etac impE 1);
   15.76  by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1);
   15.77  by (case_tac "x = 0" 1);
   15.78 @@ -71,14 +116,35 @@
   15.79    by (rtac le_trans 1);
   15.80    by (rtac deg_mult_ring 1);
   15.81    by (rtac le_trans 1);
   15.82 +(**)
   15.83 +  by (rtac add_le_mono 1); by (rtac le_refl 1);
   15.84 +    (* term order forces to use this instead of add_le_mono1 *)
   15.85 +  by (rtac deg_monom_ring 1);
   15.86 +  by (Asm_simp_tac 1);
   15.87 +(**)
   15.88 +(*
   15.89    by (rtac add_le_mono1 1);
   15.90    by (rtac deg_smult_ring 1);
   15.91  (*  by (asm_simp_tac (simpset() addsimps [leI]) 1); *)
   15.92    by (Asm_simp_tac 1);
   15.93    by (cut_inst_tac [("m", "deg x - deg g"), ("'a", "'a")] deg_monom_ring 1);
   15.94    by (arith_tac 1);
   15.95 +*)
   15.96  by (Force_tac 1);
   15.97  by (Simp_tac 1);
   15.98 +(**)
   15.99 +  (* This change is probably caused by application of commutativity *)
  15.100 +by (res_inst_tac [("m", "deg g"), ("n", "deg x")] SUM_extend 1);
  15.101 +by (Simp_tac 1);
  15.102 +by (Asm_simp_tac 1);
  15.103 +by (arith_tac 1);
  15.104 +by (res_inst_tac [("m", "deg g"), ("n", "deg g")] SUM_extend_below 1);
  15.105 +by (rtac le_refl 1);
  15.106 +by (Asm_simp_tac 1);
  15.107 +by (arith_tac 1);
  15.108 +by (Simp_tac 1);
  15.109 +(**)
  15.110 +(*
  15.111  by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
  15.112  by (Simp_tac 1);
  15.113  by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym]) 1);
  15.114 @@ -87,14 +153,19 @@
  15.115  by (rtac le_refl 1);
  15.116  by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
  15.117  by (asm_simp_tac (simpset() addsimps [diff_diff_right, leI, m_comm]) 1);
  15.118 +*)
  15.119  (* end of subproof deg f1 < deg f *)
  15.120  by (etac exE 1);
  15.121 -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);
  15.122 +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);
  15.123  by (Clarify_tac 1);
  15.124  by (dtac sym 1);
  15.125 -by (simp_tac (simpset() addsimps [l_distr, a_assoc]) 1);
  15.126 -by (Asm_simp_tac 1);
  15.127 -by (simp_tac (simpset() addsimps a_ac@[smult_l_distr, smult_r_distr, smult_r_minus, smult_assoc2, smult_assoc1]) 1);
  15.128 +by (simp_tac (simpset() addsimps [l_distr, a_assoc]
  15.129 +  delsimprocs [ring_simproc]) 1);
  15.130 +by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1);
  15.131 +by (simp_tac (simpset() addsimps [minus_def, smult_r_distr, smult_r_minus,
  15.132 +    monom_mult_smult, smult_assoc1, smult_assoc2]
  15.133 +  delsimprocs [ring_simproc]) 1);
  15.134 +by (Simp_tac 1);
  15.135  qed "long_div_eucl_size";
  15.136  
  15.137  Goal
  15.138 @@ -102,8 +173,9 @@
  15.139  \    Ex (% (q, r, k). \
  15.140  \      (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))";
  15.141  by (forw_inst_tac [("f", "f")]
  15.142 -  (simplify (simpset() addsimps [eucl_size_def]) long_div_eucl_size) 1);
  15.143 -by Auto_tac;
  15.144 +  (simplify (simpset() addsimps [eucl_size_def]
  15.145 +    delsimprocs [ring_simproc]) long_div_eucl_size) 1);
  15.146 +by (auto_tac (claset(), simpset() delsimprocs [ring_simproc]));
  15.147  by (case_tac "aa = 0" 1);
  15.148  by (Blast_tac 1);
  15.149  (* case "aa ~= 0 *)
  15.150 @@ -111,18 +183,20 @@
  15.151  by Auto_tac;
  15.152  qed "long_div_ring";
  15.153  
  15.154 +(* Next one fails *)
  15.155  Goal
  15.156 -  "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd <1> |] ==> \
  15.157 +  "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==> \
  15.158  \    Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
  15.159  by (forw_inst_tac [("f", "f")] long_div_ring 1);
  15.160  by (etac exE 1);
  15.161  by (res_inst_tac [("x", "((%(q,r,k). (inverse(lcoeff g ^k) *s q)) x, \
  15.162  \  (%(q,r,k). inverse(lcoeff g ^k) *s r) x)")] exI 1);
  15.163  by (Clarify_tac 1);
  15.164 -by (Simp_tac 1);
  15.165 +(* by (Simp_tac 1); *)
  15.166  by (rtac conjI 1);
  15.167  by (dtac sym 1);
  15.168 -by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]) 1);
  15.169 +by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]
  15.170 +  delsimprocs [ring_simproc]) 1);
  15.171  by (asm_simp_tac (simpset() addsimps [l_inverse_ring, unit_power, smult_assoc1 RS sym]) 1);
  15.172  (* degree property *)
  15.173  by (etac disjE 1);
  15.174 @@ -138,14 +212,28 @@
  15.175  \    Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
  15.176  by (rtac long_div_unit 1);
  15.177  by (assume_tac 1);
  15.178 -by (asm_simp_tac (simpset() addsimps [lcoeff_def, nonzero_lcoeff, field_ax]) 1);
  15.179 +by (asm_simp_tac (simpset() addsimps [lcoeff_def, lcoeff_nonzero, field_ax]) 1);
  15.180  qed "long_div_theorem";
  15.181  
  15.182 +Goal "- (0::'a::ring) = 0";
  15.183 +by (Simp_tac 1);
  15.184 +val uminus_zero = result();
  15.185 +
  15.186 +Goal "!!a::'a::ring. a - b = 0 ==> a = b";
  15.187 +br trans 1;
  15.188 +by (res_inst_tac [("b", "a")] (thm "bug") 2);
  15.189 +by (Asm_simp_tac 1);
  15.190 +val diff_zero_imp_eq = result();
  15.191 +
  15.192 +Goal "!!a::'a::ring. a = b ==> a + (-b) = 0";
  15.193 +by (Asm_simp_tac 1);
  15.194 +val eq_imp_diff_zero = result();
  15.195 +
  15.196  Goal
  15.197    "!!g::('a::field up). [| g ~= 0; \
  15.198  \    f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \
  15.199  \    f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2";
  15.200 -by (subgoal_tac "(q1 -- q2) * g = r2 -- r1" 1); (* 1 *)
  15.201 +by (subgoal_tac "(q1 - q2) * g = r2 - r1" 1); (* 1 *)
  15.202  by (thin_tac "f = ?x" 1);
  15.203  by (thin_tac "f = ?x" 1);
  15.204  by (rtac diff_zero_imp_eq 1);
  15.205 @@ -154,18 +242,23 @@
  15.206  (* r1 = 0 *)
  15.207  by (etac disjE 1);
  15.208  (* r2 = 0 *)
  15.209 -by (force_tac (claset() addDs [integral], simpset()) 1);
  15.210 +by (asm_full_simp_tac (simpset()
  15.211 +  addsimps [thm "integral_iff", minus_def, l_zero, uminus_zero]
  15.212 +  delsimprocs [ring_simproc]) 1);
  15.213  (* r2 ~= 0 *)
  15.214 -by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
  15.215 -by (Force_tac 1);
  15.216 +by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
  15.217 +by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero]
  15.218 +  delsimprocs [ring_simproc]) 1);
  15.219  (* r1 ~=0 *)
  15.220  by (etac disjE 1);
  15.221  (* r2 = 0 *)
  15.222 -by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
  15.223 -by (Force_tac 1);
  15.224 +by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
  15.225 +by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero]
  15.226 +  delsimprocs [ring_simproc]) 1);
  15.227  (* r2 ~= 0 *)
  15.228 -by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
  15.229 -by (Asm_full_simp_tac 1);
  15.230 +by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
  15.231 +by (asm_full_simp_tac (simpset() addsimps [minus_def]
  15.232 +  delsimprocs [ring_simproc]) 1);
  15.233  by (dtac (order_eq_refl RS add_leD2) 1);
  15.234  by (dtac leD 1);
  15.235  by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1);
  15.236 @@ -174,7 +267,7 @@
  15.237  by (rtac diff_zero_imp_eq 1);
  15.238  by (hyp_subst_tac 1);
  15.239  by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1);
  15.240 -by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1);
  15.241 +by (Asm_full_simp_tac 1);
  15.242  qed "long_div_quo_unique";
  15.243  
  15.244  Goal
  15.245 @@ -183,7 +276,11 @@
  15.246  \    f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2";
  15.247  by (subgoal_tac "q1 = q2" 1);
  15.248  by (Clarify_tac 1);
  15.249 -by (asm_full_simp_tac (simpset() addsimps [a_lcancel_eq]) 1);
  15.250 +by (res_inst_tac [("a", "q2 * g + r1 - q2 * g"), ("b", "q2 * g + r2 - q2 * g")]
  15.251 +  box_equals 1);
  15.252 +by (Asm_full_simp_tac 1);
  15.253 +by (Simp_tac 1);
  15.254 +by (Simp_tac 1);
  15.255  by (rtac long_div_quo_unique 1);
  15.256  by (REPEAT (atac 1));
  15.257  qed "long_div_rem_unique";
    16.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Wed Nov 27 17:25:41 2002 +0100
    16.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Thu Nov 28 10:50:42 2002 +0100
    16.3 @@ -7,11 +7,11 @@
    16.4  LongDiv = PolyHomo +
    16.5  
    16.6  consts
    16.7 -  lcoeff :: "'a::ringS up => 'a"
    16.8 -  eucl_size :: 'a::ringS => nat
    16.9 +  lcoeff :: "'a::ring up => 'a"
   16.10 +  eucl_size :: 'a::ring => nat
   16.11  
   16.12  defs
   16.13 -  lcoeff_def	"lcoeff p == coeff (deg p) p"
   16.14 +  lcoeff_def	"lcoeff p == coeff p (deg p)"
   16.15    eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1"
   16.16  
   16.17  end
    17.1 --- a/src/HOL/Algebra/poly/PolyHomo.ML	Wed Nov 27 17:25:41 2002 +0100
    17.2 +++ b/src/HOL/Algebra/poly/PolyHomo.ML	Thu Nov 28 10:50:42 2002 +0100
    17.3 @@ -4,8 +4,85 @@
    17.4      Author: Clemens Ballarin, started 16 April 1997
    17.5  *)
    17.6  
    17.7 +(* Summation result for tactic-style proofs *)
    17.8 +
    17.9 +val natsum_add = thm "natsum_add";
   17.10 +val natsum_ldistr = thm "natsum_ldistr";
   17.11 +val natsum_rdistr = thm "natsum_rdistr";
   17.12 +
   17.13 +Goal
   17.14 +  "!! f::(nat=>'a::ring). \
   17.15 +\    m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \
   17.16 +\    setsum f {..m} = setsum f {..n}";
   17.17 +by (induct_tac "n" 1);
   17.18 +(* Base case *)
   17.19 +by (Simp_tac 1);
   17.20 +(* Induction step *)
   17.21 +by (case_tac "m <= n" 1);
   17.22 +by Auto_tac;
   17.23 +by (subgoal_tac "m = Suc n" 1);
   17.24 +by (Asm_simp_tac 1);
   17.25 +by (fast_arith_tac 1);
   17.26 +val SUM_shrink_lemma = result();
   17.27 +
   17.28 +Goal
   17.29 +  "!! f::(nat=>'a::ring). \
   17.30 +\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \
   17.31 +\  ==> P (setsum f {..m})";
   17.32 +by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
   17.33 +by (Asm_full_simp_tac 1);
   17.34 +qed "SUM_shrink";
   17.35 +
   17.36 +Goal
   17.37 +  "!! f::(nat=>'a::ring). \
   17.38 +\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \
   17.39 +\    ==> P (setsum f {..n})";
   17.40 +by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
   17.41 +by (Asm_full_simp_tac 1);
   17.42 +qed "SUM_extend";
   17.43 +
   17.44 +Goal
   17.45 +  "!!f::nat=>'a::ring. j <= n + m --> \
   17.46 +\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \
   17.47 +\    setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}";
   17.48 +by (induct_tac "j" 1);
   17.49 +(* Base case *)
   17.50 +by (Simp_tac 1);
   17.51 +(* Induction step *)
   17.52 +by (simp_tac (simpset() addsimps [Suc_diff_le, natsum_add]) 1);
   17.53 +(*
   17.54 +by (asm_simp_tac (simpset() addsimps a_ac) 1);
   17.55 +*)
   17.56 +by (Asm_simp_tac 1);
   17.57 +val DiagSum_lemma = result();
   17.58 +
   17.59 +Goal
   17.60 +  "!!f::nat=>'a::ring. \
   17.61 +\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \
   17.62 +\    setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}";
   17.63 +by (rtac (DiagSum_lemma RS mp) 1);
   17.64 +by (rtac le_refl 1);
   17.65 +qed "DiagSum";
   17.66 +
   17.67 +Goal
   17.68 +  "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \
   17.69 +\    setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \
   17.70 +\    setsum f {..n} * setsum g {..m}";
   17.71 +by (simp_tac (simpset() addsimps [natsum_ldistr, DiagSum]) 1);
   17.72 +(* SUM_rdistr must be applied after SUM_ldistr ! *)
   17.73 +by (simp_tac (simpset() addsimps [natsum_rdistr]) 1);
   17.74 +by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
   17.75 +by (rtac le_add1 1);
   17.76 +by (Force_tac 1);
   17.77 +by (rtac (thm "natsum_cong") 1);
   17.78 +by (rtac refl 1);
   17.79 +by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
   17.80 +by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
   17.81 +by Auto_tac;
   17.82 +qed "CauchySum";
   17.83 +
   17.84  (* Ring homomorphisms and polynomials *)
   17.85 -
   17.86 +(*
   17.87  Goal "homo (const::'a::ring=>'a up)";
   17.88  by (auto_tac (claset() addSIs [homoI], simpset()));
   17.89  qed "const_homo";
   17.90 @@ -19,6 +96,15 @@
   17.91  qed "homo_smult";
   17.92  
   17.93  Addsimps [homo_smult];
   17.94 +*)
   17.95 +
   17.96 +val deg_add = thm "deg_add";
   17.97 +val deg_mult_ring = thm "deg_mult_ring";
   17.98 +val deg_aboveD = thm "deg_aboveD";
   17.99 +val coeff_add = thm "coeff_add";
  17.100 +val coeff_mult = thm "coeff_mult";
  17.101 +val boundI = thm "boundI";
  17.102 +val monom_mult_is_smult = thm "monom_mult_is_smult";
  17.103  
  17.104  (* Evaluation homomorphism *)
  17.105  
  17.106 @@ -42,7 +128,7 @@
  17.107  by (rtac le_maxI2 1);
  17.108  by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  17.109  (* actual homom property + *)
  17.110 -by (asm_simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
  17.111 +by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1);
  17.112  
  17.113  (* * commutes *)
  17.114  by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")]
  17.115 @@ -53,34 +139,33 @@
  17.116  by (rtac CauchySum 2);
  17.117  by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
  17.118  by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
  17.119 -(* getting a^i and a^(k-i) together is difficult, so we do is manually *)
  17.120 +(* getting a^i and a^(k-i) together is difficult, so we do it manually *)
  17.121  by (res_inst_tac [("s", 
  17.122  "        setsum  \
  17.123  \           (%k. setsum \
  17.124 -\                 (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \
  17.125 +\                 (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * \
  17.126  \                      (a ^ i * a ^ (k - i)))) {..k}) \
  17.127  \           {..deg aa + deg b}")] trans 1);
  17.128  by (asm_simp_tac (simpset()
  17.129 -    addsimps [power_mult, leD RS add_diff_inverse, SUM_ldistr]) 1);
  17.130 -by (simp_tac (simpset() addsimps m_ac) 1);
  17.131 -by (simp_tac (simpset() addsimps m_ac) 1);
  17.132 -(* <1> commutes *)
  17.133 +    addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1);
  17.134 +by (Simp_tac 1);
  17.135 +(* 1 commutes *)
  17.136  by (Asm_simp_tac 1);
  17.137  qed "EVAL2_homo";
  17.138  
  17.139  Goalw [EVAL2_def]
  17.140 -  "!! phi::'a::ring=>'b::ring. EVAL2 phi a (const b) = phi b";
  17.141 +  "!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b";
  17.142  by (Simp_tac 1);
  17.143  qed "EVAL2_const";
  17.144  
  17.145  Goalw [EVAL2_def]
  17.146 -  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a";
  17.147 -(* Must be able to distinguish 0 from <1>, hence 'a::domain *)
  17.148 +  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a";
  17.149 +(* Must be able to distinguish 0 from 1, hence 'a::domain *)
  17.150  by (Asm_simp_tac 1);
  17.151  qed "EVAL2_monom1";
  17.152  
  17.153  Goalw [EVAL2_def]
  17.154 -  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
  17.155 +  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n";
  17.156  by (Simp_tac 1);
  17.157  by (case_tac "n" 1); 
  17.158  by Auto_tac;
  17.159 @@ -89,19 +174,35 @@
  17.160  Goal
  17.161    "!! phi::'a::ring=>'b::ring. \
  17.162  \    homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p";
  17.163 -by (asm_simp_tac
  17.164 -  (simpset() addsimps [const_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
  17.165 +by (asm_simp_tac (simpset() 
  17.166 +    addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
  17.167  qed "EVAL2_smult";
  17.168  
  17.169 +val up_eqI = thm "up_eqI";
  17.170 +
  17.171 +Goal "monom (a::'a::ring) n = monom a 0 * monom 1 n";
  17.172 +by (simp_tac (simpset() addsimps [monom_mult_is_smult]) 1);
  17.173 +by (rtac up_eqI 1);
  17.174 +by (Simp_tac 1);
  17.175 +qed "monom_decomp";
  17.176 +
  17.177 +Goal
  17.178 +  "!! phi::'a::domain=>'b::ring. \
  17.179 +\    homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n";
  17.180 +by (stac monom_decomp 1);
  17.181 +by (asm_simp_tac (simpset() 
  17.182 +    addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1);
  17.183 +qed "EVAL2_monom_n";
  17.184 +
  17.185  Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)";
  17.186 -by (asm_simp_tac (simpset() addsimps [EVAL2_homo, id_homo]) 1);
  17.187 +by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1);
  17.188  qed "EVAL_homo";
  17.189  
  17.190 -Goalw [EVAL_def] "!! a::'a::ring. EVAL a (const b) = b";
  17.191 +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom b 0) = b";
  17.192  by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
  17.193  qed "EVAL_const";
  17.194  
  17.195 -Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom n) = a ^ n";
  17.196 +Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n";
  17.197  by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
  17.198  qed "EVAL_monom";
  17.199  
  17.200 @@ -109,19 +210,23 @@
  17.201  by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
  17.202  qed "EVAL_smult";
  17.203  
  17.204 +Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n";
  17.205 +by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1);
  17.206 +qed "EVAL_monom_n";
  17.207 +
  17.208  (* Examples *)
  17.209  
  17.210  Goal
  17.211    "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
  17.212  by (asm_simp_tac (simpset() delsimps [power_Suc]
  17.213 -    addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
  17.214 +    addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1);
  17.215  result();
  17.216  
  17.217  Goal
  17.218    "EVAL (y::'a::domain) \
  17.219 -\    (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
  17.220 +\    (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \
  17.221  \  x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
  17.222  by (asm_simp_tac (simpset() delsimps [power_Suc]
  17.223 -    addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
  17.224 +    addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1);
  17.225  result();
  17.226  
    18.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Wed Nov 27 17:25:41 2002 +0100
    18.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy	Thu Nov 28 10:50:42 2002 +0100
    18.3 @@ -4,20 +4,15 @@
    18.4      Author: Clemens Ballarin, started 15 April 1997
    18.5  *)
    18.6  
    18.7 -PolyHomo = Degree +
    18.8 -
    18.9 -(* Instantiate result from Degree.ML *)
   18.10 -
   18.11 -instance
   18.12 -  up :: (domain) domain (up_one_not_zero, up_integral)
   18.13 +PolyHomo = UnivPoly +
   18.14  
   18.15  consts
   18.16 -  EVAL2	:: "('a::ring => 'b) => 'b => 'a up => 'b::ring"
   18.17 -  EVAL	:: "'a::ring => 'a up => 'a"
   18.18 +  EVAL2	:: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
   18.19 +  EVAL	:: "['a::ring, 'a up] => 'a"
   18.20  
   18.21  defs
   18.22    EVAL2_def	"EVAL2 phi a p ==
   18.23 -                 setsum (%i. phi (coeff i p) * a ^ i) {..deg p}"
   18.24 +                 setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
   18.25    EVAL_def	"EVAL == EVAL2 (%x. x)"
   18.26  
   18.27  end
    19.1 --- a/src/HOL/Algebra/poly/PolyRing.ML	Wed Nov 27 17:25:41 2002 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,68 +0,0 @@
    19.4 -(*
    19.5 -    Instantiate polynomials to form a ring and prove further properties
    19.6 -    $Id$
    19.7 -    Author: Clemens Ballarin, started 22 January 1997
    19.8 -*)
    19.9 -
   19.10 -(* Properties of *s:
   19.11 -   Polynomials form a module *)
   19.12 -
   19.13 -goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p";
   19.14 -by (rtac up_eqI 1);
   19.15 -by (simp_tac (simpset() addsimps [l_distr]) 1);
   19.16 -qed "smult_l_distr";
   19.17 -
   19.18 -goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q";
   19.19 -by (rtac up_eqI 1);
   19.20 -by (simp_tac (simpset() addsimps [r_distr]) 1);
   19.21 -qed "smult_r_distr";
   19.22 -
   19.23 -goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)";
   19.24 -by (rtac up_eqI 1);
   19.25 -by (simp_tac (simpset() addsimps [m_assoc]) 1);
   19.26 -qed "smult_assoc1";
   19.27 -
   19.28 -goal UnivPoly.thy "(<1>::'a::ring) *s p = p";
   19.29 -by (rtac up_eqI 1);
   19.30 -by (Simp_tac 1);
   19.31 -qed "smult_one";
   19.32 -
   19.33 -(* Polynomials form an algebra *)
   19.34 -
   19.35 -goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)";
   19.36 -by (rtac up_eqI 1);
   19.37 -by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1);
   19.38 -qed "smult_assoc2";
   19.39 -
   19.40 -(* the following can be derived from the above ones,
   19.41 -   for generality reasons, it is therefore done *)
   19.42 -
   19.43 -Goal "(0::'a::ring) *s p = 0";
   19.44 -by (rtac a_lcancel 1);
   19.45 -by (rtac (smult_l_distr RS sym RS trans) 1);
   19.46 -by (Simp_tac 1);
   19.47 -qed "smult_l_null";
   19.48 -
   19.49 -Goal "!!a::'a::ring. a *s 0 = 0";
   19.50 -by (rtac a_lcancel 1);
   19.51 -by (rtac (smult_r_distr RS sym RS trans) 1);
   19.52 -by (Simp_tac 1);
   19.53 -qed "smult_r_null";
   19.54 -
   19.55 -Goal "!!a::'a::ring. (-a) *s p = - (a *s p)";
   19.56 -by (rtac a_lcancel 1);
   19.57 -by (rtac (r_neg RS sym RSN (2, trans)) 1);
   19.58 -by (rtac (smult_l_distr RS sym RS trans) 1);
   19.59 -by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1);
   19.60 -qed "smult_l_minus";
   19.61 -
   19.62 -Goal "!!a::'a::ring. a *s (-p) = - (a *s p)";
   19.63 -by (rtac a_lcancel 1);
   19.64 -by (rtac (r_neg RS sym RSN (2, trans)) 1);
   19.65 -by (rtac (smult_r_distr RS sym RS trans) 1);
   19.66 -by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1);
   19.67 -qed "smult_r_minus";
   19.68 -
   19.69 -val smult_minus = [smult_l_minus, smult_r_minus];
   19.70 -
   19.71 -Addsimps [smult_one, smult_l_null, smult_r_null];
    20.1 --- a/src/HOL/Algebra/poly/PolyRing.thy	Wed Nov 27 17:25:41 2002 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,15 +0,0 @@
    20.4 -(*
    20.5 -    Instantiate polynomials to form a ring and prove further properties
    20.6 -    $Id$
    20.7 -    Author: Clemens Ballarin, started 20 January 1997
    20.8 -*)
    20.9 -
   20.10 -PolyRing = UnivPoly +
   20.11 -
   20.12 -instance
   20.13 -  up :: (ring) ring
   20.14 -  (up_a_assoc, up_l_zero, up_l_neg, up_a_comm, 
   20.15 -   up_m_assoc, up_l_one, up_l_distr, up_m_comm,
   20.16 -   up_inverse_def, up_divide_def, up_power_def) {| ALLGOALS (rtac refl) |}
   20.17 -
   20.18 -end
    21.1 --- a/src/HOL/Algebra/poly/ProtoPoly.ML	Wed Nov 27 17:25:41 2002 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,30 +0,0 @@
    21.4 -(*
    21.5 -    Prepearing definitions for polynomials
    21.6 -    $Id$
    21.7 -    Author: Clemens Ballarin, started 9 December 1996
    21.8 -*)
    21.9 -
   21.10 -(* Rules for bound *)
   21.11 -
   21.12 -val prem = goalw ProtoPoly.thy [bound_def]
   21.13 -  "[| !! m. n < m ==> f m = 0 |] ==> bound n f";
   21.14 -by (fast_tac (claset() addIs prem) 1);
   21.15 -qed "boundI";
   21.16 -
   21.17 -Goalw [bound_def]
   21.18 -  "!! f. [| bound n f; n < m |] ==> f m = 0";
   21.19 -by (Fast_tac 1);
   21.20 -qed "boundD";
   21.21 -
   21.22 -Goalw [bound_def]
   21.23 -  "!! f. [| bound n f; n <= m  |] ==> bound m f";
   21.24 -by (fast_tac (set_cs addIs [le_less_trans]) 1);
   21.25 -(* Need set_cs, otherwise starts reasoning about naturals *)
   21.26 -qed "le_bound";
   21.27 -
   21.28 -AddSIs [boundI];
   21.29 -AddDs [boundD];
   21.30 -
   21.31 -Goal "(%x. 0) : {f. EX n. bound n f}";
   21.32 -by (Blast_tac 1);
   21.33 -qed "UP_witness";
    22.1 --- a/src/HOL/Algebra/poly/ProtoPoly.thy	Wed Nov 27 17:25:41 2002 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,15 +0,0 @@
    22.4 -(*
    22.5 -    Prepearing definitions for polynomials
    22.6 -    $Id$
    22.7 -    Author: Clemens Ballarin, started 9 December 1996
    22.8 -*)
    22.9 -
   22.10 -ProtoPoly = Abstract +
   22.11 -
   22.12 -consts
   22.13 -  bound :: [nat, nat => 'a::ringS] => bool
   22.14 -
   22.15 -defs
   22.16 -  bound_def  "bound n f == ALL i. n<i --> f i = 0"
   22.17 -
   22.18 -end
    23.1 --- a/src/HOL/Algebra/poly/UnivPoly.ML	Wed Nov 27 17:25:41 2002 +0100
    23.2 +++ b/src/HOL/Algebra/poly/UnivPoly.ML	Thu Nov 28 10:50:42 2002 +0100
    23.3 @@ -1,242 +1,359 @@
    23.4  (*
    23.5 -    Univariate Polynomials
    23.6 +    Degree of polynomials
    23.7      $Id$
    23.8 -    Author: Clemens Ballarin, started 9 December 1996
    23.9 -TODO: monom is *mono*morphism (probably induction needed)
   23.10 +    written by Clemens Ballarin, started 22 January 1997
   23.11  *)
   23.12  
   23.13 -(* Closure of UP under +, *s, monom, const and * *)
   23.14 +(*
   23.15 +(* Relating degree and bound *)
   23.16 +
   23.17 +Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
   23.18 +by (force_tac (claset() addDs [inst "m" "n" boundD], 
   23.19 +               simpset()) 1); 
   23.20 +qed "below_bound";
   23.21 +
   23.22 +goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
   23.23 +by (rtac exE 1);
   23.24 +by (rtac LeastI 2);
   23.25 +by (assume_tac 2);
   23.26 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
   23.27 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
   23.28 +qed "Least_is_bound";
   23.29 +
   23.30 +Goalw [coeff_def, deg_def]
   23.31 +  "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
   23.32 +by (rtac Least_le 1);
   23.33 +by (Fast_tac 1);
   23.34 +qed "deg_aboveI";
   23.35 +
   23.36 +Goalw [coeff_def, deg_def]
   23.37 +  "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
   23.38 +by (case_tac "n = 0" 1);
   23.39 +(* Case n=0 *)
   23.40 +by (Asm_simp_tac 1);
   23.41 +(* Case n~=0 *)
   23.42 +by (rotate_tac 1 1);
   23.43 +by (Asm_full_simp_tac 1);
   23.44 +by (rtac below_bound 1);
   23.45 +by (assume_tac 2);
   23.46 +by (rtac Least_is_bound 1);
   23.47 +qed "deg_belowI";
   23.48 +
   23.49 +Goalw [coeff_def, deg_def]
   23.50 +  "deg p < m ==> coeff m p = 0";
   23.51 +by (rtac exE 1); (* create !! x. *)
   23.52 +by (rtac boundD 2);
   23.53 +by (assume_tac 3);
   23.54 +by (rtac LeastI 2);
   23.55 +by (assume_tac 2);
   23.56 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
   23.57 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
   23.58 +qed "deg_aboveD";
   23.59 +
   23.60 +Goalw [deg_def]
   23.61 +  "deg p = Suc y ==> ~ bound y (Rep_UP p)";
   23.62 +by (rtac not_less_Least 1);
   23.63 +by (Asm_simp_tac 1);
   23.64 +val lemma1 = result();
   23.65 +
   23.66 +Goalw [deg_def, coeff_def]
   23.67 +  "deg p = Suc y ==> coeff (deg p) p ~= 0";
   23.68 +by (rtac ccontr 1);
   23.69 +by (dtac notnotD 1);
   23.70 +by (cut_inst_tac [("p", "p")] Least_is_bound 1);
   23.71 +by (subgoal_tac "bound y (Rep_UP p)" 1);
   23.72 +(* prove subgoal *)
   23.73 +by (rtac boundI 2);  
   23.74 +by (case_tac "Suc y < m" 2);
   23.75 +(* first case *)
   23.76 +by (rtac boundD 2);  
   23.77 +by (assume_tac 2);
   23.78 +by (Asm_simp_tac 2);
   23.79 +(* second case *)
   23.80 +by (dtac leI 2);
   23.81 +by (dtac Suc_leI 2);
   23.82 +by (dtac le_anti_sym 2);
   23.83 +by (assume_tac 2);
   23.84 +by (Asm_full_simp_tac 2);
   23.85 +(* end prove subgoal *)
   23.86 +by (fold_goals_tac [deg_def]);
   23.87 +by (dtac lemma1 1);
   23.88 +by (etac notE 1);
   23.89 +by (assume_tac 1);
   23.90 +val lemma2 = result();
   23.91 +
   23.92 +Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
   23.93 +by (rtac lemma2 1);
   23.94 +by (Full_simp_tac 1);
   23.95 +by (dtac Suc_pred 1);
   23.96 +by (rtac sym 1);
   23.97 +by (Asm_simp_tac 1);
   23.98 +qed "deg_lcoeff";
   23.99  
  23.100 -Goalw [UP_def]
  23.101 -  "[| f : UP; g : UP |] ==> (%n. (f n + g n::'a::ring)) : UP";
  23.102 -by Auto_tac;
  23.103 -(* instantiate bound for the sum and do case split *)
  23.104 -by (res_inst_tac [("x", "if n<=na then na else n")] exI 1);
  23.105 -by Auto_tac;
  23.106 -(* first case, bound of g higher *)
  23.107 -by (dtac le_bound 1 THEN assume_tac 1);
  23.108 -by (Force_tac 1);
  23.109 -(* second case is identical,
  23.110 -  apart from we have to massage the inequality *)
  23.111 -by (dtac (not_leE RS less_imp_le) 1);
  23.112 -by (dtac le_bound 1 THEN assume_tac 1);
  23.113 -by (Force_tac 1);
  23.114 -qed "UP_closed_add";
  23.115 +Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
  23.116 +by (etac contrapos_np 1); 
  23.117 +by (case_tac "deg p = 0" 1);
  23.118 +by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
  23.119 +by (rtac up_eqI 1);
  23.120 +by (case_tac "n=0" 1);
  23.121 +by (rotate_tac ~2 1);
  23.122 +by (Asm_full_simp_tac 1);
  23.123 +by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  23.124 +qed "nonzero_lcoeff";
  23.125 +
  23.126 +Goal "(deg p <= n) = bound n (Rep_UP p)";
  23.127 +by (rtac iffI 1);
  23.128 +(* ==> *)
  23.129 +by (rtac boundI 1);
  23.130 +by (fold_goals_tac [coeff_def]);
  23.131 +by (rtac deg_aboveD 1);
  23.132 +by (fast_arith_tac 1);
  23.133 +(* <== *)
  23.134 +by (rtac deg_aboveI 1);
  23.135 +by (rewtac coeff_def);
  23.136 +by (Fast_tac 1);
  23.137 +qed "deg_above_is_bound";
  23.138 +
  23.139 +(* Lemmas on the degree function *)
  23.140 +
  23.141 +Goalw [max_def]
  23.142 +  "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
  23.143 +by (case_tac "deg p <= deg q" 1);
  23.144 +(* case deg p <= deg q *)
  23.145 +by (rtac deg_aboveI 1);
  23.146 +by (Asm_simp_tac 1);
  23.147 +by (strip_tac 1);
  23.148 +by (dtac le_less_trans 1);
  23.149 +by (assume_tac 1);
  23.150 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  23.151 +(* case deg p > deg q *)
  23.152 +by (rtac deg_aboveI 1);
  23.153 +by (Asm_simp_tac 1);
  23.154 +by (dtac not_leE 1);
  23.155 +by (strip_tac 1);
  23.156 +by (dtac less_trans 1);
  23.157 +by (assume_tac 1);
  23.158 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  23.159 +qed "deg_add";
  23.160  
  23.161 -Goalw [UP_def]
  23.162 -  "f : UP ==> (%n. (a * f n::'a::ring)) : UP";
  23.163 -by (Force_tac 1);
  23.164 -qed "UP_closed_smult";
  23.165 +Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
  23.166 +by (rtac order_antisym 1);
  23.167 +by (rtac le_trans 1);
  23.168 +by (rtac deg_add 1);
  23.169 +by (Asm_simp_tac 1);
  23.170 +by (rtac deg_belowI 1);
  23.171 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
  23.172 +qed "deg_add_equal";
  23.173 +
  23.174 +Goal "deg (monom m::'a::ring up) <= m";
  23.175 +by (asm_simp_tac 
  23.176 +  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
  23.177 +qed "deg_monom_ring";
  23.178 +
  23.179 +Goal "deg (monom m::'a::domain up) = m";
  23.180 +by (rtac le_anti_sym 1);
  23.181 +(* <= *)
  23.182 +by (rtac deg_monom_ring 1);
  23.183 +(* >= *)
  23.184 +by (asm_simp_tac 
  23.185 +  (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
  23.186 +qed "deg_monom";
  23.187  
  23.188 -Goalw [UP_def]
  23.189 -  "(%n. if m = n then <1> else 0) : UP";
  23.190 -by Auto_tac;
  23.191 -qed "UP_closed_monom";
  23.192 +Goal "!! a::'a::ring. deg (const a) = 0";
  23.193 +by (rtac le_anti_sym 1);
  23.194 +by (rtac deg_aboveI 1);
  23.195 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  23.196 +by (rtac deg_belowI 1);
  23.197 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  23.198 +qed "deg_const";
  23.199 +
  23.200 +Goal "deg (0::'a::ringS up) = 0";
  23.201 +by (rtac le_anti_sym 1);
  23.202 +by (rtac deg_aboveI 1);
  23.203 +by (Simp_tac 1);
  23.204 +by (rtac deg_belowI 1);
  23.205 +by (Simp_tac 1);
  23.206 +qed "deg_zero";
  23.207  
  23.208 -Goalw [UP_def] "(%n. if n = 0 then a else 0) : UP";
  23.209 -by Auto_tac;
  23.210 -qed "UP_closed_const";
  23.211 +Goal "deg (<1>::'a::ring up) = 0";
  23.212 +by (rtac le_anti_sym 1);
  23.213 +by (rtac deg_aboveI 1);
  23.214 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  23.215 +by (rtac deg_belowI 1);
  23.216 +by (Simp_tac 1);
  23.217 +qed "deg_one";
  23.218 +
  23.219 +Goal "!!p::('a::ring) up. deg (-p) = deg p";
  23.220 +by (rtac le_anti_sym 1);
  23.221 +(* <= *)
  23.222 +by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
  23.223 +by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
  23.224 +qed "deg_uminus";
  23.225 +
  23.226 +Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
  23.227  
  23.228  Goal
  23.229 -  "!! f::nat=>'a::ring. \
  23.230 -\    [| bound n f; bound m g; n + m < k |] ==> f i * g (k - i) = 0";
  23.231 -(* Case split: either f i or g (k - i) is zero *)
  23.232 -by (case_tac "n<i" 1);
  23.233 -(* First case, f i is zero *)
  23.234 -by (Force_tac 1);
  23.235 -(* Second case, we have to derive m < k-i *)
  23.236 -by (subgoal_tac "m < k-i" 1);
  23.237 -by (arith_tac 2);
  23.238 -by (Force_tac 1);
  23.239 -qed "bound_mult_zero";
  23.240 +  "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
  23.241 +by (case_tac "a = 0" 1);
  23.242 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
  23.243 +qed "deg_smult_ring";
  23.244  
  23.245 -Goalw [UP_def]
  23.246 -  "[| f : UP; g : UP |] ==> \
  23.247 -\      (%n. (setsum (%i. f i * g (n-i)) {..n}::'a::ring)) : UP";
  23.248 -by (Step_tac 1);
  23.249 -(* Instantiate bound for the product, and remove bound in goal *)
  23.250 -by (res_inst_tac [("x", "n + na")] exI 1);
  23.251 -by (Step_tac 1);
  23.252 -(* Show that the sum is 0 *)
  23.253 -by (asm_simp_tac (simpset() addsimps [bound_mult_zero]) 1);
  23.254 -qed "UP_closed_mult";
  23.255 +Goal
  23.256 +  "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
  23.257 +by (rtac le_anti_sym 1);
  23.258 +by (rtac deg_smult_ring 1);
  23.259 +by (case_tac "a = 0" 1);
  23.260 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
  23.261 +qed "deg_smult";
  23.262  
  23.263 -(* %x. 0 represents a polynomial *)
  23.264 -
  23.265 -Goalw [UP_def] "(%x. 0) : UP";
  23.266 -by (Fast_tac 1);
  23.267 -qed "UP_zero";
  23.268 -
  23.269 -(* Effect of +, *s, monom, * and the other operations on the coefficients *)
  23.270 +Goal
  23.271 +  "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
  23.272 +\       coeff i p * coeff (k - i) q = 0";
  23.273 +by (simp_tac (simpset() addsimps [coeff_def]) 1);
  23.274 +by (rtac bound_mult_zero 1);
  23.275 +by (assume_tac 3);
  23.276 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
  23.277 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
  23.278 +qed "deg_above_mult_zero";
  23.279  
  23.280 -Goalw [coeff_def, up_add_def]
  23.281 -  "coeff n (p+q) = (coeff n p + coeff n q::'a::ring)";
  23.282 -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_add, Rep_UP]) 1);
  23.283 -qed "coeff_add";
  23.284 +Goal
  23.285 +  "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
  23.286 +by (rtac deg_aboveI 1);
  23.287 +by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
  23.288 +qed "deg_mult_ring";
  23.289  
  23.290 -Goalw [coeff_def, up_smult_def]
  23.291 -  "!!a::'a::ring. coeff n (a *s p) = a * coeff n p";
  23.292 -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_smult, Rep_UP]) 1);
  23.293 -qed "coeff_smult";
  23.294 +goal Main.thy 
  23.295 +  "!!k::nat. k < n ==> m < n + m - k";
  23.296 +by (arith_tac 1);
  23.297 +qed "less_add_diff";
  23.298  
  23.299 -Goalw [coeff_def, monom_def]
  23.300 -  "coeff n (monom m) = (if m=n then <1> else 0)";
  23.301 -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_monom, Rep_UP]) 1);
  23.302 -qed "coeff_monom";
  23.303 +Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
  23.304 +(* More general than deg_belowI, and simplifies the next proof! *)
  23.305 +by (rtac deg_belowI 1);
  23.306 +by (Fast_tac 1);
  23.307 +qed "deg_below2I";
  23.308  
  23.309 -Goalw [coeff_def, const_def]
  23.310 -  "coeff n (const a) = (if n=0 then a else 0)";
  23.311 -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const, Rep_UP]) 1);
  23.312 -qed "coeff_const";
  23.313 -
  23.314 -Goalw [coeff_def, up_mult_def]
  23.315 -  "coeff n (p * q) = (setsum (%i. coeff i p * coeff (n-i) q) {..n}::'a::ring)";
  23.316 -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_mult, Rep_UP]) 1);
  23.317 -qed "coeff_mult";
  23.318 -
  23.319 -Goalw [coeff_def, up_zero_def] "coeff n 0 = 0";
  23.320 -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_zero, Rep_UP]) 1);
  23.321 -qed "coeff_zero";
  23.322 -
  23.323 -Addsimps [coeff_add, coeff_smult, coeff_monom, coeff_const, 
  23.324 -	  coeff_mult, coeff_zero];
  23.325 -
  23.326 -Goalw [up_one_def]
  23.327 -  "coeff n <1> = (if n=0 then <1> else 0)";
  23.328 +Goal
  23.329 +  "!! p::'a::domain up. \
  23.330 +\    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
  23.331 +by (rtac le_anti_sym 1);
  23.332 +by (rtac deg_mult_ring 1);
  23.333 +(* deg p + deg q <= deg (p * q) *)
  23.334 +by (rtac deg_below2I 1);
  23.335  by (Simp_tac 1);
  23.336 -qed "coeff_one";
  23.337 +(*
  23.338 +by (rtac conjI 1);
  23.339 +by (rtac impI 1);
  23.340 +*)
  23.341 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
  23.342 +by (rtac le_add1 1);
  23.343 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  23.344 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
  23.345 +by (rtac le_refl 1);
  23.346 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  23.347 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
  23.348 +(*
  23.349 +by (rtac impI 1);
  23.350 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
  23.351 +by (rtac le_add1 1);
  23.352 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  23.353 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
  23.354 +by (rtac le_refl 1);
  23.355 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  23.356 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
  23.357 +*)
  23.358 +qed "deg_mult";
  23.359  
  23.360 -Goalw [up_uminus_def] "coeff n (-p) = (-coeff n p::'a::ring)";
  23.361 -by (simp_tac (simpset() addsimps m_minus) 1);
  23.362 -qed "coeff_uminus";
  23.363 +Addsimps [deg_smult, deg_mult];
  23.364 +
  23.365 +(* Representation theorems about polynomials *)
  23.366  
  23.367 -Addsimps [coeff_one, coeff_uminus];
  23.368 -
  23.369 -(* Polynomials form a ring *)
  23.370 +goal PolyRing.thy
  23.371 +  "!! p::nat=>'a::ring up. \
  23.372 +\    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
  23.373 +by (induct_tac "n" 1);
  23.374 +by Auto_tac;
  23.375 +qed "coeff_SUM";
  23.376  
  23.377 -val prems = Goalw [coeff_def]
  23.378 -  "(!! n. coeff n p = coeff n q) ==> p = q";
  23.379 -by (res_inst_tac [("t", "p")] (Rep_UP_inverse RS subst) 1);
  23.380 -by (res_inst_tac [("t", "q")] (Rep_UP_inverse RS subst) 1);
  23.381 -by (asm_simp_tac (simpset() addsimps prems) 1);
  23.382 -qed "up_eqI";
  23.383 +goal UnivPoly.thy
  23.384 +  "!! f::(nat=>'a::ring). \
  23.385 +\    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
  23.386 +by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
  23.387 +by (auto_tac
  23.388 +    (claset() addDs [not_leE],
  23.389 +     simpset()));
  23.390 +qed "bound_SUM_if";
  23.391  
  23.392 -Goalw [coeff_def]
  23.393 -  "coeff n p ~= coeff n q ==> p ~= q";
  23.394 -by Auto_tac;
  23.395 -qed "up_neqI";
  23.396 -
  23.397 -Goal "!! a::('a::ring) up. (a + b) + c = a + (b + c)";
  23.398 -by (rtac up_eqI 1);
  23.399 -by (Simp_tac 1);
  23.400 -by (rtac a_assoc 1);
  23.401 -qed "up_a_assoc";
  23.402 -
  23.403 -Goal "!! a::('a::ring) up. 0 + a = a";
  23.404 +Goal
  23.405 +  "!! p::'a::ring up. deg p <= n ==> \
  23.406 +\  setsum (%i. coeff i p *s monom i) {..n} = p";
  23.407  by (rtac up_eqI 1);
  23.408 -by (Simp_tac 1);
  23.409 -qed "up_l_zero";
  23.410 -
  23.411 -Goal "!! a::('a::ring) up. (-a) + a = 0";
  23.412 -by (rtac up_eqI 1);
  23.413 -by (Simp_tac 1);
  23.414 -qed "up_l_neg";
  23.415 -
  23.416 -Goal "!! a::('a::ring) up. a + b = b + a";
  23.417 -by (rtac up_eqI 1);
  23.418 -by (Simp_tac 1);
  23.419 -by (rtac a_comm 1);
  23.420 -qed "up_a_comm";
  23.421 -
  23.422 -Goal "!! a::('a::ring) up. (a * b) * c = a * (b * c)";
  23.423 -by (rtac up_eqI 1);
  23.424 -by (Simp_tac 1);
  23.425 -by (rtac poly_assoc_lemma 1);
  23.426 -qed "up_m_assoc";
  23.427 -
  23.428 -Goal "!! a::('a::ring) up. <1> * a = a";
  23.429 -by (rtac up_eqI 1);
  23.430 -by (Simp_tac 1);
  23.431 -by (case_tac "n" 1); 
  23.432 -(* 0 case *)
  23.433 -by (Asm_simp_tac 1);
  23.434 -(* Suc case *)
  23.435 -by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
  23.436 -qed "up_l_one";
  23.437 -
  23.438 -Goal "!! a::('a::ring) up. (a + b) * c = a * c + b * c";
  23.439 -by (rtac up_eqI 1);
  23.440 -by (simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
  23.441 -qed "up_l_distr";
  23.442 -
  23.443 -Goal "!! a::('a::ring) up. a * b = b * a";
  23.444 -by (rtac up_eqI 1);
  23.445 -by (cut_inst_tac [("a", "%i. coeff i a"), ("b", "%i. coeff i b")]
  23.446 -  poly_comm_lemma 1);
  23.447 -by (asm_full_simp_tac (simpset() addsimps [m_comm]) 1);
  23.448 -qed "up_m_comm";
  23.449 -
  23.450 -(* Further algebraic rules *)
  23.451 -
  23.452 -Goal "!! a::'a::ring. const a * p = a *s p";
  23.453 -by (rtac up_eqI 1);
  23.454 -by (case_tac "n" 1); 
  23.455 -by (Asm_simp_tac 1);
  23.456 -by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
  23.457 -qed "const_mult_is_smult";
  23.458 -
  23.459 -Goal "!! a::'a::ring. const (a + b) = const a + const b";
  23.460 -by (rtac up_eqI 1);
  23.461 -by (Simp_tac 1);
  23.462 -qed "const_add";
  23.463 -
  23.464 -Goal "!! a::'a::ring. const (a * b) = const a * const b";
  23.465 -by (simp_tac (simpset() addsimps [const_mult_is_smult]) 1);
  23.466 -by (rtac up_eqI 1);
  23.467 -by (Simp_tac 1);
  23.468 -qed "const_mult";
  23.469 -
  23.470 -Goal "const (<1>::'a::ring) = <1>";
  23.471 -by (rtac up_eqI 1);
  23.472 -by (Simp_tac 1);
  23.473 -qed "const_one";
  23.474 -
  23.475 -Goal "const (0::'a::ring) = 0";
  23.476 -by (rtac up_eqI 1);
  23.477 -by (Simp_tac 1);
  23.478 -qed "const_zero";
  23.479 -
  23.480 -Addsimps [const_add, const_mult, const_one, const_zero];
  23.481 -
  23.482 -Goalw [inj_on_def, UNIV_def, const_def] "inj const";
  23.483 -by (Simp_tac 1);
  23.484 -by (strip_tac 1);
  23.485 -by (dres_inst_tac [("f", "Rep_UP")] arg_cong 1);
  23.486 -by (full_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const,
  23.487 -				       expand_fun_eq]) 1);
  23.488 -by (dres_inst_tac [("x", "0")] spec 1);
  23.489 -by (Full_simp_tac 1);
  23.490 -qed "const_inj";
  23.491 -
  23.492 -(*Lemma used in PolyHomo*)
  23.493 -Goal
  23.494 -  "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \
  23.495 -\    setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \
  23.496 -\    setsum f {..n} * setsum g {..m}";
  23.497 -by (simp_tac (simpset() addsimps [SUM_ldistr, DiagSum]) 1);
  23.498 -(* SUM_rdistr must be applied after SUM_ldistr ! *)
  23.499 -by (simp_tac (simpset() addsimps [SUM_rdistr]) 1);
  23.500 -by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
  23.501 -by (rtac le_add1 1);
  23.502 -by (Force_tac 1);
  23.503 +by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
  23.504 +by (rtac trans 1);
  23.505 +by (res_inst_tac [("x", "na")] bound_SUM_if 2);
  23.506 +by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
  23.507  by (rtac SUM_cong 1);
  23.508  by (rtac refl 1);
  23.509 -by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
  23.510 -by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
  23.511 -by Auto_tac;
  23.512 -qed "CauchySum";
  23.513 +by (Asm_simp_tac 1);
  23.514 +qed "up_repr";
  23.515 +
  23.516 +Goal
  23.517 +  "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
  23.518 +\  P (setsum (%i. coeff i p *s monom i) {..n})";
  23.519 +by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
  23.520 +qed "up_reprD";
  23.521 +
  23.522 +Goal
  23.523 +  "!! p::'a::ring up. \
  23.524 +\  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
  23.525 +\    ==> P p";
  23.526 +by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
  23.527 +qed "up_repr2D";
  23.528 +
  23.529 +(*
  23.530 +Goal
  23.531 +  "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
  23.532 +\    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
  23.533 +\    = (coeff k f = coeff k g)
  23.534 +...
  23.535 +qed "up_unique";
  23.536 +*)
  23.537 +
  23.538 +(* Polynomials over integral domains are again integral domains *)
  23.539  
  23.540 -Goal "<1> ~= (0::('a::domain) up)";
  23.541 -by (res_inst_tac [("n", "0")] up_neqI 1);
  23.542 +Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
  23.543 +by (rtac classical 1);
  23.544 +by (subgoal_tac "deg p = 0 & deg q = 0" 1);
  23.545 +by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
  23.546 +by (Asm_simp_tac 1);
  23.547 +by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
  23.548 +by (Asm_simp_tac 1);
  23.549 +by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
  23.550 +by (force_tac (claset() addIs [up_eqI], simpset()) 1);
  23.551 +by (rtac integral 1);
  23.552 +by (subgoal_tac "coeff 0 (p * q) = 0" 1);
  23.553 +by (Asm_simp_tac 2);
  23.554 +by (Full_simp_tac 1);
  23.555 +by (dres_inst_tac [("f", "deg")] arg_cong 1);
  23.556 +by (Asm_full_simp_tac 1);
  23.557 +qed "up_integral";
  23.558 +
  23.559 +Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
  23.560 +by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
  23.561 +by (dtac up_integral 1);
  23.562 +by Auto_tac;
  23.563 +by (rtac (const_inj RS injD) 1);
  23.564  by (Simp_tac 1);
  23.565 -qed "up_one_not_zero";
  23.566 +qed "smult_integral";
  23.567 +*)
  23.568 +
  23.569 +(* Divisibility and degree *)
  23.570 +
  23.571 +Goalw [dvd_def]
  23.572 +  "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
  23.573 +by (etac exE 1);
  23.574 +by (hyp_subst_tac 1);
  23.575 +by (case_tac "p = 0" 1);
  23.576 +by (case_tac "k = 0" 2);
  23.577 +by Auto_tac;
  23.578 +qed "dvd_imp_deg";
    24.1 --- a/src/HOL/Algebra/poly/UnivPoly.thy	Wed Nov 27 17:25:41 2002 +0100
    24.2 +++ b/src/HOL/Algebra/poly/UnivPoly.thy	Thu Nov 28 10:50:42 2002 +0100
    24.3 @@ -1,44 +1,748 @@
    24.4  (*
    24.5 -    Univariate Polynomials
    24.6 -    $Id$
    24.7 -    Author: Clemens Ballarin, started 9 December 1996
    24.8 +  Title:     Univariate Polynomials
    24.9 +  Id:        $Id$
   24.10 +  Author:    Clemens Ballarin, started 9 December 1996
   24.11 +  Copyright: Clemens Ballarin
   24.12 +*)
   24.13 +
   24.14 +header {* Univariate Polynomials *}
   24.15 +
   24.16 +theory UnivPoly = Abstract:
   24.17 +
   24.18 +(* already proved in Finite_Set.thy
   24.19 +
   24.20 +lemma setsum_cong:
   24.21 +  "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
   24.22 +proof -
   24.23 +  assume prems: "A = B" "!!i. i : B ==> f i = g i"
   24.24 +  show ?thesis
   24.25 +  proof (cases "finite B")
   24.26 +    case True
   24.27 +    then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
   24.28 +      setsum f A = setsum g B"
   24.29 +    proof induct
   24.30 +      case empty thus ?case by simp
   24.31 +    next
   24.32 +      case insert thus ?case by simp
   24.33 +    qed
   24.34 +    with prems show ?thesis by simp
   24.35 +  next
   24.36 +    case False with prems show ?thesis by (simp add: setsum_def)
   24.37 +  qed
   24.38 +qed
   24.39  *)
   24.40  
   24.41 -UnivPoly = ProtoPoly +
   24.42 +(* Instruct simplifier to simplify assumptions introduced by congs.
   24.43 +   This makes setsum_cong more convenient to use, because assumptions
   24.44 +   like i:{m..n} get simplified (to m <= i & i <= n). *)
   24.45 +
   24.46 +ML_setup {* 
   24.47 +
   24.48 +Addcongs [thm "setsum_cong"];
   24.49 +Context.>> (fn thy => (simpset_ref_of thy :=
   24.50 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   24.51 +
   24.52 +section {* Definition of type up *}
   24.53 +
   24.54 +constdefs
   24.55 +  bound  :: "[nat, nat => 'a::zero] => bool"
   24.56 +  "bound n f == (ALL i. n < i --> f i = 0)"
   24.57 +
   24.58 +lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
   24.59 +proof (unfold bound_def)
   24.60 +qed fast
   24.61 +
   24.62 +lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
   24.63 +proof (unfold bound_def)
   24.64 +qed fast
   24.65 +
   24.66 +lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
   24.67 +proof (unfold bound_def)
   24.68 +qed fast
   24.69 +
   24.70 +lemma bound_below:
   24.71 +  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
   24.72 +proof (rule classical)
   24.73 +  assume "~ ?thesis"
   24.74 +  then have "m < n" by arith
   24.75 +  with bound have "f n = 0" ..
   24.76 +  with nonzero show ?thesis by contradiction
   24.77 +qed
   24.78  
   24.79  typedef (UP)
   24.80 -  ('a) up = "{f :: nat => 'a::ringS. EX n. bound n f}" (UP_witness)
   24.81 +  ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
   24.82 +by (rule+)   (* Question: what does trace_rule show??? *)
   24.83  
   24.84 -instance
   24.85 -  up :: (ringS) ringS
   24.86 +section {* Constants *}
   24.87  
   24.88  consts
   24.89 -  coeff		:: [nat, 'a up] => 'a::ringS
   24.90 -  "*s"		:: ['a::ringS, 'a up] => 'a up		(infixl 70)
   24.91 -  monom		:: nat => ('a::ringS) up
   24.92 -  const		:: 'a::ringS => 'a up
   24.93 +  coeff  :: "['a up, nat] => ('a::zero)"
   24.94 +  monom  :: "['a::zero, nat] => 'a up"              ("(3_*X^/_)" [71, 71] 70)
   24.95 +  "*s"   :: "['a::{zero, times}, 'a up] => 'a up"   (infixl 70)
   24.96 +
   24.97 +defs
   24.98 +  coeff_def: "coeff p n == Rep_UP p n"
   24.99 +  monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
  24.100 +  smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
  24.101  
  24.102 -  "*X^"		:: ['a, nat] => 'a up		("(3_*X^/_)" [71, 71] 70)
  24.103 +lemma coeff_bound_ex: "EX n. bound n (coeff p)"
  24.104 +proof -
  24.105 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  24.106 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  24.107 +  then show ?thesis ..
  24.108 +qed
  24.109 +  
  24.110 +lemma bound_coeff_obtain:
  24.111 +  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
  24.112 +proof -
  24.113 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  24.114 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  24.115 +  with prem show P .
  24.116 +qed
  24.117  
  24.118 -translations
  24.119 -  "a *X^ n"	== "a *s monom n"
  24.120 -  (* this translation is only nice for non-nested polynomials *)
  24.121 +text {* Ring operations *}
  24.122 +
  24.123 +instance up :: (zero) zero ..
  24.124 +instance up :: (one) one ..
  24.125 +instance up :: (plus) plus ..
  24.126 +instance up :: (minus) minus ..
  24.127 +instance up :: (times) times ..
  24.128 +instance up :: (inverse) inverse ..
  24.129 +instance up :: (power) power ..
  24.130  
  24.131  defs
  24.132 -  coeff_def	"coeff n p == Rep_UP p n"
  24.133 -  up_add_def	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
  24.134 -  up_smult_def	"a *s p == Abs_UP (%n. a * Rep_UP p n)"
  24.135 -  monom_def	"monom m == Abs_UP (%n. if m=n then <1> else 0)"
  24.136 -  const_def	"const a == Abs_UP (%n. if n=0 then a else 0)"
  24.137 -  up_mult_def	"p * q == Abs_UP (%n::nat. setsum
  24.138 +  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
  24.139 +  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
  24.140  		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
  24.141 +  up_zero_def:  "0 == monom 0 0"
  24.142 +  up_one_def:   "1 == monom 1 0"
  24.143 +  up_uminus_def:"- p == (- 1) *s p"
  24.144 +                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
  24.145 +                (* note: - 1 is different from -1; latter is of class number *)
  24.146 +
  24.147 +  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
  24.148 +  up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == 
  24.149 +                     (if a dvd 1 then THE x. a*x = 1 else 0)"
  24.150 +  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
  24.151 +  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
  24.152 +                     nat_rec 1 (%u b. b * a) n"
  24.153 +
  24.154 +subsection {* Effect of operations on coefficients *}
  24.155 +
  24.156 +lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
  24.157 +proof -
  24.158 +  have "(%n. if n = m then a else 0) : UP"
  24.159 +    using UP_def by force
  24.160 +  from this show ?thesis
  24.161 +    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
  24.162 +qed
  24.163 +
  24.164 +lemma coeff_zero [simp]: "coeff 0 n = 0"
  24.165 +proof (unfold up_zero_def)
  24.166 +qed simp
  24.167 +
  24.168 +lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
  24.169 +proof (unfold up_one_def)
  24.170 +qed simp
  24.171 +
  24.172 +lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
  24.173 +proof -
  24.174 +  have "!!f. f : UP ==> (%n. a * f n) : UP"
  24.175 +    by (unfold UP_def) (force simp add: ring_simps)
  24.176 +      (* this force step is slow *)
  24.177 +  then show ?thesis
  24.178 +    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
  24.179 +qed
  24.180 +
  24.181 +lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
  24.182 +proof -
  24.183 +  {
  24.184 +    fix f g
  24.185 +    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  24.186 +    have "(%i. f i + g i) : UP"
  24.187 +    proof -
  24.188 +      from fup obtain n where boundn: "bound n f"
  24.189 +	by (unfold UP_def) fast
  24.190 +      from gup obtain m where boundm: "bound m g"
  24.191 +	by (unfold UP_def) fast
  24.192 +      have "bound (max n m) (%i. (f i + g i))"
  24.193 +      proof
  24.194 +	fix i
  24.195 +	assume "max n m < i"
  24.196 +	with boundn and boundm show "f i + g i = 0"
  24.197 +          by (fastsimp simp add: ring_simps)
  24.198 +      qed
  24.199 +      then show "(%i. (f i + g i)) : UP"
  24.200 +	by (unfold UP_def) fast
  24.201 +    qed
  24.202 +  }
  24.203 +  then show ?thesis
  24.204 +    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
  24.205 +qed
  24.206 +
  24.207 +lemma coeff_mult [simp]:
  24.208 +  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
  24.209 +proof -
  24.210 +  {
  24.211 +    fix f g
  24.212 +    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  24.213 +    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  24.214 +    proof -
  24.215 +      from fup obtain n where "bound n f"
  24.216 +	by (unfold UP_def) fast
  24.217 +      from gup obtain m where "bound m g"
  24.218 +	by (unfold UP_def) fast
  24.219 +      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
  24.220 +      proof
  24.221 +	fix k
  24.222 +	assume bound: "n + m < k"
  24.223 +	{
  24.224 +	  fix i
  24.225 +	  have "f i * g (k-i) = 0"
  24.226 +	  proof cases
  24.227 +	    assume "n < i"
  24.228 +	    show ?thesis by (auto! simp add: ring_simps)
  24.229 +	  next
  24.230 +	    assume "~ (n < i)"
  24.231 +	    with bound have "m < k-i" by arith
  24.232 +	    then show ?thesis by (auto! simp add: ring_simps)
  24.233 +	  qed
  24.234 +	}
  24.235 +	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
  24.236 +	  by (simp add: ring_simps)
  24.237 +      qed
  24.238 +      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  24.239 +	by (unfold UP_def) fast
  24.240 +    qed
  24.241 +  }
  24.242 +  then show ?thesis
  24.243 +    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
  24.244 +qed
  24.245 +
  24.246 +lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
  24.247 +by (unfold up_uminus_def) (simp add: ring_simps)
  24.248 +
  24.249 +(* Other lemmas *)
  24.250 +
  24.251 +lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
  24.252 +proof -
  24.253 +  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
  24.254 +  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
  24.255 +  also have "... = q" by (simp add: Rep_UP_inverse)
  24.256 +  finally show ?thesis .
  24.257 +qed
  24.258 +
  24.259 +(* ML_setup {* Addsimprocs [ring_simproc] *} *)
  24.260 +
  24.261 +instance up :: (ring) ring
  24.262 +proof
  24.263 +  fix p q r :: "'a::ring up"
  24.264 +  fix n
  24.265 +  show "(p + q) + r = p + (q + r)"
  24.266 +    by (rule up_eqI) simp
  24.267 +  show "0 + p = p"
  24.268 +    by (rule up_eqI) simp
  24.269 +  show "(-p) + p = 0"
  24.270 +    by (rule up_eqI) simp
  24.271 +  show "p + q = q + p"
  24.272 +    by (rule up_eqI) simp
  24.273 +  show "(p * q) * r = p * (q * r)"
  24.274 +  proof (rule up_eqI)
  24.275 +    fix n 
  24.276 +    {
  24.277 +      fix k and a b c :: "nat=>'a::ring"
  24.278 +      have "k <= n ==> 
  24.279 +	setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
  24.280 +	setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
  24.281 +	(is "_ ==> ?eq k")
  24.282 +      proof (induct k)
  24.283 +	case 0 show ?case by simp
  24.284 +      next
  24.285 +	case (Suc k)
  24.286 +	then have "k <= n" by arith
  24.287 +	then have "?eq k" by (rule Suc)
  24.288 +	then show ?case
  24.289 +	  by (simp add: Suc_diff_le natsum_ldistr)
  24.290 +      qed
  24.291 +    }
  24.292 +    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
  24.293 +      by simp
  24.294 +  qed
  24.295 +  show "1 * p = p"
  24.296 +  proof (rule up_eqI)
  24.297 +    fix n
  24.298 +    show "coeff (1 * p) n = coeff p n"
  24.299 +    proof (cases n)
  24.300 +      case 0 then show ?thesis by simp
  24.301 +    next
  24.302 +      case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
  24.303 +    qed
  24.304 +  qed
  24.305 +  show "(p + q) * r = p * r + q * r"
  24.306 +    by (rule up_eqI) simp
  24.307 +  show "p * q = q * p"
  24.308 +  proof (rule up_eqI)
  24.309 +    fix n 
  24.310 +    {
  24.311 +      fix k
  24.312 +      fix a b :: "nat=>'a::ring"
  24.313 +      have "k <= n ==> 
  24.314 +	setsum (%i. a i * b (n-i)) {..k} =
  24.315 +	setsum (%i. a (k-i) * b (i+n-k)) {..k}"
  24.316 +	(is "_ ==> ?eq k")
  24.317 +      proof (induct k)
  24.318 +	case 0 show ?case by simp
  24.319 +      next
  24.320 +	case (Suc k) then show ?case by (subst natsum_Suc2) simp
  24.321 +      qed
  24.322 +    }
  24.323 +    then show "coeff (p * q) n = coeff (q * p) n"
  24.324 +      by simp
  24.325 +  qed
  24.326 +
  24.327 +  show "p - q = p + (-q)"
  24.328 +    by (simp add: up_minus_def)
  24.329 +  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
  24.330 +    by (simp add: up_inverse_def)
  24.331 +  show "p / q = p * inverse q"
  24.332 +    by (simp add: up_divide_def)
  24.333 +  show "p ^ n = nat_rec 1 (%u b. b * p) n"
  24.334 +    by (simp add: up_power_def)
  24.335 +  qed
  24.336 +
  24.337 +(* Further properties of monom *)
  24.338 +
  24.339 +lemma monom_zero [simp]:
  24.340 +  "monom 0 n = 0"
  24.341 +  by (simp add: monom_def up_zero_def)
  24.342 +
  24.343 +lemma monom_mult_is_smult:
  24.344 +  "monom (a::'a::ring) 0 * p = a *s p"
  24.345 +proof (rule up_eqI)
  24.346 +  fix k
  24.347 +  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
  24.348 +  proof (cases k)
  24.349 +    case 0 then show ?thesis by simp
  24.350 +  next
  24.351 +    case Suc then show ?thesis by simp
  24.352 +  qed
  24.353 +qed
  24.354 +
  24.355 +lemma monom_add [simp]:
  24.356 +  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
  24.357 +by (rule up_eqI) simp
  24.358 +
  24.359 +lemma monom_mult_smult:
  24.360 +  "monom (a * b) n = a *s monom (b::'a::ring) n"
  24.361 +by (rule up_eqI) simp
  24.362 +
  24.363 +lemma monom_uminus [simp]:
  24.364 +  "monom (-a) n = - monom (a::'a::ring) n"
  24.365 +by (rule up_eqI) simp
  24.366 +
  24.367 +lemma monom_one [simp]:
  24.368 +  "monom 1 0 = 1"
  24.369 +by (simp add: up_one_def)
  24.370 +
  24.371 +lemma monom_inj:
  24.372 +  "(monom a n = monom b n) = (a = b)"
  24.373 +proof
  24.374 +  assume "monom a n = monom b n"
  24.375 +  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
  24.376 +  then show "a = b" by simp
  24.377 +next
  24.378 +  assume "a = b" then show "monom a n = monom b n" by simp
  24.379 +qed
  24.380 +
  24.381 +(* Properties of *s:
  24.382 +   Polynomials form a module *)
  24.383 +
  24.384 +lemma smult_l_distr:
  24.385 +  "(a + b::'a::ring) *s p = a *s p + b *s p"
  24.386 +by (rule up_eqI) simp
  24.387 +
  24.388 +lemma smult_r_distr:
  24.389 +  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
  24.390 +by (rule up_eqI) simp
  24.391 +
  24.392 +lemma smult_assoc1:
  24.393 +  "(a * b::'a::ring) *s p = a *s (b *s p)"
  24.394 +by (rule up_eqI) simp
  24.395 +
  24.396 +lemma smult_one [simp]:
  24.397 +  "(1::'a::ring) *s p = p"
  24.398 +by (rule up_eqI) simp
  24.399 +
  24.400 +(* Polynomials form an algebra *)
  24.401 +
  24.402 +ML_setup {* Delsimprocs [ring_simproc] *}
  24.403 +
  24.404 +lemma smult_assoc2:
  24.405 +  "(a *s p) * q = (a::'a::ring) *s (p * q)"
  24.406 +by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
  24.407 +(* Simproc fails. *)
  24.408 +
  24.409 +ML_setup {* Addsimprocs [ring_simproc] *}
  24.410 +
  24.411 +(* the following can be derived from the above ones,
  24.412 +   for generality reasons, it is therefore done *)
  24.413 +
  24.414 +lemma smult_l_null [simp]:
  24.415 +  "(0::'a::ring) *s p = 0"
  24.416 +proof -
  24.417 +  fix a
  24.418 +  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
  24.419 +  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
  24.420 +  also have "... = 0" by simp
  24.421 +  finally show ?thesis .
  24.422 +qed
  24.423 +
  24.424 +lemma smult_r_null [simp]:
  24.425 +  "(a::'a::ring) *s 0 = 0";
  24.426 +proof -
  24.427 +  fix p
  24.428 +  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
  24.429 +  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
  24.430 +  also have "... = 0" by simp
  24.431 +  finally show ?thesis .
  24.432 +qed
  24.433 +
  24.434 +lemma smult_l_minus:
  24.435 +  "(-a::'a::ring) *s p = - (a *s p)"
  24.436 +proof -
  24.437 +  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
  24.438 +  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
  24.439 +  also have "... = -(a *s p)" by simp
  24.440 +  finally show ?thesis .
  24.441 +qed
  24.442 +
  24.443 +lemma smult_r_minus:
  24.444 +  "(a::'a::ring) *s (-p) = - (a *s p)"
  24.445 +proof -
  24.446 +  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
  24.447 +  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
  24.448 +  also have "... = -(a *s p)" by simp
  24.449 +  finally show ?thesis .
  24.450 +qed
  24.451 +
  24.452 +section {* The degree function *}
  24.453  
  24.454 -  up_zero_def	"0 == Abs_UP (%x. 0)"
  24.455 -  up_one_def	"<1> == monom 0"
  24.456 -  up_uminus_def	"- p == (-<1>) *s p"
  24.457 -  up_inverse_def "inverse (a::'a::ringS up) == (if a dvd <1> then @x. a*x = <1> else 0)"
  24.458 -  up_divide_def "(a::'a::ringS up) / b == a * inverse b"
  24.459 -  up_power_def	"a ^ n == nat_rec (<1>::('a::ringS) up) (%u b. b * a) n"
  24.460 -end
  24.461 +constdefs
  24.462 +  deg :: "('a::zero) up => nat"
  24.463 +  "deg p == LEAST n. bound n (coeff p)"
  24.464 +
  24.465 +lemma deg_aboveI:
  24.466 +  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
  24.467 +by (unfold deg_def) (fast intro: Least_le)
  24.468 +
  24.469 +lemma deg_aboveD:
  24.470 +  assumes prem: "deg p < m" shows "coeff p m = 0"
  24.471 +proof -
  24.472 +  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
  24.473 +  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
  24.474 +  then show "coeff p m = 0" by (rule boundD)
  24.475 +qed
  24.476 +
  24.477 +lemma deg_belowI:
  24.478 +  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
  24.479 +(* logically, this is a slightly stronger version of deg_aboveD *)
  24.480 +proof (cases "n=0")
  24.481 +  case True then show ?thesis by simp
  24.482 +next
  24.483 +  case False then have "coeff p n ~= 0" by (rule prem)
  24.484 +  then have "~ deg p < n" by (fast dest: deg_aboveD)
  24.485 +  then show ?thesis by arith
  24.486 +qed
  24.487 +
  24.488 +lemma lcoeff_nonzero_deg:
  24.489 +  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
  24.490 +proof -
  24.491 +  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
  24.492 +  proof -
  24.493 +    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
  24.494 +      by arith (* make public?, why does proof not work with "1" *)
  24.495 +    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
  24.496 +      by (unfold deg_def) arith
  24.497 +    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
  24.498 +    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
  24.499 +      by (unfold bound_def) fast
  24.500 +    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
  24.501 +    then show ?thesis by auto 
  24.502 +  qed
  24.503 +  with deg_belowI have "deg p = m" by fastsimp
  24.504 +  with m_coeff show ?thesis by simp
  24.505 +qed
  24.506 +
  24.507 +lemma lcoeff_nonzero_nonzero:
  24.508 +  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
  24.509 +proof -
  24.510 +  have "EX m. coeff p m ~= 0"
  24.511 +  proof (rule classical)
  24.512 +    assume "~ ?thesis"
  24.513 +    then have "p = 0" by (auto intro: up_eqI)
  24.514 +    with nonzero show ?thesis by contradiction
  24.515 +  qed
  24.516 +  then obtain m where coeff: "coeff p m ~= 0" ..
  24.517 +  then have "m <= deg p" by (rule deg_belowI)
  24.518 +  then have "m = 0" by (simp add: deg)
  24.519 +  with coeff show ?thesis by simp
  24.520 +qed
  24.521 +
  24.522 +lemma lcoeff_nonzero:
  24.523 +  "p ~= 0 ==> coeff p (deg p) ~= 0"
  24.524 +proof (cases "deg p = 0")
  24.525 +  case True
  24.526 +  assume "p ~= 0"
  24.527 +  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
  24.528 +next
  24.529 +  case False
  24.530 +  assume "p ~= 0"
  24.531 +  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
  24.532 +qed
  24.533 +
  24.534 +lemma deg_eqI:
  24.535 +  "[| !!m. n < m ==> coeff p m = 0;
  24.536 +      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
  24.537 +by (fast intro: le_anti_sym deg_aboveI deg_belowI)
  24.538 +
  24.539 +(* Degree and polynomial operations *)
  24.540 +
  24.541 +lemma deg_add [simp]:
  24.542 +  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
  24.543 +proof (cases "deg p <= deg q")
  24.544 +  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
  24.545 +next
  24.546 +  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
  24.547 +qed
  24.548 +
  24.549 +lemma deg_monom_ring:
  24.550 +  "deg (monom a n::'a::ring up) <= n"
  24.551 +by (rule deg_aboveI) simp
  24.552 +
  24.553 +lemma deg_monom [simp]:
  24.554 +  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
  24.555 +by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
  24.556 +
  24.557 +lemma deg_const [simp]:
  24.558 +  "deg (monom (a::'a::ring) 0) = 0"
  24.559 +proof (rule le_anti_sym)
  24.560 +  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
  24.561 +next
  24.562 +  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
  24.563 +qed
  24.564 +
  24.565 +lemma deg_zero [simp]:
  24.566 +  "deg 0 = 0"
  24.567 +proof (rule le_anti_sym)
  24.568 +  show "deg 0 <= 0" by (rule deg_aboveI) simp
  24.569 +next
  24.570 +  show "0 <= deg 0" by (rule deg_belowI) simp
  24.571 +qed
  24.572 +
  24.573 +lemma deg_one [simp]:
  24.574 +  "deg 1 = 0"
  24.575 +proof (rule le_anti_sym)
  24.576 +  show "deg 1 <= 0" by (rule deg_aboveI) simp
  24.577 +next
  24.578 +  show "0 <= deg 1" by (rule deg_belowI) simp
  24.579 +qed
  24.580 +
  24.581 +lemma uminus_monom:
  24.582 +  "!!a::'a::ring. (-a = 0) = (a = 0)"
  24.583 +proof
  24.584 +  fix a::"'a::ring"
  24.585 +  assume "a = 0"
  24.586 +  then show "-a = 0" by simp
  24.587 +next
  24.588 +  fix a::"'a::ring"
  24.589 +  assume "- a = 0"
  24.590 +  then have "-(- a) = 0" by simp
  24.591 +  then show "a = 0" by simp
  24.592 +qed
  24.593 +
  24.594 +lemma deg_uminus [simp]:
  24.595 +  "deg (-p::('a::ring) up) = deg p"
  24.596 +proof (rule le_anti_sym)
  24.597 +  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
  24.598 +next
  24.599 +  show "deg p <= deg (- p)" 
  24.600 +  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
  24.601 +qed
  24.602 +
  24.603 +lemma deg_smult_ring:
  24.604 +  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
  24.605 +proof (cases "a = 0")
  24.606 +qed (simp add: deg_aboveI deg_aboveD)+
  24.607 +
  24.608 +lemma deg_smult [simp]:
  24.609 +  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
  24.610 +proof (rule le_anti_sym)
  24.611 +  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
  24.612 +next
  24.613 +  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
  24.614 +  proof (cases "a = 0")
  24.615 +  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
  24.616 +qed
  24.617  
  24.618 +lemma deg_mult_ring:
  24.619 +  "deg (p * q::'a::ring up) <= deg p + deg q"
  24.620 +proof (rule deg_aboveI)
  24.621 +  fix m
  24.622 +  assume boundm: "deg p + deg q < m"
  24.623 +  {
  24.624 +    fix k i
  24.625 +    assume boundk: "deg p + deg q < k"
  24.626 +    then have "coeff p i * coeff q (k - i) = 0"
  24.627 +    proof (cases "deg p < i")
  24.628 +      case True then show ?thesis by (simp add: deg_aboveD)
  24.629 +    next
  24.630 +      case False with boundk have "deg q < k - i" by arith
  24.631 +      then show ?thesis by (simp add: deg_aboveD)
  24.632 +    qed
  24.633 +  }
  24.634 +      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
  24.635 +         proofs. *)
  24.636 +  with boundm show "coeff (p * q) m = 0" by simp
  24.637 +qed
  24.638  
  24.639 +lemma deg_mult [simp]:
  24.640 +  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
  24.641 +proof (rule le_anti_sym)
  24.642 +  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
  24.643 +next
  24.644 +  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
  24.645 +  assume nz: "p ~= 0" "q ~= 0"
  24.646 +  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
  24.647 +  show "deg p + deg q <= deg (p * q)"
  24.648 +  proof (rule deg_belowI, simp)
  24.649 +    have "setsum ?s {.. deg p + deg q}
  24.650 +      = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
  24.651 +      by (simp only: ivl_disj_un_one)
  24.652 +    also have "... = setsum ?s {deg p .. deg p + deg q}"
  24.653 +      by (simp add: setsum_Un_disjoint ivl_disj_int_one
  24.654 +        setsum_0 deg_aboveD less_add_diff)
  24.655 +    also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
  24.656 +      by (simp only: ivl_disj_un_singleton)
  24.657 +    also have "... = coeff p (deg p) * coeff q (deg q)" 
  24.658 +      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  24.659 +        setsum_0 deg_aboveD)
  24.660 +    finally have "setsum ?s {.. deg p + deg q} 
  24.661 +      = coeff p (deg p) * coeff q (deg q)" .
  24.662 +    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
  24.663 +      by (simp add: integral_iff lcoeff_nonzero)
  24.664 +    qed
  24.665 +  qed
  24.666 +
  24.667 +lemma coeff_natsum:
  24.668 +  "((coeff (setsum p A) k)::'a::ring) = 
  24.669 +   setsum (%i. coeff (p i) k) A"
  24.670 +proof (cases "finite A")
  24.671 +  case True then show ?thesis by induct auto
  24.672 +next
  24.673 +  case False then show ?thesis by (simp add: setsum_def)
  24.674 +qed
  24.675 +(* Instance of a more general result!!! *)
  24.676 +
  24.677 +(*
  24.678 +lemma coeff_natsum:
  24.679 +  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
  24.680 +   setsum (%i. coeff (p i) k) {..n}"
  24.681 +by (induct n) auto
  24.682 +*)
  24.683 +
  24.684 +lemma up_repr:
  24.685 +  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
  24.686 +proof (rule up_eqI)
  24.687 +  let ?s = "(%i. monom (coeff p i) i)"
  24.688 +  fix k
  24.689 +  show "coeff (setsum ?s {..deg p}) k = coeff p k"
  24.690 +  proof (cases "k <= deg p")
  24.691 +    case True
  24.692 +    hence "coeff (setsum ?s {..deg p}) k = 
  24.693 +          coeff (setsum ?s ({..k} Un {)k..deg p})) k"
  24.694 +      by (simp only: ivl_disj_un_one)
  24.695 +    also from True
  24.696 +    have "... = coeff (setsum ?s {..k}) k"
  24.697 +      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
  24.698 +        setsum_0 coeff_natsum )
  24.699 +    also
  24.700 +    have "... = coeff (setsum ?s ({..k(} Un {k})) k"
  24.701 +      by (simp only: ivl_disj_un_singleton)
  24.702 +    also have "... = coeff p k"
  24.703 +      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  24.704 +        setsum_0 coeff_natsum deg_aboveD)
  24.705 +    finally show ?thesis .
  24.706 +  next
  24.707 +    case False
  24.708 +    hence "coeff (setsum ?s {..deg p}) k = 
  24.709 +          coeff (setsum ?s ({..deg p(} Un {deg p})) k"
  24.710 +      by (simp only: ivl_disj_un_singleton)
  24.711 +    also from False have "... = coeff p k"
  24.712 +      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  24.713 +        setsum_0 coeff_natsum deg_aboveD)
  24.714 +    finally show ?thesis .
  24.715 +  qed
  24.716 +qed
  24.717 +
  24.718 +lemma up_repr_le:
  24.719 +  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
  24.720 +proof -
  24.721 +  let ?s = "(%i. monom (coeff p i) i)"
  24.722 +  assume "deg p <= n"
  24.723 +  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
  24.724 +    by (simp only: ivl_disj_un_one)
  24.725 +  also have "... = setsum ?s {..deg p}"
  24.726 +    by (simp add: setsum_Un_disjoint ivl_disj_int_one
  24.727 +      setsum_0 deg_aboveD)
  24.728 +  also have "... = p" by (rule up_repr)
  24.729 +  finally show ?thesis .
  24.730 +qed
  24.731 +
  24.732 +instance up :: ("domain") "domain"
  24.733 +proof
  24.734 +  show "1 ~= (0::'a up)"
  24.735 +  proof (* notI is applied here *)
  24.736 +    assume "1 = (0::'a up)"
  24.737 +    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
  24.738 +    hence "1 = (0::'a)" by simp
  24.739 +    with one_not_zero show "False" by contradiction
  24.740 +  qed
  24.741 +next
  24.742 +  fix p q :: "'a::domain up"
  24.743 +  assume pq: "p * q = 0"
  24.744 +  show "p = 0 | q = 0"
  24.745 +  proof (rule classical)
  24.746 +    assume c: "~ (p = 0 | q = 0)"
  24.747 +    then have "deg p + deg q = deg (p * q)" by simp
  24.748 +    also from pq have "... = 0" by simp
  24.749 +    finally have "deg p + deg q = 0" .
  24.750 +    then have f1: "deg p = 0 & deg q = 0" by simp
  24.751 +    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
  24.752 +      by (simp only: up_repr_le)
  24.753 +    also have "... = monom (coeff p 0) 0" by simp
  24.754 +    finally have p: "p = monom (coeff p 0) 0" .
  24.755 +    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
  24.756 +      by (simp only: up_repr_le)
  24.757 +    also have "... = monom (coeff q 0) 0" by simp
  24.758 +    finally have q: "q = monom (coeff q 0) 0" .
  24.759 +    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
  24.760 +    also from pq have "... = 0" by simp
  24.761 +    finally have "coeff p 0 * coeff q 0 = 0" .
  24.762 +    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
  24.763 +    with p q show "p = 0 | q = 0" by fastsimp
  24.764 +  qed
  24.765 +qed
  24.766 +
  24.767 +lemma monom_inj_zero:
  24.768 +  "(monom a n = 0) = (a = 0)"
  24.769 +proof -
  24.770 +  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
  24.771 +  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
  24.772 +  finally show ?thesis .
  24.773 +qed
  24.774 +
  24.775 +lemma smult_integral:
  24.776 +  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
  24.777 +by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
  24.778 +
  24.779 +end
  24.780 \ No newline at end of file
    25.1 --- a/src/HOL/Finite_Set.thy	Wed Nov 27 17:25:41 2002 +0100
    25.2 +++ b/src/HOL/Finite_Set.thy	Thu Nov 28 10:50:42 2002 +0100
    25.3 @@ -273,6 +273,22 @@
    25.4  lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
    25.5    by (induct k) (simp_all add: atMost_Suc)
    25.6  
    25.7 +lemma finite_greaterThanLessThan [iff]:
    25.8 +  fixes l :: nat shows "finite {)l..u(}"
    25.9 +by (simp add: greaterThanLessThan_def)
   25.10 +
   25.11 +lemma finite_atLeastLessThan [iff]:
   25.12 +  fixes l :: nat shows "finite {l..u(}"
   25.13 +by (simp add: atLeastLessThan_def)
   25.14 +
   25.15 +lemma finite_greaterThanAtMost [iff]:
   25.16 +  fixes l :: nat shows "finite {)l..u}"
   25.17 +by (simp add: greaterThanAtMost_def)
   25.18 +
   25.19 +lemma finite_atLeastAtMost [iff]:
   25.20 +  fixes l :: nat shows "finite {l..u}"
   25.21 +by (simp add: atLeastAtMost_def)
   25.22 +
   25.23  lemma bounded_nat_set_is_finite:
   25.24      "(ALL i:N. i < (n::nat)) ==> finite N"
   25.25    -- {* A bounded set of natural numbers is finite. *}
    26.1 --- a/src/HOL/IsaMakefile	Wed Nov 27 17:25:41 2002 +0100
    26.2 +++ b/src/HOL/IsaMakefile	Thu Nov 28 10:50:42 2002 +0100
    26.3 @@ -78,7 +78,8 @@
    26.4    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    26.5    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
    26.6    $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
    26.7 -  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
    26.8 +  $(SRC)/Provers/splitter.ML $(SRC)/Provers/linorder.ML \
    26.9 +  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
   26.10    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
   26.11    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
   26.12    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
   26.13 @@ -341,16 +342,13 @@
   26.14    Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
   26.15    Algebra/abstract/Field.thy \
   26.16    Algebra/abstract/Ideal.ML Algebra/abstract/Ideal.thy \
   26.17 -  Algebra/abstract/NatSum.ML Algebra/abstract/NatSum.thy \
   26.18    Algebra/abstract/PID.thy \
   26.19    Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \
   26.20    Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
   26.21 -  Algebra/poly/Degree.ML Algebra/poly/Degree.thy \
   26.22 +  Algebra/abstract/order.ML \
   26.23    Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
   26.24    Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
   26.25 -  Algebra/poly/PolyRing.ML Algebra/poly/PolyRing.thy \
   26.26    Algebra/poly/Polynomial.thy \
   26.27 -  Algebra/poly/ProtoPoly.ML Algebra/poly/ProtoPoly.thy \
   26.28    Algebra/poly/UnivPoly.ML Algebra/poly/UnivPoly.thy
   26.29  	@$(ISATOOL) usedir $(OUT)/HOL Algebra
   26.30  
    27.1 --- a/src/HOL/ROOT.ML	Wed Nov 27 17:25:41 2002 +0100
    27.2 +++ b/src/HOL/ROOT.ML	Thu Nov 28 10:50:42 2002 +0100
    27.3 @@ -35,6 +35,7 @@
    27.4  use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
    27.5  use "~~/src/Provers/Arith/extract_common_term.ML";
    27.6  use "~~/src/Provers/Arith/cancel_div_mod.ML";
    27.7 +use "~~/src/Provers/linorder.ML";
    27.8  
    27.9  with_path "Integ" use_thy "Main";
   27.10  
    28.1 --- a/src/HOL/SetInterval.ML	Wed Nov 27 17:25:41 2002 +0100
    28.2 +++ b/src/HOL/SetInterval.ML	Thu Nov 28 10:50:42 2002 +0100
    28.3 @@ -1,137 +1,51 @@
    28.4  (*  Title:      HOL/SetInterval.ML
    28.5      ID:         $Id$
    28.6 -    Author:     Tobias Nipkow
    28.7 -    Copyright   2000  TU Muenchen
    28.8 -
    28.9 -Set Intervals: lessThan, greaterThan, atLeast, atMost
   28.10 +    Author:     Clemens Ballarin
   28.11 +    Copyright   2002  TU Muenchen
   28.12  *)
   28.13  
   28.14 -
   28.15 -(*** lessThan ***)
   28.16 -
   28.17 -Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
   28.18 -by (Blast_tac 1);
   28.19 -qed "lessThan_iff";
   28.20 -AddIffs [lessThan_iff];
   28.21 -
   28.22 -Goalw [lessThan_def] "lessThan (0::nat) = {}";
   28.23 -by (Simp_tac 1);
   28.24 -qed "lessThan_0";
   28.25 -Addsimps [lessThan_0];
   28.26 -
   28.27 -Goalw [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
   28.28 -by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   28.29 -by (Blast_tac 1);
   28.30 -qed "lessThan_Suc";
   28.31 -
   28.32 -Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
   28.33 -by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
   28.34 -qed "lessThan_Suc_atMost";
   28.35 -
   28.36 -Goal "(UN m::nat. lessThan m) = UNIV";
   28.37 -by (Blast_tac 1);
   28.38 -qed "UN_lessThan_UNIV";
   28.39 -
   28.40 -Goalw [lessThan_def, atLeast_def]
   28.41 -    "!!k:: 'a::linorder. -lessThan k = atLeast k";
   28.42 -by Auto_tac;
   28.43 -by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
   28.44 -by (blast_tac (claset() addDs [order_le_less_trans]) 1);
   28.45 -qed "Compl_lessThan";
   28.46 -
   28.47 -Goal "!!k:: 'a::order. {k} - lessThan k = {k}";
   28.48 -by Auto_tac;
   28.49 -qed "single_Diff_lessThan";
   28.50 -Addsimps [single_Diff_lessThan];
   28.51 -
   28.52 -(*** greaterThan ***)
   28.53 -
   28.54 -Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
   28.55 -by (Blast_tac 1);
   28.56 -qed "greaterThan_iff";
   28.57 -AddIffs [greaterThan_iff];
   28.58 -
   28.59 -Goalw [greaterThan_def] "greaterThan 0 = range Suc";
   28.60 -by (blast_tac (claset() addDs [gr0_conv_Suc RS iffD1]) 1);
   28.61 -qed "greaterThan_0";
   28.62 -Addsimps [greaterThan_0];
   28.63 -
   28.64 -Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
   28.65 -by (auto_tac (claset() addEs [linorder_neqE], simpset()));
   28.66 -qed "greaterThan_Suc";
   28.67 -
   28.68 -Goal "(INT m::nat. greaterThan m) = {}";
   28.69 -by (Blast_tac 1);
   28.70 -qed "INT_greaterThan_UNIV";
   28.71 -
   28.72 -Goalw [greaterThan_def, atMost_def, le_def]
   28.73 -    "!!k:: 'a::linorder. -greaterThan k = atMost k";
   28.74 -by Auto_tac;
   28.75 -by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
   28.76 -by (blast_tac (claset() addDs [order_le_less_trans]) 1);
   28.77 -qed "Compl_greaterThan";
   28.78 +(* Legacy ML bindings *)
   28.79  
   28.80 -Goal "!!k:: 'a::linorder. -atMost k = greaterThan k";
   28.81 -by (simp_tac (simpset() addsimps [Compl_greaterThan RS sym]) 1);
   28.82 -qed "Compl_atMost";
   28.83 -
   28.84 -Addsimps [Compl_greaterThan, Compl_atMost];
   28.85 -
   28.86 -(*** atLeast ***)
   28.87 -
   28.88 -Goalw [atLeast_def] "(i: atLeast k) = (k<=i)";
   28.89 -by (Blast_tac 1);
   28.90 -qed "atLeast_iff";
   28.91 -AddIffs [atLeast_iff];
   28.92 -
   28.93 -Goalw [atLeast_def, UNIV_def] "atLeast (0::nat) = UNIV";
   28.94 -by (Simp_tac 1);
   28.95 -qed "atLeast_0";
   28.96 -Addsimps [atLeast_0];
   28.97 -
   28.98 -Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
   28.99 -by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
  28.100 -by (simp_tac (simpset() addsimps [order_le_less]) 1);
  28.101 -by (Blast_tac 1);
  28.102 -qed "atLeast_Suc";
  28.103 -
  28.104 -Goal "(UN m::nat. atLeast m) = UNIV";
  28.105 -by (Blast_tac 1);
  28.106 -qed "UN_atLeast_UNIV";
  28.107 -
  28.108 -Goalw [lessThan_def, atLeast_def, le_def]
  28.109 -    "!!k:: 'a::linorder. -atLeast k = lessThan k";
  28.110 -by Auto_tac;
  28.111 -by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
  28.112 -by (blast_tac (claset() addDs [order_le_less_trans]) 1);
  28.113 -qed "Compl_atLeast";
  28.114 -
  28.115 -Addsimps [Compl_lessThan, Compl_atLeast];
  28.116 -
  28.117 -(*** atMost ***)
  28.118 -
  28.119 -Goalw [atMost_def] "(i: atMost k) = (i<=k)";
  28.120 -by (Blast_tac 1);
  28.121 -qed "atMost_iff";
  28.122 -AddIffs [atMost_iff];
  28.123 -
  28.124 -Goalw [atMost_def] "atMost (0::nat) = {0}";
  28.125 -by (Simp_tac 1);
  28.126 -qed "atMost_0";
  28.127 -Addsimps [atMost_0];
  28.128 -
  28.129 -Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
  28.130 -by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
  28.131 -by (Blast_tac 1);
  28.132 -qed "atMost_Suc";
  28.133 -
  28.134 -Goal "(UN m::nat. atMost m) = UNIV";
  28.135 -by (Blast_tac 1);
  28.136 -qed "UN_atMost_UNIV";
  28.137 -
  28.138 -
  28.139 -(*** Combined properties ***)
  28.140 -
  28.141 -Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";
  28.142 -by (blast_tac (claset() addIs [order_antisym]) 1);
  28.143 -qed "atMost_Int_atLeast";
  28.144 +val Compl_atLeast = thm "Compl_atLeast";
  28.145 +val Compl_atMost = thm "Compl_atMost";
  28.146 +val Compl_greaterThan = thm "Compl_greaterThan";
  28.147 +val Compl_lessThan = thm "Compl_lessThan";
  28.148 +val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV";
  28.149 +val UN_atLeast_UNIV = thm "UN_atLeast_UNIV";
  28.150 +val UN_atMost_UNIV = thm "UN_atMost_UNIV";
  28.151 +val UN_lessThan_UNIV = thm "UN_lessThan_UNIV";
  28.152 +val atLeastAtMost_def = thm "atLeastAtMost_def";
  28.153 +val atLeastAtMost_iff = thm "atLeastAtMost_iff";
  28.154 +val atLeastLessThan_def  = thm "atLeastLessThan_def";
  28.155 +val atLeastLessThan_iff = thm "atLeastLessThan_iff";
  28.156 +val atLeast_0 = thm "atLeast_0";
  28.157 +val atLeast_Suc = thm "atLeast_Suc";
  28.158 +val atLeast_def      = thm "atLeast_def";
  28.159 +val atLeast_iff = thm "atLeast_iff";
  28.160 +val atMost_0 = thm "atMost_0";
  28.161 +val atMost_Int_atLeast = thm "atMost_Int_atLeast";
  28.162 +val atMost_Suc = thm "atMost_Suc";
  28.163 +val atMost_def       = thm "atMost_def";
  28.164 +val atMost_iff = thm "atMost_iff";
  28.165 +val greaterThanAtMost_def  = thm "greaterThanAtMost_def";
  28.166 +val greaterThanAtMost_iff = thm "greaterThanAtMost_iff";
  28.167 +val greaterThanLessThan_def  = thm "greaterThanLessThan_def";
  28.168 +val greaterThanLessThan_iff = thm "greaterThanLessThan_iff";
  28.169 +val greaterThan_0 = thm "greaterThan_0";
  28.170 +val greaterThan_Suc = thm "greaterThan_Suc";
  28.171 +val greaterThan_def  = thm "greaterThan_def";
  28.172 +val greaterThan_iff = thm "greaterThan_iff";
  28.173 +val ivl_disj_int = thms "ivl_disj_int";
  28.174 +val ivl_disj_int_one = thms "ivl_disj_int_one";
  28.175 +val ivl_disj_int_singleton = thms "ivl_disj_int_singleton";
  28.176 +val ivl_disj_int_two = thms "ivl_disj_int_two";
  28.177 +val ivl_disj_un = thms "ivl_disj_un";
  28.178 +val ivl_disj_un_one = thms "ivl_disj_un_one";
  28.179 +val ivl_disj_un_singleton = thms "ivl_disj_un_singleton";
  28.180 +val ivl_disj_un_two = thms "ivl_disj_un_two";
  28.181 +val lessThan_0 = thm "lessThan_0";
  28.182 +val lessThan_Suc = thm "lessThan_Suc";
  28.183 +val lessThan_Suc_atMost = thm "lessThan_Suc_atMost";
  28.184 +val lessThan_def     = thm "lessThan_def";
  28.185 +val lessThan_iff = thm "lessThan_iff";
  28.186 +val single_Diff_lessThan = thm "single_Diff_lessThan";
    29.1 --- a/src/HOL/SetInterval.thy	Wed Nov 27 17:25:41 2002 +0100
    29.2 +++ b/src/HOL/SetInterval.thy	Thu Nov 28 10:50:42 2002 +0100
    29.3 @@ -1,12 +1,12 @@
    29.4  (*  Title:      HOL/SetInterval.thy
    29.5      ID:         $Id$
    29.6 -    Author:     Tobias Nipkow
    29.7 +    Author:     Tobias Nipkow and Clemens Ballarin
    29.8      Copyright   2000  TU Muenchen
    29.9  
   29.10 -lessThan, greaterThan, atLeast, atMost
   29.11 +lessThan, greaterThan, atLeast, atMost and two-sided intervals
   29.12  *)
   29.13  
   29.14 -SetInterval = NatArith + 
   29.15 +theory SetInterval = NatArith:
   29.16  
   29.17  constdefs
   29.18    lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
   29.19 @@ -21,4 +21,320 @@
   29.20    atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
   29.21    "{l..} == {x. l<=x}"
   29.22  
   29.23 +  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
   29.24 +  "{)l..u(} == {)l..} Int {..u(}"
   29.25 +
   29.26 +  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
   29.27 +  "{l..u(} == {l..} Int {..u(}"
   29.28 +
   29.29 +  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
   29.30 +  "{)l..u} == {)l..} Int {..u}"
   29.31 +
   29.32 +  atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
   29.33 +  "{l..u} == {l..} Int {..u}"
   29.34 +
   29.35 +(* Setup of transitivity reasoner *)
   29.36 +
   29.37 +ML {*
   29.38 +
   29.39 +structure Trans_Tac = Trans_Tac_Fun (
   29.40 +  struct
   29.41 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   29.42 +    val le_refl = thm "order_refl";
   29.43 +    val less_imp_le = thm "order_less_imp_le";
   29.44 +    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
   29.45 +    val not_leI = thm "linorder_not_less" RS thm "iffD2";
   29.46 +    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
   29.47 +    val not_leD = thm "linorder_not_le" RS thm "iffD1";
   29.48 +    val eqI = thm "order_antisym";
   29.49 +    val eqD1 = thm "order_eq_refl";
   29.50 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
   29.51 +    val less_trans = thm "order_less_trans";
   29.52 +    val less_le_trans = thm "order_less_le_trans";
   29.53 +    val le_less_trans = thm "order_le_less_trans";
   29.54 +    val le_trans = thm "order_trans";
   29.55 +    fun decomp (Trueprop $ t) =
   29.56 +      let fun dec (Const ("Not", _) $ t) = (
   29.57 +              case dec t of
   29.58 +		None => None
   29.59 +	      | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
   29.60 +	    | dec (Const (rel, _) $ t1 $ t2) = 
   29.61 +                Some (t1, implode (drop (3, explode rel)), t2)
   29.62 +	    | dec _ = None
   29.63 +      in dec t end
   29.64 +      | decomp _ = None
   29.65 +  end);
   29.66 +
   29.67 +val trans_tac = Trans_Tac.trans_tac;
   29.68 +
   29.69 +*}
   29.70 +
   29.71 +method_setup trans =
   29.72 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *}
   29.73 +  {* simple transitivity reasoner *}
   29.74 +
   29.75 +(*** lessThan ***)
   29.76 +
   29.77 +lemma lessThan_iff: "(i: lessThan k) = (i<k)"
   29.78 +
   29.79 +apply (unfold lessThan_def)
   29.80 +apply blast
   29.81 +done
   29.82 +declare lessThan_iff [iff]
   29.83 +
   29.84 +lemma lessThan_0: "lessThan (0::nat) = {}"
   29.85 +apply (unfold lessThan_def)
   29.86 +apply (simp (no_asm))
   29.87 +done
   29.88 +declare lessThan_0 [simp]
   29.89 +
   29.90 +lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
   29.91 +apply (unfold lessThan_def)
   29.92 +apply (simp (no_asm) add: less_Suc_eq)
   29.93 +apply blast
   29.94 +done
   29.95 +
   29.96 +lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
   29.97 +apply (unfold lessThan_def atMost_def)
   29.98 +apply (simp (no_asm) add: less_Suc_eq_le)
   29.99 +done
  29.100 +
  29.101 +lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
  29.102 +apply blast
  29.103 +done
  29.104 +
  29.105 +lemma Compl_lessThan: 
  29.106 +    "!!k:: 'a::linorder. -lessThan k = atLeast k"
  29.107 +apply (unfold lessThan_def atLeast_def)
  29.108 +apply auto
  29.109 +apply (blast intro: linorder_not_less [THEN iffD1])
  29.110 +apply (blast dest: order_le_less_trans)
  29.111 +done
  29.112 +
  29.113 +lemma single_Diff_lessThan: "!!k:: 'a::order. {k} - lessThan k = {k}"
  29.114 +apply auto
  29.115 +done
  29.116 +declare single_Diff_lessThan [simp]
  29.117 +
  29.118 +(*** greaterThan ***)
  29.119 +
  29.120 +lemma greaterThan_iff: "(i: greaterThan k) = (k<i)"
  29.121 +
  29.122 +apply (unfold greaterThan_def)
  29.123 +apply blast
  29.124 +done
  29.125 +declare greaterThan_iff [iff]
  29.126 +
  29.127 +lemma greaterThan_0: "greaterThan 0 = range Suc"
  29.128 +apply (unfold greaterThan_def)
  29.129 +apply (blast dest: gr0_conv_Suc [THEN iffD1])
  29.130 +done
  29.131 +declare greaterThan_0 [simp]
  29.132 +
  29.133 +lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
  29.134 +apply (unfold greaterThan_def)
  29.135 +apply (auto elim: linorder_neqE)
  29.136 +done
  29.137 +
  29.138 +lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
  29.139 +apply blast
  29.140 +done
  29.141 +
  29.142 +lemma Compl_greaterThan: 
  29.143 +    "!!k:: 'a::linorder. -greaterThan k = atMost k"
  29.144 +apply (unfold greaterThan_def atMost_def le_def)
  29.145 +apply auto
  29.146 +apply (blast intro: linorder_not_less [THEN iffD1])
  29.147 +apply (blast dest: order_le_less_trans)
  29.148 +done
  29.149 +
  29.150 +lemma Compl_atMost: "!!k:: 'a::linorder. -atMost k = greaterThan k"
  29.151 +apply (simp (no_asm) add: Compl_greaterThan [symmetric])
  29.152 +done
  29.153 +
  29.154 +declare Compl_greaterThan [simp] Compl_atMost [simp]
  29.155 +
  29.156 +(*** atLeast ***)
  29.157 +
  29.158 +lemma atLeast_iff: "(i: atLeast k) = (k<=i)"
  29.159 +
  29.160 +apply (unfold atLeast_def)
  29.161 +apply blast
  29.162 +done
  29.163 +declare atLeast_iff [iff]
  29.164 +
  29.165 +lemma atLeast_0: "atLeast (0::nat) = UNIV"
  29.166 +apply (unfold atLeast_def UNIV_def)
  29.167 +apply (simp (no_asm))
  29.168 +done
  29.169 +declare atLeast_0 [simp]
  29.170 +
  29.171 +lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
  29.172 +apply (unfold atLeast_def)
  29.173 +apply (simp (no_asm) add: Suc_le_eq)
  29.174 +apply (simp (no_asm) add: order_le_less)
  29.175 +apply blast
  29.176 +done
  29.177 +
  29.178 +lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
  29.179 +apply blast
  29.180 +done
  29.181 +
  29.182 +lemma Compl_atLeast: 
  29.183 +    "!!k:: 'a::linorder. -atLeast k = lessThan k"
  29.184 +apply (unfold lessThan_def atLeast_def le_def)
  29.185 +apply auto
  29.186 +apply (blast intro: linorder_not_less [THEN iffD1])
  29.187 +apply (blast dest: order_le_less_trans)
  29.188 +done
  29.189 +
  29.190 +declare Compl_lessThan [simp] Compl_atLeast [simp]
  29.191 +
  29.192 +(*** atMost ***)
  29.193 +
  29.194 +lemma atMost_iff: "(i: atMost k) = (i<=k)"
  29.195 +
  29.196 +apply (unfold atMost_def)
  29.197 +apply blast
  29.198 +done
  29.199 +declare atMost_iff [iff]
  29.200 +
  29.201 +lemma atMost_0: "atMost (0::nat) = {0}"
  29.202 +apply (unfold atMost_def)
  29.203 +apply (simp (no_asm))
  29.204 +done
  29.205 +declare atMost_0 [simp]
  29.206 +
  29.207 +lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
  29.208 +apply (unfold atMost_def)
  29.209 +apply (simp (no_asm) add: less_Suc_eq order_le_less)
  29.210 +apply blast
  29.211 +done
  29.212 +
  29.213 +lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
  29.214 +apply blast
  29.215 +done
  29.216 +
  29.217 +
  29.218 +(*** Combined properties ***)
  29.219 +
  29.220 +lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
  29.221 +apply (blast intro: order_antisym)
  29.222 +done
  29.223 +
  29.224 +(*** Two-sided intervals ***)
  29.225 +
  29.226 +(* greaterThanLessThan *)
  29.227 +
  29.228 +lemma greaterThanLessThan_iff [simp]:
  29.229 +  "(i : {)l..u(}) = (l < i & i < u)"
  29.230 +by (simp add: greaterThanLessThan_def)
  29.231 +
  29.232 +(* atLeastLessThan *)
  29.233 +
  29.234 +lemma atLeastLessThan_iff [simp]:
  29.235 +  "(i : {l..u(}) = (l <= i & i < u)"
  29.236 +by (simp add: atLeastLessThan_def)
  29.237 +
  29.238 +(* greaterThanAtMost *)
  29.239 +
  29.240 +lemma greaterThanAtMost_iff [simp]:
  29.241 +  "(i : {)l..u}) = (l < i & i <= u)"
  29.242 +by (simp add: greaterThanAtMost_def)
  29.243 +
  29.244 +(* atLeastAtMost *)
  29.245 +
  29.246 +lemma atLeastAtMost_iff [simp]:
  29.247 +  "(i : {l..u}) = (l <= i & i <= u)"
  29.248 +by (simp add: atLeastAtMost_def)
  29.249 +
  29.250 +(* The above four lemmas could be declared as iffs.
  29.251 +   If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
  29.252 +   seems to take forever (more than one hour). *)
  29.253 +
  29.254 +(*** The following lemmas are useful with the summation operator setsum ***)
  29.255 +(* For examples, see Algebra/poly/UnivPoly.thy *)
  29.256 +
  29.257 +(** Disjoint Unions **)
  29.258 +
  29.259 +(* Singletons and open intervals *)
  29.260 +
  29.261 +lemma ivl_disj_un_singleton:
  29.262 +  "{l::'a::linorder} Un {)l..} = {l..}"
  29.263 +  "{..u(} Un {u::'a::linorder} = {..u}"
  29.264 +  "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
  29.265 +  "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
  29.266 +  "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
  29.267 +  "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
  29.268 +by auto (elim linorder_neqE | trans+)+
  29.269 +
  29.270 +(* One- and two-sided intervals *)
  29.271 +
  29.272 +lemma ivl_disj_un_one:
  29.273 +  "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
  29.274 +  "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
  29.275 +  "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
  29.276 +  "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
  29.277 +  "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
  29.278 +  "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
  29.279 +  "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
  29.280 +  "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
  29.281 +by auto trans+
  29.282 +
  29.283 +(* Two- and two-sided intervals *)
  29.284 +
  29.285 +lemma ivl_disj_un_two:
  29.286 +  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
  29.287 +  "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
  29.288 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
  29.289 +  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
  29.290 +  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
  29.291 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
  29.292 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
  29.293 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
  29.294 +by auto trans+
  29.295 +
  29.296 +lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
  29.297 +
  29.298 +(** Disjoint Intersections **)
  29.299 +
  29.300 +(* Singletons and open intervals *)
  29.301 +
  29.302 +lemma ivl_disj_int_singleton:
  29.303 +  "{l::'a::order} Int {)l..} = {}"
  29.304 +  "{..u(} Int {u} = {}"
  29.305 +  "{l} Int {)l..u(} = {}"
  29.306 +  "{)l..u(} Int {u} = {}"
  29.307 +  "{l} Int {)l..u} = {}"
  29.308 +  "{l..u(} Int {u} = {}"
  29.309 +  by simp+
  29.310 +
  29.311 +(* One- and two-sided intervals *)
  29.312 +
  29.313 +lemma ivl_disj_int_one:
  29.314 +  "{..l::'a::order} Int {)l..u(} = {}"
  29.315 +  "{..l(} Int {l..u(} = {}"
  29.316 +  "{..l} Int {)l..u} = {}"
  29.317 +  "{..l(} Int {l..u} = {}"
  29.318 +  "{)l..u} Int {)u..} = {}"
  29.319 +  "{)l..u(} Int {u..} = {}"
  29.320 +  "{l..u} Int {)u..} = {}"
  29.321 +  "{l..u(} Int {u..} = {}"
  29.322 +  by auto trans+
  29.323 +
  29.324 +(* Two- and two-sided intervals *)
  29.325 +
  29.326 +lemma ivl_disj_int_two:
  29.327 +  "{)l::'a::order..m(} Int {m..u(} = {}"
  29.328 +  "{)l..m} Int {)m..u(} = {}"
  29.329 +  "{l..m(} Int {m..u(} = {}"
  29.330 +  "{l..m} Int {)m..u(} = {}"
  29.331 +  "{)l..m(} Int {m..u} = {}"
  29.332 +  "{)l..m} Int {)m..u} = {}"
  29.333 +  "{l..m(} Int {m..u} = {}"
  29.334 +  "{l..m} Int {)m..u} = {}"
  29.335 +  by auto trans+
  29.336 +
  29.337 +lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
  29.338 +
  29.339  end
    30.1 --- a/src/Provers/README	Wed Nov 27 17:25:41 2002 +0100
    30.2 +++ b/src/Provers/README	Thu Nov 28 10:50:42 2002 +0100
    30.3 @@ -16,6 +16,7 @@
    30.4    simplifier.ML         fast simplifier
    30.5    split_paired_all.ML	turn surjective pairing into split rule
    30.6    splitter.ML           performs case splits for simplifier.ML
    30.7 +  trans.ML              transitivity reasoner for linear (total) orders
    30.8    typedsimp.ML          basic simplifier for explicitly typed logics
    30.9  
   30.10  directory Arith:
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/Provers/linorder.ML	Thu Nov 28 10:50:42 2002 +0100
    31.3 @@ -0,0 +1,214 @@
    31.4 +(*
    31.5 +  Title:	Transitivity reasoner for linear orders
    31.6 +  Id:		$Id$
    31.7 +  Author:	Clemens Ballarin, started 8 November 2002
    31.8 +  Copyright:	TU Muenchen
    31.9 +*)
   31.10 +
   31.11 +(***
   31.12 +This is a very simple package for transitivity reasoning over linear orders.
   31.13 +Simple means exponential time (and space) in the number of premises.
   31.14 +Should be replaced by a graph-theoretic algorithm.
   31.15 +
   31.16 +The package provides a tactic trans_tac that uses all premises of the form
   31.17 +
   31.18 +  t = u, t < u, t <= u, ~(t < u) and ~(t <= u)
   31.19 +
   31.20 +to
   31.21 +1. either derive a contradiction,
   31.22 +   in which case the conclusion can be any term,
   31.23 +2. or prove the conclusion, which must be of the same form as the premises.
   31.24 +
   31.25 +To get rid of ~= in the premises, it is advisable to use an elimination
   31.26 +rule of the form
   31.27 +
   31.28 +  [| t ~= u; t < u ==> P; u < t ==> P |] ==> P.
   31.29 +
   31.30 +The package is implemented as an ML functor and thus not limited to the
   31.31 +relation <= and friends.  It can be instantiated to any total order ---
   31.32 +for example, the divisibility relation "dvd".
   31.33 +***)
   31.34 +
   31.35 +(*** Credits ***
   31.36 +
   31.37 +This package is closely based on a (no longer used) transitivity reasoner for
   31.38 +the natural numbers, which was written by Tobias Nipkow.
   31.39 +
   31.40 +****************)
   31.41 +
   31.42 +signature LESS_ARITH =
   31.43 +sig
   31.44 +  val less_reflE: thm  (* x < x ==> P *)
   31.45 +  val le_refl: thm  (* x <= x *)
   31.46 +  val less_imp_le: thm (* x <= y ==> x < y *)
   31.47 +  val not_lessI: thm (* y <= x  ==> ~(x < y) *)
   31.48 +  val not_leI: thm (* y < x  ==> ~(x <= y) *)
   31.49 +  val not_lessD: thm (* ~(x < y) ==> y <= x *)
   31.50 +  val not_leD: thm (* ~(x <= y) ==> y < x *)
   31.51 +  val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
   31.52 +  val eqD1: thm (* x = y ==> x <= y *)
   31.53 +  val eqD2: thm (* x = y ==> y <= x *)
   31.54 +  val less_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
   31.55 +  val less_le_trans: thm  (* [| x <= y; y < z |] ==> x < z *)
   31.56 +  val le_less_trans: thm  (* [| x < y; y <= z |] ==> x < z *)
   31.57 +  val le_trans: thm  (* [| x < y; y < z |] ==> x < z *)
   31.58 +  val decomp: term -> (term * string * term) option
   31.59 +    (* decomp (`x Rel y') should yield (x, Rel, y)
   31.60 +       where Rel is one of "<", "<=", "~<", "~<=", "=" and "~="
   31.61 +       other relation symbols are ignored *)
   31.62 +end;
   31.63 +
   31.64 +signature TRANS_TAC =
   31.65 +sig
   31.66 +  val trans_tac: int -> tactic
   31.67 +end;
   31.68 +
   31.69 +functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
   31.70 +struct
   31.71 +
   31.72 +(*** Proof objects ***)
   31.73 +
   31.74 +datatype proof
   31.75 +  = Asm of int
   31.76 +  | Thm of proof list * thm;
   31.77 +
   31.78 +(* Turn proof objects into theorems *)
   31.79 +
   31.80 +fun prove asms =
   31.81 +  let fun pr (Asm i) = nth_elem (i, asms)
   31.82 +        | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
   31.83 +  in pr end;
   31.84 +
   31.85 +(*** Exceptions ***)
   31.86 +
   31.87 +exception Contr of proof;  (* Raised when contradiction is found *)
   31.88 +
   31.89 +exception Cannot;  (* Raised when goal cannot be proved *)
   31.90 +
   31.91 +(*** Internal representation of inequalities ***)
   31.92 +
   31.93 +datatype less
   31.94 +  = Less of term * term * proof
   31.95 +  | Le of term * term * proof;
   31.96 +
   31.97 +fun lower (Less (x, _, _)) = x
   31.98 +  | lower (Le (x, _, _)) = x;
   31.99 +
  31.100 +fun upper (Less (_, y, _)) = y
  31.101 +  | upper (Le (_, y, _)) = y;
  31.102 +
  31.103 +infix subsumes;
  31.104 +
  31.105 +fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
  31.106 +  | (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y')
  31.107 +  | (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
  31.108 +  | _ subsumes _ = false;
  31.109 +
  31.110 +fun trivial (Le (x, x', _)) = (x = x')
  31.111 +  | trivial _ = false;
  31.112 +
  31.113 +(*** Transitive closure ***)
  31.114 +
  31.115 +fun add new =
  31.116 +  let fun adds([], news) = new::news
  31.117 +        | adds(old::olds, news) = if new subsumes old then adds(olds, news)
  31.118 +                                  else adds(olds, old::news)
  31.119 +  in adds end;
  31.120 +
  31.121 +fun ctest (less as Less (x, x', p)) = 
  31.122 +    if x = x' then raise Contr (Thm ([p], Less.less_reflE))
  31.123 +    else less
  31.124 +  | ctest less = less;
  31.125 +
  31.126 +fun mktrans (Less (x, _, p), Less (_, z, q)) =
  31.127 +    Less (x, z, Thm([p, q], Less.less_trans))
  31.128 +  | mktrans (Less (x, _, p), Le (_, z, q)) =
  31.129 +    Less (x, z, Thm([p, q], Less.less_le_trans))
  31.130 +  | mktrans (Le (x, _, p), Less (_, z, q)) =
  31.131 +    Less (x, z, Thm([p, q], Less.le_less_trans))
  31.132 +  | mktrans (Le (x, _, p), Le (_, z, q)) =
  31.133 +    Le (x, z, Thm([p, q], Less.le_trans));
  31.134 +
  31.135 +fun trans new olds =
  31.136 +  let fun tr (news, old) =
  31.137 +            if upper old = lower new then mktrans (old, new)::news
  31.138 +            else if upper new = lower old then mktrans (new, old)::news
  31.139 +            else news
  31.140 +  in foldl tr ([], olds) end;
  31.141 +
  31.142 +fun close1 olds new =
  31.143 +    if trivial new orelse exists (fn old => old subsumes new) olds then olds
  31.144 +    else let val news = trans new olds
  31.145 +         in close (add new (olds, [])) news end
  31.146 +and close olds [] = olds
  31.147 +  | close olds (new::news) = close (close1 olds (ctest new)) news;
  31.148 +
  31.149 +(*** Solving and proving goals ***)
  31.150 +
  31.151 +(* Recognise and solve trivial goal *)
  31.152 +
  31.153 +fun triv_sol (Le (x, x',  _)) = 
  31.154 +    if x = x' then Some (Thm ([], Less.le_refl)) 
  31.155 +    else None
  31.156 +  | triv_sol _ = None;
  31.157 +
  31.158 +(* Solve less starting from facts *)
  31.159 +
  31.160 +fun solve facts less =
  31.161 +  case triv_sol less of
  31.162 +    None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of
  31.163 +	(None, _) => raise Cannot
  31.164 +      | (Some (Less (_, _, p)), Less _) => p
  31.165 +      | (Some (Le (_, _, p)), Less _) =>
  31.166 +	   error "trans_tac/solve: internal error: le cannot subsume less"
  31.167 +      | (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le)
  31.168 +      | (Some (Le (_, _, p)), Le _) => p)
  31.169 +  | Some prf => prf;
  31.170 +
  31.171 +(* Turn term t into Less or Le; n is position of t in list of assumptions *)
  31.172 +
  31.173 +fun mkasm (t, n) =
  31.174 +  case Less.decomp t of
  31.175 +    Some (x, rel, y) => (case rel of
  31.176 +      "<"   => [Less (x, y, Asm n)]
  31.177 +    | "~<"  => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
  31.178 +    | "<="  => [Le (x, y, Asm n)]
  31.179 +    | "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))]
  31.180 +    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
  31.181 +                Le (x, y, Thm ([Asm n], Less.eqD1))]
  31.182 +    | "~="  => []
  31.183 +    | _     => error ("trans_tac/mkasm: unknown relation " ^ rel))
  31.184 +  | None => [];
  31.185 +
  31.186 +(* Turn goal t into a pair (goals, proof) where goals is a list of
  31.187 +   Le/Less-subgoals to solve, and proof the validation that proves the concl t
  31.188 +   Asm ~1 is dummy (denotes a goal)
  31.189 +*)
  31.190 +
  31.191 +fun mkconcl t =
  31.192 +  case Less.decomp t of
  31.193 +    Some (x, rel, y) => (case rel of
  31.194 +      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
  31.195 +    | "~<"  => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
  31.196 +    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
  31.197 +    | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
  31.198 +    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
  31.199 +                 Thm ([Asm 0, Asm 1], Less.eqI))
  31.200 +    | _  => raise Cannot)
  31.201 +  | None => raise Cannot;
  31.202 +
  31.203 +val trans_tac = SUBGOAL (fn (A, n) =>
  31.204 +  let val Hs = Logic.strip_assums_hyp A
  31.205 +    val C = Logic.strip_assums_concl A
  31.206 +    val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
  31.207 +    val clesss = close [] lesss
  31.208 +    val (subgoals, prf) = mkconcl C
  31.209 +    val prfs = map (solve clesss) subgoals
  31.210 +  in METAHYPS (fn asms =>
  31.211 +    let val thms = map (prove asms) prfs
  31.212 +    in rtac (prove thms prf) 1 end) n
  31.213 +  end
  31.214 +  handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
  31.215 +       | Cannot => no_tac);
  31.216 +
  31.217 +end;