2204 by auto |
2204 by auto |
2205 |
2205 |
2206 lemma arctan_ubound: "arctan y < pi/2" |
2206 lemma arctan_ubound: "arctan y < pi/2" |
2207 by (auto simp only: arctan) |
2207 by (auto simp only: arctan) |
2208 |
2208 |
|
2209 lemma arctan_unique: |
|
2210 assumes "-(pi/2) < x" and "x < pi/2" and "tan x = y" |
|
2211 shows "arctan y = x" |
|
2212 using assms arctan [of y] tan_total [of y] by (fast elim: ex1E) |
|
2213 |
2209 lemma arctan_tan: |
2214 lemma arctan_tan: |
2210 "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x" |
2215 "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x" |
2211 apply (unfold arctan_def) |
2216 by (rule arctan_unique, simp_all) |
2212 apply (rule the1_equality) |
|
2213 apply (rule tan_total, auto) |
|
2214 done |
|
2215 |
2217 |
2216 lemma arctan_zero_zero [simp]: "arctan 0 = 0" |
2218 lemma arctan_zero_zero [simp]: "arctan 0 = 0" |
2217 by (insert arctan_tan [of 0], simp) |
2219 by (rule arctan_unique, simp_all) |
|
2220 |
|
2221 lemma arctan_minus: "arctan (- x) = - arctan x" |
|
2222 apply (rule arctan_unique) |
|
2223 apply (simp only: neg_less_iff_less arctan_ubound) |
|
2224 apply (metis minus_less_iff arctan_lbound) |
|
2225 apply simp |
|
2226 done |
2218 |
2227 |
2219 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0" |
2228 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0" |
2220 by (intro less_imp_neq [symmetric] cos_gt_zero_pi |
2229 by (intro less_imp_neq [symmetric] cos_gt_zero_pi |
2221 arctan_lbound arctan_ubound) |
2230 arctan_lbound arctan_ubound) |
2222 |
2231 |
2242 apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1]) |
2251 apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1]) |
2243 apply (auto dest: field_power_not_zero |
2252 apply (auto dest: field_power_not_zero |
2244 simp add: power_mult_distrib left_distrib power_divide tan_def |
2253 simp add: power_mult_distrib left_distrib power_divide tan_def |
2245 mult_assoc power_inverse [symmetric]) |
2254 mult_assoc power_inverse [symmetric]) |
2246 done |
2255 done |
|
2256 |
|
2257 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y" |
|
2258 by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan) |
|
2259 |
|
2260 lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y" |
|
2261 by (simp only: not_less [symmetric] arctan_less_iff) |
|
2262 |
|
2263 lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y" |
|
2264 by (simp only: eq_iff [where 'a=real] arctan_le_iff) |
|
2265 |
|
2266 lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x" |
|
2267 using arctan_less_iff [of 0 x] by simp |
|
2268 |
|
2269 lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0" |
|
2270 using arctan_less_iff [of x 0] by simp |
|
2271 |
|
2272 lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x" |
|
2273 using arctan_le_iff [of 0 x] by simp |
|
2274 |
|
2275 lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0" |
|
2276 using arctan_le_iff [of x 0] by simp |
|
2277 |
|
2278 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0" |
|
2279 using arctan_eq_iff [of x 0] by simp |
2247 |
2280 |
2248 lemma isCont_inverse_function2: |
2281 lemma isCont_inverse_function2: |
2249 fixes f g :: "real \<Rightarrow> real" shows |
2282 fixes f g :: "real \<Rightarrow> real" shows |
2250 "\<lbrakk>a < x; x < b; |
2283 "\<lbrakk>a < x; x < b; |
2251 \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z; |
2284 \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z; |
2435 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0" |
2468 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0" |
2436 by (cut_tac x = x in sin_cos_squared_add3, auto) |
2469 by (cut_tac x = x in sin_cos_squared_add3, auto) |
2437 |
2470 |
2438 subsection {* Machins formula *} |
2471 subsection {* Machins formula *} |
2439 |
2472 |
|
2473 lemma arctan_one: "arctan 1 = pi / 4" |
|
2474 by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi) |
|
2475 |
2440 lemma tan_total_pi4: assumes "\<bar>x\<bar> < 1" |
2476 lemma tan_total_pi4: assumes "\<bar>x\<bar> < 1" |
2441 shows "\<exists> z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x" |
2477 shows "\<exists> z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x" |
2442 proof - |
2478 proof |
2443 obtain z where "- (pi / 2) < z" and "z < pi / 2" and "tan z = x" using tan_total by blast |
2479 show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x" |
2444 have "tan (pi / 4) = 1" and "tan (- (pi / 4)) = - 1" using tan_45 tan_minus by auto |
2480 unfolding arctan_one [symmetric] arctan_minus [symmetric] |
2445 have "z \<noteq> pi / 4" |
2481 unfolding arctan_less_iff using assms by auto |
2446 proof (rule ccontr) |
|
2447 assume "\<not> (z \<noteq> pi / 4)" hence "z = pi / 4" by auto |
|
2448 have "tan z = 1" unfolding `z = pi / 4` `tan (pi / 4) = 1` .. |
|
2449 thus False unfolding `tan z = x` using `\<bar>x\<bar> < 1` by auto |
|
2450 qed |
|
2451 have "z \<noteq> - (pi / 4)" |
|
2452 proof (rule ccontr) |
|
2453 assume "\<not> (z \<noteq> - (pi / 4))" hence "z = - (pi / 4)" by auto |
|
2454 have "tan z = - 1" unfolding `z = - (pi / 4)` `tan (- (pi / 4)) = - 1` .. |
|
2455 thus False unfolding `tan z = x` using `\<bar>x\<bar> < 1` by auto |
|
2456 qed |
|
2457 |
|
2458 have "z < pi / 4" |
|
2459 proof (rule ccontr) |
|
2460 assume "\<not> (z < pi / 4)" hence "pi / 4 < z" using `z \<noteq> pi / 4` by auto |
|
2461 have "- (pi / 2) < pi / 4" using m2pi_less_pi by auto |
|
2462 from tan_monotone[OF this `pi / 4 < z` `z < pi / 2`] |
|
2463 have "1 < x" unfolding `tan z = x` `tan (pi / 4) = 1` . |
|
2464 thus False using `\<bar>x\<bar> < 1` by auto |
|
2465 qed |
|
2466 moreover |
|
2467 have "-(pi / 4) < z" |
|
2468 proof (rule ccontr) |
|
2469 assume "\<not> (-(pi / 4) < z)" hence "z < - (pi / 4)" using `z \<noteq> - (pi / 4)` by auto |
|
2470 have "-(pi / 4) < pi / 2" using m2pi_less_pi by auto |
|
2471 from tan_monotone[OF `-(pi / 2) < z` `z < -(pi / 4)` this] |
|
2472 have "x < - 1" unfolding `tan z = x` `tan (-(pi / 4)) = - 1` . |
|
2473 thus False using `\<bar>x\<bar> < 1` by auto |
|
2474 qed |
|
2475 ultimately show ?thesis using `tan z = x` by auto |
|
2476 qed |
2482 qed |
2477 |
2483 |
2478 lemma arctan_add: assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1" |
2484 lemma arctan_add: assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1" |
2479 shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))" |
2485 shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))" |
2480 proof - |
2486 proof (rule arctan_unique [symmetric]) |
2481 obtain y' where "-(pi/4) < y'" and "y' < pi/4" and "tan y' = y" using tan_total_pi4[OF `\<bar>y\<bar> < 1`] by blast |
2487 have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y" |
2482 |
2488 unfolding arctan_one [symmetric] arctan_minus [symmetric] |
2483 have "pi / 4 < pi / 2" by auto |
2489 unfolding arctan_le_iff arctan_less_iff using assms by auto |
2484 |
2490 from add_le_less_mono [OF this] |
2485 have "\<exists> x'. -(pi/4) \<le> x' \<and> x' \<le> pi/4 \<and> tan x' = x" |
2491 show 1: "- (pi / 2) < arctan x + arctan y" by simp |
2486 proof (cases "\<bar>x\<bar> < 1") |
2492 have "arctan x \<le> pi / 4" and "arctan y < pi / 4" |
2487 case True from tan_total_pi4[OF this] obtain x' where "-(pi/4) < x'" and "x' < pi/4" and "tan x' = x" by blast |
2493 unfolding arctan_one [symmetric] |
2488 hence "-(pi/4) \<le> x'" and "x' \<le> pi/4" and "tan x' = x" by auto |
2494 unfolding arctan_le_iff arctan_less_iff using assms by auto |
2489 thus ?thesis by auto |
2495 from add_le_less_mono [OF this] |
2490 next |
2496 show 2: "arctan x + arctan y < pi / 2" by simp |
2491 case False |
2497 show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)" |
2492 show ?thesis |
2498 using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add) |
2493 proof (cases "x = 1") |
2499 qed |
2494 case True hence "tan (pi/4) = x" using tan_45 by auto |
|
2495 moreover |
|
2496 have "- pi \<le> pi" unfolding minus_le_self_iff by auto |
|
2497 hence "-(pi/4) \<le> pi/4" and "pi/4 \<le> pi/4" by auto |
|
2498 ultimately show ?thesis by blast |
|
2499 next |
|
2500 case False hence "x = -1" using `\<not> \<bar>x\<bar> < 1` and `\<bar>x\<bar> \<le> 1` by auto |
|
2501 hence "tan (-(pi/4)) = x" using tan_45 tan_minus by auto |
|
2502 moreover |
|
2503 have "- pi \<le> pi" unfolding minus_le_self_iff by auto |
|
2504 hence "-(pi/4) \<le> pi/4" and "-(pi/4) \<le> -(pi/4)" by auto |
|
2505 ultimately show ?thesis by blast |
|
2506 qed |
|
2507 qed |
|
2508 then obtain x' where "-(pi/4) \<le> x'" and "x' \<le> pi/4" and "tan x' = x" by blast |
|
2509 hence "-(pi/2) < x'" and "x' < pi/2" using order_le_less_trans[OF `x' \<le> pi/4` `pi / 4 < pi / 2`] by auto |
|
2510 |
|
2511 have "cos x' \<noteq> 0" using cos_gt_zero_pi[THEN less_imp_neq] and `-(pi/2) < x'` and `x' < pi/2` by auto |
|
2512 moreover have "cos y' \<noteq> 0" using cos_gt_zero_pi[THEN less_imp_neq] and `-(pi/4) < y'` and `y' < pi/4` by auto |
|
2513 ultimately have "cos x' * cos y' \<noteq> 0" by auto |
|
2514 |
|
2515 have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> (A / C) / (B / C) = A / B" by auto |
|
2516 have divide_mult_commute: "\<And> A B C D :: real. A * B / (C * D) = (A / C) * (B / D)" by auto |
|
2517 |
|
2518 have "tan (x' + y') = sin (x' + y') / (cos x' * cos y' - sin x' * sin y')" unfolding tan_def cos_add .. |
|
2519 also have "\<dots> = (tan x' + tan y') / ((cos x' * cos y' - sin x' * sin y') / (cos x' * cos y'))" unfolding add_tan_eq[OF `cos x' \<noteq> 0` `cos y' \<noteq> 0`] divide_nonzero_divide[OF `cos x' * cos y' \<noteq> 0`] .. |
|
2520 also have "\<dots> = (tan x' + tan y') / (1 - tan x' * tan y')" unfolding tan_def diff_divide_distrib divide_self[OF `cos x' * cos y' \<noteq> 0`] unfolding divide_mult_commute .. |
|
2521 finally have tan_eq: "tan (x' + y') = (x + y) / (1 - x * y)" unfolding `tan y' = y` `tan x' = x` . |
|
2522 |
|
2523 have "arctan (tan (x' + y')) = x' + y'" using `-(pi/4) < y'` `-(pi/4) \<le> x'` `y' < pi/4` and `x' \<le> pi/4` by (auto intro!: arctan_tan) |
|
2524 moreover have "arctan (tan (x')) = x'" using `-(pi/2) < x'` and `x' < pi/2` by (auto intro!: arctan_tan) |
|
2525 moreover have "arctan (tan (y')) = y'" using `-(pi/4) < y'` and `y' < pi/4` by (auto intro!: arctan_tan) |
|
2526 ultimately have "arctan x + arctan y = arctan (tan (x' + y'))" unfolding `tan y' = y` [symmetric] `tan x' = x`[symmetric] by auto |
|
2527 thus "arctan x + arctan y = arctan ((x + y) / (1 - x * y))" unfolding tan_eq . |
|
2528 qed |
|
2529 |
|
2530 lemma arctan1_eq_pi4: "arctan 1 = pi / 4" unfolding tan_45[symmetric] by (rule arctan_tan, auto simp add: m2pi_less_pi) |
|
2531 |
2500 |
2532 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)" |
2501 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)" |
2533 proof - |
2502 proof - |
2534 have "\<bar>1 / 5\<bar> < (1 :: real)" by auto |
2503 have "\<bar>1 / 5\<bar> < (1 :: real)" by auto |
2535 from arctan_add[OF less_imp_le[OF this] this] |
2504 from arctan_add[OF less_imp_le[OF this] this] |
2835 finally show ?thesis unfolding eq `tan y = x` . |
2805 finally show ?thesis unfolding eq `tan y = x` . |
2836 qed |
2806 qed |
2837 |
2807 |
2838 lemma arctan_monotone: assumes "x < y" |
2808 lemma arctan_monotone: assumes "x < y" |
2839 shows "arctan x < arctan y" |
2809 shows "arctan x < arctan y" |
2840 proof - |
2810 using assms by (simp only: arctan_less_iff) |
2841 obtain z where "-(pi / 2) < z" and "z < pi / 2" and "tan z = x" using tan_total by blast |
|
2842 obtain w where "-(pi / 2) < w" and "w < pi / 2" and "tan w = y" using tan_total by blast |
|
2843 have "z < w" unfolding tan_monotone'[OF `-(pi / 2) < z` `z < pi / 2` `-(pi / 2) < w` `w < pi / 2`] `tan z = x` `tan w = y` using `x < y` . |
|
2844 thus ?thesis |
|
2845 unfolding `tan z = x`[symmetric] arctan_tan[OF `-(pi / 2) < z` `z < pi / 2`] |
|
2846 unfolding `tan w = y`[symmetric] arctan_tan[OF `-(pi / 2) < w` `w < pi / 2`] . |
|
2847 qed |
|
2848 |
2811 |
2849 lemma arctan_monotone': assumes "x \<le> y" shows "arctan x \<le> arctan y" |
2812 lemma arctan_monotone': assumes "x \<le> y" shows "arctan x \<le> arctan y" |
2850 proof (cases "x = y") |
2813 using assms by (simp only: arctan_le_iff) |
2851 case False hence "x < y" using `x \<le> y` by auto from arctan_monotone[OF this] show ?thesis by auto |
2814 |
2852 qed auto |
2815 lemma arctan_inverse: |
2853 |
2816 assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x" |
2854 lemma arctan_minus: "arctan (- x) = - arctan x" |
2817 proof (rule arctan_unique) |
2855 proof - |
2818 show "- (pi / 2) < sgn x * pi / 2 - arctan x" |
2856 obtain y where "- (pi / 2) < y" and "y < pi / 2" and "tan y = x" using tan_total by blast |
2819 using arctan_bounded [of x] assms |
2857 thus ?thesis unfolding `tan y = x`[symmetric] tan_minus[symmetric] using arctan_tan[of y] arctan_tan[of "-y"] by auto |
2820 unfolding sgn_real_def |
2858 qed |
2821 apply (auto simp add: algebra_simps) |
2859 |
2822 apply (drule zero_less_arctan_iff [THEN iffD2]) |
2860 lemma arctan_inverse: assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x" |
2823 apply arith |
2861 proof - |
2824 done |
2862 obtain y where "- (pi / 2) < y" and "y < pi / 2" and "tan y = x" using tan_total by blast |
2825 show "sgn x * pi / 2 - arctan x < pi / 2" |
2863 hence "y = arctan x" unfolding `tan y = x`[symmetric] using arctan_tan by auto |
2826 using arctan_bounded [of "- x"] assms |
2864 |
2827 unfolding sgn_real_def arctan_minus |
2865 { fix y x :: real assume "0 < y" and "y < pi /2" and "y = arctan x" and "tan y = x" hence "- (pi / 2) < y" by auto |
2828 by auto |
2866 have "tan y > 0" using tan_monotone'[OF _ _ `- (pi / 2) < y` `y < pi / 2`, of 0] tan_zero `0 < y` by auto |
2829 show "tan (sgn x * pi / 2 - arctan x) = 1 / x" |
2867 hence "x > 0" using `tan y = x` by auto |
2830 unfolding tan_inverse [of "arctan x", unfolded tan_arctan] |
2868 |
2831 unfolding sgn_real_def |
2869 have "- (pi / 2) < pi / 2 - y" using `y > 0` `y < pi / 2` by auto |
2832 by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff) |
2870 moreover have "pi / 2 - y < pi / 2" using `y > 0` `y < pi / 2` by auto |
|
2871 ultimately have "arctan (1 / x) = pi / 2 - y" unfolding `tan y = x`[symmetric] tan_inverse using arctan_tan by auto |
|
2872 hence "arctan (1 / x) = sgn x * pi / 2 - arctan x" unfolding `y = arctan x` real_sgn_pos[OF `x > 0`] by auto |
|
2873 } note pos_y = this |
|
2874 |
|
2875 show ?thesis |
|
2876 proof (cases "y > 0") |
|
2877 case True from pos_y[OF this `y < pi / 2` `y = arctan x` `tan y = x`] show ?thesis . |
|
2878 next |
|
2879 case False hence "y \<le> 0" by auto |
|
2880 moreover have "y \<noteq> 0" |
|
2881 proof (rule ccontr) |
|
2882 assume "\<not> y \<noteq> 0" hence "y = 0" by auto |
|
2883 have "x = 0" unfolding `tan y = x`[symmetric] `y = 0` tan_zero .. |
|
2884 thus False using `x \<noteq> 0` by auto |
|
2885 qed |
|
2886 ultimately have "y < 0" by auto |
|
2887 hence "0 < - y" and "-y < pi / 2" using `- (pi / 2) < y` by auto |
|
2888 moreover have "-y = arctan (-x)" unfolding arctan_minus `y = arctan x` .. |
|
2889 moreover have "tan (-y) = -x" unfolding tan_minus `tan y = x` .. |
|
2890 ultimately have "arctan (1 / -x) = sgn (-x) * pi / 2 - arctan (-x)" using pos_y by blast |
|
2891 hence "arctan (- (1 / x)) = - (sgn x * pi / 2 - arctan x)" unfolding arctan_minus[of x] divide_minus_right sgn_minus by auto |
|
2892 thus ?thesis unfolding arctan_minus neg_equal_iff_equal . |
|
2893 qed |
|
2894 qed |
2833 qed |
2895 |
2834 |
2896 theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM") |
2835 theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM") |
2897 proof - |
2836 proof - |
2898 have "pi / 4 = arctan 1" using arctan1_eq_pi4 by auto |
2837 have "pi / 4 = arctan 1" using arctan_one by auto |
2899 also have "\<dots> = ?SUM" using arctan_series[of 1] by auto |
2838 also have "\<dots> = ?SUM" using arctan_series[of 1] by auto |
2900 finally show ?thesis by auto |
2839 finally show ?thesis by auto |
2901 qed |
2840 qed |
2902 |
2841 |
2903 subsection {* Existence of Polar Coordinates *} |
2842 subsection {* Existence of Polar Coordinates *} |