1 (* Title: HOL/Library/Float.thy |
|
2 Author: Steven Obua 2008 |
|
3 Author: Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 |
|
4 *) |
|
5 |
|
6 header {* Floating-Point Numbers *} |
1 header {* Floating-Point Numbers *} |
7 |
2 |
8 theory Float |
3 theory Float |
9 imports Complex_Main Lattice_Algebras |
4 imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras" |
10 begin |
5 begin |
11 |
6 |
12 definition pow2 :: "int \<Rightarrow> real" where |
7 typedef float = "{m * 2 powr e | (m :: int) (e :: int). True }" |
13 [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))" |
8 morphisms real_of_float float_of |
14 |
9 by auto |
15 datatype float = Float int int |
10 |
16 |
11 declare [[coercion "real::float\<Rightarrow>real"]] |
17 primrec of_float :: "float \<Rightarrow> real" where |
12 |
18 "of_float (Float a b) = real a * pow2 b" |
13 lemmas float_of_inject[simp] |
|
14 lemmas float_of_cases2 = float_of_cases[case_product float_of_cases] |
|
15 lemmas float_of_cases3 = float_of_cases2[case_product float_of_cases] |
19 |
16 |
20 defs (overloaded) |
17 defs (overloaded) |
21 real_of_float_def [code_unfold]: "real == of_float" |
18 real_of_float_def[code_unfold]: "real == real_of_float" |
22 |
19 |
23 declare [[coercion "% x . Float x 0"]] |
20 lemma real_of_float_eq[simp]: |
24 declare [[coercion "real::float\<Rightarrow>real"]] |
21 fixes f1 f2 :: float shows "real f1 = real f2 \<longleftrightarrow> f1 = f2" |
25 |
22 unfolding real_of_float_def real_of_float_inject .. |
26 primrec mantissa :: "float \<Rightarrow> int" where |
23 |
27 "mantissa (Float a b) = a" |
24 lemma float_of_real[simp]: "float_of (real x) = x" |
28 |
25 unfolding real_of_float_def by (rule real_of_float_inverse) |
29 primrec scale :: "float \<Rightarrow> int" where |
26 |
30 "scale (Float a b) = b" |
27 lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x" |
31 |
28 unfolding real_of_float_def by (rule float_of_inverse) |
32 instantiation float :: zero |
29 |
|
30 subsection {* Real operations preserving the representation as floating point number *} |
|
31 |
|
32 lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float" |
|
33 by (auto simp: float_def) |
|
34 |
|
35 lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def) |
|
36 lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp |
|
37 lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp |
|
38 lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp |
|
39 lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp |
|
40 lemma real_of_nat_float[simp]: "real (x ::nat) \<in> float" by (intro floatI[of x 0]) simp |
|
41 lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp |
|
42 lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \<in> float" by (intro floatI[of 1 i]) simp |
|
43 lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp |
|
44 lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \<in> float" by (intro floatI[of 1 "-i"]) simp |
|
45 lemma two_powr_numeral_float[simp]: "2 powr numeral i \<in> float" by (intro floatI[of 1 "numeral i"]) simp |
|
46 lemma two_powr_neg_numeral_float[simp]: "2 powr neg_numeral i \<in> float" by (intro floatI[of 1 "neg_numeral i"]) simp |
|
47 lemma two_pow_float[simp]: "2 ^ n \<in> float" by (intro floatI[of 1 "n"]) (simp add: powr_realpow) |
|
48 lemma real_of_float_float[simp]: "real (f::float) \<in> float" by (cases f) simp |
|
49 |
|
50 lemma plus_float[simp]: "r \<in> float \<Longrightarrow> p \<in> float \<Longrightarrow> r + p \<in> float" |
|
51 unfolding float_def |
|
52 proof (safe, simp) |
|
53 fix e1 m1 e2 m2 :: int |
|
54 { fix e1 m1 e2 m2 :: int assume "e1 \<le> e2" |
|
55 then have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1" |
|
56 by (simp add: powr_realpow[symmetric] powr_divide2[symmetric] field_simps) |
|
57 then have "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e" |
|
58 by blast } |
|
59 note * = this |
|
60 show "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e" |
|
61 proof (cases e1 e2 rule: linorder_le_cases) |
|
62 assume "e2 \<le> e1" from *[OF this, of m2 m1] show ?thesis by (simp add: ac_simps) |
|
63 qed (rule *) |
|
64 qed |
|
65 |
|
66 lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float" |
|
67 apply (auto simp: float_def) |
|
68 apply (rule_tac x="-x" in exI) |
|
69 apply (rule_tac x="xa" in exI) |
|
70 apply (simp add: field_simps) |
|
71 done |
|
72 |
|
73 lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float" |
|
74 apply (auto simp: float_def) |
|
75 apply (rule_tac x="x * xa" in exI) |
|
76 apply (rule_tac x="xb + xc" in exI) |
|
77 apply (simp add: powr_add) |
|
78 done |
|
79 |
|
80 lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float" |
|
81 unfolding ab_diff_minus by (intro uminus_float plus_float) |
|
82 |
|
83 lemma abs_float[simp]: "x \<in> float \<Longrightarrow> abs x \<in> float" |
|
84 by (cases x rule: linorder_cases[of 0]) auto |
|
85 |
|
86 lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float" |
|
87 by (cases x rule: linorder_cases[of 0]) (auto intro!: uminus_float) |
|
88 |
|
89 lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float" |
|
90 apply (auto simp add: float_def) |
|
91 apply (rule_tac x="x" in exI) |
|
92 apply (rule_tac x="xa - d" in exI) |
|
93 apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric]) |
|
94 done |
|
95 |
|
96 lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float" |
|
97 apply (auto simp add: float_def) |
|
98 apply (rule_tac x="x" in exI) |
|
99 apply (rule_tac x="xa - d" in exI) |
|
100 apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric]) |
|
101 done |
|
102 |
|
103 lemma div_numeral_Bit0_float[simp]: |
|
104 assumes x: "x / numeral n \<in> float" shows "x / (numeral (Num.Bit0 n)) \<in> float" |
|
105 proof - |
|
106 have "(x / numeral n) / 2^1 \<in> float" |
|
107 by (intro x div_power_2_float) |
|
108 also have "(x / numeral n) / 2^1 = x / (numeral (Num.Bit0 n))" |
|
109 by (induct n) auto |
|
110 finally show ?thesis . |
|
111 qed |
|
112 |
|
113 lemma div_neg_numeral_Bit0_float[simp]: |
|
114 assumes x: "x / numeral n \<in> float" shows "x / (neg_numeral (Num.Bit0 n)) \<in> float" |
|
115 proof - |
|
116 have "- (x / numeral (Num.Bit0 n)) \<in> float" using x by simp |
|
117 also have "- (x / numeral (Num.Bit0 n)) = x / neg_numeral (Num.Bit0 n)" |
|
118 unfolding neg_numeral_def by (simp del: minus_numeral) |
|
119 finally show ?thesis . |
|
120 qed |
|
121 |
|
122 subsection {* Arithmetic operations on floating point numbers *} |
|
123 |
|
124 instantiation float :: ring_1 |
33 begin |
125 begin |
34 definition zero_float where "0 = Float 0 0" |
126 |
35 instance .. |
127 definition [simp]: "(0::float) = float_of 0" |
|
128 |
|
129 definition [simp]: "(1::float) = float_of 1" |
|
130 |
|
131 definition "(x + y::float) = float_of (real x + real y)" |
|
132 |
|
133 lemma float_plus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x + float_of y = float_of (x + y)" |
|
134 by (simp add: plus_float_def) |
|
135 |
|
136 definition "(-x::float) = float_of (- real x)" |
|
137 |
|
138 lemma uminus_of_float[simp]: "x \<in> float \<Longrightarrow> - float_of x = float_of (- x)" |
|
139 by (simp add: uminus_float_def) |
|
140 |
|
141 definition "(x - y::float) = float_of (real x - real y)" |
|
142 |
|
143 lemma float_minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x - float_of y = float_of (x - y)" |
|
144 by (simp add: minus_float_def) |
|
145 |
|
146 definition "(x * y::float) = float_of (real x * real y)" |
|
147 |
|
148 lemma float_times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x * float_of y = float_of (x * y)" |
|
149 by (simp add: times_float_def) |
|
150 |
|
151 instance |
|
152 proof |
|
153 fix a b c :: float |
|
154 show "0 + a = a" |
|
155 by (cases a rule: float_of_cases) simp |
|
156 show "1 * a = a" |
|
157 by (cases a rule: float_of_cases) simp |
|
158 show "a * 1 = a" |
|
159 by (cases a rule: float_of_cases) simp |
|
160 show "-a + a = 0" |
|
161 by (cases a rule: float_of_cases) simp |
|
162 show "a + b = b + a" |
|
163 by (cases a b rule: float_of_cases2) (simp add: ac_simps) |
|
164 show "a - b = a + -b" |
|
165 by (cases a b rule: float_of_cases2) (simp add: field_simps) |
|
166 show "a + b + c = a + (b + c)" |
|
167 by (cases a b c rule: float_of_cases3) (simp add: ac_simps) |
|
168 show "a * b * c = a * (b * c)" |
|
169 by (cases a b c rule: float_of_cases3) (simp add: ac_simps) |
|
170 show "(a + b) * c = a * c + b * c" |
|
171 by (cases a b c rule: float_of_cases3) (simp add: field_simps) |
|
172 show "a * (b + c) = a * b + a * c" |
|
173 by (cases a b c rule: float_of_cases3) (simp add: field_simps) |
|
174 show "0 \<noteq> (1::float)" by simp |
|
175 qed |
36 end |
176 end |
37 |
177 |
38 instantiation float :: one |
178 lemma real_of_float_uminus[simp]: |
|
179 fixes f g::float shows "real (- g) = - real g" |
|
180 by (simp add: uminus_float_def) |
|
181 |
|
182 lemma real_of_float_plus[simp]: |
|
183 fixes f g::float shows "real (f + g) = real f + real g" |
|
184 by (simp add: plus_float_def) |
|
185 |
|
186 lemma real_of_float_minus[simp]: |
|
187 fixes f g::float shows "real (f - g) = real f - real g" |
|
188 by (simp add: minus_float_def) |
|
189 |
|
190 lemma real_of_float_times[simp]: |
|
191 fixes f g::float shows "real (f * g) = real f * real g" |
|
192 by (simp add: times_float_def) |
|
193 |
|
194 lemma real_of_float_zero[simp]: "real (0::float) = 0" by simp |
|
195 lemma real_of_float_one[simp]: "real (1::float) = 1" by simp |
|
196 |
|
197 lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n" |
|
198 by (induct n) simp_all |
|
199 |
|
200 instantiation float :: linorder |
39 begin |
201 begin |
40 definition one_float where "1 = Float 1 0" |
202 |
41 instance .. |
203 definition "x \<le> (y::float) \<longleftrightarrow> real x \<le> real y" |
|
204 |
|
205 lemma float_le_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x \<le> float_of y \<longleftrightarrow> x \<le> y" |
|
206 by (simp add: less_eq_float_def) |
|
207 |
|
208 definition "x < (y::float) \<longleftrightarrow> real x < real y" |
|
209 |
|
210 lemma float_less_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> float_of x < float_of y \<longleftrightarrow> x < y" |
|
211 by (simp add: less_float_def) |
|
212 |
|
213 instance |
|
214 proof |
|
215 fix a b c :: float |
|
216 show "a \<le> a" |
|
217 by (cases a rule: float_of_cases) simp |
|
218 show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" |
|
219 by (cases a b rule: float_of_cases2) auto |
|
220 show "a \<le> b \<or> b \<le> a" |
|
221 by (cases a b rule: float_of_cases2) auto |
|
222 { assume "a \<le> b" "b \<le> a" then show "a = b" |
|
223 by (cases a b rule: float_of_cases2) auto } |
|
224 { assume "a \<le> b" "b \<le> c" then show "a \<le> c" |
|
225 by (cases a b c rule: float_of_cases3) auto } |
|
226 qed |
42 end |
227 end |
43 |
228 |
44 lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b" |
229 lemma real_of_float_min: fixes a b::float shows "real (min a b) = min (real a) (real b)" |
45 unfolding real_of_float_def using of_float.simps . |
230 by (simp add: min_def less_eq_float_def) |
46 |
231 |
47 lemma real_of_float_neg_exp: "e < 0 \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto |
232 lemma real_of_float_max: fixes a b::float shows "real (max a b) = max (real a) (real b)" |
48 lemma real_of_float_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto |
233 by (simp add: max_def less_eq_float_def) |
49 lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto |
234 |
50 |
235 instantiation float :: linordered_ring |
51 lemma Float_num[simp]: shows |
236 begin |
52 "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and |
237 |
53 "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and |
238 definition "(abs x :: float) = float_of (abs (real x))" |
54 "real (Float -1 0) = -1" and "real (Float (numeral n) 0) = numeral n" |
239 |
55 by auto |
240 lemma float_abs[simp]: "x \<in> float \<Longrightarrow> abs (float_of x) = float_of (abs x)" |
56 |
241 by (simp add: abs_float_def) |
57 lemma float_number_of_int[simp]: "real (Float n 0) = real n" |
242 |
|
243 instance |
|
244 proof |
|
245 fix a b c :: float |
|
246 show "\<bar>a\<bar> = (if a < 0 then - a else a)" |
|
247 by (cases a rule: float_of_cases) simp |
|
248 assume "a \<le> b" |
|
249 then show "c + a \<le> c + b" |
|
250 by (cases a b c rule: float_of_cases3) simp |
|
251 assume "0 \<le> c" |
|
252 with `a \<le> b` show "c * a \<le> c * b" |
|
253 by (cases a b c rule: float_of_cases3) (auto intro: mult_left_mono) |
|
254 from `0 \<le> c` `a \<le> b` show "a * c \<le> b * c" |
|
255 by (cases a b c rule: float_of_cases3) (auto intro: mult_right_mono) |
|
256 qed |
|
257 end |
|
258 |
|
259 lemma real_of_abs_float[simp]: fixes f::float shows "real (abs f) = abs (real f)" |
|
260 unfolding abs_float_def by simp |
|
261 |
|
262 instance float :: dense_linorder |
|
263 proof |
|
264 fix a b :: float |
|
265 show "\<exists>c. a < c" |
|
266 apply (intro exI[of _ "a + 1"]) |
|
267 apply (cases a rule: float_of_cases) |
|
268 apply simp |
|
269 done |
|
270 show "\<exists>c. c < a" |
|
271 apply (intro exI[of _ "a - 1"]) |
|
272 apply (cases a rule: float_of_cases) |
|
273 apply simp |
|
274 done |
|
275 assume "a < b" |
|
276 then show "\<exists>c. a < c \<and> c < b" |
|
277 apply (intro exI[of _ "(b + a) * float_of (1/2)"]) |
|
278 apply (cases a b rule: float_of_cases2) |
|
279 apply simp |
|
280 done |
|
281 qed |
|
282 |
|
283 instantiation float :: linordered_idom |
|
284 begin |
|
285 |
|
286 definition "sgn x = float_of (sgn (real x))" |
|
287 |
|
288 lemma sgn_float[simp]: "x \<in> float \<Longrightarrow> sgn (float_of x) = float_of (sgn x)" |
|
289 by (simp add: sgn_float_def) |
|
290 |
|
291 instance |
|
292 proof |
|
293 fix a b c :: float |
|
294 show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" |
|
295 by (cases a rule: float_of_cases) simp |
|
296 show "a * b = b * a" |
|
297 by (cases a b rule: float_of_cases2) (simp add: field_simps) |
|
298 show "1 * a = a" "(a + b) * c = a * c + b * c" |
|
299 by (simp_all add: field_simps del: one_float_def) |
|
300 assume "a < b" "0 < c" then show "c * a < c * b" |
|
301 by (cases a b c rule: float_of_cases3) (simp add: field_simps) |
|
302 qed |
|
303 end |
|
304 |
|
305 definition Float :: "int \<Rightarrow> int \<Rightarrow> float" where |
|
306 [simp, code del]: "Float m e = float_of (m * 2 powr e)" |
|
307 |
|
308 lemma real_of_float_Float[code]: "real_of_float (Float m e) = |
|
309 (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))" |
|
310 by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric]) |
|
311 |
|
312 code_datatype Float |
|
313 |
|
314 lemma real_Float: "real (Float m e) = m * 2 powr e" by simp |
|
315 |
|
316 definition normfloat :: "float \<Rightarrow> float" where |
|
317 [simp]: "normfloat x = x" |
|
318 |
|
319 lemma compute_normfloat[code]: "normfloat (Float m e) = |
|
320 (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1)) |
|
321 else if m = 0 then 0 else Float m e)" |
|
322 by (simp del: real_of_int_add split: prod.split) |
|
323 (auto simp add: powr_add zmod_eq_0_iff) |
|
324 |
|
325 lemma compute_zero[code_unfold, code]: "0 = Float 0 0" |
58 by simp |
326 by simp |
59 |
327 |
60 lemma pow2_0[simp]: "pow2 0 = 1" by simp |
328 lemma compute_one[code_unfold, code]: "1 = Float 1 0" |
61 lemma pow2_1[simp]: "pow2 1 = 2" by simp |
329 by simp |
62 lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp |
330 |
63 |
331 instance float :: numeral .. |
64 lemma pow2_powr: "pow2 a = 2 powr a" |
332 |
65 by (simp add: powr_realpow[symmetric] powr_minus) |
333 lemma float_of_numeral[simp]: "numeral k = float_of (numeral k)" |
66 |
334 by (induct k) |
67 declare pow2_def[simp del] |
335 (simp_all only: numeral.simps one_float_def float_plus_float numeral_float one_float plus_float) |
68 |
336 |
69 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)" |
337 lemma float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)" |
70 by (simp add: pow2_powr powr_add) |
338 by (simp add: minus_numeral[symmetric] del: minus_numeral) |
71 |
339 |
72 lemma pow2_diff: "pow2 (a - b) = pow2 a / pow2 b" |
340 lemma |
73 by (simp add: pow2_powr powr_divide2) |
341 shows float_numeral[simp]: "real (numeral x :: float) = numeral x" |
74 |
342 and float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x" |
75 lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)" |
343 by simp_all |
76 by (simp add: pow2_add) |
344 |
77 |
345 subsection {* Represent floats as unique mantissa and exponent *} |
78 lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto |
346 |
79 |
347 |
80 lemma float_split: "\<exists> a b. x = Float a b" by (cases x) auto |
348 lemma int_induct_abs[case_names less]: |
81 |
349 fixes j :: int |
82 lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split) |
350 assumes H: "\<And>n. (\<And>i. \<bar>i\<bar> < \<bar>n\<bar> \<Longrightarrow> P i) \<Longrightarrow> P n" |
83 |
351 shows "P j" |
84 lemma float_zero[simp]: "real (Float 0 e) = 0" by simp |
352 proof (induct "nat \<bar>j\<bar>" arbitrary: j rule: less_induct) |
85 |
353 case less show ?case by (rule H[OF less]) simp |
86 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a" |
354 qed |
87 by arith |
355 |
88 |
356 lemma int_cancel_factors: |
89 function normfloat :: "float \<Rightarrow> float" where |
357 fixes n :: int assumes "1 < r" shows "n = 0 \<or> (\<exists>k i. n = k * r ^ i \<and> \<not> r dvd k)" |
90 "normfloat (Float a b) = |
358 proof (induct n rule: int_induct_abs) |
91 (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1)) |
359 case (less n) |
92 else if a=0 then Float 0 0 else Float a b)" |
360 { fix m assume n: "n \<noteq> 0" "n = m * r" |
93 by pat_completeness auto |
361 then have "\<bar>m \<bar> < \<bar>n\<bar>" |
94 termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less) |
362 by (metis abs_dvd_iff abs_ge_self assms comm_semiring_1_class.normalizing_semiring_rules(7) |
95 declare normfloat.simps[simp del] |
363 dvd_imp_le_int dvd_refl dvd_triv_right linorder_neq_iff linorder_not_le |
96 |
364 mult_eq_0_iff zdvd_mult_cancel1) |
97 theorem normfloat[symmetric, simp]: "real f = real (normfloat f)" |
365 from less[OF this] n have "\<exists>k i. n = k * r ^ Suc i \<and> \<not> r dvd k" by auto } |
98 proof (induct f rule: normfloat.induct) |
366 then show ?case |
99 case (1 a b) |
367 by (metis comm_semiring_1_class.normalizing_semiring_rules(12,7) dvdE power_0) |
100 have real2: "2 = real (2::int)" |
368 qed |
101 by auto |
369 |
102 show ?case |
370 lemma mult_powr_eq_mult_powr_iff_asym: |
103 apply (subst normfloat.simps) |
371 fixes m1 m2 e1 e2 :: int |
104 apply auto |
372 assumes m1: "\<not> 2 dvd m1" and "e1 \<le> e2" |
105 apply (subst 1[symmetric]) |
373 shows "m1 * 2 powr e1 = m2 * 2 powr e2 \<longleftrightarrow> m1 = m2 \<and> e1 = e2" |
106 apply (auto simp add: pow2_add even_def) |
374 proof |
107 done |
375 have "m1 \<noteq> 0" using m1 unfolding dvd_def by auto |
108 qed |
376 assume eq: "m1 * 2 powr e1 = m2 * 2 powr e2" |
109 |
377 with `e1 \<le> e2` have "m1 = m2 * 2 powr nat (e2 - e1)" |
110 lemma pow2_neq_zero[simp]: "pow2 x \<noteq> 0" |
378 by (simp add: powr_divide2[symmetric] field_simps) |
111 by (auto simp add: pow2_def) |
379 also have "\<dots> = m2 * 2^nat (e2 - e1)" |
112 |
380 by (simp add: powr_realpow) |
113 lemma pow2_int: "pow2 (int c) = 2^c" |
381 finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)" |
114 by (simp add: pow2_def) |
382 unfolding real_of_int_inject . |
115 |
383 with m1 have "m1 = m2" |
116 lemma zero_less_pow2[simp]: "0 < pow2 x" |
384 by (cases "nat (e2 - e1)") (auto simp add: dvd_def) |
117 by (simp add: pow2_powr) |
385 then show "m1 = m2 \<and> e1 = e2" |
118 |
386 using eq `m1 \<noteq> 0` by (simp add: powr_inj) |
119 lemma normfloat_imp_odd_or_zero: |
387 qed simp |
120 "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)" |
388 |
121 proof (induct f rule: normfloat.induct) |
389 lemma mult_powr_eq_mult_powr_iff: |
122 case (1 u v) |
390 fixes m1 m2 e1 e2 :: int |
123 from 1 have ab: "normfloat (Float u v) = Float a b" by auto |
391 shows "\<not> 2 dvd m1 \<Longrightarrow> \<not> 2 dvd m2 \<Longrightarrow> m1 * 2 powr e1 = m2 * 2 powr e2 \<longleftrightarrow> m1 = m2 \<and> e1 = e2" |
124 { |
392 using mult_powr_eq_mult_powr_iff_asym[of m1 e1 e2 m2] |
125 assume eu: "even u" |
393 using mult_powr_eq_mult_powr_iff_asym[of m2 e2 e1 m1] |
126 assume z: "u \<noteq> 0" |
394 by (cases e1 e2 rule: linorder_le_cases) auto |
127 have "normfloat (Float u v) = normfloat (Float (u div 2) (v + 1))" |
395 |
128 apply (subst normfloat.simps) |
396 lemma floatE_normed: |
129 by (simp add: eu z) |
397 assumes x: "x \<in> float" |
130 with ab have "normfloat (Float (u div 2) (v + 1)) = Float a b" by simp |
398 obtains (zero) "x = 0" |
131 with 1 eu z have ?case by auto |
399 | (powr) m e :: int where "x = m * 2 powr e" "\<not> 2 dvd m" "x \<noteq> 0" |
132 } |
400 proof atomize_elim |
133 note case1 = this |
401 { assume "x \<noteq> 0" |
134 { |
402 from x obtain m e :: int where x: "x = m * 2 powr e" by (auto simp: float_def) |
135 assume "odd u \<or> u = 0" |
403 with `x \<noteq> 0` int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\<not> 2 dvd k" |
136 then have ou: "\<not> (u \<noteq> 0 \<and> even u)" by auto |
404 by auto |
137 have "normfloat (Float u v) = (if u = 0 then Float 0 0 else Float u v)" |
405 with `\<not> 2 dvd k` x have "\<exists>(m::int) (e::int). x = m * 2 powr e \<and> \<not> (2::int) dvd m" |
138 apply (subst normfloat.simps) |
406 by (rule_tac exI[of _ "k"], rule_tac exI[of _ "e + int i"]) |
139 apply (simp add: ou) |
407 (simp add: powr_add powr_realpow) } |
|
408 then show "x = 0 \<or> (\<exists>(m::int) (e::int). x = m * 2 powr e \<and> \<not> (2::int) dvd m \<and> x \<noteq> 0)" |
|
409 by blast |
|
410 qed |
|
411 |
|
412 lemma float_normed_cases: |
|
413 fixes f :: float |
|
414 obtains (zero) "f = 0" |
|
415 | (powr) m e :: int where "real f = m * 2 powr e" "\<not> 2 dvd m" "f \<noteq> 0" |
|
416 proof (atomize_elim, induct f) |
|
417 case (float_of y) then show ?case |
|
418 by (cases rule: floatE_normed) auto |
|
419 qed |
|
420 |
|
421 definition mantissa :: "float \<Rightarrow> int" where |
|
422 "mantissa f = fst (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) |
|
423 \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))" |
|
424 |
|
425 definition exponent :: "float \<Rightarrow> int" where |
|
426 "exponent f = snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) |
|
427 \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))" |
|
428 |
|
429 lemma |
|
430 shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E) |
|
431 and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M) |
|
432 proof - |
|
433 have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)" by auto |
|
434 then show ?E ?M |
|
435 by (auto simp add: mantissa_def exponent_def) |
|
436 qed |
|
437 |
|
438 lemma |
|
439 shows mantissa_exponent: "real f = mantissa f * 2 powr exponent f" (is ?E) |
|
440 and mantissa_not_dvd: "f \<noteq> (float_of 0) \<Longrightarrow> \<not> 2 dvd mantissa f" (is "_ \<Longrightarrow> ?D") |
|
441 proof cases |
|
442 assume [simp]: "f \<noteq> (float_of 0)" |
|
443 have "f = mantissa f * 2 powr exponent f \<and> \<not> 2 dvd mantissa f" |
|
444 proof (cases f rule: float_normed_cases) |
|
445 case (powr m e) |
|
446 then have "\<exists>p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) |
|
447 \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p)" |
|
448 by auto |
|
449 then show ?thesis |
|
450 unfolding exponent_def mantissa_def |
|
451 by (rule someI2_ex) simp |
|
452 qed simp |
|
453 then show ?E ?D by auto |
|
454 qed simp |
|
455 |
|
456 lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0" |
|
457 using mantissa_not_dvd[of f] by auto |
|
458 |
|
459 lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f" |
|
460 unfolding real_of_float_eq[symmetric] mantissa_exponent[of f] by simp |
|
461 |
|
462 lemma Float_cases[case_names Float, cases type: float]: |
|
463 fixes f :: float |
|
464 obtains (Float) m e :: int where "f = Float m e" |
|
465 using Float_mantissa_exponent[symmetric] |
|
466 by (atomize_elim) auto |
|
467 |
|
468 lemma |
|
469 fixes m e :: int |
|
470 defines "f \<equiv> float_of (m * 2 powr e)" |
|
471 assumes dvd: "\<not> 2 dvd m" |
|
472 shows mantissa_float: "mantissa f = m" (is "?M") |
|
473 and exponent_float: "m \<noteq> 0 \<Longrightarrow> exponent f = e" (is "_ \<Longrightarrow> ?E") |
|
474 proof cases |
|
475 assume "m = 0" with dvd show "mantissa f = m" by auto |
|
476 next |
|
477 assume "m \<noteq> 0" |
|
478 then have f_not_0: "f \<noteq> float_of 0" by (simp add: f_def) |
|
479 from mantissa_exponent[of f] |
|
480 have "m * 2 powr e = mantissa f * 2 powr exponent f" |
|
481 by (auto simp add: f_def) |
|
482 then show "?M" "?E" |
|
483 using mantissa_not_dvd[OF f_not_0] dvd |
|
484 by (auto simp: mult_powr_eq_mult_powr_iff) |
|
485 qed |
|
486 |
|
487 lemma denormalize_shift: |
|
488 assumes f_def: "f \<equiv> Float m e" and not_0: "f \<noteq> float_of 0" |
|
489 obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i" |
|
490 proof |
|
491 from mantissa_exponent[of f] f_def |
|
492 have "m * 2 powr e = mantissa f * 2 powr exponent f" |
|
493 by simp |
|
494 then have eq: "m = mantissa f * 2 powr (exponent f - e)" |
|
495 by (simp add: powr_divide2[symmetric] field_simps) |
|
496 moreover |
|
497 have "e \<le> exponent f" |
|
498 proof (rule ccontr) |
|
499 assume "\<not> e \<le> exponent f" |
|
500 then have pos: "exponent f < e" by simp |
|
501 then have "2 powr (exponent f - e) = 2 powr - real (e - exponent f)" |
|
502 by simp |
|
503 also have "\<dots> = 1 / 2^nat (e - exponent f)" |
|
504 using pos by (simp add: powr_realpow[symmetric] powr_divide2[symmetric]) |
|
505 finally have "m * 2^nat (e - exponent f) = real (mantissa f)" |
|
506 using eq by simp |
|
507 then have "mantissa f = m * 2^nat (e - exponent f)" |
|
508 unfolding real_of_int_inject by simp |
|
509 with `exponent f < e` have "2 dvd mantissa f" |
|
510 apply (intro dvdI[where k="m * 2^(nat (e-exponent f)) div 2"]) |
|
511 apply (cases "nat (e - exponent f)") |
|
512 apply auto |
140 done |
513 done |
141 with ab have "Float a b = (if u = 0 then Float 0 0 else Float u v)" by auto |
514 then show False using mantissa_not_dvd[OF not_0] by simp |
142 then have ?case |
515 qed |
143 apply (case_tac "u=0") |
516 ultimately have "real m = mantissa f * 2^nat (exponent f - e)" |
144 apply (auto) |
517 by (simp add: powr_realpow[symmetric]) |
145 by (insert ou, auto) |
518 with `e \<le> exponent f` |
146 } |
519 show "m = mantissa f * 2 ^ nat (exponent f - e)" "e = exponent f - nat (exponent f - e)" |
147 note case2 = this |
520 unfolding real_of_int_inject by auto |
148 show ?case |
521 qed |
149 apply (case_tac "odd u \<or> u = 0") |
522 |
150 apply (rule case2) |
523 subsection {* Compute arithmetic operations *} |
151 apply simp |
524 |
152 apply (rule case1) |
525 lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k" |
153 apply auto |
526 by simp |
154 done |
527 |
155 qed |
528 lemma compute_float_neg_numeral[code_abbrev]: "Float (neg_numeral k) 0 = neg_numeral k" |
156 |
529 by simp |
157 lemma float_eq_odd_helper: |
530 |
158 assumes odd: "odd a'" |
531 lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1" |
159 and floateq: "real (Float a b) = real (Float a' b')" |
532 by simp |
160 shows "b \<le> b'" |
533 |
161 proof - |
534 lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)" |
162 from odd have "a' \<noteq> 0" by auto |
535 by (simp add: field_simps powr_add) |
163 with floateq have a': "real a' = real a * pow2 (b - b')" |
536 |
164 by (simp add: pow2_diff field_simps) |
537 lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 = |
165 |
538 (if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1 |
166 { |
539 else Float (m2 + m1 * 2^nat (e1 - e2)) e2)" |
167 assume bcmp: "b > b'" |
540 by (simp add: field_simps) |
168 then obtain c :: nat where "b - b' = int c + 1" |
541 (simp add: powr_realpow[symmetric] powr_divide2[symmetric]) |
169 by atomize_elim arith |
542 |
170 with a' have "real a' = real (a * 2^c * 2)" |
543 lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)" by simp |
171 by (simp add: pow2_def nat_add_distrib) |
544 |
172 with odd have False |
545 lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)" |
173 unfolding real_of_int_inject by simp |
546 by (simp add: sgn_times) |
174 } |
547 |
175 then show ?thesis by arith |
548 definition is_float_pos :: "float \<Rightarrow> bool" where |
176 qed |
549 "is_float_pos f \<longleftrightarrow> 0 < f" |
177 |
550 |
178 lemma float_eq_odd: |
551 lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m" |
179 assumes odd1: "odd a" |
552 by (auto simp add: is_float_pos_def zero_less_mult_iff) (simp add: not_le[symmetric]) |
180 and odd2: "odd a'" |
553 |
181 and floateq: "real (Float a b) = real (Float a' b')" |
554 lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)" |
182 shows "a = a' \<and> b = b'" |
555 by (simp add: is_float_pos_def field_simps del: zero_float_def) |
183 proof - |
556 |
184 from |
557 definition is_float_nonneg :: "float \<Rightarrow> bool" where |
185 float_eq_odd_helper[OF odd2 floateq] |
558 "is_float_nonneg f \<longleftrightarrow> 0 \<le> f" |
186 float_eq_odd_helper[OF odd1 floateq[symmetric]] |
559 |
187 have beq: "b = b'" by arith |
560 lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m" |
188 with floateq show ?thesis by auto |
561 by (auto simp add: is_float_nonneg_def zero_le_mult_iff) (simp add: not_less[symmetric]) |
189 qed |
562 |
190 |
563 lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)" |
191 theorem normfloat_unique: |
564 by (simp add: is_float_nonneg_def field_simps del: zero_float_def) |
192 assumes real_of_float_eq: "real f = real g" |
565 |
193 shows "normfloat f = normfloat g" |
566 definition is_float_zero :: "float \<Rightarrow> bool" where |
194 proof - |
567 "is_float_zero f \<longleftrightarrow> 0 = f" |
195 from float_split[of "normfloat f"] obtain a b where normf:"normfloat f = Float a b" by auto |
568 |
196 from float_split[of "normfloat g"] obtain a' b' where normg:"normfloat g = Float a' b'" by auto |
569 lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m" |
197 have "real (normfloat f) = real (normfloat g)" |
570 by (auto simp add: is_float_zero_def) |
198 by (simp add: real_of_float_eq) |
571 |
199 then have float_eq: "real (Float a b) = real (Float a' b')" |
572 lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e" by (simp add: abs_mult) |
200 by (simp add: normf normg) |
573 |
201 have ab: "odd a \<or> (a = 0 \<and> b = 0)" by (rule normfloat_imp_odd_or_zero[OF normf]) |
574 instantiation float :: equal |
202 have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg]) |
|
203 { |
|
204 assume odd: "odd a" |
|
205 then have "a \<noteq> 0" by (simp add: even_def) arith |
|
206 with float_eq have "a' \<noteq> 0" by auto |
|
207 with ab' have "odd a'" by simp |
|
208 from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd) |
|
209 } |
|
210 note odd_case = this |
|
211 { |
|
212 assume even: "even a" |
|
213 with ab have a0: "a = 0" by simp |
|
214 with float_eq have a0': "a' = 0" by auto |
|
215 from a0 a0' ab ab' have "a = a' \<and> b = b'" by auto |
|
216 } |
|
217 note even_case = this |
|
218 from odd_case even_case show ?thesis |
|
219 apply (simp add: normf normg) |
|
220 apply (case_tac "even a") |
|
221 apply auto |
|
222 done |
|
223 qed |
|
224 |
|
225 instantiation float :: plus |
|
226 begin |
575 begin |
227 fun plus_float where |
576 |
228 [simp del]: "(Float a_m a_e) + (Float b_m b_e) = |
577 definition "equal_float (f1 :: float) f2 \<longleftrightarrow> is_float_zero (f1 - f2)" |
229 (if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e - a_e))) a_e |
578 |
230 else Float (a_m * 2^(nat (a_e - b_e)) + b_m) b_e)" |
579 instance proof qed (auto simp: equal_float_def is_float_zero_def simp del: zero_float_def) |
231 instance .. |
|
232 end |
580 end |
233 |
581 |
234 instantiation float :: uminus |
582 subsection {* Rounding Real numbers *} |
235 begin |
583 |
236 primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e" |
584 definition round_down :: "int \<Rightarrow> real \<Rightarrow> real" where |
237 instance .. |
585 "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec" |
238 end |
586 |
239 |
587 definition round_up :: "int \<Rightarrow> real \<Rightarrow> real" where |
240 instantiation float :: minus |
588 "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec" |
241 begin |
589 |
242 definition minus_float where "(z::float) - w = z + (- w)" |
590 lemma round_down_float[simp]: "round_down prec x \<in> float" |
243 instance .. |
591 unfolding round_down_def |
244 end |
592 by (auto intro!: times_float simp: real_of_int_minus[symmetric] simp del: real_of_int_minus) |
245 |
593 |
246 instantiation float :: times |
594 lemma round_up_float[simp]: "round_up prec x \<in> float" |
247 begin |
595 unfolding round_up_def |
248 fun times_float where [simp del]: "(Float a_m a_e) * (Float b_m b_e) = Float (a_m * b_m) (a_e + b_e)" |
596 by (auto intro!: times_float simp: real_of_int_minus[symmetric] simp del: real_of_int_minus) |
249 instance .. |
597 |
250 end |
598 lemma round_up: "x \<le> round_up prec x" |
251 |
599 by (simp add: powr_minus_divide le_divide_eq round_up_def) |
252 primrec float_pprt :: "float \<Rightarrow> float" where |
600 |
253 "float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)" |
601 lemma round_down: "round_down prec x \<le> x" |
254 |
602 by (simp add: powr_minus_divide divide_le_eq round_down_def) |
255 primrec float_nprt :: "float \<Rightarrow> float" where |
603 |
256 "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" |
604 lemma round_up_0[simp]: "round_up p 0 = 0" |
257 |
605 unfolding round_up_def by simp |
258 instantiation float :: ord |
606 |
259 begin |
607 lemma round_down_0[simp]: "round_down p 0 = 0" |
260 definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w" |
608 unfolding round_down_def by simp |
261 definition less_float_def: "z < (w :: float) \<equiv> real z < real w" |
609 |
262 instance .. |
610 lemma round_up_diff_round_down: |
263 end |
611 "round_up prec x - round_down prec x \<le> 2 powr -prec" |
264 |
612 proof - |
265 lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)" |
613 have "round_up prec x - round_down prec x = |
266 by (cases a, cases b) (simp add: algebra_simps plus_float.simps, |
614 (ceiling (x * 2 powr prec) - floor (x * 2 powr prec)) * 2 powr -prec" |
267 auto simp add: pow2_int[symmetric] pow2_add[symmetric]) |
615 by (simp add: round_up_def round_down_def field_simps) |
268 |
616 also have "\<dots> \<le> 1 * 2 powr -prec" |
269 lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)" |
617 by (rule mult_mono) |
270 by (cases a) simp |
618 (auto simp del: real_of_int_diff |
271 |
619 simp: real_of_int_diff[symmetric] real_of_int_le_one_cancel_iff ceiling_diff_floor_le_1) |
272 lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)" |
620 finally show ?thesis by simp |
273 by (cases a, cases b) (simp add: minus_float_def) |
621 qed |
274 |
622 |
275 lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)" |
623 lemma round_down_shift: "round_down p (x * 2 powr k) = 2 powr k * round_down (p + k) x" |
276 by (cases a, cases b) (simp add: times_float.simps pow2_add) |
624 unfolding round_down_def |
277 |
625 by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric]) |
278 lemma real_of_float_0[simp]: "real (0 :: float) = 0" |
626 (simp add: powr_add[symmetric]) |
279 by (auto simp add: zero_float_def) |
627 |
280 |
628 lemma round_up_shift: "round_up p (x * 2 powr k) = 2 powr k * round_up (p + k) x" |
281 lemma real_of_float_1[simp]: "real (1 :: float) = 1" |
629 unfolding round_up_def |
282 by (auto simp add: one_float_def) |
630 by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric]) |
283 |
631 (simp add: powr_add[symmetric]) |
284 lemma zero_le_float: |
632 |
285 "(0 <= real (Float a b)) = (0 <= a)" |
633 subsection {* Rounding Floats *} |
286 apply auto |
634 |
287 apply (auto simp add: zero_le_mult_iff) |
635 definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" where |
288 apply (insert zero_less_pow2[of b]) |
636 "float_up prec x = float_of (round_up prec (real x))" |
289 apply (simp_all) |
637 |
290 done |
638 lemma float_up_float: |
291 |
639 "x \<in> float \<Longrightarrow> float_up prec (float_of x) = float_of (round_up prec x)" |
292 lemma float_le_zero: |
640 unfolding float_up_def by simp |
293 "(real (Float a b) <= 0) = (a <= 0)" |
641 |
294 apply auto |
642 lemma float_up_correct: |
295 apply (auto simp add: mult_le_0_iff) |
643 shows "real (float_up e f) - real f \<in> {0..2 powr -e}" |
296 apply (insert zero_less_pow2[of b]) |
644 unfolding atLeastAtMost_iff |
297 apply auto |
645 proof |
298 done |
646 have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp |
299 |
647 also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp |
300 lemma zero_less_float: |
648 finally show "real (float_up e f) - real f \<le> 2 powr real (- e)" |
301 "(0 < real (Float a b)) = (0 < a)" |
649 by (simp add: float_up_def) |
302 apply auto |
650 qed (simp add: algebra_simps float_up_def round_up) |
303 apply (auto simp add: zero_less_mult_iff) |
651 |
304 apply (insert zero_less_pow2[of b]) |
652 definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" where |
305 apply (simp_all) |
653 "float_down prec x = float_of (round_down prec (real x))" |
306 done |
654 |
307 |
655 lemma float_down_float: |
308 lemma float_less_zero: |
656 "x \<in> float \<Longrightarrow> float_down prec (float_of x) = float_of (round_down prec x)" |
309 "(real (Float a b) < 0) = (a < 0)" |
657 unfolding float_down_def by simp |
310 apply auto |
658 |
311 apply (auto simp add: mult_less_0_iff) |
659 lemma float_down_correct: |
312 apply (insert zero_less_pow2[of b]) |
660 shows "real f - real (float_down e f) \<in> {0..2 powr -e}" |
313 apply (simp_all) |
661 unfolding atLeastAtMost_iff |
314 done |
662 proof |
315 |
663 have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp |
316 declare real_of_float_simp[simp del] |
664 also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp |
317 |
665 finally show "real f - real (float_down e f) \<le> 2 powr real (- e)" |
318 lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)" |
666 by (simp add: float_down_def) |
319 by (cases a) (auto simp add: zero_le_float float_le_zero) |
667 qed (simp add: algebra_simps float_down_def round_down) |
320 |
668 |
321 lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)" |
669 lemma round_down_Float_id: |
322 by (cases a) (auto simp add: zero_le_float float_le_zero) |
670 assumes "p + e \<ge> 0" |
323 |
671 shows "round_down p (Float m e) = Float m e" |
324 instance float :: ab_semigroup_add |
672 proof - |
325 proof (intro_classes) |
673 from assms have r: "real e + real p = real (nat (e + p))" by simp |
326 fix a b c :: float |
674 have r: "\<lfloor>real (Float m e) * 2 powr real p\<rfloor> = real (Float m e) * 2 powr real p" |
327 show "a + b + c = a + (b + c)" |
675 by (auto intro: exI[where x="m*2^nat (e+p)"] |
328 by (cases a, cases b, cases c) |
676 simp add: ac_simps powr_add[symmetric] r powr_realpow) |
329 (auto simp add: algebra_simps power_add[symmetric] plus_float.simps) |
677 show ?thesis using assms |
|
678 unfolding round_down_def floor_divide_eq_div r |
|
679 by (simp add: ac_simps powr_add[symmetric]) |
|
680 qed |
|
681 |
|
682 lemma compute_float_down[code]: |
|
683 "float_down p (Float m e) = |
|
684 (if p + e < 0 then Float (m div 2^nat (-(p + e))) (-p) else Float m e)" |
|
685 proof cases |
|
686 assume "p + e < 0" |
|
687 hence "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))" |
|
688 using powr_realpow[of 2 "nat (-(p + e))"] by simp |
|
689 also have "... = 1 / 2 powr p / 2 powr e" |
|
690 unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add) |
|
691 finally show ?thesis |
|
692 unfolding float_down_def round_down_def floor_divide_eq_div[symmetric] |
|
693 using `p + e < 0` by (simp add: ac_simps) |
330 next |
694 next |
331 fix a b :: float |
695 assume "\<not> p + e < 0" with round_down_Float_id show ?thesis by (simp add: float_down_def) |
332 show "a + b = b + a" |
696 qed |
333 by (cases a, cases b) (simp add: plus_float.simps) |
697 |
334 qed |
698 lemma ceil_divide_floor_conv: |
335 |
699 assumes "b \<noteq> 0" |
336 instance float :: numeral .. |
700 shows "\<lceil>real a / real b\<rceil> = (if b dvd a then a div b else \<lfloor>real a / real b\<rfloor> + 1)" |
337 |
701 proof cases |
338 lemma Float_add_same_scale: "Float x e + Float y e = Float (x + y) e" |
702 assume "\<not> b dvd a" |
339 by (simp add: plus_float.simps) |
703 hence "a mod b \<noteq> 0" by auto |
340 |
704 hence ne: "real (a mod b) / real b \<noteq> 0" using `b \<noteq> 0` by auto |
341 (* FIXME: define other constant for code_unfold_post *) |
705 have "\<lceil>real a / real b\<rceil> = \<lfloor>real a / real b\<rfloor> + 1" |
342 lemma numeral_float_Float (*[code_unfold_post]*): |
706 apply (rule ceiling_eq) apply (auto simp: floor_divide_eq_div[symmetric]) |
343 "numeral k = Float (numeral k) 0" |
707 proof - |
344 by (induct k, simp_all only: numeral.simps one_float_def |
708 have "real \<lfloor>real a / real b\<rfloor> \<le> real a / real b" by simp |
345 Float_add_same_scale) |
709 moreover have "real \<lfloor>real a / real b\<rfloor> \<noteq> real a / real b" |
346 |
710 apply (subst (2) real_of_int_div_aux) unfolding floor_divide_eq_div using ne `b \<noteq> 0` by auto |
347 lemma float_number_of[simp]: "real (numeral x :: float) = numeral x" |
711 ultimately show "real \<lfloor>real a / real b\<rfloor> < real a / real b" by arith |
348 by (simp only: numeral_float_Float Float_num) |
|
349 |
|
350 |
|
351 instance float :: comm_monoid_mult |
|
352 proof (intro_classes) |
|
353 fix a b c :: float |
|
354 show "a * b * c = a * (b * c)" |
|
355 by (cases a, cases b, cases c) (simp add: times_float.simps) |
|
356 next |
|
357 fix a b :: float |
|
358 show "a * b = b * a" |
|
359 by (cases a, cases b) (simp add: times_float.simps) |
|
360 next |
|
361 fix a :: float |
|
362 show "1 * a = a" |
|
363 by (cases a) (simp add: times_float.simps one_float_def) |
|
364 qed |
|
365 |
|
366 (* Floats do NOT form a cancel_semigroup_add: *) |
|
367 lemma "0 + Float 0 1 = 0 + Float 0 2" |
|
368 by (simp add: plus_float.simps zero_float_def) |
|
369 |
|
370 instance float :: comm_semiring |
|
371 proof (intro_classes) |
|
372 fix a b c :: float |
|
373 show "(a + b) * c = a * c + b * c" |
|
374 by (cases a, cases b, cases c) (simp add: plus_float.simps times_float.simps algebra_simps) |
|
375 qed |
|
376 |
|
377 (* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *) |
|
378 |
|
379 instance float :: zero_neq_one |
|
380 proof (intro_classes) |
|
381 show "(0::float) \<noteq> 1" |
|
382 by (simp add: zero_float_def one_float_def) |
|
383 qed |
|
384 |
|
385 lemma float_le_simp: "((x::float) \<le> y) = (0 \<le> y - x)" |
|
386 by (auto simp add: le_float_def) |
|
387 |
|
388 lemma float_less_simp: "((x::float) < y) = (0 < y - x)" |
|
389 by (auto simp add: less_float_def) |
|
390 |
|
391 lemma real_of_float_min: "real (min x y :: float) = min (real x) (real y)" unfolding min_def le_float_def by auto |
|
392 lemma real_of_float_max: "real (max a b :: float) = max (real a) (real b)" unfolding max_def le_float_def by auto |
|
393 |
|
394 lemma float_power: "real (x ^ n :: float) = real x ^ n" |
|
395 by (induct n) simp_all |
|
396 |
|
397 lemma zero_le_pow2[simp]: "0 \<le> pow2 s" |
|
398 apply (subgoal_tac "0 < pow2 s") |
|
399 apply (auto simp only:) |
|
400 apply auto |
|
401 done |
|
402 |
|
403 lemma pow2_less_0_eq_False[simp]: "(pow2 s < 0) = False" |
|
404 apply auto |
|
405 apply (subgoal_tac "0 \<le> pow2 s") |
|
406 apply simp |
|
407 apply simp |
|
408 done |
|
409 |
|
410 lemma pow2_le_0_eq_False[simp]: "(pow2 s \<le> 0) = False" |
|
411 apply auto |
|
412 apply (subgoal_tac "0 < pow2 s") |
|
413 apply simp |
|
414 apply simp |
|
415 done |
|
416 |
|
417 lemma float_pos_m_pos: "0 < Float m e \<Longrightarrow> 0 < m" |
|
418 unfolding less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff |
|
419 by auto |
|
420 |
|
421 lemma float_pos_less1_e_neg: assumes "0 < Float m e" and "Float m e < 1" shows "e < 0" |
|
422 proof - |
|
423 have "0 < m" using float_pos_m_pos `0 < Float m e` by auto |
|
424 hence "0 \<le> real m" and "1 \<le> real m" by auto |
|
425 |
|
426 show "e < 0" |
|
427 proof (rule ccontr) |
|
428 assume "\<not> e < 0" hence "0 \<le> e" by auto |
|
429 hence "1 \<le> pow2 e" unfolding pow2_def by auto |
|
430 from mult_mono[OF `1 \<le> real m` this `0 \<le> real m`] |
|
431 have "1 \<le> Float m e" by (simp add: le_float_def real_of_float_simp) |
|
432 thus False using `Float m e < 1` unfolding less_float_def le_float_def by auto |
|
433 qed |
712 qed |
434 qed |
713 thus ?thesis using `\<not> b dvd a` by simp |
435 |
714 qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric] |
436 lemma float_less1_mantissa_bound: assumes "0 < Float m e" "Float m e < 1" shows "m < 2^(nat (-e))" |
715 floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus) |
437 proof - |
716 |
438 have "e < 0" using float_pos_less1_e_neg assms by auto |
717 lemma round_up_Float_id: |
439 have "\<And>x. (0::real) < 2^x" by auto |
718 assumes "p + e \<ge> 0" |
440 have "real m < 2^(nat (-e))" using `Float m e < 1` |
719 shows "round_up p (Float m e) = Float m e" |
441 unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1 |
720 proof - |
442 real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric] |
721 from assms have r1: "real e + real p = real (nat (e + p))" by simp |
443 mult_assoc by auto |
722 have r: "\<lceil>real (Float m e) * 2 powr real p\<rceil> = real (Float m e) * 2 powr real p" |
444 thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto |
723 by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow |
445 qed |
724 intro: exI[where x="m*2^nat (e+p)"]) |
446 |
725 show ?thesis using assms |
447 function bitlen :: "int \<Rightarrow> int" where |
726 unfolding float_up_def round_up_def floor_divide_eq_div Let_def r |
448 "bitlen 0 = 0" | |
727 by (simp add: ac_simps powr_add[symmetric]) |
449 "bitlen -1 = 1" | |
728 qed |
450 "0 < x \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))" | |
729 |
451 "x < -1 \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))" |
730 lemma compute_float_up[code]: |
452 apply (case_tac "x = 0 \<or> x = -1 \<or> x < -1 \<or> x > 0") |
731 "float_up p (Float m e) = |
453 apply auto |
732 (let P = 2^nat (-(p + e)); r = m mod P in |
454 done |
733 if p + e < 0 then Float (m div P + (if r = 0 then 0 else 1)) (-p) else Float m e)" |
455 termination by (relation "measure (nat o abs)", auto) |
734 proof cases |
456 |
735 assume "p + e < 0" |
457 lemma bitlen_ge0: "0 \<le> bitlen x" by (induct x rule: bitlen.induct, auto) |
736 hence "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))" |
458 lemma bitlen_ge1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> bitlen x" by (induct x rule: bitlen.induct, auto simp add: bitlen_ge0) |
737 using powr_realpow[of 2 "nat (-(p + e))"] by simp |
459 |
738 also have "... = 1 / 2 powr p / 2 powr e" |
460 lemma bitlen_bounds': assumes "0 < x" shows "2^nat (bitlen x - 1) \<le> x \<and> x + 1 \<le> 2^nat (bitlen x)" (is "?P x") |
739 unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add) |
461 using `0 < x` |
740 finally have twopow_rewrite: |
462 proof (induct x rule: bitlen.induct) |
741 "real ((2::int) ^ nat (- (p + e))) = 1 / 2 powr real p / 2 powr real e" . |
463 fix x |
742 with `p + e < 0` have powr_rewrite: |
464 assume "0 < x" and hyp: "0 < x div 2 \<Longrightarrow> ?P (x div 2)" hence "0 \<le> x" and "x \<noteq> 0" by auto |
743 "2 powr real e * 2 powr real p = 1 / real ((2::int) ^ nat (- (p + e)))" |
465 { fix x have "0 \<le> 1 + bitlen x" using bitlen_ge0[of x] by auto } note gt0_pls1 = this |
744 unfolding powr_divide2 by simp |
466 |
745 show ?thesis |
467 have "0 < (2::int)" by auto |
746 proof cases |
468 |
747 assume "2^nat (-(p + e)) dvd m" |
469 show "?P x" |
748 with `p + e < 0` twopow_rewrite show ?thesis |
470 proof (cases "x = 1") |
749 by (auto simp: ac_simps float_up_def round_up_def floor_divide_eq_div dvd_eq_mod_eq_0) |
471 case True show "?P x" unfolding True by auto |
|
472 next |
750 next |
473 case False hence "2 \<le> x" using `0 < x` `x \<noteq> 1` by auto |
751 assume ndvd: "\<not> 2 ^ nat (- (p + e)) dvd m" |
474 hence "2 div 2 \<le> x div 2" by (rule zdiv_mono1, auto) |
752 have one_div: "real m * (1 / real ((2::int) ^ nat (- (p + e)))) = |
475 hence "0 < x div 2" and "x div 2 \<noteq> 0" by auto |
753 real m / real ((2::int) ^ nat (- (p + e)))" |
476 hence bitlen_s1_ge0: "0 \<le> bitlen (x div 2) - 1" using bitlen_ge1[OF `x div 2 \<noteq> 0`] by auto |
754 by (simp add: field_simps) |
477 |
755 have "real \<lceil>real m * (2 powr real e * 2 powr real p)\<rceil> = |
478 { from hyp[OF `0 < x div 2`] |
756 real \<lfloor>real m * (2 powr real e * 2 powr real p)\<rfloor> + 1" |
479 have "2 ^ nat (bitlen (x div 2) - 1) \<le> x div 2" by auto |
757 using ndvd unfolding powr_rewrite one_div |
480 hence "2 ^ nat (bitlen (x div 2) - 1) * 2 \<le> x div 2 * 2" by (rule mult_right_mono, auto) |
758 by (subst ceil_divide_floor_conv) (auto simp: field_simps) |
481 also have "\<dots> \<le> x" using `0 < x` by auto |
759 thus ?thesis using `p + e < 0` twopow_rewrite |
482 finally have "2^nat (1 + bitlen (x div 2) - 1) \<le> x" unfolding power_Suc2[symmetric] Suc_nat_eq_nat_zadd1[OF bitlen_s1_ge0] by auto |
760 by (auto simp: ac_simps Let_def float_up_def round_up_def floor_divide_eq_div[symmetric]) |
483 } moreover |
|
484 { have "x + 1 \<le> x - x mod 2 + 2" |
|
485 proof - |
|
486 have "x mod 2 < 2" using `0 < x` by auto |
|
487 hence "x < x - x mod 2 + 2" unfolding algebra_simps by auto |
|
488 thus ?thesis by auto |
|
489 qed |
|
490 also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` div_mod_equality[of x 2 0] by auto |
|
491 also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto) |
|
492 also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto |
|
493 finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" . |
|
494 } |
|
495 ultimately show ?thesis |
|
496 unfolding bitlen.simps(3)[OF `0 < x`] nat_add_distrib[OF zero_le_one bitlen_ge0] |
|
497 unfolding add_commute nat_add_distrib[OF zero_le_one gt0_pls1] |
|
498 by auto |
|
499 qed |
761 qed |
500 next |
762 next |
501 fix x :: int assume "x < -1" and "0 < x" hence False by auto |
763 assume "\<not> p + e < 0" with round_up_Float_id show ?thesis by (simp add: float_up_def) |
502 thus "?P x" by auto |
764 qed |
503 qed auto |
765 |
504 |
766 lemmas real_of_ints = |
505 lemma bitlen_bounds: assumes "0 < x" shows "2^nat (bitlen x - 1) \<le> x \<and> x < 2^nat (bitlen x)" |
767 real_of_int_zero |
506 using bitlen_bounds'[OF `0<x`] by auto |
768 real_of_one |
|
769 real_of_int_add |
|
770 real_of_int_minus |
|
771 real_of_int_diff |
|
772 real_of_int_mult |
|
773 real_of_int_power |
|
774 real_numeral |
|
775 lemmas real_of_nats = |
|
776 real_of_nat_zero |
|
777 real_of_nat_one |
|
778 real_of_nat_1 |
|
779 real_of_nat_add |
|
780 real_of_nat_mult |
|
781 real_of_nat_power |
|
782 |
|
783 lemmas int_of_reals = real_of_ints[symmetric] |
|
784 lemmas nat_of_reals = real_of_nats[symmetric] |
|
785 |
|
786 lemma two_real_int: "(2::real) = real (2::int)" by simp |
|
787 lemma two_real_nat: "(2::real) = real (2::nat)" by simp |
|
788 |
|
789 lemma mult_cong: "a = c ==> b = d ==> a*b = c*d" by simp |
|
790 |
|
791 subsection {* Compute bitlen of integers *} |
|
792 |
|
793 definition bitlen::"int => int" |
|
794 where "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)" |
|
795 |
|
796 lemma bitlen_nonneg: "0 \<le> bitlen x" |
|
797 proof - |
|
798 { |
|
799 assume "0 > x" |
|
800 have "-1 = log 2 (inverse 2)" by (subst log_inverse) simp_all |
|
801 also have "... < log 2 (-x)" using `0 > x` by auto |
|
802 finally have "-1 < log 2 (-x)" . |
|
803 } thus "0 \<le> bitlen x" unfolding bitlen_def by (auto intro!: add_nonneg_nonneg) |
|
804 qed |
|
805 |
|
806 lemma bitlen_bounds: |
|
807 assumes "x > 0" |
|
808 shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)" |
|
809 proof |
|
810 have "(2::real) ^ nat \<lfloor>log 2 (real x)\<rfloor> = 2 powr real (floor (log 2 (real x)))" |
|
811 using powr_realpow[symmetric, of 2 "nat \<lfloor>log 2 (real x)\<rfloor>"] `x > 0` |
|
812 using real_nat_eq_real[of "floor (log 2 (real x))"] |
|
813 by simp |
|
814 also have "... \<le> 2 powr log 2 (real x)" |
|
815 by simp |
|
816 also have "... = real x" |
|
817 using `0 < x` by simp |
|
818 finally have "2 ^ nat \<lfloor>log 2 (real x)\<rfloor> \<le> real x" by simp |
|
819 thus "2 ^ nat (bitlen x - 1) \<le> x" using `x > 0` |
|
820 by (simp add: bitlen_def) |
|
821 next |
|
822 have "x \<le> 2 powr (log 2 x)" using `x > 0` by simp |
|
823 also have "... < 2 ^ nat (\<lfloor>log 2 (real x)\<rfloor> + 1)" |
|
824 apply (simp add: powr_realpow[symmetric]) |
|
825 using `x > 0` by simp |
|
826 finally show "x < 2 ^ nat (bitlen x)" using `x > 0` |
|
827 by (simp add: bitlen_def ac_simps int_of_reals del: real_of_ints) |
|
828 qed |
|
829 |
|
830 lemma bitlen_pow2[simp]: |
|
831 assumes "b > 0" |
|
832 shows "bitlen (b * 2 ^ c) = bitlen b + c" |
|
833 proof - |
|
834 from assms have "b * 2 ^ c > 0" by (auto intro: mult_pos_pos) |
|
835 thus ?thesis |
|
836 using floor_add[of "log 2 b" c] assms |
|
837 by (auto simp add: log_mult log_nat_power bitlen_def) |
|
838 qed |
|
839 |
|
840 lemma bitlen_Float: |
|
841 fixes m e |
|
842 defines "f \<equiv> Float m e" |
|
843 shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)" |
|
844 proof cases |
|
845 assume "m \<noteq> 0" hence "f \<noteq> float_of 0" by (simp add: f_def) hence "mantissa f \<noteq> 0" |
|
846 by (simp add: mantissa_noteq_0) |
|
847 moreover |
|
848 from f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`] guess i . |
|
849 ultimately show ?thesis by (simp add: abs_mult) |
|
850 qed (simp add: f_def bitlen_def) |
|
851 |
|
852 lemma compute_bitlen[code]: |
|
853 shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)" |
|
854 proof - |
|
855 { assume "2 \<le> x" |
|
856 then have "\<lfloor>log 2 (x div 2)\<rfloor> + 1 = \<lfloor>log 2 (x - x mod 2)\<rfloor>" |
|
857 by (simp add: log_mult zmod_zdiv_equality') |
|
858 also have "\<dots> = \<lfloor>log 2 (real x)\<rfloor>" |
|
859 proof cases |
|
860 assume "x mod 2 = 0" then show ?thesis by simp |
|
861 next |
|
862 def n \<equiv> "\<lfloor>log 2 (real x)\<rfloor>" |
|
863 then have "0 \<le> n" |
|
864 using `2 \<le> x` by simp |
|
865 assume "x mod 2 \<noteq> 0" |
|
866 with `2 \<le> x` have "x mod 2 = 1" "\<not> 2 dvd x" by (auto simp add: dvd_eq_mod_eq_0) |
|
867 with `2 \<le> x` have "x \<noteq> 2^nat n" by (cases "nat n") auto |
|
868 moreover |
|
869 { have "real (2^nat n :: int) = 2 powr (nat n)" |
|
870 by (simp add: powr_realpow) |
|
871 also have "\<dots> \<le> 2 powr (log 2 x)" |
|
872 using `2 \<le> x` by (simp add: n_def del: powr_log_cancel) |
|
873 finally have "2^nat n \<le> x" using `2 \<le> x` by simp } |
|
874 ultimately have "2^nat n \<le> x - 1" by simp |
|
875 then have "2^nat n \<le> real (x - 1)" |
|
876 unfolding real_of_int_le_iff[symmetric] by simp |
|
877 { have "n = \<lfloor>log 2 (2^nat n)\<rfloor>" |
|
878 using `0 \<le> n` by (simp add: log_nat_power) |
|
879 also have "\<dots> \<le> \<lfloor>log 2 (x - 1)\<rfloor>" |
|
880 using `2^nat n \<le> real (x - 1)` `0 \<le> n` `2 \<le> x` by (auto intro: floor_mono) |
|
881 finally have "n \<le> \<lfloor>log 2 (x - 1)\<rfloor>" . } |
|
882 moreover have "\<lfloor>log 2 (x - 1)\<rfloor> \<le> n" |
|
883 using `2 \<le> x` by (auto simp add: n_def intro!: floor_mono) |
|
884 ultimately show "\<lfloor>log 2 (x - x mod 2)\<rfloor> = \<lfloor>log 2 x\<rfloor>" |
|
885 unfolding n_def `x mod 2 = 1` by auto |
|
886 qed |
|
887 finally have "\<lfloor>log 2 (x div 2)\<rfloor> + 1 = \<lfloor>log 2 x\<rfloor>" . } |
|
888 moreover |
|
889 { assume "x < 2" "0 < x" |
|
890 then have "x = 1" by simp |
|
891 then have "\<lfloor>log 2 (real x)\<rfloor> = 0" by simp } |
|
892 ultimately show ?thesis |
|
893 unfolding bitlen_def |
|
894 by (auto simp: pos_imp_zdiv_pos_iff not_le) |
|
895 qed |
|
896 |
|
897 lemma float_gt1_scale: assumes "1 \<le> Float m e" |
|
898 shows "0 \<le> e + (bitlen m - 1)" |
|
899 proof - |
|
900 have "0 < Float m e" using assms by auto |
|
901 hence "0 < m" using powr_gt_zero[of 2 e] |
|
902 by (auto simp: less_float_def less_eq_float_def zero_less_mult_iff) |
|
903 hence "m \<noteq> 0" by auto |
|
904 show ?thesis |
|
905 proof (cases "0 \<le> e") |
|
906 case True thus ?thesis using `0 < m` by (simp add: bitlen_def) |
|
907 next |
|
908 have "(1::int) < 2" by simp |
|
909 case False let ?S = "2^(nat (-e))" |
|
910 have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"] |
|
911 by (auto simp: powr_minus field_simps inverse_eq_divide) |
|
912 hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"] |
|
913 by (auto simp: powr_minus) |
|
914 hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto) |
|
915 hence "?S \<le> real m" unfolding mult_assoc by auto |
|
916 hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto |
|
917 from this bitlen_bounds[OF `0 < m`, THEN conjunct2] |
|
918 have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans) |
|
919 hence "-e < bitlen m" using False by auto |
|
920 thus ?thesis by auto |
|
921 qed |
|
922 qed |
507 |
923 |
508 lemma bitlen_div: assumes "0 < m" shows "1 \<le> real m / 2^nat (bitlen m - 1)" and "real m / 2^nat (bitlen m - 1) < 2" |
924 lemma bitlen_div: assumes "0 < m" shows "1 \<le> real m / 2^nat (bitlen m - 1)" and "real m / 2^nat (bitlen m - 1) < 2" |
509 proof - |
925 proof - |
510 let ?B = "2^nat(bitlen m - 1)" |
926 let ?B = "2^nat(bitlen m - 1)" |
511 |
927 |
512 have "?B \<le> m" using bitlen_bounds[OF `0 <m`] .. |
928 have "?B \<le> m" using bitlen_bounds[OF `0 <m`] .. |
513 hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto |
929 hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto |
514 thus "1 \<le> real m / ?B" by auto |
930 thus "1 \<le> real m / ?B" by auto |
515 |
931 |
516 have "m \<noteq> 0" using assms by auto |
932 have "m \<noteq> 0" using assms by auto |
517 have "0 \<le> bitlen m - 1" using bitlen_ge1[OF `m \<noteq> 0`] by auto |
933 have "0 \<le> bitlen m - 1" using `0 < m` by (auto simp: bitlen_def) |
518 |
934 |
519 have "m < 2^nat(bitlen m)" using bitlen_bounds[OF `0 <m`] .. |
935 have "m < 2^nat(bitlen m)" using bitlen_bounds[OF `0 <m`] .. |
520 also have "\<dots> = 2^nat(bitlen m - 1 + 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto |
936 also have "\<dots> = 2^nat(bitlen m - 1 + 1)" using `0 < m` by (auto simp: bitlen_def) |
521 also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF `0 \<le> bitlen m - 1` zero_le_one] by auto |
937 also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF `0 \<le> bitlen m - 1` zero_le_one] by auto |
522 finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto |
938 finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto |
523 hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto) |
939 hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto) |
524 thus "real m / ?B < 2" by auto |
940 thus "real m / ?B < 2" by auto |
525 qed |
941 qed |
526 |
942 |
527 lemma float_gt1_scale: assumes "1 \<le> Float m e" |
943 subsection {* Approximation of positive rationals *} |
528 shows "0 \<le> e + (bitlen m - 1)" |
944 |
529 proof (cases "0 \<le> e") |
945 lemma zdiv_zmult_twopow_eq: fixes a b::int shows "a div b div (2 ^ n) = a div (b * 2 ^ n)" |
530 have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto |
946 by (simp add: zdiv_zmult2_eq) |
531 hence "0 < m" using float_pos_m_pos by auto |
947 |
532 hence "m \<noteq> 0" by auto |
948 lemma div_mult_twopow_eq: fixes a b::nat shows "a div ((2::nat) ^ n) div b = a div (b * 2 ^ n)" |
533 case True with bitlen_ge1[OF `m \<noteq> 0`] show ?thesis by auto |
949 by (cases "b=0") (simp_all add: div_mult2_eq[symmetric] ac_simps) |
|
950 |
|
951 lemma real_div_nat_eq_floor_of_divide: |
|
952 fixes a b::nat |
|
953 shows "a div b = real (floor (a/b))" |
|
954 by (metis floor_divide_eq_div real_of_int_of_nat_eq zdiv_int) |
|
955 |
|
956 definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)" |
|
957 |
|
958 definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" where |
|
959 "lapprox_posrat prec x y = float_of (round_down (rat_precision prec x y) (x / y))" |
|
960 |
|
961 lemma compute_lapprox_posrat[code]: |
|
962 fixes prec x y |
|
963 shows "lapprox_posrat prec x y = |
|
964 (let |
|
965 l = rat_precision prec x y; |
|
966 d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y |
|
967 in normfloat (Float d (- l)))" |
|
968 unfolding lapprox_posrat_def div_mult_twopow_eq |
|
969 by (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide |
|
970 field_simps Let_def |
|
971 del: two_powr_minus_int_float) |
|
972 |
|
973 definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" where |
|
974 "rapprox_posrat prec x y = float_of (round_up (rat_precision prec x y) (x / y))" |
|
975 |
|
976 (* TODO: optimize using zmod_zmult2_eq, pdivmod ? *) |
|
977 lemma compute_rapprox_posrat[code]: |
|
978 fixes prec x y |
|
979 defines "l \<equiv> rat_precision prec x y" |
|
980 shows "rapprox_posrat prec x y = (let |
|
981 l = l ; |
|
982 X = if 0 \<le> l then (x * 2^nat l, y) else (x, y * 2^nat(-l)) ; |
|
983 d = fst X div snd X ; |
|
984 m = fst X mod snd X |
|
985 in normfloat (Float (d + (if m = 0 \<or> y = 0 then 0 else 1)) (- l)))" |
|
986 proof (cases "y = 0") |
|
987 assume "y = 0" thus ?thesis by (simp add: rapprox_posrat_def Let_def) |
534 next |
988 next |
535 have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto |
989 assume "y \<noteq> 0" |
536 hence "0 < m" using float_pos_m_pos by auto |
|
537 hence "m \<noteq> 0" and "1 < (2::int)" by auto |
|
538 case False let ?S = "2^(nat (-e))" |
|
539 have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def real_of_float_nge0_exp[OF False] by auto |
|
540 hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto) |
|
541 hence "?S \<le> real m" unfolding mult_assoc by auto |
|
542 hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto |
|
543 from this bitlen_bounds[OF `0 < m`, THEN conjunct2] |
|
544 have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans) |
|
545 hence "-e < bitlen m" using False bitlen_ge0 by auto |
|
546 thus ?thesis by auto |
|
547 qed |
|
548 |
|
549 lemma normalized_float: assumes "m \<noteq> 0" shows "real (Float m (- (bitlen m - 1))) = real m / 2^nat (bitlen m - 1)" |
|
550 proof (cases "- (bitlen m - 1) = 0") |
|
551 case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto |
|
552 next |
|
553 case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto |
|
554 show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto |
|
555 qed |
|
556 |
|
557 (* BROKEN |
|
558 lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp) |
|
559 |
|
560 lemma bitlen_Min: "bitlen (Int.Min) = Int.Bit1 Int.Pls" by (subst Min_def, simp add: Bit1_def) |
|
561 |
|
562 lemma bitlen_B0: "bitlen (Int.Bit0 b) = (if iszero b then Int.Pls else Int.succ (bitlen b))" |
|
563 apply (auto simp add: iszero_def succ_def) |
|
564 apply (simp add: Bit0_def Pls_def) |
|
565 apply (subst Bit0_def) |
|
566 apply simp |
|
567 apply (subgoal_tac "0 < 2 * b \<or> 2 * b < -1") |
|
568 apply auto |
|
569 done |
|
570 |
|
571 lemma bitlen_B1: "bitlen (Int.Bit1 b) = (if iszero (Int.succ b) then Int.Bit1 Int.Pls else Int.succ (bitlen b))" |
|
572 proof - |
|
573 have h: "! x. (2*x + 1) div 2 = (x::int)" |
|
574 by arith |
|
575 show ?thesis |
990 show ?thesis |
576 apply (auto simp add: iszero_def succ_def) |
991 proof (cases "0 \<le> l") |
577 apply (subst Bit1_def)+ |
992 assume "0 \<le> l" |
578 apply simp |
993 def x' == "x * 2 ^ nat l" |
579 apply (subgoal_tac "2 * b + 1 = -1") |
994 have "int x * 2 ^ nat l = x'" by (simp add: x'_def int_mult int_power) |
580 apply (simp only:) |
995 moreover have "real x * 2 powr real l = real x'" |
581 apply simp_all |
996 by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def) |
582 apply (subst Bit1_def) |
997 ultimately show ?thesis |
583 apply simp |
998 unfolding rapprox_posrat_def round_up_def l_def[symmetric] |
584 apply (subgoal_tac "0 < 2 * b + 1 \<or> 2 * b + 1 < -1") |
999 using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0` |
585 apply (auto simp add: h) |
1000 by (simp add: Let_def floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 int_of_reals |
586 done |
1001 del: real_of_ints) |
587 qed |
1002 next |
588 |
1003 assume "\<not> 0 \<le> l" |
589 lemma bitlen_number_of: "bitlen (number_of w) = number_of (bitlen w)" |
1004 def y' == "y * 2 ^ nat (- l)" |
590 by (simp add: number_of_is_id) |
1005 from `y \<noteq> 0` have "y' \<noteq> 0" by (simp add: y'_def) |
591 BH *) |
1006 have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power) |
592 |
1007 moreover have "real x * real (2::int) powr real l / real y = x / real y'" |
593 lemma [code]: "bitlen x = |
1008 using `\<not> 0 \<le> l` |
594 (if x = 0 then 0 |
1009 by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide) |
595 else if x = -1 then 1 |
1010 ultimately show ?thesis |
596 else (1 + (bitlen (x div 2))))" |
1011 using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0` |
597 by (cases "x = 0 \<or> x = -1 \<or> 0 < x") auto |
1012 by (simp add: rapprox_posrat_def l_def round_up_def ceil_divide_floor_conv |
598 |
1013 floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 int_of_reals |
599 definition lapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" |
1014 del: real_of_ints) |
600 where |
|
601 "lapprox_posrat prec x y = |
|
602 (let |
|
603 l = nat (int prec + bitlen y - bitlen x) ; |
|
604 d = (x * 2^l) div y |
|
605 in normfloat (Float d (- (int l))))" |
|
606 |
|
607 lemma pow2_minus: "pow2 (-x) = inverse (pow2 x)" |
|
608 unfolding pow2_neg[of "-x"] by auto |
|
609 |
|
610 lemma lapprox_posrat: |
|
611 assumes x: "0 \<le> x" |
|
612 and y: "0 < y" |
|
613 shows "real (lapprox_posrat prec x y) \<le> real x / real y" |
|
614 proof - |
|
615 let ?l = "nat (int prec + bitlen y - bitlen x)" |
|
616 |
|
617 have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)" |
|
618 by (rule mult_right_mono, fact real_of_int_div4, simp) |
|
619 also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto |
|
620 finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding mult_assoc by auto |
|
621 thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp |
|
622 unfolding pow2_minus pow2_int minus_minus . |
|
623 qed |
|
624 |
|
625 lemma real_of_int_div_mult: |
|
626 fixes x y c :: int assumes "0 < y" and "0 < c" |
|
627 shows "real (x div y) \<le> real (x * c div y) * inverse (real c)" |
|
628 proof - |
|
629 have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y] |
|
630 by (rule add_left_mono, |
|
631 auto intro!: mult_nonneg_nonneg |
|
632 simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`]) |
|
633 hence "real (x div y) * real c \<le> real (x * c div y)" |
|
634 unfolding real_of_int_mult[symmetric] real_of_int_le_iff mult_commute by auto |
|
635 hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)" |
|
636 using `0 < c` by auto |
|
637 thus ?thesis unfolding mult_assoc using `0 < c` by auto |
|
638 qed |
|
639 |
|
640 lemma lapprox_posrat_bottom: assumes "0 < y" |
|
641 shows "real (x div y) \<le> real (lapprox_posrat n x y)" |
|
642 proof - |
|
643 have pow: "\<And>x. (0::int) < 2^x" by auto |
|
644 show ?thesis |
|
645 unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int |
|
646 using real_of_int_div_mult[OF `0 < y` pow] by auto |
|
647 qed |
|
648 |
|
649 lemma lapprox_posrat_nonneg: assumes "0 \<le> x" and "0 < y" |
|
650 shows "0 \<le> real (lapprox_posrat n x y)" |
|
651 proof - |
|
652 show ?thesis |
|
653 unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int |
|
654 using pos_imp_zdiv_nonneg_iff[OF `0 < y`] assms by (auto intro!: mult_nonneg_nonneg) |
|
655 qed |
|
656 |
|
657 definition rapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" |
|
658 where |
|
659 "rapprox_posrat prec x y = (let |
|
660 l = nat (int prec + bitlen y - bitlen x) ; |
|
661 X = x * 2^l ; |
|
662 d = X div y ; |
|
663 m = X mod y |
|
664 in normfloat (Float (d + (if m = 0 then 0 else 1)) (- (int l))))" |
|
665 |
|
666 lemma rapprox_posrat: |
|
667 assumes x: "0 \<le> x" |
|
668 and y: "0 < y" |
|
669 shows "real x / real y \<le> real (rapprox_posrat prec x y)" |
|
670 proof - |
|
671 let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l" |
|
672 show ?thesis |
|
673 proof (cases "?X mod y = 0") |
|
674 case True hence "y dvd ?X" using `0 < y` by auto |
|
675 from real_of_int_div[OF this] |
|
676 have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto |
|
677 also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto |
|
678 finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto |
|
679 thus ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True] |
|
680 unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto |
|
681 next |
|
682 case False |
|
683 have "0 \<le> real y" and "real y \<noteq> 0" using `0 < y` by auto |
|
684 have "0 \<le> real y * 2^?l" by (rule mult_nonneg_nonneg, rule `0 \<le> real y`, auto) |
|
685 |
|
686 have "?X = y * (?X div y) + ?X mod y" by auto |
|
687 also have "\<dots> \<le> y * (?X div y) + y" by (rule add_mono, auto simp add: pos_mod_bound[OF `0 < y`, THEN less_imp_le]) |
|
688 also have "\<dots> = y * (?X div y + 1)" unfolding right_distrib by auto |
|
689 finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] . |
|
690 hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)" |
|
691 by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`) |
|
692 also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto |
|
693 also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`] |
|
694 unfolding divide_inverse .. |
|
695 finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] |
|
696 unfolding pow2_minus pow2_int minus_minus by auto |
|
697 qed |
1015 qed |
698 qed |
1016 qed |
699 |
1017 |
700 lemma rapprox_posrat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y" |
1018 |
701 shows "real (rapprox_posrat n x y) \<le> 1" |
1019 lemma rat_precision_pos: |
702 proof - |
1020 assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n" |
703 let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l" |
1021 shows "rat_precision n (int x) (int y) > 0" |
704 show ?thesis |
1022 proof - |
705 proof (cases "?X mod y = 0") |
1023 { assume "0 < x" hence "log 2 x + 1 = log 2 (2 * x)" by (simp add: log_mult) } |
706 case True hence "y dvd ?X" using `0 < y` by auto |
1024 hence "bitlen (int x) < bitlen (int y)" using assms |
707 from real_of_int_div[OF this] |
1025 by (simp add: bitlen_def del: floor_add_one) |
708 have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto |
1026 (auto intro!: floor_mono simp add: floor_add_one[symmetric] simp del: floor_add floor_add_one) |
709 also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto |
1027 thus ?thesis |
710 finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto |
1028 using assms by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def) |
711 also have "real x / real y \<le> 1" using `0 \<le> x` and `0 < y` and `x \<le> y` by auto |
1029 qed |
712 finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True] |
1030 |
713 unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto |
1031 lemma power_aux: assumes "x > 0" shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1" |
714 next |
1032 proof - |
715 case False |
1033 def y \<equiv> "nat (x - 1)" moreover |
716 have "x \<noteq> y" |
1034 have "(2::int) ^ y \<le> (2 ^ (y + 1)) - 1" by simp |
717 proof (rule ccontr) |
1035 ultimately show ?thesis using assms by simp |
718 assume "\<not> x \<noteq> y" hence "x = y" by auto |
|
719 have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto |
|
720 thus False using False by auto |
|
721 qed |
|
722 hence "x < y" using `x \<le> y` by auto |
|
723 hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto |
|
724 |
|
725 from real_of_int_div4[of "?X" y] |
|
726 have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_numeral . |
|
727 also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto) |
|
728 finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto |
|
729 hence "?X div y + 1 \<le> 2^?l" by auto |
|
730 hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)" |
|
731 unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_numeral |
|
732 by (rule mult_right_mono, auto) |
|
733 hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto |
|
734 thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] |
|
735 unfolding pow2_minus pow2_int minus_minus by auto |
|
736 qed |
|
737 qed |
|
738 |
|
739 lemma zdiv_greater_zero: fixes a b :: int assumes "0 < a" and "a \<le> b" |
|
740 shows "0 < b div a" |
|
741 proof (rule ccontr) |
|
742 have "0 \<le> b" using assms by auto |
|
743 assume "\<not> 0 < b div a" hence "b div a = 0" using `0 \<le> b`[unfolded pos_imp_zdiv_nonneg_iff[OF `0<a`, of b, symmetric]] by auto |
|
744 have "b = a * (b div a) + b mod a" by auto |
|
745 hence "b = b mod a" unfolding `b div a = 0` by auto |
|
746 hence "b < a" using `0 < a`[THEN pos_mod_bound, of b] by auto |
|
747 thus False using `a \<le> b` by auto |
|
748 qed |
1036 qed |
749 |
1037 |
750 lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n" |
1038 lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n" |
751 shows "real (rapprox_posrat n x y) < 1" |
1039 shows "real (rapprox_posrat n x y) < 1" |
752 proof (cases "x = 0") |
1040 proof - |
753 case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat real_of_float_simp by auto |
1041 have powr1: "2 powr real (rat_precision n (int x) (int y)) = |
|
1042 2 ^ nat (rat_precision n (int x) (int y))" using rat_precision_pos[of x y n] assms |
|
1043 by (simp add: powr_realpow[symmetric]) |
|
1044 have "x * 2 powr real (rat_precision n (int x) (int y)) / y = (x / y) * |
|
1045 2 powr real (rat_precision n (int x) (int y))" by simp |
|
1046 also have "... < (1 / 2) * 2 powr real (rat_precision n (int x) (int y))" |
|
1047 apply (rule mult_strict_right_mono) by (insert assms) auto |
|
1048 also have "\<dots> = 2 powr real (rat_precision n (int x) (int y) - 1)" |
|
1049 by (simp add: powr_add diff_def powr_neg_numeral) |
|
1050 also have "\<dots> = 2 ^ nat (rat_precision n (int x) (int y) - 1)" |
|
1051 using rat_precision_pos[of x y n] assms by (simp add: powr_realpow[symmetric]) |
|
1052 also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1" |
|
1053 unfolding int_of_reals real_of_int_le_iff |
|
1054 using rat_precision_pos[OF assms] by (rule power_aux) |
|
1055 finally show ?thesis unfolding rapprox_posrat_def |
|
1056 apply (simp add: round_up_def) |
|
1057 apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide) |
|
1058 unfolding powr1 |
|
1059 unfolding int_of_reals real_of_int_less_iff |
|
1060 unfolding ceiling_less_eq using rat_precision_pos[of x y n] assms apply simp done |
|
1061 qed |
|
1062 |
|
1063 definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" where |
|
1064 "lapprox_rat prec x y = float_of (round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y))" |
|
1065 |
|
1066 lemma compute_lapprox_rat[code]: |
|
1067 "lapprox_rat prec x y = |
|
1068 (if y = 0 then 0 |
|
1069 else if 0 \<le> x then |
|
1070 (if 0 < y then lapprox_posrat prec (nat x) (nat y) |
|
1071 else - (rapprox_posrat prec (nat x) (nat (-y)))) |
|
1072 else (if 0 < y |
|
1073 then - (rapprox_posrat prec (nat (-x)) (nat y)) |
|
1074 else lapprox_posrat prec (nat (-x)) (nat (-y))))" |
|
1075 apply (cases "y = 0") |
|
1076 apply (simp add: lapprox_posrat_def rapprox_posrat_def round_down_def lapprox_rat_def) |
|
1077 apply (auto simp: lapprox_rat_def lapprox_posrat_def rapprox_posrat_def round_up_def round_down_def |
|
1078 ceiling_def real_of_float_uminus[symmetric] ac_simps int_of_reals simp del: real_of_ints) |
|
1079 apply (auto simp: ac_simps) |
|
1080 done |
|
1081 |
|
1082 definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" where |
|
1083 "rapprox_rat prec x y = float_of (round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y))" |
|
1084 |
|
1085 lemma compute_rapprox_rat[code]: |
|
1086 "rapprox_rat prec x y = |
|
1087 (if y = 0 then 0 |
|
1088 else if 0 \<le> x then |
|
1089 (if 0 < y then rapprox_posrat prec (nat x) (nat y) |
|
1090 else - (lapprox_posrat prec (nat x) (nat (-y)))) |
|
1091 else (if 0 < y |
|
1092 then - (lapprox_posrat prec (nat (-x)) (nat y)) |
|
1093 else rapprox_posrat prec (nat (-x)) (nat (-y))))" |
|
1094 apply (cases "y = 0", simp add: lapprox_posrat_def rapprox_posrat_def round_up_def rapprox_rat_def) |
|
1095 apply (auto simp: rapprox_rat_def lapprox_posrat_def rapprox_posrat_def round_up_def round_down_def |
|
1096 ceiling_def real_of_float_uminus[symmetric] ac_simps int_of_reals simp del: real_of_ints) |
|
1097 apply (auto simp: ac_simps) |
|
1098 done |
|
1099 |
|
1100 subsection {* Division *} |
|
1101 |
|
1102 definition div_precision |
|
1103 where "div_precision prec x y = |
|
1104 rat_precision prec \<bar>mantissa x\<bar> \<bar>mantissa y\<bar> - exponent x + exponent y" |
|
1105 |
|
1106 definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" |
|
1107 where "float_divl prec a b = |
|
1108 float_of (round_down (div_precision prec a b) (a / b))" |
|
1109 |
|
1110 lemma compute_float_divl[code]: |
|
1111 fixes m1 s1 m2 s2 |
|
1112 defines "f1 \<equiv> Float m1 s1" and "f2 \<equiv> Float m2 s2" |
|
1113 shows "float_divl prec f1 f2 = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)" |
|
1114 proof cases |
|
1115 assume "f1 \<noteq> 0 \<and> f2 \<noteq> 0" |
|
1116 then have "f1 \<noteq> float_of 0" "f2 \<noteq> float_of 0" by auto |
|
1117 with mantissa_not_dvd[of f1] mantissa_not_dvd[of f2] |
|
1118 have "mantissa f1 \<noteq> 0" "mantissa f2 \<noteq> 0" |
|
1119 by (auto simp add: dvd_def) |
|
1120 then have pos: "0 < \<bar>mantissa f1\<bar>" "0 < \<bar>mantissa f2\<bar>" |
|
1121 by simp_all |
|
1122 moreover from f1_def[THEN denormalize_shift, OF `f1 \<noteq> float_of 0`] guess i . note i = this |
|
1123 moreover from f2_def[THEN denormalize_shift, OF `f2 \<noteq> float_of 0`] guess j . note j = this |
|
1124 moreover have "(real (mantissa f1) * 2 ^ i / (real (mantissa f2) * 2 ^ j)) |
|
1125 = (real (mantissa f1) / real (mantissa f2)) * 2 powr (int i - int j)" |
|
1126 by (simp add: powr_divide2[symmetric] powr_realpow) |
|
1127 moreover have "real f1 / real f2 = real (mantissa f1) / real (mantissa f2) * 2 powr real (exponent f1 - exponent f2)" |
|
1128 unfolding mantissa_exponent by (simp add: powr_divide2[symmetric]) |
|
1129 moreover have "rat_precision prec (\<bar>mantissa f1\<bar> * 2 ^ i) (\<bar>mantissa f2\<bar> * 2 ^ j) = |
|
1130 rat_precision prec \<bar>mantissa f1\<bar> \<bar>mantissa f2\<bar> + j - i" |
|
1131 using pos by (simp add: rat_precision_def) |
|
1132 ultimately show ?thesis |
|
1133 unfolding float_divl_def lapprox_rat_def div_precision_def |
|
1134 by (simp add: abs_mult round_down_shift powr_divide2[symmetric] |
|
1135 del: int_nat_eq real_of_int_diff times_divide_eq_left ) |
|
1136 (simp add: field_simps powr_divide2[symmetric] powr_add) |
754 next |
1137 next |
755 case False hence "0 < x" using `0 \<le> x` by auto |
1138 assume "\<not> (f1 \<noteq> 0 \<and> f2 \<noteq> 0)" then show ?thesis |
756 hence "x < y" using assms by auto |
1139 by (auto simp add: float_divl_def f1_def f2_def lapprox_rat_def) |
757 |
1140 qed |
758 let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l" |
1141 |
759 show ?thesis |
1142 definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" |
760 proof (cases "?X mod y = 0") |
1143 where "float_divr prec a b = |
761 case True hence "y dvd ?X" using `0 < y` by auto |
1144 float_of (round_up (div_precision prec a b) (a / b))" |
762 from real_of_int_div[OF this] |
1145 |
763 have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto |
1146 lemma compute_float_divr[code]: |
764 also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto |
1147 fixes m1 s1 m2 s2 |
765 finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto |
1148 defines "f1 \<equiv> Float m1 s1" and "f2 \<equiv> Float m2 s2" |
766 also have "real x / real y < 1" using `0 \<le> x` and `0 < y` and `x < y` by auto |
1149 shows "float_divr prec f1 f2 = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)" |
767 finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_P[OF True] |
1150 proof cases |
768 unfolding pow2_minus pow2_int minus_minus by auto |
1151 assume "f1 \<noteq> 0 \<and> f2 \<noteq> 0" |
769 next |
1152 then have "f1 \<noteq> float_of 0" "f2 \<noteq> float_of 0" by auto |
770 case False |
1153 with mantissa_not_dvd[of f1] mantissa_not_dvd[of f2] |
771 hence "(real x / real y) < 1 / 2" using `0 < y` and `0 \<le> x` `2 * x < y` by auto |
1154 have "mantissa f1 \<noteq> 0" "mantissa f2 \<noteq> 0" |
772 |
1155 by (auto simp add: dvd_def) |
773 have "0 < ?X div y" |
1156 then have pos: "0 < \<bar>mantissa f1\<bar>" "0 < \<bar>mantissa f2\<bar>" |
774 proof - |
1157 by simp_all |
775 have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)" |
1158 moreover from f1_def[THEN denormalize_shift, OF `f1 \<noteq> float_of 0`] guess i . note i = this |
776 using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto |
1159 moreover from f2_def[THEN denormalize_shift, OF `f2 \<noteq> float_of 0`] guess j . note j = this |
777 hence "(2::int)^nat (bitlen x - 1) < 2^nat (bitlen y)" by (rule order_le_less_trans) |
1160 moreover have "(real (mantissa f1) * 2 ^ i / (real (mantissa f2) * 2 ^ j)) |
778 hence "bitlen x \<le> bitlen y" by auto |
1161 = (real (mantissa f1) / real (mantissa f2)) * 2 powr (int i - int j)" |
779 hence len_less: "nat (bitlen x - 1) \<le> nat (int (n - 1) + bitlen y)" by auto |
1162 by (simp add: powr_divide2[symmetric] powr_realpow) |
780 |
1163 moreover have "real f1 / real f2 = real (mantissa f1) / real (mantissa f2) * 2 powr real (exponent f1 - exponent f2)" |
781 have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto |
1164 unfolding mantissa_exponent by (simp add: powr_divide2[symmetric]) |
782 |
1165 moreover have "rat_precision prec (\<bar>mantissa f1\<bar> * 2 ^ i) (\<bar>mantissa f2\<bar> * 2 ^ j) = |
783 have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l" |
1166 rat_precision prec \<bar>mantissa f1\<bar> \<bar>mantissa f2\<bar> + j - i" |
784 using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto |
1167 using pos by (simp add: rat_precision_def) |
785 |
1168 ultimately show ?thesis |
786 have "y * 2^nat (bitlen x - 1) \<le> y * x" |
1169 unfolding float_divr_def rapprox_rat_def div_precision_def |
787 using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono) |
1170 by (simp add: abs_mult round_up_shift powr_divide2[symmetric] |
788 also have "\<dots> \<le> 2^nat (bitlen y) * x" using bitlen_bounds[OF `0 < y`, THEN conjunct2, THEN less_imp_le] `0 \<le> x` by (rule mult_right_mono) |
1171 del: int_nat_eq real_of_int_diff times_divide_eq_left) |
789 also have "\<dots> \<le> x * 2^nat (int (n - 1) + bitlen y)" unfolding mult_commute[of x] by (rule mult_right_mono, auto simp add: `0 \<le> x`) |
1172 (simp add: field_simps powr_divide2[symmetric] powr_add) |
790 finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))" |
1173 next |
791 unfolding real_of_int_le_iff[symmetric] by auto |
1174 assume "\<not> (f1 \<noteq> 0 \<and> f2 \<noteq> 0)" then show ?thesis |
792 hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" |
1175 by (auto simp add: float_divr_def f1_def f2_def rapprox_rat_def) |
793 unfolding mult_assoc divide_inverse by auto |
1176 qed |
794 also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto |
1177 |
795 finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto |
1178 subsection {* Lemmas needed by Approximate *} |
796 thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto |
1179 |
797 qed |
1180 declare one_float_def[simp del] zero_float_def[simp del] |
798 |
1181 |
799 from real_of_int_div4[of "?X" y] |
1182 lemma Float_num[simp]: shows |
800 have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_numeral . |
1183 "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and |
801 also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto) |
1184 "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and |
802 finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto |
1185 "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n" |
803 hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto |
1186 using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"] two_powr_int_float[of "-3"] |
804 hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)" |
1187 using powr_realpow[of 2 2] powr_realpow[of 2 3] |
805 unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_numeral |
1188 using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3] |
806 by (rule mult_strict_right_mono, auto) |
1189 by auto |
807 hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto |
1190 |
808 thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] |
1191 lemma real_of_Float_int[simp]: "real (Float n 0) = real n" by simp |
809 unfolding pow2_minus pow2_int minus_minus by auto |
1192 |
810 qed |
1193 lemma float_zero[simp]: "real (Float 0 e) = 0" by simp |
811 qed |
1194 |
812 |
1195 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a" |
813 lemma approx_rat_pattern: fixes P and ps :: "nat * int * int" |
1196 by arith |
814 assumes Y: "\<And>y prec x. \<lbrakk>y = 0; ps = (prec, x, 0)\<rbrakk> \<Longrightarrow> P" |
1197 |
815 and A: "\<And>x y prec. \<lbrakk>0 \<le> x; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" |
1198 lemma lapprox_rat: |
816 and B: "\<And>x y prec. \<lbrakk>x < 0; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" |
1199 shows "real (lapprox_rat prec x y) \<le> real x / real y" |
817 and C: "\<And>x y prec. \<lbrakk>x < 0; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" |
1200 using round_down by (simp add: lapprox_rat_def) |
818 and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" |
1201 |
819 shows P |
1202 lemma mult_div_le: fixes a b:: int assumes "b > 0" shows "a \<ge> b * (a div b)" |
820 proof - |
1203 proof - |
821 obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps) auto |
1204 from zmod_zdiv_equality'[of a b] |
822 from Y have "y = 0 \<Longrightarrow> P" by auto |
1205 have "a = b * (a div b) + a mod b" by simp |
823 moreover { |
1206 also have "... \<ge> b * (a div b) + 0" apply (rule add_left_mono) apply (rule pos_mod_sign) |
824 assume "0 < y" |
1207 using assms by simp |
825 have P |
1208 finally show ?thesis by simp |
826 proof (cases "0 \<le> x") |
1209 qed |
827 case True |
1210 |
828 with A and `0 < y` show P by auto |
1211 lemma lapprox_rat_nonneg: |
829 next |
1212 fixes n x y |
830 case False |
1213 defines "p == int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))" |
831 with B and `0 < y` show P by auto |
1214 assumes "0 \<le> x" "0 < y" |
832 qed |
1215 shows "0 \<le> real (lapprox_rat n x y)" |
833 } |
1216 using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric] |
834 moreover { |
1217 powr_int[of 2, simplified] |
835 assume "y < 0" |
1218 by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos mult_pos_pos) |
836 have P |
1219 |
837 proof (cases "0 \<le> x") |
1220 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)" |
838 case True |
1221 using round_up by (simp add: rapprox_rat_def) |
839 with D and `y < 0` show P by auto |
1222 |
840 next |
1223 lemma rapprox_rat_le1: |
841 case False |
1224 fixes n x y |
842 with C and `y < 0` show P by auto |
1225 assumes xy: "0 \<le> x" "0 < y" "x \<le> y" |
843 qed |
1226 shows "real (rapprox_rat n x y) \<le> 1" |
844 } |
1227 proof - |
845 ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0") auto |
1228 have "bitlen \<bar>x\<bar> \<le> bitlen \<bar>y\<bar>" |
846 qed |
1229 using xy unfolding bitlen_def by (auto intro!: floor_mono) |
847 |
1230 then have "0 \<le> rat_precision n \<bar>x\<bar> \<bar>y\<bar>" by (simp add: rat_precision_def) |
848 function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" |
1231 have "real \<lceil>real x / real y * 2 powr real (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)\<rceil> |
849 where |
1232 \<le> real \<lceil>2 powr real (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)\<rceil>" |
850 "y = 0 \<Longrightarrow> lapprox_rat prec x y = 0" |
1233 using xy by (auto intro!: ceiling_mono simp: field_simps) |
851 | "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec x y" |
1234 also have "\<dots> = 2 powr real (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)" |
852 | "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec (-x) y)" |
1235 using `0 \<le> rat_precision n \<bar>x\<bar> \<bar>y\<bar>` |
853 | "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec (-x) (-y)" |
1236 by (auto intro!: exI[of _ "2^nat (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)"] simp: powr_int) |
854 | "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec x (-y))" |
1237 finally show ?thesis |
855 apply simp_all by (rule approx_rat_pattern) |
1238 by (simp add: rapprox_rat_def round_up_def) |
856 termination by lexicographic_order |
1239 (simp add: powr_minus inverse_eq_divide) |
857 |
1240 qed |
858 lemma compute_lapprox_rat[code]: |
1241 |
859 "lapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then lapprox_posrat prec x y else - (rapprox_posrat prec x (-y))) |
1242 lemma rapprox_rat_nonneg_neg: |
860 else (if 0 < y then - (rapprox_posrat prec (-x) y) else lapprox_posrat prec (-x) (-y)))" |
1243 "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0" |
861 by auto |
1244 unfolding rapprox_rat_def round_up_def |
862 |
1245 by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff) |
863 lemma lapprox_rat: "real (lapprox_rat prec x y) \<le> real x / real y" |
1246 |
864 proof - |
1247 lemma rapprox_rat_neg: |
865 have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto |
1248 "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0" |
866 show ?thesis |
1249 unfolding rapprox_rat_def round_up_def |
867 apply (case_tac "y = 0") |
1250 by (auto simp: field_simps mult_le_0_iff) |
|
1251 |
|
1252 lemma rapprox_rat_nonpos_pos: |
|
1253 "x \<le> 0 \<Longrightarrow> 0 < y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0" |
|
1254 unfolding rapprox_rat_def round_up_def |
|
1255 by (auto simp: field_simps mult_le_0_iff) |
|
1256 |
|
1257 lemma float_divl: "real (float_divl prec x y) \<le> real x / real y" |
|
1258 using round_down by (simp add: float_divl_def) |
|
1259 |
|
1260 lemma float_divl_lower_bound: |
|
1261 fixes x y prec |
|
1262 defines "p == rat_precision prec \<bar>mantissa x\<bar> \<bar>mantissa y\<bar> - exponent x + exponent y" |
|
1263 assumes xy: "0 \<le> x" "0 < y" shows "0 \<le> real (float_divl prec x y)" |
|
1264 using xy unfolding float_divl_def p_def[symmetric] round_down_def |
|
1265 by (simp add: zero_le_mult_iff zero_le_divide_iff less_eq_float_def less_float_def) |
|
1266 |
|
1267 lemma exponent_1: "exponent 1 = 0" |
|
1268 using exponent_float[of 1 0] by (simp add: one_float_def) |
|
1269 |
|
1270 lemma mantissa_1: "mantissa 1 = 1" |
|
1271 using mantissa_float[of 1 0] by (simp add: one_float_def) |
|
1272 |
|
1273 lemma bitlen_1: "bitlen 1 = 1" |
|
1274 by (simp add: bitlen_def) |
|
1275 |
|
1276 lemma mantissa_eq_zero_iff: "mantissa x = 0 \<longleftrightarrow> x = 0" |
|
1277 proof |
|
1278 assume "mantissa x = 0" hence z: "0 = real x" using mantissa_exponent by simp |
|
1279 show "x = 0" by (simp add: zero_float_def z) |
|
1280 qed (simp add: zero_float_def) |
|
1281 |
|
1282 lemma float_upper_bound: "x \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x)" |
|
1283 proof (cases "x = 0", simp) |
|
1284 assume "x \<noteq> 0" hence "mantissa x \<noteq> 0" using mantissa_eq_zero_iff by auto |
|
1285 have "x = mantissa x * 2 powr (exponent x)" by (rule mantissa_exponent) |
|
1286 also have "mantissa x \<le> \<bar>mantissa x\<bar>" by simp |
|
1287 also have "... \<le> 2 powr (bitlen \<bar>mantissa x\<bar>)" |
|
1288 using bitlen_bounds[of "\<bar>mantissa x\<bar>"] bitlen_nonneg `mantissa x \<noteq> 0` |
|
1289 by (simp add: powr_int) (simp only: two_real_int int_of_reals real_of_int_abs[symmetric] |
|
1290 real_of_int_le_iff less_imp_le) |
|
1291 finally show ?thesis by (simp add: powr_add) |
|
1292 qed |
|
1293 |
|
1294 lemma float_divl_pos_less1_bound: |
|
1295 assumes "0 < real x" and "real x < 1" and "prec \<ge> 1" |
|
1296 shows "1 \<le> real (float_divl prec 1 x)" |
|
1297 proof cases |
|
1298 assume nonneg: "div_precision prec 1 x \<ge> 0" |
|
1299 hence "2 powr real (div_precision prec 1 x) = |
|
1300 floor (real ((2::int) ^ nat (div_precision prec 1 x))) * floor (1::real)" |
|
1301 by (simp add: powr_int del: real_of_int_power) simp |
|
1302 also have "floor (1::real) \<le> floor (1 / x)" using assms by simp |
|
1303 also have "floor (real ((2::int) ^ nat (div_precision prec 1 x))) * floor (1 / x) \<le> |
|
1304 floor (real ((2::int) ^ nat (div_precision prec 1 x)) * (1 / x))" |
|
1305 by (rule le_mult_floor) (auto simp: assms less_imp_le) |
|
1306 finally have "2 powr real (div_precision prec 1 x) <= |
|
1307 floor (2 powr nat (div_precision prec 1 x) / x)" by (simp add: powr_realpow) |
|
1308 thus ?thesis |
|
1309 using assms nonneg |
|
1310 unfolding float_divl_def round_down_def |
|
1311 by simp (simp add: powr_minus inverse_eq_divide) |
|
1312 next |
|
1313 assume neg: "\<not> 0 \<le> div_precision prec 1 x" |
|
1314 have "1 \<le> 1 * 2 powr (prec - 1)" using assms by (simp add: powr_realpow) |
|
1315 also have "... \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x) / x * 2 powr (prec - 1)" |
|
1316 apply (rule mult_mono) using assms float_upper_bound |
|
1317 by (auto intro!: divide_nonneg_pos) |
|
1318 also have "2 powr (bitlen \<bar>mantissa x\<bar> + exponent x) / x * 2 powr (prec - 1) = |
|
1319 2 powr real (div_precision prec 1 x) / real x" |
|
1320 using assms |
|
1321 apply (simp add: div_precision_def rat_precision_def diff_diff_eq2 |
|
1322 mantissa_1 exponent_1 bitlen_1 powr_add powr_minus real_of_nat_diff) |
|
1323 apply (simp only: diff_def powr_add) |
868 apply simp |
1324 apply simp |
869 apply (case_tac "0 \<le> x \<and> 0 < y") |
|
870 apply (simp add: lapprox_posrat) |
|
871 apply (case_tac "x < 0 \<and> 0 < y") |
|
872 apply simp |
|
873 apply (subst minus_le_iff) |
|
874 apply (rule h[OF rapprox_posrat]) |
|
875 apply (simp_all) |
|
876 apply (case_tac "x < 0 \<and> y < 0") |
|
877 apply simp |
|
878 apply (rule h[OF _ lapprox_posrat]) |
|
879 apply (simp_all) |
|
880 apply (case_tac "0 \<le> x \<and> y < 0") |
|
881 apply (simp) |
|
882 apply (subst minus_le_iff) |
|
883 apply (rule h[OF rapprox_posrat]) |
|
884 apply simp_all |
|
885 apply arith |
|
886 done |
1325 done |
887 qed |
1326 finally have "1 \<le> \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor>" |
888 |
1327 using floor_mono[of "1::real"] by simp thm mult_mono |
889 lemma lapprox_rat_bottom: assumes "0 \<le> x" and "0 < y" |
1328 hence "1 \<le> real \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor>" |
890 shows "real (x div y) \<le> real (lapprox_rat n x y)" |
1329 by (metis floor_real_of_int one_le_floor) |
891 unfolding lapprox_rat.simps(2)[OF assms] using lapprox_posrat_bottom[OF `0<y`] . |
1330 hence "1 * 1 \<le> |
892 |
1331 real \<lfloor>2 powr real (div_precision prec 1 x) / real x\<rfloor> * 2 powr - real (div_precision prec 1 x)" |
893 function rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" |
1332 apply (rule mult_mono) |
894 where |
1333 using assms neg |
895 "y = 0 \<Longrightarrow> rapprox_rat prec x y = 0" |
1334 by (auto intro: divide_nonneg_pos mult_nonneg_nonneg simp: real_of_int_minus[symmetric] powr_int simp del: real_of_int_minus) find_theorems "real (- _)" |
896 | "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec x y" |
1335 thus ?thesis |
897 | "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec (-x) y)" |
1336 using assms neg |
898 | "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec (-x) (-y)" |
1337 unfolding float_divl_def round_down_def |
899 | "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec x (-y))" |
1338 by simp |
900 apply simp_all by (rule approx_rat_pattern) |
1339 qed |
901 termination by lexicographic_order |
|
902 |
|
903 lemma compute_rapprox_rat[code]: |
|
904 "rapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then rapprox_posrat prec x y else - (lapprox_posrat prec x (-y))) else |
|
905 (if 0 < y then - (lapprox_posrat prec (-x) y) else rapprox_posrat prec (-x) (-y)))" |
|
906 by auto |
|
907 |
|
908 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)" |
|
909 proof - |
|
910 have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto |
|
911 show ?thesis |
|
912 apply (case_tac "y = 0") |
|
913 apply simp |
|
914 apply (case_tac "0 \<le> x \<and> 0 < y") |
|
915 apply (simp add: rapprox_posrat) |
|
916 apply (case_tac "x < 0 \<and> 0 < y") |
|
917 apply simp |
|
918 apply (subst le_minus_iff) |
|
919 apply (rule h[OF _ lapprox_posrat]) |
|
920 apply (simp_all) |
|
921 apply (case_tac "x < 0 \<and> y < 0") |
|
922 apply simp |
|
923 apply (rule h[OF rapprox_posrat]) |
|
924 apply (simp_all) |
|
925 apply (case_tac "0 \<le> x \<and> y < 0") |
|
926 apply (simp) |
|
927 apply (subst le_minus_iff) |
|
928 apply (rule h[OF _ lapprox_posrat]) |
|
929 apply simp_all |
|
930 apply arith |
|
931 done |
|
932 qed |
|
933 |
|
934 lemma rapprox_rat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y" |
|
935 shows "real (rapprox_rat n x y) \<le> 1" |
|
936 unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] using rapprox_posrat_le1[OF assms] . |
|
937 |
|
938 lemma rapprox_rat_neg: assumes "x < 0" and "0 < y" |
|
939 shows "real (rapprox_rat n x y) \<le> 0" |
|
940 unfolding rapprox_rat.simps(3)[OF assms] using lapprox_posrat_nonneg[of "-x" y n] assms by auto |
|
941 |
|
942 lemma rapprox_rat_nonneg_neg: assumes "0 \<le> x" and "y < 0" |
|
943 shows "real (rapprox_rat n x y) \<le> 0" |
|
944 unfolding rapprox_rat.simps(5)[OF assms] using lapprox_posrat_nonneg[of x "-y" n] assms by auto |
|
945 |
|
946 lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y" |
|
947 shows "real (rapprox_rat n x y) \<le> 0" |
|
948 proof (cases "x = 0") |
|
949 case True |
|
950 hence "0 \<le> x" by auto show ?thesis |
|
951 unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] |
|
952 unfolding True rapprox_posrat_def Let_def |
|
953 by auto |
|
954 next |
|
955 case False |
|
956 hence "x < 0" using assms by auto |
|
957 show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] . |
|
958 qed |
|
959 |
|
960 fun float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" |
|
961 where |
|
962 "float_divl prec (Float m1 s1) (Float m2 s2) = |
|
963 (let |
|
964 l = lapprox_rat prec m1 m2; |
|
965 f = Float 1 (s1 - s2) |
|
966 in |
|
967 f * l)" |
|
968 |
|
969 lemma float_divl: "real (float_divl prec x y) \<le> real x / real y" |
|
970 using lapprox_rat[of prec "mantissa x" "mantissa y"] |
|
971 by (cases x y rule: float.exhaust[case_product float.exhaust]) |
|
972 (simp split: split_if_asm |
|
973 add: real_of_float_simp pow2_diff field_simps le_divide_eq mult_less_0_iff zero_less_mult_iff) |
|
974 |
|
975 lemma float_divl_lower_bound: assumes "0 \<le> x" and "0 < y" shows "0 \<le> float_divl prec x y" |
|
976 proof (cases x, cases y) |
|
977 fix xm xe ym ye :: int |
|
978 assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" |
|
979 have "0 \<le> xm" |
|
980 using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] |
|
981 by auto |
|
982 have "0 < ym" |
|
983 using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] |
|
984 by auto |
|
985 |
|
986 have "\<And>n. 0 \<le> real (Float 1 n)" |
|
987 unfolding real_of_float_simp using zero_le_pow2 by auto |
|
988 moreover have "0 \<le> real (lapprox_rat prec xm ym)" |
|
989 apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]]) |
|
990 apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`]) |
|
991 done |
|
992 ultimately show "0 \<le> float_divl prec x y" |
|
993 unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 |
|
994 by (auto intro!: mult_nonneg_nonneg) |
|
995 qed |
|
996 |
|
997 lemma float_divl_pos_less1_bound: |
|
998 assumes "0 < x" and "x < 1" and "0 < prec" |
|
999 shows "1 \<le> float_divl prec 1 x" |
|
1000 proof (cases x) |
|
1001 case (Float m e) |
|
1002 from `0 < x` `x < 1` have "0 < m" "e < 0" |
|
1003 using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto |
|
1004 let ?b = "nat (bitlen m)" and ?e = "nat (-e)" |
|
1005 have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto |
|
1006 with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto |
|
1007 hence "1 \<le> bitlen m" using power_le_imp_le_exp[of "2::int" 1 ?b] by auto |
|
1008 hence pow_split: "nat (int prec + bitlen m - 1) = (prec - 1) + ?b" using `0 < prec` by auto |
|
1009 |
|
1010 have pow_not0: "\<And>x. (2::real)^x \<noteq> 0" by auto |
|
1011 |
|
1012 from float_less1_mantissa_bound `0 < x` `x < 1` Float |
|
1013 have "m < 2^?e" by auto |
|
1014 with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m - 1) < 2^?e" |
|
1015 by (rule order_le_less_trans) |
|
1016 from power_less_imp_less_exp[OF _ this] |
|
1017 have "bitlen m \<le> - e" by auto |
|
1018 hence "(2::real)^?b \<le> 2^?e" by auto |
|
1019 hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)" |
|
1020 by (rule mult_right_mono) auto |
|
1021 hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto |
|
1022 also |
|
1023 let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))" |
|
1024 { |
|
1025 have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" |
|
1026 using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto |
|
1027 also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" |
|
1028 unfolding pow_split power_add by auto |
|
1029 finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" |
|
1030 using `0 < m` by (rule zdiv_mono1) |
|
1031 hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" |
|
1032 unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] . |
|
1033 hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d" |
|
1034 unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto |
|
1035 } |
|
1036 from mult_left_mono[OF this [unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"] |
|
1037 have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto |
|
1038 finally have "1 \<le> 2^?e * ?d" . |
|
1039 |
|
1040 have e_nat: "0 - e = int (nat (-e))" using `e < 0` by auto |
|
1041 have "bitlen 1 = 1" using bitlen.simps by auto |
|
1042 |
|
1043 show ?thesis |
|
1044 unfolding one_float_def Float float_divl.simps Let_def |
|
1045 lapprox_rat.simps(2)[OF zero_le_one `0 < m`] |
|
1046 lapprox_posrat_def `bitlen 1 = 1` |
|
1047 unfolding le_float_def real_of_float_mult normfloat real_of_float_simp |
|
1048 pow2_minus pow2_int e_nat |
|
1049 using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def) |
|
1050 qed |
|
1051 |
|
1052 fun float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" |
|
1053 where |
|
1054 "float_divr prec (Float m1 s1) (Float m2 s2) = |
|
1055 (let |
|
1056 r = rapprox_rat prec m1 m2; |
|
1057 f = Float 1 (s1 - s2) |
|
1058 in |
|
1059 f * r)" |
|
1060 |
1340 |
1061 lemma float_divr: "real x / real y \<le> real (float_divr prec x y)" |
1341 lemma float_divr: "real x / real y \<le> real (float_divr prec x y)" |
1062 using rapprox_rat[of "mantissa x" "mantissa y" prec] |
1342 using round_up by (simp add: float_divr_def) |
1063 by (cases x y rule: float.exhaust[case_product float.exhaust]) |
|
1064 (simp split: split_if_asm |
|
1065 add: real_of_float_simp pow2_diff field_simps divide_le_eq mult_less_0_iff zero_less_mult_iff) |
|
1066 |
1343 |
1067 lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x" |
1344 lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x" |
1068 proof - |
1345 proof - |
1069 have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto |
1346 have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto |
1070 also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto |
1347 also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto |
1071 finally show ?thesis unfolding le_float_def by auto |
1348 finally show ?thesis unfolding less_eq_float_def by auto |
1072 qed |
1349 qed |
1073 |
1350 |
1074 lemma float_divr_nonpos_pos_upper_bound: assumes "x \<le> 0" and "0 < y" shows "float_divr prec x y \<le> 0" |
1351 lemma float_divr_nonpos_pos_upper_bound: |
1075 proof (cases x, cases y) |
1352 assumes "real x \<le> 0" and "0 < real y" |
1076 fix xm xe ym ye :: int |
1353 shows "real (float_divr prec x y) \<le> 0" |
1077 assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" |
1354 using assms |
1078 have "xm \<le> 0" using `x \<le> 0`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 mult_le_0_iff] by auto |
1355 unfolding float_divr_def round_up_def |
1079 have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto |
1356 by (auto simp: field_simps mult_le_0_iff divide_le_0_iff) |
1080 |
1357 |
1081 have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto |
1358 lemma float_divr_nonneg_neg_upper_bound: |
1082 moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] . |
1359 assumes "0 \<le> real x" and "real y < 0" |
1083 ultimately show "float_divr prec x y \<le> 0" |
1360 shows "real (float_divr prec x y) \<le> 0" |
1084 unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos) |
1361 using assms |
1085 qed |
1362 unfolding float_divr_def round_up_def |
1086 |
1363 by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff) |
1087 lemma float_divr_nonneg_neg_upper_bound: assumes "0 \<le> x" and "y < 0" shows "float_divr prec x y \<le> 0" |
1364 |
1088 proof (cases x, cases y) |
1365 definition "round_prec p f = int p - (bitlen \<bar>mantissa f\<bar> + exponent f)" |
1089 fix xm xe ym ye :: int |
1366 |
1090 assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" |
1367 definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where |
1091 have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto |
1368 "float_round_down prec f = float_of (round_down (round_prec prec f) f)" |
1092 have "ym < 0" using `y < 0`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 mult_less_0_iff] by auto |
1369 |
1093 hence "0 < - ym" by auto |
1370 definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where |
1094 |
1371 "float_round_up prec f = float_of (round_up (round_prec prec f) f)" |
1095 have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto |
1372 |
1096 moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] . |
1373 lemma compute_float_round_down[code]: |
1097 ultimately show "float_divr prec x y \<le> 0" |
1374 fixes prec m e |
1098 unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos) |
1375 defines "d == bitlen (abs m) - int prec" |
1099 qed |
1376 defines "P == 2^nat d" |
1100 |
1377 defines "f == Float m e" |
1101 primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where |
1378 shows "float_round_down prec f = (let d = d in |
1102 "round_down prec (Float m e) = (let d = bitlen m - int prec in |
1379 if 0 < d then let P = P ; n = m div P in Float n (e + d) |
1103 if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d) |
1380 else f)" |
1104 else Float m e)" |
1381 unfolding float_round_down_def float_down_def[symmetric] |
1105 |
1382 compute_float_down f_def Let_def P_def round_prec_def d_def bitlen_Float |
1106 primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where |
1383 by (simp add: field_simps) |
1107 "round_up prec (Float m e) = (let d = bitlen m - int prec in |
1384 |
1108 if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d) |
1385 lemma compute_float_round_up[code]: |
1109 else Float m e)" |
1386 fixes prec m e |
1110 |
1387 defines "d == bitlen (abs m) - int prec" |
1111 lemma round_up: "real x \<le> real (round_up prec x)" |
1388 defines "P == 2^nat d" |
1112 proof (cases x) |
1389 defines "f == Float m e" |
1113 case (Float m e) |
1390 shows "float_round_up prec f = (let d = d in |
1114 let ?d = "bitlen m - int prec" |
1391 if 0 < d then let P = P ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d) |
1115 let ?p = "(2::int)^nat ?d" |
1392 else f)" |
1116 have "0 < ?p" by auto |
1393 unfolding float_round_up_def float_up_def[symmetric] |
1117 show "?thesis" |
1394 compute_float_up f_def Let_def P_def round_prec_def d_def bitlen_Float |
1118 proof (cases "0 < ?d") |
1395 by (simp add: field_simps) |
1119 case True |
1396 |
1120 hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp |
1397 lemma float_round_up: "real x \<le> real (float_round_up prec x)" |
1121 show ?thesis |
1398 using round_up |
1122 proof (cases "m mod ?p = 0") |
1399 by (simp add: float_round_up_def) |
1123 case True |
1400 |
1124 have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using mod_div_equality [symmetric] . |
1401 lemma float_round_down: "real (float_round_down prec x) \<le> real x" |
1125 have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real] |
1402 using round_down |
1126 by (auto simp add: pow2_add `0 < ?d` pow_d) |
1403 by (simp add: float_round_down_def) |
1127 thus ?thesis |
1404 |
1128 unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`] |
1405 instantiation float :: lattice_ab_group_add |
1129 by auto |
|
1130 next |
|
1131 case False |
|
1132 have "m = m div ?p * ?p + m mod ?p" unfolding mod_div_equality .. |
|
1133 also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) |
|
1134 finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e] |
|
1135 unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric] |
|
1136 by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) |
|
1137 thus ?thesis |
|
1138 unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] . |
|
1139 qed |
|
1140 next |
|
1141 case False |
|
1142 show ?thesis |
|
1143 unfolding Float round_up.simps Let_def if_not_P[OF False] .. |
|
1144 qed |
|
1145 qed |
|
1146 |
|
1147 lemma round_down: "real (round_down prec x) \<le> real x" |
|
1148 proof (cases x) |
|
1149 case (Float m e) |
|
1150 let ?d = "bitlen m - int prec" |
|
1151 let ?p = "(2::int)^nat ?d" |
|
1152 have "0 < ?p" by auto |
|
1153 show "?thesis" |
|
1154 proof (cases "0 < ?d") |
|
1155 case True |
|
1156 hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp |
|
1157 have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) |
|
1158 also have "\<dots> \<le> m" unfolding mod_div_equality .. |
|
1159 finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e] |
|
1160 unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric] |
|
1161 by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) |
|
1162 thus ?thesis |
|
1163 unfolding Float round_down.simps Let_def if_P[OF `0 < ?d`] . |
|
1164 next |
|
1165 case False |
|
1166 show ?thesis |
|
1167 unfolding Float round_down.simps Let_def if_not_P[OF False] .. |
|
1168 qed |
|
1169 qed |
|
1170 |
|
1171 definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
|
1172 "lb_mult prec x y = |
|
1173 (case normfloat (x * y) of Float m e \<Rightarrow> |
|
1174 let |
|
1175 l = bitlen m - int prec |
|
1176 in if l > 0 then Float (m div (2^nat l)) (e + l) |
|
1177 else Float m e)" |
|
1178 |
|
1179 definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
|
1180 "ub_mult prec x y = |
|
1181 (case normfloat (x * y) of Float m e \<Rightarrow> |
|
1182 let |
|
1183 l = bitlen m - int prec |
|
1184 in if l > 0 then Float (m div (2^nat l) + 1) (e + l) |
|
1185 else Float m e)" |
|
1186 |
|
1187 lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)" |
|
1188 proof (cases "normfloat (x * y)") |
|
1189 case (Float m e) |
|
1190 hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero) |
|
1191 let ?l = "bitlen m - int prec" |
|
1192 have "real (lb_mult prec x y) \<le> real (normfloat (x * y))" |
|
1193 proof (cases "?l > 0") |
|
1194 case False thus ?thesis unfolding lb_mult_def Float Let_def float.cases by auto |
|
1195 next |
|
1196 case True |
|
1197 have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m" |
|
1198 proof - |
|
1199 have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_numeral unfolding pow2_int[symmetric] |
|
1200 using `?l > 0` by auto |
|
1201 also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto |
|
1202 also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] .. |
|
1203 finally show ?thesis by auto |
|
1204 qed |
|
1205 thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto |
|
1206 qed |
|
1207 also have "\<dots> = real (x * y)" unfolding normfloat .. |
|
1208 finally show ?thesis . |
|
1209 qed |
|
1210 |
|
1211 lemma ub_mult: "real (x * y) \<le> real (ub_mult prec x y)" |
|
1212 proof (cases "normfloat (x * y)") |
|
1213 case (Float m e) |
|
1214 hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero) |
|
1215 let ?l = "bitlen m - int prec" |
|
1216 have "real (x * y) = real (normfloat (x * y))" unfolding normfloat .. |
|
1217 also have "\<dots> \<le> real (ub_mult prec x y)" |
|
1218 proof (cases "?l > 0") |
|
1219 case False thus ?thesis unfolding ub_mult_def Float Let_def float.cases by auto |
|
1220 next |
|
1221 case True |
|
1222 have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l" |
|
1223 proof - |
|
1224 have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto |
|
1225 hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding mult_1 real_of_int_less_iff[symmetric] by auto |
|
1226 |
|
1227 have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] .. |
|
1228 also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto |
|
1229 also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding left_distrib using mod_uneq by auto |
|
1230 finally show ?thesis unfolding pow2_int[symmetric] using True by auto |
|
1231 qed |
|
1232 thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto |
|
1233 qed |
|
1234 finally show ?thesis . |
|
1235 qed |
|
1236 |
|
1237 primrec float_abs :: "float \<Rightarrow> float" where |
|
1238 "float_abs (Float m e) = Float \<bar>m\<bar> e" |
|
1239 |
|
1240 instantiation float :: abs |
|
1241 begin |
1406 begin |
1242 definition abs_float_def: "\<bar>x\<bar> = float_abs x" |
1407 |
1243 instance .. |
1408 definition inf_float::"float\<Rightarrow>float\<Rightarrow>float" |
|
1409 where "inf_float a b = min a b" |
|
1410 |
|
1411 definition sup_float::"float\<Rightarrow>float\<Rightarrow>float" |
|
1412 where "sup_float a b = max a b" |
|
1413 |
|
1414 instance |
|
1415 proof |
|
1416 fix x y :: float show "inf x y \<le> x" unfolding inf_float_def by simp |
|
1417 show "inf x y \<le> y" unfolding inf_float_def by simp |
|
1418 show "x \<le> sup x y" unfolding sup_float_def by simp |
|
1419 show "y \<le> sup x y" unfolding sup_float_def by simp |
|
1420 fix z::float |
|
1421 assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z" unfolding inf_float_def by simp |
|
1422 next fix x y z :: float |
|
1423 assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x" unfolding sup_float_def by simp |
|
1424 qed |
|
1425 |
1244 end |
1426 end |
1245 |
1427 |
1246 lemma real_of_float_abs: "real \<bar>x :: float\<bar> = \<bar>real x\<bar>" |
1428 lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0" |
1247 proof (cases x) |
1429 apply (auto simp: zero_float_def mult_le_0_iff) |
1248 case (Float m e) |
1430 using powr_gt_zero[of 2 b] by simp |
1249 have "\<bar>real m\<bar> * pow2 e = \<bar>real m * pow2 e\<bar>" unfolding abs_mult by auto |
1431 |
1250 thus ?thesis unfolding Float abs_float_def float_abs.simps real_of_float_simp by auto |
1432 (* TODO: how to use as code equation? -> pprt_float?! *) |
1251 qed |
1433 lemma compute_pprt[code]: "pprt (Float a e) = (if a <= 0 then 0 else (Float a e))" |
1252 |
1434 unfolding pprt_def sup_float_def max_def Float_le_zero_iff .. |
1253 primrec floor_fl :: "float \<Rightarrow> float" where |
1435 |
1254 "floor_fl (Float m e) = (if 0 \<le> e then Float m e |
1436 (* TODO: how to use as code equation? *) |
|
1437 lemma compute_nprt[code]: "nprt (Float a e) = (if a <= 0 then (Float a e) else 0)" |
|
1438 unfolding nprt_def inf_float_def min_def Float_le_zero_iff .. |
|
1439 |
|
1440 lemma of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)" |
|
1441 unfolding pprt_def sup_float_def max_def sup_real_def by (auto simp: less_eq_float_def) |
|
1442 |
|
1443 lemma of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)" |
|
1444 unfolding nprt_def inf_float_def min_def inf_real_def by (auto simp: less_eq_float_def) |
|
1445 |
|
1446 definition int_floor_fl :: "float \<Rightarrow> int" where |
|
1447 "int_floor_fl f = floor f" |
|
1448 |
|
1449 lemma compute_int_floor_fl[code]: |
|
1450 shows "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e |
|
1451 else m div (2 ^ (nat (-e))))" |
|
1452 by (simp add: int_floor_fl_def powr_int int_of_reals floor_divide_eq_div del: real_of_ints) |
|
1453 |
|
1454 definition floor_fl :: "float \<Rightarrow> float" where |
|
1455 "floor_fl f = float_of (floor f)" |
|
1456 |
|
1457 lemma compute_floor_fl[code]: |
|
1458 shows "floor_fl (Float m e) = (if 0 \<le> e then Float m e |
1255 else Float (m div (2 ^ (nat (-e)))) 0)" |
1459 else Float (m div (2 ^ (nat (-e)))) 0)" |
1256 |
1460 by (simp add: floor_fl_def powr_int int_of_reals floor_divide_eq_div del: real_of_ints) |
1257 lemma floor_fl: "real (floor_fl x) \<le> real x" |
1461 |
1258 proof (cases x) |
1462 lemma floor_fl: "real (floor_fl x) \<le> real x" by (simp add: floor_fl_def) |
1259 case (Float m e) |
1463 lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by (simp add: int_floor_fl_def) |
1260 show ?thesis |
1464 |
1261 proof (cases "0 \<le> e") |
1465 lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0" |
1262 case False |
1466 proof cases |
1263 hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto |
1467 assume nzero: "floor_fl x \<noteq> float_of 0" |
1264 have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto |
1468 have "floor_fl x \<equiv> Float \<lfloor>real x\<rfloor> 0" by (simp add: floor_fl_def) |
1265 also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 . |
1469 from denormalize_shift[OF this nzero] guess i . note i = this |
1266 also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_numeral divide_inverse .. |
1470 thus ?thesis by simp |
1267 also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] .. |
1471 qed (simp add: floor_fl_def) |
1268 finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] . |
1472 |
1269 next |
1473 (* TODO: not used in approximation |
1270 case True thus ?thesis unfolding Float by auto |
1474 definition ceiling_fl :: "float_of \<Rightarrow> float" where |
1271 qed |
1475 "ceiling_fl f = float_of (ceiling f)" |
1272 qed |
1476 |
1273 |
1477 lemma compute_ceiling_fl: |
1274 lemma floor_pos_exp: assumes floor: "Float m e = floor_fl x" shows "0 \<le> e" |
|
1275 proof (cases x) |
|
1276 case (Float mx me) |
|
1277 from floor[unfolded Float floor_fl.simps] show ?thesis by (cases "0 \<le> me", auto) |
|
1278 qed |
|
1279 |
|
1280 declare floor_fl.simps[simp del] |
|
1281 |
|
1282 primrec ceiling_fl :: "float \<Rightarrow> float" where |
|
1283 "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e |
1478 "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e |
1284 else Float (m div (2 ^ (nat (-e))) + 1) 0)" |
1479 else Float (m div (2 ^ (nat (-e))) + 1) 0)" |
1285 |
1480 |
1286 lemma ceiling_fl: "real x \<le> real (ceiling_fl x)" |
1481 lemma ceiling_fl: "real x \<le> real (ceiling_fl x)" |
1287 proof (cases x) |
1482 |
1288 case (Float m e) |
1483 definition lb_mod :: "nat \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float" where |
1289 show ?thesis |
1484 "lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub" |
1290 proof (cases "0 \<le> e") |
1485 |
1291 case False |
1486 definition ub_mod :: "nat \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float_of \<Rightarrow> float" where |
1292 hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto |
1487 "ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb" |
1293 have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] .. |
|
1294 also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_numeral divide_inverse .. |
|
1295 also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] . |
|
1296 also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto |
|
1297 finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] . |
|
1298 next |
|
1299 case True thus ?thesis unfolding Float by auto |
|
1300 qed |
|
1301 qed |
|
1302 |
|
1303 declare ceiling_fl.simps[simp del] |
|
1304 |
|
1305 definition lb_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
|
1306 "lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub" |
|
1307 |
|
1308 definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
|
1309 "ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb" |
|
1310 |
1488 |
1311 lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x") |
1489 lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x") |
1312 assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub") |
1490 assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub") |
1313 shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y" |
1491 shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y" |
1314 proof - |
1492 |
1315 have "?lb \<le> ?ub" using assms by auto |
1493 lemma ub_mod: fixes k :: int and x :: float_of assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y") |
1316 have "0 \<le> ?lb" and "?lb \<noteq> 0" using assms by auto |
|
1317 have "?k * y \<le> ?x" using assms by auto |
|
1318 also have "\<dots> \<le> ?x / ?lb * ?ub" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?lb` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?lb \<noteq> 0`]) |
|
1319 also have "\<dots> \<le> real (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl) |
|
1320 finally show ?thesis unfolding lb_mod_def real_of_float_sub real_of_float_mult by auto |
|
1321 qed |
|
1322 |
|
1323 lemma ub_mod: |
|
1324 fixes k :: int and x :: float |
|
1325 assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y") |
|
1326 assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub") |
1494 assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub") |
1327 shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)" |
1495 shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)" |
1328 proof - |
1496 |
1329 have "?lb \<le> ?ub" using assms by auto |
1497 *) |
1330 hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" using assms by auto |
|
1331 have "real (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl) |
|
1332 also have "\<dots> \<le> ?x" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?ub` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?ub \<noteq> 0`]) |
|
1333 also have "\<dots> \<le> ?k * y" using assms by auto |
|
1334 finally show ?thesis unfolding ub_mod_def real_of_float_sub real_of_float_mult by auto |
|
1335 qed |
|
1336 |
|
1337 lemma le_float_def'[code]: "f \<le> g = (case f - g of Float a b \<Rightarrow> a \<le> 0)" |
|
1338 proof - |
|
1339 have le_transfer: "(f \<le> g) = (real (f - g) \<le> 0)" by (auto simp add: le_float_def) |
|
1340 from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto |
|
1341 with le_transfer have le_transfer': "f \<le> g = (real (Float a b) \<le> 0)" by simp |
|
1342 show ?thesis by (simp add: le_transfer' f_diff_g float_le_zero) |
|
1343 qed |
|
1344 |
|
1345 lemma less_float_def'[code]: "f < g = (case f - g of Float a b \<Rightarrow> a < 0)" |
|
1346 proof - |
|
1347 have less_transfer: "(f < g) = (real (f - g) < 0)" by (auto simp add: less_float_def) |
|
1348 from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto |
|
1349 with less_transfer have less_transfer': "f < g = (real (Float a b) < 0)" by simp |
|
1350 show ?thesis by (simp add: less_transfer' f_diff_g float_less_zero) |
|
1351 qed |
|
1352 |
1498 |
1353 end |
1499 end |
|
1500 |