src/HOL/ex/Approximations.thy
 author paulson Wed Apr 01 15:47:55 2015 +0100 (2015-04-01) changeset 59871 e1a49ac9c537 permissions -rw-r--r--
John Harrison's example: a 32-bit approximation to pi. SLOW
 lp15@59871 ` 1` ```section {* Binary Approximations to Constants *} ``` lp15@59871 ` 2` lp15@59871 ` 3` ```theory Approximations ``` lp15@59871 ` 4` ```imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental" ``` lp15@59871 ` 5` lp15@59871 ` 6` ```begin ``` lp15@59871 ` 7` lp15@59871 ` 8` ```declare of_real_numeral [simp] ``` lp15@59871 ` 9` lp15@59871 ` 10` ```subsection{*Approximation to pi*} ``` lp15@59871 ` 11` lp15@59871 ` 12` ```lemma sin_pi6_straddle: ``` lp15@59871 ` 13` ``` assumes "0 \ a" "a \ b" "b \ 4" "sin(a/6) \ 1/2" "1/2 \ sin(b/6)" ``` lp15@59871 ` 14` ``` shows "a \ pi \ pi \ b" ``` lp15@59871 ` 15` ```proof - ``` lp15@59871 ` 16` ``` have *: "\x::real. 0 < x & x < 7/5 \ 0 < sin x" ``` lp15@59871 ` 17` ``` using pi_ge_two ``` lp15@59871 ` 18` ``` by (auto intro: sin_gt_zero) ``` lp15@59871 ` 19` ``` have ab: "(b \ pi * 3 \ pi \ b)" "(a \ pi * 3 \ a \ pi)" ``` lp15@59871 ` 20` ``` using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms ``` lp15@59871 ` 21` ``` by (simp_all add: sin_30 power.power_Suc norm_divide) ``` lp15@59871 ` 22` ``` show ?thesis ``` lp15@59871 ` 23` ``` using assms Taylor_sin [of "a/6" 0] pi_ge_two ``` lp15@59871 ` 24` ``` by (auto simp: sin_30 power.power_Suc norm_divide intro: ab) ``` lp15@59871 ` 25` ```qed ``` lp15@59871 ` 26` lp15@59871 ` 27` ```(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*) ``` lp15@59871 ` 28` ```lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \ inverse(2 ^ 32)" ``` lp15@59871 ` 29` ``` apply (simp only: abs_diff_le_iff) ``` lp15@59871 ` 30` ``` apply (rule sin_pi6_straddle, simp_all) ``` lp15@59871 ` 31` ``` using Taylor_sin [of "1686629713/3221225472" 11] ``` lp15@59871 ` 32` ``` apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) ``` lp15@59871 ` 33` ``` apply (simp only: pos_le_divide_eq [symmetric]) ``` lp15@59871 ` 34` ``` using Taylor_sin [of "6746518853/12884901888" 11] ``` lp15@59871 ` 35` ``` apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) ``` lp15@59871 ` 36` ``` apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric]) ``` lp15@59871 ` 37` ``` done ``` lp15@59871 ` 38` lp15@59871 ` 39` ```end ```