src/HOL/Hyperreal/Transcendental.thy
changeset 15085 5693a977a767
parent 15081 32402f5624d1
child 15086 e6a2a98d5ef5
equal deleted inserted replaced
15084:07f7b158ef32 15085:5693a977a767
     6 *)
     6 *)
     7 
     7 
     8 header{*Power Series, Transcendental Functions etc.*}
     8 header{*Power Series, Transcendental Functions etc.*}
     9 
     9 
    10 theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:
    10 theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:
    11 
       
    12 (*????FOR RING_AND_FIELD*)
       
    13 
    11 
    14 constdefs
    12 constdefs
    15     root :: "[nat,real] => real"
    13     root :: "[nat,real] => real"
    16     "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
    14     "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
    17 
    15 
   662 apply (auto intro!: summable_sums)
   660 apply (auto intro!: summable_sums)
   663 apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
   661 apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
   664 apply (auto simp add: add_commute)
   662 apply (auto simp add: add_commute)
   665 apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) 
   663 apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) 
   666 apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
   664 apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
   667 apply (rule sums_unique [symmetric])
   665 apply (rule sums_unique)
   668 apply (simp add: diff_def divide_inverse add_ac mult_ac)
   666 apply (simp add: diff_def divide_inverse add_ac mult_ac)
   669 apply (rule LIM_zero_cancel)
   667 apply (rule LIM_zero_cancel)
   670 apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans)
   668 apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans)
   671  prefer 2 apply (blast intro: termdiffs_aux) 
   669  prefer 2 apply (blast intro: termdiffs_aux) 
   672 apply (simp add: LIM_def, safe)
   670 apply (simp add: LIM_def, safe)
   688                right_diff_distrib [symmetric])
   686                right_diff_distrib [symmetric])
   689 apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
   687 apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
   690 apply (simp add: sums_summable [THEN suminf_mult2])
   688 apply (simp add: sums_summable [THEN suminf_mult2])
   691 apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)
   689 apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)
   692 apply assumption
   690 apply assumption
   693 apply (subst minus_equation_iff, simp (no_asm))  
       
   694 apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
   691 apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
   695 apply (rule_tac f = suminf in arg_cong)
   692 apply (rule_tac f = suminf in arg_cong)
   696 apply (rule ext)
   693 apply (rule ext)
   697 apply (simp add: diff_def right_distrib add_ac mult_ac)
   694 apply (simp add: diff_def right_distrib add_ac mult_ac)
   698 done
   695 done
  1266 done
  1263 done
  1267 
  1264 
  1268 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  1265 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  1269 apply (cut_tac x = x and y = y in sin_cos_add)
  1266 apply (cut_tac x = x and y = y in sin_cos_add)
  1270 apply (auto dest!: real_sum_squares_cancel_a 
  1267 apply (auto dest!: real_sum_squares_cancel_a 
  1271             simp add: numeral_2_eq_2 simp del: sin_cos_add)
  1268             simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
  1272 done
  1269 done
  1273 
  1270 
  1274 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  1271 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  1275 apply (cut_tac x = x and y = y in sin_cos_add)
  1272 apply (cut_tac x = x and y = y in sin_cos_add)
  1276 apply (auto dest!: real_sum_squares_cancel_a
  1273 apply (auto dest!: real_sum_squares_cancel_a
  1277             simp add: numeral_2_eq_2 simp del: sin_cos_add)
  1274             simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
  1278 done
  1275 done
  1279 
  1276 
  1280 lemma lemma_DERIV_sin_cos_minus: "\<forall>x.  
  1277 lemma lemma_DERIV_sin_cos_minus:
  1281           DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
  1278     "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
  1282 apply (safe, rule lemma_DERIV_subst)
  1279 apply (safe, rule lemma_DERIV_subst)
  1283 apply (best intro!: DERIV_intros intro: DERIV_chain2) 
  1280 apply (best intro!: DERIV_intros intro: DERIV_chain2) 
  1284 apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
  1281 apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
  1285 done
  1282 done
  1286 
  1283 
  1287 lemma sin_cos_minus [simp]: "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
  1284 lemma sin_cos_minus [simp]: 
  1288 apply (cut_tac y = 0 and x = x in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
  1285     "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
       
  1286 apply (cut_tac y = 0 and x = x 
       
  1287        in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
  1289 apply (auto simp add: numeral_2_eq_2)
  1288 apply (auto simp add: numeral_2_eq_2)
  1290 done
  1289 done
  1291 
  1290 
  1292 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  1291 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  1293 apply (cut_tac x = x in sin_cos_minus)
  1292 apply (cut_tac x = x in sin_cos_minus)
  1294 apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus)
  1293 apply (auto dest!: real_sum_squares_cancel_a 
       
  1294        simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_minus)
  1295 done
  1295 done
  1296 
  1296 
  1297 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  1297 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  1298 apply (cut_tac x = x in sin_cos_minus)
  1298 apply (cut_tac x = x in sin_cos_minus)
  1299 apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus)
  1299 apply (auto dest!: real_sum_squares_cancel_a 
       
  1300                    simp add: numeral_2_eq_2 simp del: sin_cos_minus)
  1300 done
  1301 done
  1301 
  1302 
  1302 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  1303 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  1303 apply (unfold real_diff_def)
  1304 apply (unfold real_diff_def)
  1304 apply (simp (no_asm) add: sin_add)
  1305 apply (simp (no_asm) add: sin_add)
  1366 apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
  1367 apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
  1367 apply (simp only: mult_less_cancel_left, simp)
  1368 apply (simp only: mult_less_cancel_left, simp)
  1368 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
  1369 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
  1369 apply (subgoal_tac "x*x < 2*3", simp) 
  1370 apply (subgoal_tac "x*x < 2*3", simp) 
  1370 apply (rule mult_strict_mono)
  1371 apply (rule mult_strict_mono)
  1371 apply (auto simp add: real_of_nat_Suc simp del: fact_Suc)
  1372 apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
  1372 apply (subst fact_Suc)
  1373 apply (subst fact_Suc)
  1373 apply (subst fact_Suc)
  1374 apply (subst fact_Suc)
  1374 apply (subst fact_Suc)
  1375 apply (subst fact_Suc)
  1375 apply (subst fact_Suc)
  1376 apply (subst fact_Suc)
  1376 apply (subst real_of_nat_mult)
  1377 apply (subst real_of_nat_mult)
  1428 apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n))) " in order_less_trans)
  1429 apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n))) " in order_less_trans)
  1429 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
  1430 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
  1430 apply (simp (no_asm) add: mult_assoc del: sumr_Suc)
  1431 apply (simp (no_asm) add: mult_assoc del: sumr_Suc)
  1431 apply (rule sumr_pos_lt_pair)
  1432 apply (rule sumr_pos_lt_pair)
  1432 apply (erule sums_summable, safe)
  1433 apply (erule sums_summable, safe)
  1433 apply (simp (no_asm) add: divide_inverse mult_assoc [symmetric] del: fact_Suc)
  1434 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
       
  1435             del: fact_Suc)
  1434 apply (rule real_mult_inverse_cancel2)
  1436 apply (rule real_mult_inverse_cancel2)
  1435 apply (rule real_of_nat_fact_gt_zero)+
  1437 apply (rule real_of_nat_fact_gt_zero)+
  1436 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
  1438 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
  1437 apply (subst fact_lemma) 
  1439 apply (subst fact_lemma) 
  1438 apply (subst fact_Suc)
  1440 apply (subst fact_Suc)
  1690 lemma sin_zero_lemma: "[| 0 \<le> x; sin x = 0 |] ==>  
  1692 lemma sin_zero_lemma: "[| 0 \<le> x; sin x = 0 |] ==>  
  1691       \<exists>n::nat. even n & x = real n * (pi/2)"
  1693       \<exists>n::nat. even n & x = real n * (pi/2)"
  1692 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  1694 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  1693  apply (clarify, rule_tac x = "n - 1" in exI)
  1695  apply (clarify, rule_tac x = "n - 1" in exI)
  1694  apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
  1696  apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
  1695 apply (rule cos_zero_lemma, clarify) 
  1697 apply (rule cos_zero_lemma)
  1696 apply (rule minus_le_iff [THEN iffD1])  
  1698 apply (simp_all add: add_increasing)  
  1697 apply (rule_tac y=0 in order_trans, auto)
       
  1698 done
  1699 done
  1699 
  1700 
  1700 
  1701 
  1701 (* also spoilt by numeral arithmetic *)
  1702 (* also spoilt by numeral arithmetic *)
  1702 lemma cos_zero_iff: "(cos x = 0) =  
  1703 lemma cos_zero_iff: "(cos x = 0) =  
  1990         simp add: power_mult_distrib left_distrib realpow_divide tan_def 
  1991         simp add: power_mult_distrib left_distrib realpow_divide tan_def 
  1991                   mult_assoc power_inverse [symmetric] 
  1992                   mult_assoc power_inverse [symmetric] 
  1992         simp del: realpow_Suc)
  1993         simp del: realpow_Suc)
  1993 done
  1994 done
  1994 
  1995 
  1995 lemma lemma_sin_cos_eq [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =  
  1996 text{*NEEDED??*}
       
  1997 lemma [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =  
  1996       cos (xa + 1 / 2 * real  (m) * pi)"
  1998       cos (xa + 1 / 2 * real  (m) * pi)"
  1997 apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
  1999 apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
  1998 done
  2000 done
  1999 
  2001 
  2000 lemma lemma_sin_cos_eq2 [simp]: "sin (xa + real (Suc m) * pi / 2) =  
  2002 text{*NEEDED??*}
       
  2003 lemma [simp]: "sin (xa + real (Suc m) * pi / 2) =  
  2001       cos (xa + real (m) * pi / 2)"
  2004       cos (xa + real (m) * pi / 2)"
  2002 apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
  2005 apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
  2003 done
  2006 done
  2004 
  2007 
  2005 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
  2008 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
  2331 lemma lemma_sin_cos_eq:
  2334 lemma lemma_sin_cos_eq:
  2332      "[| 0 < x * x + y * y;  
  2335      "[| 0 < x * x + y * y;  
  2333          1 - (cos xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]
  2336          1 - (cos xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]
  2334       ==> (cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2"
  2337       ==> (cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2"
  2335 apply (auto simp add: realpow_divide power2_eq_square [symmetric])
  2338 apply (auto simp add: realpow_divide power2_eq_square [symmetric])
  2336 apply (rule add_commute [THEN subst])
  2339 apply (subst add_commute)
  2337 apply (rule lemma_divide_rearrange, simp)
  2340 apply (rule lemma_divide_rearrange, simp add: real_add_eq_0_iff)
  2338 apply (simp add: add_commute)
  2341 apply (simp add: add_commute)
  2339 done
  2342 done
  2340 
  2343 
  2341 lemma sin_x_y_disj:
  2344 lemma sin_x_y_disj:
  2342      "[| x \<noteq> 0;  
  2345      "[| x \<noteq> 0;  
  2393 apply (drule sin_ge_zero, assumption)
  2396 apply (drule sin_ge_zero, assumption)
  2394 apply (drule_tac x = x in real_sqrt_divide_less_zero, auto)
  2397 apply (drule_tac x = x in real_sqrt_divide_less_zero, auto)
  2395 done
  2398 done
  2396 
  2399 
  2397 lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
  2400 lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
  2398 by (auto intro: real_sum_squares_cancel)
  2401 by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
  2399 
  2402 
  2400 lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
  2403 lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
  2401 apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)
  2404 apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)
  2402 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)
  2405 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)
  2403 apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)
  2406 apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)
  2404 apply (auto dest: real_sum_squares_cancel2a simp add: power2_eq_square)
  2407 apply (auto dest: real_sum_squares_cancel2a 
       
  2408             simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff)
  2405 apply (unfold arcsin_def)
  2409 apply (unfold arcsin_def)
  2406 apply (cut_tac x1 = x and y1 = y 
  2410 apply (cut_tac x1 = x and y1 = y 
  2407        in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])
  2411        in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])
  2408 apply (rule someI2_ex, blast)
  2412 apply (rule someI2_ex, blast)
  2409 apply (erule_tac V = "EX! xa. - (pi/2) \<le> xa & xa \<le> pi/2 & sin xa = y / sqrt (x * x + y * y) " in thin_rl)
  2413 apply (erule_tac V = "EX! xa. - (pi/2) \<le> xa & xa \<le> pi/2 & sin xa = y / sqrt (x * x + y * y) " in thin_rl)
  2410 apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast, auto)
  2414 apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast)
       
  2415 apply (auto simp add: real_0_le_add_iff real_add_eq_0_iff)
  2411 apply (drule cos_ge_zero, force)
  2416 apply (drule cos_ge_zero, force)
  2412 apply (drule_tac x = y in real_sqrt_divide_less_zero)
  2417 apply (drule_tac x = y in real_sqrt_divide_less_zero)
  2413 apply (auto simp add: real_add_commute)
  2418 apply (auto simp add: add_commute)
  2414 apply (insert polar_ex1 [of x "-y"], simp, clarify) 
  2419 apply (insert polar_ex1 [of x "-y"], simp, clarify) 
  2415 apply (rule_tac x = r in exI)
  2420 apply (rule_tac x = r in exI)
  2416 apply (rule_tac x = "-a" in exI, simp) 
  2421 apply (rule_tac x = "-a" in exI, simp) 
  2417 done
  2422 done
  2418 
  2423 
  2537 apply (subgoal_tac "\<forall>z. \<bar>z - x\<bar> \<le> e --> isCont f z")
  2542 apply (subgoal_tac "\<forall>z. \<bar>z - x\<bar> \<le> e --> isCont f z")
  2538 prefer 2 apply force
  2543 prefer 2 apply force
  2539 apply (drule_tac d = e in isCont_inj_range)
  2544 apply (drule_tac d = e in isCont_inj_range)
  2540 prefer 2 apply (assumption, assumption, safe)
  2545 prefer 2 apply (assumption, assumption, safe)
  2541 apply (rule_tac x = ea in exI, auto)
  2546 apply (rule_tac x = ea in exI, auto)
  2542 apply (rotate_tac 4)
  2547 apply (drule_tac x = "f (x) + xa" and P = "%y. \<bar>y - f x\<bar> \<le> ea \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)" in spec)
  2543 apply (drule_tac x = "f (x) + xa" in spec)
       
  2544 apply auto
  2548 apply auto
  2545 apply (drule sym, auto, arith)
  2549 apply (drule sym, auto, arith)
  2546 done
  2550 done
  2547 
  2551 
  2548 lemma isCont_inv_fun_inv:
  2552 lemma isCont_inv_fun_inv:
  2865 val arcos_ge_minus_pi = thm "arcos_ge_minus_pi";
  2869 val arcos_ge_minus_pi = thm "arcos_ge_minus_pi";
  2866 val sin_x_y_disj = thm "sin_x_y_disj";
  2870 val sin_x_y_disj = thm "sin_x_y_disj";
  2867 val cos_x_y_disj = thm "cos_x_y_disj";
  2871 val cos_x_y_disj = thm "cos_x_y_disj";
  2868 val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero";
  2872 val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero";
  2869 val polar_ex1 = thm "polar_ex1";
  2873 val polar_ex1 = thm "polar_ex1";
  2870 val real_sum_squares_cancel2a = thm "real_sum_squares_cancel2a";
       
  2871 val polar_ex2 = thm "polar_ex2";
  2874 val polar_ex2 = thm "polar_ex2";
  2872 val polar_Ex = thm "polar_Ex";
  2875 val polar_Ex = thm "polar_Ex";
  2873 val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1";
  2876 val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1";
  2874 val real_sqrt_ge_abs2 = thm "real_sqrt_ge_abs2";
  2877 val real_sqrt_ge_abs2 = thm "real_sqrt_ge_abs2";
  2875 val real_sqrt_two_gt_zero = thm "real_sqrt_two_gt_zero";
  2878 val real_sqrt_two_gt_zero = thm "real_sqrt_two_gt_zero";