equal
deleted
inserted
replaced
25 |
25 |
26 (*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*) |
26 (*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*) |
27 lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)" |
27 lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)" |
28 apply (simp only: abs_diff_le_iff) |
28 apply (simp only: abs_diff_le_iff) |
29 apply (rule sin_pi6_straddle, simp_all) |
29 apply (rule sin_pi6_straddle, simp_all) |
30 using Taylor_sin [of "1686629713/3221225472" 11] |
30 using Taylor_sin [of "1686629713/3221225472" 11] |
31 apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
31 apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
32 apply (simp only: pos_le_divide_eq [symmetric]) |
32 apply (simp only: pos_le_divide_eq [symmetric]) |
33 using Taylor_sin [of "6746518853/12884901888" 11] |
33 using Taylor_sin [of "6746518853/12884901888" 11] |
34 apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
34 apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) |
35 apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric]) |
35 apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric]) |
36 done |
36 done |
37 |
37 |