1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Hyperreal/MacLaurin_lemmas.ML Tue May 11 20:11:08 2004 +0200
1.3 @@ -0,0 +1,672 @@
1.4 +(* Title : MacLaurin.thy
1.5 + Author : Jacques D. Fleuriot
1.6 + Copyright : 2001 University of Edinburgh
1.7 + Description : MacLaurin series
1.8 +*)
1.9 +
1.10 +Goal "sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";
1.11 +by (induct_tac "n" 1);
1.12 +by Auto_tac;
1.13 +qed "sumr_offset";
1.14 +
1.15 +Goal "ALL f. sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";
1.16 +by (induct_tac "n" 1);
1.17 +by Auto_tac;
1.18 +qed "sumr_offset2";
1.19 +
1.20 +Goal "sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";
1.21 +by (simp_tac (simpset() addsimps [sumr_offset]) 1);
1.22 +qed "sumr_offset3";
1.23 +
1.24 +Goal "ALL n f. sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";
1.25 +by (simp_tac (simpset() addsimps [sumr_offset]) 1);
1.26 +qed "sumr_offset4";
1.27 +
1.28 +Goal "0 < n ==> \
1.29 +\ sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else \
1.30 +\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = \
1.31 +\ sumr 0 (Suc n) (%n. (if even(n) then 0 else \
1.32 +\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)";
1.33 +by (res_inst_tac [("n1","1")] (sumr_split_add RS subst) 1);
1.34 +by Auto_tac;
1.35 +qed "sumr_from_1_from_0";
1.36 +
1.37 +(*---------------------------------------------------------------------------*)
1.38 +(* Maclaurin's theorem with Lagrange form of remainder *)
1.39 +(*---------------------------------------------------------------------------*)
1.40 +
1.41 +(* Annoying: Proof is now even longer due mostly to
1.42 + change in behaviour of simplifier since Isabelle99 *)
1.43 +Goal " [| 0 < h; 0 < n; diff 0 = f; \
1.44 +\ ALL m t. \
1.45 +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \
1.46 +\ ==> EX t. 0 < t & \
1.47 +\ t < h & \
1.48 +\ f h = \
1.49 +\ sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + \
1.50 +\ (diff n t / real (fact n)) * h ^ n";
1.51 +by (case_tac "n = 0" 1);
1.52 +by (Force_tac 1);
1.53 +by (dtac not0_implies_Suc 1);
1.54 +by (etac exE 1);
1.55 +by (subgoal_tac
1.56 + "EX B. f h = sumr 0 n (%m. (diff m 0 / real (fact m)) * (h ^ m)) \
1.57 +\ + (B * ((h ^ n) / real (fact n)))" 1);
1.58 +
1.59 +by (simp_tac (HOL_ss addsimps [real_add_commute, real_divide_def,
1.60 + ARITH_PROVE "(x = z + (y::real)) = (x - y = z)"]) 2);
1.61 +by (res_inst_tac
1.62 + [("x","(f(h) - sumr 0 n (%m. (diff(m)(0) / real (fact m)) * (h ^ m))) \
1.63 +\ * real (fact n) / (h ^ n)")] exI 2);
1.64 +by (simp_tac (HOL_ss addsimps [real_mult_assoc,real_divide_def]) 2);
1.65 + by (rtac (CLAIM "x = (1::real) ==> a = a * (x::real)") 2);
1.66 +by (asm_simp_tac (HOL_ss addsimps
1.67 + [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"]
1.68 + delsimps [realpow_Suc]) 2);
1.69 +by (stac left_inverse 2);
1.70 +by (stac left_inverse 3);
1.71 +by (rtac (real_not_refl2 RS not_sym) 2);
1.72 +by (etac zero_less_power 2);
1.73 +by (rtac real_of_nat_fact_not_zero 2);
1.74 +by (Simp_tac 2);
1.75 +by (etac exE 1);
1.76 +by (cut_inst_tac [("b","%t. f t - \
1.77 +\ (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \
1.78 +\ (B * ((t ^ n) / real (fact n))))")]
1.79 + (CLAIM "EX g. g = b") 1);
1.80 +by (etac exE 1);
1.81 +by (subgoal_tac "g 0 = 0 & g h =0" 1);
1.82 +by (asm_simp_tac (simpset() addsimps
1.83 + [ARITH_PROVE "(x - y = z) = (x = z + (y::real))"]
1.84 + delsimps [sumr_Suc]) 2);
1.85 +by (cut_inst_tac [("n","m"),("k","1")] sumr_offset2 2);
1.86 +by (asm_full_simp_tac (simpset() addsimps
1.87 + [ARITH_PROVE "(x = y - z) = (y = x + (z::real))"]
1.88 + delsimps [sumr_Suc]) 2);
1.89 +by (cut_inst_tac [("b","%m t. diff m t - \
1.90 +\ (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) \
1.91 +\ + (B * ((t ^ (n - m)) / real (fact(n - m)))))")]
1.92 + (CLAIM "EX difg. difg = b") 1);
1.93 +by (etac exE 1);
1.94 +by (subgoal_tac "difg 0 = g" 1);
1.95 +by (asm_simp_tac (simpset() delsimps [realpow_Suc,fact_Suc]) 2);
1.96 +by (subgoal_tac "ALL m t. m < n & 0 <= t & t <= h --> \
1.97 +\ DERIV (difg m) t :> difg (Suc m) t" 1);
1.98 +by (Clarify_tac 2);
1.99 +by (rtac DERIV_diff 2);
1.100 +by (Asm_simp_tac 2);
1.101 +by DERIV_tac;
1.102 +by DERIV_tac;
1.103 +by (rtac lemma_DERIV_subst 3);
1.104 +by (rtac DERIV_quotient 3);
1.105 +by (rtac DERIV_const 4);
1.106 +by (rtac DERIV_pow 3);
1.107 +by (asm_simp_tac (simpset() addsimps [inverse_mult_distrib,
1.108 + CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e"
1.109 + mult_ac,fact_diff_Suc]) 4);
1.110 +by (Asm_simp_tac 3);
1.111 +by (forw_inst_tac [("m","ma")] less_add_one 2);
1.112 +by (Clarify_tac 2);
1.113 +by (asm_simp_tac (simpset() addsimps
1.114 + [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"]
1.115 + delsimps [sumr_Suc]) 2);
1.116 +by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])
1.117 + (read_instantiate [("k","1")] sumr_offset4))]
1.118 + delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
1.119 +by (rtac lemma_DERIV_subst 2);
1.120 +by (rtac DERIV_add 2);
1.121 +by (rtac DERIV_const 3);
1.122 +by (rtac DERIV_sumr 2);
1.123 +by (Clarify_tac 2);
1.124 +by (Simp_tac 3);
1.125 +by (simp_tac (simpset() addsimps [real_divide_def,real_mult_assoc]
1.126 + delsimps [fact_Suc,realpow_Suc]) 2);
1.127 +by (rtac DERIV_cmult 2);
1.128 +by (rtac lemma_DERIV_subst 2);
1.129 +by DERIV_tac;
1.130 +by (stac fact_Suc 2);
1.131 +by (stac real_of_nat_mult 2);
1.132 +by (simp_tac (simpset() addsimps [inverse_mult_distrib] @
1.133 + mult_ac) 2);
1.134 +by (subgoal_tac "ALL ma. ma < n --> \
1.135 +\ (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1);
1.136 +by (rotate_tac 11 1);
1.137 +by (dres_inst_tac [("x","m")] spec 1);
1.138 +by (etac impE 1);
1.139 +by (Asm_simp_tac 1);
1.140 +by (etac exE 1);
1.141 +by (res_inst_tac [("x","t")] exI 1);
1.142 +by (asm_full_simp_tac (simpset() addsimps
1.143 + [ARITH_PROVE "(x - y = 0) = (y = (x::real))"]
1.144 + delsimps [realpow_Suc,fact_Suc]) 1);
1.145 +by (subgoal_tac "ALL m. m < n --> difg m 0 = 0" 1);
1.146 +by (Clarify_tac 2);
1.147 +by (Asm_simp_tac 2);
1.148 +by (forw_inst_tac [("m","ma")] less_add_one 2);
1.149 +by (Clarify_tac 2);
1.150 +by (asm_simp_tac (simpset() delsimps [sumr_Suc]) 2);
1.151 +by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])
1.152 + (read_instantiate [("k","1")] sumr_offset4))]
1.153 + delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
1.154 +by (subgoal_tac "ALL m. m < n --> (EX t. 0 < t & t < h & \
1.155 +\ DERIV (difg m) t :> 0)" 1);
1.156 +by (rtac allI 1 THEN rtac impI 1);
1.157 +by (rotate_tac 12 1);
1.158 +by (dres_inst_tac [("x","ma")] spec 1);
1.159 +by (etac impE 1 THEN assume_tac 1);
1.160 +by (etac exE 1);
1.161 +by (res_inst_tac [("x","t")] exI 1);
1.162 +(* do some tidying up *)
1.163 +by (ALLGOALS(thin_tac "difg = \
1.164 +\ (%m t. diff m t - \
1.165 +\ (sumr 0 (n - m) \
1.166 +\ (%p. diff (m + p) 0 / real (fact p) * t ^ p) + \
1.167 +\ B * (t ^ (n - m) / real (fact (n - m)))))"));
1.168 +by (ALLGOALS(thin_tac "g = \
1.169 +\ (%t. f t - \
1.170 +\ (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + \
1.171 +\ B * (t ^ n / real (fact n))))"));
1.172 +by (ALLGOALS(thin_tac "f h = \
1.173 +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
1.174 +\ B * (h ^ n / real (fact n))"));
1.175 +(* back to business *)
1.176 +by (Asm_simp_tac 1);
1.177 +by (rtac DERIV_unique 1);
1.178 +by (Blast_tac 2);
1.179 +by (Force_tac 1);
1.180 +by (rtac allI 1 THEN induct_tac "ma" 1);
1.181 +by (rtac impI 1 THEN rtac Rolle 1);
1.182 +by (assume_tac 1);
1.183 +by (Asm_full_simp_tac 1);
1.184 +by (Asm_full_simp_tac 1);
1.185 +by (subgoal_tac "ALL t. 0 <= t & t <= h --> g differentiable t" 1);
1.186 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
1.187 +by (blast_tac (claset() addDs [DERIV_isCont]) 1);
1.188 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
1.189 +by (Clarify_tac 1);
1.190 +by (res_inst_tac [("x","difg (Suc 0) t")] exI 1);
1.191 +by (Force_tac 1);
1.192 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
1.193 +by (Clarify_tac 1);
1.194 +by (res_inst_tac [("x","difg (Suc 0) x")] exI 1);
1.195 +by (Force_tac 1);
1.196 +by (Step_tac 1);
1.197 +by (Force_tac 1);
1.198 +by (subgoal_tac "EX ta. 0 < ta & ta < t & \
1.199 +\ DERIV difg (Suc n) ta :> 0" 1);
1.200 +by (rtac Rolle 2 THEN assume_tac 2);
1.201 +by (Asm_full_simp_tac 2);
1.202 +by (rotate_tac 2 2);
1.203 +by (dres_inst_tac [("x","n")] spec 2);
1.204 +by (ftac (ARITH_PROVE "n < m ==> n < Suc m") 2);
1.205 +by (rtac DERIV_unique 2);
1.206 +by (assume_tac 3);
1.207 +by (Force_tac 2);
1.208 +by (subgoal_tac
1.209 + "ALL ta. 0 <= ta & ta <= t --> (difg (Suc n)) differentiable ta" 2);
1.210 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
1.211 +by (blast_tac (claset() addSDs [DERIV_isCont]) 2);
1.212 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
1.213 +by (Clarify_tac 2);
1.214 +by (res_inst_tac [("x","difg (Suc (Suc n)) ta")] exI 2);
1.215 +by (Force_tac 2);
1.216 +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);
1.217 +by (Clarify_tac 2);
1.218 +by (res_inst_tac [("x","difg (Suc (Suc n)) x")] exI 2);
1.219 +by (Force_tac 2);
1.220 +by (Step_tac 1);
1.221 +by (res_inst_tac [("x","ta")] exI 1);
1.222 +by (Force_tac 1);
1.223 +qed "Maclaurin";
1.224 +
1.225 +Goal "0 < h & 0 < n & diff 0 = f & \
1.226 +\ (ALL m t. \
1.227 +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \
1.228 +\ --> (EX t. 0 < t & \
1.229 +\ t < h & \
1.230 +\ f h = \
1.231 +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
1.232 +\ diff n t / real (fact n) * h ^ n)";
1.233 +by (blast_tac (claset() addIs [Maclaurin]) 1);
1.234 +qed "Maclaurin_objl";
1.235 +
1.236 +Goal " [| 0 < h; diff 0 = f; \
1.237 +\ ALL m t. \
1.238 +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \
1.239 +\ ==> EX t. 0 < t & \
1.240 +\ t <= h & \
1.241 +\ f h = \
1.242 +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
1.243 +\ diff n t / real (fact n) * h ^ n";
1.244 +by (case_tac "n" 1);
1.245 +by Auto_tac;
1.246 +by (dtac Maclaurin 1 THEN Auto_tac);
1.247 +qed "Maclaurin2";
1.248 +
1.249 +Goal "0 < h & diff 0 = f & \
1.250 +\ (ALL m t. \
1.251 +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \
1.252 +\ --> (EX t. 0 < t & \
1.253 +\ t <= h & \
1.254 +\ f h = \
1.255 +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
1.256 +\ diff n t / real (fact n) * h ^ n)";
1.257 +by (blast_tac (claset() addIs [Maclaurin2]) 1);
1.258 +qed "Maclaurin2_objl";
1.259 +
1.260 +Goal " [| h < 0; 0 < n; diff 0 = f; \
1.261 +\ ALL m t. \
1.262 +\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t |] \
1.263 +\ ==> EX t. h < t & \
1.264 +\ t < 0 & \
1.265 +\ f h = \
1.266 +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
1.267 +\ diff n t / real (fact n) * h ^ n";
1.268 +by (cut_inst_tac [("f","%x. f (-x)"),
1.269 + ("diff","%n x. ((- 1) ^ n) * diff n (-x)"),
1.270 + ("h","-h"),("n","n")] Maclaurin_objl 1);
1.271 +by (Asm_full_simp_tac 1);
1.272 +by (etac impE 1 THEN Step_tac 1);
1.273 +by (stac minus_mult_right 1);
1.274 +by (rtac DERIV_cmult 1);
1.275 +by (rtac lemma_DERIV_subst 1);
1.276 +by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1);
1.277 +by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2);
1.278 +by (Force_tac 2);
1.279 +by (Force_tac 1);
1.280 +by (res_inst_tac [("x","-t")] exI 1);
1.281 +by Auto_tac;
1.282 +by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1);
1.283 +by (rtac sumr_fun_eq 1);
1.284 +by (Asm_full_simp_tac 1);
1.285 +by (auto_tac (claset(),simpset() addsimps [real_divide_def,
1.286 + CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))",
1.287 + power_mult_distrib RS sym]));
1.288 +qed "Maclaurin_minus";
1.289 +
1.290 +Goal "(h < 0 & 0 < n & diff 0 = f & \
1.291 +\ (ALL m t. \
1.292 +\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\
1.293 +\ --> (EX t. h < t & \
1.294 +\ t < 0 & \
1.295 +\ f h = \
1.296 +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \
1.297 +\ diff n t / real (fact n) * h ^ n)";
1.298 +by (blast_tac (claset() addIs [Maclaurin_minus]) 1);
1.299 +qed "Maclaurin_minus_objl";
1.300 +
1.301 +(* ------------------------------------------------------------------------- *)
1.302 +(* More convenient "bidirectional" version. *)
1.303 +(* ------------------------------------------------------------------------- *)
1.304 +
1.305 +(* not good for PVS sin_approx, cos_approx *)
1.306 +Goal " [| diff 0 = f; \
1.307 +\ ALL m t. \
1.308 +\ m < n & abs t <= abs x --> DERIV (diff m) t :> diff (Suc m) t |] \
1.309 +\ ==> EX t. abs t <= abs x & \
1.310 +\ f x = \
1.311 +\ sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + \
1.312 +\ diff n t / real (fact n) * x ^ n";
1.313 +by (case_tac "n = 0" 1);
1.314 +by (Force_tac 1);
1.315 +by (case_tac "x = 0" 1);
1.316 +by (res_inst_tac [("x","0")] exI 1);
1.317 +by (Asm_full_simp_tac 1);
1.318 +by (res_inst_tac [("P","0 < n")] impE 1);
1.319 +by (assume_tac 2 THEN assume_tac 2);
1.320 +by (induct_tac "n" 1);
1.321 +by (Simp_tac 1);
1.322 +by Auto_tac;
1.323 +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
1.324 +by Auto_tac;
1.325 +by (cut_inst_tac [("f","diff 0"),
1.326 + ("diff","diff"),
1.327 + ("h","x"),("n","n")] Maclaurin_objl 2);
1.328 +by (Step_tac 2);
1.329 +by (blast_tac (claset() addDs
1.330 + [ARITH_PROVE "[|(0::real) <= t;t <= x |] ==> abs t <= abs x"]) 2);
1.331 +by (res_inst_tac [("x","t")] exI 2);
1.332 +by (force_tac (claset() addIs
1.333 + [ARITH_PROVE "[| 0 < t; (t::real) < x|] ==> abs t <= abs x"],simpset()) 2);
1.334 +by (cut_inst_tac [("f","diff 0"),
1.335 + ("diff","diff"),
1.336 + ("h","x"),("n","n")] Maclaurin_minus_objl 1);
1.337 +by (Step_tac 1);
1.338 +by (blast_tac (claset() addDs
1.339 + [ARITH_PROVE "[|x <= t;t <= (0::real) |] ==> abs t <= abs x"]) 1);
1.340 +by (res_inst_tac [("x","t")] exI 1);
1.341 +by (force_tac (claset() addIs
1.342 + [ARITH_PROVE "[| x < t; (t::real) < 0|] ==> abs t <= abs x"],simpset()) 1);
1.343 +qed "Maclaurin_bi_le";
1.344 +
1.345 +Goal "[| diff 0 = f; \
1.346 +\ ALL m x. DERIV (diff m) x :> diff(Suc m) x; \
1.347 +\ x ~= 0; 0 < n \
1.348 +\ |] ==> EX t. 0 < abs t & abs t < abs x & \
1.349 +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
1.350 +\ (diff n t / real (fact n)) * x ^ n";
1.351 +by (res_inst_tac [("x","x"),("y","0")] linorder_cases 1);
1.352 +by (Blast_tac 2);
1.353 +by (dtac Maclaurin_minus 1);
1.354 +by (dtac Maclaurin 5);
1.355 +by (TRYALL(assume_tac));
1.356 +by (Blast_tac 1);
1.357 +by (Blast_tac 2);
1.358 +by (Step_tac 1);
1.359 +by (ALLGOALS(res_inst_tac [("x","t")] exI));
1.360 +by (Step_tac 1);
1.361 +by (ALLGOALS(arith_tac));
1.362 +qed "Maclaurin_all_lt";
1.363 +
1.364 +Goal "diff 0 = f & \
1.365 +\ (ALL m x. DERIV (diff m) x :> diff(Suc m) x) & \
1.366 +\ x ~= 0 & 0 < n \
1.367 +\ --> (EX t. 0 < abs t & abs t < abs x & \
1.368 +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
1.369 +\ (diff n t / real (fact n)) * x ^ n)";
1.370 +by (blast_tac (claset() addIs [Maclaurin_all_lt]) 1);
1.371 +qed "Maclaurin_all_lt_objl";
1.372 +
1.373 +Goal "x = (0::real) \
1.374 +\ ==> 0 < n --> \
1.375 +\ sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = \
1.376 +\ diff 0 0";
1.377 +by (Asm_simp_tac 1);
1.378 +by (induct_tac "n" 1);
1.379 +by Auto_tac;
1.380 +qed_spec_mp "Maclaurin_zero";
1.381 +
1.382 +Goal "[| diff 0 = f; \
1.383 +\ ALL m x. DERIV (diff m) x :> diff (Suc m) x \
1.384 +\ |] ==> EX t. abs t <= abs x & \
1.385 +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
1.386 +\ (diff n t / real (fact n)) * x ^ n";
1.387 +by (cut_inst_tac [("n","n"),("m","0")]
1.388 + (ARITH_PROVE "n <= m | m < (n::nat)") 1);
1.389 +by (etac disjE 1);
1.390 +by (Force_tac 1);
1.391 +by (case_tac "x = 0" 1);
1.392 +by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_zero 1);
1.393 +by (assume_tac 1);
1.394 +by (dtac (gr_implies_not0 RS not0_implies_Suc) 1);
1.395 +by (res_inst_tac [("x","0")] exI 1);
1.396 +by (Force_tac 1);
1.397 +by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_all_lt 1);
1.398 +by (TRYALL(assume_tac));
1.399 +by (Step_tac 1);
1.400 +by (res_inst_tac [("x","t")] exI 1);
1.401 +by Auto_tac;
1.402 +qed "Maclaurin_all_le";
1.403 +
1.404 +Goal "diff 0 = f & \
1.405 +\ (ALL m x. DERIV (diff m) x :> diff (Suc m) x) \
1.406 +\ --> (EX t. abs t <= abs x & \
1.407 +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \
1.408 +\ (diff n t / real (fact n)) * x ^ n)";
1.409 +by (blast_tac (claset() addIs [Maclaurin_all_le]) 1);
1.410 +qed "Maclaurin_all_le_objl";
1.411 +
1.412 +(* ------------------------------------------------------------------------- *)
1.413 +(* Version for exp. *)
1.414 +(* ------------------------------------------------------------------------- *)
1.415 +
1.416 +Goal "[| x ~= 0; 0 < n |] \
1.417 +\ ==> (EX t. 0 < abs t & \
1.418 +\ abs t < abs x & \
1.419 +\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \
1.420 +\ (exp t / real (fact n)) * x ^ n)";
1.421 +by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")]
1.422 + Maclaurin_all_lt_objl 1);
1.423 +by Auto_tac;
1.424 +qed "Maclaurin_exp_lt";
1.425 +
1.426 +Goal "EX t. abs t <= abs x & \
1.427 +\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \
1.428 +\ (exp t / real (fact n)) * x ^ n";
1.429 +by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")]
1.430 + Maclaurin_all_le_objl 1);
1.431 +by Auto_tac;
1.432 +qed "Maclaurin_exp_le";
1.433 +
1.434 +(* ------------------------------------------------------------------------- *)
1.435 +(* Version for sin function *)
1.436 +(* ------------------------------------------------------------------------- *)
1.437 +
1.438 +Goal "[| a < b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \
1.439 +\ ==> EX z. a < z & z < b & (f b - f a = (b - a) * f'(z))";
1.440 +by (dtac MVT 1);
1.441 +by (blast_tac (claset() addIs [DERIV_isCont]) 1);
1.442 +by (force_tac (claset() addDs [order_less_imp_le],
1.443 + simpset() addsimps [differentiable_def]) 1);
1.444 +by (blast_tac (claset() addDs [DERIV_unique,order_less_imp_le]) 1);
1.445 +qed "MVT2";
1.446 +
1.447 +Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3";
1.448 +by (case_tac "d" 1 THEN Auto_tac);
1.449 +qed "lemma_exhaust_less_4";
1.450 +
1.451 +bind_thm ("real_mult_le_lemma",
1.452 + simplify (simpset()) (inst "b" "1" mult_right_mono));
1.453 +
1.454 +
1.455 +Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n";
1.456 +by (induct_tac "n" 1);
1.457 +by Auto_tac;
1.458 +qed_spec_mp "Suc_Suc_mult_two_diff_two";
1.459 +Addsimps [Suc_Suc_mult_two_diff_two];
1.460 +
1.461 +Goal "0 < n --> Suc (Suc (4*n - 2)) = 4*n";
1.462 +by (induct_tac "n" 1);
1.463 +by Auto_tac;
1.464 +qed_spec_mp "lemma_Suc_Suc_4n_diff_2";
1.465 +Addsimps [lemma_Suc_Suc_4n_diff_2];
1.466 +
1.467 +Goal "0 < n --> Suc (2 * n - 1) = 2*n";
1.468 +by (induct_tac "n" 1);
1.469 +by Auto_tac;
1.470 +qed_spec_mp "Suc_mult_two_diff_one";
1.471 +Addsimps [Suc_mult_two_diff_one];
1.472 +
1.473 +Goal "EX t. sin x = \
1.474 +\ (sumr 0 n (%m. (if even m then 0 \
1.475 +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
1.476 +\ x ^ m)) \
1.477 +\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
1.478 +by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
1.479 + ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
1.480 + Maclaurin_all_lt_objl 1);
1.481 +by (Safe_tac);
1.482 +by (Simp_tac 1);
1.483 +by (Simp_tac 1);
1.484 +by (case_tac "n" 1);
1.485 +by (Clarify_tac 1);
1.486 +by (Asm_full_simp_tac 1);
1.487 +by (dres_inst_tac [("x","0")] spec 1 THEN Asm_full_simp_tac 1);
1.488 +by (Asm_full_simp_tac 1);
1.489 +by (rtac ccontr 1);
1.490 +by (Asm_full_simp_tac 1);
1.491 +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
1.492 +by (dtac ssubst 1 THEN assume_tac 2);
1.493 +by (res_inst_tac [("x","t")] exI 1);
1.494 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
1.495 +by (rtac sumr_fun_eq 1);
1.496 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
1.497 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
1.498 +(*Could sin_zero_iff help?*)
1.499 +qed "Maclaurin_sin_expansion";
1.500 +
1.501 +Goal "EX t. abs t <= abs x & \
1.502 +\ sin x = \
1.503 +\ (sumr 0 n (%m. (if even m then 0 \
1.504 +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
1.505 +\ x ^ m)) \
1.506 +\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
1.507 +
1.508 +by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
1.509 + ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
1.510 + Maclaurin_all_lt_objl 1);
1.511 +by (Step_tac 1);
1.512 +by (Simp_tac 1);
1.513 +by (Simp_tac 1);
1.514 +by (case_tac "n" 1);
1.515 +by (Clarify_tac 1);
1.516 +by (Asm_full_simp_tac 1);
1.517 +by (Asm_full_simp_tac 1);
1.518 +by (rtac ccontr 1);
1.519 +by (Asm_full_simp_tac 1);
1.520 +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
1.521 +by (dtac ssubst 1 THEN assume_tac 2);
1.522 +by (res_inst_tac [("x","t")] exI 1);
1.523 +by (rtac conjI 1);
1.524 +by (arith_tac 1);
1.525 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
1.526 +by (rtac sumr_fun_eq 1);
1.527 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
1.528 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
1.529 +qed "Maclaurin_sin_expansion2";
1.530 +
1.531 +Goal "[| 0 < n; 0 < x |] ==> \
1.532 +\ EX t. 0 < t & t < x & \
1.533 +\ sin x = \
1.534 +\ (sumr 0 n (%m. (if even m then 0 \
1.535 +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
1.536 +\ x ^ m)) \
1.537 +\ + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)";
1.538 +by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),
1.539 + ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
1.540 + Maclaurin_objl 1);
1.541 +by (Step_tac 1);
1.542 +by (Asm_full_simp_tac 1);
1.543 +by (Simp_tac 1);
1.544 +by (dtac ssubst 1 THEN assume_tac 2);
1.545 +by (res_inst_tac [("x","t")] exI 1);
1.546 +by (rtac conjI 1 THEN rtac conjI 2);
1.547 +by (assume_tac 1 THEN assume_tac 1);
1.548 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
1.549 +by (rtac sumr_fun_eq 1);
1.550 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
1.551 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
1.552 +qed "Maclaurin_sin_expansion3";
1.553 +
1.554 +Goal "0 < x ==> \
1.555 +\ EX t. 0 < t & t <= x & \
1.556 +\ sin x = \
1.557 +\ (sumr 0 n (%m. (if even m then 0 \
1.558 +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \
1.559 +\ x ^ m)) \
1.560 +\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
1.561 +by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),
1.562 + ("diff","%n x. sin(x + 1/2*real (n)*pi)")]
1.563 + Maclaurin2_objl 1);
1.564 +by (Step_tac 1);
1.565 +by (Asm_full_simp_tac 1);
1.566 +by (Simp_tac 1);
1.567 +by (dtac ssubst 1 THEN assume_tac 2);
1.568 +by (res_inst_tac [("x","t")] exI 1);
1.569 +by (rtac conjI 1 THEN rtac conjI 2);
1.570 +by (assume_tac 1 THEN assume_tac 1);
1.571 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
1.572 +by (rtac sumr_fun_eq 1);
1.573 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
1.574 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
1.575 +qed "Maclaurin_sin_expansion4";
1.576 +
1.577 +(*-----------------------------------------------------------------------------*)
1.578 +(* Maclaurin expansion for cos *)
1.579 +(*-----------------------------------------------------------------------------*)
1.580 +
1.581 +Goal "sumr 0 (Suc n) \
1.582 +\ (%m. (if even m \
1.583 +\ then (- 1) ^ (m div 2)/(real (fact m)) \
1.584 +\ else 0) * \
1.585 +\ 0 ^ m) = 1";
1.586 +by (induct_tac "n" 1);
1.587 +by Auto_tac;
1.588 +qed "sumr_cos_zero_one";
1.589 +Addsimps [sumr_cos_zero_one];
1.590 +
1.591 +Goal "EX t. abs t <= abs x & \
1.592 +\ cos x = \
1.593 +\ (sumr 0 n (%m. (if even m \
1.594 +\ then (- 1) ^ (m div 2)/(real (fact m)) \
1.595 +\ else 0) * \
1.596 +\ x ^ m)) \
1.597 +\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
1.598 +by (cut_inst_tac [("f","cos"),("n","n"),("x","x"),
1.599 + ("diff","%n x. cos(x + 1/2*real (n)*pi)")]
1.600 + Maclaurin_all_lt_objl 1);
1.601 +by (Step_tac 1);
1.602 +by (Simp_tac 1);
1.603 +by (Simp_tac 1);
1.604 +by (case_tac "n" 1);
1.605 +by (Asm_full_simp_tac 1);
1.606 +by (asm_full_simp_tac (simpset() delsimps [sumr_Suc]) 1);
1.607 +by (rtac ccontr 1);
1.608 +by (Asm_full_simp_tac 1);
1.609 +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);
1.610 +by (dtac ssubst 1 THEN assume_tac 2);
1.611 +by (res_inst_tac [("x","t")] exI 1);
1.612 +by (rtac conjI 1);
1.613 +by (arith_tac 1);
1.614 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
1.615 +by (rtac sumr_fun_eq 1);
1.616 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
1.617 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps
1.618 + [fact_Suc,realpow_Suc]));
1.619 +by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
1.620 +qed "Maclaurin_cos_expansion";
1.621 +
1.622 +Goal "[| 0 < x; 0 < n |] ==> \
1.623 +\ EX t. 0 < t & t < x & \
1.624 +\ cos x = \
1.625 +\ (sumr 0 n (%m. (if even m \
1.626 +\ then (- 1) ^ (m div 2)/(real (fact m)) \
1.627 +\ else 0) * \
1.628 +\ x ^ m)) \
1.629 +\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
1.630 +by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),
1.631 + ("diff","%n x. cos(x + 1/2*real (n)*pi)")]
1.632 + Maclaurin_objl 1);
1.633 +by (Step_tac 1);
1.634 +by (Asm_full_simp_tac 1);
1.635 +by (Simp_tac 1);
1.636 +by (dtac ssubst 1 THEN assume_tac 2);
1.637 +by (res_inst_tac [("x","t")] exI 1);
1.638 +by (rtac conjI 1 THEN rtac conjI 2);
1.639 +by (assume_tac 1 THEN assume_tac 1);
1.640 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
1.641 +by (rtac sumr_fun_eq 1);
1.642 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
1.643 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc]));
1.644 +by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
1.645 +qed "Maclaurin_cos_expansion2";
1.646 +
1.647 +Goal "[| x < 0; 0 < n |] ==> \
1.648 +\ EX t. x < t & t < 0 & \
1.649 +\ cos x = \
1.650 +\ (sumr 0 n (%m. (if even m \
1.651 +\ then (- 1) ^ (m div 2)/(real (fact m)) \
1.652 +\ else 0) * \
1.653 +\ x ^ m)) \
1.654 +\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";
1.655 +by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),
1.656 + ("diff","%n x. cos(x + 1/2*real (n)*pi)")]
1.657 + Maclaurin_minus_objl 1);
1.658 +by (Step_tac 1);
1.659 +by (Asm_full_simp_tac 1);
1.660 +by (Simp_tac 1);
1.661 +by (dtac ssubst 1 THEN assume_tac 2);
1.662 +by (res_inst_tac [("x","t")] exI 1);
1.663 +by (rtac conjI 1 THEN rtac conjI 2);
1.664 +by (assume_tac 1 THEN assume_tac 1);
1.665 +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
1.666 +by (rtac sumr_fun_eq 1);
1.667 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
1.668 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc]));
1.669 +by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
1.670 +qed "Maclaurin_minus_cos_expansion";
1.671 +
1.672 +(* ------------------------------------------------------------------------- *)
1.673 +(* Version for ln(1 +/- x). Where is it?? *)
1.674 +(* ------------------------------------------------------------------------- *)
1.675 +