1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Fri Apr 03 21:25:55 2015 +0200
     1.3 @@ -0,0 +1,38 @@
     1.4 +section {* Binary Approximations to Constants *}
     1.5 +
     1.6 +theory Approximations
     1.7 +imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental"
     1.8 +begin
     1.9 +
    1.10 +declare of_real_numeral [simp]
    1.11 +
    1.12 +subsection{*Approximation to pi*}
    1.13 +
    1.14 +lemma sin_pi6_straddle:
    1.15 +  assumes "0 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)"
    1.16 +    shows "a \<le> pi \<and> pi \<le> b"
    1.17 +proof -
    1.18 +  have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 0 < sin x"
    1.19 +    using pi_ge_two
    1.20 +    by (auto intro: sin_gt_zero)
    1.21 +  have ab: "(b \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> pi)"
    1.22 +    using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms
    1.23 +    by (simp_all add: sin_30 power.power_Suc norm_divide)
    1.24 +  show ?thesis
    1.25 +    using assms Taylor_sin [of "a/6" 0] pi_ge_two
    1.26 +    by (auto simp: sin_30 power.power_Suc norm_divide intro: ab)
    1.27 +qed
    1.28 +
    1.29 +(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*)
    1.30 +lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)"
    1.31 +  apply (simp only: abs_diff_le_iff)
    1.32 +  apply (rule sin_pi6_straddle, simp_all)
    1.33 +  using Taylor_sin [of "1686629713/3221225472" 11]
    1.34 +  apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
    1.35 +  apply (simp only: pos_le_divide_eq [symmetric])
    1.36 +  using Taylor_sin [of "6746518853/12884901888" 11]
    1.37 +  apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
    1.38 +  apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric])
    1.39 +  done
    1.40 +
    1.41 +end

     2.1 --- a/src/HOL/ROOT	Fri Apr 03 21:04:56 2015 +0200
     2.2 +++ b/src/HOL/ROOT	Fri Apr 03 21:25:55 2015 +0200
     2.3 @@ -527,7 +527,6 @@
     2.4      "~~/src/HOL/Library/Transitive_Closure_Table"
     2.5      Cartouche_Examples
     2.6    theories
     2.7 -    Approximations
     2.8      Commands
     2.9      Adhoc_Overloading_Examples
    2.10      Iff_Oracle
    2.11 @@ -693,6 +692,10 @@
    2.12    document_files
    2.13      "root.tex"
    2.14  
    2.15 +session "HOL-Multivariate_Analysis-ex" in "Multivariate_Analysis/ex" = "HOL-Multivariate_Analysis" +
    2.16 +  theories
    2.17 +    Approximations
    2.18 +
    2.19  session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
    2.20    theories [document = false]
    2.21      "~~/src/HOL/Library/Countable"

     3.1 --- a/src/HOL/ex/Approximations.thy	Fri Apr 03 21:04:56 2015 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,39 +0,0 @@
     3.4 -section {* Binary Approximations to Constants *}
     3.5 -
     3.6 -theory Approximations
     3.7 -imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental"
     3.8 -
     3.9 -begin
    3.10 -
    3.11 -declare of_real_numeral [simp]
    3.12 -
    3.13 -subsection{*Approximation to pi*}
    3.14 -
    3.15 -lemma sin_pi6_straddle:
    3.16 -  assumes "0 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)"
    3.17 -    shows "a \<le> pi \<and> pi \<le> b"
    3.18 -proof -
    3.19 -  have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 0 < sin x"
    3.20 -    using pi_ge_two
    3.21 -    by (auto intro: sin_gt_zero)
    3.22 -  have ab: "(b \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> pi)"
    3.23 -    using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms
    3.24 -    by (simp_all add: sin_30 power.power_Suc norm_divide)
    3.25 -  show ?thesis
    3.26 -    using assms Taylor_sin [of "a/6" 0] pi_ge_two
    3.27 -    by (auto simp: sin_30 power.power_Suc norm_divide intro: ab)
    3.28 -qed
    3.29 -
    3.30 -(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*)
    3.31 -lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)"
    3.32 -  apply (simp only: abs_diff_le_iff)
    3.33 -  apply (rule sin_pi6_straddle, simp_all)
    3.34 -  using Taylor_sin [of "1686629713/3221225472" 11]
    3.35 -  apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
    3.36 -  apply (simp only: pos_le_divide_eq [symmetric])
    3.37 -  using Taylor_sin [of "6746518853/12884901888" 11]
    3.38 -  apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
    3.39 -  apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric])
    3.40 -  done
    3.41 -
    3.42 -end