even more theories from Jacques
authorpaulson
Fri Nov 16 18:24:11 2001 +0100 (2001-11-16)
changeset 1222402df7cbe7d25
parent 12223 d5e76c2e335c
child 12225 2d5b513199da
even more theories from Jacques
src/HOL/Hyperreal/Hyperreal.thy
src/HOL/Hyperreal/Log.ML
src/HOL/Hyperreal/Log.thy
src/HOL/Hyperreal/MacLaurin.ML
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Poly.ML
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/Series.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Hyperreal/Hyperreal.thy	Fri Nov 16 15:25:17 2001 +0100
     1.2 +++ b/src/HOL/Hyperreal/Hyperreal.thy	Fri Nov 16 18:24:11 2001 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4  
     1.5 -theory Hyperreal = Transcendental:
     1.6 +theory Hyperreal = Poly + MacLaurin:
     1.7  
     1.8  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Hyperreal/Log.ML	Fri Nov 16 18:24:11 2001 +0100
     2.3 @@ -0,0 +1,163 @@
     2.4 +(*  Title       : Log.ML
     2.5 +    Author      : Jacques D. Fleuriot
     2.6 +    Copyright   : 2000,2001 University of Edinburgh
     2.7 +    Description : standard logarithms only 
     2.8 +*)
     2.9 +
    2.10 +
    2.11 +Goalw [powr_def] "1 powr a = 1";
    2.12 +by (Simp_tac 1);
    2.13 +qed "powr_one_eq_one";
    2.14 +Addsimps [powr_one_eq_one];
    2.15 +
    2.16 +Goalw [powr_def] "x powr 0 = 1";
    2.17 +by (Simp_tac 1);
    2.18 +qed "powr_zero_eq_one";
    2.19 +Addsimps [powr_zero_eq_one];
    2.20 +
    2.21 +Goalw [powr_def] 
    2.22 +      "(x powr 1 = x) = (0 < x)";
    2.23 +by (Simp_tac 1);
    2.24 +qed "powr_one_gt_zero_iff";
    2.25 +Addsimps [powr_one_gt_zero_iff];
    2.26 +Addsimps [powr_one_gt_zero_iff RS iffD2];
    2.27 +
    2.28 +Goalw [powr_def] 
    2.29 +      "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)";
    2.30 +by (asm_simp_tac (simpset() addsimps [exp_add RS sym,ln_mult,
    2.31 +    real_add_mult_distrib2]) 1);
    2.32 +qed "powr_mult";
    2.33 +
    2.34 +Goalw [powr_def] "0 < x powr a";
    2.35 +by (Simp_tac 1);
    2.36 +qed "powr_gt_zero";
    2.37 +Addsimps [powr_gt_zero];
    2.38 +
    2.39 +Goalw [powr_def] "x powr a ~= 0";
    2.40 +by (Simp_tac 1);
    2.41 +qed "powr_not_zero";
    2.42 +Addsimps [powr_not_zero];
    2.43 +
    2.44 +Goal "[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)";
    2.45 +by (asm_simp_tac (simpset() addsimps [real_divide_def,real_inverse_gt_0,
    2.46 +    powr_mult]) 1);
    2.47 +by (asm_simp_tac (simpset() addsimps [powr_def,exp_minus RS sym,
    2.48 +    exp_add RS sym,ln_inverse]) 1);
    2.49 +qed "powr_divide";
    2.50 +
    2.51 +Goalw [powr_def] "x powr (a + b) = (x powr a) * (x powr b)";
    2.52 +by (asm_simp_tac (simpset() addsimps [exp_add RS sym,
    2.53 +    real_add_mult_distrib]) 1);
    2.54 +qed "powr_add";
    2.55 +
    2.56 +Goalw [powr_def] "(x powr a) powr b = x powr (a * b)";
    2.57 +by (simp_tac (simpset() addsimps real_mult_ac) 1);
    2.58 +qed "powr_powr";
    2.59 +
    2.60 +Goal "(x powr a) powr b = (x powr b) powr a";
    2.61 +by (simp_tac (simpset() addsimps [powr_powr,real_mult_commute]) 1);
    2.62 +qed "powr_powr_swap";
    2.63 +
    2.64 +Goalw [powr_def] "x powr (-a) = inverse (x powr a)";
    2.65 +by (simp_tac (simpset() addsimps [exp_minus RS sym]) 1);
    2.66 +qed "powr_minus";
    2.67 +
    2.68 +Goalw [real_divide_def] "x powr (-a) = 1/(x powr a)";
    2.69 +by (simp_tac (simpset() addsimps [powr_minus]) 1);
    2.70 +qed "powr_minus_divide";
    2.71 +
    2.72 +Goalw [powr_def] 
    2.73 +   "[| a < b; 1 < x |] ==> x powr a < x powr b";
    2.74 +by Auto_tac;
    2.75 +qed "powr_less_mono";
    2.76 +
    2.77 +Goalw [powr_def] 
    2.78 +   "[| x powr a < x powr b; 1 < x |] ==> a < b";
    2.79 +by (auto_tac (claset() addDs [ln_gt_zero],
    2.80 +    simpset() addsimps [rename_numerals real_mult_less_cancel2]));
    2.81 +qed "powr_less_cancel";
    2.82 +
    2.83 +Goal "1 < x ==> (x powr a < x powr b) = (a < b)";
    2.84 +by (blast_tac (claset() addIs [powr_less_cancel,powr_less_mono]) 1);
    2.85 +qed "powr_less_cancel_iff";
    2.86 +Addsimps [powr_less_cancel_iff];
    2.87 +
    2.88 +Goalw [real_le_def] "1 < x ==> (x powr a <= x powr b) = (a <= b)";
    2.89 +by (Auto_tac);
    2.90 +qed "powr_le_cancel_iff";
    2.91 +Addsimps [powr_le_cancel_iff];
    2.92 +
    2.93 +Goalw [log_def] "ln x = log (exp(1)) x";
    2.94 +by (Simp_tac 1);
    2.95 +qed "log_ln";
    2.96 +
    2.97 +Goalw [powr_def,log_def] 
    2.98 +    "[| 0 < a; a ~= 1; 0 < x |] ==> a powr (log a x) = x";
    2.99 +by Auto_tac;
   2.100 +qed "powr_log_cancel";
   2.101 +Addsimps [powr_log_cancel];
   2.102 +
   2.103 +Goalw [log_def,powr_def] 
   2.104 +    "[| 0 < a; a ~= 1 |] ==> log a (a powr y) = y";
   2.105 +by (auto_tac (claset(),simpset() addsimps [real_divide_def,
   2.106 +    real_mult_assoc]));
   2.107 +qed "log_powr_cancel";
   2.108 +Addsimps [log_powr_cancel];
   2.109 +
   2.110 +Goalw [log_def] 
   2.111 +     "[| 0 < a; a ~= 1; 0 < x; 0 < y  |] \
   2.112 +\     ==> log a (x * y) = log a x + log a y";
   2.113 +by (auto_tac (claset(),simpset() addsimps [ln_mult,real_divide_def,
   2.114 +    real_add_mult_distrib]));
   2.115 +qed "log_mult";
   2.116 +
   2.117 +Goalw [log_def,real_divide_def]
   2.118 +     "[| 0 < a; a ~= 1; 0 < b; b ~= 1; 0 < x |] \
   2.119 +\     ==> log a x = (ln b/ln a) * log b x";
   2.120 +by Auto_tac;
   2.121 +qed "log_eq_div_ln_mult_log";
   2.122 +
   2.123 +(* specific case *)
   2.124 +Goal "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x";
   2.125 +by (auto_tac (claset(),simpset() addsimps [log_def]));
   2.126 +qed "log_base_10_eq1";
   2.127 +
   2.128 +Goal "0 < x ==> log 10 x = (log 10 (exp 1)) * ln x";
   2.129 +by (auto_tac (claset(),simpset() addsimps [log_def]));
   2.130 +qed "log_base_10_eq2";
   2.131 +
   2.132 +Goalw [log_def] "log a 1 = 0";
   2.133 +by Auto_tac;
   2.134 +qed "log_one";
   2.135 +Addsimps [log_one];
   2.136 +
   2.137 +Goalw [log_def] 
   2.138 +    "[| 0 < a; a ~= 1 |] ==> log a a = 1";
   2.139 +by Auto_tac;
   2.140 +qed "log_eq_one";
   2.141 +Addsimps [log_eq_one];
   2.142 +
   2.143 +Goal "[| 0 < a; a ~= 1; 0 < x |] ==> log a (inverse x) = - log a x";
   2.144 +by (res_inst_tac [("x1","log a x")] (real_add_left_cancel RS iffD1) 1);
   2.145 +by (auto_tac (claset(),simpset() addsimps [log_mult RS sym]));
   2.146 +qed "log_inverse";
   2.147 +
   2.148 +Goal "[|0 < a; a ~= 1; 0 < x; 0 < y|] \
   2.149 +\     ==> log a (x/y) = log a x - log a y";
   2.150 +by (auto_tac (claset(),simpset() addsimps [log_mult,real_divide_def,
   2.151 +    log_inverse]));
   2.152 +qed "log_divide";
   2.153 +
   2.154 +Goal "[| 1 < a; 0 < x; 0 < y |] ==> (log a x < log a y) = (x < y)";
   2.155 +by (Step_tac 1);
   2.156 +by (rtac powr_less_cancel 2);
   2.157 +by (dres_inst_tac [("a","log a x")] powr_less_mono 1);
   2.158 +by Auto_tac;
   2.159 +qed "log_less_cancel_iff";
   2.160 +Addsimps [log_less_cancel_iff];
   2.161 +
   2.162 +Goal "[| 1 < a; 0 < x; 0 < y |] ==> (log a x <= log a y) = (x <= y)";
   2.163 +by (auto_tac (claset(),simpset() addsimps [real_le_def]));
   2.164 +qed "log_le_cancel_iff";
   2.165 +Addsimps [log_le_cancel_iff];
   2.166 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Hyperreal/Log.thy	Fri Nov 16 18:24:11 2001 +0100
     3.3 @@ -0,0 +1,19 @@
     3.4 +(*  Title       : Log.thy
     3.5 +    Author      : Jacques D. Fleuriot
     3.6 +    Copyright   : 2000,2001 University of Edinburgh
     3.7 +    Description : standard logarithms only 
     3.8 +*)
     3.9 +
    3.10 +Log = Transcendental +
    3.11 +
    3.12 +constdefs
    3.13 +
    3.14 +    (* power function with exponent a *)
    3.15 +    powr  :: [real,real] => real     (infixr 80)
    3.16 +    "x powr a == exp(a * ln x)"
    3.17 +
    3.18 +    (* logarithm of x to base a *)
    3.19 +    log :: [real,real] => real
    3.20 +    "log a x == ln x / ln a"
    3.21 +
    3.22 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Hyperreal/MacLaurin.ML	Fri Nov 16 18:24:11 2001 +0100
     4.3 @@ -0,0 +1,726 @@
     4.4 +(*  Title       : MacLaurin.thy
     4.5 +    Author      : Jacques D. Fleuriot
     4.6 +    Copyright   : 2001 University of Edinburgh
     4.7 +    Description : MacLaurin series
     4.8 +*)
     4.9 +
    4.10 +Goal "sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";
    4.11 +by (induct_tac "n" 1);
    4.12 +by Auto_tac;
    4.13 +qed "sumr_offset";
    4.14 +
    4.15 +Goal "ALL f. sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";
    4.16 +by (induct_tac "n" 1);
    4.17 +by Auto_tac;
    4.18 +qed "sumr_offset2";
    4.19 +
    4.20 +Goal "sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";
    4.21 +by (simp_tac (simpset() addsimps [sumr_offset]) 1);
    4.22 +qed "sumr_offset3";
    4.23 +
    4.24 +Goal "ALL n f. sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";
    4.25 +by (simp_tac (simpset() addsimps [sumr_offset]) 1);
    4.26 +qed "sumr_offset4";
    4.27 +
    4.28 +Goal "0 < n ==> \
    4.29 +\     sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else \
    4.30 +\            ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = \
    4.31 +\     sumr 0 (Suc n) (%n. (if even(n) then 0 else \
    4.32 +\            ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)";
    4.33 +by (res_inst_tac [("n1","1")] (sumr_split_add RS subst) 1);
    4.34 +by Auto_tac;
    4.35 +qed "sumr_from_1_from_0";
    4.36 +
    4.37 +(*---------------------------------------------------------------------------*)
    4.38 +(* Maclaurin's theorem with Lagrange form of remainder                       *)
    4.39 +(*---------------------------------------------------------------------------*)
    4.40 +
    4.41 +(* Annoying: Proof is now even longer due mostly to 
    4.42 +   change in behaviour of simplifier  since Isabelle99 *)
    4.43 +Goal " [| 0 < h; 0 < n; diff 0 = f; \
    4.44 +\      ALL m t. \
    4.45 +\         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \
    4.46 +\   ==> EX t. 0 < t & \
    4.47 +\             t < h & \
    4.48 +\             f h = \
    4.49 +\             sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + \
    4.50 +\             (diff n t / real (fact n)) * h ^ n";
    4.51 +by (case_tac "n = 0" 1);
    4.52 +by (Force_tac 1);
    4.53 +by (dtac not0_implies_Suc 1);
    4.54 +by (etac exE 1);
    4.55 +by (subgoal_tac 
    4.56 +     "EX B. f h = sumr 0 n (%m. (diff m 0 / real (fact m)) * (h ^ m)) \
    4.57 +\                  + (B * ((h ^ n) / real (fact n)))" 1);
    4.58 +
    4.59 +by (simp_tac (HOL_ss addsimps [real_add_commute, real_divide_def,
    4.60 +    ARITH_PROVE "(x = z + (y::real)) = (x - y = z)"]) 2);
    4.61 +by (res_inst_tac 
    4.62 +  [("x","(f(h) - sumr 0 n (%m. (diff(m)(0) / real (fact m)) * (h ^ m))) \
    4.63 +\        * real (fact n) / (h ^ n)")] exI 2);
    4.64 +by (simp_tac (HOL_ss addsimps [real_mult_assoc,real_divide_def]) 2);
    4.65 + by (rtac (CLAIM "x = (1::real) ==>  a = a * (x::real)") 2);
    4.66 +by (asm_simp_tac (HOL_ss addsimps 
    4.67 +    [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"]
    4.68 +     delsimps [realpow_Suc]) 2);
    4.69 +by (rtac (real_mult_inv_left RS ssubst) 2);
    4.70 +by (rtac (real_mult_inv_left RS ssubst) 3);
    4.71 +by (dtac (realpow_gt_zero RS real_not_refl2 RS not_sym) 2);
    4.72 +by (assume_tac 2);
    4.73 +by (rtac real_of_nat_fact_not_zero 2);
    4.74 +by (Simp_tac 2);
    4.75 +by (etac exE 1);
    4.76 +by (cut_inst_tac [("b","%t. f t - \
    4.77 +\      (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \
    4.78 +\                       (B * ((t ^ n) / real (fact n))))")] 
    4.79 +    (CLAIM "EX g. g = b") 1);
    4.80 +by (etac exE 1);
    4.81 +by (subgoal_tac "g 0 = 0 & g h =0" 1);
    4.82 +by (asm_simp_tac (simpset() addsimps 
    4.83 +    [ARITH_PROVE "(x - y = z) = (x = z + (y::real))"]
    4.84 +    delsimps [sumr_Suc]) 2);
    4.85 +by (cut_inst_tac [("n","m"),("k","1")] sumr_offset2 2);
    4.86 +by (asm_full_simp_tac (simpset() addsimps 
    4.87 +    [ARITH_PROVE "(x = y - z) = (y = x + (z::real))"]
    4.88 +    delsimps [sumr_Suc]) 2);
    4.89 +by (cut_inst_tac [("b","%m t. diff m t - \
    4.90 +\      (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) \
    4.91 +\       + (B * ((t ^ (n - m)) / real (fact(n - m)))))")] 
    4.92 +    (CLAIM "EX difg. difg = b") 1);
    4.93 +by (etac exE 1);
    4.94 +by (subgoal_tac "difg 0 = g" 1);
    4.95 +by (asm_simp_tac (simpset() delsimps [realpow_Suc,fact_Suc]) 2);
    4.96 +by (subgoal_tac "ALL m t. m < n & 0 <= t & t <= h --> \
    4.97 +\                   DERIV (difg m) t :> difg (Suc m) t" 1);
    4.98 +by (Clarify_tac 2);
    4.99 +by (rtac DERIV_diff 2);
   4.100 +by (Asm_simp_tac 2);
   4.101 +by DERIV_tac;
   4.102 +by DERIV_tac;
   4.103 +by (rtac lemma_DERIV_subst 3);
   4.104 +by (rtac DERIV_quotient 3);
   4.105 +by (rtac DERIV_const 4);
   4.106 +by (rtac DERIV_pow 3);
   4.107 +by (asm_simp_tac (simpset() addsimps [real_inverse_distrib,
   4.108 +    CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e" 
   4.109 +    real_mult_ac,fact_diff_Suc]) 4);
   4.110 +by (Asm_simp_tac 3);
   4.111 +by (forw_inst_tac [("m","ma")] less_add_one 2);
   4.112 +by (Clarify_tac 2);
   4.113 +by (asm_simp_tac (simpset() addsimps 
   4.114 +    [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"]
   4.115 +    delsimps [sumr_Suc]) 2);
   4.116 +by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) 
   4.117 +          (read_instantiate [("k","1")] sumr_offset4))] 
   4.118 +    delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
   4.119 +by (rtac lemma_DERIV_subst 2);
   4.120 +by (rtac DERIV_add 2);
   4.121 +by (rtac DERIV_const 3);
   4.122 +by (rtac DERIV_sumr 2);
   4.123 +by (Clarify_tac 2);
   4.124 +by (Simp_tac 3);
   4.125 +by (simp_tac (simpset() addsimps [real_divide_def,real_mult_assoc] 
   4.126 +    delsimps [fact_Suc,realpow_Suc]) 2);
   4.127 +by (rtac DERIV_cmult 2);
   4.128 +by (rtac lemma_DERIV_subst 2);
   4.129 +by DERIV_tac;
   4.130 +by (rtac (fact_Suc RS ssubst) 2);
   4.131 +by (rtac (real_of_nat_mult RS ssubst) 2);
   4.132 +by (simp_tac (simpset() addsimps [real_inverse_distrib] @
   4.133 +    real_mult_ac) 2);
   4.134 +by (subgoal_tac "ALL ma. ma < n --> \
   4.135 +\        (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1);
   4.136 +by (rotate_tac 11 1);
   4.137 +by (dres_inst_tac [("x","m")] spec 1);
   4.138 +by (etac impE 1);
   4.139 +by (Asm_simp_tac 1);
   4.140 +by (etac exE 1);
   4.141 +by (res_inst_tac [("x","t")] exI 1);
   4.142 +by (asm_full_simp_tac (simpset() addsimps 
   4.143 +     [ARITH_PROVE "(x - y = 0) = (y = (x::real))"] 
   4.144 +      delsimps [realpow_Suc,fact_Suc]) 1);
   4.145 +by (subgoal_tac "ALL m. m < n --> difg m 0 = 0" 1);
   4.146 +by (Clarify_tac 2);
   4.147 +by (Asm_simp_tac 2);
   4.148 +by (forw_inst_tac [("m","ma")] less_add_one 2);
   4.149 +by (Clarify_tac 2);
   4.150 +by (asm_simp_tac (simpset() delsimps [sumr_Suc]) 2);
   4.151 +by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) 
   4.152 +          (read_instantiate [("k","1")] sumr_offset4))] 
   4.153 +    delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
   4.154 +by (subgoal_tac "ALL m. m < n --> (EX t. 0 < t & t < h & \
   4.155 +\                DERIV (difg m) t :> 0)" 1);
   4.156 +by (rtac allI 1 THEN rtac impI 1);
   4.157 +by (rotate_tac 12 1);
   4.158 +by (dres_inst_tac [("x","ma")] spec 1);
   4.159 +by (etac impE 1 THEN assume_tac 1);
   4.160 +by (etac exE 1);
   4.161 +by (res_inst_tac [("x","t")] exI 1);
   4.162 +(* do some tidying up *)
   4.163 +by (ALLGOALS(thin_tac "difg = \
   4.164 +\          (%m t. diff m t - \
   4.165 +\                 (sumr 0 (n - m) \
   4.166 +\                   (%p. diff (m + p) 0 / real (fact p) * t ^ p) + \
   4.167 +\                  B * (t ^ (n - m) / real (fact (n - m)))))"));
   4.168 +by (ALLGOALS(thin_tac "g = \
   4.169 +\          (%t. f t - \
   4.170 +\               (sumr 0 n (%m. diff m 0 / real  (fact m) * t ^ m) + \
   4.171 +\                B * (t ^ n / real (fact n))))"));
   4.172 +by (ALLGOALS(thin_tac "f h = \
   4.173 +\          sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
   4.174 +\          B * (h ^ n / real (fact n))"));
   4.175 +(* back to business *)
   4.176 +by (Asm_simp_tac 1);
   4.177 +by (rtac DERIV_unique 1);
   4.178 +by (Blast_tac 2);
   4.179 +by (Force_tac 1);
   4.180 +by (rtac allI 1 THEN induct_tac "ma" 1);
   4.181 +by (rtac impI 1 THEN rtac Rolle 1);
   4.182 +by (assume_tac 1);
   4.183 +by (Asm_full_simp_tac 1);
   4.184 +by (Asm_full_simp_tac 1);
   4.185 +by (subgoal_tac "ALL t. 0 <= t & t <= h --> g differentiable t" 1);
   4.186 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
   4.187 +by (blast_tac (claset() addDs [DERIV_isCont]) 1);
   4.188 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
   4.189 +by (Clarify_tac 1);
   4.190 +by (res_inst_tac [("x","difg (Suc 0) t")] exI 1);
   4.191 +by (Force_tac 1);
   4.192 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
   4.193 +by (Clarify_tac 1);
   4.194 +by (res_inst_tac [("x","difg (Suc 0) x")] exI 1);
   4.195 +by (Force_tac 1);
   4.196 +by (Step_tac 1);
   4.197 +by (Force_tac 1);
   4.198 +by (subgoal_tac "EX ta. 0 < ta & ta < t & \
   4.199 +\                DERIV difg (Suc n) ta :> 0" 1);
   4.200 +by (rtac Rolle 2 THEN assume_tac 2);
   4.201 +by (Asm_full_simp_tac 2);
   4.202 +by (rotate_tac 2 2);
   4.203 +by (dres_inst_tac [("x","n")] spec 2);
   4.204 +by (ftac (ARITH_PROVE "n < m  ==> n < Suc m") 2);
   4.205 +by (rtac DERIV_unique 2);
   4.206 +by (assume_tac 3);
   4.207 +by (Force_tac 2);
   4.208 +by (subgoal_tac 
   4.209 +    "ALL ta. 0 <= ta & ta <= t --> (difg (Suc n)) differentiable ta" 2);
   4.210 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
   4.211 +by (blast_tac (claset() addSDs [DERIV_isCont]) 2);
   4.212 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
   4.213 +by (Clarify_tac 2);
   4.214 +by (res_inst_tac [("x","difg (Suc (Suc n)) ta")] exI 2);
   4.215 +by (Force_tac 2);
   4.216 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
   4.217 +by (Clarify_tac 2);
   4.218 +by (res_inst_tac [("x","difg (Suc (Suc n)) x")] exI 2);
   4.219 +by (Force_tac 2);
   4.220 +by (Step_tac 1);
   4.221 +by (res_inst_tac [("x","ta")] exI 1);
   4.222 +by (Force_tac 1);
   4.223 +qed "Maclaurin";
   4.224 +
   4.225 +Goal "0 < h & 0 < n & diff 0 = f & \
   4.226 +\      (ALL m t. \
   4.227 +\         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \
   4.228 +\   --> (EX t. 0 < t & \
   4.229 +\             t < h & \
   4.230 +\             f h = \
   4.231 +\             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
   4.232 +\             diff n t / real (fact n) * h ^ n)";
   4.233 +by (blast_tac (claset() addIs [Maclaurin]) 1);
   4.234 +qed "Maclaurin_objl";
   4.235 +
   4.236 +Goal " [| 0 < h; diff 0 = f; \
   4.237 +\      ALL m t. \
   4.238 +\         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \
   4.239 +\   ==> EX t. 0 < t & \
   4.240 +\             t <= h & \
   4.241 +\             f h = \
   4.242 +\             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
   4.243 +\             diff n t / real (fact n) * h ^ n";
   4.244 +by (case_tac "n" 1);
   4.245 +by Auto_tac;
   4.246 +by (dtac Maclaurin 1 THEN Auto_tac);
   4.247 +qed "Maclaurin2";
   4.248 +
   4.249 +Goal "0 < h & diff 0 = f & \
   4.250 +\      (ALL m t. \
   4.251 +\         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \
   4.252 +\   --> (EX t. 0 < t & \
   4.253 +\             t <= h & \
   4.254 +\             f h = \
   4.255 +\             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
   4.256 +\             diff n t / real (fact n) * h ^ n)";
   4.257 +by (blast_tac (claset() addIs [Maclaurin2]) 1);
   4.258 +qed "Maclaurin2_objl";
   4.259 +
   4.260 +Goal " [| h < 0; 0 < n; diff 0 = f; \
   4.261 +\      ALL m t. \
   4.262 +\         m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t |] \
   4.263 +\   ==> EX t. h < t & \
   4.264 +\             t < 0 & \
   4.265 +\             f h = \
   4.266 +\             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
   4.267 +\             diff n t / real (fact n) * h ^ n";
   4.268 +by (cut_inst_tac [("f","%x. f (-x)"),
   4.269 +                 ("diff","%n x. ((- 1) ^ n) * diff n (-x)"),
   4.270 +                 ("h","-h"),("n","n")] Maclaurin_objl 1);
   4.271 +by (Asm_full_simp_tac 1);
   4.272 +by (etac impE 1 THEN Step_tac 1);
   4.273 +by (rtac (real_minus_mult_eq2 RS ssubst) 1);
   4.274 +by (rtac DERIV_cmult 1);
   4.275 +by (rtac lemma_DERIV_subst 1);
   4.276 +by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1);
   4.277 +by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2);
   4.278 +by (Force_tac 2);
   4.279 +by (Force_tac 1);
   4.280 +by (res_inst_tac [("x","-t")] exI 1);
   4.281 +by Auto_tac;
   4.282 +by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1);
   4.283 +by (rtac sumr_fun_eq 1);
   4.284 +by (Asm_full_simp_tac 1);
   4.285 +by (auto_tac (claset(),simpset() addsimps [real_divide_def,
   4.286 +    CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))",
   4.287 +    realpow_mult RS sym]));
   4.288 +qed "Maclaurin_minus";
   4.289 +
   4.290 +Goal "(h < 0 & 0 < n & diff 0 = f & \
   4.291 +\      (ALL m t. \
   4.292 +\         m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\
   4.293 +\   --> (EX t. h < t & \
   4.294 +\             t < 0 & \
   4.295 +\             f h = \
   4.296 +\             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
   4.297 +\             diff n t / real (fact n) * h ^ n)";
   4.298 +by (blast_tac (claset() addIs [Maclaurin_minus]) 1);
   4.299 +qed "Maclaurin_minus_objl";
   4.300 +
   4.301 +(* ------------------------------------------------------------------------- *)
   4.302 +(* More convenient "bidirectional" version.                                  *)
   4.303 +(* ------------------------------------------------------------------------- *)
   4.304 +
   4.305 +(* not good for PVS sin_approx, cos_approx *)
   4.306 +Goal " [| diff 0 = f; \
   4.307 +\      ALL m t. \
   4.308 +\         m < n & abs t <= abs x --> DERIV (diff m) t :> diff (Suc m) t |] \
   4.309 +\   ==> EX t. abs t <= abs x & \
   4.310 +\             f x = \
   4.311 +\             sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + \
   4.312 +\             diff n t / real (fact n) * x ^ n";
   4.313 +by (case_tac "n = 0" 1);
   4.314 +by (Force_tac 1);
   4.315 +by (case_tac "x = 0" 1);
   4.316 +by (res_inst_tac [("x","0")] exI 1);
   4.317 +by (Asm_full_simp_tac 1);
   4.318 +by (res_inst_tac [("P","0 < n")] impE 1);
   4.319 +by (assume_tac 2 THEN assume_tac 2);
   4.320 +by (induct_tac "n" 1);
   4.321 +by (Simp_tac 1);
   4.322 +by Auto_tac;
   4.323 +by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
   4.324 +by Auto_tac;
   4.325 +by (cut_inst_tac [("f","diff 0"),
   4.326 +                 ("diff","diff"),
   4.327 +                 ("h","x"),("n","n")] Maclaurin_objl 2);
   4.328 +by (Step_tac 2);
   4.329 +by (blast_tac (claset() addDs 
   4.330 +    [ARITH_PROVE "[|(0::real) <= t;t <= x |] ==> abs t <= abs x"]) 2);
   4.331 +by (res_inst_tac [("x","t")] exI 2);
   4.332 +by (force_tac (claset() addIs 
   4.333 +    [ARITH_PROVE "[| 0 < t; (t::real) < x|] ==> abs t <= abs x"],simpset()) 2);
   4.334 +by (cut_inst_tac [("f","diff 0"),
   4.335 +                 ("diff","diff"),
   4.336 +                 ("h","x"),("n","n")] Maclaurin_minus_objl 1);
   4.337 +by (Step_tac 1);
   4.338 +by (blast_tac (claset() addDs 
   4.339 +    [ARITH_PROVE "[|x <= t;t <= (0::real) |] ==> abs t <= abs x"]) 1);
   4.340 +by (res_inst_tac [("x","t")] exI 1);
   4.341 +by (force_tac (claset() addIs 
   4.342 +    [ARITH_PROVE "[| x < t; (t::real) < 0|] ==> abs t <= abs x"],simpset()) 1);
   4.343 +qed "Maclaurin_bi_le";
   4.344 +
   4.345 +Goal "[| diff 0 = f; \
   4.346 +\        ALL m x. DERIV (diff m) x :> diff(Suc m) x; \ 
   4.347 +\       x ~= 0; 0 < n \
   4.348 +\     |] ==> EX t. 0 < abs t & abs t < abs x & \
   4.349 +\              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
   4.350 +\                    (diff n t / real (fact n)) * x ^ n";
   4.351 +by (res_inst_tac [("R1.0","x"),("R2.0","0")] real_linear_less2 1);
   4.352 +by (Blast_tac 2);
   4.353 +by (dtac Maclaurin_minus 1);
   4.354 +by (dtac Maclaurin 5);
   4.355 +by (TRYALL(assume_tac));
   4.356 +by (Blast_tac 1);
   4.357 +by (Blast_tac 2);
   4.358 +by (Step_tac 1);
   4.359 +by (ALLGOALS(res_inst_tac [("x","t")] exI));
   4.360 +by (Step_tac 1);
   4.361 +by (ALLGOALS(arith_tac));
   4.362 +qed "Maclaurin_all_lt";
   4.363 +
   4.364 +Goal "diff 0 = f & \
   4.365 +\     (ALL m x. DERIV (diff m) x :> diff(Suc m) x) & \
   4.366 +\     x ~= 0 & 0 < n \
   4.367 +\     --> (EX t. 0 < abs t & abs t < abs x & \
   4.368 +\              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
   4.369 +\                    (diff n t / real (fact n)) * x ^ n)";
   4.370 +by (blast_tac (claset() addIs [Maclaurin_all_lt]) 1);
   4.371 +qed "Maclaurin_all_lt_objl";
   4.372 +
   4.373 +Goal "x = (0::real)  \
   4.374 +\     ==> 0 < n --> \
   4.375 +\         sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = \
   4.376 +\         diff 0 0";
   4.377 +by (Asm_simp_tac 1);
   4.378 +by (induct_tac "n" 1);
   4.379 +by Auto_tac; 
   4.380 +qed_spec_mp "Maclaurin_zero";
   4.381 +
   4.382 +Goal "[| diff 0 = f; \
   4.383 +\       ALL m x. DERIV (diff m) x :> diff (Suc m) x \
   4.384 +\     |] ==> EX t. abs t <= abs x & \
   4.385 +\             f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
   4.386 +\                   (diff n t / real (fact n)) * x ^ n";
   4.387 +by (cut_inst_tac [("n","n"),("m","0")] 
   4.388 +       (ARITH_PROVE "n <= m | m < (n::nat)") 1);
   4.389 +by (etac disjE 1);
   4.390 +by (Force_tac 1);
   4.391 +by (case_tac "x = 0" 1);
   4.392 +by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_zero 1);
   4.393 +by (assume_tac 1);
   4.394 +by (dtac (gr_implies_not0 RS  not0_implies_Suc) 1);
   4.395 +by (res_inst_tac [("x","0")] exI 1);
   4.396 +by (Force_tac 1);
   4.397 +by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_all_lt 1);
   4.398 +by (TRYALL(assume_tac));
   4.399 +by (Step_tac 1);
   4.400 +by (res_inst_tac [("x","t")] exI 1);
   4.401 +by Auto_tac;
   4.402 +qed "Maclaurin_all_le";
   4.403 +
   4.404 +Goal "diff 0 = f & \
   4.405 +\     (ALL m x. DERIV (diff m) x :> diff (Suc m) x)  \
   4.406 +\     --> (EX t. abs t <= abs x & \
   4.407 +\             f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
   4.408 +\                   (diff n t / real (fact n)) * x ^ n)";
   4.409 +by (blast_tac (claset() addIs [Maclaurin_all_le]) 1);
   4.410 +qed "Maclaurin_all_le_objl";
   4.411 +
   4.412 +(* ------------------------------------------------------------------------- *)
   4.413 +(* Version for exp.                                                          *)
   4.414 +(* ------------------------------------------------------------------------- *)
   4.415 +
   4.416 +Goal "[| x ~= 0; 0 < n |] \
   4.417 +\     ==> (EX t. 0 < abs t & \
   4.418 +\               abs t < abs x & \
   4.419 +\               exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \
   4.420 +\                       (exp t / real (fact n)) * x ^ n)";
   4.421 +by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] 
   4.422 +    Maclaurin_all_lt_objl 1);
   4.423 +by Auto_tac;
   4.424 +qed "Maclaurin_exp_lt";
   4.425 +
   4.426 +Goal "EX t. abs t <= abs x & \
   4.427 +\           exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \
   4.428 +\                      (exp t / real (fact n)) * x ^ n";
   4.429 +by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] 
   4.430 +    Maclaurin_all_le_objl 1);
   4.431 +by Auto_tac;
   4.432 +qed "Maclaurin_exp_le";
   4.433 +
   4.434 +(* ------------------------------------------------------------------------- *)
   4.435 +(* Version for sin function                                                  *)
   4.436 +(* ------------------------------------------------------------------------- *)
   4.437 +
   4.438 +Goal "[| a < b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \
   4.439 +\     ==> EX z. a < z & z < b & (f b - f a = (b - a) * f'(z))";
   4.440 +by (dtac MVT 1);
   4.441 +by (blast_tac (claset() addIs [DERIV_isCont]) 1);
   4.442 +by (force_tac (claset() addDs [order_less_imp_le],
   4.443 +    simpset() addsimps [differentiable_def]) 1);
   4.444 +by (blast_tac (claset() addDs [DERIV_unique,order_less_imp_le]) 1);
   4.445 +qed "MVT2";
   4.446 +
   4.447 +Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3";
   4.448 +by (case_tac "d" 1 THEN Auto_tac);
   4.449 +by (case_tac "nat" 1 THEN Auto_tac);
   4.450 +by (case_tac "nata" 1 THEN Auto_tac);
   4.451 +qed "lemma_exhaust_less_4";
   4.452 +
   4.453 +bind_thm ("real_mult_le_lemma",
   4.454 +          simplify (simpset()) (inst "y" "1" real_mult_le_le_mono2));
   4.455 +
   4.456 +
   4.457 +Goal "abs(sin x - \
   4.458 +\          sumr 0 n (%m. (if even m then 0 \
   4.459 +\                         else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
   4.460 +\                         x ^ m)) \
   4.461 +\      <= inverse(real (fact n)) * abs(x) ^ n";
   4.462 +by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
   4.463 +       ("diff","%n x. if n mod 4 = 0 then sin(x) \
   4.464 +\                     else if n mod 4 = 1 then cos(x) \
   4.465 +\                     else if n mod 4 = 2 then -sin(x) \
   4.466 +\                     else -cos(x)")] Maclaurin_all_le_objl 1);
   4.467 +by (Step_tac 1);
   4.468 +by (Asm_full_simp_tac 1);
   4.469 +by (rtac (mod_Suc_eq_Suc_mod RS ssubst) 1);
   4.470 +by (cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor
   4.471 +    RS lemma_exhaust_less_4) 1);
   4.472 +by (Step_tac 1);
   4.473 +by (Asm_simp_tac 1);
   4.474 +by (Asm_simp_tac 1);
   4.475 +by (Asm_simp_tac 1);
   4.476 +by (rtac DERIV_minus 1 THEN Simp_tac 1);
   4.477 +by (Asm_simp_tac 1);
   4.478 +by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_minus 1 THEN rtac DERIV_cos 1);
   4.479 +by (Simp_tac 1);
   4.480 +by (dtac ssubst 1 THEN assume_tac 2);
   4.481 +by (rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1);
   4.482 +by (rtac sumr_fun_eq 1);
   4.483 +by (Step_tac 1);
   4.484 +by (rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1);
   4.485 +by (rtac (even_even_mod_4_iff RS ssubst) 1);
   4.486 +by (cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor
   4.487 +    RS lemma_exhaust_less_4) 1);
   4.488 +by (Step_tac 1);
   4.489 +by (Asm_simp_tac 1);
   4.490 +by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2);
   4.491 +by (asm_simp_tac (simpset() addsimps [even_num_iff]) 1);
   4.492 +by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2);
   4.493 +by (dtac lemma_even_mod_4_div_2 1);
   4.494 +by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2,real_divide_def]) 1);
   4.495 +by (dtac lemma_odd_mod_4_div_2 1);
   4.496 +by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1);
   4.497 +by (auto_tac (claset() addSIs [real_mult_le_lemma,real_mult_le_le_mono2],
   4.498 +      simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs]));
   4.499 +qed "Maclaurin_sin_bound";
   4.500 +
   4.501 +Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n";
   4.502 +by (induct_tac "n" 1);
   4.503 +by Auto_tac;
   4.504 +qed_spec_mp "Suc_Suc_mult_two_diff_two";
   4.505 +Addsimps [Suc_Suc_mult_two_diff_two];
   4.506 +
   4.507 +Goal "0 < n --> Suc (Suc (4*n - 2)) = 4*n";
   4.508 +by (induct_tac "n" 1);
   4.509 +by Auto_tac;
   4.510 +qed_spec_mp "lemma_Suc_Suc_4n_diff_2";
   4.511 +Addsimps [lemma_Suc_Suc_4n_diff_2];
   4.512 +
   4.513 +Goal "0 < n --> Suc (2 * n - 1) = 2*n";
   4.514 +by (induct_tac "n" 1);
   4.515 +by Auto_tac;
   4.516 +qed_spec_mp "Suc_mult_two_diff_one";
   4.517 +Addsimps [Suc_mult_two_diff_one];
   4.518 +
   4.519 +Goal "EX t. sin x = \
   4.520 +\      (sumr 0 n (%m. (if even m then 0 \
   4.521 +\                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
   4.522 +\                      x ^ m)) \
   4.523 +\     + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
   4.524 +by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
   4.525 +       ("diff","%n x. sin(x + 1/2*real (n)*pi)")] 
   4.526 +       Maclaurin_all_lt_objl 1);
   4.527 +by (Step_tac 1);
   4.528 +by (Simp_tac 1);
   4.529 +by (Simp_tac 1);
   4.530 +by (case_tac "n" 1);
   4.531 +by (Clarify_tac 1); 
   4.532 +by (Asm_full_simp_tac 1);
   4.533 +by (dres_inst_tac [("x","0")] spec 1 THEN Asm_full_simp_tac 1);
   4.534 +by (Asm_full_simp_tac 1);
   4.535 +by (rtac ccontr 1);
   4.536 +by (Asm_full_simp_tac 1);
   4.537 +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
   4.538 +by (dtac ssubst 1 THEN assume_tac 2);
   4.539 +by (res_inst_tac [("x","t")] exI 1);
   4.540 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   4.541 +by (rtac sumr_fun_eq 1);
   4.542 +by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   4.543 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   4.544 +    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   4.545 +qed "Maclaurin_sin_expansion";
   4.546 +
   4.547 +Goal "EX t. abs t <= abs x &  \
   4.548 +\      sin x = \
   4.549 +\      (sumr 0 n (%m. (if even m then 0 \
   4.550 +\                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
   4.551 +\                      x ^ m)) \
   4.552 +\     + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
   4.553 +
   4.554 +by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
   4.555 +       ("diff","%n x. sin(x + 1/2*real (n)*pi)")] 
   4.556 +       Maclaurin_all_lt_objl 1);
   4.557 +by (Step_tac 1);
   4.558 +by (Simp_tac 1);
   4.559 +by (Simp_tac 1);
   4.560 +by (case_tac "n" 1);
   4.561 +by (Clarify_tac 1); 
   4.562 +by (Asm_full_simp_tac 1);
   4.563 +by (Asm_full_simp_tac 1);
   4.564 +by (rtac ccontr 1);
   4.565 +by (Asm_full_simp_tac 1);
   4.566 +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
   4.567 +by (dtac ssubst 1 THEN assume_tac 2);
   4.568 +by (res_inst_tac [("x","t")] exI 1);
   4.569 +by (rtac conjI 1);
   4.570 +by (arith_tac 1);
   4.571 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   4.572 +by (rtac sumr_fun_eq 1);
   4.573 +by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   4.574 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   4.575 +    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   4.576 +qed "Maclaurin_sin_expansion2";
   4.577 +
   4.578 +Goal "[| 0 < n; 0 < x |] ==> \
   4.579 +\      EX t. 0 < t & t < x & \
   4.580 +\      sin x = \
   4.581 +\      (sumr 0 n (%m. (if even m then 0 \
   4.582 +\                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
   4.583 +\                      x ^ m)) \
   4.584 +\     + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)";
   4.585 +by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),
   4.586 +       ("diff","%n x. sin(x + 1/2*real (n)*pi)")] 
   4.587 +       Maclaurin_objl 1);
   4.588 +by (Step_tac 1);
   4.589 +by (Asm_full_simp_tac 1);
   4.590 +by (Simp_tac 1);
   4.591 +by (dtac ssubst 1 THEN assume_tac 2);
   4.592 +by (res_inst_tac [("x","t")] exI 1);
   4.593 +by (rtac conjI 1 THEN rtac conjI 2);
   4.594 +by (assume_tac 1 THEN assume_tac 1);
   4.595 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   4.596 +by (rtac sumr_fun_eq 1);
   4.597 +by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   4.598 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   4.599 +    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   4.600 +qed "Maclaurin_sin_expansion3";
   4.601 +
   4.602 +Goal "0 < x ==> \
   4.603 +\      EX t. 0 < t & t <= x & \
   4.604 +\      sin x = \
   4.605 +\      (sumr 0 n (%m. (if even m then 0 \
   4.606 +\                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
   4.607 +\                      x ^ m)) \
   4.608 +\     + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
   4.609 +by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),
   4.610 +       ("diff","%n x. sin(x + 1/2*real (n)*pi)")] 
   4.611 +       Maclaurin2_objl 1);
   4.612 +by (Step_tac 1);
   4.613 +by (Asm_full_simp_tac 1);
   4.614 +by (Simp_tac 1);
   4.615 +by (dtac ssubst 1 THEN assume_tac 2);
   4.616 +by (res_inst_tac [("x","t")] exI 1);
   4.617 +by (rtac conjI 1 THEN rtac conjI 2);
   4.618 +by (assume_tac 1 THEN assume_tac 1);
   4.619 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   4.620 +by (rtac sumr_fun_eq 1);
   4.621 +by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   4.622 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   4.623 +    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   4.624 +qed "Maclaurin_sin_expansion4";
   4.625 +
   4.626 +(*-----------------------------------------------------------------------------*)
   4.627 +(* Maclaurin expansion for cos                                                 *)
   4.628 +(*-----------------------------------------------------------------------------*)
   4.629 +
   4.630 +Goal "sumr 0 (Suc n) \
   4.631 +\        (%m. (if even m \
   4.632 +\              then (- 1) ^ (m div 2)/(real  (fact m)) \
   4.633 +\              else 0) * \
   4.634 +\             0 ^ m) = 1";
   4.635 +by (induct_tac "n" 1);
   4.636 +by Auto_tac;
   4.637 +qed "sumr_cos_zero_one";
   4.638 +Addsimps [sumr_cos_zero_one];
   4.639 +
   4.640 +Goal "EX t. abs t <= abs x & \
   4.641 +\      cos x = \
   4.642 +\      (sumr 0 n (%m. (if even m \
   4.643 +\                      then (- 1) ^ (m div 2)/(real (fact m)) \
   4.644 +\                      else 0) * \
   4.645 +\                      x ^ m)) \
   4.646 +\     + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
   4.647 +by (cut_inst_tac [("f","cos"),("n","n"),("x","x"),
   4.648 +       ("diff","%n x. cos(x + 1/2*real (n)*pi)")] 
   4.649 +       Maclaurin_all_lt_objl 1);
   4.650 +by (Step_tac 1);
   4.651 +by (Simp_tac 1);
   4.652 +by (Simp_tac 1);
   4.653 +by (case_tac "n" 1);
   4.654 +by (Asm_full_simp_tac 1);
   4.655 +by (asm_full_simp_tac (simpset() delsimps [sumr_Suc]) 1);
   4.656 +by (rtac ccontr 1);
   4.657 +by (Asm_full_simp_tac 1);
   4.658 +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
   4.659 +by (dtac ssubst 1 THEN assume_tac 2);
   4.660 +by (res_inst_tac [("x","t")] exI 1);
   4.661 +by (rtac conjI 1);
   4.662 +by (arith_tac 1);
   4.663 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   4.664 +by (rtac sumr_fun_eq 1);
   4.665 +by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   4.666 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   4.667 +    even_mult_two_ex,real_add_mult_distrib,cos_add]  delsimps 
   4.668 +    [fact_Suc,realpow_Suc]));
   4.669 +by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   4.670 +qed "Maclaurin_cos_expansion";
   4.671 +
   4.672 +Goal "[| 0 < x; 0 < n |] ==> \
   4.673 +\      EX t. 0 < t & t < x & \
   4.674 +\      cos x = \
   4.675 +\      (sumr 0 n (%m. (if even m \
   4.676 +\                      then (- 1) ^ (m div 2)/(real (fact m)) \
   4.677 +\                      else 0) * \
   4.678 +\                      x ^ m)) \
   4.679 +\     + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
   4.680 +by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),
   4.681 +       ("diff","%n x. cos(x + 1/2*real (n)*pi)")] 
   4.682 +       Maclaurin_objl 1);
   4.683 +by (Step_tac 1);
   4.684 +by (Asm_full_simp_tac 1);
   4.685 +by (Simp_tac 1);
   4.686 +by (dtac ssubst 1 THEN assume_tac 2);
   4.687 +by (res_inst_tac [("x","t")] exI 1);
   4.688 +by (rtac conjI 1 THEN rtac conjI 2);
   4.689 +by (assume_tac 1 THEN assume_tac 1);
   4.690 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   4.691 +by (rtac sumr_fun_eq 1);
   4.692 +by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   4.693 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   4.694 +    even_mult_two_ex,real_add_mult_distrib,cos_add]  delsimps 
   4.695 +    [fact_Suc,realpow_Suc]));
   4.696 +by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   4.697 +qed "Maclaurin_cos_expansion2";
   4.698 +
   4.699 +Goal "[| x < 0; 0 < n |] ==> \
   4.700 +\      EX t. x < t & t < 0 & \
   4.701 +\      cos x = \
   4.702 +\      (sumr 0 n (%m. (if even m \
   4.703 +\                      then (- 1) ^ (m div 2)/(real (fact m)) \
   4.704 +\                      else 0) * \
   4.705 +\                      x ^ m)) \
   4.706 +\     + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
   4.707 +by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),
   4.708 +       ("diff","%n x. cos(x + 1/2*real (n)*pi)")] 
   4.709 +       Maclaurin_minus_objl 1);
   4.710 +by (Step_tac 1);
   4.711 +by (Asm_full_simp_tac 1);
   4.712 +by (Simp_tac 1);
   4.713 +by (dtac ssubst 1 THEN assume_tac 2);
   4.714 +by (res_inst_tac [("x","t")] exI 1);
   4.715 +by (rtac conjI 1 THEN rtac conjI 2);
   4.716 +by (assume_tac 1 THEN assume_tac 1);
   4.717 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   4.718 +by (rtac sumr_fun_eq 1);
   4.719 +by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   4.720 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   4.721 +    even_mult_two_ex,real_add_mult_distrib,cos_add]  delsimps 
   4.722 +    [fact_Suc,realpow_Suc]));
   4.723 +by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   4.724 +qed "Maclaurin_minus_cos_expansion";
   4.725 +
   4.726 +(* ------------------------------------------------------------------------- *)
   4.727 +(* Version for ln(1 +/- x). Where is it??                                    *)
   4.728 +(* ------------------------------------------------------------------------- *)
   4.729 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Nov 16 18:24:11 2001 +0100
     5.3 @@ -0,0 +1,7 @@
     5.4 +(*  Title       : MacLaurin.thy
     5.5 +    Author      : Jacques D. Fleuriot
     5.6 +    Copyright   : 2001 University of Edinburgh
     5.7 +    Description : MacLaurin series
     5.8 +*)
     5.9 +
    5.10 +MacLaurin = Log
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Hyperreal/Poly.ML	Fri Nov 16 18:24:11 2001 +0100
     6.3 @@ -0,0 +1,1208 @@
     6.4 +(*  Title:       Poly.ML
     6.5 +    Author:      Jacques D. Fleuriot
     6.6 +    Copyright:   2000 University of Edinburgh
     6.7 +    Description: Properties of real polynomials following 
     6.8 +                 John Harrison's HOL-Light implementation.
     6.9 +                 Some early theorems by Lucas Dixon
    6.10 +*)
    6.11 +
    6.12 +Goal "p +++ [] = p";
    6.13 +by (induct_tac "p" 1);
    6.14 +by Auto_tac;
    6.15 +qed "padd_Nil2";
    6.16 +Addsimps [padd_Nil2];
    6.17 +
    6.18 +Goal "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)";
    6.19 +by Auto_tac;
    6.20 +qed "padd_Cons_Cons";
    6.21 +
    6.22 +Goal "-- [] = []";
    6.23 +by (rewtac poly_minus_def);
    6.24 +by (Auto_tac);
    6.25 +qed "pminus_Nil";
    6.26 +Addsimps [pminus_Nil];
    6.27 +
    6.28 +Goal "[h1] *** p1 = h1 %* p1";
    6.29 +by (Simp_tac 1);
    6.30 +qed "pmult_singleton";
    6.31 +
    6.32 +Goal "1 %* t = t";
    6.33 +by (induct_tac "t" 1);
    6.34 +by Auto_tac;
    6.35 +qed "poly_ident_mult";
    6.36 +Addsimps [poly_ident_mult];
    6.37 +
    6.38 +Goal "[a] +++ ((0)#t) = (a#t)"; 
    6.39 +by (Simp_tac 1);
    6.40 +qed "poly_simple_add_Cons";
    6.41 +Addsimps [poly_simple_add_Cons];
    6.42 +
    6.43 +(*-------------------------------------------------------------------------*)
    6.44 +(*  Handy general properties                                               *)
    6.45 +(*-------------------------------------------------------------------------*)
    6.46 +
    6.47 +Goal "b +++ a = a +++ b"; 
    6.48 +by (subgoal_tac "ALL a. b +++ a = a +++ b" 1);
    6.49 +by (induct_tac "b" 2);
    6.50 +by Auto_tac;
    6.51 +by (rtac (padd_Cons RS ssubst) 1);
    6.52 +by (case_tac "aa" 1);
    6.53 +by Auto_tac;
    6.54 +qed "padd_commut";
    6.55 +
    6.56 +Goal "(a +++ b) +++ c = a +++ (b +++ c)"; 
    6.57 +by (subgoal_tac "ALL b c. (a +++ b) +++ c = a +++ (b +++ c)" 1);
    6.58 +by (Asm_simp_tac 1);
    6.59 +by (induct_tac "a" 1);
    6.60 +by (Step_tac 2);
    6.61 +by (case_tac "b" 2);
    6.62 +by (Asm_simp_tac 2);
    6.63 +by (Asm_simp_tac 2);
    6.64 +by (Asm_simp_tac 1);
    6.65 +qed "padd_assoc";
    6.66 +
    6.67 +Goal "a %* ( p +++ q ) = (a %* p +++ a %* q)";
    6.68 +by (subgoal_tac "ALL q. a %* ( p +++ q ) = (a %* p +++ a %* q) " 1);
    6.69 +by (induct_tac "p" 2);
    6.70 +by (Simp_tac 2);
    6.71 +by (rtac allI 2 );
    6.72 +by (case_tac "q" 2);
    6.73 +by (Asm_simp_tac 2);
    6.74 +by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib2] ) 2);
    6.75 +by (Asm_simp_tac 1);
    6.76 +qed "poly_cmult_distr";
    6.77 +
    6.78 +Goal "[0, 1] *** t = ((0)#t)";
    6.79 +by (induct_tac "t" 1);
    6.80 +by (Simp_tac 1);
    6.81 +by (simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1);
    6.82 +by (case_tac "list" 1);
    6.83 +by (Asm_simp_tac 1);
    6.84 +by (asm_full_simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1);
    6.85 +qed "pmult_by_x";
    6.86 +Addsimps [pmult_by_x];
    6.87 +
    6.88 +
    6.89 +(*-------------------------------------------------------------------------*)
    6.90 +(*  properties of evaluation of polynomials.                               *)
    6.91 +(*-------------------------------------------------------------------------*)
    6.92 +
    6.93 +Goal "poly (p1 +++ p2) x = poly p1 x + poly p2 x";
    6.94 +by (subgoal_tac "ALL p2. poly (p1 +++ p2) x = poly( p1 ) x + poly( p2 ) x" 1);
    6.95 +by (induct_tac "p1" 2);
    6.96 +by Auto_tac;
    6.97 +by (case_tac "p2" 1);
    6.98 +by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2]));
    6.99 +qed "poly_add";
   6.100 +
   6.101 +Goal "poly (c %* p) x = c * poly p x";
   6.102 +by (induct_tac "p" 1); 
   6.103 +by (case_tac "x=0" 2);
   6.104 +by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2] 
   6.105 +    @ real_mult_ac));
   6.106 +qed "poly_cmult";
   6.107 +
   6.108 +Goalw [poly_minus_def] "poly (-- p) x = - (poly p x)";
   6.109 +by (auto_tac (claset(),simpset() addsimps [poly_cmult]));
   6.110 +qed "poly_minus";
   6.111 +
   6.112 +Goal "poly (p1 *** p2) x = poly p1 x * poly p2 x";
   6.113 +by (subgoal_tac "ALL p2. poly (p1 *** p2) x = poly p1 x * poly p2 x" 1);
   6.114 +by (Asm_simp_tac 1);
   6.115 +by (induct_tac "p1" 1);
   6.116 +by (auto_tac (claset(),simpset() addsimps [poly_cmult]));
   6.117 +by (case_tac "list" 1);
   6.118 +by (auto_tac (claset(),simpset() addsimps [poly_cmult,poly_add,
   6.119 +    real_add_mult_distrib,real_add_mult_distrib2] @ real_mult_ac));
   6.120 +qed "poly_mult";
   6.121 +
   6.122 +Goal "poly (p %^ n) x = (poly p x) ^ n";
   6.123 +by (induct_tac "n" 1);
   6.124 +by (auto_tac (claset(),simpset() addsimps [poly_cmult, poly_mult]));
   6.125 +qed "poly_exp";
   6.126 +
   6.127 +(*-------------------------------------------------------------------------*)
   6.128 +(*  More Polynomial Evaluation Lemmas                                      *)
   6.129 +(*-------------------------------------------------------------------------*)
   6.130 +
   6.131 +Goal "poly (a +++ []) x = poly a x";
   6.132 +by (Simp_tac 1);
   6.133 +qed "poly_add_rzero";
   6.134 +Addsimps [poly_add_rzero];
   6.135 +
   6.136 +Goal "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x";
   6.137 +by (simp_tac (simpset() addsimps [poly_mult,real_mult_assoc])  1);
   6.138 +qed "poly_mult_assoc";
   6.139 +
   6.140 +Goal "poly (p *** []) x = 0";
   6.141 +by (induct_tac "p" 1);
   6.142 +by Auto_tac;
   6.143 +qed "poly_mult_Nil2";
   6.144 +Addsimps [poly_mult_Nil2];
   6.145 +
   6.146 +Goal "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d ) x";
   6.147 +by (induct_tac "n" 1);
   6.148 +by (auto_tac (claset(), simpset() addsimps [poly_mult,real_mult_assoc]));
   6.149 +qed "poly_exp_add";
   6.150 +
   6.151 +(*-------------------------------------------------------------------------*)
   6.152 +(*  The derivative                                                         *)
   6.153 +(*-------------------------------------------------------------------------*)
   6.154 +
   6.155 +Goalw [pderiv_def] "pderiv [] = []";
   6.156 +by (Simp_tac 1);
   6.157 +qed "pderiv_Nil";
   6.158 +Addsimps [pderiv_Nil];
   6.159 +
   6.160 +Goalw [pderiv_def] "pderiv [c] = []";
   6.161 +by (Simp_tac 1);
   6.162 +qed "pderiv_singleton";
   6.163 +Addsimps [pderiv_singleton];
   6.164 +
   6.165 +Goalw [pderiv_def] "pderiv (h#t) = pderiv_aux 1 t";
   6.166 +by (Simp_tac 1);
   6.167 +qed "pderiv_Cons";
   6.168 +
   6.169 +Goal "DERIV f x :> D ==> DERIV (%x. (f x) * c) x :> D * c";
   6.170 +by (auto_tac (claset() addIs [DERIV_cmult,real_mult_commute RS subst],
   6.171 +    simpset() addsimps [real_mult_commute]));
   6.172 +qed "DERIV_cmult2";
   6.173 +
   6.174 +Goal "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)";
   6.175 +by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_pow 1);
   6.176 +by (Simp_tac 1);
   6.177 +qed "DERIV_pow2";
   6.178 +Addsimps [DERIV_pow2,DERIV_pow];
   6.179 +
   6.180 +Goal "ALL n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \
   6.181 +    \   x ^ n * poly (pderiv_aux (Suc n) p) x ";
   6.182 +by (induct_tac "p" 1);
   6.183 +by (auto_tac (claset() addSIs [DERIV_add,DERIV_cmult2],simpset() addsimps 
   6.184 +    [pderiv_def,real_add_mult_distrib2,real_mult_assoc RS sym] delsimps 
   6.185 +    [realpow_Suc]));
   6.186 +by (rtac (real_mult_commute RS subst) 1);
   6.187 +by (simp_tac (simpset() delsimps [realpow_Suc]) 1);
   6.188 +by (asm_full_simp_tac (simpset() addsimps [real_mult_commute,realpow_Suc RS sym] 
   6.189 +    delsimps [realpow_Suc]) 1);
   6.190 +qed "lemma_DERIV_poly1";
   6.191 +
   6.192 +Goal "DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \
   6.193 +    \   x ^ n * poly (pderiv_aux (Suc n) p) x ";
   6.194 +by (simp_tac (simpset() addsimps [lemma_DERIV_poly1] delsimps [realpow_Suc]) 1);
   6.195 +qed "lemma_DERIV_poly";
   6.196 +
   6.197 +Goal "DERIV f x :> D ==>  DERIV (%x. a + f x) x :> D";
   6.198 +by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_add 1);
   6.199 +by Auto_tac;
   6.200 +qed "DERIV_add_const";
   6.201 +
   6.202 +Goal "DERIV (%x. poly p x) x :> poly (pderiv p) x";
   6.203 +by (induct_tac "p" 1);
   6.204 +by (auto_tac (claset(),simpset() addsimps [pderiv_Cons]));
   6.205 +by (rtac DERIV_add_const 1);
   6.206 +by (rtac lemma_DERIV_subst 1);
   6.207 +by (rtac (full_simplify (simpset()) 
   6.208 +    (read_instantiate [("n","0")] lemma_DERIV_poly)) 1);
   6.209 +by (simp_tac (simpset() addsimps [CLAIM "1 = 1"]) 1);
   6.210 +qed "poly_DERIV";
   6.211 +Addsimps [poly_DERIV];
   6.212 +
   6.213 +
   6.214 +(*-------------------------------------------------------------------------*)
   6.215 +(* Consequences of the derivative theorem above                            *)
   6.216 +(*-------------------------------------------------------------------------*)
   6.217 +
   6.218 +Goalw [differentiable_def] "(%x. poly p x) differentiable x";
   6.219 +by (blast_tac (claset() addIs [poly_DERIV]) 1);
   6.220 +qed "poly_differentiable";
   6.221 +Addsimps [poly_differentiable];
   6.222 +
   6.223 +Goal "isCont (%x. poly p x) x";
   6.224 +by (rtac (poly_DERIV RS DERIV_isCont) 1);
   6.225 +qed "poly_isCont";
   6.226 +Addsimps [poly_isCont];
   6.227 +
   6.228 +Goal "[| a < b; poly p a < 0; 0 < poly p b |] \
   6.229 +\     ==> EX x. a < x & x < b & (poly p x = 0)";
   6.230 +by (cut_inst_tac [("f","%x. poly p x"),("a","a"),("b","b"),("y","0")] 
   6.231 +    IVT_objl 1);
   6.232 +by (auto_tac (claset(),simpset() addsimps [real_le_less]));
   6.233 +qed "poly_IVT_pos";
   6.234 +
   6.235 +Goal "[| a < b; 0 < poly p a; poly p b < 0 |] \
   6.236 +\     ==> EX x. a < x & x < b & (poly p x = 0)";
   6.237 +by (blast_tac (claset() addIs [full_simplify (simpset() 
   6.238 +    addsimps [poly_minus, rename_numerals real_minus_zero_less_iff2])
   6.239 +   (read_instantiate [("p","-- p")] poly_IVT_pos)]) 1);
   6.240 +qed "poly_IVT_neg";
   6.241 +
   6.242 +Goal "a < b ==> \
   6.243 +\    EX x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)";
   6.244 +by (dres_inst_tac [("f","poly p")] MVT 1);
   6.245 +by Auto_tac;
   6.246 +by (res_inst_tac [("x","z")] exI 1);
   6.247 +by (auto_tac (claset() addDs [ARITH_PROVE 
   6.248 +    "[| a < z; z < b |] ==> (b - (a::real)) ~= 0"],simpset()
   6.249 +     addsimps [real_mult_left_cancel,poly_DERIV RS DERIV_unique]));
   6.250 +qed "poly_MVT";
   6.251 +
   6.252 +
   6.253 +(*-------------------------------------------------------------------------*)
   6.254 +(*  Lemmas for Derivatives                                                 *)
   6.255 +(*-------------------------------------------------------------------------*)
   6.256 +
   6.257 +Goal "ALL p2 n. poly (pderiv_aux n (p1 +++ p2)) x = \
   6.258 +    \           poly (pderiv_aux n p1 +++ pderiv_aux n p2) x";
   6.259 +by (induct_tac "p1" 1);
   6.260 +by (Step_tac 2);
   6.261 +by (case_tac "p2" 2);
   6.262 +by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2]));
   6.263 +qed "lemma_poly_pderiv_aux_add";
   6.264 +
   6.265 +Goal "poly (pderiv_aux n (p1 +++ p2)) x = \
   6.266 +    \ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x";
   6.267 +by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_add]) 1);
   6.268 +qed "poly_pderiv_aux_add";
   6.269 +
   6.270 +Goal "ALL n. poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x";
   6.271 +by (induct_tac "p" 1);
   6.272 +by (auto_tac (claset(),simpset() addsimps [poly_cmult] @ real_mult_ac));
   6.273 +qed "lemma_poly_pderiv_aux_cmult";
   6.274 +
   6.275 +Goal "poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x";
   6.276 +by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_cmult]) 1);
   6.277 +qed "poly_pderiv_aux_cmult";
   6.278 +
   6.279 +Goalw [poly_minus_def]
   6.280 +   "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x";
   6.281 +by (simp_tac (simpset() addsimps [poly_pderiv_aux_cmult]) 1);
   6.282 +qed "poly_pderiv_aux_minus";
   6.283 +
   6.284 +Goal "ALL n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x";
   6.285 +by (induct_tac "p" 1);
   6.286 +by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
   6.287 +    real_add_mult_distrib]));
   6.288 +qed "lemma_poly_pderiv_aux_mult1";
   6.289 +
   6.290 +Goal "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x";
   6.291 +by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_mult1]) 1);
   6.292 +qed "lemma_poly_pderiv_aux_mult";
   6.293 +
   6.294 +Goal "ALL q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x";
   6.295 +by (induct_tac "p" 1);
   6.296 +by (Step_tac 2);
   6.297 +by (case_tac "q" 2);
   6.298 +by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_add,poly_add,
   6.299 +    pderiv_def]));
   6.300 +qed "lemma_poly_pderiv_add";
   6.301 +
   6.302 +Goal "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x";
   6.303 +by (simp_tac (simpset() addsimps [lemma_poly_pderiv_add]) 1);
   6.304 +qed "poly_pderiv_add";
   6.305 +
   6.306 +Goal "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x";
   6.307 +by (induct_tac "p" 1);
   6.308 +by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_cmult,poly_cmult,
   6.309 +    pderiv_def]));
   6.310 +qed "poly_pderiv_cmult";
   6.311 +
   6.312 +Goalw [poly_minus_def] "poly (pderiv (--p)) x = poly (--(pderiv p)) x";
   6.313 +by (simp_tac (simpset() addsimps [poly_pderiv_cmult]) 1);
   6.314 +qed "poly_pderiv_minus";
   6.315 +
   6.316 +Goalw [pderiv_def] 
   6.317 +   "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x";
   6.318 +by (induct_tac "t" 1);
   6.319 +by (auto_tac (claset(),simpset() addsimps [poly_add,
   6.320 +    lemma_poly_pderiv_aux_mult]));
   6.321 +qed "lemma_poly_mult_pderiv";
   6.322 +
   6.323 +Goal "ALL q. poly (pderiv (p *** q)) x = \
   6.324 +\     poly (p *** (pderiv q) +++ q *** (pderiv p)) x";
   6.325 +by (induct_tac "p" 1);
   6.326 +by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
   6.327 +    poly_pderiv_cmult,poly_pderiv_add,poly_mult]));
   6.328 +by (rtac (lemma_poly_mult_pderiv RS ssubst) 1);
   6.329 +by (rtac (lemma_poly_mult_pderiv RS ssubst) 1);
   6.330 +by (rtac (poly_add RS ssubst) 1);
   6.331 +by (rtac (poly_add RS ssubst) 1);
   6.332 +by (asm_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2] 
   6.333 +    @ real_add_ac @ real_mult_ac) 1);
   6.334 +qed "poly_pderiv_mult";
   6.335 +
   6.336 +Goal "poly (pderiv (p %^ (Suc n))) x = \
   6.337 +    \    poly ((real (Suc n)) %* (p %^ n) *** pderiv p ) x";
   6.338 +by (induct_tac "n" 1);
   6.339 +by (auto_tac (claset(),simpset() addsimps [poly_add,poly_pderiv_cmult,
   6.340 +    poly_cmult,poly_pderiv_mult,real_of_nat_zero,poly_mult,
   6.341 +    real_of_nat_Suc,real_add_mult_distrib2,real_add_mult_distrib]
   6.342 +    @ real_mult_ac));
   6.343 +qed "poly_pderiv_exp";
   6.344 +
   6.345 +Goal "poly (pderiv ([-a, 1] %^ (Suc n))) x = \
   6.346 +\     poly (real (Suc n) %* ([-a, 1] %^ n)) x";
   6.347 +by (simp_tac (simpset() addsimps [poly_pderiv_exp,poly_mult] 
   6.348 +    delsimps [pexp_Suc]) 1);
   6.349 +by (simp_tac (simpset() addsimps [poly_cmult,pderiv_def]) 1);
   6.350 +qed "poly_pderiv_exp_prime";
   6.351 +
   6.352 +(* ----------------------------------------------------------------------- *)
   6.353 +(* Key property that f(a) = 0 ==> (x - a) divides p(x).                    *)
   6.354 +(* ----------------------------------------------------------------------- *)
   6.355 +
   6.356 +Goal "ALL h. EX q r. h#t = [r] +++ [-a, 1] *** q";
   6.357 +by (induct_tac "t" 1);
   6.358 +by (Step_tac 1);
   6.359 +by (res_inst_tac [("x","[]")] exI 1);
   6.360 +by (res_inst_tac [("x","h")] exI 1);
   6.361 +by (Simp_tac 1);
   6.362 +by (dres_inst_tac [("x","aa")] spec 1);
   6.363 +by (Step_tac 1);
   6.364 +by (res_inst_tac [("x","r#q")] exI 1);
   6.365 +by (res_inst_tac [("x","a*r + h")] exI 1);
   6.366 +by (case_tac "q" 1);
   6.367 +by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1 RS sym]));
   6.368 +qed "lemma_poly_linear_rem";
   6.369 +
   6.370 +Goal "EX q r. h#t = [r] +++ [-a, 1] *** q";
   6.371 +by (cut_inst_tac [("t","t"),("a","a")] lemma_poly_linear_rem 1);
   6.372 +by Auto_tac;
   6.373 +qed "poly_linear_rem";
   6.374 +
   6.375 +
   6.376 +Goal "(poly p a = 0) = ((p = []) | (EX q. p = [-a, 1] *** q))";
   6.377 +by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
   6.378 +    real_add_mult_distrib2]));
   6.379 +by (case_tac "p" 1);
   6.380 +by (cut_inst_tac [("h","aa"),("t","list"),("a","a")] poly_linear_rem 2);
   6.381 +by (Step_tac 2);
   6.382 +by (case_tac "q" 1);
   6.383 +by Auto_tac;
   6.384 +by (dres_inst_tac [("x","[]")] spec 1);
   6.385 +by (Asm_full_simp_tac 1);
   6.386 +by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
   6.387 +    real_add_assoc]));
   6.388 +by (dres_inst_tac [("x","aa#lista")] spec 1);
   6.389 +by Auto_tac;
   6.390 +qed "poly_linear_divides";
   6.391 +
   6.392 +Goal "ALL h k a. length (k %* p +++  (h # (a %* p))) = Suc (length p)";
   6.393 +by (induct_tac "p" 1);
   6.394 +by Auto_tac;
   6.395 +qed "lemma_poly_length_mult";
   6.396 +Addsimps [lemma_poly_length_mult];
   6.397 +
   6.398 +Goal "ALL h k. length (k %* p +++  (h # p)) = Suc (length p)";
   6.399 +by (induct_tac "p" 1);
   6.400 +by Auto_tac;
   6.401 +qed "lemma_poly_length_mult2";
   6.402 +Addsimps [lemma_poly_length_mult2];
   6.403 +
   6.404 +Goal "length([-a ,1] *** q) = Suc (length q)";
   6.405 +by Auto_tac;
   6.406 +qed "poly_length_mult";
   6.407 +Addsimps [poly_length_mult];
   6.408 +
   6.409 +
   6.410 +(*-------------------------------------------------------------------------*)
   6.411 +(* Polynomial length                                                       *)
   6.412 +(*-------------------------------------------------------------------------*)
   6.413 +
   6.414 +Goal "length (a %* p) = length p";
   6.415 +by (induct_tac "p" 1);
   6.416 +by Auto_tac;
   6.417 +qed "poly_cmult_length";
   6.418 +Addsimps [poly_cmult_length];
   6.419 +
   6.420 +Goal "length (p1 +++ p2) = (if (length( p1 ) < length( p2 )) \
   6.421 +\   then (length( p2 )) else (length( p1) ))";
   6.422 +by (subgoal_tac "ALL p2. length (p1 +++ p2) = (if (length( p1 ) < \
   6.423 +\   length( p2 )) then (length( p2 )) else (length( p1) ))" 1);
   6.424 +by (induct_tac "p1" 2);
   6.425 +by (Simp_tac 2);
   6.426 +by (Simp_tac 2);
   6.427 +by (Step_tac 2);  
   6.428 +by (Asm_full_simp_tac 2);
   6.429 +by (arith_tac 2);
   6.430 +by (Asm_full_simp_tac 2);
   6.431 +by (arith_tac 2);
   6.432 +by (induct_tac "p2" 1);
   6.433 +by (Asm_full_simp_tac 1);
   6.434 +by (Asm_full_simp_tac 1);
   6.435 +qed "poly_add_length";
   6.436 +
   6.437 +Goal "length([a,b] *** p) = Suc (length p)";
   6.438 +by (asm_full_simp_tac (simpset() addsimps [poly_cmult_length, 
   6.439 +    poly_add_length]) 1);
   6.440 +qed "poly_root_mult_length";
   6.441 +Addsimps [poly_root_mult_length];
   6.442 +
   6.443 +Goal "(poly (p *** q) x ~= poly [] x) = \
   6.444 +\     (poly p x ~= poly [] x & poly q x ~= poly [] x)";
   6.445 +by (auto_tac (claset(),simpset() addsimps [poly_mult,rename_numerals
   6.446 +    real_mult_not_zero]));
   6.447 +qed "poly_mult_not_eq_poly_Nil";
   6.448 +Addsimps [poly_mult_not_eq_poly_Nil];
   6.449 +
   6.450 +Goal "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)";
   6.451 +by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"],
   6.452 +    simpset() addsimps [poly_mult]));
   6.453 +qed "poly_mult_eq_zero_disj";
   6.454 +
   6.455 +(*-------------------------------------------------------------------------*)
   6.456 +(*  Normalisation Properties                                               *)
   6.457 +(*-------------------------------------------------------------------------*)
   6.458 +
   6.459 +Goal "(pnormalize p = []) --> (poly p x = 0)";
   6.460 +by (induct_tac "p" 1);
   6.461 +by Auto_tac;
   6.462 +qed "poly_normalized_nil";
   6.463 +
   6.464 +(*-------------------------------------------------------------------------*)
   6.465 +(*  A nontrivial polynomial of degree n has no more than n roots           *)
   6.466 +(*-------------------------------------------------------------------------*)
   6.467 +
   6.468 +Goal 
   6.469 +   "ALL p x. (poly p x ~= poly [] x & length p = n  \
   6.470 +\   --> (EX i. ALL x. (poly p x = (0::real)) --> (EX m. (m <= n & x = i m))))";
   6.471 +by (induct_tac "n" 1);
   6.472 +by (Step_tac 1);
   6.473 +by (rtac ccontr 1);
   6.474 +by (subgoal_tac "EX a. poly p a = 0" 1 THEN Step_tac 1);
   6.475 +by (dtac (poly_linear_divides RS iffD1) 1);
   6.476 +by (Step_tac 1);
   6.477 +by (dres_inst_tac [("x","q")] spec 1);
   6.478 +by (dres_inst_tac [("x","x")] spec 1);
   6.479 +by (asm_full_simp_tac (simpset() delsimps [poly_Nil,pmult_Cons]) 1);
   6.480 +by (etac exE 1);
   6.481 +by (dres_inst_tac [("x","%m. if m = Suc n then a else i m")] spec 1);
   6.482 +by (Step_tac 1);
   6.483 +by (dtac (poly_mult_eq_zero_disj RS iffD1) 1);
   6.484 +by (Step_tac 1);
   6.485 +by (dres_inst_tac [("x","Suc(length q)")] spec 1);
   6.486 +by (Asm_full_simp_tac 1);
   6.487 +by (dres_inst_tac [("x","xa")] spec 1 THEN Step_tac 1);
   6.488 +by (dres_inst_tac [("x","m")] spec 1);
   6.489 +by (Asm_full_simp_tac 1);
   6.490 +by (Blast_tac 1);
   6.491 +qed_spec_mp "poly_roots_index_lemma";
   6.492 +bind_thm ("poly_roots_index_lemma2",conjI RS poly_roots_index_lemma);
   6.493 +
   6.494 +Goal "poly p x ~= poly [] x ==> \
   6.495 +\     EX i. ALL x. (poly p x = 0) --> (EX n. n <= length p & x = i n)";
   6.496 +by (blast_tac (claset() addIs [poly_roots_index_lemma2]) 1);
   6.497 +qed "poly_roots_index_length";
   6.498 +
   6.499 +Goal "poly p x ~= poly [] x ==> \
   6.500 +\     EX N i. ALL x. (poly p x = 0) --> (EX n. (n::nat) < N & x = i n)";
   6.501 +by (dtac poly_roots_index_length 1 THEN Step_tac 1);
   6.502 +by (res_inst_tac [("x","Suc (length p)")] exI 1);
   6.503 +by (res_inst_tac [("x","i")] exI 1);
   6.504 +by (auto_tac (claset(),simpset() addsimps 
   6.505 +    [ARITH_PROVE "(m < Suc n) = (m <= n)"]));
   6.506 +qed "poly_roots_finite_lemma";
   6.507 +
   6.508 +(* annoying proof *)
   6.509 +Goal "ALL P. (ALL x. P x --> (EX n. (n::nat) < N & x = (j::nat=>real) n)) \
   6.510 +\     --> (EX a. ALL x. P x --> x < a)";
   6.511 +by (induct_tac "N" 1);
   6.512 +by (Asm_full_simp_tac 1);
   6.513 +by (Step_tac 1);
   6.514 +by (dres_inst_tac [("x","%z. P z & (z ~= (j::nat=>real) n)")] spec 1);
   6.515 +by Auto_tac;
   6.516 +by (dres_inst_tac [("x","x")] spec 1);
   6.517 +by (Step_tac 1);
   6.518 +by (res_inst_tac [("x","na")] exI 1);
   6.519 +by (auto_tac (claset() addDs [ARITH_PROVE "na < Suc n ==> na = n | na < n"],
   6.520 +    simpset()));
   6.521 +by (res_inst_tac [("x","abs a + abs(j n) + 1")] exI 1);
   6.522 +by (Step_tac 1);
   6.523 +by (dres_inst_tac [("x","x")] spec 1);
   6.524 +by (Step_tac 1);
   6.525 +by (dres_inst_tac [("x","j na")] spec 1);
   6.526 +by (Step_tac 1);
   6.527 +by (ALLGOALS(arith_tac));
   6.528 +qed_spec_mp "real_finite_lemma";
   6.529 +
   6.530 +Goal "(poly p ~= poly []) = \
   6.531 +\     (EX N j. ALL x. poly p x = 0 --> (EX n. (n::nat) < N & x = j n))";
   6.532 +by (Step_tac 1);
   6.533 +by (etac swap 1 THEN rtac ext 1);
   6.534 +by (rtac ccontr 1);
   6.535 +by (clarify_tac (claset() addSDs [poly_roots_finite_lemma]) 1);
   6.536 +by (clarify_tac (claset() addSDs [real_finite_lemma]) 1);
   6.537 +by (dres_inst_tac [("x","a")] fun_cong 1);
   6.538 +by Auto_tac;
   6.539 +qed "poly_roots_finite";
   6.540 +
   6.541 +(*-------------------------------------------------------------------------*)
   6.542 +(*  Entirety and Cancellation for polynomials                              *)
   6.543 +(*-------------------------------------------------------------------------*)
   6.544 +
   6.545 +Goal "[| poly p ~= poly [] ; poly q ~= poly [] |] \
   6.546 +\     ==>  poly (p *** q) ~= poly []";
   6.547 +by (auto_tac (claset(),simpset() addsimps [poly_roots_finite]));
   6.548 +by (res_inst_tac [("x","N + Na")] exI 1);
   6.549 +by (res_inst_tac [("x","%n. if n < N then j n else ja (n - N)")] exI 1);
   6.550 +by (auto_tac (claset(),simpset() addsimps [poly_mult_eq_zero_disj]));
   6.551 +by (flexflex_tac THEN rotate_tac 1 1);
   6.552 +by (dtac spec 1 THEN Auto_tac);
   6.553 +qed "poly_entire_lemma";
   6.554 +
   6.555 +Goal "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))";
   6.556 +by (auto_tac (claset() addIs [ext] addDs [fun_cong],simpset() 
   6.557 +    addsimps [poly_entire_lemma,poly_mult]));
   6.558 +by (blast_tac (claset() addIs [ccontr] addDs [poly_entire_lemma,
   6.559 +    poly_mult RS subst]) 1);
   6.560 +qed "poly_entire";
   6.561 +
   6.562 +Goal "(poly (p *** q) ~= poly []) = ((poly p ~= poly []) & (poly q ~= poly []))";
   6.563 +by (asm_full_simp_tac (simpset() addsimps [poly_entire]) 1);
   6.564 +qed "poly_entire_neg";
   6.565 +
   6.566 +Goal " (f = g) = (ALL x. f x = g x)";
   6.567 +by (auto_tac (claset() addSIs [ext],simpset()));
   6.568 +qed "fun_eq";
   6.569 +
   6.570 +Goal "(poly (p +++ -- q) = poly []) = (poly p = poly q)";
   6.571 +by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def,
   6.572 +    fun_eq,poly_cmult,ARITH_PROVE "(p + -q = 0) = (p = (q::real))"]));
   6.573 +qed "poly_add_minus_zero_iff";
   6.574 +
   6.575 +Goal "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))";
   6.576 +by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def,
   6.577 +    fun_eq,poly_mult,poly_cmult,real_add_mult_distrib2]));
   6.578 +qed "poly_add_minus_mult_eq";
   6.579 +
   6.580 +Goal "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)";
   6.581 +by (res_inst_tac [("p1","p *** q")] (poly_add_minus_zero_iff RS subst) 1);
   6.582 +by (auto_tac (claset() addIs [ext], simpset() addsimps [poly_add_minus_mult_eq,
   6.583 +    poly_entire,poly_add_minus_zero_iff]));
   6.584 +qed "poly_mult_left_cancel";
   6.585 +
   6.586 +Goal "(x * y = 0) = (x = (0::real) | y = 0)";
   6.587 +by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"],
   6.588 +    simpset()));
   6.589 +qed "real_mult_zero_disj_iff";
   6.590 +
   6.591 +Goal "(poly (p %^ n) = poly []) = (poly p = poly [] & n ~= 0)";
   6.592 +by (simp_tac (simpset() addsimps [fun_eq]) 1);
   6.593 +by (rtac (CLAIM "((ALL x. P x) & Q) = (ALL x. P x & Q)" RS ssubst) 1);
   6.594 +by (rtac (CLAIM "f = g ==> (ALL x. f x) = (ALL x. g x)") 1);
   6.595 +by (rtac ext 1);
   6.596 +by (induct_tac "n" 1);
   6.597 +by (auto_tac (claset(),simpset() addsimps [poly_mult,
   6.598 +    real_mult_zero_disj_iff]));
   6.599 +qed "poly_exp_eq_zero";
   6.600 +Addsimps [poly_exp_eq_zero];
   6.601 +
   6.602 +Goal "poly [a,1] ~= poly []";
   6.603 +by (simp_tac (simpset() addsimps [fun_eq]) 1);
   6.604 +by (res_inst_tac [("x","1 - a")] exI 1);
   6.605 +by (Simp_tac 1);
   6.606 +qed "poly_prime_eq_zero";
   6.607 +Addsimps [poly_prime_eq_zero];
   6.608 +
   6.609 +Goal "(poly ([a, 1] %^ n) ~= poly [])";
   6.610 +by Auto_tac;
   6.611 +qed "poly_exp_prime_eq_zero";
   6.612 +Addsimps [poly_exp_prime_eq_zero];
   6.613 +
   6.614 +(*-------------------------------------------------------------------------*)
   6.615 +(*  A more constructive notion of polynomials being trivial                *)
   6.616 +(*-------------------------------------------------------------------------*)
   6.617 +
   6.618 +Goal "poly (h # t) = poly [] ==> h = 0 & poly t = poly []";
   6.619 +by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
   6.620 +by (case_tac "h = 0" 1);
   6.621 +by (dres_inst_tac [("x","0")] spec 2);
   6.622 +by (rtac conjI 1);
   6.623 +by (rtac ((simplify (simpset()) (read_instantiate [("g","poly []")] fun_eq))
   6.624 +    RS iffD1) 2 THEN rtac ccontr 2);
   6.625 +by (auto_tac (claset(),simpset() addsimps [poly_roots_finite,
   6.626 +    real_mult_zero_disj_iff]));
   6.627 +by (dtac real_finite_lemma 1 THEN Step_tac 1);
   6.628 +by (REPEAT(dres_inst_tac [("x","abs a + 1")] spec 1));
   6.629 +by (arith_tac 1);
   6.630 +qed "poly_zero_lemma";
   6.631 +
   6.632 +Goal "(poly p = poly []) = list_all (%c. c = 0) p";
   6.633 +by (induct_tac "p" 1);
   6.634 +by (Asm_full_simp_tac 1);
   6.635 +by (rtac iffI 1);
   6.636 +by (dtac poly_zero_lemma 1);
   6.637 +by Auto_tac;
   6.638 +qed "poly_zero";
   6.639 +
   6.640 +Addsimps [real_mult_zero_disj_iff];
   6.641 +Goal "ALL n. (list_all (%c. c = 0) (pderiv_aux (Suc n) p) = \
   6.642 +\     list_all (%c. c = 0) p)";
   6.643 +by (induct_tac "p" 1);
   6.644 +by Auto_tac;
   6.645 +qed_spec_mp "pderiv_aux_iszero";
   6.646 +Addsimps [pderiv_aux_iszero];
   6.647 +
   6.648 +Goal "(number_of n :: nat) ~= 0 \
   6.649 +\     ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) = \
   6.650 +\     list_all (%c. c = 0) p)";
   6.651 +by (res_inst_tac [("n1","number_of n"),("m1","0")] (less_imp_Suc_add RS exE) 1);
   6.652 +by (Force_tac 1);
   6.653 +by (res_inst_tac [("n1","0 + x")] (pderiv_aux_iszero RS subst) 1);
   6.654 +by (asm_simp_tac (simpset() delsimps [pderiv_aux_iszero]) 1);
   6.655 +qed "pderiv_aux_iszero_num";
   6.656 +
   6.657 +Goal "poly (pderiv p) = poly [] --> (EX h. poly p = poly [h])";
   6.658 +by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1);
   6.659 +by (induct_tac "p" 1);
   6.660 +by (Force_tac 1);
   6.661 +by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons,
   6.662 +    pderiv_aux_iszero_num] delsimps [poly_Cons]) 1);
   6.663 +by (auto_tac (claset(),simpset() addsimps [poly_zero RS sym]));
   6.664 +qed_spec_mp "pderiv_iszero";
   6.665 +
   6.666 +Goal "poly p = poly [] --> (poly (pderiv p) = poly [])";
   6.667 +by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1);
   6.668 +by (induct_tac "p" 1);
   6.669 +by (Force_tac 1);
   6.670 +by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons,
   6.671 +    pderiv_aux_iszero_num] delsimps [poly_Cons]) 1);
   6.672 +qed "pderiv_zero_obj";
   6.673 +
   6.674 +Goal "poly p = poly [] ==> (poly (pderiv p) = poly [])";
   6.675 +by (blast_tac (claset() addEs [pderiv_zero_obj RS impE]) 1);
   6.676 +qed "pderiv_zero";
   6.677 +Addsimps [pderiv_zero];
   6.678 +
   6.679 +Goal "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))";
   6.680 +by (cut_inst_tac [("p","p +++ --q")] pderiv_zero_obj 1);
   6.681 +by (auto_tac (claset() addIs [ ARITH_PROVE "x + - y = 0 ==> x = (y::real)"],
   6.682 +    simpset() addsimps [fun_eq,poly_add,poly_minus,poly_pderiv_add,
   6.683 +    poly_pderiv_minus] delsimps [pderiv_zero]));
   6.684 +qed "poly_pderiv_welldef";
   6.685 +
   6.686 +(* ------------------------------------------------------------------------- *)
   6.687 +(* Basics of divisibility.                                                   *)
   6.688 +(* ------------------------------------------------------------------------- *)
   6.689 +
   6.690 +Goal "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)";
   6.691 +by (auto_tac (claset(),simpset() addsimps [divides_def,fun_eq,poly_mult,
   6.692 +    poly_add,poly_cmult,real_add_mult_distrib RS sym]));
   6.693 +by (dres_inst_tac [("x","-a")] spec 1);
   6.694 +by (auto_tac (claset(),simpset() addsimps [poly_linear_divides,poly_add,
   6.695 +    poly_cmult,real_add_mult_distrib RS sym]));
   6.696 +by (res_inst_tac [("x","qa *** q")] exI 1);
   6.697 +by (res_inst_tac [("x","p *** qa")] exI 2);
   6.698 +by (auto_tac (claset(),simpset() addsimps [poly_add,poly_mult,
   6.699 +    poly_cmult] @ real_mult_ac));
   6.700 +qed "poly_primes";
   6.701 +
   6.702 +Goalw [divides_def] "p divides p";
   6.703 +by (res_inst_tac [("x","[1]")] exI 1);
   6.704 +by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq]));
   6.705 +qed "poly_divides_refl";
   6.706 +Addsimps [poly_divides_refl];
   6.707 +
   6.708 +Goalw [divides_def] "[| p divides q; q divides r |] ==> p divides r";
   6.709 +by (Step_tac 1);
   6.710 +by (res_inst_tac [("x","qa *** qaa")] exI 1);
   6.711 +by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,
   6.712 +    real_mult_assoc]));
   6.713 +qed "poly_divides_trans";
   6.714 +
   6.715 +Goal "(m::nat) <= n = (EX d. n = m + d)";
   6.716 +by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
   6.717 +    less_iff_Suc_add]));
   6.718 +qed "le_iff_add";
   6.719 +
   6.720 +Goal "m <= n ==> (p %^ m) divides (p %^ n)";
   6.721 +by (auto_tac (claset(),simpset() addsimps [le_iff_add]));
   6.722 +by (induct_tac "d" 1);
   6.723 +by (rtac poly_divides_trans 2);
   6.724 +by (auto_tac (claset(),simpset() addsimps [divides_def]));
   6.725 +by (res_inst_tac [("x","p")] exI 1);
   6.726 +by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq]
   6.727 +    @ real_mult_ac));
   6.728 +qed "poly_divides_exp";
   6.729 +
   6.730 +Goal "[| (p %^ n) divides q;  m <= n |] ==> (p %^ m) divides q";
   6.731 +by (blast_tac (claset() addIs [poly_divides_exp,poly_divides_trans]) 1);
   6.732 +qed "poly_exp_divides";
   6.733 +
   6.734 +Goalw [divides_def] 
   6.735 +   "[| p divides q; p divides r |] ==> p divides (q +++ r)";
   6.736 +by Auto_tac;
   6.737 +by (res_inst_tac [("x","qa +++ qaa")] exI 1);
   6.738 +by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
   6.739 +    real_add_mult_distrib2]));
   6.740 +qed "poly_divides_add";
   6.741 +
   6.742 +Goalw [divides_def] 
   6.743 +   "[| p divides q; p divides (q +++ r) |] ==> p divides r";
   6.744 +by Auto_tac;
   6.745 +by (res_inst_tac [("x","qaa +++ -- qa")] exI 1);
   6.746 +by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
   6.747 +    poly_minus,real_add_mult_distrib2,real_minus_mult_eq2 RS sym,
   6.748 +    ARITH_PROVE "(x = y + -z) = (z + x = (y::real))"]));
   6.749 +qed "poly_divides_diff";
   6.750 +
   6.751 +Goal "[| p divides r; p divides (q +++ r) |] ==> p divides q";
   6.752 +by (etac poly_divides_diff 1);
   6.753 +by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
   6.754 +    divides_def] @ real_add_ac));
   6.755 +qed "poly_divides_diff2";
   6.756 +
   6.757 +Goalw [divides_def] "poly p = poly [] ==> q divides p";
   6.758 +by (auto_tac (claset(),simpset() addsimps [fun_eq,poly_mult]));
   6.759 +qed "poly_divides_zero";
   6.760 +
   6.761 +Goalw [divides_def] "q divides []";
   6.762 +by (res_inst_tac [("x","[]")] exI 1); 
   6.763 +by (auto_tac (claset(),simpset() addsimps [fun_eq]));
   6.764 +qed "poly_divides_zero2";
   6.765 +Addsimps [poly_divides_zero2];
   6.766 +
   6.767 +(* ------------------------------------------------------------------------- *)
   6.768 +(* At last, we can consider the order of a root.                             *)
   6.769 +(* ------------------------------------------------------------------------- *)
   6.770 +
   6.771 +(* FIXME: Tidy up *)
   6.772 +Goal "[| length p = d; poly p ~= poly [] |] \
   6.773 +\     ==> EX n. ([-a, 1] %^ n) divides p & \
   6.774 +\               ~(([-a, 1] %^ (Suc n)) divides p)";
   6.775 +by (subgoal_tac "ALL p. length p = d & poly p ~= poly [] \
   6.776 +\     --> (EX n q. p = mulexp n [-a, 1] q & poly q a ~= 0)" 1);
   6.777 +by (induct_tac "d" 2);
   6.778 +by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 2);
   6.779 +by (Step_tac 2);
   6.780 +by (case_tac "poly pa a = 0" 2);
   6.781 +by (dtac (poly_linear_divides RS iffD1) 2);
   6.782 +by (Step_tac 2);
   6.783 +by (dres_inst_tac [("x","q")] spec 2);
   6.784 +by (dtac (poly_entire_neg RS iffD1) 2);
   6.785 +by (Step_tac 2);
   6.786 +by (Force_tac 2 THEN Blast_tac 2);
   6.787 +by (res_inst_tac [("x","Suc na")] exI 2);
   6.788 +by (res_inst_tac [("x","qa")] exI 2);
   6.789 +by (asm_full_simp_tac (simpset() delsimps [pmult_Cons]) 2);
   6.790 +by (res_inst_tac [("x","0")] exI 2);
   6.791 +by (Force_tac 2);
   6.792 +by (dres_inst_tac [("x","p")] spec 1 THEN Step_tac 1);
   6.793 +by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1);
   6.794 +by (rewtac divides_def);
   6.795 +by (res_inst_tac [("x","q")] exI 1);
   6.796 +by (induct_tac "n" 1);
   6.797 +by (Simp_tac 1);
   6.798 +by (asm_simp_tac (simpset() addsimps [poly_add,poly_cmult,poly_mult,
   6.799 +    real_add_mult_distrib2] @ real_mult_ac) 1);
   6.800 +by (Step_tac 1);
   6.801 +by (rotate_tac 2 1);
   6.802 +by (rtac swap 1 THEN assume_tac 2);
   6.803 +by (induct_tac "n" 1);
   6.804 +by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
   6.805 +by (eres_inst_tac [("Pa","poly q a = 0")] swap 1);
   6.806 +by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult,
   6.807 +    real_minus_mult_eq1 RS sym]) 1);
   6.808 +by (rtac (pexp_Suc RS ssubst) 1);
   6.809 +by (rtac ccontr 1);
   6.810 +by (asm_full_simp_tac (simpset() addsimps [poly_mult_left_cancel,
   6.811 +    poly_mult_assoc] delsimps [pmult_Cons,pexp_Suc]) 1);
   6.812 +qed "poly_order_exists";
   6.813 +
   6.814 +Goalw [divides_def] "[1] divides p";
   6.815 +by Auto_tac;
   6.816 +qed "poly_one_divides";
   6.817 +Addsimps [poly_one_divides];
   6.818 +
   6.819 +Goal "poly p ~= poly [] \
   6.820 +\     ==> EX! n. ([-a, 1] %^ n) divides p & \
   6.821 +\                ~(([-a, 1] %^ (Suc n)) divides p)";
   6.822 +by (auto_tac (claset() addIs [poly_order_exists],
   6.823 +    simpset() addsimps [less_linear] delsimps [pmult_Cons,pexp_Suc]));
   6.824 +by (cut_inst_tac [("m","y"),("n","n")] less_linear 1);
   6.825 +by (dres_inst_tac [("m","n")] poly_exp_divides 1);
   6.826 +by (auto_tac (claset() addDs [ARITH_PROVE "n < m ==> Suc n <= m" RSN  
   6.827 +    (2,poly_exp_divides)],simpset() delsimps [pmult_Cons,pexp_Suc]));
   6.828 +qed "poly_order";
   6.829 +
   6.830 +(* ------------------------------------------------------------------------- *)
   6.831 +(* Order                                                                     *)
   6.832 +(* ------------------------------------------------------------------------- *)
   6.833 +
   6.834 +Goal "[| n = (@n. P n); EX! n. P n |] ==> P n";
   6.835 +by (blast_tac (claset() addIs [someI2]) 1);
   6.836 +qed "some1_equalityD";
   6.837 +
   6.838 +Goalw [order_def]
   6.839 +      "(([-a, 1] %^ n) divides p & \
   6.840 +\       ~(([-a, 1] %^ (Suc n)) divides p)) = \
   6.841 +\       ((n = order a p) & ~(poly p = poly []))";
   6.842 +by (rtac iffI 1);
   6.843 +by (blast_tac (claset() addDs [poly_divides_zero] 
   6.844 +    addSIs [some1_equality RS sym, poly_order]) 1);
   6.845 +by (blast_tac (claset() addSIs [poly_order RSN (2,some1_equalityD)]) 1);
   6.846 +qed "order";
   6.847 +
   6.848 +Goal "[| poly p ~= poly [] |] \
   6.849 +\     ==> ([-a, 1] %^ (order a p)) divides p & \
   6.850 +\             ~(([-a, 1] %^ (Suc(order a p))) divides p)";
   6.851 +by (asm_full_simp_tac (simpset() addsimps [order] delsimps [pexp_Suc]) 1);
   6.852 +qed "order2";
   6.853 +
   6.854 +Goal "[| poly p ~= poly []; ([-a, 1] %^ n) divides p; \
   6.855 +\        ~(([-a, 1] %^ (Suc n)) divides p) \
   6.856 +\     |] ==> (n = order a p)";
   6.857 +by (cut_inst_tac [("p","p"),("a","a"),("n","n")] order 1);
   6.858 +by Auto_tac;
   6.859 +qed "order_unique";
   6.860 +
   6.861 +Goal "(poly p ~= poly [] & ([-a, 1] %^ n) divides p & \
   6.862 +\        ~(([-a, 1] %^ (Suc n)) divides p)) \
   6.863 +\     ==> (n = order a p)";
   6.864 +by (blast_tac (claset() addIs [order_unique]) 1);
   6.865 +qed "order_unique_lemma";
   6.866 +
   6.867 +Goal "poly p = poly q ==> order a p = order a q";
   6.868 +by (auto_tac (claset(),simpset() addsimps [fun_eq,divides_def,poly_mult,
   6.869 +    order_def]));
   6.870 +qed "order_poly";
   6.871 +
   6.872 +Goal "p %^ (Suc 0) = p";
   6.873 +by (induct_tac "p" 1);
   6.874 +by (auto_tac (claset(),simpset() addsimps [numeral_1_eq_1]));
   6.875 +qed "pexp_one";
   6.876 +Addsimps [pexp_one];
   6.877 +
   6.878 +Goal "ALL p a. 0 < n & [- a, 1] %^ n divides p & \
   6.879 +\            ~ [- a, 1] %^ (Suc n) divides p \
   6.880 +\            --> poly p a = 0";
   6.881 +by (induct_tac "n" 1);
   6.882 +by (Blast_tac 1);
   6.883 +by (auto_tac (claset(),simpset() addsimps [divides_def,poly_mult] 
   6.884 +    delsimps [pmult_Cons]));
   6.885 +qed_spec_mp "lemma_order_root";
   6.886 +
   6.887 +Goal "(poly p a = 0) = ((poly p = poly []) | order a p ~= 0)";
   6.888 +by (case_tac "poly p = poly []" 1);
   6.889 +by Auto_tac;
   6.890 +by (asm_full_simp_tac (simpset() addsimps [poly_linear_divides]
   6.891 +    delsimps [pmult_Cons]) 1);
   6.892 +by (Step_tac 1);
   6.893 +by (ALLGOALS(dres_inst_tac [("a","a")] order2));
   6.894 +by (rtac ccontr 1);
   6.895 +by (asm_full_simp_tac (simpset() addsimps [divides_def,poly_mult,fun_eq]
   6.896 +    delsimps [pmult_Cons]) 1);
   6.897 +by (Blast_tac 1);
   6.898 +by (blast_tac (claset() addIs [lemma_order_root]) 1);
   6.899 +qed "order_root";
   6.900 +
   6.901 +Goal "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n <= order a p)";
   6.902 +by (case_tac "poly p = poly []" 1);
   6.903 +by Auto_tac;
   6.904 +by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_mult]) 1);
   6.905 +by (res_inst_tac [("x","[]")] exI 1);
   6.906 +by (TRYALL(dres_inst_tac [("a","a")] order2));
   6.907 +by (auto_tac (claset() addIs [poly_exp_divides],simpset()
   6.908 +    delsimps [pexp_Suc]));
   6.909 +qed "order_divides";
   6.910 +
   6.911 +Goalw [divides_def] 
   6.912 +     "poly p ~= poly [] \
   6.913 +\     ==> EX q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) & \
   6.914 +\               ~([-a, 1] divides q)";
   6.915 +by (dres_inst_tac [("a","a")] order2 1);
   6.916 +by (asm_full_simp_tac (simpset() addsimps [divides_def]
   6.917 +     delsimps [pexp_Suc,pmult_Cons]) 1);
   6.918 +by (Step_tac 1);
   6.919 +by (res_inst_tac [("x","q")] exI 1);
   6.920 +by (Step_tac 1);
   6.921 +by (dres_inst_tac [("x","qa")] spec 1);
   6.922 +by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,poly_exp] 
   6.923 +    @ real_mult_ac delsimps [pmult_Cons]));
   6.924 +qed "order_decomp";
   6.925 +
   6.926 +(* ------------------------------------------------------------------------- *)
   6.927 +(* Important composition properties of orders.                               *)
   6.928 +(* ------------------------------------------------------------------------- *)
   6.929 +
   6.930 +Goal "poly (p *** q) ~= poly [] \
   6.931 +\     ==> order a (p *** q) = order a p + order a q";
   6.932 +by (cut_inst_tac [("a","a"),("p","p***q"),("n","order a p + order a q")] 
   6.933 +    order 1);
   6.934 +by (auto_tac (claset(),simpset() addsimps [poly_entire] delsimps [pmult_Cons]));
   6.935 +by (REPEAT(dres_inst_tac [("a","a")] order2 1));
   6.936 +by (Step_tac 1);
   6.937 +by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_exp_add,
   6.938 +    poly_mult] delsimps [pmult_Cons]) 1);
   6.939 +by (Step_tac 1);
   6.940 +by (res_inst_tac [("x","qa *** qaa")] exI 1);
   6.941 +by (asm_full_simp_tac (simpset() addsimps [poly_mult] @ real_mult_ac
   6.942 +    delsimps [pmult_Cons]) 1);
   6.943 +by (REPEAT(dres_inst_tac [("a","a")] order_decomp 1));
   6.944 +by (Step_tac 1);
   6.945 +by (subgoal_tac "[-a,1] divides (qa *** qaa)" 1);
   6.946 +by (asm_full_simp_tac (simpset() addsimps [poly_primes] 
   6.947 +    delsimps [pmult_Cons]) 1);
   6.948 +by (auto_tac (claset(),simpset() addsimps [divides_def] 
   6.949 +    delsimps [pmult_Cons]));
   6.950 +by (res_inst_tac [("x","qb")] exI 1);
   6.951 +by (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = \
   6.952 +\                poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))" 1);
   6.953 +by (dtac (poly_mult_left_cancel RS iffD1) 1);
   6.954 +by (Force_tac 1);
   6.955 +by (subgoal_tac "poly ([-a, 1] %^ (order a q) *** \
   6.956 +\                      ([-a, 1] %^ (order a p) *** (qa *** qaa))) = \
   6.957 +\                poly ([-a, 1] %^ (order a q) *** \
   6.958 +\                      ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb)))" 1);
   6.959 +by (dtac (poly_mult_left_cancel RS iffD1) 1);
   6.960 +by (Force_tac 1);
   6.961 +by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_exp_add,poly_mult] 
   6.962 +    @ real_mult_ac delsimps [pmult_Cons]) 1);
   6.963 +qed "order_mult";
   6.964 +
   6.965 +(* FIXME: too too long! *)
   6.966 +Goal "ALL p q a. 0 < n &  \
   6.967 +\      poly (pderiv p) ~= poly [] & \
   6.968 +\      poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q \
   6.969 +\      --> n = Suc (order a (pderiv p))";
   6.970 +by (induct_tac "n" 1);
   6.971 +by (Step_tac 1);
   6.972 +by (rtac order_unique_lemma 1 THEN rtac conjI 1);
   6.973 +by (assume_tac 1);
   6.974 +by (subgoal_tac "ALL r. r divides (pderiv p) = \
   6.975 +\                       r divides (pderiv ([-a, 1] %^ Suc n *** q))" 1);
   6.976 +by (dtac poly_pderiv_welldef 2);
   6.977 +by (asm_full_simp_tac (simpset() addsimps [divides_def] delsimps [pmult_Cons,
   6.978 +    pexp_Suc]) 2);
   6.979 +by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
   6.980 +by (rtac conjI 1);
   6.981 +by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq] 
   6.982 +    delsimps [pmult_Cons,pexp_Suc]) 1);
   6.983 +by (res_inst_tac 
   6.984 +    [("x","[-a, 1] *** (pderiv q) +++ real (Suc n) %* q")] exI 1);
   6.985 +by (asm_full_simp_tac (simpset() addsimps [poly_pderiv_mult,
   6.986 +    poly_pderiv_exp_prime,poly_add,poly_mult,poly_cmult,
   6.987 +    real_add_mult_distrib2] @ real_mult_ac
   6.988 +    delsimps [pmult_Cons,pexp_Suc]) 1);
   6.989 +by (asm_full_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2,
   6.990 +    real_add_mult_distrib] @ real_mult_ac delsimps [pmult_Cons]) 1);
   6.991 +by (thin_tac "ALL r. \
   6.992 +\             r divides pderiv p = \
   6.993 +\             r divides pderiv ([- a, 1] %^ Suc n *** q)" 1);
   6.994 +by (rewtac divides_def);
   6.995 +by (simp_tac (simpset() addsimps [poly_pderiv_mult,
   6.996 +    poly_pderiv_exp_prime,fun_eq,poly_add,poly_mult] 
   6.997 +    delsimps [pmult_Cons,pexp_Suc]) 1);
   6.998 +by (rtac swap 1 THEN assume_tac 1);
   6.999 +by (rotate_tac  3 1 THEN etac swap 1);
  6.1000 +by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
  6.1001 +by (Step_tac 1);
  6.1002 +by (res_inst_tac [("x","inverse(real (Suc n)) %* (qa +++ --(pderiv q))")]
  6.1003 +    exI 1);
  6.1004 +by (subgoal_tac "poly ([-a, 1] %^ n *** q) = \
  6.1005 +\         poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* \
  6.1006 +\         (qa +++ -- (pderiv q)))))" 1);
  6.1007 +by (dtac (poly_mult_left_cancel RS iffD1) 1);
  6.1008 +by (Asm_full_simp_tac 1);
  6.1009 +by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult,
  6.1010 +    poly_minus] delsimps [pmult_Cons]) 1);
  6.1011 +by (Step_tac 1);
  6.1012 +by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel 
  6.1013 +    RS iffD1) 1);
  6.1014 +by (Simp_tac 1);
  6.1015 +by (rtac ((CLAIM_SIMP 
  6.1016 +    "a * (b * (c * (d * e))) = e * (b * (c * (d * (a::real))))" 
  6.1017 +     real_mult_ac) RS ssubst) 1);
  6.1018 +by (rotate_tac 2 1);
  6.1019 +by (dres_inst_tac [("x","xa")] spec 1);
  6.1020 +by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib,
  6.1021 +    real_minus_mult_eq1 RS sym] @ real_mult_ac
  6.1022 +    delsimps [pmult_Cons]) 1);
  6.1023 +qed_spec_mp "lemma_order_pderiv";
  6.1024 +
  6.1025 +Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \
  6.1026 +\     ==> (order a p = Suc (order a (pderiv p)))";
  6.1027 +by (case_tac "poly p = poly []" 1);
  6.1028 +by (auto_tac (claset() addDs [pderiv_zero],simpset()));
  6.1029 +by (dres_inst_tac [("a","a"),("p","p")] order_decomp 1);
  6.1030 +by (blast_tac (claset() addIs [lemma_order_pderiv]) 1);
  6.1031 +qed "order_pderiv";
  6.1032 +
  6.1033 +(* ------------------------------------------------------------------------- *)
  6.1034 +(* Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
  6.1035 +(* `a la Harrison                                                            *)
  6.1036 +(* ------------------------------------------------------------------------- *)
  6.1037 +
  6.1038 +Goal "[| poly (pderiv p) ~= poly []; \
  6.1039 +\        poly p = poly (q *** d); \
  6.1040 +\        poly (pderiv p) = poly (e *** d); \
  6.1041 +\        poly d = poly (r *** p +++ s *** pderiv p) \
  6.1042 +\     |] ==> order a q = (if order a p = 0 then 0 else 1)";
  6.1043 +by (subgoal_tac "order a p = order a q + order a d" 1);
  6.1044 +by (res_inst_tac [("s","order a (q *** d)")] trans 2);
  6.1045 +by (blast_tac (claset() addIs [order_poly]) 2);
  6.1046 +by (rtac order_mult 2);
  6.1047 +by (rtac notI 2 THEN Asm_full_simp_tac 2);
  6.1048 +by (dres_inst_tac [("p","p")] pderiv_zero 2);
  6.1049 +by (Asm_full_simp_tac 2);
  6.1050 +by (case_tac "order a p = 0" 1);
  6.1051 +by (Asm_full_simp_tac 1);
  6.1052 +by (subgoal_tac "order a (pderiv p) = order a e + order a d" 1);
  6.1053 +by (res_inst_tac [("s","order a (e *** d)")] trans 2);
  6.1054 +by (blast_tac (claset() addIs [order_poly]) 2);
  6.1055 +by (rtac order_mult 2);
  6.1056 +by (rtac notI 2 THEN Asm_full_simp_tac 2);
  6.1057 +by (case_tac "poly p = poly []" 1);
  6.1058 +by (dres_inst_tac [("p","p")] pderiv_zero 1);
  6.1059 +by (Asm_full_simp_tac 1);
  6.1060 +by (dtac order_pderiv 1 THEN assume_tac 1);
  6.1061 +by (subgoal_tac "order a (pderiv p) <= order a d" 1);
  6.1062 +by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides d" 2);
  6.1063 +by (asm_full_simp_tac (simpset() addsimps [poly_entire,order_divides]) 2);
  6.1064 +by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides p & \
  6.1065 +\       ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p)" 2);
  6.1066 +by (asm_simp_tac (simpset() addsimps [order_divides]) 3);
  6.1067 +by (asm_full_simp_tac (simpset() addsimps [divides_def]
  6.1068 +    delsimps [pexp_Suc,pmult_Cons]) 2);
  6.1069 +by (Step_tac 2);
  6.1070 +by (res_inst_tac [("x","r *** qa +++ s *** qaa")] exI 2);
  6.1071 +by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_add,poly_mult,
  6.1072 +    real_add_mult_distrib, real_add_mult_distrib2] @ real_mult_ac
  6.1073 +    delsimps [pexp_Suc,pmult_Cons]) 2);
  6.1074 +by Auto_tac;
  6.1075 +qed "poly_squarefree_decomp_order";
  6.1076 +
  6.1077 +
  6.1078 +Goal "[| poly (pderiv p) ~= poly []; \
  6.1079 +\        poly p = poly (q *** d); \
  6.1080 +\        poly (pderiv p) = poly (e *** d); \
  6.1081 +\        poly d = poly (r *** p +++ s *** pderiv p) \
  6.1082 +\     |] ==> ALL a. order a q = (if order a p = 0 then 0 else 1)";
  6.1083 +by (blast_tac (claset() addIs [poly_squarefree_decomp_order]) 1);
  6.1084 +qed "poly_squarefree_decomp_order2";
  6.1085 +
  6.1086 +Goal "poly p ~= poly [] ==> (poly p a = 0) = (order a p ~= 0)";
  6.1087 +by (rtac (order_root RS ssubst) 1);
  6.1088 +by Auto_tac;
  6.1089 +qed "order_root2";
  6.1090 +
  6.1091 +Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \
  6.1092 +\     ==> (order a (pderiv p) = n) = (order a p = Suc n)";
  6.1093 +by (auto_tac (claset() addDs [order_pderiv],simpset()));
  6.1094 +qed "order_pderiv2";
  6.1095 +
  6.1096 +Goalw [rsquarefree_def]
  6.1097 +  "rsquarefree p = (ALL a. ~(poly p a = 0 & poly (pderiv p) a = 0))";
  6.1098 +by (case_tac "poly p = poly []" 1);
  6.1099 +by (Asm_full_simp_tac 1);
  6.1100 +by (Asm_full_simp_tac 1);
  6.1101 +by (case_tac "poly (pderiv p) = poly []" 1);
  6.1102 +by (Asm_full_simp_tac 1);
  6.1103 +by (dtac pderiv_iszero 1 THEN Clarify_tac 1);
  6.1104 +by (subgoal_tac "ALL a. order a p = order a [h]" 1);
  6.1105 +by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
  6.1106 +by (rtac allI 1);
  6.1107 +by (cut_inst_tac [("p","[h]"),("a","a")] order_root 1);
  6.1108 +by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
  6.1109 +by (blast_tac (claset() addIs [order_poly]) 1);
  6.1110 +by (auto_tac (claset(),simpset() addsimps [order_root,order_pderiv2]));
  6.1111 +by (dtac spec 1 THEN Auto_tac);
  6.1112 +qed "rsquarefree_roots";
  6.1113 +
  6.1114 +Goal "[1] *** p = p";
  6.1115 +by Auto_tac;
  6.1116 +qed "pmult_one";
  6.1117 +Addsimps [pmult_one];
  6.1118 +
  6.1119 +Goal "poly [] = poly [0]";
  6.1120 +by (simp_tac (simpset() addsimps [fun_eq]) 1);
  6.1121 +qed "poly_Nil_zero";
  6.1122 +
  6.1123 +Goalw [rsquarefree_def]
  6.1124 +     "[| rsquarefree p; poly p a = 0 |] \
  6.1125 +\     ==> EX q. (poly p = poly ([-a, 1] *** q)) & poly q a ~= 0";
  6.1126 +by (Step_tac 1);
  6.1127 +by (forw_inst_tac [("a","a")] order_decomp 1);
  6.1128 +by (dres_inst_tac [("x","a")] spec 1);
  6.1129 +by (dres_inst_tac [("a1","a")] (order_root2 RS sym) 1);
  6.1130 +by (auto_tac (claset(),simpset() delsimps [pmult_Cons]));
  6.1131 +by (res_inst_tac [("x","q")] exI 1 THEN Step_tac 1);
  6.1132 +by (asm_full_simp_tac (simpset() addsimps [poly_mult,fun_eq]) 1);
  6.1133 +by (dres_inst_tac [("p1","q")] (poly_linear_divides RS iffD1) 1);
  6.1134 +by (asm_full_simp_tac (simpset() addsimps [divides_def]
  6.1135 +    delsimps [pmult_Cons]) 1);
  6.1136 +by (Step_tac 1);
  6.1137 +by (dres_inst_tac [("x","[]")] spec 1); 
  6.1138 +by (auto_tac (claset(),simpset() addsimps [fun_eq]));
  6.1139 +qed "rsquarefree_decomp";
  6.1140 +
  6.1141 +Goal "[| poly (pderiv p) ~= poly []; \
  6.1142 +\        poly p = poly (q *** d); \
  6.1143 +\        poly (pderiv p) = poly (e *** d); \
  6.1144 +\        poly d = poly (r *** p +++ s *** pderiv p) \
  6.1145 +\     |] ==> rsquarefree q & (ALL a. (poly q a = 0) = (poly p a = 0))";
  6.1146 +by (ftac poly_squarefree_decomp_order2 1);
  6.1147 +by (TRYALL(assume_tac));
  6.1148 +by (case_tac "poly p = poly []" 1);
  6.1149 +by (blast_tac (claset() addDs [pderiv_zero]) 1);
  6.1150 +by (simp_tac (simpset() addsimps [rsquarefree_def,
  6.1151 +    order_root] delsimps [pmult_Cons]) 1);
  6.1152 +by (asm_full_simp_tac (simpset() addsimps [poly_entire] 
  6.1153 +    delsimps [pmult_Cons]) 1);
  6.1154 +qed "poly_squarefree_decomp";
  6.1155 +
  6.1156 +
  6.1157 +(* ------------------------------------------------------------------------- *)
  6.1158 +(* Normalization of a polynomial.                                            *)
  6.1159 +(* ------------------------------------------------------------------------- *)
  6.1160 +
  6.1161 +Goal "poly (pnormalize p) = poly p";
  6.1162 +by (induct_tac "p" 1);
  6.1163 +by (auto_tac (claset(),simpset() addsimps [fun_eq]));
  6.1164 +qed "poly_normalize";
  6.1165 +Addsimps [poly_normalize];
  6.1166 +
  6.1167 +
  6.1168 +(* ------------------------------------------------------------------------- *)
  6.1169 +(* The degree of a polynomial.                                               *)
  6.1170 +(* ------------------------------------------------------------------------- *)
  6.1171 +
  6.1172 +Goal "list_all (%c. c = 0) p -->  pnormalize p = []";
  6.1173 +by (induct_tac "p" 1);
  6.1174 +by Auto_tac;
  6.1175 +qed_spec_mp "lemma_degree_zero";
  6.1176 +
  6.1177 +Goalw [degree_def] "poly p = poly [] ==> degree p = 0";
  6.1178 +by (case_tac "pnormalize p = []" 1);
  6.1179 +by (auto_tac (claset() addDs [lemma_degree_zero],simpset() 
  6.1180 +    addsimps [poly_zero]));
  6.1181 +qed "degree_zero";
  6.1182 +
  6.1183 +(* ------------------------------------------------------------------------- *)
  6.1184 +(* Tidier versions of finiteness of roots.                                   *)
  6.1185 +(* ------------------------------------------------------------------------- *)
  6.1186 +
  6.1187 +Goal "poly p ~= poly [] ==> finite {x. poly p x = 0}";
  6.1188 +by (auto_tac (claset(),simpset() addsimps [poly_roots_finite]));
  6.1189 +by (res_inst_tac [("B","{x::real. EX n. (n::nat) < N & (x = j n)}")] 
  6.1190 +    finite_subset 1);
  6.1191 +by (induct_tac "N" 2);
  6.1192 +by Auto_tac;
  6.1193 +by (subgoal_tac "{x::real. EX na. na < Suc n & (x = j na)} = \
  6.1194 +\                 {(j n)} Un {x. EX na. na < n & (x = j na)}" 1);
  6.1195 +by (auto_tac (claset(),simpset() addsimps [ARITH_PROVE 
  6.1196 +    "(na < Suc n) = (na = n | na < n)"]));
  6.1197 +qed "poly_roots_finite_set";
  6.1198 +
  6.1199 +(* ------------------------------------------------------------------------- *)
  6.1200 +(* bound for polynomial.                                                     *)
  6.1201 +(* ------------------------------------------------------------------------- *)
  6.1202 +
  6.1203 +Goal "abs(x) <= k --> abs(poly p x) <= poly (map abs p) k";
  6.1204 +by (induct_tac "p" 1);
  6.1205 +by Auto_tac;
  6.1206 +by (res_inst_tac [("j","abs a + abs(x * poly list x)")] real_le_trans 1);
  6.1207 +by (rtac abs_triangle_ineq 1);
  6.1208 +by (auto_tac (claset() addSIs [real_mult_le_mono],simpset() 
  6.1209 +    addsimps [abs_mult]));
  6.1210 +by (arith_tac 1);
  6.1211 +qed_spec_mp "poly_mono"; 
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Hyperreal/Poly.thy	Fri Nov 16 18:24:11 2001 +0100
     7.3 @@ -0,0 +1,121 @@
     7.4 +(*  Title:       Poly.thy
     7.5 +    Author:      Jacques D. Fleuriot
     7.6 +    Copyright:   2000 University of Edinburgh
     7.7 +    Description: Properties of univariate real polynomials (cf. Harrison)
     7.8 +*)
     7.9 +
    7.10 +Poly = Transcendental + 
    7.11 +
    7.12 +(* ------------------------------------------------------------------------- *)
    7.13 +(* Application of polynomial as a real function.                             *)
    7.14 +(* ------------------------------------------------------------------------- *)
    7.15 +
    7.16 +consts poly :: real list => real => real
    7.17 +primrec
    7.18 +  poly_Nil  "poly [] x = 0"
    7.19 +  poly_Cons "poly (h#t) x = h + x * poly t x"
    7.20 +
    7.21 +
    7.22 +(* ------------------------------------------------------------------------- *)
    7.23 +(* Arithmetic operations on polynomials.                                     *)
    7.24 +(* ------------------------------------------------------------------------- *)
    7.25 +
    7.26 +(* addition *)
    7.27 +consts "+++" :: [real list, real list] => real list  (infixl 65)
    7.28 +primrec
    7.29 +  padd_Nil  "[] +++ l2 = l2"
    7.30 +  padd_Cons "(h#t) +++ l2 = (if l2 = [] then h#t 
    7.31 +                            else (h + hd l2)#(t +++ tl l2))"
    7.32 +
    7.33 +(* Multiplication by a constant *)
    7.34 +consts "%*" :: [real, real list] => real list  (infixl 70)
    7.35 +primrec
    7.36 +   cmult_Nil  "c %* [] = []"
    7.37 +   cmult_Cons "c %* (h#t) = (c * h)#(c %* t)"
    7.38 +
    7.39 +(* Multiplication by a polynomial *)
    7.40 +consts "***" :: [real list, real list] => real list  (infixl 70)
    7.41 +primrec
    7.42 +   pmult_Nil  "[] *** l2 = []"
    7.43 +   pmult_Cons "(h#t) *** l2 = (if t = [] then h %* l2 
    7.44 +                              else (h %* l2) +++ ((0) # (t *** l2)))"
    7.45 +
    7.46 +(* Repeated multiplication by a polynomial *)
    7.47 +consts mulexp :: [nat, real list, real list] => real list
    7.48 +primrec
    7.49 +   mulexp_zero "mulexp 0 p q = q"
    7.50 +   mulexp_Suc  "mulexp (Suc n) p q = p *** mulexp n p q"
    7.51 +  
    7.52 +  
    7.53 +(* Exponential *)
    7.54 +consts "%^" :: [real list, nat] => real list  (infixl 80)
    7.55 +primrec
    7.56 +   pexp_0   "p %^ 0 = [1]"
    7.57 +   pexp_Suc "p %^ (Suc n) = p *** (p %^ n)"
    7.58 +
    7.59 +(* Quotient related value of dividing a polynomial by x + a *)
    7.60 +(* Useful for divisor properties in inductive proofs *)
    7.61 +consts "pquot" :: [real list, real] => real list
    7.62 +primrec
    7.63 +   pquot_Nil  "pquot [] a= []"
    7.64 +   pquot_Cons "pquot (h#t) a = (if t = [] then [h]
    7.65 +                   else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
    7.66 +
    7.67 +(* ------------------------------------------------------------------------- *)
    7.68 +(* Differentiation of polynomials (needs an auxiliary function).             *)
    7.69 +(* ------------------------------------------------------------------------- *)
    7.70 +consts pderiv_aux :: nat => real list => real list
    7.71 +primrec
    7.72 +   pderiv_aux_Nil  "pderiv_aux n [] = []"
    7.73 +   pderiv_aux_Cons "pderiv_aux n (h#t) =
    7.74 +                     (real n * h)#(pderiv_aux (Suc n) t)"
    7.75 +
    7.76 +(* ------------------------------------------------------------------------- *)
    7.77 +(* normalization of polynomials (remove extra 0 coeff)                       *)
    7.78 +(* ------------------------------------------------------------------------- *)
    7.79 +consts pnormalize :: real list => real list
    7.80 +primrec 
    7.81 +   pnormalize_Nil  "pnormalize [] = []"
    7.82 +   pnormalize_Cons "pnormalize (h#p) = (if ( (pnormalize p) = [])
    7.83 +                                     then (if (h = 0) then [] else [h]) 
    7.84 +                                     else (h#(pnormalize p)))"
    7.85 +
    7.86 +
    7.87 +(* ------------------------------------------------------------------------- *)
    7.88 +(* Other definitions                                                         *)
    7.89 +(* ------------------------------------------------------------------------- *)
    7.90 +
    7.91 +constdefs
    7.92 +   poly_minus :: real list => real list      ("-- _" [80] 80)
    7.93 +   "-- p == (- 1) %* p"
    7.94 +
    7.95 +   pderiv :: real list => real list
    7.96 +   "pderiv p == if p = [] then [] else pderiv_aux 1 (tl p)"
    7.97 +
    7.98 +   divides :: [real list,real list] => bool (infixl 70)
    7.99 +   "p1 divides p2 == EX q. poly p2 = poly(p1 *** q)"
   7.100 +
   7.101 +(* ------------------------------------------------------------------------- *)
   7.102 +(* Definition of order.                                                      *)
   7.103 +(* ------------------------------------------------------------------------- *)
   7.104 +
   7.105 +   order :: real => real list => nat
   7.106 +   "order a p == (@n. ([-a, 1] %^ n) divides p &
   7.107 +                      ~ (([-a, 1] %^ (Suc n)) divides p))"
   7.108 +
   7.109 +(* ------------------------------------------------------------------------- *)
   7.110 +(* Definition of degree.                                                     *)
   7.111 +(* ------------------------------------------------------------------------- *)
   7.112 +
   7.113 +   degree :: real list => nat
   7.114 +   "degree p == length (pnormalize p)"
   7.115 +  
   7.116 +(* ------------------------------------------------------------------------- *)
   7.117 +(* Define being "squarefree" --- NB with respect to real roots only.         *)
   7.118 +(* ------------------------------------------------------------------------- *)
   7.119 +
   7.120 +   rsquarefree :: real list => bool
   7.121 +   "rsquarefree p == poly p ~= poly [] &
   7.122 +                     (ALL a. (order a p = 0) | (order a p = 1))"
   7.123 +
   7.124 +end
     8.1 --- a/src/HOL/Hyperreal/Series.ML	Fri Nov 16 15:25:17 2001 +0100
     8.2 +++ b/src/HOL/Hyperreal/Series.ML	Fri Nov 16 18:24:11 2001 +0100
     8.3 @@ -52,6 +52,17 @@
     8.4  by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
     8.5  qed "sumr_split_add_minus";
     8.6  
     8.7 +Goal "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f";
     8.8 +by (induct_tac "p" 1);
     8.9 +by (auto_tac (claset() addSDs [CLAIM "[| m < Suc n; n <= m |] ==> m = n"],
    8.10 +    simpset()));
    8.11 +qed_spec_mp "sumr_split_add2";
    8.12 +
    8.13 +Goal "[| 0<n; n <= p |] ==> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f";
    8.14 +by (dtac le_imp_less_or_eq 1 THEN Auto_tac);
    8.15 +by (blast_tac (claset() addIs [sumr_split_add2]) 1);
    8.16 +qed "sumr_split_add3";
    8.17 +
    8.18  Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))";
    8.19  by (induct_tac "n" 1);
    8.20  by (auto_tac (claset() addIs [abs_triangle_ineq RS order_trans,
    8.21 @@ -588,4 +599,4 @@
    8.22  \     --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)";
    8.23  by (induct_tac "n" 1);
    8.24  by (auto_tac (claset() addIs [DERIV_add], simpset()));
    8.25 -qed "DERIV_sumr";
    8.26 +qed_spec_mp "DERIV_sumr";
     9.1 --- a/src/HOL/IsaMakefile	Fri Nov 16 15:25:17 2001 +0100
     9.2 +++ b/src/HOL/IsaMakefile	Fri Nov 16 18:24:11 2001 +0100
     9.3 @@ -140,10 +140,13 @@
     9.4    Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy Hyperreal/HyperDef.ML\
     9.5    Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
     9.6    Hyperreal/HyperOrd.ML Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
     9.7 -  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy Hyperreal/Lim.ML\
     9.8 -  Hyperreal/Lim.thy Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
     9.9 +  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
    9.10 +  Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
    9.11 +  Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\
    9.12 +  Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
    9.13    Hyperreal/NSA.ML Hyperreal/NSA.thy\
    9.14    Hyperreal/NthRoot.ML Hyperreal/NthRoot.thy\
    9.15 +  Hyperreal/Poly.ML Hyperreal/Poly.thy\
    9.16    Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\
    9.17    Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\
    9.18    Hyperreal/Transcendental.thy Hyperreal/Zorn.ML Hyperreal/Zorn.thy\