|
1 (* Title: HOL/Matrix/ComputeFloat.thy |
|
2 Author: Steven Obua |
|
3 *) |
|
4 |
|
5 header {* Floating Point Representation of the Reals *} |
|
6 |
|
7 theory ComputeFloat |
|
8 imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras" |
|
9 uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML") |
|
10 begin |
|
11 |
|
12 definition int_of_real :: "real \<Rightarrow> int" |
|
13 where "int_of_real x = (SOME y. real y = x)" |
|
14 |
|
15 definition real_is_int :: "real \<Rightarrow> bool" |
|
16 where "real_is_int x = (EX (u::int). x = real u)" |
|
17 |
|
18 lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))" |
|
19 by (auto simp add: real_is_int_def int_of_real_def) |
|
20 |
|
21 lemma real_is_int_real[simp]: "real_is_int (real (x::int))" |
|
22 by (auto simp add: real_is_int_def int_of_real_def) |
|
23 |
|
24 lemma int_of_real_real[simp]: "int_of_real (real x) = x" |
|
25 by (simp add: int_of_real_def) |
|
26 |
|
27 lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real (int_of_real x) = x" |
|
28 by (auto simp add: int_of_real_def real_is_int_def) |
|
29 |
|
30 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)" |
|
31 by (auto simp add: int_of_real_def real_is_int_def) |
|
32 |
|
33 lemma real_is_int_add[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a+b)" |
|
34 apply (subst real_is_int_def2) |
|
35 apply (simp add: real_is_int_add_int_of_real real_int_of_real) |
|
36 done |
|
37 |
|
38 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)" |
|
39 by (auto simp add: int_of_real_def real_is_int_def) |
|
40 |
|
41 lemma real_is_int_sub[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a-b)" |
|
42 apply (subst real_is_int_def2) |
|
43 apply (simp add: int_of_real_sub real_int_of_real) |
|
44 done |
|
45 |
|
46 lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x" |
|
47 by (auto simp add: real_is_int_def) |
|
48 |
|
49 lemma int_of_real_mult: |
|
50 assumes "real_is_int a" "real_is_int b" |
|
51 shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)" |
|
52 using assms |
|
53 by (auto simp add: real_is_int_def real_of_int_mult[symmetric] |
|
54 simp del: real_of_int_mult) |
|
55 |
|
56 lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)" |
|
57 apply (subst real_is_int_def2) |
|
58 apply (simp add: int_of_real_mult) |
|
59 done |
|
60 |
|
61 lemma real_is_int_0[simp]: "real_is_int (0::real)" |
|
62 by (simp add: real_is_int_def int_of_real_def) |
|
63 |
|
64 lemma real_is_int_1[simp]: "real_is_int (1::real)" |
|
65 proof - |
|
66 have "real_is_int (1::real) = real_is_int(real (1::int))" by auto |
|
67 also have "\<dots> = True" by (simp only: real_is_int_real) |
|
68 ultimately show ?thesis by auto |
|
69 qed |
|
70 |
|
71 lemma real_is_int_n1: "real_is_int (-1::real)" |
|
72 proof - |
|
73 have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto |
|
74 also have "\<dots> = True" by (simp only: real_is_int_real) |
|
75 ultimately show ?thesis by auto |
|
76 qed |
|
77 |
|
78 lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)" |
|
79 by (auto simp: real_is_int_def intro!: exI[of _ "number_of x"]) |
|
80 |
|
81 lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)" |
|
82 by (simp add: int_of_real_def) |
|
83 |
|
84 lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)" |
|
85 proof - |
|
86 have 1: "(1::real) = real (1::int)" by auto |
|
87 show ?thesis by (simp only: 1 int_of_real_real) |
|
88 qed |
|
89 |
|
90 lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b" |
|
91 unfolding int_of_real_def |
|
92 by (intro some_equality) |
|
93 (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject) |
|
94 |
|
95 lemma int_div_zdiv: "int (a div b) = (int a) div (int b)" |
|
96 by (rule zdiv_int) |
|
97 |
|
98 lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)" |
|
99 by (rule zmod_int) |
|
100 |
|
101 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a" |
|
102 by arith |
|
103 |
|
104 lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1" |
|
105 by auto |
|
106 |
|
107 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)" |
|
108 by simp |
|
109 |
|
110 lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)" |
|
111 by simp |
|
112 |
|
113 lemma mult_left_one: "1 * a = (a::'a::semiring_1)" |
|
114 by simp |
|
115 |
|
116 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)" |
|
117 by simp |
|
118 |
|
119 lemma int_pow_0: "(a::int)^(Numeral0) = 1" |
|
120 by simp |
|
121 |
|
122 lemma int_pow_1: "(a::int)^(Numeral1) = a" |
|
123 by simp |
|
124 |
|
125 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0" |
|
126 by simp |
|
127 |
|
128 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1" |
|
129 by simp |
|
130 |
|
131 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0" |
|
132 by simp |
|
133 |
|
134 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1" |
|
135 by simp |
|
136 |
|
137 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1" |
|
138 by simp |
|
139 |
|
140 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1" |
|
141 proof - |
|
142 have 1:"((-1)::nat) = 0" |
|
143 by simp |
|
144 show ?thesis by (simp add: 1) |
|
145 qed |
|
146 |
|
147 lemma fst_cong: "a=a' \<Longrightarrow> fst (a,b) = fst (a',b)" |
|
148 by simp |
|
149 |
|
150 lemma snd_cong: "b=b' \<Longrightarrow> snd (a,b) = snd (a,b')" |
|
151 by simp |
|
152 |
|
153 lemma lift_bool: "x \<Longrightarrow> x=True" |
|
154 by simp |
|
155 |
|
156 lemma nlift_bool: "~x \<Longrightarrow> x=False" |
|
157 by simp |
|
158 |
|
159 lemma not_false_eq_true: "(~ False) = True" by simp |
|
160 |
|
161 lemma not_true_eq_false: "(~ True) = False" by simp |
|
162 |
|
163 lemmas binarith = |
|
164 normalize_bin_simps |
|
165 pred_bin_simps succ_bin_simps |
|
166 add_bin_simps minus_bin_simps mult_bin_simps |
|
167 |
|
168 lemma int_eq_number_of_eq: |
|
169 "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)" |
|
170 by (rule eq_number_of_eq) |
|
171 |
|
172 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" |
|
173 by (simp only: iszero_number_of_Pls) |
|
174 |
|
175 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))" |
|
176 by simp |
|
177 |
|
178 lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)" |
|
179 by simp |
|
180 |
|
181 lemma int_iszero_number_of_Bit1: "\<not> iszero ((number_of (Int.Bit1 w))::int)" |
|
182 by simp |
|
183 |
|
184 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)" |
|
185 unfolding neg_def number_of_is_id by simp |
|
186 |
|
187 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" |
|
188 by simp |
|
189 |
|
190 lemma int_neg_number_of_Min: "neg (-1::int)" |
|
191 by simp |
|
192 |
|
193 lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)" |
|
194 by simp |
|
195 |
|
196 lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)" |
|
197 by simp |
|
198 |
|
199 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))" |
|
200 unfolding neg_def number_of_is_id by (simp add: not_less) |
|
201 |
|
202 lemmas intarithrel = |
|
203 int_eq_number_of_eq |
|
204 lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0 |
|
205 lift_bool[OF int_iszero_number_of_Bit1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min] |
|
206 int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq |
|
207 |
|
208 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)" |
|
209 by simp |
|
210 |
|
211 lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))" |
|
212 by simp |
|
213 |
|
214 lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)" |
|
215 by simp |
|
216 |
|
217 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)" |
|
218 by simp |
|
219 |
|
220 lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym |
|
221 |
|
222 lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of |
|
223 |
|
224 lemmas powerarith = nat_number_of zpower_number_of_even |
|
225 zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring] |
|
226 zpower_Pls zpower_Min |
|
227 |
|
228 definition float :: "(int \<times> int) \<Rightarrow> real" where |
|
229 "float = (\<lambda>(a, b). real a * 2 powr real b)" |
|
230 |
|
231 lemma float_add_l0: "float (0, e) + x = x" |
|
232 by (simp add: float_def) |
|
233 |
|
234 lemma float_add_r0: "x + float (0, e) = x" |
|
235 by (simp add: float_def) |
|
236 |
|
237 lemma float_add: |
|
238 "float (a1, e1) + float (a2, e2) = |
|
239 (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) else float (a1*2^(nat (e1-e2))+a2, e2))" |
|
240 by (simp add: float_def algebra_simps powr_realpow[symmetric] powr_divide2[symmetric]) |
|
241 |
|
242 lemma float_mult_l0: "float (0, e) * x = float (0, 0)" |
|
243 by (simp add: float_def) |
|
244 |
|
245 lemma float_mult_r0: "x * float (0, e) = float (0, 0)" |
|
246 by (simp add: float_def) |
|
247 |
|
248 lemma float_mult: |
|
249 "float (a1, e1) * float (a2, e2) = (float (a1 * a2, e1 + e2))" |
|
250 by (simp add: float_def powr_add) |
|
251 |
|
252 lemma float_minus: |
|
253 "- (float (a,b)) = float (-a, b)" |
|
254 by (simp add: float_def) |
|
255 |
|
256 lemma zero_le_float: |
|
257 "(0 <= float (a,b)) = (0 <= a)" |
|
258 using powr_gt_zero[of 2 "real b", arith] |
|
259 by (simp add: float_def zero_le_mult_iff) |
|
260 |
|
261 lemma float_le_zero: |
|
262 "(float (a,b) <= 0) = (a <= 0)" |
|
263 using powr_gt_zero[of 2 "real b", arith] |
|
264 by (simp add: float_def mult_le_0_iff) |
|
265 |
|
266 lemma float_abs: |
|
267 "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))" |
|
268 using powr_gt_zero[of 2 "real b", arith] |
|
269 by (simp add: float_def abs_if mult_less_0_iff) |
|
270 |
|
271 lemma float_zero: |
|
272 "float (0, b) = 0" |
|
273 by (simp add: float_def) |
|
274 |
|
275 lemma float_pprt: |
|
276 "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))" |
|
277 by (auto simp add: zero_le_float float_le_zero float_zero) |
|
278 |
|
279 lemma float_nprt: |
|
280 "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))" |
|
281 by (auto simp add: zero_le_float float_le_zero float_zero) |
|
282 |
|
283 definition lbound :: "real \<Rightarrow> real" |
|
284 where "lbound x = min 0 x" |
|
285 |
|
286 definition ubound :: "real \<Rightarrow> real" |
|
287 where "ubound x = max 0 x" |
|
288 |
|
289 lemma lbound: "lbound x \<le> x" |
|
290 by (simp add: lbound_def) |
|
291 |
|
292 lemma ubound: "x \<le> ubound x" |
|
293 by (simp add: ubound_def) |
|
294 |
|
295 lemma pprt_lbound: "pprt (lbound x) = float (0, 0)" |
|
296 by (auto simp: float_def lbound_def) |
|
297 |
|
298 lemma nprt_ubound: "nprt (ubound x) = float (0, 0)" |
|
299 by (auto simp: float_def ubound_def) |
|
300 |
|
301 lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 |
|
302 float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound |
|
303 |
|
304 (* for use with the compute oracle *) |
|
305 lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false |
|
306 |
|
307 use "~~/src/HOL/Tools/float_arith.ML" |
|
308 |
|
309 end |