John Harrison's example: a 32-bit approximation to pi. SLOW
authorpaulson <lp15@cam.ac.uk>
Wed Apr 01 15:47:55 2015 +0100 (2015-04-01)
changeset 59871e1a49ac9c537
parent 59870 68d6b6aa4450
child 59872 db4000b71fdb
John Harrison's example: a 32-bit approximation to pi. SLOW
src/HOL/ROOT
src/HOL/ex/Approximations.thy
src/HOL/ex/BinEx.thy
     1.1 --- a/src/HOL/ROOT	Wed Apr 01 14:48:38 2015 +0100
     1.2 +++ b/src/HOL/ROOT	Wed Apr 01 15:47:55 2015 +0100
     1.3 @@ -527,6 +527,7 @@
     1.4      "~~/src/HOL/Library/Transitive_Closure_Table"
     1.5      Cartouche_Examples
     1.6    theories
     1.7 +    Approximations
     1.8      Commands
     1.9      Adhoc_Overloading_Examples
    1.10      Iff_Oracle
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Approximations.thy	Wed Apr 01 15:47:55 2015 +0100
     2.3 @@ -0,0 +1,39 @@
     2.4 +section {* Binary Approximations to Constants *}
     2.5 +
     2.6 +theory Approximations
     2.7 +imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental"
     2.8 +
     2.9 +begin
    2.10 +
    2.11 +declare of_real_numeral [simp]
    2.12 +
    2.13 +subsection{*Approximation to pi*}
    2.14 +
    2.15 +lemma sin_pi6_straddle:
    2.16 +  assumes "0 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)"
    2.17 +    shows "a \<le> pi \<and> pi \<le> b"
    2.18 +proof -
    2.19 +  have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 0 < sin x"
    2.20 +    using pi_ge_two
    2.21 +    by (auto intro: sin_gt_zero)
    2.22 +  have ab: "(b \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> pi)"
    2.23 +    using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms
    2.24 +    by (simp_all add: sin_30 power.power_Suc norm_divide)
    2.25 +  show ?thesis
    2.26 +    using assms Taylor_sin [of "a/6" 0] pi_ge_two
    2.27 +    by (auto simp: sin_30 power.power_Suc norm_divide intro: ab)
    2.28 +qed
    2.29 +
    2.30 +(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*)
    2.31 +lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)"
    2.32 +  apply (simp only: abs_diff_le_iff)
    2.33 +  apply (rule sin_pi6_straddle, simp_all)
    2.34 +  using Taylor_sin [of "1686629713/3221225472" 11]
    2.35 +  apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
    2.36 +  apply (simp only: pos_le_divide_eq [symmetric])
    2.37 +  using Taylor_sin [of "6746518853/12884901888" 11]
    2.38 +  apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
    2.39 +  apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric])
    2.40 +  done
    2.41 +
    2.42 +end
     3.1 --- a/src/HOL/ex/BinEx.thy	Wed Apr 01 14:48:38 2015 +0100
     3.2 +++ b/src/HOL/ex/BinEx.thy	Wed Apr 01 15:47:55 2015 +0100
     3.3 @@ -78,6 +78,9 @@
     3.4  lemma "- (2*i) + 3  + (2*i + 4) = (0::int)"
     3.5  apply simp  oops
     3.6  
     3.7 +(*Tobias's example dated 2015-03-02*)
     3.8 +lemma "(pi * (real u * 2) = pi * (real (xa v) * - 2))"
     3.9 +apply simp oops
    3.10  
    3.11  
    3.12  subsection {* Arithmetic Method Tests *}