11 Goal "hypreal_of_real (number_of w) = number_of w"; |
11 Goal "hypreal_of_real (number_of w) = number_of w"; |
12 by (simp_tac (simpset() addsimps [hypreal_number_of_def]) 1); |
12 by (simp_tac (simpset() addsimps [hypreal_number_of_def]) 1); |
13 qed "hypreal_number_of"; |
13 qed "hypreal_number_of"; |
14 Addsimps [hypreal_number_of]; |
14 Addsimps [hypreal_number_of]; |
15 |
15 |
16 Goalw [hypreal_number_of_def] "(0::hypreal) = Numeral0"; |
16 Goalw [hypreal_number_of_def] "Numeral0 = (0::hypreal)"; |
17 by (simp_tac (simpset() addsimps [hypreal_of_real_zero RS sym]) 1); |
17 by (Simp_tac 1); |
18 qed "zero_eq_numeral_0"; |
18 qed "hypreal_numeral_0_eq_0"; |
19 |
19 |
20 Goalw [hypreal_number_of_def] "(1::hypreal) = Numeral1"; |
20 Goalw [hypreal_number_of_def] "Numeral1 = (1::hypreal)"; |
21 by (simp_tac (simpset() addsimps [hypreal_of_real_one RS sym]) 1); |
21 by (Simp_tac 1); |
22 qed "one_eq_numeral_1"; |
22 qed "hypreal_numeral_1_eq_1"; |
23 |
23 |
24 (** Addition **) |
24 (** Addition **) |
25 |
25 |
26 Goal "(number_of v :: hypreal) + number_of v' = number_of (bin_add v v')"; |
26 Goal "(number_of v :: hypreal) + number_of v' = number_of (bin_add v v')"; |
27 by (simp_tac |
27 by (simp_tac |
55 (HOL_ss addsimps [hypreal_number_of_def, |
55 (HOL_ss addsimps [hypreal_number_of_def, |
56 hypreal_of_real_mult RS sym, mult_real_number_of]) 1); |
56 hypreal_of_real_mult RS sym, mult_real_number_of]) 1); |
57 qed "mult_hypreal_number_of"; |
57 qed "mult_hypreal_number_of"; |
58 Addsimps [mult_hypreal_number_of]; |
58 Addsimps [mult_hypreal_number_of]; |
59 |
59 |
60 Goal "(2::hypreal) = Numeral1 + Numeral1"; |
60 Goal "(2::hypreal) = 1 + 1"; |
61 by (Simp_tac 1); |
61 by (simp_tac (simpset() addsimps [hypreal_numeral_1_eq_1 RS sym]) 1); |
62 val lemma = result(); |
62 val lemma = result(); |
63 |
63 |
64 (*For specialist use: NOT as default simprules*) |
64 (*For specialist use: NOT as default simprules*) |
65 Goal "2 * z = (z+z::hypreal)"; |
65 Goal "2 * z = (z+z::hypreal)"; |
66 by (simp_tac (simpset () |
66 by (simp_tac (simpset () |
67 addsimps [lemma, hypreal_add_mult_distrib, |
67 addsimps [lemma, hypreal_add_mult_distrib, |
68 one_eq_numeral_1 RS sym]) 1); |
68 hypreal_numeral_1_eq_1]) 1); |
69 qed "hypreal_mult_2"; |
69 qed "hypreal_mult_2"; |
70 |
70 |
71 Goal "z * 2 = (z+z::hypreal)"; |
71 Goal "z * 2 = (z+z::hypreal)"; |
72 by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1); |
72 by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1); |
73 qed "hypreal_mult_2_right"; |
73 qed "hypreal_mult_2_right"; |
105 qed "le_hypreal_number_of_eq_not_less"; |
105 qed "le_hypreal_number_of_eq_not_less"; |
106 Addsimps [le_hypreal_number_of_eq_not_less]; |
106 Addsimps [le_hypreal_number_of_eq_not_less]; |
107 |
107 |
108 (*** New versions of existing theorems involving 0, 1 ***) |
108 (*** New versions of existing theorems involving 0, 1 ***) |
109 |
109 |
110 Goal "- Numeral1 = (-1::hypreal)"; |
110 Goal "- 1 = (-1::hypreal)"; |
111 by (Simp_tac 1); |
111 by (simp_tac (simpset() addsimps [hypreal_numeral_1_eq_1 RS sym]) 1); |
112 qed "minus_numeral_one"; |
112 qed "hypreal_minus_1_eq_m1"; |
113 |
113 |
114 (*Maps 0 to Numeral0 and (1::hypreal) to Numeral1 and -(Numeral1) to -1*) |
114 (*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*) |
115 val hypreal_numeral_ss = |
115 val hypreal_numeral_ss = |
116 real_numeral_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, |
116 real_numeral_ss addsimps [hypreal_numeral_0_eq_0 RS sym, |
117 minus_numeral_one]; |
117 hypreal_numeral_1_eq_1 RS sym, |
|
118 hypreal_minus_1_eq_m1]; |
118 |
119 |
119 fun rename_numerals th = |
120 fun rename_numerals th = |
120 asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th); |
121 asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th); |
121 |
|
122 |
|
123 (*Now insert some identities previously stated for 0 and 1*) |
|
124 |
|
125 (** HyperDef **) |
|
126 |
|
127 Addsimps (map rename_numerals |
|
128 [hypreal_minus_zero, hypreal_minus_zero_iff, |
|
129 hypreal_add_zero_left, hypreal_add_zero_right, |
|
130 hypreal_diff_zero, hypreal_diff_zero_right, |
|
131 hypreal_mult_0_right, hypreal_mult_0, |
|
132 hypreal_mult_1_right, hypreal_mult_1, |
|
133 hypreal_inverse_1, hypreal_minus_zero_less_iff]); |
|
134 |
|
135 bind_thm ("hypreal_0_less_mult_iff", |
|
136 rename_numerals hypreal_zero_less_mult_iff); |
|
137 bind_thm ("hypreal_0_le_mult_iff", |
|
138 rename_numerals hypreal_zero_le_mult_iff); |
|
139 bind_thm ("hypreal_mult_less_0_iff", |
|
140 rename_numerals hypreal_mult_less_zero_iff); |
|
141 bind_thm ("hypreal_mult_le_0_iff", |
|
142 rename_numerals hypreal_mult_le_zero_iff); |
|
143 |
|
144 bind_thm ("hypreal_inverse_less_0", rename_numerals hypreal_inverse_less_zero); |
|
145 bind_thm ("hypreal_inverse_gt_0", rename_numerals hypreal_inverse_gt_zero); |
|
146 |
|
147 Addsimps [zero_eq_numeral_0,one_eq_numeral_1]; |
|
148 |
122 |
149 |
123 |
150 (** Simplification of arithmetic when nested to the right **) |
124 (** Simplification of arithmetic when nested to the right **) |
151 |
125 |
152 Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)"; |
126 Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)"; |
174 |
148 |
175 (**** Simprocs for numeric literals ****) |
149 (**** Simprocs for numeric literals ****) |
176 |
150 |
177 (** Combining of literal coefficients in sums of products **) |
151 (** Combining of literal coefficients in sums of products **) |
178 |
152 |
179 Goal "(x < y) = (x-y < (Numeral0::hypreal))"; |
153 Goal "(x < y) = (x-y < (0::hypreal))"; |
180 by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1); |
154 by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1); |
181 qed "hypreal_less_iff_diff_less_0"; |
155 qed "hypreal_less_iff_diff_less_0"; |
182 |
156 |
183 Goal "(x = y) = (x-y = (Numeral0::hypreal))"; |
157 Goal "(x = y) = (x-y = (0::hypreal))"; |
184 by (simp_tac (simpset() addsimps [hypreal_diff_eq_eq]) 1); |
158 by (simp_tac (simpset() addsimps [hypreal_diff_eq_eq]) 1); |
185 qed "hypreal_eq_iff_diff_eq_0"; |
159 qed "hypreal_eq_iff_diff_eq_0"; |
186 |
160 |
187 Goal "(x <= y) = (x-y <= (Numeral0::hypreal))"; |
161 Goal "(x <= y) = (x-y <= (0::hypreal))"; |
188 by (simp_tac (simpset() addsimps [hypreal_diff_le_eq]) 1); |
162 by (simp_tac (simpset() addsimps [hypreal_diff_le_eq]) 1); |
189 qed "hypreal_le_iff_diff_le_0"; |
163 qed "hypreal_le_iff_diff_le_0"; |
190 |
164 |
191 |
165 |
192 (** For combine_numerals **) |
166 (** For combine_numerals **) |
207 hypreal_le_iff_diff_le_0]; |
181 hypreal_le_iff_diff_le_0]; |
208 |
182 |
209 Goal "!!i::hypreal. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; |
183 Goal "!!i::hypreal. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; |
210 by (asm_simp_tac |
184 by (asm_simp_tac |
211 (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ |
185 (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ |
212 hypreal_add_ac@rel_iff_rel_0_rls) 1); |
186 hypreal_add_ac@rel_iff_rel_0_rls) 1); |
213 qed "hypreal_eq_add_iff1"; |
187 qed "hypreal_eq_add_iff1"; |
214 |
188 |
215 Goal "!!i::hypreal. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; |
189 Goal "!!i::hypreal. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; |
216 by (asm_simp_tac |
190 by (asm_simp_tac |
217 (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ |
191 (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ |
240 by (asm_simp_tac |
214 by (asm_simp_tac |
241 (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ |
215 (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ |
242 hypreal_add_ac@rel_iff_rel_0_rls) 1); |
216 hypreal_add_ac@rel_iff_rel_0_rls) 1); |
243 qed "hypreal_le_add_iff2"; |
217 qed "hypreal_le_add_iff2"; |
244 |
218 |
|
219 Goal "-1 * (z::hypreal) = -z"; |
|
220 by (simp_tac (simpset() addsimps [hypreal_minus_1_eq_m1 RS sym, |
|
221 hypreal_mult_minus_1]) 1); |
|
222 qed "hypreal_mult_minus1"; |
|
223 Addsimps [hypreal_mult_minus1]; |
|
224 |
245 Goal "(z::hypreal) * -1 = -z"; |
225 Goal "(z::hypreal) * -1 = -z"; |
246 by (stac (minus_numeral_one RS sym) 1); |
226 by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_minus1 1); |
247 by (stac (hypreal_minus_mult_eq2 RS sym) 1); |
227 qed "hypreal_mult_minus1_right"; |
248 by Auto_tac; |
228 Addsimps [hypreal_mult_minus1_right]; |
249 qed "hypreal_mult_minus_1_right"; |
229 |
250 Addsimps [hypreal_mult_minus_1_right]; |
230 |
251 |
231 Addsimps [hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1]; |
252 Goal "-1 * (z::hypreal) = -z"; |
|
253 by (simp_tac (simpset() addsimps [hypreal_mult_commute]) 1); |
|
254 qed "hypreal_mult_minus_1"; |
|
255 Addsimps [hypreal_mult_minus_1]; |
|
256 |
|
257 |
232 |
258 |
233 |
259 structure Hyperreal_Numeral_Simprocs = |
234 structure Hyperreal_Numeral_Simprocs = |
260 struct |
235 struct |
261 |
236 |
|
237 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs |
|
238 isn't complicated by the abstract 0 and 1.*) |
|
239 val numeral_syms = [hypreal_numeral_0_eq_0 RS sym, |
|
240 hypreal_numeral_1_eq_1 RS sym]; |
|
241 |
262 (*Utilities*) |
242 (*Utilities*) |
263 |
243 |
264 |
|
265 val hyprealT = Type("HyperDef.hypreal",[]); |
244 val hyprealT = Type("HyperDef.hypreal",[]); |
266 |
245 |
267 fun mk_numeral n = HOLogic.number_of_const hyprealT $ HOLogic.mk_bin n; |
246 fun mk_numeral n = HOLogic.number_of_const hyprealT $ HOLogic.mk_bin n; |
268 |
247 |
269 val dest_numeral = Real_Numeral_Simprocs.dest_numeral; |
248 val dest_numeral = Real_Numeral_Simprocs.dest_numeral; |
270 |
249 |
271 val find_first_numeral = Real_Numeral_Simprocs.find_first_numeral; |
250 val find_first_numeral = Real_Numeral_Simprocs.find_first_numeral; |
272 |
251 |
273 val zero = mk_numeral 0; |
252 val zero = mk_numeral 0; |
274 val mk_plus = HOLogic.mk_binop "op +"; |
253 val mk_plus = Real_Numeral_Simprocs.mk_plus; |
275 |
254 |
276 val uminus_const = Const ("uminus", hyprealT --> hyprealT); |
255 val uminus_const = Const ("uminus", hyprealT --> hyprealT); |
277 |
256 |
278 (*Thus mk_sum[t] yields t+Numeral0; longer sums don't have a trailing zero*) |
257 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
279 fun mk_sum [] = zero |
258 fun mk_sum [] = zero |
280 | mk_sum [t,u] = mk_plus (t, u) |
259 | mk_sum [t,u] = mk_plus (t, u) |
281 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
260 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
282 |
261 |
283 (*this version ALWAYS includes a trailing zero*) |
262 (*this version ALWAYS includes a trailing zero*) |
333 else find_first_coeff (t::past) u terms |
312 else find_first_coeff (t::past) u terms |
334 end |
313 end |
335 handle TERM _ => find_first_coeff (t::past) u terms; |
314 handle TERM _ => find_first_coeff (t::past) u terms; |
336 |
315 |
337 |
316 |
338 (*Simplify Numeral1*n and n*Numeral1 to n*) |
317 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*) |
339 val add_0s = map rename_numerals |
318 val add_0s = map rename_numerals |
340 [hypreal_add_zero_left, hypreal_add_zero_right]; |
319 [hypreal_add_zero_left, hypreal_add_zero_right]; |
341 val mult_plus_1s = map rename_numerals |
320 val mult_1s = map rename_numerals [hypreal_mult_1, hypreal_mult_1_right] @ |
342 [hypreal_mult_1, hypreal_mult_1_right]; |
321 [hypreal_mult_minus1, hypreal_mult_minus1_right]; |
343 val mult_minus_1s = map rename_numerals |
|
344 [hypreal_mult_minus_1, hypreal_mult_minus_1_right]; |
|
345 val mult_1s = mult_plus_1s @ mult_minus_1s; |
|
346 |
322 |
347 (*To perform binary arithmetic*) |
323 (*To perform binary arithmetic*) |
348 val bin_simps = |
324 val bin_simps = |
349 [add_hypreal_number_of, hypreal_add_number_of_left, |
325 [hypreal_numeral_0_eq_0 RS sym, hypreal_numeral_1_eq_1 RS sym, |
350 minus_hypreal_number_of, diff_hypreal_number_of, mult_hypreal_number_of, |
326 add_hypreal_number_of, hypreal_add_number_of_left, |
|
327 minus_hypreal_number_of, |
|
328 diff_hypreal_number_of, mult_hypreal_number_of, |
351 hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps; |
329 hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps; |
352 |
330 |
353 (*To evaluate binary negations of coefficients*) |
331 (*To evaluate binary negations of coefficients*) |
354 val hypreal_minus_simps = NCons_simps @ |
332 val hypreal_minus_simps = NCons_simps @ |
355 [minus_hypreal_number_of, |
333 [hypreal_minus_1_eq_m1, minus_hypreal_number_of, |
356 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
334 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
357 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; |
335 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; |
358 |
336 |
359 (*To let us treat subtraction as addition*) |
337 (*To let us treat subtraction as addition*) |
360 val diff_simps = [hypreal_diff_def, hypreal_minus_add_distrib, |
338 val diff_simps = [hypreal_diff_def, hypreal_minus_add_distrib, |
371 hypreal_minus_mult_eq2 RS sym]; |
349 hypreal_minus_mult_eq2 RS sym]; |
372 |
350 |
373 (*combine unary minus with numeric literals, however nested within a product*) |
351 (*combine unary minus with numeric literals, however nested within a product*) |
374 val hypreal_mult_minus_simps = |
352 val hypreal_mult_minus_simps = |
375 [hypreal_mult_assoc, hypreal_minus_mult_eq1, hypreal_minus_mult_eq_1_to_2]; |
353 [hypreal_mult_assoc, hypreal_minus_mult_eq1, hypreal_minus_mult_eq_1_to_2]; |
376 |
|
377 (*Apply the given rewrite (if present) just once*) |
|
378 fun trans_tac None = all_tac |
|
379 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
|
380 |
|
381 fun prove_conv name tacs sg (hyps: thm list) (t,u) = |
|
382 if t aconv u then None |
|
383 else |
|
384 let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) |
|
385 in Some |
|
386 (prove_goalw_cterm [] ct (K tacs) |
|
387 handle ERROR => error |
|
388 ("The error(s) above occurred while trying to prove " ^ |
|
389 string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) |
|
390 end; |
|
391 |
|
392 (*version without the hyps argument*) |
|
393 fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []; |
|
394 |
354 |
395 (*Final simplification: cancel + and * *) |
355 (*Final simplification: cancel + and * *) |
396 val simplify_meta_eq = |
356 val simplify_meta_eq = |
397 Int_Numeral_Simprocs.simplify_meta_eq |
357 Int_Numeral_Simprocs.simplify_meta_eq |
398 [hypreal_add_zero_left, hypreal_add_zero_right, |
358 [hypreal_add_zero_left, hypreal_add_zero_right, |
407 val mk_sum = mk_sum |
367 val mk_sum = mk_sum |
408 val dest_sum = dest_sum |
368 val dest_sum = dest_sum |
409 val mk_coeff = mk_coeff |
369 val mk_coeff = mk_coeff |
410 val dest_coeff = dest_coeff 1 |
370 val dest_coeff = dest_coeff 1 |
411 val find_first_coeff = find_first_coeff [] |
371 val find_first_coeff = find_first_coeff [] |
412 val trans_tac = trans_tac |
372 val trans_tac = Real_Numeral_Simprocs.trans_tac |
413 val norm_tac = |
373 val norm_tac = |
414 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
374 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
415 hypreal_minus_simps@hypreal_add_ac)) |
375 hypreal_minus_simps@hypreal_add_ac)) |
416 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps)) |
376 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps)) |
417 THEN ALLGOALS |
377 THEN ALLGOALS |
422 end; |
382 end; |
423 |
383 |
424 |
384 |
425 structure EqCancelNumerals = CancelNumeralsFun |
385 structure EqCancelNumerals = CancelNumeralsFun |
426 (open CancelNumeralsCommon |
386 (open CancelNumeralsCommon |
427 val prove_conv = prove_conv "hyprealeq_cancel_numerals" |
387 val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealeq_cancel_numerals" |
428 val mk_bal = HOLogic.mk_eq |
388 val mk_bal = HOLogic.mk_eq |
429 val dest_bal = HOLogic.dest_bin "op =" hyprealT |
389 val dest_bal = HOLogic.dest_bin "op =" hyprealT |
430 val bal_add1 = hypreal_eq_add_iff1 RS trans |
390 val bal_add1 = hypreal_eq_add_iff1 RS trans |
431 val bal_add2 = hypreal_eq_add_iff2 RS trans |
391 val bal_add2 = hypreal_eq_add_iff2 RS trans |
432 ); |
392 ); |
433 |
393 |
434 structure LessCancelNumerals = CancelNumeralsFun |
394 structure LessCancelNumerals = CancelNumeralsFun |
435 (open CancelNumeralsCommon |
395 (open CancelNumeralsCommon |
436 val prove_conv = prove_conv "hyprealless_cancel_numerals" |
396 val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealless_cancel_numerals" |
437 val mk_bal = HOLogic.mk_binrel "op <" |
397 val mk_bal = HOLogic.mk_binrel "op <" |
438 val dest_bal = HOLogic.dest_bin "op <" hyprealT |
398 val dest_bal = HOLogic.dest_bin "op <" hyprealT |
439 val bal_add1 = hypreal_less_add_iff1 RS trans |
399 val bal_add1 = hypreal_less_add_iff1 RS trans |
440 val bal_add2 = hypreal_less_add_iff2 RS trans |
400 val bal_add2 = hypreal_less_add_iff2 RS trans |
441 ); |
401 ); |
442 |
402 |
443 structure LeCancelNumerals = CancelNumeralsFun |
403 structure LeCancelNumerals = CancelNumeralsFun |
444 (open CancelNumeralsCommon |
404 (open CancelNumeralsCommon |
445 val prove_conv = prove_conv "hyprealle_cancel_numerals" |
405 val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealle_cancel_numerals" |
446 val mk_bal = HOLogic.mk_binrel "op <=" |
406 val mk_bal = HOLogic.mk_binrel "op <=" |
447 val dest_bal = HOLogic.dest_bin "op <=" hyprealT |
407 val dest_bal = HOLogic.dest_bin "op <=" hyprealT |
448 val bal_add1 = hypreal_le_add_iff1 RS trans |
408 val bal_add1 = hypreal_le_add_iff1 RS trans |
449 val bal_add2 = hypreal_le_add_iff2 RS trans |
409 val bal_add2 = hypreal_le_add_iff2 RS trans |
450 ); |
410 ); |
474 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) |
434 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) |
475 val dest_sum = dest_sum |
435 val dest_sum = dest_sum |
476 val mk_coeff = mk_coeff |
436 val mk_coeff = mk_coeff |
477 val dest_coeff = dest_coeff 1 |
437 val dest_coeff = dest_coeff 1 |
478 val left_distrib = left_hypreal_add_mult_distrib RS trans |
438 val left_distrib = left_hypreal_add_mult_distrib RS trans |
479 val prove_conv = prove_conv_nohyps "hypreal_combine_numerals" |
439 val prove_conv = Real_Numeral_Simprocs.prove_conv_nohyps |
480 val trans_tac = trans_tac |
440 "hypreal_combine_numerals" |
|
441 val trans_tac = Real_Numeral_Simprocs.trans_tac |
481 val norm_tac = |
442 val norm_tac = |
482 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
443 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
483 hypreal_minus_simps@hypreal_add_ac)) |
444 hypreal_minus_simps@hypreal_add_ac)) |
484 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps)) |
445 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps)) |
485 THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ |
446 THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ |
514 fun cancel_simplify_meta_eq cancel_th th = |
475 fun cancel_simplify_meta_eq cancel_th th = |
515 Int_Numeral_Simprocs.simplify_meta_eq |
476 Int_Numeral_Simprocs.simplify_meta_eq |
516 [hypreal_mult_1, hypreal_mult_1_right] |
477 [hypreal_mult_1, hypreal_mult_1_right] |
517 (([th, cancel_th]) MRS trans); |
478 (([th, cancel_th]) MRS trans); |
518 |
479 |
|
480 (*** Making constant folding work for 0 and 1 too ***) |
|
481 |
|
482 structure HyperrealAbstractNumeralsData = |
|
483 struct |
|
484 val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of |
|
485 val is_numeral = Bin_Simprocs.is_numeral |
|
486 val numeral_0_eq_0 = hypreal_numeral_0_eq_0 |
|
487 val numeral_1_eq_1 = hypreal_numeral_1_eq_1 |
|
488 val prove_conv = Real_Numeral_Simprocs.prove_conv_nohyps |
|
489 "hypreal_abstract_numerals" |
|
490 fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) |
|
491 val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq |
|
492 end |
|
493 |
|
494 structure HyperrealAbstractNumerals = |
|
495 AbstractNumeralsFun (HyperrealAbstractNumeralsData) |
|
496 |
|
497 (*For addition, we already have rules for the operand 0. |
|
498 Multiplication is omitted because there are already special rules for |
|
499 both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1. |
|
500 For the others, having three patterns is a compromise between just having |
|
501 one (many spurious calls) and having nine (just too many!) *) |
|
502 val eval_numerals = |
|
503 map prep_simproc |
|
504 [("hypreal_add_eval_numerals", |
|
505 prep_pats ["(m::hypreal) + 1", "(m::hypreal) + number_of v"], |
|
506 HyperrealAbstractNumerals.proc add_hypreal_number_of), |
|
507 ("hypreal_diff_eval_numerals", |
|
508 prep_pats ["(m::hypreal) - 1", "(m::hypreal) - number_of v"], |
|
509 HyperrealAbstractNumerals.proc diff_hypreal_number_of), |
|
510 ("hypreal_eq_eval_numerals", |
|
511 prep_pats ["(m::hypreal) = 0", "(m::hypreal) = 1", |
|
512 "(m::hypreal) = number_of v"], |
|
513 HyperrealAbstractNumerals.proc eq_hypreal_number_of), |
|
514 ("hypreal_less_eval_numerals", |
|
515 prep_pats ["(m::hypreal) < 0", "(m::hypreal) < 1", |
|
516 "(m::hypreal) < number_of v"], |
|
517 HyperrealAbstractNumerals.proc less_hypreal_number_of), |
|
518 ("hypreal_le_eval_numerals", |
|
519 prep_pats ["(m::hypreal) <= 0", "(m::hypreal) <= 1", |
|
520 "(m::hypreal) <= number_of v"], |
|
521 HyperrealAbstractNumerals.proc le_hypreal_number_of_eq_not_less)] |
|
522 |
519 end; |
523 end; |
520 |
524 |
|
525 Addsimprocs Hyperreal_Numeral_Simprocs.eval_numerals; |
521 Addsimprocs Hyperreal_Numeral_Simprocs.cancel_numerals; |
526 Addsimprocs Hyperreal_Numeral_Simprocs.cancel_numerals; |
522 Addsimprocs [Hyperreal_Numeral_Simprocs.combine_numerals]; |
527 Addsimprocs [Hyperreal_Numeral_Simprocs.combine_numerals]; |
523 |
528 |
524 (*The Abel_Cancel simprocs are now obsolete*) |
529 (*The Abel_Cancel simprocs are now obsolete*) |
525 Delsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
530 Delsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
579 |
584 |
580 structure Hyperreal_Times_Assoc = Assoc_Fold (Hyperreal_Times_Assoc_Data); |
585 structure Hyperreal_Times_Assoc = Assoc_Fold (Hyperreal_Times_Assoc_Data); |
581 |
586 |
582 Addsimprocs [Hyperreal_Times_Assoc.conv]; |
587 Addsimprocs [Hyperreal_Times_Assoc.conv]; |
583 |
588 |
584 Addsimps [rename_numerals hypreal_of_real_zero_iff]; |
|
585 |
|
586 (*Simplification of x-y < 0, etc.*) |
589 (*Simplification of x-y < 0, etc.*) |
587 AddIffs [hypreal_less_iff_diff_less_0 RS sym]; |
590 AddIffs [hypreal_less_iff_diff_less_0 RS sym]; |
588 AddIffs [hypreal_eq_iff_diff_eq_0 RS sym]; |
591 AddIffs [hypreal_eq_iff_diff_eq_0 RS sym]; |
589 AddIffs [hypreal_le_iff_diff_le_0 RS sym]; |
592 AddIffs [hypreal_le_iff_diff_le_0 RS sym]; |
590 |
593 |
601 by (stac (hypreal_of_real_le_iff RS sym) 1); |
604 by (stac (hypreal_of_real_le_iff RS sym) 1); |
602 by (Simp_tac 1); |
605 by (Simp_tac 1); |
603 qed "number_of_le_hypreal_of_real_iff"; |
606 qed "number_of_le_hypreal_of_real_iff"; |
604 Addsimps [number_of_le_hypreal_of_real_iff]; |
607 Addsimps [number_of_le_hypreal_of_real_iff]; |
605 |
608 |
|
609 Goal "(hypreal_of_real z = number_of w) = (z = number_of w)"; |
|
610 by (stac (hypreal_of_real_eq_iff RS sym) 1); |
|
611 by (Simp_tac 1); |
|
612 qed "hypreal_of_real_eq_number_of_iff"; |
|
613 Addsimps [hypreal_of_real_eq_number_of_iff]; |
|
614 |
606 Goal "(hypreal_of_real z < number_of w) = (z < number_of w)"; |
615 Goal "(hypreal_of_real z < number_of w) = (z < number_of w)"; |
607 by (stac (hypreal_of_real_less_iff RS sym) 1); |
616 by (stac (hypreal_of_real_less_iff RS sym) 1); |
608 by (Simp_tac 1); |
617 by (Simp_tac 1); |
609 qed "hypreal_of_real_less_number_of_iff"; |
618 qed "hypreal_of_real_less_number_of_iff"; |
610 Addsimps [hypreal_of_real_less_number_of_iff]; |
619 Addsimps [hypreal_of_real_less_number_of_iff]; |
612 Goal "(hypreal_of_real z <= number_of w) = (z <= number_of w)"; |
621 Goal "(hypreal_of_real z <= number_of w) = (z <= number_of w)"; |
613 by (stac (hypreal_of_real_le_iff RS sym) 1); |
622 by (stac (hypreal_of_real_le_iff RS sym) 1); |
614 by (Simp_tac 1); |
623 by (Simp_tac 1); |
615 qed "hypreal_of_real_le_number_of_iff"; |
624 qed "hypreal_of_real_le_number_of_iff"; |
616 Addsimps [hypreal_of_real_le_number_of_iff]; |
625 Addsimps [hypreal_of_real_le_number_of_iff]; |
|
626 |
|
627 (*As above, for the special case of zero*) |
|
628 Addsimps |
|
629 (map (simplify (simpset()) o inst "w" "Pls") |
|
630 [hypreal_of_real_eq_number_of_iff, |
|
631 hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff, |
|
632 number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]); |
|
633 |
|
634 (*As above, for the special case of one*) |
|
635 Addsimps |
|
636 (map (simplify (simpset()) o inst "w" "Pls BIT True") |
|
637 [hypreal_of_real_eq_number_of_iff, |
|
638 hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff, |
|
639 number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]); |
617 |
640 |
618 (** <= monotonicity results: needed for arithmetic **) |
641 (** <= monotonicity results: needed for arithmetic **) |
619 |
642 |
620 Goal "[| i <= j; (0::hypreal) <= k |] ==> i*k <= j*k"; |
643 Goal "[| i <= j; (0::hypreal) <= k |] ==> i*k <= j*k"; |
621 by (auto_tac (claset(), |
644 by (auto_tac (claset(), |