src/HOL/Hyperreal/Poly.ML

For the Isar version of the ZF logics manual

(*  Title:       Poly.ML
    Author:      Jacques D. Fleuriot
    Copyright:   2000 University of Edinburgh
    Description: Properties of real polynomials following 
                 John Harrison's HOL-Light implementation.
                 Some early theorems by Lucas Dixon
*)

Goal "p +++ [] = p";
by (induct_tac "p" 1);
by Auto_tac;
qed "padd_Nil2";
Addsimps [padd_Nil2];

Goal "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)";
by Auto_tac;
qed "padd_Cons_Cons";

Goal "-- [] = []";
by (rewtac poly_minus_def);
by (Auto_tac);
qed "pminus_Nil";
Addsimps [pminus_Nil];

Goal "[h1] *** p1 = h1 %* p1";
by (Simp_tac 1);
qed "pmult_singleton";

Goal "1 %* t = t";
by (induct_tac "t" 1);
by Auto_tac;
qed "poly_ident_mult";
Addsimps [poly_ident_mult];

Goal "[a] +++ ((0)#t) = (a#t)"; 
by (Simp_tac 1);
qed "poly_simple_add_Cons";
Addsimps [poly_simple_add_Cons];

(*-------------------------------------------------------------------------*)
(*  Handy general properties                                               *)
(*-------------------------------------------------------------------------*)

Goal "b +++ a = a +++ b"; 
by (subgoal_tac "ALL a. b +++ a = a +++ b" 1);
by (induct_tac "b" 2);
by Auto_tac;
by (rtac (padd_Cons RS ssubst) 1);
by (case_tac "aa" 1);
by Auto_tac;
qed "padd_commut";

Goal "(a +++ b) +++ c = a +++ (b +++ c)"; 
by (subgoal_tac "ALL b c. (a +++ b) +++ c = a +++ (b +++ c)" 1);
by (Asm_simp_tac 1);
by (induct_tac "a" 1);
by (Step_tac 2);
by (case_tac "b" 2);
by (Asm_simp_tac 2);
by (Asm_simp_tac 2);
by (Asm_simp_tac 1);
qed "padd_assoc";

Goal "a %* ( p +++ q ) = (a %* p +++ a %* q)";
by (subgoal_tac "ALL q. a %* ( p +++ q ) = (a %* p +++ a %* q) " 1);
by (induct_tac "p" 2);
by (Simp_tac 2);
by (rtac allI 2 );
by (case_tac "q" 2);
by (Asm_simp_tac 2);
by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib2] ) 2);
by (Asm_simp_tac 1);
qed "poly_cmult_distr";

Goal "[0, 1] *** t = ((0)#t)";
by (induct_tac "t" 1);
by (Simp_tac 1);
by (simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1);
by (case_tac "list" 1);
by (Asm_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1);
qed "pmult_by_x";
Addsimps [pmult_by_x];


(*-------------------------------------------------------------------------*)
(*  properties of evaluation of polynomials.                               *)
(*-------------------------------------------------------------------------*)

Goal "poly (p1 +++ p2) x = poly p1 x + poly p2 x";
by (subgoal_tac "ALL p2. poly (p1 +++ p2) x = poly( p1 ) x + poly( p2 ) x" 1);
by (induct_tac "p1" 2);
by Auto_tac;
by (case_tac "p2" 1);
by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2]));
qed "poly_add";

Goal "poly (c %* p) x = c * poly p x";
by (induct_tac "p" 1); 
by (case_tac "x=0" 2);
by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2] 
    @ real_mult_ac));
qed "poly_cmult";

Goalw [poly_minus_def] "poly (-- p) x = - (poly p x)";
by (auto_tac (claset(),simpset() addsimps [poly_cmult]));
qed "poly_minus";

Goal "poly (p1 *** p2) x = poly p1 x * poly p2 x";
by (subgoal_tac "ALL p2. poly (p1 *** p2) x = poly p1 x * poly p2 x" 1);
by (Asm_simp_tac 1);
by (induct_tac "p1" 1);
by (auto_tac (claset(),simpset() addsimps [poly_cmult]));
by (case_tac "list" 1);
by (auto_tac (claset(),simpset() addsimps [poly_cmult,poly_add,
    real_add_mult_distrib,real_add_mult_distrib2] @ real_mult_ac));
qed "poly_mult";

Goal "poly (p %^ n) x = (poly p x) ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [poly_cmult, poly_mult]));
qed "poly_exp";

(*-------------------------------------------------------------------------*)
(*  More Polynomial Evaluation Lemmas                                      *)
(*-------------------------------------------------------------------------*)

Goal "poly (a +++ []) x = poly a x";
by (Simp_tac 1);
qed "poly_add_rzero";
Addsimps [poly_add_rzero];

Goal "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x";
by (simp_tac (simpset() addsimps [poly_mult,real_mult_assoc])  1);
qed "poly_mult_assoc";

Goal "poly (p *** []) x = 0";
by (induct_tac "p" 1);
by Auto_tac;
qed "poly_mult_Nil2";
Addsimps [poly_mult_Nil2];

Goal "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d ) x";
by (induct_tac "n" 1);
by (auto_tac (claset(), simpset() addsimps [poly_mult,real_mult_assoc]));
qed "poly_exp_add";

(*-------------------------------------------------------------------------*)
(*  The derivative                                                         *)
(*-------------------------------------------------------------------------*)

Goalw [pderiv_def] "pderiv [] = []";
by (Simp_tac 1);
qed "pderiv_Nil";
Addsimps [pderiv_Nil];

Goalw [pderiv_def] "pderiv [c] = []";
by (Simp_tac 1);
qed "pderiv_singleton";
Addsimps [pderiv_singleton];

Goalw [pderiv_def] "pderiv (h#t) = pderiv_aux 1 t";
by (Simp_tac 1);
qed "pderiv_Cons";

Goal "DERIV f x :> D ==> DERIV (%x. (f x) * c) x :> D * c";
by (auto_tac (claset() addIs [DERIV_cmult,real_mult_commute RS subst],
    simpset() addsimps [real_mult_commute]));
qed "DERIV_cmult2";

Goal "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)";
by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_pow 1);
by (Simp_tac 1);
qed "DERIV_pow2";
Addsimps [DERIV_pow2,DERIV_pow];

Goal "ALL n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \
    \   x ^ n * poly (pderiv_aux (Suc n) p) x ";
by (induct_tac "p" 1);
by (auto_tac (claset() addSIs [DERIV_add,DERIV_cmult2],simpset() addsimps 
    [pderiv_def,real_add_mult_distrib2,real_mult_assoc RS sym] delsimps 
    [realpow_Suc]));
by (rtac (real_mult_commute RS subst) 1);
by (simp_tac (simpset() delsimps [realpow_Suc]) 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_commute,realpow_Suc RS sym] 
    delsimps [realpow_Suc]) 1);
qed "lemma_DERIV_poly1";

Goal "DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \
    \   x ^ n * poly (pderiv_aux (Suc n) p) x ";
by (simp_tac (simpset() addsimps [lemma_DERIV_poly1] delsimps [realpow_Suc]) 1);
qed "lemma_DERIV_poly";

Goal "DERIV f x :> D ==>  DERIV (%x. a + f x) x :> D";
by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_add 1);
by Auto_tac;
qed "DERIV_add_const";

Goal "DERIV (%x. poly p x) x :> poly (pderiv p) x";
by (induct_tac "p" 1);
by (auto_tac (claset(),simpset() addsimps [pderiv_Cons]));
by (rtac DERIV_add_const 1);
by (rtac lemma_DERIV_subst 1);
by (rtac (full_simplify (simpset()) 
    (read_instantiate [("n","0")] lemma_DERIV_poly)) 1);
by (simp_tac (simpset() addsimps [CLAIM "1 = 1"]) 1);
qed "poly_DERIV";
Addsimps [poly_DERIV];


(*-------------------------------------------------------------------------*)
(* Consequences of the derivative theorem above                            *)
(*-------------------------------------------------------------------------*)

Goalw [differentiable_def] "(%x. poly p x) differentiable x";
by (blast_tac (claset() addIs [poly_DERIV]) 1);
qed "poly_differentiable";
Addsimps [poly_differentiable];

Goal "isCont (%x. poly p x) x";
by (rtac (poly_DERIV RS DERIV_isCont) 1);
qed "poly_isCont";
Addsimps [poly_isCont];

Goal "[| a < b; poly p a < 0; 0 < poly p b |] \
\     ==> EX x. a < x & x < b & (poly p x = 0)";
by (cut_inst_tac [("f","%x. poly p x"),("a","a"),("b","b"),("y","0")] 
    IVT_objl 1);
by (auto_tac (claset(),simpset() addsimps [real_le_less]));
qed "poly_IVT_pos";

Goal "[| a < b; 0 < poly p a; poly p b < 0 |] \
\     ==> EX x. a < x & x < b & (poly p x = 0)";
by (blast_tac (claset() addIs [full_simplify (simpset() 
    addsimps [poly_minus, rename_numerals real_minus_zero_less_iff2])
   (read_instantiate [("p","-- p")] poly_IVT_pos)]) 1);
qed "poly_IVT_neg";

Goal "a < b ==> \
\    EX x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)";
by (dres_inst_tac [("f","poly p")] MVT 1);
by Auto_tac;
by (res_inst_tac [("x","z")] exI 1);
by (auto_tac (claset() addDs [ARITH_PROVE 
    "[| a < z; z < b |] ==> (b - (a::real)) ~= 0"],simpset()
     addsimps [real_mult_left_cancel,poly_DERIV RS DERIV_unique]));
qed "poly_MVT";


(*-------------------------------------------------------------------------*)
(*  Lemmas for Derivatives                                                 *)
(*-------------------------------------------------------------------------*)

Goal "ALL p2 n. poly (pderiv_aux n (p1 +++ p2)) x = \
    \           poly (pderiv_aux n p1 +++ pderiv_aux n p2) x";
by (induct_tac "p1" 1);
by (Step_tac 2);
by (case_tac "p2" 2);
by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2]));
qed "lemma_poly_pderiv_aux_add";

Goal "poly (pderiv_aux n (p1 +++ p2)) x = \
    \ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x";
by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_add]) 1);
qed "poly_pderiv_aux_add";

Goal "ALL n. poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x";
by (induct_tac "p" 1);
by (auto_tac (claset(),simpset() addsimps [poly_cmult] @ real_mult_ac));
qed "lemma_poly_pderiv_aux_cmult";

Goal "poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x";
by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_cmult]) 1);
qed "poly_pderiv_aux_cmult";

Goalw [poly_minus_def]
   "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x";
by (simp_tac (simpset() addsimps [poly_pderiv_aux_cmult]) 1);
qed "poly_pderiv_aux_minus";

Goal "ALL n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x";
by (induct_tac "p" 1);
by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
    real_add_mult_distrib]));
qed "lemma_poly_pderiv_aux_mult1";

Goal "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x";
by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_mult1]) 1);
qed "lemma_poly_pderiv_aux_mult";

Goal "ALL q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x";
by (induct_tac "p" 1);
by (Step_tac 2);
by (case_tac "q" 2);
by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_add,poly_add,
    pderiv_def]));
qed "lemma_poly_pderiv_add";

Goal "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x";
by (simp_tac (simpset() addsimps [lemma_poly_pderiv_add]) 1);
qed "poly_pderiv_add";

Goal "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x";
by (induct_tac "p" 1);
by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_cmult,poly_cmult,
    pderiv_def]));
qed "poly_pderiv_cmult";

Goalw [poly_minus_def] "poly (pderiv (--p)) x = poly (--(pderiv p)) x";
by (simp_tac (simpset() addsimps [poly_pderiv_cmult]) 1);
qed "poly_pderiv_minus";

Goalw [pderiv_def] 
   "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x";
by (induct_tac "t" 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,
    lemma_poly_pderiv_aux_mult]));
qed "lemma_poly_mult_pderiv";

Goal "ALL q. poly (pderiv (p *** q)) x = \
\     poly (p *** (pderiv q) +++ q *** (pderiv p)) x";
by (induct_tac "p" 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
    poly_pderiv_cmult,poly_pderiv_add,poly_mult]));
by (rtac (lemma_poly_mult_pderiv RS ssubst) 1);
by (rtac (lemma_poly_mult_pderiv RS ssubst) 1);
by (rtac (poly_add RS ssubst) 1);
by (rtac (poly_add RS ssubst) 1);
by (asm_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2] 
    @ real_add_ac @ real_mult_ac) 1);
qed "poly_pderiv_mult";

Goal "poly (pderiv (p %^ (Suc n))) x = \
    \    poly ((real (Suc n)) %* (p %^ n) *** pderiv p ) x";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,poly_pderiv_cmult,
    poly_cmult,poly_pderiv_mult,real_of_nat_zero,poly_mult,
    real_of_nat_Suc,real_add_mult_distrib2,real_add_mult_distrib]
    @ real_mult_ac));
qed "poly_pderiv_exp";

Goal "poly (pderiv ([-a, 1] %^ (Suc n))) x = \
\     poly (real (Suc n) %* ([-a, 1] %^ n)) x";
by (simp_tac (simpset() addsimps [poly_pderiv_exp,poly_mult] 
    delsimps [pexp_Suc]) 1);
by (simp_tac (simpset() addsimps [poly_cmult,pderiv_def]) 1);
qed "poly_pderiv_exp_prime";

(* ----------------------------------------------------------------------- *)
(* Key property that f(a) = 0 ==> (x - a) divides p(x).                    *)
(* ----------------------------------------------------------------------- *)

Goal "ALL h. EX q r. h#t = [r] +++ [-a, 1] *** q";
by (induct_tac "t" 1);
by (Step_tac 1);
by (res_inst_tac [("x","[]")] exI 1);
by (res_inst_tac [("x","h")] exI 1);
by (Simp_tac 1);
by (dres_inst_tac [("x","aa")] spec 1);
by (Step_tac 1);
by (res_inst_tac [("x","r#q")] exI 1);
by (res_inst_tac [("x","a*r + h")] exI 1);
by (case_tac "q" 1);
by (Auto_tac);
qed "lemma_poly_linear_rem";

Goal "EX q r. h#t = [r] +++ [-a, 1] *** q";
by (cut_inst_tac [("t","t"),("a","a")] lemma_poly_linear_rem 1);
by Auto_tac;
qed "poly_linear_rem";


Goal "(poly p a = 0) = ((p = []) | (EX q. p = [-a, 1] *** q))";
by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
    real_add_mult_distrib2]));
by (case_tac "p" 1);
by (cut_inst_tac [("h","aa"),("t","list"),("a","a")] poly_linear_rem 2);
by (Step_tac 2);
by (case_tac "q" 1);
by Auto_tac;
by (dres_inst_tac [("x","[]")] spec 1);
by (Asm_full_simp_tac 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
    real_add_assoc]));
by (dres_inst_tac [("x","aa#lista")] spec 1);
by Auto_tac;
qed "poly_linear_divides";

Goal "ALL h k a. length (k %* p +++  (h # (a %* p))) = Suc (length p)";
by (induct_tac "p" 1);
by Auto_tac;
qed "lemma_poly_length_mult";
Addsimps [lemma_poly_length_mult];

Goal "ALL h k. length (k %* p +++  (h # p)) = Suc (length p)";
by (induct_tac "p" 1);
by Auto_tac;
qed "lemma_poly_length_mult2";
Addsimps [lemma_poly_length_mult2];

Goal "length([-a ,1] *** q) = Suc (length q)";
by Auto_tac;
qed "poly_length_mult";
Addsimps [poly_length_mult];


(*-------------------------------------------------------------------------*)
(* Polynomial length                                                       *)
(*-------------------------------------------------------------------------*)

Goal "length (a %* p) = length p";
by (induct_tac "p" 1);
by Auto_tac;
qed "poly_cmult_length";
Addsimps [poly_cmult_length];

Goal "length (p1 +++ p2) = (if (length( p1 ) < length( p2 )) \
\   then (length( p2 )) else (length( p1) ))";
by (subgoal_tac "ALL p2. length (p1 +++ p2) = (if (length( p1 ) < \
\   length( p2 )) then (length( p2 )) else (length( p1) ))" 1);
by (induct_tac "p1" 2);
by (Simp_tac 2);
by (Simp_tac 2);
by (Step_tac 2);  
by (Asm_full_simp_tac 2);
by (arith_tac 2);
by (Asm_full_simp_tac 2);
by (arith_tac 2);
by (induct_tac "p2" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "poly_add_length";

Goal "length([a,b] *** p) = Suc (length p)";
by (asm_full_simp_tac (simpset() addsimps [poly_cmult_length, 
    poly_add_length]) 1);
qed "poly_root_mult_length";
Addsimps [poly_root_mult_length];

Goal "(poly (p *** q) x ~= poly [] x) = \
\     (poly p x ~= poly [] x & poly q x ~= poly [] x)";
by (auto_tac (claset(),simpset() addsimps [poly_mult,rename_numerals
    real_mult_not_zero]));
qed "poly_mult_not_eq_poly_Nil";
Addsimps [poly_mult_not_eq_poly_Nil];

Goal "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)";
by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"],
    simpset() addsimps [poly_mult]));
qed "poly_mult_eq_zero_disj";

(*-------------------------------------------------------------------------*)
(*  Normalisation Properties                                               *)
(*-------------------------------------------------------------------------*)

Goal "(pnormalize p = []) --> (poly p x = 0)";
by (induct_tac "p" 1);
by Auto_tac;
qed "poly_normalized_nil";

(*-------------------------------------------------------------------------*)
(*  A nontrivial polynomial of degree n has no more than n roots           *)
(*-------------------------------------------------------------------------*)

Goal 
   "ALL p x. (poly p x ~= poly [] x & length p = n  \
\   --> (EX i. ALL x. (poly p x = (0::real)) --> (EX m. (m <= n & x = i m))))";
by (induct_tac "n" 1);
by (Step_tac 1);
by (rtac ccontr 1);
by (subgoal_tac "EX a. poly p a = 0" 1 THEN Step_tac 1);
by (dtac (poly_linear_divides RS iffD1) 1);
by (Step_tac 1);
by (dres_inst_tac [("x","q")] spec 1);
by (dres_inst_tac [("x","x")] spec 1);
by (asm_full_simp_tac (simpset() delsimps [poly_Nil,pmult_Cons]) 1);
by (etac exE 1);
by (dres_inst_tac [("x","%m. if m = Suc n then a else i m")] spec 1);
by (Step_tac 1);
by (dtac (poly_mult_eq_zero_disj RS iffD1) 1);
by (Step_tac 1);
by (dres_inst_tac [("x","Suc(length q)")] spec 1);
by (Asm_full_simp_tac 1);
by (dres_inst_tac [("x","xa")] spec 1 THEN Step_tac 1);
by (dres_inst_tac [("x","m")] spec 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
qed_spec_mp "poly_roots_index_lemma";
bind_thm ("poly_roots_index_lemma2",conjI RS poly_roots_index_lemma);

Goal "poly p x ~= poly [] x ==> \
\     EX i. ALL x. (poly p x = 0) --> (EX n. n <= length p & x = i n)";
by (blast_tac (claset() addIs [poly_roots_index_lemma2]) 1);
qed "poly_roots_index_length";

Goal "poly p x ~= poly [] x ==> \
\     EX N i. ALL x. (poly p x = 0) --> (EX n. (n::nat) < N & x = i n)";
by (dtac poly_roots_index_length 1 THEN Step_tac 1);
by (res_inst_tac [("x","Suc (length p)")] exI 1);
by (res_inst_tac [("x","i")] exI 1);
by (auto_tac (claset(),simpset() addsimps 
    [ARITH_PROVE "(m < Suc n) = (m <= n)"]));
qed "poly_roots_finite_lemma";

(* annoying proof *)
Goal "ALL P. (ALL x. P x --> (EX n. (n::nat) < N & x = (j::nat=>real) n)) \
\     --> (EX a. ALL x. P x --> x < a)";
by (induct_tac "N" 1);
by (Asm_full_simp_tac 1);
by (Step_tac 1);
by (dres_inst_tac [("x","%z. P z & (z ~= (j::nat=>real) n)")] spec 1);
by Auto_tac;
by (dres_inst_tac [("x","x")] spec 1);
by (Step_tac 1);
by (res_inst_tac [("x","na")] exI 1);
by (auto_tac (claset() addDs [ARITH_PROVE "na < Suc n ==> na = n | na < n"],
    simpset()));
by (res_inst_tac [("x","abs a + abs(j n) + 1")] exI 1);
by (Step_tac 1);
by (dres_inst_tac [("x","x")] spec 1);
by (Step_tac 1);
by (dres_inst_tac [("x","j na")] spec 1);
by (Step_tac 1);
by (ALLGOALS(arith_tac));
qed_spec_mp "real_finite_lemma";

Goal "(poly p ~= poly []) = \
\     (EX N j. ALL x. poly p x = 0 --> (EX n. (n::nat) < N & x = j n))";
by (Step_tac 1);
by (etac swap 1 THEN rtac ext 1);
by (rtac ccontr 1);
by (clarify_tac (claset() addSDs [poly_roots_finite_lemma]) 1);
by (clarify_tac (claset() addSDs [real_finite_lemma]) 1);
by (dres_inst_tac [("x","a")] fun_cong 1);
by Auto_tac;
qed "poly_roots_finite";

(*-------------------------------------------------------------------------*)
(*  Entirety and Cancellation for polynomials                              *)
(*-------------------------------------------------------------------------*)

Goal "[| poly p ~= poly [] ; poly q ~= poly [] |] \
\     ==>  poly (p *** q) ~= poly []";
by (auto_tac (claset(),simpset() addsimps [poly_roots_finite]));
by (res_inst_tac [("x","N + Na")] exI 1);
by (res_inst_tac [("x","%n. if n < N then j n else ja (n - N)")] exI 1);
by (auto_tac (claset(),simpset() addsimps [poly_mult_eq_zero_disj]));
by (flexflex_tac THEN rotate_tac 1 1);
by (dtac spec 1 THEN Auto_tac);
qed "poly_entire_lemma";

Goal "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))";
by (auto_tac (claset() addIs [ext] addDs [fun_cong],simpset() 
    addsimps [poly_entire_lemma,poly_mult]));
by (blast_tac (claset() addIs [ccontr] addDs [poly_entire_lemma,
    poly_mult RS subst]) 1);
qed "poly_entire";

Goal "(poly (p *** q) ~= poly []) = ((poly p ~= poly []) & (poly q ~= poly []))";
by (asm_full_simp_tac (simpset() addsimps [poly_entire]) 1);
qed "poly_entire_neg";

Goal " (f = g) = (ALL x. f x = g x)";
by (auto_tac (claset() addSIs [ext],simpset()));
qed "fun_eq";

Goal "(poly (p +++ -- q) = poly []) = (poly p = poly q)";
by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def,
    fun_eq,poly_cmult,ARITH_PROVE "(p + -q = 0) = (p = (q::real))"]));
qed "poly_add_minus_zero_iff";

Goal "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))";
by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def,
    fun_eq,poly_mult,poly_cmult,real_add_mult_distrib2]));
qed "poly_add_minus_mult_eq";

Goal "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)";
by (res_inst_tac [("p1","p *** q")] (poly_add_minus_zero_iff RS subst) 1);
by (auto_tac (claset() addIs [ext], simpset() addsimps [poly_add_minus_mult_eq,
    poly_entire,poly_add_minus_zero_iff]));
qed "poly_mult_left_cancel";

Goal "(x * y = 0) = (x = (0::real) | y = 0)";
by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"],
    simpset()));
qed "real_mult_zero_disj_iff";

Goal "(poly (p %^ n) = poly []) = (poly p = poly [] & n ~= 0)";
by (simp_tac (simpset() addsimps [fun_eq]) 1);
by (rtac (CLAIM "((ALL x. P x) & Q) = (ALL x. P x & Q)" RS ssubst) 1);
by (rtac (CLAIM "f = g ==> (ALL x. f x) = (ALL x. g x)") 1);
by (rtac ext 1);
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [poly_mult,
    real_mult_zero_disj_iff]));
qed "poly_exp_eq_zero";
Addsimps [poly_exp_eq_zero];

Goal "poly [a,1] ~= poly []";
by (simp_tac (simpset() addsimps [fun_eq]) 1);
by (res_inst_tac [("x","1 - a")] exI 1);
by (Simp_tac 1);
qed "poly_prime_eq_zero";
Addsimps [poly_prime_eq_zero];

Goal "(poly ([a, 1] %^ n) ~= poly [])";
by Auto_tac;
qed "poly_exp_prime_eq_zero";
Addsimps [poly_exp_prime_eq_zero];

(*-------------------------------------------------------------------------*)
(*  A more constructive notion of polynomials being trivial                *)
(*-------------------------------------------------------------------------*)

Goal "poly (h # t) = poly [] ==> h = 0 & poly t = poly []";
by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
by (case_tac "h = 0" 1);
by (dres_inst_tac [("x","0")] spec 2);
by (rtac conjI 1);
by (rtac ((simplify (simpset()) (read_instantiate [("g","poly []")] fun_eq))
    RS iffD1) 2 THEN rtac ccontr 2);
by (auto_tac (claset(),simpset() addsimps [poly_roots_finite,
    real_mult_zero_disj_iff]));
by (dtac real_finite_lemma 1 THEN Step_tac 1);
by (REPEAT(dres_inst_tac [("x","abs a + 1")] spec 1));
by (arith_tac 1);
qed "poly_zero_lemma";

Goal "(poly p = poly []) = list_all (%c. c = 0) p";
by (induct_tac "p" 1);
by (Asm_full_simp_tac 1);
by (rtac iffI 1);
by (dtac poly_zero_lemma 1);
by Auto_tac;
qed "poly_zero";

Addsimps [real_mult_zero_disj_iff];
Goal "ALL n. (list_all (%c. c = 0) (pderiv_aux (Suc n) p) = \
\     list_all (%c. c = 0) p)";
by (induct_tac "p" 1);
by Auto_tac;
qed_spec_mp "pderiv_aux_iszero";
Addsimps [pderiv_aux_iszero];

Goal "(number_of n :: nat) ~= 0 \
\     ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) = \
\     list_all (%c. c = 0) p)";
by (res_inst_tac [("n1","number_of n"),("m1","0")] (less_imp_Suc_add RS exE) 1);
by (Force_tac 1);
by (res_inst_tac [("n1","0 + x")] (pderiv_aux_iszero RS subst) 1);
by (asm_simp_tac (simpset() delsimps [pderiv_aux_iszero]) 1);
qed "pderiv_aux_iszero_num";

Goal "poly (pderiv p) = poly [] --> (EX h. poly p = poly [h])";
by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1);
by (induct_tac "p" 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons,
    pderiv_aux_iszero_num] delsimps [poly_Cons]) 1);
by (auto_tac (claset(),simpset() addsimps [poly_zero RS sym]));
qed_spec_mp "pderiv_iszero";

Goal "poly p = poly [] --> (poly (pderiv p) = poly [])";
by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1);
by (induct_tac "p" 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons,
    pderiv_aux_iszero_num] delsimps [poly_Cons]) 1);
qed "pderiv_zero_obj";

Goal "poly p = poly [] ==> (poly (pderiv p) = poly [])";
by (blast_tac (claset() addEs [pderiv_zero_obj RS impE]) 1);
qed "pderiv_zero";
Addsimps [pderiv_zero];

Goal "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))";
by (cut_inst_tac [("p","p +++ --q")] pderiv_zero_obj 1);
by (auto_tac (claset() addIs [ ARITH_PROVE "x + - y = 0 ==> x = (y::real)"],
    simpset() addsimps [fun_eq,poly_add,poly_minus,poly_pderiv_add,
    poly_pderiv_minus] delsimps [pderiv_zero]));
qed "poly_pderiv_welldef";

(* ------------------------------------------------------------------------- *)
(* Basics of divisibility.                                                   *)
(* ------------------------------------------------------------------------- *)

Goal "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)";
by (auto_tac (claset(),simpset() addsimps [divides_def,fun_eq,poly_mult,
    poly_add,poly_cmult,real_add_mult_distrib RS sym]));
by (dres_inst_tac [("x","-a")] spec 1);
by (auto_tac (claset(),simpset() addsimps [poly_linear_divides,poly_add,
    poly_cmult,real_add_mult_distrib RS sym]));
by (res_inst_tac [("x","qa *** q")] exI 1);
by (res_inst_tac [("x","p *** qa")] exI 2);
by (auto_tac (claset(),simpset() addsimps [poly_add,poly_mult,
    poly_cmult] @ real_mult_ac));
qed "poly_primes";

Goalw [divides_def] "p divides p";
by (res_inst_tac [("x","[1]")] exI 1);
by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq]));
qed "poly_divides_refl";
Addsimps [poly_divides_refl];

Goalw [divides_def] "[| p divides q; q divides r |] ==> p divides r";
by (Step_tac 1);
by (res_inst_tac [("x","qa *** qaa")] exI 1);
by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,
    real_mult_assoc]));
qed "poly_divides_trans";

Goal "(m::nat) <= n = (EX d. n = m + d)";
by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
    less_iff_Suc_add]));
qed "le_iff_add";

Goal "m <= n ==> (p %^ m) divides (p %^ n)";
by (auto_tac (claset(),simpset() addsimps [le_iff_add]));
by (induct_tac "d" 1);
by (rtac poly_divides_trans 2);
by (auto_tac (claset(),simpset() addsimps [divides_def]));
by (res_inst_tac [("x","p")] exI 1);
by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq]
    @ real_mult_ac));
qed "poly_divides_exp";

Goal "[| (p %^ n) divides q;  m <= n |] ==> (p %^ m) divides q";
by (blast_tac (claset() addIs [poly_divides_exp,poly_divides_trans]) 1);
qed "poly_exp_divides";

Goalw [divides_def] 
   "[| p divides q; p divides r |] ==> p divides (q +++ r)";
by Auto_tac;
by (res_inst_tac [("x","qa +++ qaa")] exI 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
    real_add_mult_distrib2]));
qed "poly_divides_add";

Goalw [divides_def] 
   "[| p divides q; p divides (q +++ r) |] ==> p divides r";
by Auto_tac;
by (res_inst_tac [("x","qaa +++ -- qa")] exI 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
    poly_minus,real_add_mult_distrib2,
    ARITH_PROVE "(x = y + -z) = (z + x = (y::real))"]));
qed "poly_divides_diff";

Goal "[| p divides r; p divides (q +++ r) |] ==> p divides q";
by (etac poly_divides_diff 1);
by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
    divides_def] @ real_add_ac));
qed "poly_divides_diff2";

Goalw [divides_def] "poly p = poly [] ==> q divides p";
by (auto_tac (claset(),simpset() addsimps [fun_eq,poly_mult]));
qed "poly_divides_zero";

Goalw [divides_def] "q divides []";
by (res_inst_tac [("x","[]")] exI 1); 
by (auto_tac (claset(),simpset() addsimps [fun_eq]));
qed "poly_divides_zero2";
Addsimps [poly_divides_zero2];

(* ------------------------------------------------------------------------- *)
(* At last, we can consider the order of a root.                             *)
(* ------------------------------------------------------------------------- *)

(* FIXME: Tidy up *)
Goal "[| length p = d; poly p ~= poly [] |] \
\     ==> EX n. ([-a, 1] %^ n) divides p & \
\               ~(([-a, 1] %^ (Suc n)) divides p)";
by (subgoal_tac "ALL p. length p = d & poly p ~= poly [] \
\     --> (EX n q. p = mulexp n [-a, 1] q & poly q a ~= 0)" 1);
by (induct_tac "d" 2);
by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 2);
by (Step_tac 2);
by (case_tac "poly pa a = 0" 2);
by (dtac (poly_linear_divides RS iffD1) 2);
by (Step_tac 2);
by (dres_inst_tac [("x","q")] spec 2);
by (dtac (poly_entire_neg RS iffD1) 2);
by (Step_tac 2);
by (Force_tac 2 THEN Blast_tac 2);
by (res_inst_tac [("x","Suc na")] exI 2);
by (res_inst_tac [("x","qa")] exI 2);
by (asm_full_simp_tac (simpset() delsimps [pmult_Cons]) 2);
by (res_inst_tac [("x","0")] exI 2);
by (Force_tac 2);
by (dres_inst_tac [("x","p")] spec 1 THEN Step_tac 1);
by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1);
by (rewtac divides_def);
by (res_inst_tac [("x","q")] exI 1);
by (induct_tac "n" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [poly_add,poly_cmult,poly_mult,
    real_add_mult_distrib2] @ real_mult_ac) 1);
by (Step_tac 1);
by (rotate_tac 2 1);
by (rtac swap 1 THEN assume_tac 2);
by (induct_tac "n" 1);
by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
by (eres_inst_tac [("Pa","poly q a = 0")] swap 1);
by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult]) 1);
by (rtac (pexp_Suc RS ssubst) 1);
by (rtac ccontr 1);
by (asm_full_simp_tac (simpset() addsimps [poly_mult_left_cancel,
    poly_mult_assoc] delsimps [pmult_Cons,pexp_Suc]) 1);
qed "poly_order_exists";

Goalw [divides_def] "[1] divides p";
by Auto_tac;
qed "poly_one_divides";
Addsimps [poly_one_divides];

Goal "poly p ~= poly [] \
\     ==> EX! n. ([-a, 1] %^ n) divides p & \
\                ~(([-a, 1] %^ (Suc n)) divides p)";
by (auto_tac (claset() addIs [poly_order_exists],
    simpset() addsimps [less_linear] delsimps [pmult_Cons,pexp_Suc]));
by (cut_inst_tac [("m","y"),("n","n")] less_linear 1);
by (dres_inst_tac [("m","n")] poly_exp_divides 1);
by (auto_tac (claset() addDs [ARITH_PROVE "n < m ==> Suc n <= m" RSN  
    (2,poly_exp_divides)],simpset() delsimps [pmult_Cons,pexp_Suc]));
qed "poly_order";

(* ------------------------------------------------------------------------- *)
(* Order                                                                     *)
(* ------------------------------------------------------------------------- *)

Goal "[| n = (@n. P n); EX! n. P n |] ==> P n";
by (blast_tac (claset() addIs [someI2]) 1);
qed "some1_equalityD";

Goalw [order_def]
      "(([-a, 1] %^ n) divides p & \
\       ~(([-a, 1] %^ (Suc n)) divides p)) = \
\       ((n = order a p) & ~(poly p = poly []))";
by (rtac iffI 1);
by (blast_tac (claset() addDs [poly_divides_zero] 
    addSIs [some1_equality RS sym, poly_order]) 1);
by (blast_tac (claset() addSIs [poly_order RSN (2,some1_equalityD)]) 1);
qed "order";

Goal "[| poly p ~= poly [] |] \
\     ==> ([-a, 1] %^ (order a p)) divides p & \
\             ~(([-a, 1] %^ (Suc(order a p))) divides p)";
by (asm_full_simp_tac (simpset() addsimps [order] delsimps [pexp_Suc]) 1);
qed "order2";

Goal "[| poly p ~= poly []; ([-a, 1] %^ n) divides p; \
\        ~(([-a, 1] %^ (Suc n)) divides p) \
\     |] ==> (n = order a p)";
by (cut_inst_tac [("p","p"),("a","a"),("n","n")] order 1);
by Auto_tac;
qed "order_unique";

Goal "(poly p ~= poly [] & ([-a, 1] %^ n) divides p & \
\        ~(([-a, 1] %^ (Suc n)) divides p)) \
\     ==> (n = order a p)";
by (blast_tac (claset() addIs [order_unique]) 1);
qed "order_unique_lemma";

Goal "poly p = poly q ==> order a p = order a q";
by (auto_tac (claset(),simpset() addsimps [fun_eq,divides_def,poly_mult,
    order_def]));
qed "order_poly";

Goal "p %^ (Suc 0) = p";
by (induct_tac "p" 1);
by (auto_tac (claset(),simpset() addsimps [numeral_1_eq_1]));
qed "pexp_one";
Addsimps [pexp_one];

Goal "ALL p a. 0 < n & [- a, 1] %^ n divides p & \
\            ~ [- a, 1] %^ (Suc n) divides p \
\            --> poly p a = 0";
by (induct_tac "n" 1);
by (Blast_tac 1);
by (auto_tac (claset(),simpset() addsimps [divides_def,poly_mult] 
    delsimps [pmult_Cons]));
qed_spec_mp "lemma_order_root";

Goal "(poly p a = 0) = ((poly p = poly []) | order a p ~= 0)";
by (case_tac "poly p = poly []" 1);
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [poly_linear_divides]
    delsimps [pmult_Cons]) 1);
by (Step_tac 1);
by (ALLGOALS(dres_inst_tac [("a","a")] order2));
by (rtac ccontr 1);
by (asm_full_simp_tac (simpset() addsimps [divides_def,poly_mult,fun_eq]
    delsimps [pmult_Cons]) 1);
by (Blast_tac 1);
by (blast_tac (claset() addIs [lemma_order_root]) 1);
qed "order_root";

Goal "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n <= order a p)";
by (case_tac "poly p = poly []" 1);
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_mult]) 1);
by (res_inst_tac [("x","[]")] exI 1);
by (TRYALL(dres_inst_tac [("a","a")] order2));
by (auto_tac (claset() addIs [poly_exp_divides],simpset()
    delsimps [pexp_Suc]));
qed "order_divides";

Goalw [divides_def] 
     "poly p ~= poly [] \
\     ==> EX q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) & \
\               ~([-a, 1] divides q)";
by (dres_inst_tac [("a","a")] order2 1);
by (asm_full_simp_tac (simpset() addsimps [divides_def]
     delsimps [pexp_Suc,pmult_Cons]) 1);
by (Step_tac 1);
by (res_inst_tac [("x","q")] exI 1);
by (Step_tac 1);
by (dres_inst_tac [("x","qa")] spec 1);
by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,poly_exp] 
    @ real_mult_ac delsimps [pmult_Cons]));
qed "order_decomp";

(* ------------------------------------------------------------------------- *)
(* Important composition properties of orders.                               *)
(* ------------------------------------------------------------------------- *)

Goal "poly (p *** q) ~= poly [] \
\     ==> order a (p *** q) = order a p + order a q";
by (cut_inst_tac [("a","a"),("p","p***q"),("n","order a p + order a q")] 
    order 1);
by (auto_tac (claset(),simpset() addsimps [poly_entire] delsimps [pmult_Cons]));
by (REPEAT(dres_inst_tac [("a","a")] order2 1));
by (Step_tac 1);
by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_exp_add,
    poly_mult] delsimps [pmult_Cons]) 1);
by (Step_tac 1);
by (res_inst_tac [("x","qa *** qaa")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [poly_mult] @ real_mult_ac
    delsimps [pmult_Cons]) 1);
by (REPEAT(dres_inst_tac [("a","a")] order_decomp 1));
by (Step_tac 1);
by (subgoal_tac "[-a,1] divides (qa *** qaa)" 1);
by (asm_full_simp_tac (simpset() addsimps [poly_primes] 
    delsimps [pmult_Cons]) 1);
by (auto_tac (claset(),simpset() addsimps [divides_def] 
    delsimps [pmult_Cons]));
by (res_inst_tac [("x","qb")] exI 1);
by (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = \
\                poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))" 1);
by (dtac (poly_mult_left_cancel RS iffD1) 1);
by (Force_tac 1);
by (subgoal_tac "poly ([-a, 1] %^ (order a q) *** \
\                      ([-a, 1] %^ (order a p) *** (qa *** qaa))) = \
\                poly ([-a, 1] %^ (order a q) *** \
\                      ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb)))" 1);
by (dtac (poly_mult_left_cancel RS iffD1) 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_exp_add,poly_mult] 
    @ real_mult_ac delsimps [pmult_Cons]) 1);
qed "order_mult";

(* FIXME: too too long! *)
Goal "ALL p q a. 0 < n &  \
\      poly (pderiv p) ~= poly [] & \
\      poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q \
\      --> n = Suc (order a (pderiv p))";
by (induct_tac "n" 1);
by (Step_tac 1);
by (rtac order_unique_lemma 1 THEN rtac conjI 1);
by (assume_tac 1);
by (subgoal_tac "ALL r. r divides (pderiv p) = \
\                       r divides (pderiv ([-a, 1] %^ Suc n *** q))" 1);
by (dtac poly_pderiv_welldef 2);
by (asm_full_simp_tac (simpset() addsimps [divides_def] delsimps [pmult_Cons,
    pexp_Suc]) 2);
by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
by (rtac conjI 1);
by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq] 
    delsimps [pmult_Cons,pexp_Suc]) 1);
by (res_inst_tac 
    [("x","[-a, 1] *** (pderiv q) +++ real (Suc n) %* q")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [poly_pderiv_mult,
    poly_pderiv_exp_prime,poly_add,poly_mult,poly_cmult,
    real_add_mult_distrib2] @ real_mult_ac
    delsimps [pmult_Cons,pexp_Suc]) 1);
by (asm_full_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2,
    real_add_mult_distrib] @ real_mult_ac delsimps [pmult_Cons]) 1);
by (thin_tac "ALL r. \
\             r divides pderiv p = \
\             r divides pderiv ([- a, 1] %^ Suc n *** q)" 1);
by (rewtac divides_def);
by (simp_tac (simpset() addsimps [poly_pderiv_mult,
    poly_pderiv_exp_prime,fun_eq,poly_add,poly_mult] 
    delsimps [pmult_Cons,pexp_Suc]) 1);
by (rtac swap 1 THEN assume_tac 1);
by (rotate_tac  3 1 THEN etac swap 1);
by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
by (Step_tac 1);
by (res_inst_tac [("x","inverse(real (Suc n)) %* (qa +++ --(pderiv q))")]
    exI 1);
by (subgoal_tac "poly ([-a, 1] %^ n *** q) = \
\         poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* \
\         (qa +++ -- (pderiv q)))))" 1);
by (dtac (poly_mult_left_cancel RS iffD1) 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult,
    poly_minus] delsimps [pmult_Cons]) 1);
by (Step_tac 1);
by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel 
    RS iffD1) 1);
by (Simp_tac 1);
by (rtac ((CLAIM_SIMP 
    "a * (b * (c * (d * e))) = e * (b * (c * (d * (a::real))))" 
     real_mult_ac) RS ssubst) 1);
by (rotate_tac 2 1);
by (dres_inst_tac [("x","xa")] spec 1);
by (asm_full_simp_tac (simpset()
    addsimps [real_add_mult_distrib] @ real_mult_ac
    delsimps [pmult_Cons]) 1);
qed_spec_mp "lemma_order_pderiv";

Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \
\     ==> (order a p = Suc (order a (pderiv p)))";
by (case_tac "poly p = poly []" 1);
by (auto_tac (claset() addDs [pderiv_zero],simpset()));
by (dres_inst_tac [("a","a"),("p","p")] order_decomp 1);
by (blast_tac (claset() addIs [lemma_order_pderiv]) 1);
qed "order_pderiv";

(* ------------------------------------------------------------------------- *)
(* Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
(* `a la Harrison                                                            *)
(* ------------------------------------------------------------------------- *)

Goal "[| poly (pderiv p) ~= poly []; \
\        poly p = poly (q *** d); \
\        poly (pderiv p) = poly (e *** d); \
\        poly d = poly (r *** p +++ s *** pderiv p) \
\     |] ==> order a q = (if order a p = 0 then 0 else 1)";
by (subgoal_tac "order a p = order a q + order a d" 1);
by (res_inst_tac [("s","order a (q *** d)")] trans 2);
by (blast_tac (claset() addIs [order_poly]) 2);
by (rtac order_mult 2);
by (rtac notI 2 THEN Asm_full_simp_tac 2);
by (case_tac "order a p = 0" 1);
by (Asm_full_simp_tac 1);
by (subgoal_tac "order a (pderiv p) = order a e + order a d" 1);
by (res_inst_tac [("s","order a (e *** d)")] trans 2);
by (blast_tac (claset() addIs [order_poly]) 2);
by (rtac order_mult 2);
by (rtac notI 2 THEN Asm_full_simp_tac 2);
by (case_tac "poly p = poly []" 1);
by (dres_inst_tac [("p","p")] pderiv_zero 1);
by (Asm_full_simp_tac 1);
by (dtac order_pderiv 1 THEN assume_tac 1);
by (subgoal_tac "order a (pderiv p) <= order a d" 1);
by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides d" 2);
by (asm_full_simp_tac (simpset() addsimps [poly_entire,order_divides]) 2);
by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides p & \
\       ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p)" 2);
by (asm_simp_tac (simpset() addsimps [order_divides]) 3);
by (asm_full_simp_tac (simpset() addsimps [divides_def]
    delsimps [pexp_Suc,pmult_Cons]) 2);
by (Step_tac 2);
by (res_inst_tac [("x","r *** qa +++ s *** qaa")] exI 2);
by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_add,poly_mult,
    real_add_mult_distrib, real_add_mult_distrib2] @ real_mult_ac
    delsimps [pexp_Suc,pmult_Cons]) 2);
by Auto_tac;
qed "poly_squarefree_decomp_order";


Goal "[| poly (pderiv p) ~= poly []; \
\        poly p = poly (q *** d); \
\        poly (pderiv p) = poly (e *** d); \
\        poly d = poly (r *** p +++ s *** pderiv p) \
\     |] ==> ALL a. order a q = (if order a p = 0 then 0 else 1)";
by (blast_tac (claset() addIs [poly_squarefree_decomp_order]) 1);
qed "poly_squarefree_decomp_order2";

Goal "poly p ~= poly [] ==> (poly p a = 0) = (order a p ~= 0)";
by (rtac (order_root RS ssubst) 1);
by Auto_tac;
qed "order_root2";

Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \
\     ==> (order a (pderiv p) = n) = (order a p = Suc n)";
by (auto_tac (claset() addDs [order_pderiv],simpset()));
qed "order_pderiv2";

Goalw [rsquarefree_def]
  "rsquarefree p = (ALL a. ~(poly p a = 0 & poly (pderiv p) a = 0))";
by (case_tac "poly p = poly []" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (case_tac "poly (pderiv p) = poly []" 1);
by (Asm_full_simp_tac 1);
by (dtac pderiv_iszero 1 THEN Clarify_tac 1);
by (subgoal_tac "ALL a. order a p = order a [h]" 1);
by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
by (rtac allI 1);
by (cut_inst_tac [("p","[h]"),("a","a")] order_root 1);
by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
by (blast_tac (claset() addIs [order_poly]) 1);
by (auto_tac (claset(),simpset() addsimps [order_root,order_pderiv2]));
by (dtac spec 1 THEN Auto_tac);
qed "rsquarefree_roots";

Goal "[1] *** p = p";
by Auto_tac;
qed "pmult_one";
Addsimps [pmult_one];

Goal "poly [] = poly [0]";
by (simp_tac (simpset() addsimps [fun_eq]) 1);
qed "poly_Nil_zero";

Goalw [rsquarefree_def]
     "[| rsquarefree p; poly p a = 0 |] \
\     ==> EX q. (poly p = poly ([-a, 1] *** q)) & poly q a ~= 0";
by (Step_tac 1);
by (forw_inst_tac [("a","a")] order_decomp 1);
by (dres_inst_tac [("x","a")] spec 1);
by (dres_inst_tac [("a1","a")] (order_root2 RS sym) 1);
by (auto_tac (claset(),simpset() delsimps [pmult_Cons]));
by (res_inst_tac [("x","q")] exI 1 THEN Step_tac 1);
by (asm_full_simp_tac (simpset() addsimps [poly_mult,fun_eq]) 1);
by (dres_inst_tac [("p1","q")] (poly_linear_divides RS iffD1) 1);
by (asm_full_simp_tac (simpset() addsimps [divides_def]
    delsimps [pmult_Cons]) 1);
by (Step_tac 1);
by (dres_inst_tac [("x","[]")] spec 1); 
by (auto_tac (claset(),simpset() addsimps [fun_eq]));
qed "rsquarefree_decomp";

Goal "[| poly (pderiv p) ~= poly []; \
\        poly p = poly (q *** d); \
\        poly (pderiv p) = poly (e *** d); \
\        poly d = poly (r *** p +++ s *** pderiv p) \
\     |] ==> rsquarefree q & (ALL a. (poly q a = 0) = (poly p a = 0))";
by (ftac poly_squarefree_decomp_order2 1);
by (TRYALL(assume_tac));
by (case_tac "poly p = poly []" 1);
by (blast_tac (claset() addDs [pderiv_zero]) 1);
by (simp_tac (simpset() addsimps [rsquarefree_def,
    order_root] delsimps [pmult_Cons]) 1);
by (asm_full_simp_tac (simpset() addsimps [poly_entire] 
    delsimps [pmult_Cons]) 1);
qed "poly_squarefree_decomp";


(* ------------------------------------------------------------------------- *)
(* Normalization of a polynomial.                                            *)
(* ------------------------------------------------------------------------- *)

Goal "poly (pnormalize p) = poly p";
by (induct_tac "p" 1);
by (auto_tac (claset(),simpset() addsimps [fun_eq]));
qed "poly_normalize";
Addsimps [poly_normalize];


(* ------------------------------------------------------------------------- *)
(* The degree of a polynomial.                                               *)
(* ------------------------------------------------------------------------- *)

Goal "list_all (%c. c = 0) p -->  pnormalize p = []";
by (induct_tac "p" 1);
by Auto_tac;
qed_spec_mp "lemma_degree_zero";

Goalw [degree_def] "poly p = poly [] ==> degree p = 0";
by (case_tac "pnormalize p = []" 1);
by (auto_tac (claset() addDs [lemma_degree_zero],simpset() 
    addsimps [poly_zero]));
qed "degree_zero";

(* ------------------------------------------------------------------------- *)
(* Tidier versions of finiteness of roots.                                   *)
(* ------------------------------------------------------------------------- *)

Goal "poly p ~= poly [] ==> finite {x. poly p x = 0}";
by (auto_tac (claset(),simpset() addsimps [poly_roots_finite]));
by (res_inst_tac [("B","{x::real. EX n. (n::nat) < N & (x = j n)}")] 
    finite_subset 1);
by (induct_tac "N" 2);
by Auto_tac;
by (subgoal_tac "{x::real. EX na. na < Suc n & (x = j na)} = \
\                 {(j n)} Un {x. EX na. na < n & (x = j na)}" 1);
by (auto_tac (claset(),simpset() addsimps [ARITH_PROVE 
    "(na < Suc n) = (na = n | na < n)"]));
qed "poly_roots_finite_set";

(* ------------------------------------------------------------------------- *)
(* bound for polynomial.                                                     *)
(* ------------------------------------------------------------------------- *)

Goal "abs(x) <= k --> abs(poly p x) <= poly (map abs p) k";
by (induct_tac "p" 1);
by Auto_tac;
by (res_inst_tac [("j","abs a + abs(x * poly list x)")] real_le_trans 1);
by (rtac abs_triangle_ineq 1);
by (auto_tac (claset() addSIs [real_mult_le_mono],simpset() 
    addsimps [abs_mult]));
by (arith_tac 1);
qed_spec_mp "poly_mono";