--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/MacLaurin.ML Fri Nov 16 18:24:11 2001 +0100
@@ -0,0 +1,726 @@
+(* Title : MacLaurin.thy
+ Author : Jacques D. Fleuriot
+ Copyright : 2001 University of Edinburgh
+ Description : MacLaurin series
+*)
+
+Goal "sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sumr_offset";
+
+Goal "ALL f. sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sumr_offset2";
+
+Goal "sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";
+by (simp_tac (simpset() addsimps [sumr_offset]) 1);
+qed "sumr_offset3";
+
+Goal "ALL n f. sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";
+by (simp_tac (simpset() addsimps [sumr_offset]) 1);
+qed "sumr_offset4";
+
+Goal "0 < n ==> \
+\ sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else \
+\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = \
+\ sumr 0 (Suc n) (%n. (if even(n) then 0 else \
+\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)";
+by (res_inst_tac [("n1","1")] (sumr_split_add RS subst) 1);
+by Auto_tac;
+qed "sumr_from_1_from_0";
+
+(*---------------------------------------------------------------------------*)
+(* Maclaurin's theorem with Lagrange form of remainder *)
+(*---------------------------------------------------------------------------*)
+
+(* Annoying: Proof is now even longer due mostly to
+ change in behaviour of simplifier since Isabelle99 *)
+Goal " [| 0 < h; 0 < n; diff 0 = f; \
+\ ALL m t. \
+\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \
+\ ==> EX t. 0 < t & \
+\ t < h & \
+\ f h = \
+\ sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + \
+\ (diff n t / real (fact n)) * h ^ n";
+by (case_tac "n = 0" 1);
+by (Force_tac 1);
+by (dtac not0_implies_Suc 1);
+by (etac exE 1);
+by (subgoal_tac
+ "EX B. f h = sumr 0 n (%m. (diff m 0 / real (fact m)) * (h ^ m)) \
+\ + (B * ((h ^ n) / real (fact n)))" 1);
+
+by (simp_tac (HOL_ss addsimps [real_add_commute, real_divide_def,
+ ARITH_PROVE "(x = z + (y::real)) = (x - y = z)"]) 2);
+by (res_inst_tac
+ [("x","(f(h) - sumr 0 n (%m. (diff(m)(0) / real (fact m)) * (h ^ m))) \
+\ * real (fact n) / (h ^ n)")] exI 2);
+by (simp_tac (HOL_ss addsimps [real_mult_assoc,real_divide_def]) 2);
+ by (rtac (CLAIM "x = (1::real) ==> a = a * (x::real)") 2);
+by (asm_simp_tac (HOL_ss addsimps
+ [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"]
+ delsimps [realpow_Suc]) 2);
+by (rtac (real_mult_inv_left RS ssubst) 2);
+by (rtac (real_mult_inv_left RS ssubst) 3);
+by (dtac (realpow_gt_zero RS real_not_refl2 RS not_sym) 2);
+by (assume_tac 2);
+by (rtac real_of_nat_fact_not_zero 2);
+by (Simp_tac 2);
+by (etac exE 1);
+by (cut_inst_tac [("b","%t. f t - \
+\ (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \
+\ (B * ((t ^ n) / real (fact n))))")]
+ (CLAIM "EX g. g = b") 1);
+by (etac exE 1);
+by (subgoal_tac "g 0 = 0 & g h =0" 1);
+by (asm_simp_tac (simpset() addsimps
+ [ARITH_PROVE "(x - y = z) = (x = z + (y::real))"]
+ delsimps [sumr_Suc]) 2);
+by (cut_inst_tac [("n","m"),("k","1")] sumr_offset2 2);
+by (asm_full_simp_tac (simpset() addsimps
+ [ARITH_PROVE "(x = y - z) = (y = x + (z::real))"]
+ delsimps [sumr_Suc]) 2);
+by (cut_inst_tac [("b","%m t. diff m t - \
+\ (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) \
+\ + (B * ((t ^ (n - m)) / real (fact(n - m)))))")]
+ (CLAIM "EX difg. difg = b") 1);
+by (etac exE 1);
+by (subgoal_tac "difg 0 = g" 1);
+by (asm_simp_tac (simpset() delsimps [realpow_Suc,fact_Suc]) 2);
+by (subgoal_tac "ALL m t. m < n & 0 <= t & t <= h --> \
+\ DERIV (difg m) t :> difg (Suc m) t" 1);
+by (Clarify_tac 2);
+by (rtac DERIV_diff 2);
+by (Asm_simp_tac 2);
+by DERIV_tac;
+by DERIV_tac;
+by (rtac lemma_DERIV_subst 3);
+by (rtac DERIV_quotient 3);
+by (rtac DERIV_const 4);
+by (rtac DERIV_pow 3);
+by (asm_simp_tac (simpset() addsimps [real_inverse_distrib,
+ CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e"
+ real_mult_ac,fact_diff_Suc]) 4);
+by (Asm_simp_tac 3);
+by (forw_inst_tac [("m","ma")] less_add_one 2);
+by (Clarify_tac 2);
+by (asm_simp_tac (simpset() addsimps
+ [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"]
+ delsimps [sumr_Suc]) 2);
+by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])
+ (read_instantiate [("k","1")] sumr_offset4))]
+ delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
+by (rtac lemma_DERIV_subst 2);
+by (rtac DERIV_add 2);
+by (rtac DERIV_const 3);
+by (rtac DERIV_sumr 2);
+by (Clarify_tac 2);
+by (Simp_tac 3);
+by (simp_tac (simpset() addsimps [real_divide_def,real_mult_assoc]
+ delsimps [fact_Suc,realpow_Suc]) 2);
+by (rtac DERIV_cmult 2);
+by (rtac lemma_DERIV_subst 2);
+by DERIV_tac;
+by (rtac (fact_Suc RS ssubst) 2);
+by (rtac (real_of_nat_mult RS ssubst) 2);
+by (simp_tac (simpset() addsimps [real_inverse_distrib] @
+ real_mult_ac) 2);
+by (subgoal_tac "ALL ma. ma < n --> \
+\ (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1);
+by (rotate_tac 11 1);
+by (dres_inst_tac [("x","m")] spec 1);
+by (etac impE 1);
+by (Asm_simp_tac 1);
+by (etac exE 1);
+by (res_inst_tac [("x","t")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [ARITH_PROVE "(x - y = 0) = (y = (x::real))"]
+ delsimps [realpow_Suc,fact_Suc]) 1);
+by (subgoal_tac "ALL m. m < n --> difg m 0 = 0" 1);
+by (Clarify_tac 2);
+by (Asm_simp_tac 2);
+by (forw_inst_tac [("m","ma")] less_add_one 2);
+by (Clarify_tac 2);
+by (asm_simp_tac (simpset() delsimps [sumr_Suc]) 2);
+by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])
+ (read_instantiate [("k","1")] sumr_offset4))]
+ delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
+by (subgoal_tac "ALL m. m < n --> (EX t. 0 < t & t < h & \
+\ DERIV (difg m) t :> 0)" 1);
+by (rtac allI 1 THEN rtac impI 1);
+by (rotate_tac 12 1);
+by (dres_inst_tac [("x","ma")] spec 1);
+by (etac impE 1 THEN assume_tac 1);
+by (etac exE 1);
+by (res_inst_tac [("x","t")] exI 1);
+(* do some tidying up *)
+by (ALLGOALS(thin_tac "difg = \
+\ (%m t. diff m t - \
+\ (sumr 0 (n - m) \
+\ (%p. diff (m + p) 0 / real (fact p) * t ^ p) + \
+\ B * (t ^ (n - m) / real (fact (n - m)))))"));
+by (ALLGOALS(thin_tac "g = \
+\ (%t. f t - \
+\ (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + \
+\ B * (t ^ n / real (fact n))))"));
+by (ALLGOALS(thin_tac "f h = \
+\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
+\ B * (h ^ n / real (fact n))"));
+(* back to business *)
+by (Asm_simp_tac 1);
+by (rtac DERIV_unique 1);
+by (Blast_tac 2);
+by (Force_tac 1);
+by (rtac allI 1 THEN induct_tac "ma" 1);
+by (rtac impI 1 THEN rtac Rolle 1);
+by (assume_tac 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "ALL t. 0 <= t & t <= h --> g differentiable t" 1);
+by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
+by (blast_tac (claset() addDs [DERIV_isCont]) 1);
+by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x","difg (Suc 0) t")] exI 1);
+by (Force_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x","difg (Suc 0) x")] exI 1);
+by (Force_tac 1);
+by (Step_tac 1);
+by (Force_tac 1);
+by (subgoal_tac "EX ta. 0 < ta & ta < t & \
+\ DERIV difg (Suc n) ta :> 0" 1);
+by (rtac Rolle 2 THEN assume_tac 2);
+by (Asm_full_simp_tac 2);
+by (rotate_tac 2 2);
+by (dres_inst_tac [("x","n")] spec 2);
+by (ftac (ARITH_PROVE "n < m ==> n < Suc m") 2);
+by (rtac DERIV_unique 2);
+by (assume_tac 3);
+by (Force_tac 2);
+by (subgoal_tac
+ "ALL ta. 0 <= ta & ta <= t --> (difg (Suc n)) differentiable ta" 2);
+by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
+by (blast_tac (claset() addSDs [DERIV_isCont]) 2);
+by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
+by (Clarify_tac 2);
+by (res_inst_tac [("x","difg (Suc (Suc n)) ta")] exI 2);
+by (Force_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
+by (Clarify_tac 2);
+by (res_inst_tac [("x","difg (Suc (Suc n)) x")] exI 2);
+by (Force_tac 2);
+by (Step_tac 1);
+by (res_inst_tac [("x","ta")] exI 1);
+by (Force_tac 1);
+qed "Maclaurin";
+
+Goal "0 < h & 0 < n & diff 0 = f & \
+\ (ALL m t. \
+\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \
+\ --> (EX t. 0 < t & \
+\ t < h & \
+\ f h = \
+\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
+\ diff n t / real (fact n) * h ^ n)";
+by (blast_tac (claset() addIs [Maclaurin]) 1);
+qed "Maclaurin_objl";
+
+Goal " [| 0 < h; diff 0 = f; \
+\ ALL m t. \
+\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \
+\ ==> EX t. 0 < t & \
+\ t <= h & \
+\ f h = \
+\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
+\ diff n t / real (fact n) * h ^ n";
+by (case_tac "n" 1);
+by Auto_tac;
+by (dtac Maclaurin 1 THEN Auto_tac);
+qed "Maclaurin2";
+
+Goal "0 < h & diff 0 = f & \
+\ (ALL m t. \
+\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \
+\ --> (EX t. 0 < t & \
+\ t <= h & \
+\ f h = \
+\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
+\ diff n t / real (fact n) * h ^ n)";
+by (blast_tac (claset() addIs [Maclaurin2]) 1);
+qed "Maclaurin2_objl";
+
+Goal " [| h < 0; 0 < n; diff 0 = f; \
+\ ALL m t. \
+\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t |] \
+\ ==> EX t. h < t & \
+\ t < 0 & \
+\ f h = \
+\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
+\ diff n t / real (fact n) * h ^ n";
+by (cut_inst_tac [("f","%x. f (-x)"),
+ ("diff","%n x. ((- 1) ^ n) * diff n (-x)"),
+ ("h","-h"),("n","n")] Maclaurin_objl 1);
+by (Asm_full_simp_tac 1);
+by (etac impE 1 THEN Step_tac 1);
+by (rtac (real_minus_mult_eq2 RS ssubst) 1);
+by (rtac DERIV_cmult 1);
+by (rtac lemma_DERIV_subst 1);
+by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1);
+by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2);
+by (Force_tac 2);
+by (Force_tac 1);
+by (res_inst_tac [("x","-t")] exI 1);
+by Auto_tac;
+by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (Asm_full_simp_tac 1);
+by (auto_tac (claset(),simpset() addsimps [real_divide_def,
+ CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))",
+ realpow_mult RS sym]));
+qed "Maclaurin_minus";
+
+Goal "(h < 0 & 0 < n & diff 0 = f & \
+\ (ALL m t. \
+\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\
+\ --> (EX t. h < t & \
+\ t < 0 & \
+\ f h = \
+\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
+\ diff n t / real (fact n) * h ^ n)";
+by (blast_tac (claset() addIs [Maclaurin_minus]) 1);
+qed "Maclaurin_minus_objl";
+
+(* ------------------------------------------------------------------------- *)
+(* More convenient "bidirectional" version. *)
+(* ------------------------------------------------------------------------- *)
+
+(* not good for PVS sin_approx, cos_approx *)
+Goal " [| diff 0 = f; \
+\ ALL m t. \
+\ m < n & abs t <= abs x --> DERIV (diff m) t :> diff (Suc m) t |] \
+\ ==> EX t. abs t <= abs x & \
+\ f x = \
+\ sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + \
+\ diff n t / real (fact n) * x ^ n";
+by (case_tac "n = 0" 1);
+by (Force_tac 1);
+by (case_tac "x = 0" 1);
+by (res_inst_tac [("x","0")] exI 1);
+by (Asm_full_simp_tac 1);
+by (res_inst_tac [("P","0 < n")] impE 1);
+by (assume_tac 2 THEN assume_tac 2);
+by (induct_tac "n" 1);
+by (Simp_tac 1);
+by Auto_tac;
+by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by Auto_tac;
+by (cut_inst_tac [("f","diff 0"),
+ ("diff","diff"),
+ ("h","x"),("n","n")] Maclaurin_objl 2);
+by (Step_tac 2);
+by (blast_tac (claset() addDs
+ [ARITH_PROVE "[|(0::real) <= t;t <= x |] ==> abs t <= abs x"]) 2);
+by (res_inst_tac [("x","t")] exI 2);
+by (force_tac (claset() addIs
+ [ARITH_PROVE "[| 0 < t; (t::real) < x|] ==> abs t <= abs x"],simpset()) 2);
+by (cut_inst_tac [("f","diff 0"),
+ ("diff","diff"),
+ ("h","x"),("n","n")] Maclaurin_minus_objl 1);
+by (Step_tac 1);
+by (blast_tac (claset() addDs
+ [ARITH_PROVE "[|x <= t;t <= (0::real) |] ==> abs t <= abs x"]) 1);
+by (res_inst_tac [("x","t")] exI 1);
+by (force_tac (claset() addIs
+ [ARITH_PROVE "[| x < t; (t::real) < 0|] ==> abs t <= abs x"],simpset()) 1);
+qed "Maclaurin_bi_le";
+
+Goal "[| diff 0 = f; \
+\ ALL m x. DERIV (diff m) x :> diff(Suc m) x; \
+\ x ~= 0; 0 < n \
+\ |] ==> EX t. 0 < abs t & abs t < abs x & \
+\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
+\ (diff n t / real (fact n)) * x ^ n";
+by (res_inst_tac [("R1.0","x"),("R2.0","0")] real_linear_less2 1);
+by (Blast_tac 2);
+by (dtac Maclaurin_minus 1);
+by (dtac Maclaurin 5);
+by (TRYALL(assume_tac));
+by (Blast_tac 1);
+by (Blast_tac 2);
+by (Step_tac 1);
+by (ALLGOALS(res_inst_tac [("x","t")] exI));
+by (Step_tac 1);
+by (ALLGOALS(arith_tac));
+qed "Maclaurin_all_lt";
+
+Goal "diff 0 = f & \
+\ (ALL m x. DERIV (diff m) x :> diff(Suc m) x) & \
+\ x ~= 0 & 0 < n \
+\ --> (EX t. 0 < abs t & abs t < abs x & \
+\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
+\ (diff n t / real (fact n)) * x ^ n)";
+by (blast_tac (claset() addIs [Maclaurin_all_lt]) 1);
+qed "Maclaurin_all_lt_objl";
+
+Goal "x = (0::real) \
+\ ==> 0 < n --> \
+\ sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = \
+\ diff 0 0";
+by (Asm_simp_tac 1);
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "Maclaurin_zero";
+
+Goal "[| diff 0 = f; \
+\ ALL m x. DERIV (diff m) x :> diff (Suc m) x \
+\ |] ==> EX t. abs t <= abs x & \
+\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
+\ (diff n t / real (fact n)) * x ^ n";
+by (cut_inst_tac [("n","n"),("m","0")]
+ (ARITH_PROVE "n <= m | m < (n::nat)") 1);
+by (etac disjE 1);
+by (Force_tac 1);
+by (case_tac "x = 0" 1);
+by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_zero 1);
+by (assume_tac 1);
+by (dtac (gr_implies_not0 RS not0_implies_Suc) 1);
+by (res_inst_tac [("x","0")] exI 1);
+by (Force_tac 1);
+by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_all_lt 1);
+by (TRYALL(assume_tac));
+by (Step_tac 1);
+by (res_inst_tac [("x","t")] exI 1);
+by Auto_tac;
+qed "Maclaurin_all_le";
+
+Goal "diff 0 = f & \
+\ (ALL m x. DERIV (diff m) x :> diff (Suc m) x) \
+\ --> (EX t. abs t <= abs x & \
+\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
+\ (diff n t / real (fact n)) * x ^ n)";
+by (blast_tac (claset() addIs [Maclaurin_all_le]) 1);
+qed "Maclaurin_all_le_objl";
+
+(* ------------------------------------------------------------------------- *)
+(* Version for exp. *)
+(* ------------------------------------------------------------------------- *)
+
+Goal "[| x ~= 0; 0 < n |] \
+\ ==> (EX t. 0 < abs t & \
+\ abs t < abs x & \
+\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \
+\ (exp t / real (fact n)) * x ^ n)";
+by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")]
+ Maclaurin_all_lt_objl 1);
+by Auto_tac;
+qed "Maclaurin_exp_lt";
+
+Goal "EX t. abs t <= abs x & \
+\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \
+\ (exp t / real (fact n)) * x ^ n";
+by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")]
+ Maclaurin_all_le_objl 1);
+by Auto_tac;
+qed "Maclaurin_exp_le";
+
+(* ------------------------------------------------------------------------- *)
+(* Version for sin function *)
+(* ------------------------------------------------------------------------- *)
+
+Goal "[| a < b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \
+\ ==> EX z. a < z & z < b & (f b - f a = (b - a) * f'(z))";
+by (dtac MVT 1);
+by (blast_tac (claset() addIs [DERIV_isCont]) 1);
+by (force_tac (claset() addDs [order_less_imp_le],
+ simpset() addsimps [differentiable_def]) 1);
+by (blast_tac (claset() addDs [DERIV_unique,order_less_imp_le]) 1);
+qed "MVT2";
+
+Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3";
+by (case_tac "d" 1 THEN Auto_tac);
+by (case_tac "nat" 1 THEN Auto_tac);
+by (case_tac "nata" 1 THEN Auto_tac);
+qed "lemma_exhaust_less_4";
+
+bind_thm ("real_mult_le_lemma",
+ simplify (simpset()) (inst "y" "1" real_mult_le_le_mono2));
+
+
+Goal "abs(sin x - \
+\ sumr 0 n (%m. (if even m then 0 \
+\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
+\ x ^ m)) \
+\ <= inverse(real (fact n)) * abs(x) ^ n";
+by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
+ ("diff","%n x. if n mod 4 = 0 then sin(x) \
+\ else if n mod 4 = 1 then cos(x) \
+\ else if n mod 4 = 2 then -sin(x) \
+\ else -cos(x)")] Maclaurin_all_le_objl 1);
+by (Step_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac (mod_Suc_eq_Suc_mod RS ssubst) 1);
+by (cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor
+ RS lemma_exhaust_less_4) 1);
+by (Step_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (rtac DERIV_minus 1 THEN Simp_tac 1);
+by (Asm_simp_tac 1);
+by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_minus 1 THEN rtac DERIV_cos 1);
+by (Simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1);
+by (rtac sumr_fun_eq 1);
+by (Step_tac 1);
+by (rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1);
+by (rtac (even_even_mod_4_iff RS ssubst) 1);
+by (cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor
+ RS lemma_exhaust_less_4) 1);
+by (Step_tac 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2);
+by (asm_simp_tac (simpset() addsimps [even_num_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2);
+by (dtac lemma_even_mod_4_div_2 1);
+by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2,real_divide_def]) 1);
+by (dtac lemma_odd_mod_4_div_2 1);
+by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1);
+by (auto_tac (claset() addSIs [real_mult_le_lemma,real_mult_le_le_mono2],
+ simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs]));
+qed "Maclaurin_sin_bound";
+
+Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "Suc_Suc_mult_two_diff_two";
+Addsimps [Suc_Suc_mult_two_diff_two];
+
+Goal "0 < n --> Suc (Suc (4*n - 2)) = 4*n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "lemma_Suc_Suc_4n_diff_2";
+Addsimps [lemma_Suc_Suc_4n_diff_2];
+
+Goal "0 < n --> Suc (2 * n - 1) = 2*n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "Suc_mult_two_diff_one";
+Addsimps [Suc_mult_two_diff_one];
+
+Goal "EX t. sin x = \
+\ (sumr 0 n (%m. (if even m then 0 \
+\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
+\ x ^ m)) \
+\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
+by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
+ ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
+ Maclaurin_all_lt_objl 1);
+by (Step_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (case_tac "n" 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","0")] spec 1 THEN Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac ccontr 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (res_inst_tac [("x","t")] exI 1);
+by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
+ even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+qed "Maclaurin_sin_expansion";
+
+Goal "EX t. abs t <= abs x & \
+\ sin x = \
+\ (sumr 0 n (%m. (if even m then 0 \
+\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
+\ x ^ m)) \
+\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
+
+by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
+ ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
+ Maclaurin_all_lt_objl 1);
+by (Step_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (case_tac "n" 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac ccontr 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (res_inst_tac [("x","t")] exI 1);
+by (rtac conjI 1);
+by (arith_tac 1);
+by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
+ even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+qed "Maclaurin_sin_expansion2";
+
+Goal "[| 0 < n; 0 < x |] ==> \
+\ EX t. 0 < t & t < x & \
+\ sin x = \
+\ (sumr 0 n (%m. (if even m then 0 \
+\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
+\ x ^ m)) \
+\ + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)";
+by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),
+ ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
+ Maclaurin_objl 1);
+by (Step_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (res_inst_tac [("x","t")] exI 1);
+by (rtac conjI 1 THEN rtac conjI 2);
+by (assume_tac 1 THEN assume_tac 1);
+by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
+ even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+qed "Maclaurin_sin_expansion3";
+
+Goal "0 < x ==> \
+\ EX t. 0 < t & t <= x & \
+\ sin x = \
+\ (sumr 0 n (%m. (if even m then 0 \
+\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
+\ x ^ m)) \
+\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
+by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),
+ ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
+ Maclaurin2_objl 1);
+by (Step_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (res_inst_tac [("x","t")] exI 1);
+by (rtac conjI 1 THEN rtac conjI 2);
+by (assume_tac 1 THEN assume_tac 1);
+by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
+ even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+qed "Maclaurin_sin_expansion4";
+
+(*-----------------------------------------------------------------------------*)
+(* Maclaurin expansion for cos *)
+(*-----------------------------------------------------------------------------*)
+
+Goal "sumr 0 (Suc n) \
+\ (%m. (if even m \
+\ then (- 1) ^ (m div 2)/(real (fact m)) \
+\ else 0) * \
+\ 0 ^ m) = 1";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sumr_cos_zero_one";
+Addsimps [sumr_cos_zero_one];
+
+Goal "EX t. abs t <= abs x & \
+\ cos x = \
+\ (sumr 0 n (%m. (if even m \
+\ then (- 1) ^ (m div 2)/(real (fact m)) \
+\ else 0) * \
+\ x ^ m)) \
+\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
+by (cut_inst_tac [("f","cos"),("n","n"),("x","x"),
+ ("diff","%n x. cos(x + 1/2*real (n)*pi)")]
+ Maclaurin_all_lt_objl 1);
+by (Step_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (case_tac "n" 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [sumr_Suc]) 1);
+by (rtac ccontr 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (res_inst_tac [("x","t")] exI 1);
+by (rtac conjI 1);
+by (arith_tac 1);
+by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
+ even_mult_two_ex,real_add_mult_distrib,cos_add] delsimps
+ [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
+qed "Maclaurin_cos_expansion";
+
+Goal "[| 0 < x; 0 < n |] ==> \
+\ EX t. 0 < t & t < x & \
+\ cos x = \
+\ (sumr 0 n (%m. (if even m \
+\ then (- 1) ^ (m div 2)/(real (fact m)) \
+\ else 0) * \
+\ x ^ m)) \
+\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
+by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),
+ ("diff","%n x. cos(x + 1/2*real (n)*pi)")]
+ Maclaurin_objl 1);
+by (Step_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (res_inst_tac [("x","t")] exI 1);
+by (rtac conjI 1 THEN rtac conjI 2);
+by (assume_tac 1 THEN assume_tac 1);
+by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
+ even_mult_two_ex,real_add_mult_distrib,cos_add] delsimps
+ [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
+qed "Maclaurin_cos_expansion2";
+
+Goal "[| x < 0; 0 < n |] ==> \
+\ EX t. x < t & t < 0 & \
+\ cos x = \
+\ (sumr 0 n (%m. (if even m \
+\ then (- 1) ^ (m div 2)/(real (fact m)) \
+\ else 0) * \
+\ x ^ m)) \
+\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
+by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),
+ ("diff","%n x. cos(x + 1/2*real (n)*pi)")]
+ Maclaurin_minus_objl 1);
+by (Step_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+by (dtac ssubst 1 THEN assume_tac 2);
+by (res_inst_tac [("x","t")] exI 1);
+by (rtac conjI 1 THEN rtac conjI 2);
+by (assume_tac 1 THEN assume_tac 1);
+by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
+by (rtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
+ even_mult_two_ex,real_add_mult_distrib,cos_add] delsimps
+ [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
+qed "Maclaurin_minus_cos_expansion";
+
+(* ------------------------------------------------------------------------- *)
+(* Version for ln(1 +/- x). Where is it?? *)
+(* ------------------------------------------------------------------------- *)
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Poly.ML Fri Nov 16 18:24:11 2001 +0100
@@ -0,0 +1,1208 @@
+(* 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 (claset(),simpset() addsimps [real_minus_mult_eq1 RS sym]));
+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,real_minus_mult_eq2 RS sym,
+ 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,
+ real_minus_mult_eq1 RS sym]) 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_minus_mult_eq1 RS sym] @ 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 (dres_inst_tac [("p","p")] pderiv_zero 2);
+by (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";