1.1 --- a/src/HOL/Decision_Procs/Approximation.thy Thu Jun 25 17:07:28 2009 +0200
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Mon Jun 15 12:14:40 2009 +0200
1.3 @@ -38,7 +38,7 @@
1.4 and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
1.5 and ub_0: "\<And> i k x. ub 0 i k x = 0"
1.6 and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
1.7 - shows "real (lb n ((F ^^ j') s) (f j') x) \<le> horner F G n ((F ^^ j') s) (f j') (real x) \<and>
1.8 + shows "real (lb n ((F ^^ j') s) (f j') x) \<le> horner F G n ((F ^^ j') s) (f j') (real x) \<and>
1.9 horner F G n ((F ^^ j') s) (f j') (real x) \<le> real (ub n ((F ^^ j') s) (f j') x)"
1.10 (is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'")
1.11 proof (induct n arbitrary: j')
1.12 @@ -56,7 +56,7 @@
1.13 proof (rule add_mono)
1.14 show "1 / real (f j') \<le> real (rapprox_rat prec 1 (int (f j')))" using rapprox_rat[of 1 "int (f j')" prec] by auto
1.15 from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> real x`
1.16 - show "- (real x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (real x)) \<le>
1.17 + show "- (real x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (real x)) \<le>
1.18 - real (x * lb n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x)"
1.19 unfolding real_of_float_mult neg_le_iff_le by (rule mult_left_mono)
1.20 qed
1.21 @@ -78,10 +78,10 @@
1.22 and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
1.23 and ub_0: "\<And> i k x. ub 0 i k x = 0"
1.24 and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
1.25 - shows "real (lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * real x ^ j)" (is "?lb") and
1.26 + shows "real (lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * real x ^ j)" (is "?lb") and
1.27 "(\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * (real x ^ j)) \<le> real (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
1.28 proof -
1.29 - have "?lb \<and> ?ub"
1.30 + have "?lb \<and> ?ub"
1.31 using horner_bounds'[where lb=lb, OF `0 \<le> real x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
1.32 unfolding horner_schema[where f=f, OF f_Suc] .
1.33 thus "?lb" and "?ub" by auto
1.34 @@ -93,7 +93,7 @@
1.35 and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) + x * (ub n (F i) (G i k) x)"
1.36 and ub_0: "\<And> i k x. ub 0 i k x = 0"
1.37 and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) + x * (lb n (F i) (G i k) x)"
1.38 - shows "real (lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * real x ^ j)" (is "?lb") and
1.39 + shows "real (lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * real x ^ j)" (is "?lb") and
1.40 "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (real x ^ j)) \<le> real (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
1.41 proof -
1.42 { fix x y z :: float have "x - y * z = x + - y * z"
1.43 @@ -104,7 +104,7 @@
1.44
1.45 have move_minus: "real (-x) = -1 * real x" by auto
1.46
1.47 - have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * real x ^ j) =
1.48 + have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * real x ^ j) =
1.49 (\<Sum>j = 0..<n. -1 ^ j * (1 / real (f (j' + j))) * real (- x) ^ j)"
1.50 proof (rule setsum_cong, simp)
1.51 fix j assume "j \<in> {0 ..< n}"
1.52 @@ -174,7 +174,7 @@
1.53 show ?thesis
1.54 proof (cases "u < 0")
1.55 case True hence "0 \<le> - real u" and "- real u \<le> - x" and "0 \<le> - x" and "-x \<le> - real l" using assms unfolding less_float_def by auto
1.56 - hence "real u ^ n \<le> x ^ n" and "x ^ n \<le> real l ^ n" using power_mono[of "-x" "-real l" n] power_mono[of "-real u" "-x" n]
1.57 + hence "real u ^ n \<le> x ^ n" and "x ^ n \<le> real l ^ n" using power_mono[of "-x" "-real l" n] power_mono[of "-real u" "-x" n]
1.58 unfolding power_minus_even[OF `even n`] by auto
1.59 moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
1.60 ultimately show ?thesis using float_power by auto
1.61 @@ -315,7 +315,7 @@
1.62 shows "0 \<le> real (lb_sqrt prec x)"
1.63 proof (cases "0 < x")
1.64 case True hence "0 < real x" and "0 \<le> x" using `0 \<le> real x` unfolding less_float_def le_float_def by auto
1.65 - hence "0 < sqrt_iteration prec prec x" unfolding less_float_def using sqrt_iteration_lower_bound by auto
1.66 + hence "0 < sqrt_iteration prec prec x" unfolding less_float_def using sqrt_iteration_lower_bound by auto
1.67 hence "0 \<le> real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF `0 \<le> x`] unfolding le_float_def by auto
1.68 thus ?thesis unfolding lb_sqrt.simps using True by auto
1.69 next
1.70 @@ -336,7 +336,7 @@
1.71 also have "\<dots> < real x / sqrt (real x)"
1.72 by (rule divide_strict_left_mono[OF sqrt_ub `0 < real x`
1.73 mult_pos_pos[OF order_less_trans[OF sqrt_gt0 sqrt_ub] sqrt_gt0]])
1.74 - also have "\<dots> = sqrt (real x)"
1.75 + also have "\<dots> = sqrt (real x)"
1.76 unfolding inverse_eq_iff_eq[of _ "sqrt (real x)", symmetric]
1.77 sqrt_divide_self_eq[OF `0 \<le> real x`, symmetric] by auto
1.78 finally have "real (lb_sqrt prec x) \<le> sqrt (real x)"
1.79 @@ -357,7 +357,7 @@
1.80 case True with lb ub show ?thesis by auto
1.81 next case False show ?thesis
1.82 proof (cases "real x = 0")
1.83 - case True thus ?thesis
1.84 + case True thus ?thesis
1.85 by (auto simp add: less_float_def lb_sqrt.simps ub_sqrt.simps)
1.86 next
1.87 case False with `\<not> 0 < x` have "x < 0" and "0 < -x"
1.88 @@ -399,10 +399,10 @@
1.89 fun ub_arctan_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
1.90 and lb_arctan_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
1.91 "ub_arctan_horner prec 0 k x = 0"
1.92 -| "ub_arctan_horner prec (Suc n) k x =
1.93 +| "ub_arctan_horner prec (Suc n) k x =
1.94 (rapprox_rat prec 1 (int k)) - x * (lb_arctan_horner prec n (k + 2) x)"
1.95 | "lb_arctan_horner prec 0 k x = 0"
1.96 -| "lb_arctan_horner prec (Suc n) k x =
1.97 +| "lb_arctan_horner prec (Suc n) k x =
1.98 (lapprox_rat prec 1 (int k)) - x * (ub_arctan_horner prec n (k + 2) x)"
1.99
1.100 lemma arctan_0_1_bounds': assumes "0 \<le> real x" "real x \<le> 1" and "even n"
1.101 @@ -413,12 +413,12 @@
1.102
1.103 have "0 \<le> real (x * x)" by auto
1.104 from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
1.105 -
1.106 +
1.107 have "arctan (real x) \<in> { ?S n .. ?S (Suc n) }"
1.108 proof (cases "real x = 0")
1.109 case False
1.110 hence "0 < real x" using `0 \<le> real x` by auto
1.111 - hence prem: "0 < 1 / real (0 * 2 + (1::nat)) * real x ^ (0 * 2 + 1)" by auto
1.112 + hence prem: "0 < 1 / real (0 * 2 + (1::nat)) * real x ^ (0 * 2 + 1)" by auto
1.113
1.114 have "\<bar> real x \<bar> \<le> 1" using `0 \<le> real x` `real x \<le> 1` by auto
1.115 from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`]
1.116 @@ -428,9 +428,9 @@
1.117
1.118 have F: "\<And>n. 2 * Suc n + 1 = 2 * n + 1 + 2" by auto
1.119
1.120 - note bounds = horner_bounds[where s=1 and f="\<lambda>i. 2 * i + 1" and j'=0
1.121 + note bounds = horner_bounds[where s=1 and f="\<lambda>i. 2 * i + 1" and j'=0
1.122 and lb="\<lambda>n i k x. lb_arctan_horner prec n k x"
1.123 - and ub="\<lambda>n i k x. ub_arctan_horner prec n k x",
1.124 + and ub="\<lambda>n i k x. ub_arctan_horner prec n k x",
1.125 OF `0 \<le> real (x*x)` F lb_arctan_horner.simps ub_arctan_horner.simps]
1.126
1.127 { have "real (x * lb_arctan_horner prec n 1 (x*x)) \<le> ?S n"
1.128 @@ -481,15 +481,15 @@
1.129 subsection "Compute \<pi>"
1.130
1.131 definition ub_pi :: "nat \<Rightarrow> float" where
1.132 - "ub_pi prec = (let A = rapprox_rat prec 1 5 ;
1.133 + "ub_pi prec = (let A = rapprox_rat prec 1 5 ;
1.134 B = lapprox_rat prec 1 239
1.135 - in ((Float 1 2) * ((Float 1 2) * A * (ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (A * A)) -
1.136 + in ((Float 1 2) * ((Float 1 2) * A * (ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (A * A)) -
1.137 B * (lb_arctan_horner prec (get_even (prec div 14 + 1)) 1 (B * B)))))"
1.138
1.139 definition lb_pi :: "nat \<Rightarrow> float" where
1.140 - "lb_pi prec = (let A = lapprox_rat prec 1 5 ;
1.141 + "lb_pi prec = (let A = lapprox_rat prec 1 5 ;
1.142 B = rapprox_rat prec 1 239
1.143 - in ((Float 1 2) * ((Float 1 2) * A * (lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (A * A)) -
1.144 + in ((Float 1 2) * ((Float 1 2) * A * (lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (A * A)) -
1.145 B * (ub_arctan_horner prec (get_odd (prec div 14 + 1)) 1 (B * B)))))"
1.146
1.147 lemma pi_boundaries: "pi \<in> {real (lb_pi n) .. real (ub_pi n)}"
1.148 @@ -499,7 +499,7 @@
1.149 { fix prec n :: nat fix k :: int assume "1 < k" hence "0 \<le> k" and "0 < k" and "1 \<le> k" by auto
1.150 let ?k = "rapprox_rat prec 1 k"
1.151 have "1 div k = 0" using div_pos_pos_trivial[OF _ `1 < k`] by auto
1.152 -
1.153 +
1.154 have "0 \<le> real ?k" by (rule order_trans[OF _ rapprox_rat], auto simp add: `0 \<le> k`)
1.155 have "real ?k \<le> 1" unfolding rapprox_rat.simps(2)[OF zero_le_one `0 < k`]
1.156 by (rule rapprox_posrat_le1, auto simp add: `0 < k` `1 \<le> k`)
1.157 @@ -616,7 +616,7 @@
1.158 using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
1.159 also have "\<dots> \<le> 2 * arctan (real x / ?R)"
1.160 using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
1.161 - also have "2 * arctan (real x / ?R) = arctan (real x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
1.162 + also have "2 * arctan (real x / ?R) = arctan (real x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
1.163 finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
1.164 next
1.165 case False
1.166 @@ -629,7 +629,7 @@
1.167 show ?thesis
1.168 proof (cases "1 < ?invx")
1.169 case True
1.170 - show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] if_P[OF True]
1.171 + show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] if_P[OF True]
1.172 using `0 \<le> arctan (real x)` by auto
1.173 next
1.174 case False
1.175 @@ -731,7 +731,7 @@
1.176 have "real (?lb_horner ?invx) \<le> arctan (real ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
1.177 also have "\<dots> \<le> arctan (1 / real x)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divl)
1.178 finally have "arctan (real x) \<le> pi / 2 - real (?lb_horner ?invx)"
1.179 - using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
1.180 + using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
1.181 unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
1.182 moreover
1.183 have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto
1.184 @@ -780,10 +780,10 @@
1.185 fun ub_sin_cos_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
1.186 and lb_sin_cos_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
1.187 "ub_sin_cos_aux prec 0 i k x = 0"
1.188 -| "ub_sin_cos_aux prec (Suc n) i k x =
1.189 +| "ub_sin_cos_aux prec (Suc n) i k x =
1.190 (rapprox_rat prec 1 (int k)) - x * (lb_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
1.191 | "lb_sin_cos_aux prec 0 i k x = 0"
1.192 -| "lb_sin_cos_aux prec (Suc n) i k x =
1.193 +| "lb_sin_cos_aux prec (Suc n) i k x =
1.194 (lapprox_rat prec 1 (int k)) - x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
1.195
1.196 lemma cos_aux:
1.197 @@ -793,12 +793,12 @@
1.198 have "0 \<le> real (x * x)" unfolding real_of_float_mult by auto
1.199 let "?f n" = "fact (2 * n)"
1.200
1.201 - { fix n
1.202 + { fix n
1.203 have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
1.204 have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 1 * (((\<lambda>i. i + 2) ^^ n) 1 + 1)"
1.205 unfolding F by auto } note f_eq = this
1.206 -
1.207 - from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
1.208 +
1.209 + from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
1.210 OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
1.211 show "?lb" and "?ub" by (auto simp add: power_mult power2_eq_square[of "real x"])
1.212 qed
1.213 @@ -815,7 +815,7 @@
1.214 = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
1.215 proof -
1.216 have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
1.217 - also have "\<dots> =
1.218 + also have "\<dots> =
1.219 (\<Sum> j = 0 ..< n. -1 ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
1.220 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
1.221 unfolding sum_split_even_odd ..
1.222 @@ -828,8 +828,8 @@
1.223 { fix n :: nat assume "0 < n"
1.224 hence "0 < 2 * n" by auto
1.225 obtain t where "0 < t" and "t < real x" and
1.226 - cos_eq: "cos (real x) = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
1.227 - + (cos (t + 1/2 * real (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
1.228 + cos_eq: "cos (real x) = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
1.229 + + (cos (t + 1/2 * real (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
1.230 (is "_ = ?SUM + ?rest / ?fact * ?pow")
1.231 using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] by auto
1.232
1.233 @@ -848,7 +848,7 @@
1.234 {
1.235 assume "even n"
1.236 have "real (lb_sin_cos_aux prec n 1 1 (x * x)) \<le> ?SUM"
1.237 - unfolding morph_to_if_power[symmetric] using cos_aux by auto
1.238 + unfolding morph_to_if_power[symmetric] using cos_aux by auto
1.239 also have "\<dots> \<le> cos (real x)"
1.240 proof -
1.241 from even[OF `even n`] `0 < ?fact` `0 < ?pow`
1.242 @@ -874,7 +874,7 @@
1.243 } note ub = this(1) and lb = this(2)
1.244
1.245 have "cos (real x) \<le> real (ub_sin_cos_aux prec (get_odd n) 1 1 (x * x))" using ub[OF odd_pos[OF get_odd] get_odd] .
1.246 - moreover have "real (lb_sin_cos_aux prec (get_even n) 1 1 (x * x)) \<le> cos (real x)"
1.247 + moreover have "real (lb_sin_cos_aux prec (get_even n) 1 1 (x * x)) \<le> cos (real x)"
1.248 proof (cases "0 < get_even n")
1.249 case True show ?thesis using lb[OF True get_even] .
1.250 next
1.251 @@ -889,7 +889,7 @@
1.252 case True
1.253 show ?thesis
1.254 proof (cases "n = 0")
1.255 - case True
1.256 + case True
1.257 thus ?thesis unfolding `n = 0` get_even_def get_odd_def using `real x = 0` lapprox_rat[where x="-1" and y=1] by auto
1.258 next
1.259 case False with not0_implies_Suc obtain m where "n = Suc m" by blast
1.260 @@ -904,11 +904,11 @@
1.261 have "0 \<le> real (x * x)" unfolding real_of_float_mult by auto
1.262 let "?f n" = "fact (2 * n + 1)"
1.263
1.264 - { fix n
1.265 + { fix n
1.266 have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
1.267 have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
1.268 unfolding F by auto } note f_eq = this
1.269 -
1.270 +
1.271 from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
1.272 OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
1.273 show "?lb" and "?ub" using `0 \<le> real x` unfolding real_of_float_mult
1.274 @@ -940,8 +940,8 @@
1.275 { fix n :: nat assume "0 < n"
1.276 hence "0 < 2 * n + 1" by auto
1.277 obtain t where "0 < t" and "t < real x" and
1.278 - sin_eq: "sin (real x) = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
1.279 - + (sin (t + 1/2 * real (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
1.280 + sin_eq: "sin (real x) = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
1.281 + + (sin (t + 1/2 * real (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
1.282 (is "_ = ?SUM + ?rest / ?fact * ?pow")
1.283 using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] by auto
1.284
1.285 @@ -956,7 +956,7 @@
1.286
1.287 {
1.288 assume "even n"
1.289 - have "real (x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
1.290 + have "real (x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
1.291 (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
1.292 using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
1.293 also have "\<dots> \<le> ?SUM" by auto
1.294 @@ -980,14 +980,14 @@
1.295 qed
1.296 also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
1.297 by auto
1.298 - also have "\<dots> \<le> real (x * ub_sin_cos_aux prec n 2 1 (x * x))"
1.299 + also have "\<dots> \<le> real (x * ub_sin_cos_aux prec n 2 1 (x * x))"
1.300 using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
1.301 finally have "sin (real x) \<le> real (x * ub_sin_cos_aux prec n 2 1 (x * x))" .
1.302 } note ub = this and lb
1.303 } note ub = this(1) and lb = this(2)
1.304
1.305 have "sin (real x) \<le> real (x * ub_sin_cos_aux prec (get_odd n) 2 1 (x * x))" using ub[OF odd_pos[OF get_odd] get_odd] .
1.306 - moreover have "real (x * lb_sin_cos_aux prec (get_even n) 2 1 (x * x)) \<le> sin (real x)"
1.307 + moreover have "real (x * lb_sin_cos_aux prec (get_even n) 2 1 (x * x)) \<le> sin (real x)"
1.308 proof (cases "0 < get_even n")
1.309 case True show ?thesis using lb[OF True get_even] .
1.310 next
1.311 @@ -1001,7 +1001,7 @@
1.312 case True
1.313 show ?thesis
1.314 proof (cases "n = 0")
1.315 - case True
1.316 + case True
1.317 thus ?thesis unfolding `n = 0` get_even_def get_odd_def using `real x = 0` lapprox_rat[where x="-1" and y=1] by auto
1.318 next
1.319 case False with not0_implies_Suc obtain m where "n = Suc m" by blast
1.320 @@ -1106,7 +1106,7 @@
1.321 moreover have "?cos x \<le> real (?ub x)"
1.322 proof -
1.323 from ub_half[OF ub `-pi \<le> real x` `real x \<le> pi`]
1.324 - show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
1.325 + show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
1.326 qed
1.327 ultimately show ?thesis by auto
1.328 next
1.329 @@ -1435,7 +1435,7 @@
1.330 qed
1.331 finally have "real (lb_exp_horner prec (get_even n) 1 1 x) \<le> exp (real x)" .
1.332 } moreover
1.333 - {
1.334 + {
1.335 have x_less_zero: "real x ^ get_odd n \<le> 0"
1.336 proof (cases "real x = 0")
1.337 case True
1.338 @@ -1462,12 +1462,12 @@
1.339
1.340 function ub_exp :: "nat \<Rightarrow> float \<Rightarrow> float" and lb_exp :: "nat \<Rightarrow> float \<Rightarrow> float" where
1.341 "lb_exp prec x = (if 0 < x then float_divl prec 1 (ub_exp prec (-x))
1.342 - else let
1.343 + else let
1.344 horner = (\<lambda> x. let y = lb_exp_horner prec (get_even (prec + 2)) 1 1 x in if y \<le> 0 then Float 1 -2 else y)
1.345 in if x < - 1 then (case floor_fl x of (Float m e) \<Rightarrow> (horner (float_divl prec x (- Float m e))) ^ (nat (-m) * 2 ^ nat e))
1.346 else horner x)" |
1.347 "ub_exp prec x = (if 0 < x then float_divr prec 1 (lb_exp prec (-x))
1.348 - else if x < - 1 then (case floor_fl x of (Float m e) \<Rightarrow>
1.349 + else if x < - 1 then (case floor_fl x of (Float m e) \<Rightarrow>
1.350 (ub_exp_horner prec (get_odd (prec + 2)) 1 1 (float_divr prec x (- Float m e))) ^ (nat (-m) * 2 ^ nat e))
1.351 else ub_exp_horner prec (get_odd (prec + 2)) 1 1 x)"
1.352 by pat_completeness auto
1.353 @@ -1479,10 +1479,10 @@
1.354
1.355 have "1 / 4 = real (Float 1 -2)" unfolding Float_num by auto
1.356 also have "\<dots> \<le> real (lb_exp_horner 1 (get_even 4) 1 1 (- 1))"
1.357 - unfolding get_even_def eq4
1.358 + unfolding get_even_def eq4
1.359 by (auto simp add: lapprox_posrat_def rapprox_posrat_def normfloat.simps)
1.360 also have "\<dots> \<le> exp (real (- 1 :: float))" using bnds_exp_horner[where x="- 1"] by auto
1.361 - finally show ?thesis unfolding real_of_float_minus real_of_float_1 .
1.362 + finally show ?thesis unfolding real_of_float_minus real_of_float_1 .
1.363 qed
1.364
1.365 lemma lb_exp_pos: assumes "\<not> 0 < x" shows "0 < lb_exp prec x"
1.366 @@ -1523,10 +1523,10 @@
1.367 qed
1.368 next
1.369 case True
1.370 -
1.371 +
1.372 obtain m e where Float_floor: "floor_fl x = Float m e" by (cases "floor_fl x", auto)
1.373 let ?num = "nat (- m) * 2 ^ nat e"
1.374 -
1.375 +
1.376 have "real (floor_fl x) < - 1" using floor_fl `x < - 1` unfolding le_float_def less_float_def real_of_float_minus real_of_float_1 by (rule order_le_less_trans)
1.377 hence "real (floor_fl x) < 0" unfolding Float_floor real_of_float_simp using zero_less_pow2[of xe] by auto
1.378 hence "m < 0"
1.379 @@ -1544,12 +1544,12 @@
1.380 unfolding Float_floor real_of_float_minus real_of_float_simp real_of_nat_mult pow2_int[of "nat e", unfolded e_nat] realpow_real_of_nat[symmetric] by auto
1.381 have "0 < - floor_fl x" using `0 < ?num`[unfolded real_of_nat_less_iff[symmetric]] unfolding less_float_def num_eq[symmetric] real_of_float_0 real_of_nat_zero .
1.382 hence "real (floor_fl x) < 0" unfolding less_float_def by auto
1.383 -
1.384 +
1.385 have "exp (real x) \<le> real (ub_exp prec x)"
1.386 proof -
1.387 - have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
1.388 + have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
1.389 using float_divr_nonpos_pos_upper_bound[OF `x \<le> 0` `0 < - floor_fl x`] unfolding le_float_def real_of_float_0 .
1.390 -
1.391 +
1.392 have "exp (real x) = exp (real ?num * (real x / real ?num))" using `real ?num \<noteq> 0` by auto
1.393 also have "\<dots> = exp (real x / real ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
1.394 also have "\<dots> \<le> exp (real (float_divr prec x (- floor_fl x))) ^ ?num" unfolding num_eq
1.395 @@ -1558,21 +1558,21 @@
1.396 by (rule power_mono, rule bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct2], auto)
1.397 finally show ?thesis unfolding ub_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def .
1.398 qed
1.399 - moreover
1.400 + moreover
1.401 have "real (lb_exp prec x) \<le> exp (real x)"
1.402 proof -
1.403 let ?divl = "float_divl prec x (- Float m e)"
1.404 let ?horner = "?lb_exp_horner ?divl"
1.405 -
1.406 +
1.407 show ?thesis
1.408 proof (cases "?horner \<le> 0")
1.409 case False hence "0 \<le> real ?horner" unfolding le_float_def by auto
1.410 -
1.411 +
1.412 have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
1.413 using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
1.414 -
1.415 - have "real ((?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num) \<le>
1.416 - exp (real (float_divl prec x (- floor_fl x))) ^ ?num" unfolding float_power
1.417 +
1.418 + have "real ((?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num) \<le>
1.419 + exp (real (float_divl prec x (- floor_fl x))) ^ ?num" unfolding float_power
1.420 using `0 \<le> real ?horner`[unfolded Float_floor[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
1.421 also have "\<dots> \<le> exp (real x / real ?num) ^ ?num" unfolding num_eq
1.422 using float_divl by (auto intro!: power_mono simp del: real_of_float_minus)
1.423 @@ -1602,16 +1602,16 @@
1.424 proof -
1.425 show ?thesis
1.426 proof (cases "0 < x")
1.427 - case False hence "x \<le> 0" unfolding less_float_def le_float_def by auto
1.428 + case False hence "x \<le> 0" unfolding less_float_def le_float_def by auto
1.429 from exp_boundaries'[OF this] show ?thesis .
1.430 next
1.431 case True hence "-x \<le> 0" unfolding less_float_def le_float_def by auto
1.432 -
1.433 +
1.434 have "real (lb_exp prec x) \<le> exp (real x)"
1.435 proof -
1.436 from exp_boundaries'[OF `-x \<le> 0`]
1.437 have ub_exp: "exp (- real x) \<le> real (ub_exp prec (-x))" unfolding atLeastAtMost_iff real_of_float_minus by auto
1.438 -
1.439 +
1.440 have "real (float_divl prec 1 (ub_exp prec (-x))) \<le> 1 / real (ub_exp prec (-x))" using float_divl[where x=1] by auto
1.441 also have "\<dots> \<le> exp (real x)"
1.442 using ub_exp[unfolded inverse_le_iff_le[OF order_less_le_trans[OF exp_gt_zero ub_exp] exp_gt_zero, symmetric]]
1.443 @@ -1622,12 +1622,12 @@
1.444 have "exp (real x) \<le> real (ub_exp prec x)"
1.445 proof -
1.446 have "\<not> 0 < -x" using `0 < x` unfolding less_float_def by auto
1.447 -
1.448 +
1.449 from exp_boundaries'[OF `-x \<le> 0`]
1.450 have lb_exp: "real (lb_exp prec (-x)) \<le> exp (- real x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
1.451 -
1.452 +
1.453 have "exp (real x) \<le> real (1 :: float) / real (lb_exp prec (-x))"
1.454 - using lb_exp[unfolded inverse_le_iff_le[OF exp_gt_zero lb_exp_pos[OF `\<not> 0 < -x`, unfolded less_float_def real_of_float_0],
1.455 + using lb_exp[unfolded inverse_le_iff_le[OF exp_gt_zero lb_exp_pos[OF `\<not> 0 < -x`, unfolded less_float_def real_of_float_0],
1.456 symmetric]]
1.457 unfolding exp_minus nonzero_inverse_inverse_eq[OF exp_not_eq_zero] inverse_eq_divide real_of_float_1 by auto
1.458 also have "\<dots> \<le> real (float_divr prec 1 (lb_exp prec (-x)))" using float_divr .
1.459 @@ -1658,7 +1658,7 @@
1.460
1.461 subsection "Compute the logarithm series"
1.462
1.463 -fun ub_ln_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
1.464 +fun ub_ln_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
1.465 and lb_ln_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
1.466 "ub_ln_horner prec 0 i x = 0" |
1.467 "ub_ln_horner prec (Suc n) i x = rapprox_rat prec 1 (int i) - x * lb_ln_horner prec n (Suc i) x" |
1.468 @@ -1676,13 +1676,13 @@
1.469 using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
1.470
1.471 have "norm x < 1" using assms by auto
1.472 - have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
1.473 + have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
1.474 using LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
1.475 { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
1.476 { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
1.477 proof (rule mult_mono)
1.478 show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
1.479 - have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 real_mult_assoc[symmetric]
1.480 + have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 real_mult_assoc[symmetric]
1.481 by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
1.482 thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
1.483 qed auto }
1.484 @@ -1690,7 +1690,7 @@
1.485 show "?lb" and "?ub" by auto
1.486 qed
1.487
1.488 -lemma ln_float_bounds:
1.489 +lemma ln_float_bounds:
1.490 assumes "0 \<le> real x" and "real x < 1"
1.491 shows "real (x * lb_ln_horner prec (get_even n) 1 x) \<le> ln (real x + 1)" (is "?lb \<le> ?ln")
1.492 and "ln (real x + 1) \<le> real (x * ub_ln_horner prec (get_odd n) 1 x)" (is "?ln \<le> ?ub")
1.493 @@ -1705,21 +1705,21 @@
1.494 OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
1.495 by (rule mult_right_mono)
1.496 also have "\<dots> \<le> ?ln" using ln_bounds(1)[OF `0 \<le> real x` `real x < 1`] by auto
1.497 - finally show "?lb \<le> ?ln" .
1.498 + finally show "?lb \<le> ?ln" .
1.499
1.500 have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
1.501 also have "\<dots> \<le> ?ub" unfolding power_Suc2 real_mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding real_mult_commute[of "real x"] od
1.502 using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
1.503 OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
1.504 by (rule mult_right_mono)
1.505 - finally show "?ln \<le> ?ub" .
1.506 + finally show "?ln \<le> ?ub" .
1.507 qed
1.508
1.509 lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
1.510 proof -
1.511 have "x \<noteq> 0" using assms by auto
1.512 have "x + y = x * (1 + y / x)" unfolding right_distrib times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
1.513 - moreover
1.514 + moreover
1.515 have "0 < y / x" using assms divide_pos_pos by auto
1.516 hence "0 < 1 + y / x" by auto
1.517 ultimately show ?thesis using ln_mult assms by auto
1.518 @@ -1727,11 +1727,11 @@
1.519
1.520 subsection "Compute the logarithm of 2"
1.521
1.522 -definition ub_ln2 where "ub_ln2 prec = (let third = rapprox_rat (max prec 1) 1 3
1.523 - in (Float 1 -1 * ub_ln_horner prec (get_odd prec) 1 (Float 1 -1)) +
1.524 +definition ub_ln2 where "ub_ln2 prec = (let third = rapprox_rat (max prec 1) 1 3
1.525 + in (Float 1 -1 * ub_ln_horner prec (get_odd prec) 1 (Float 1 -1)) +
1.526 (third * ub_ln_horner prec (get_odd prec) 1 third))"
1.527 -definition lb_ln2 where "lb_ln2 prec = (let third = lapprox_rat prec 1 3
1.528 - in (Float 1 -1 * lb_ln_horner prec (get_even prec) 1 (Float 1 -1)) +
1.529 +definition lb_ln2 where "lb_ln2 prec = (let third = lapprox_rat prec 1 3
1.530 + in (Float 1 -1 * lb_ln_horner prec (get_even prec) 1 (Float 1 -1)) +
1.531 (third * lb_ln_horner prec (get_even prec) 1 third))"
1.532
1.533 lemma ub_ln2: "ln 2 \<le> real (ub_ln2 prec)" (is "?ub_ln2")
1.534 @@ -2128,10 +2128,10 @@
1.535
1.536 fun approx approx' :: "nat \<Rightarrow> floatarith \<Rightarrow> (float * float) list \<Rightarrow> (float * float) option" where
1.537 "approx' prec a bs = (case (approx prec a bs) of Some (l, u) \<Rightarrow> Some (round_down prec l, round_up prec u) | None \<Rightarrow> None)" |
1.538 -"approx prec (Add a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (\<lambda> l1 u1 l2 u2. (l1 + l2, u1 + u2))" |
1.539 +"approx prec (Add a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (\<lambda> l1 u1 l2 u2. (l1 + l2, u1 + u2))" |
1.540 "approx prec (Minus a) bs = lift_un' (approx' prec a bs) (\<lambda> l u. (-u, -l))" |
1.541 "approx prec (Mult a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs)
1.542 - (\<lambda> a1 a2 b1 b2. (float_nprt a1 * float_pprt b2 + float_nprt a2 * float_nprt b2 + float_pprt a1 * float_pprt b1 + float_pprt a2 * float_nprt b1,
1.543 + (\<lambda> a1 a2 b1 b2. (float_nprt a1 * float_pprt b2 + float_nprt a2 * float_nprt b2 + float_pprt a1 * float_pprt b1 + float_pprt a2 * float_nprt b1,
1.544 float_pprt a2 * float_pprt b2 + float_pprt a1 * float_nprt b2 + float_nprt a2 * float_pprt b1 + float_nprt a1 * float_nprt b1))" |
1.545 "approx prec (Inverse a) bs = lift_un (approx' prec a bs) (\<lambda> l u. if (0 < l \<or> u < 0) then (Some (float_divl prec 1 u), Some (float_divr prec 1 l)) else (None, None))" |
1.546 "approx prec (Cos a) bs = lift_un' (approx' prec a bs) (bnds_cos prec)" |
1.547 @@ -2174,9 +2174,9 @@
1.548 proof -
1.549 obtain l1 u1 l2 u2
1.550 where Sa: "Some (l1, u1) = g a" and Sb: "Some (l2, u2) = g b" using lift_bin'_ex[OF assms(1)] by auto
1.551 - have lu: "(l, u) = f l1 u1 l2 u2" using lift_bin'_Some[unfolded Sa[symmetric] Sb[symmetric] lift_bin'.simps] by auto
1.552 + have lu: "(l, u) = f l1 u1 l2 u2" using lift_bin'_Some[unfolded Sa[symmetric] Sb[symmetric] lift_bin'.simps] by auto
1.553 have "l = fst (f l1 u1 l2 u2)" and "u = snd (f l1 u1 l2 u2)" unfolding lu[symmetric] by auto
1.554 - thus ?thesis using Pa[OF Sa] Pb[OF Sb] by auto
1.555 + thus ?thesis using Pa[OF Sa] Pb[OF Sb] by auto
1.556 qed
1.557
1.558 lemma approx_approx':
1.559 @@ -2188,7 +2188,7 @@
1.560 using approx' unfolding approx'.simps by (cases "approx prec a vs", auto)
1.561 have l': "l = round_down prec l'" and u': "u = round_up prec u'"
1.562 using approx' unfolding approx'.simps S[symmetric] by auto
1.563 - show ?thesis unfolding l' u'
1.564 + show ?thesis unfolding l' u'
1.565 using order_trans[OF Pa[OF S, THEN conjunct2] round_up[of u']]
1.566 using order_trans[OF round_down[of _ l'] Pa[OF S, THEN conjunct1]] by auto
1.567 qed
1.568 @@ -2197,8 +2197,8 @@
1.569 assumes lift_bin'_Some: "Some (l, u) = lift_bin' (approx' prec a bs) (approx' prec b bs) f"
1.570 and Pa: "\<And>l u. Some (l, u) = approx prec a bs \<Longrightarrow> real l \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u" (is "\<And>l u. _ = ?g a \<Longrightarrow> ?P l u a")
1.571 and Pb: "\<And>l u. Some (l, u) = approx prec b bs \<Longrightarrow> real l \<le> interpret_floatarith b xs \<and> interpret_floatarith b xs \<le> real u"
1.572 - shows "\<exists> l1 u1 l2 u2. (real l1 \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u1) \<and>
1.573 - (real l2 \<le> interpret_floatarith b xs \<and> interpret_floatarith b xs \<le> real u2) \<and>
1.574 + shows "\<exists> l1 u1 l2 u2. (real l1 \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u1) \<and>
1.575 + (real l2 \<le> interpret_floatarith b xs \<and> interpret_floatarith b xs \<le> real u2) \<and>
1.576 l = fst (f l1 u1 l2 u2) \<and> u = snd (f l1 u1 l2 u2)"
1.577 proof -
1.578 { fix l u assume "Some (l, u) = approx' prec a bs"
1.579 @@ -2238,7 +2238,7 @@
1.580 lemma lift_un':
1.581 assumes lift_un'_Some: "Some (l, u) = lift_un' (approx' prec a bs) f"
1.582 and Pa: "\<And>l u. Some (l, u) = approx prec a bs \<Longrightarrow> real l \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u" (is "\<And>l u. _ = ?g a \<Longrightarrow> ?P l u a")
1.583 - shows "\<exists> l1 u1. (real l1 \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u1) \<and>
1.584 + shows "\<exists> l1 u1. (real l1 \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u1) \<and>
1.585 l = fst (f l1 u1) \<and> u = snd (f l1 u1)"
1.586 proof -
1.587 { fix l u assume "Some (l, u) = approx' prec a bs"
1.588 @@ -2282,7 +2282,7 @@
1.589 proof (rule ccontr)
1.590 assume "\<not> (fst (f l1 u1) \<noteq> None \<and> snd (f l1 u1) \<noteq> None)"
1.591 hence or: "fst (f l1 u1) = None \<or> snd (f l1 u1) = None" by auto
1.592 - hence "lift_un (g a) f = None"
1.593 + hence "lift_un (g a) f = None"
1.594 proof (cases "fst (f l1 u1) = None")
1.595 case True
1.596 then obtain b where b: "f l1 u1 = (None, b)" by (cases "f l1 u1", auto)
1.597 @@ -2303,7 +2303,7 @@
1.598 lemma lift_un:
1.599 assumes lift_un_Some: "Some (l, u) = lift_un (approx' prec a bs) f"
1.600 and Pa: "\<And>l u. Some (l, u) = approx prec a bs \<Longrightarrow> real l \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u" (is "\<And>l u. _ = ?g a \<Longrightarrow> ?P l u a")
1.601 - shows "\<exists> l1 u1. (real l1 \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u1) \<and>
1.602 + shows "\<exists> l1 u1. (real l1 \<le> interpret_floatarith a xs \<and> interpret_floatarith a xs \<le> real u1) \<and>
1.603 Some l = fst (f l1 u1) \<and> Some u = snd (f l1 u1)"
1.604 proof -
1.605 { fix l u assume "Some (l, u) = approx' prec a bs"
1.606 @@ -2329,7 +2329,7 @@
1.607 assumes "bounded_by xs vs"
1.608 and "Some (l, u) = approx prec arith vs" (is "_ = ?g arith")
1.609 shows "real l \<le> interpret_floatarith arith xs \<and> interpret_floatarith arith xs \<le> real u" (is "?P l u arith")
1.610 - using `Some (l, u) = approx prec arith vs`
1.611 + using `Some (l, u) = approx prec arith vs`
1.612 proof (induct arith arbitrary: l u x)
1.613 case (Add a b)
1.614 from lift_bin'[OF Add.prems[unfolded approx.simps]] Add.hyps
1.615 @@ -2346,17 +2346,17 @@
1.616 next
1.617 case (Mult a b)
1.618 from lift_bin'[OF Mult.prems[unfolded approx.simps]] Mult.hyps
1.619 - obtain l1 u1 l2 u2
1.620 + obtain l1 u1 l2 u2
1.621 where l: "l = float_nprt l1 * float_pprt u2 + float_nprt u1 * float_nprt u2 + float_pprt l1 * float_pprt l2 + float_pprt u1 * float_nprt l2"
1.622 and u: "u = float_pprt u1 * float_pprt u2 + float_pprt l1 * float_nprt u2 + float_nprt u1 * float_pprt l2 + float_nprt l1 * float_nprt l2"
1.623 and "real l1 \<le> interpret_floatarith a xs" and "interpret_floatarith a xs \<le> real u1"
1.624 and "real l2 \<le> interpret_floatarith b xs" and "interpret_floatarith b xs \<le> real u2" unfolding fst_conv snd_conv by blast
1.625 - thus ?case unfolding interpret_floatarith.simps l u real_of_float_add real_of_float_mult real_of_float_nprt real_of_float_pprt
1.626 + thus ?case unfolding interpret_floatarith.simps l u real_of_float_add real_of_float_mult real_of_float_nprt real_of_float_pprt
1.627 using mult_le_prts mult_ge_prts by auto
1.628 next
1.629 case (Inverse a)
1.630 from lift_un[OF Inverse.prems[unfolded approx.simps], unfolded if_distrib[of fst] if_distrib[of snd] fst_conv snd_conv] Inverse.hyps
1.631 - obtain l1 u1 where l': "Some l = (if 0 < l1 \<or> u1 < 0 then Some (float_divl prec 1 u1) else None)"
1.632 + obtain l1 u1 where l': "Some l = (if 0 < l1 \<or> u1 < 0 then Some (float_divl prec 1 u1) else None)"
1.633 and u': "Some u = (if 0 < l1 \<or> u1 < 0 then Some (float_divr prec 1 l1) else None)"
1.634 and l1: "real l1 \<le> interpret_floatarith a xs" and u1: "interpret_floatarith a xs \<le> real u1" by blast
1.635 have either: "0 < l1 \<or> u1 < 0" proof (rule ccontr) assume P: "\<not> (0 < l1 \<or> u1 < 0)" show False using l' unfolding if_not_P[OF P] by auto qed
1.636 @@ -2366,7 +2366,7 @@
1.637 have inv: "inverse (real u1) \<le> inverse (interpret_floatarith a xs)
1.638 \<and> inverse (interpret_floatarith a xs) \<le> inverse (real l1)"
1.639 proof (cases "0 < l1")
1.640 - case True hence "0 < real u1" and "0 < real l1" "0 < interpret_floatarith a xs"
1.641 + case True hence "0 < real u1" and "0 < real l1" "0 < interpret_floatarith a xs"
1.642 unfolding less_float_def using l1_le_u1 l1 by auto
1.643 show ?thesis
1.644 unfolding inverse_le_iff_le[OF `0 < real u1` `0 < interpret_floatarith a xs`]
1.645 @@ -2374,7 +2374,7 @@
1.646 using l1 u1 by auto
1.647 next
1.648 case False hence "u1 < 0" using either by blast
1.649 - hence "real u1 < 0" and "real l1 < 0" "interpret_floatarith a xs < 0"
1.650 + hence "real u1 < 0" and "real l1 < 0" "interpret_floatarith a xs < 0"
1.651 unfolding less_float_def using l1_le_u1 u1 by auto
1.652 show ?thesis
1.653 unfolding inverse_le_iff_le_neg[OF `real u1 < 0` `interpret_floatarith a xs < 0`]
1.654 @@ -2420,7 +2420,7 @@
1.655 next case (Power a n) with lift_un'_bnds[OF bnds_power] show ?case by auto
1.656 next case (Num f) thus ?case by auto
1.657 next
1.658 - case (Atom n)
1.659 + case (Atom n)
1.660 show ?case
1.661 proof (cases "n < length vs")
1.662 case True
1.663 @@ -2431,14 +2431,14 @@
1.664 qed
1.665 qed
1.666
1.667 -datatype inequality = Less floatarith floatarith
1.668 - | LessEqual floatarith floatarith
1.669 +datatype inequality = Less floatarith floatarith
1.670 + | LessEqual floatarith floatarith
1.671
1.672 -fun interpret_inequality :: "inequality \<Rightarrow> real list \<Rightarrow> bool" where
1.673 +fun interpret_inequality :: "inequality \<Rightarrow> real list \<Rightarrow> bool" where
1.674 "interpret_inequality (Less a b) vs = (interpret_floatarith a vs < interpret_floatarith b vs)" |
1.675 "interpret_inequality (LessEqual a b) vs = (interpret_floatarith a vs \<le> interpret_floatarith b vs)"
1.676
1.677 -fun approx_inequality :: "nat \<Rightarrow> inequality \<Rightarrow> (float * float) list \<Rightarrow> bool" where
1.678 +fun approx_inequality :: "nat \<Rightarrow> inequality \<Rightarrow> (float * float) list \<Rightarrow> bool" where
1.679 "approx_inequality prec (Less a b) bs = (case (approx prec a bs, approx prec b bs) of (Some (l, u), Some (l', u')) \<Rightarrow> u < l' | _ \<Rightarrow> False)" |
1.680 "approx_inequality prec (LessEqual a b) bs = (case (approx prec a bs, approx prec b bs) of (Some (l, u), Some (l', u')) \<Rightarrow> u \<le> l' | _ \<Rightarrow> False)"
1.681
1.682 @@ -2447,7 +2447,7 @@
1.683 proof (cases eq)
1.684 case (Less a b)
1.685 show ?thesis
1.686 - proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
1.687 + proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
1.688 approx prec b bs = Some (l', u')")
1.689 case True
1.690 then obtain l u l' u' where a_approx: "approx prec a bs = Some (l, u)"
1.691 @@ -2462,14 +2462,14 @@
1.692 case False
1.693 hence "approx prec a bs = None \<or> approx prec b bs = None"
1.694 unfolding not_Some_eq[symmetric] by auto
1.695 - hence "\<not> approx_inequality prec eq bs" unfolding Less approx_inequality.simps
1.696 + hence "\<not> approx_inequality prec eq bs" unfolding Less approx_inequality.simps
1.697 by (cases "approx prec a bs = None", auto)
1.698 thus ?thesis using assms by auto
1.699 qed
1.700 next
1.701 case (LessEqual a b)
1.702 show ?thesis
1.703 - proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
1.704 + proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
1.705 approx prec b bs = Some (l', u')")
1.706 case True
1.707 then obtain l u l' u' where a_approx: "approx prec a bs = Some (l, u)"
1.708 @@ -2484,7 +2484,7 @@
1.709 case False
1.710 hence "approx prec a bs = None \<or> approx prec b bs = None"
1.711 unfolding not_Some_eq[symmetric] by auto
1.712 - hence "\<not> approx_inequality prec eq bs" unfolding LessEqual approx_inequality.simps
1.713 + hence "\<not> approx_inequality prec eq bs" unfolding LessEqual approx_inequality.simps
1.714 by (cases "approx prec a bs = None", auto)
1.715 thus ?thesis using assms by auto
1.716 qed
1.717 @@ -2496,7 +2496,7 @@
1.718 lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
1.719 unfolding real_diff_def interpret_floatarith.simps ..
1.720
1.721 -lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
1.722 +lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
1.723 sin (interpret_floatarith a vs)"
1.724 unfolding sin_cos_eq interpret_floatarith.simps
1.725 interpret_floatarith_divide interpret_floatarith_diff real_diff_def