src/HOL/Real/Float.thy
 author nipkow Tue Oct 23 23:27:23 2007 +0200 (2007-10-23) changeset 25162 ad4d5365d9d8 parent 24653 3d3ebc0c927c child 26076 b9c716a9fb5f permissions -rw-r--r--
went back to >0
1 (*  Title: HOL/Real/Float.thy
2     ID:    \$Id\$
3     Author: Steven Obua
4 *)
6 header {* Floating Point Representation of the Reals *}
8 theory Float
9 imports Real Parity
10 uses "~~/src/Tools/float.ML" ("float_arith.ML")
11 begin
13 definition
14   pow2 :: "int \<Rightarrow> real" where
15   "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
17 definition
18   float :: "int * int \<Rightarrow> real" where
19   "float x = real (fst x) * pow2 (snd x)"
21 lemma pow2_0[simp]: "pow2 0 = 1"
24 lemma pow2_1[simp]: "pow2 1 = 2"
27 lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
30 lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
31 proof -
32   have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
33   have g: "! a b. a - -1 = a + (1::int)" by arith
34   have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
35     apply (auto, induct_tac n)
37     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
38     by (auto simp add: h)
39   show ?thesis
40   proof (induct a)
41     case (1 n)
42     from pos show ?case by (simp add: ring_simps)
43   next
44     case (2 n)
45     show ?case
46       apply (auto)
47       apply (subst pow2_neg[of "- int n"])
48       apply (subst pow2_neg[of "-1 - int n"])
49       apply (auto simp add: g pos)
50       done
51   qed
52 qed
54 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
55 proof (induct b)
56   case (1 n)
57   show ?case
58   proof (induct n)
59     case 0
60     show ?case by simp
61   next
62     case (Suc m)
64   qed
65 next
66   case (2 n)
67   show ?case
68   proof (induct n)
69     case 0
70     show ?case
71       apply (auto)
72       apply (subst pow2_neg[of "a + -1"])
73       apply (subst pow2_neg[of "-1"])
74       apply (simp)
77       apply (subst pow2_neg[of "-a"])
78       apply (simp)
79       done
80     case (Suc m)
81     have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
82     have b: "int m - -2 = 1 + (int m + 1)" by arith
83     show ?case
84       apply (auto)
85       apply (subst pow2_neg[of "a + (-2 - int m)"])
86       apply (subst pow2_neg[of "-2 - int m"])
87       apply (auto simp add: ring_simps)
88       apply (subst a)
89       apply (subst b)
91       apply (subst pow2_neg[of "int m - a + 1"])
92       apply (subst pow2_neg[of "int m + 1"])
93       apply auto
94       apply (insert prems)
95       apply (auto simp add: ring_simps)
96       done
97   qed
98 qed
100 lemma "float (a, e) + float (b, e) = float (a + b, e)"
101 by (simp add: float_def ring_simps)
103 definition
104   int_of_real :: "real \<Rightarrow> int" where
105   "int_of_real x = (SOME y. real y = x)"
107 definition
108   real_is_int :: "real \<Rightarrow> bool" where
109   "real_is_int x = (EX (u::int). x = real u)"
111 lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
112 by (auto simp add: real_is_int_def int_of_real_def)
114 lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \<Longrightarrow> float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)"
117 lemma pow2_int: "pow2 (int c) = (2::real)^c"
120 lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
123 lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
124 by (auto simp add: real_is_int_def int_of_real_def)
126 lemma int_of_real_real[simp]: "int_of_real (real x) = x"
129 lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real (int_of_real x) = x"
130 by (auto simp add: int_of_real_def real_is_int_def)
132 lemma real_is_int_add_int_of_real: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)"
133 by (auto simp add: int_of_real_def real_is_int_def)
135 lemma real_is_int_add[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a+b)"
136 apply (subst real_is_int_def2)
138 done
140 lemma int_of_real_sub: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)"
141 by (auto simp add: int_of_real_def real_is_int_def)
143 lemma real_is_int_sub[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a-b)"
144 apply (subst real_is_int_def2)
145 apply (simp add: int_of_real_sub real_int_of_real)
146 done
148 lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
149 by (auto simp add: real_is_int_def)
151 lemma int_of_real_mult:
152   assumes "real_is_int a" "real_is_int b"
153   shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
154 proof -
155   from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
156   from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
157   from a obtain a'::int where a':"a = real a'" by auto
158   from b obtain b'::int where b':"b = real b'" by auto
159   have r: "real a' * real b' = real (a' * b')" by auto
160   show ?thesis
161     apply (simp add: a' b')
162     apply (subst r)
163     apply (simp only: int_of_real_real)
164     done
165 qed
167 lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)"
168 apply (subst real_is_int_def2)
170 done
172 lemma real_is_int_0[simp]: "real_is_int (0::real)"
173 by (simp add: real_is_int_def int_of_real_def)
175 lemma real_is_int_1[simp]: "real_is_int (1::real)"
176 proof -
177   have "real_is_int (1::real) = real_is_int(real (1::int))" by auto
178   also have "\<dots> = True" by (simp only: real_is_int_real)
179   ultimately show ?thesis by auto
180 qed
182 lemma real_is_int_n1: "real_is_int (-1::real)"
183 proof -
184   have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
185   also have "\<dots> = True" by (simp only: real_is_int_real)
186   ultimately show ?thesis by auto
187 qed
189 lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
190 proof -
191   have neg1: "real_is_int (-1::real)"
192   proof -
193     have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
194     also have "\<dots> = True" by (simp only: real_is_int_real)
195     ultimately show ?thesis by auto
196   qed
198   {
199     fix x :: int
200     have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
201       unfolding number_of_eq
202       apply (induct x)
203       apply (induct_tac n)
204       apply (simp)
205       apply (simp)
206       apply (induct_tac n)
208     proof -
209       fix n :: nat
210       assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
211       have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
212       show "real_is_int (of_int (- (int (Suc (Suc n)))))"
213         apply (simp only: s of_int_add)
216         apply (simp only: rn)
217         done
218     qed
219   }
220   note Abs_Bin = this
221   {
222     fix x :: int
223     have "? u. x = u"
224       apply (rule exI[where x = "x"])
225       apply (simp)
226       done
227   }
228   then obtain u::int where "x = u" by auto
229   with Abs_Bin show ?thesis by auto
230 qed
232 lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
235 lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
236 proof -
237   have 1: "(1::real) = real (1::int)" by auto
238   show ?thesis by (simp only: 1 int_of_real_real)
239 qed
241 lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b"
242 proof -
243   have "real_is_int (number_of b)" by simp
244   then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
245   then obtain u::int where u:"number_of b = real u" by auto
246   have "number_of b = real ((number_of b)::int)"
247     by (simp add: number_of_eq real_of_int_def)
248   have ub: "number_of b = real ((number_of b)::int)"
249     by (simp add: number_of_eq real_of_int_def)
250   from uu u ub have unb: "u = number_of b"
251     by blast
252   have "int_of_real (number_of b) = u" by (simp add: u)
253   with unb show ?thesis by simp
254 qed
256 lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
257   apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
258   apply (simp_all add: pow2_def even_def real_is_int_def ring_simps)
259   apply (auto)
260 proof -
261   fix q::int
262   have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
263   show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
265 qed
267 consts
268   norm_float :: "int*int \<Rightarrow> int*int"
270 lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
271 by (rule zdiv_int)
273 lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
274 by (rule zmod_int)
276 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
277 by arith
279 lemma terminating_norm_float: "\<forall>a. (a::int) \<noteq> 0 \<and> even a \<longrightarrow> a \<noteq> 0 \<and> \<bar>a div 2\<bar> < \<bar>a\<bar>"
280 apply (auto)
281 apply (rule abs_div_2_less)
282 apply (auto)
283 done
285 declare [[simp_depth_limit = 2]]
286 recdef norm_float "measure (% (a,b). nat (abs a))"
287   "norm_float (a,b) = (if (a \<noteq> 0) & (even a) then norm_float (a div 2, b+1) else (if a=0 then (0,0) else (a,b)))"
288 (hints simp: even_def terminating_norm_float)
289 declare [[simp_depth_limit = 100]]
291 lemma norm_float: "float x = float (norm_float x)"
292 proof -
293   {
294     fix a b :: int
295     have norm_float_pair: "float (a,b) = float (norm_float (a,b))"
296     proof (induct a b rule: norm_float.induct)
297       case (1 u v)
298       show ?case
299       proof cases
300         assume u: "u \<noteq> 0 \<and> even u"
301         with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2, v + 1))" by auto
302         with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
303         then show ?thesis
304           apply (subst norm_float.simps)
306           done
307       next
308         assume "~(u \<noteq> 0 \<and> even u)"
309         then show ?thesis
310           by (simp add: prems float_def)
311       qed
312     qed
313   }
314   note helper = this
315   have "? a b. x = (a,b)" by auto
316   then obtain a b where "x = (a, b)" by blast
317   then show ?thesis by (simp only: helper)
318 qed
320 lemma pow2_int: "pow2 (int n) = 2^n"
323 lemma float_add_l0: "float (0, e) + x = x"
326 lemma float_add_r0: "x + float (0, e) = x"
330   "float (a1, e1) + float (a2, e2) =
331   (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
332   else float (a1*2^(nat (e1-e2))+a2, e2))"
333   apply (simp add: float_def ring_simps)
335   done
338   "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
339   by simp
342   "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
343   by simp
346   "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x"
347   by simp
350   "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x"
351   by simp
353 lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
356 lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
359 definition
360   lbound :: "real \<Rightarrow> real"
361 where
362   "lbound x = min 0 x"
364 definition
365   ubound :: "real \<Rightarrow> real"
366 where
367   "ubound x = max 0 x"
369 lemma lbound: "lbound x \<le> x"
372 lemma ubound: "x \<le> ubound x"
375 lemma float_mult:
376   "float (a1, e1) * float (a2, e2) =
377   (float (a1 * a2, e1 + e2))"
380 lemma float_minus:
381   "- (float (a,b)) = float (-a, b)"
384 lemma zero_less_pow2:
385   "0 < pow2 x"
386 proof -
387   {
388     fix y
389     have "0 <= y \<Longrightarrow> 0 < pow2 y"
391   }
392   note helper=this
393   show ?thesis
394     apply (case_tac "0 <= x")
396     apply (subst pow2_neg)
398     done
399 qed
401 lemma zero_le_float:
402   "(0 <= float (a,b)) = (0 <= a)"
403   apply (auto simp add: float_def)
404   apply (auto simp add: zero_le_mult_iff zero_less_pow2)
405   apply (insert zero_less_pow2[of b])
406   apply (simp_all)
407   done
409 lemma float_le_zero:
410   "(float (a,b) <= 0) = (a <= 0)"
411   apply (auto simp add: float_def)
412   apply (auto simp add: mult_le_0_iff)
413   apply (insert zero_less_pow2[of b])
414   apply auto
415   done
417 lemma float_abs:
418   "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
419   apply (auto simp add: abs_if)
420   apply (simp_all add: zero_le_float[symmetric, of a b] float_minus)
421   done
423 lemma float_zero:
424   "float (0, b) = 0"
427 lemma float_pprt:
428   "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
429   by (auto simp add: zero_le_float float_le_zero float_zero)
431 lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
433   apply (rule pprt_eq_0)
435   done
437 lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
439   apply (rule nprt_eq_0)
441   done
443 lemma float_nprt:
444   "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
445   by (auto simp add: zero_le_float float_le_zero float_zero)
447 lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
448   by auto
451   by simp
454   by simp
456 lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
457   by simp
459 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
460   by simp
462 lemma int_pow_0: "(a::int)^(Numeral0) = 1"
463   by simp
465 lemma int_pow_1: "(a::int)^(Numeral1) = a"
466   by simp
468 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
469   by simp
471 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
472   by simp
474 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
475   by simp
477 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
478   by simp
480 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
481   by simp
483 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
484 proof -
485   have 1:"((-1)::nat) = 0"
486     by simp
487   show ?thesis by (simp add: 1)
488 qed
490 lemma fst_cong: "a=a' \<Longrightarrow> fst (a,b) = fst (a',b)"
491   by simp
493 lemma snd_cong: "b=b' \<Longrightarrow> snd (a,b) = snd (a,b')"
494   by simp
496 lemma lift_bool: "x \<Longrightarrow> x=True"
497   by simp
499 lemma nlift_bool: "~x \<Longrightarrow> x=False"
500   by simp
502 lemma not_false_eq_true: "(~ False) = True" by simp
504 lemma not_true_eq_false: "(~ True) = False" by simp
506 lemmas binarith =
507   Pls_0_eq Min_1_eq
508   pred_Pls pred_Min pred_1 pred_0
509   succ_Pls succ_Min succ_1 succ_0
512   minus_0 mult_Pls mult_Min mult_num1 mult_num0
515 lemma int_eq_number_of_eq:
516   "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
517   by simp
519 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
520   by (simp only: iszero_number_of_Pls)
522 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
523   by simp
525 lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
526   by simp
528 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
529   by simp
531 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
532   by simp
534 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
535   by simp
537 lemma int_neg_number_of_Min: "neg (-1::int)"
538   by simp
540 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
541   by simp
543 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
544   by simp
546 lemmas intarithrel =
547   int_eq_number_of_eq
548   lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
549   lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
550   int_neg_number_of_BIT int_le_number_of_eq
552 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
553   by simp
555 lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
556   by simp
558 lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
559   by simp
561 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
562   by simp
564 lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
566 lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
568 lemmas powerarith = nat_number_of zpower_number_of_even
569   zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
570   zpower_Pls zpower_Min