equal
deleted
inserted
replaced
|
1 section {* Binary Approximations to Constants *} |
|
2 |
|
3 theory Approximations |
|
4 imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental" |
|
5 |
|
6 begin |
|
7 |
|
8 declare of_real_numeral [simp] |
|
9 |
|
10 subsection{*Approximation to pi*} |
|
11 |
|
12 lemma sin_pi6_straddle: |
|
13 assumes "0 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)" |
|
14 shows "a \<le> pi \<and> pi \<le> b" |
|
15 proof - |
|
16 have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 0 < sin x" |
|
17 using pi_ge_two |
|
18 by (auto intro: sin_gt_zero) |
|
19 have ab: "(b \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> pi)" |
|
20 using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms |
|
21 by (simp_all add: sin_30 power.power_Suc norm_divide) |
|
22 show ?thesis |
|
23 using assms Taylor_sin [of "a/6" 0] pi_ge_two |
|
24 by (auto simp: sin_30 power.power_Suc norm_divide intro: ab) |
|
25 qed |
|
26 |
|
27 (*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*) |
|
28 lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)" |
|
29 apply (simp only: abs_diff_le_iff) |
|
30 apply (rule sin_pi6_straddle, simp_all) |
|
31 using Taylor_sin [of "1686629713/3221225472" 11] |
|
32 apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
|
33 apply (simp only: pos_le_divide_eq [symmetric]) |
|
34 using Taylor_sin [of "6746518853/12884901888" 11] |
|
35 apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
|
36 apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric]) |
|
37 done |
|
38 |
|
39 end |