author | wenzelm |
Tue, 03 Nov 2015 16:47:37 +0100 | |
changeset 61560 | 7c985fd653c5 |
parent 61286 | dcf7be51bf5d |
child 61694 | 6571c78c9667 |
permissions | -rw-r--r-- |
60420 | 1 |
section \<open>Binary Approximations to Constants\<close> |
59871
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
|
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
theory Approximations |
61560 | 4 |
imports Complex_Transcendental |
59871
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
begin |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
|
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
declare of_real_numeral [simp] |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
|
60420 | 9 |
subsection\<open>Approximation to pi\<close> |
59871
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
|
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
11 |
lemma sin_pi6_straddle: |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
assumes "0 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)" |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
shows "a \<le> pi \<and> pi \<le> b" |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
proof - |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 0 < sin x" |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
using pi_ge_two |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
by (auto intro: sin_gt_zero) |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
have ab: "(b \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> pi)" |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
20 |
by (simp_all add: sin_30 power.power_Suc norm_divide) |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
show ?thesis |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
using assms Taylor_sin [of "a/6" 0] pi_ge_two |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
by (auto simp: sin_30 power.power_Suc norm_divide intro: ab) |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
qed |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
|
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*) |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)" |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
28 |
apply (simp only: abs_diff_le_iff) |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
apply (rule sin_pi6_straddle, simp_all) |
61286 | 30 |
using Taylor_sin [of "1686629713/3221225472" 11] |
59871
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
61286 | 32 |
apply (simp only: pos_le_divide_eq [symmetric]) |
59871
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
using Taylor_sin [of "6746518853/12884901888" 11] |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric]) |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
done |
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
|
e1a49ac9c537
John Harrison's example: a 32-bit approximation to pi. SLOW
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
end |