rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
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