wneuper/isa: src/HOL/Hyperreal/MacLaurin

     1 (*  Title       : MacLaurin.thy

     2     Author      : Jacques D. Fleuriot

     3     Copyright   : 2001 University of Edinburgh

     4     Description : MacLaurin series

     5 *)

     7 Goal "sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";

     8 by (induct_tac "n" 1);

     9 by Auto_tac;

    10 qed "sumr_offset";

    12 Goal "ALL f. sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f";

    13 by (induct_tac "n" 1);

    14 by Auto_tac;

    15 qed "sumr_offset2";

    17 Goal "sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";

    18 by (simp_tac (simpset() addsimps [sumr_offset]) 1);

    19 qed "sumr_offset3";

    21 Goal "ALL n f. sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f";

    22 by (simp_tac (simpset() addsimps [sumr_offset]) 1);

    23 qed "sumr_offset4";

    25 Goal "0 < n ==> \

    26 \     sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else \

    27 \            ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = \

    28 \     sumr 0 (Suc n) (%n. (if even(n) then 0 else \

    29 \            ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)";

    30 by (res_inst_tac [("n1","1")] (sumr_split_add RS subst) 1);

    31 by Auto_tac;

    32 qed "sumr_from_1_from_0";

    34 (*---------------------------------------------------------------------------*)

    35 (* Maclaurin's theorem with Lagrange form of remainder                       *)

    36 (*---------------------------------------------------------------------------*)

    38 (* Annoying: Proof is now even longer due mostly to

    39    change in behaviour of simplifier  since Isabelle99 *)

    40 Goal " [| 0 < h; 0 < n; diff 0 = f; \

    41 \      ALL m t. \

    42 \         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \

    43 \   ==> EX t. 0 < t & \

    44 \             t < h & \

    45 \             f h = \

    46 \             sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + \

    47 \             (diff n t / real (fact n)) * h ^ n";

    48 by (case_tac "n = 0" 1);

    49 by (Force_tac 1);

    50 by (dtac not0_implies_Suc 1);

    51 by (etac exE 1);

    52 by (subgoal_tac

    53      "EX B. f h = sumr 0 n (%m. (diff m 0 / real (fact m)) * (h ^ m)) \

    54 \                  + (B * ((h ^ n) / real (fact n)))" 1);

    56 by (simp_tac (HOL_ss addsimps [real_add_commute, real_divide_def,

    57     ARITH_PROVE "(x = z + (y::real)) = (x - y = z)"]) 2);

    58 by (res_inst_tac

    59   [("x","(f(h) - sumr 0 n (%m. (diff(m)(0) / real (fact m)) * (h ^ m))) \

    60 \        * real (fact n) / (h ^ n)")] exI 2);

    61 by (simp_tac (HOL_ss addsimps [real_mult_assoc,real_divide_def]) 2);

    62  by (rtac (CLAIM "x = (1::real) ==>  a = a * (x::real)") 2);

    63 by (asm_simp_tac (HOL_ss addsimps

    64     [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"]

    65      delsimps [realpow_Suc]) 2);

    66 by (stac left_inverse 2);

    67 by (stac left_inverse 3);

    68 by (rtac (real_not_refl2 RS not_sym) 2);

    69 by (etac zero_less_power 2);

    70 by (rtac real_of_nat_fact_not_zero 2);

    71 by (Simp_tac 2);

    72 by (etac exE 1);

    73 by (cut_inst_tac [("b","%t. f t - \

    74 \      (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \

    75 \                       (B * ((t ^ n) / real (fact n))))")]

    76     (CLAIM "EX g. g = b") 1);

    77 by (etac exE 1);

    78 by (subgoal_tac "g 0 = 0 & g h =0" 1);

    79 by (asm_simp_tac (simpset() addsimps

    80     [ARITH_PROVE "(x - y = z) = (x = z + (y::real))"]

    81     delsimps [sumr_Suc]) 2);

    82 by (cut_inst_tac [("n","m"),("k","1")] sumr_offset2 2);

    83 by (asm_full_simp_tac (simpset() addsimps

    84     [ARITH_PROVE "(x = y - z) = (y = x + (z::real))"]

    85     delsimps [sumr_Suc]) 2);

    86 by (cut_inst_tac [("b","%m t. diff m t - \

    87 \      (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) \

    88 \       + (B * ((t ^ (n - m)) / real (fact(n - m)))))")]

    89     (CLAIM "EX difg. difg = b") 1);

    90 by (etac exE 1);

    91 by (subgoal_tac "difg 0 = g" 1);

    92 by (asm_simp_tac (simpset() delsimps [realpow_Suc,fact_Suc]) 2);

    93 by (subgoal_tac "ALL m t. m < n & 0 <= t & t <= h --> \

    94 \                   DERIV (difg m) t :> difg (Suc m) t" 1);

    95 by (Clarify_tac 2);

    96 by (rtac DERIV_diff 2);

    97 by (Asm_simp_tac 2);

    98 by DERIV_tac;

    99 by DERIV_tac;

   100 by (rtac lemma_DERIV_subst 3);

   101 by (rtac DERIV_quotient 3);

   102 by (rtac DERIV_const 4);

   103 by (rtac DERIV_pow 3);

   104 by (asm_simp_tac (simpset() addsimps [inverse_mult_distrib,

   105     CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e"

   106     mult_ac,fact_diff_Suc]) 4);

   107 by (Asm_simp_tac 3);

   108 by (forw_inst_tac [("m","ma")] less_add_one 2);

   109 by (Clarify_tac 2);

   110 by (asm_simp_tac (simpset() addsimps

   111     [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"]

   112     delsimps [sumr_Suc]) 2);

   113 by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])

   114           (read_instantiate [("k","1")] sumr_offset4))]

   115     delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);

   116 by (rtac lemma_DERIV_subst 2);

   117 by (rtac DERIV_add 2);

   118 by (rtac DERIV_const 3);

   119 by (rtac DERIV_sumr 2);

   120 by (Clarify_tac 2);

   121 by (Simp_tac 3);

   122 by (simp_tac (simpset() addsimps [real_divide_def,real_mult_assoc]

   123     delsimps [fact_Suc,realpow_Suc]) 2);

   124 by (rtac DERIV_cmult 2);

   125 by (rtac lemma_DERIV_subst 2);

   126 by DERIV_tac;

   127 by (stac fact_Suc 2);

   128 by (stac real_of_nat_mult 2);

   129 by (simp_tac (simpset() addsimps [inverse_mult_distrib] @

   130     mult_ac) 2);

   131 by (subgoal_tac "ALL ma. ma < n --> \

   132 \        (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1);

   133 by (rotate_tac 11 1);

   134 by (dres_inst_tac [("x","m")] spec 1);

   135 by (etac impE 1);

   136 by (Asm_simp_tac 1);

   137 by (etac exE 1);

   138 by (res_inst_tac [("x","t")] exI 1);

   139 by (asm_full_simp_tac (simpset() addsimps

   140      [ARITH_PROVE "(x - y = 0) = (y = (x::real))"]

   141       delsimps [realpow_Suc,fact_Suc]) 1);

   142 by (subgoal_tac "ALL m. m < n --> difg m 0 = 0" 1);

   143 by (Clarify_tac 2);

   144 by (Asm_simp_tac 2);

   145 by (forw_inst_tac [("m","ma")] less_add_one 2);

   146 by (Clarify_tac 2);

   147 by (asm_simp_tac (simpset() delsimps [sumr_Suc]) 2);

   148 by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])

   149           (read_instantiate [("k","1")] sumr_offset4))]

   150     delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);

   151 by (subgoal_tac "ALL m. m < n --> (EX t. 0 < t & t < h & \

   152 \                DERIV (difg m) t :> 0)" 1);

   153 by (rtac allI 1 THEN rtac impI 1);

   154 by (rotate_tac 12 1);

   155 by (dres_inst_tac [("x","ma")] spec 1);

   156 by (etac impE 1 THEN assume_tac 1);

   157 by (etac exE 1);

   158 by (res_inst_tac [("x","t")] exI 1);

   159 (* do some tidying up *)

   160 by (ALLGOALS(thin_tac "difg = \

   161 \          (%m t. diff m t - \

   162 \                 (sumr 0 (n - m) \

   163 \                   (%p. diff (m + p) 0 / real (fact p) * t ^ p) + \

   164 \                  B * (t ^ (n - m) / real (fact (n - m)))))"));

   165 by (ALLGOALS(thin_tac "g = \

   166 \          (%t. f t - \

   167 \               (sumr 0 n (%m. diff m 0 / real  (fact m) * t ^ m) + \

   168 \                B * (t ^ n / real (fact n))))"));

   169 by (ALLGOALS(thin_tac "f h = \

   170 \          sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \

   171 \          B * (h ^ n / real (fact n))"));

   172 (* back to business *)

   173 by (Asm_simp_tac 1);

   174 by (rtac DERIV_unique 1);

   175 by (Blast_tac 2);

   176 by (Force_tac 1);

   177 by (rtac allI 1 THEN induct_tac "ma" 1);

   178 by (rtac impI 1 THEN rtac Rolle 1);

   179 by (assume_tac 1);

   180 by (Asm_full_simp_tac 1);

   181 by (Asm_full_simp_tac 1);

   182 by (subgoal_tac "ALL t. 0 <= t & t <= h --> g differentiable t" 1);

   183 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);

   184 by (blast_tac (claset() addDs [DERIV_isCont]) 1);

   185 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);

   186 by (Clarify_tac 1);

   187 by (res_inst_tac [("x","difg (Suc 0) t")] exI 1);

   188 by (Force_tac 1);

   189 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);

   190 by (Clarify_tac 1);

   191 by (res_inst_tac [("x","difg (Suc 0) x")] exI 1);

   192 by (Force_tac 1);

   193 by (Step_tac 1);

   194 by (Force_tac 1);

   195 by (subgoal_tac "EX ta. 0 < ta & ta < t & \

   196 \                DERIV difg (Suc n) ta :> 0" 1);

   197 by (rtac Rolle 2 THEN assume_tac 2);

   198 by (Asm_full_simp_tac 2);

   199 by (rotate_tac 2 2);

   200 by (dres_inst_tac [("x","n")] spec 2);

   201 by (ftac (ARITH_PROVE "n < m  ==> n < Suc m") 2);

   202 by (rtac DERIV_unique 2);

   203 by (assume_tac 3);

   204 by (Force_tac 2);

   205 by (subgoal_tac

   206     "ALL ta. 0 <= ta & ta <= t --> (difg (Suc n)) differentiable ta" 2);

   207 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);

   208 by (blast_tac (claset() addSDs [DERIV_isCont]) 2);

   209 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);

   210 by (Clarify_tac 2);

   211 by (res_inst_tac [("x","difg (Suc (Suc n)) ta")] exI 2);

   212 by (Force_tac 2);

   213 by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2);

   214 by (Clarify_tac 2);

   215 by (res_inst_tac [("x","difg (Suc (Suc n)) x")] exI 2);

   216 by (Force_tac 2);

   217 by (Step_tac 1);

   218 by (res_inst_tac [("x","ta")] exI 1);

   219 by (Force_tac 1);

   220 qed "Maclaurin";

   222 Goal "0 < h & 0 < n & diff 0 = f & \

   223 \      (ALL m t. \

   224 \         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \

   225 \   --> (EX t. 0 < t & \

   226 \             t < h & \

   227 \             f h = \

   228 \             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \

   229 \             diff n t / real (fact n) * h ^ n)";

   230 by (blast_tac (claset() addIs [Maclaurin]) 1);

   231 qed "Maclaurin_objl";

   233 Goal " [| 0 < h; diff 0 = f; \

   234 \      ALL m t. \

   235 \         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \

   236 \   ==> EX t. 0 < t & \

   237 \             t <= h & \

   238 \             f h = \

   239 \             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \

   240 \             diff n t / real (fact n) * h ^ n";

   241 by (case_tac "n" 1);

   242 by Auto_tac;

   243 by (dtac Maclaurin 1 THEN Auto_tac);

   244 qed "Maclaurin2";

   246 Goal "0 < h & diff 0 = f & \

   247 \      (ALL m t. \

   248 \         m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \

   249 \   --> (EX t. 0 < t & \

   250 \             t <= h & \

   251 \             f h = \

   252 \             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \

   253 \             diff n t / real (fact n) * h ^ n)";

   254 by (blast_tac (claset() addIs [Maclaurin2]) 1);

   255 qed "Maclaurin2_objl";

   257 Goal " [| h < 0; 0 < n; diff 0 = f; \

   258 \      ALL m t. \

   259 \         m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t |] \

   260 \   ==> EX t. h < t & \

   261 \             t < 0 & \

   262 \             f h = \

   263 \             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \

   264 \             diff n t / real (fact n) * h ^ n";

   265 by (cut_inst_tac [("f","%x. f (-x)"),

   266                  ("diff","%n x. ((- 1) ^ n) * diff n (-x)"),

   267                  ("h","-h"),("n","n")] Maclaurin_objl 1);

   268 by (Asm_full_simp_tac 1);

   269 by (etac impE 1 THEN Step_tac 1);

   270 by (stac minus_mult_right 1);

   271 by (rtac DERIV_cmult 1);

   272 by (rtac lemma_DERIV_subst 1);

   273 by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1);

   274 by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2);

   275 by (Force_tac 2);

   276 by (Force_tac 1);

   277 by (res_inst_tac [("x","-t")] exI 1);

   278 by Auto_tac;

   279 by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1);

   280 by (rtac sumr_fun_eq 1);

   281 by (Asm_full_simp_tac 1);

   282 by (auto_tac (claset(),simpset() addsimps [real_divide_def,

   283     CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))",

   284     power_mult_distrib RS sym]));

   285 qed "Maclaurin_minus";

   287 Goal "(h < 0 & 0 < n & diff 0 = f & \

   288 \      (ALL m t. \

   289 \         m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\

   290 \   --> (EX t. h < t & \

   291 \             t < 0 & \

   292 \             f h = \

   293 \             sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \

   294 \             diff n t / real (fact n) * h ^ n)";

   295 by (blast_tac (claset() addIs [Maclaurin_minus]) 1);

   296 qed "Maclaurin_minus_objl";

   298 (* ------------------------------------------------------------------------- *)

   299 (* More convenient "bidirectional" version.                                  *)

   300 (* ------------------------------------------------------------------------- *)

   302 (* not good for PVS sin_approx, cos_approx *)

   303 Goal " [| diff 0 = f; \

   304 \      ALL m t. \

   305 \         m < n & abs t <= abs x --> DERIV (diff m) t :> diff (Suc m) t |] \

   306 \   ==> EX t. abs t <= abs x & \

   307 \             f x = \

   308 \             sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + \

   309 \             diff n t / real (fact n) * x ^ n";

   310 by (case_tac "n = 0" 1);

   311 by (Force_tac 1);

   312 by (case_tac "x = 0" 1);

   313 by (res_inst_tac [("x","0")] exI 1);

   314 by (Asm_full_simp_tac 1);

   315 by (res_inst_tac [("P","0 < n")] impE 1);

   316 by (assume_tac 2 THEN assume_tac 2);

   317 by (induct_tac "n" 1);

   318 by (Simp_tac 1);

   319 by Auto_tac;

   320 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);

   321 by Auto_tac;

   322 by (cut_inst_tac [("f","diff 0"),

   323                  ("diff","diff"),

   324                  ("h","x"),("n","n")] Maclaurin_objl 2);

   325 by (Step_tac 2);

   326 by (blast_tac (claset() addDs

   327     [ARITH_PROVE "[|(0::real) <= t;t <= x |] ==> abs t <= abs x"]) 2);

   328 by (res_inst_tac [("x","t")] exI 2);

   329 by (force_tac (claset() addIs

   330     [ARITH_PROVE "[| 0 < t; (t::real) < x|] ==> abs t <= abs x"],simpset()) 2);

   331 by (cut_inst_tac [("f","diff 0"),

   332                  ("diff","diff"),

   333                  ("h","x"),("n","n")] Maclaurin_minus_objl 1);

   334 by (Step_tac 1);

   335 by (blast_tac (claset() addDs

   336     [ARITH_PROVE "[|x <= t;t <= (0::real) |] ==> abs t <= abs x"]) 1);

   337 by (res_inst_tac [("x","t")] exI 1);

   338 by (force_tac (claset() addIs

   339     [ARITH_PROVE "[| x < t; (t::real) < 0|] ==> abs t <= abs x"],simpset()) 1);

   340 qed "Maclaurin_bi_le";

   342 Goal "[| diff 0 = f; \

   343 \        ALL m x. DERIV (diff m) x :> diff(Suc m) x; \

   344 \       x ~= 0; 0 < n \

   345 \     |] ==> EX t. 0 < abs t & abs t < abs x & \

   346 \              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \

   347 \                    (diff n t / real (fact n)) * x ^ n";

   348 by (res_inst_tac [("x","x"),("y","0")] linorder_cases 1);

   349 by (Blast_tac 2);

   350 by (dtac Maclaurin_minus 1);

   351 by (dtac Maclaurin 5);

   352 by (TRYALL(assume_tac));

   353 by (Blast_tac 1);

   354 by (Blast_tac 2);

   355 by (Step_tac 1);

   356 by (ALLGOALS(res_inst_tac [("x","t")] exI));

   357 by (Step_tac 1);

   358 by (ALLGOALS(arith_tac));

   359 qed "Maclaurin_all_lt";

   361 Goal "diff 0 = f & \

   362 \     (ALL m x. DERIV (diff m) x :> diff(Suc m) x) & \

   363 \     x ~= 0 & 0 < n \

   364 \     --> (EX t. 0 < abs t & abs t < abs x & \

   365 \              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \

   366 \                    (diff n t / real (fact n)) * x ^ n)";

   367 by (blast_tac (claset() addIs [Maclaurin_all_lt]) 1);

   368 qed "Maclaurin_all_lt_objl";

   370 Goal "x = (0::real)  \

   371 \     ==> 0 < n --> \

   372 \         sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = \

   373 \         diff 0 0";

   374 by (Asm_simp_tac 1);

   375 by (induct_tac "n" 1);

   376 by Auto_tac;

   377 qed_spec_mp "Maclaurin_zero";

   379 Goal "[| diff 0 = f; \

   380 \       ALL m x. DERIV (diff m) x :> diff (Suc m) x \

   381 \     |] ==> EX t. abs t <= abs x & \

   382 \             f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \

   383 \                   (diff n t / real (fact n)) * x ^ n";

   384 by (cut_inst_tac [("n","n"),("m","0")]

   385        (ARITH_PROVE "n <= m | m < (n::nat)") 1);

   386 by (etac disjE 1);

   387 by (Force_tac 1);

   388 by (case_tac "x = 0" 1);

   389 by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_zero 1);

   390 by (assume_tac 1);

   391 by (dtac (gr_implies_not0 RS  not0_implies_Suc) 1);

   392 by (res_inst_tac [("x","0")] exI 1);

   393 by (Force_tac 1);

   394 by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_all_lt 1);

   395 by (TRYALL(assume_tac));

   396 by (Step_tac 1);

   397 by (res_inst_tac [("x","t")] exI 1);

   398 by Auto_tac;

   399 qed "Maclaurin_all_le";

   401 Goal "diff 0 = f & \

   402 \     (ALL m x. DERIV (diff m) x :> diff (Suc m) x)  \

   403 \     --> (EX t. abs t <= abs x & \

   404 \             f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \

   405 \                   (diff n t / real (fact n)) * x ^ n)";

   406 by (blast_tac (claset() addIs [Maclaurin_all_le]) 1);

   407 qed "Maclaurin_all_le_objl";

   409 (* ------------------------------------------------------------------------- *)

   410 (* Version for exp.                                                          *)

   411 (* ------------------------------------------------------------------------- *)

   413 Goal "[| x ~= 0; 0 < n |] \

   414 \     ==> (EX t. 0 < abs t & \

   415 \               abs t < abs x & \

   416 \               exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \

   417 \                       (exp t / real (fact n)) * x ^ n)";

   418 by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")]

   419     Maclaurin_all_lt_objl 1);

   420 by Auto_tac;

   421 qed "Maclaurin_exp_lt";

   423 Goal "EX t. abs t <= abs x & \

   424 \           exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \

   425 \                      (exp t / real (fact n)) * x ^ n";

   426 by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")]

   427     Maclaurin_all_le_objl 1);

   428 by Auto_tac;

   429 qed "Maclaurin_exp_le";

   431 (* ------------------------------------------------------------------------- *)

   432 (* Version for sin function                                                  *)

   433 (* ------------------------------------------------------------------------- *)

   435 Goal "[| a < b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \

   436 \     ==> EX z. a < z & z < b & (f b - f a = (b - a) * f'(z))";

   437 by (dtac MVT 1);

   438 by (blast_tac (claset() addIs [DERIV_isCont]) 1);

   439 by (force_tac (claset() addDs [order_less_imp_le],

   440     simpset() addsimps [differentiable_def]) 1);

   441 by (blast_tac (claset() addDs [DERIV_unique,order_less_imp_le]) 1);

   442 qed "MVT2";

   444 Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3";

   445 by (case_tac "d" 1 THEN Auto_tac);

   446 qed "lemma_exhaust_less_4";

   448 bind_thm ("real_mult_le_lemma",

   449           simplify (simpset()) (inst "b" "1" mult_right_mono));

   452 Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n";

   453 by (induct_tac "n" 1);

   454 by Auto_tac;

   455 qed_spec_mp "Suc_Suc_mult_two_diff_two";

   456 Addsimps [Suc_Suc_mult_two_diff_two];

   458 Goal "0 < n --> Suc (Suc (4*n - 2)) = 4*n";

   459 by (induct_tac "n" 1);

   460 by Auto_tac;

   461 qed_spec_mp "lemma_Suc_Suc_4n_diff_2";

   462 Addsimps [lemma_Suc_Suc_4n_diff_2];

   464 Goal "0 < n --> Suc (2 * n - 1) = 2*n";

   465 by (induct_tac "n" 1);

   466 by Auto_tac;

   467 qed_spec_mp "Suc_mult_two_diff_one";

   468 Addsimps [Suc_mult_two_diff_one];

   470 Goal "EX t. sin x = \

   471 \      (sumr 0 n (%m. (if even m then 0 \

   472 \                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \

   473 \                      x ^ m)) \

   474 \     + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";

   475 by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),

   476        ("diff","%n x. sin(x + 1/2*real (n)*pi)")]

   477        Maclaurin_all_lt_objl 1);

   478 by (Safe_tac);

   479 by (Simp_tac 1);

   480 by (Simp_tac 1);

   481 by (case_tac "n" 1);

   482 by (Clarify_tac 1);

   483 by (Asm_full_simp_tac 1);

   484 by (dres_inst_tac [("x","0")] spec 1 THEN Asm_full_simp_tac 1);

   485 by (Asm_full_simp_tac 1);

   486 by (rtac ccontr 1);

   487 by (Asm_full_simp_tac 1);

   488 by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);

   489 by (dtac ssubst 1 THEN assume_tac 2);

   490 by (res_inst_tac [("x","t")] exI 1);

   491 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);

   492 by (rtac sumr_fun_eq 1);

   493 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));

   494 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));

   495 (*Could sin_zero_iff help?*)

   496 qed "Maclaurin_sin_expansion";

   498 Goal "EX t. abs t <= abs x &  \

   499 \      sin x = \

   500 \      (sumr 0 n (%m. (if even m then 0 \

   501 \                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \

   502 \                      x ^ m)) \

   503 \     + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";

   505 by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),

   506        ("diff","%n x. sin(x + 1/2*real (n)*pi)")]

   507        Maclaurin_all_lt_objl 1);

   508 by (Step_tac 1);

   509 by (Simp_tac 1);

   510 by (Simp_tac 1);

   511 by (case_tac "n" 1);

   512 by (Clarify_tac 1);

   513 by (Asm_full_simp_tac 1);

   514 by (Asm_full_simp_tac 1);

   515 by (rtac ccontr 1);

   516 by (Asm_full_simp_tac 1);

   517 by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);

   518 by (dtac ssubst 1 THEN assume_tac 2);

   519 by (res_inst_tac [("x","t")] exI 1);

   520 by (rtac conjI 1);

   521 by (arith_tac 1);

   522 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);

   523 by (rtac sumr_fun_eq 1);

   524 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));

   525 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));

   526 qed "Maclaurin_sin_expansion2";

   528 Goal "[| 0 < n; 0 < x |] ==> \

   529 \      EX t. 0 < t & t < x & \

   530 \      sin x = \

   531 \      (sumr 0 n (%m. (if even m then 0 \

   532 \                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \

   533 \                      x ^ m)) \

   534 \     + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)";

   535 by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),

   536        ("diff","%n x. sin(x + 1/2*real (n)*pi)")]

   537        Maclaurin_objl 1);

   538 by (Step_tac 1);

   539 by (Asm_full_simp_tac 1);

   540 by (Simp_tac 1);

   541 by (dtac ssubst 1 THEN assume_tac 2);

   542 by (res_inst_tac [("x","t")] exI 1);

   543 by (rtac conjI 1 THEN rtac conjI 2);

   544 by (assume_tac 1 THEN assume_tac 1);

   545 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);

   546 by (rtac sumr_fun_eq 1);

   547 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));

   548 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));

   549 qed "Maclaurin_sin_expansion3";

   551 Goal "0 < x ==> \

   552 \      EX t. 0 < t & t <= x & \

   553 \      sin x = \

   554 \      (sumr 0 n (%m. (if even m then 0 \

   555 \                      else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \

   556 \                      x ^ m)) \

   557 \     + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";

   558 by (cut_inst_tac [("f","sin"),("n","n"),("h","x"),

   559        ("diff","%n x. sin(x + 1/2*real (n)*pi)")]

   560        Maclaurin2_objl 1);

   561 by (Step_tac 1);

   562 by (Asm_full_simp_tac 1);

   563 by (Simp_tac 1);

   564 by (dtac ssubst 1 THEN assume_tac 2);

   565 by (res_inst_tac [("x","t")] exI 1);

   566 by (rtac conjI 1 THEN rtac conjI 2);

   567 by (assume_tac 1 THEN assume_tac 1);

   568 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);

   569 by (rtac sumr_fun_eq 1);

   570 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));

   571 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));

   572 qed "Maclaurin_sin_expansion4";

   574 (*-----------------------------------------------------------------------------*)

   575 (* Maclaurin expansion for cos                                                 *)

   576 (*-----------------------------------------------------------------------------*)

   578 Goal "sumr 0 (Suc n) \

   579 \        (%m. (if even m \

   580 \              then (- 1) ^ (m div 2)/(real  (fact m)) \

   581 \              else 0) * \

   582 \             0 ^ m) = 1";

   583 by (induct_tac "n" 1);

   584 by Auto_tac;

   585 qed "sumr_cos_zero_one";

   586 Addsimps [sumr_cos_zero_one];

   588 Goal "EX t. abs t <= abs x & \

   589 \      cos x = \

   590 \      (sumr 0 n (%m. (if even m \

   591 \                      then (- 1) ^ (m div 2)/(real (fact m)) \

   592 \                      else 0) * \

   593 \                      x ^ m)) \

   594 \     + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";

   595 by (cut_inst_tac [("f","cos"),("n","n"),("x","x"),

   596        ("diff","%n x. cos(x + 1/2*real (n)*pi)")]

   597        Maclaurin_all_lt_objl 1);

   598 by (Step_tac 1);

   599 by (Simp_tac 1);

   600 by (Simp_tac 1);

   601 by (case_tac "n" 1);

   602 by (Asm_full_simp_tac 1);

   603 by (asm_full_simp_tac (simpset() delsimps [sumr_Suc]) 1);

   604 by (rtac ccontr 1);

   605 by (Asm_full_simp_tac 1);

   606 by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1);

   607 by (dtac ssubst 1 THEN assume_tac 2);

   608 by (res_inst_tac [("x","t")] exI 1);

   609 by (rtac conjI 1);

   610 by (arith_tac 1);

   611 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);

   612 by (rtac sumr_fun_eq 1);

   613 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));

   614 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps

   615     [fact_Suc,realpow_Suc]));

   616 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));

   617 qed "Maclaurin_cos_expansion";

   619 Goal "[| 0 < x; 0 < n |] ==> \

   620 \      EX t. 0 < t & t < x & \

   621 \      cos x = \

   622 \      (sumr 0 n (%m. (if even m \

   623 \                      then (- 1) ^ (m div 2)/(real (fact m)) \

   624 \                      else 0) * \

   625 \                      x ^ m)) \

   626 \     + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";

   627 by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),

   628        ("diff","%n x. cos(x + 1/2*real (n)*pi)")]

   629        Maclaurin_objl 1);

   630 by (Step_tac 1);

   631 by (Asm_full_simp_tac 1);

   632 by (Simp_tac 1);

   633 by (dtac ssubst 1 THEN assume_tac 2);

   634 by (res_inst_tac [("x","t")] exI 1);

   635 by (rtac conjI 1 THEN rtac conjI 2);

   636 by (assume_tac 1 THEN assume_tac 1);

   637 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);

   638 by (rtac sumr_fun_eq 1);

   639 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));

   640 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps [fact_Suc,realpow_Suc]));

   641 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));

   642 qed "Maclaurin_cos_expansion2";

   644 Goal "[| x < 0; 0 < n |] ==> \

   645 \      EX t. x < t & t < 0 & \

   646 \      cos x = \

   647 \      (sumr 0 n (%m. (if even m \

   648 \                      then (- 1) ^ (m div 2)/(real (fact m)) \

   649 \                      else 0) * \

   650 \                      x ^ m)) \

   651 \     + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)";

   652 by (cut_inst_tac [("f","cos"),("n","n"),("h","x"),

   653        ("diff","%n x. cos(x + 1/2*real (n)*pi)")]

   654        Maclaurin_minus_objl 1);

   655 by (Step_tac 1);

   656 by (Asm_full_simp_tac 1);

   657 by (Simp_tac 1);

   658 by (dtac ssubst 1 THEN assume_tac 2);

   659 by (res_inst_tac [("x","t")] exI 1);

   660 by (rtac conjI 1 THEN rtac conjI 2);

   661 by (assume_tac 1 THEN assume_tac 1);

   662 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);

   663 by (rtac sumr_fun_eq 1);

   664 by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));

   665 by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps [fact_Suc,realpow_Suc]));

   666 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));

   667 qed "Maclaurin_minus_cos_expansion";

   669 (* ------------------------------------------------------------------------- *)

   670 (* Version for ln(1 +/- x). Where is it??                                    *)

   671 (* ------------------------------------------------------------------------- *)

author	obua
	Tue, 11 May 2004 20:11:08 +0200
changeset 14738	83f1a514dcb4
child 15047	fa62de5862b9
permissions	-rw-r--r--