src/HOL/ex/Approximations.thy
author paulson <lp15@cam.ac.uk>
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 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)"
lp15@59871
    14
    shows "a \<le> pi \<and> pi \<le> b"
lp15@59871
    15
proof -
lp15@59871
    16
  have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 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 \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> 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) \<le> 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