13 |
13 |
14 val hypreal_mult_left_mono = |
14 val hypreal_mult_left_mono = |
15 read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; |
15 read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; |
16 |
16 |
17 |
17 |
18 val hypreal_number_of = thm "hypreal_number_of"; |
|
19 val hypreal_numeral_0_eq_0 = thm "hypreal_numeral_0_eq_0"; |
|
20 val hypreal_numeral_1_eq_1 = thm "hypreal_numeral_1_eq_1"; |
|
21 val hypreal_number_of_def = thm "hypreal_number_of_def"; |
|
22 val add_hypreal_number_of = thm "add_hypreal_number_of"; |
|
23 val minus_hypreal_number_of = thm "minus_hypreal_number_of"; |
|
24 val diff_hypreal_number_of = thm "diff_hypreal_number_of"; |
|
25 val mult_hypreal_number_of = thm "mult_hypreal_number_of"; |
|
26 val hypreal_mult_2 = thm "hypreal_mult_2"; |
|
27 val hypreal_mult_2_right = thm "hypreal_mult_2_right"; |
|
28 val eq_hypreal_number_of = thm "eq_hypreal_number_of"; |
|
29 val less_hypreal_number_of = thm "less_hypreal_number_of"; |
|
30 val hypreal_minus_1_eq_m1 = thm "hypreal_minus_1_eq_m1"; |
|
31 val hypreal_mult_minus1 = thm "hypreal_mult_minus1"; |
|
32 val hypreal_mult_minus1_right = thm "hypreal_mult_minus1_right"; |
|
33 val hypreal_add_number_of_left = thm "hypreal_add_number_of_left"; |
|
34 val hypreal_mult_number_of_left = thm "hypreal_mult_number_of_left"; |
|
35 val hypreal_add_number_of_diff1 = thm "hypreal_add_number_of_diff1"; |
|
36 val hypreal_add_number_of_diff2 = thm "hypreal_add_number_of_diff2"; |
|
37 |
|
38 (*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*) |
|
39 val hypreal_numeral_ss = |
|
40 real_numeral_ss addsimps [hypreal_numeral_0_eq_0 RS sym, |
|
41 hypreal_numeral_1_eq_1 RS sym, |
|
42 hypreal_minus_1_eq_m1] |
|
43 |
|
44 fun rename_numerals th = |
|
45 asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th) |
|
46 |
|
47 |
|
48 structure Hyperreal_Numeral_Simprocs = |
|
49 struct |
|
50 |
|
51 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs |
|
52 isn't complicated by the abstract 0 and 1.*) |
|
53 val numeral_syms = [hypreal_numeral_0_eq_0 RS sym, |
|
54 hypreal_numeral_1_eq_1 RS sym] |
|
55 |
|
56 (*Utilities*) |
|
57 |
|
58 val hyprealT = Type("HyperDef.hypreal",[]) |
|
59 |
|
60 fun mk_numeral n = HOLogic.number_of_const hyprealT $ HOLogic.mk_bin n |
|
61 |
|
62 val dest_numeral = Real_Numeral_Simprocs.dest_numeral |
|
63 |
|
64 val find_first_numeral = Real_Numeral_Simprocs.find_first_numeral |
|
65 |
|
66 val zero = mk_numeral 0 |
|
67 val mk_plus = Real_Numeral_Simprocs.mk_plus |
|
68 |
|
69 val uminus_const = Const ("uminus", hyprealT --> hyprealT) |
|
70 |
|
71 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
|
72 fun mk_sum [] = zero |
|
73 | mk_sum [t,u] = mk_plus (t, u) |
|
74 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts) |
|
75 |
|
76 (*this version ALWAYS includes a trailing zero*) |
|
77 fun long_mk_sum [] = zero |
|
78 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts) |
|
79 |
|
80 val dest_plus = HOLogic.dest_bin "op +" hyprealT |
|
81 |
|
82 (*decompose additions AND subtractions as a sum*) |
|
83 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = |
|
84 dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
85 | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = |
|
86 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
87 | dest_summing (pos, t, ts) = |
|
88 if pos then t::ts else uminus_const$t :: ts |
|
89 |
|
90 fun dest_sum t = dest_summing (true, t, []) |
|
91 |
|
92 val mk_diff = HOLogic.mk_binop "op -" |
|
93 val dest_diff = HOLogic.dest_bin "op -" hyprealT |
|
94 |
|
95 val one = mk_numeral 1 |
|
96 val mk_times = HOLogic.mk_binop "op *" |
|
97 |
|
98 fun mk_prod [] = one |
|
99 | mk_prod [t] = t |
|
100 | mk_prod (t :: ts) = if t = one then mk_prod ts |
|
101 else mk_times (t, mk_prod ts) |
|
102 |
|
103 val dest_times = HOLogic.dest_bin "op *" hyprealT |
|
104 |
|
105 fun dest_prod t = |
|
106 let val (t,u) = dest_times t |
|
107 in dest_prod t @ dest_prod u end |
|
108 handle TERM _ => [t] |
|
109 |
|
110 (*DON'T do the obvious simplifications; that would create special cases*) |
|
111 fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts) |
|
112 |
|
113 (*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
114 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t |
|
115 | dest_coeff sign t = |
|
116 let val ts = sort Term.term_ord (dest_prod t) |
|
117 val (n, ts') = find_first_numeral [] ts |
|
118 handle TERM _ => (1, ts) |
|
119 in (sign*n, mk_prod ts') end |
|
120 |
|
121 (*Find first coefficient-term THAT MATCHES u*) |
|
122 fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
123 | find_first_coeff past u (t::terms) = |
|
124 let val (n,u') = dest_coeff 1 t |
|
125 in if u aconv u' then (n, rev past @ terms) |
|
126 else find_first_coeff (t::past) u terms |
|
127 end |
|
128 handle TERM _ => find_first_coeff (t::past) u terms |
|
129 |
|
130 |
|
131 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*) |
|
132 val add_0s = map rename_numerals |
|
133 [hypreal_add_zero_left, hypreal_add_zero_right] |
|
134 val mult_1s = map rename_numerals [hypreal_mult_1, hypreal_mult_1_right] @ |
|
135 [hypreal_mult_minus1, hypreal_mult_minus1_right] |
|
136 |
|
137 (*To perform binary arithmetic*) |
|
138 val bin_simps = |
|
139 [hypreal_numeral_0_eq_0 RS sym, hypreal_numeral_1_eq_1 RS sym, |
|
140 add_hypreal_number_of, hypreal_add_number_of_left, |
|
141 minus_hypreal_number_of, |
|
142 diff_hypreal_number_of, mult_hypreal_number_of, |
|
143 hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps |
|
144 |
|
145 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms |
|
146 during re-arrangement*) |
|
147 val non_add_bin_simps = |
|
148 bin_simps \\ [hypreal_add_number_of_left, add_hypreal_number_of] |
|
149 |
|
150 (*To evaluate binary negations of coefficients*) |
|
151 val hypreal_minus_simps = NCons_simps @ |
|
152 [hypreal_minus_1_eq_m1, minus_hypreal_number_of, |
|
153 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
|
154 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min] |
|
155 |
|
156 (*To let us treat subtraction as addition*) |
|
157 val diff_simps = [hypreal_diff_def, minus_add_distrib, minus_minus] |
|
158 |
|
159 (*push the unary minus down: - x * y = x * - y *) |
|
160 val hypreal_minus_mult_eq_1_to_2 = |
|
161 [minus_mult_left RS sym, minus_mult_right] MRS trans |
|
162 |> standard |
|
163 |
|
164 (*to extract again any uncancelled minuses*) |
|
165 val hypreal_minus_from_mult_simps = |
|
166 [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym] |
|
167 |
|
168 (*combine unary minus with numeric literals, however nested within a product*) |
|
169 val hypreal_mult_minus_simps = |
|
170 [hypreal_mult_assoc, minus_mult_left, hypreal_minus_mult_eq_1_to_2] |
|
171 |
|
172 (*Final simplification: cancel + and * *) |
|
173 val simplify_meta_eq = |
|
174 Int_Numeral_Simprocs.simplify_meta_eq |
|
175 [hypreal_add_zero_left, hypreal_add_zero_right, |
|
176 mult_zero_left, mult_zero_right, mult_1, mult_1_right] |
|
177 |
|
178 val prep_simproc = Real_Numeral_Simprocs.prep_simproc |
|
179 |
|
180 structure CancelNumeralsCommon = |
|
181 struct |
|
182 val mk_sum = mk_sum |
|
183 val dest_sum = dest_sum |
|
184 val mk_coeff = mk_coeff |
|
185 val dest_coeff = dest_coeff 1 |
|
186 val find_first_coeff = find_first_coeff [] |
|
187 val trans_tac = Real_Numeral_Simprocs.trans_tac |
|
188 val norm_tac = |
|
189 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
|
190 hypreal_minus_simps@add_ac)) |
|
191 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) |
|
192 THEN ALLGOALS |
|
193 (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ |
|
194 add_ac@mult_ac)) |
|
195 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
|
196 val simplify_meta_eq = simplify_meta_eq |
|
197 end |
|
198 |
|
199 |
|
200 structure EqCancelNumerals = CancelNumeralsFun |
|
201 (open CancelNumeralsCommon |
|
202 val prove_conv = Bin_Simprocs.prove_conv |
|
203 val mk_bal = HOLogic.mk_eq |
|
204 val dest_bal = HOLogic.dest_bin "op =" hyprealT |
|
205 val bal_add1 = eq_add_iff1 RS trans |
|
206 val bal_add2 = eq_add_iff2 RS trans |
|
207 ) |
|
208 |
|
209 structure LessCancelNumerals = CancelNumeralsFun |
|
210 (open CancelNumeralsCommon |
|
211 val prove_conv = Bin_Simprocs.prove_conv |
|
212 val mk_bal = HOLogic.mk_binrel "op <" |
|
213 val dest_bal = HOLogic.dest_bin "op <" hyprealT |
|
214 val bal_add1 = less_add_iff1 RS trans |
|
215 val bal_add2 = less_add_iff2 RS trans |
|
216 ) |
|
217 |
|
218 structure LeCancelNumerals = CancelNumeralsFun |
|
219 (open CancelNumeralsCommon |
|
220 val prove_conv = Bin_Simprocs.prove_conv |
|
221 val mk_bal = HOLogic.mk_binrel "op <=" |
|
222 val dest_bal = HOLogic.dest_bin "op <=" hyprealT |
|
223 val bal_add1 = le_add_iff1 RS trans |
|
224 val bal_add2 = le_add_iff2 RS trans |
|
225 ) |
|
226 |
|
227 val cancel_numerals = |
|
228 map prep_simproc |
|
229 [("hyprealeq_cancel_numerals", |
|
230 ["(l::hypreal) + m = n", "(l::hypreal) = m + n", |
|
231 "(l::hypreal) - m = n", "(l::hypreal) = m - n", |
|
232 "(l::hypreal) * m = n", "(l::hypreal) = m * n"], |
|
233 EqCancelNumerals.proc), |
|
234 ("hyprealless_cancel_numerals", |
|
235 ["(l::hypreal) + m < n", "(l::hypreal) < m + n", |
|
236 "(l::hypreal) - m < n", "(l::hypreal) < m - n", |
|
237 "(l::hypreal) * m < n", "(l::hypreal) < m * n"], |
|
238 LessCancelNumerals.proc), |
|
239 ("hyprealle_cancel_numerals", |
|
240 ["(l::hypreal) + m <= n", "(l::hypreal) <= m + n", |
|
241 "(l::hypreal) - m <= n", "(l::hypreal) <= m - n", |
|
242 "(l::hypreal) * m <= n", "(l::hypreal) <= m * n"], |
|
243 LeCancelNumerals.proc)] |
|
244 |
|
245 |
|
246 structure CombineNumeralsData = |
|
247 struct |
|
248 val add = op + : int*int -> int |
|
249 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) |
|
250 val dest_sum = dest_sum |
|
251 val mk_coeff = mk_coeff |
|
252 val dest_coeff = dest_coeff 1 |
|
253 val left_distrib = combine_common_factor RS trans |
|
254 val prove_conv = Bin_Simprocs.prove_conv_nohyps |
|
255 val trans_tac = Real_Numeral_Simprocs.trans_tac |
|
256 val norm_tac = |
|
257 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ |
|
258 diff_simps@hypreal_minus_simps@add_ac)) |
|
259 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) |
|
260 THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ |
|
261 add_ac@mult_ac)) |
|
262 val numeral_simp_tac = ALLGOALS |
|
263 (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
|
264 val simplify_meta_eq = simplify_meta_eq |
|
265 end |
|
266 |
|
267 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData) |
|
268 |
|
269 val combine_numerals = |
|
270 prep_simproc |
|
271 ("hypreal_combine_numerals", ["(i::hypreal) + j", "(i::hypreal) - j"], CombineNumerals.proc) |
|
272 |
|
273 |
|
274 (** Declarations for ExtractCommonTerm **) |
|
275 |
|
276 (*this version ALWAYS includes a trailing one*) |
|
277 fun long_mk_prod [] = one |
|
278 | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts) |
|
279 |
|
280 (*Find first term that matches u*) |
|
281 fun find_first past u [] = raise TERM("find_first", []) |
|
282 | find_first past u (t::terms) = |
|
283 if u aconv t then (rev past @ terms) |
|
284 else find_first (t::past) u terms |
|
285 handle TERM _ => find_first (t::past) u terms |
|
286 |
|
287 (*Final simplification: cancel + and * *) |
|
288 fun cancel_simplify_meta_eq cancel_th th = |
|
289 Int_Numeral_Simprocs.simplify_meta_eq |
|
290 [mult_1, mult_1_right] |
|
291 (([th, cancel_th]) MRS trans) |
|
292 |
|
293 (*** Making constant folding work for 0 and 1 too ***) |
|
294 |
|
295 structure HyperrealAbstractNumeralsData = |
|
296 struct |
|
297 val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of |
|
298 val is_numeral = Bin_Simprocs.is_numeral |
|
299 val numeral_0_eq_0 = hypreal_numeral_0_eq_0 |
|
300 val numeral_1_eq_1 = hypreal_numeral_1_eq_1 |
|
301 val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars |
|
302 fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) |
|
303 val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq |
|
304 end |
|
305 |
|
306 structure HyperrealAbstractNumerals = |
|
307 AbstractNumeralsFun (HyperrealAbstractNumeralsData) |
|
308 |
|
309 (*For addition, we already have rules for the operand 0. |
|
310 Multiplication is omitted because there are already special rules for |
|
311 both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1. |
|
312 For the others, having three patterns is a compromise between just having |
|
313 one (many spurious calls) and having nine (just too many!) *) |
|
314 val eval_numerals = |
|
315 map prep_simproc |
|
316 [("hypreal_add_eval_numerals", |
|
317 ["(m::hypreal) + 1", "(m::hypreal) + number_of v"], |
|
318 HyperrealAbstractNumerals.proc add_hypreal_number_of), |
|
319 ("hypreal_diff_eval_numerals", |
|
320 ["(m::hypreal) - 1", "(m::hypreal) - number_of v"], |
|
321 HyperrealAbstractNumerals.proc diff_hypreal_number_of), |
|
322 ("hypreal_eq_eval_numerals", |
|
323 ["(m::hypreal) = 0", "(m::hypreal) = 1", "(m::hypreal) = number_of v"], |
|
324 HyperrealAbstractNumerals.proc eq_hypreal_number_of), |
|
325 ("hypreal_less_eval_numerals", |
|
326 ["(m::hypreal) < 0", "(m::hypreal) < 1", "(m::hypreal) < number_of v"], |
|
327 HyperrealAbstractNumerals.proc less_hypreal_number_of), |
|
328 ("hypreal_le_eval_numerals", |
|
329 ["(m::hypreal) <= 0", "(m::hypreal) <= 1", "(m::hypreal) <= number_of v"], |
|
330 HyperrealAbstractNumerals.proc le_number_of_eq_not_less)] |
|
331 |
|
332 end; |
|
333 |
|
334 Addsimprocs Hyperreal_Numeral_Simprocs.eval_numerals; |
|
335 Addsimprocs Hyperreal_Numeral_Simprocs.cancel_numerals; |
|
336 Addsimprocs [Hyperreal_Numeral_Simprocs.combine_numerals]; |
|
337 |
|
338 |
|
339 |
|
340 |
|
341 (**** Constant folding for hypreal plus and times ****) |
|
342 |
|
343 (*We do not need |
|
344 structure Hyperreal_Plus_Assoc = Assoc_Fold (Hyperreal_Plus_Assoc_Data) |
|
345 because combine_numerals does the same thing*) |
|
346 |
|
347 structure Hyperreal_Times_Assoc_Data : ASSOC_FOLD_DATA = |
|
348 struct |
|
349 val ss = HOL_ss |
|
350 val eq_reflection = eq_reflection |
|
351 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
|
352 val T = Hyperreal_Numeral_Simprocs.hyprealT |
|
353 val plus = Const ("op *", [T,T] ---> T) |
|
354 val add_ac = mult_ac |
|
355 end; |
|
356 |
|
357 structure Hyperreal_Times_Assoc = Assoc_Fold (Hyperreal_Times_Assoc_Data); |
|
358 |
|
359 Addsimprocs [Hyperreal_Times_Assoc.conv]; |
|
360 |
|
361 |
|
362 |
|
363 (**** Simprocs for numeric literals ****) |
|
364 |
|
365 |
|
366 (****Common factor cancellation****) |
|
367 |
|
368 local |
|
369 open Hyperreal_Numeral_Simprocs |
|
370 in |
|
371 |
|
372 val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of, |
|
373 le_number_of_eq_not_less]; |
|
374 |
|
375 structure CancelNumeralFactorCommon = |
|
376 struct |
|
377 val mk_coeff = mk_coeff |
|
378 val dest_coeff = dest_coeff 1 |
|
379 val trans_tac = Real_Numeral_Simprocs.trans_tac |
|
380 val norm_tac = |
|
381 ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps @ mult_1s)) |
|
382 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps)) |
|
383 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac)) |
|
384 val numeral_simp_tac = |
|
385 ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps)) |
|
386 val simplify_meta_eq = simplify_meta_eq |
|
387 end |
|
388 |
|
389 structure DivCancelNumeralFactor = CancelNumeralFactorFun |
|
390 (open CancelNumeralFactorCommon |
|
391 val prove_conv = Bin_Simprocs.prove_conv |
|
392 val mk_bal = HOLogic.mk_binop "HOL.divide" |
|
393 val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT |
|
394 val cancel = mult_divide_cancel_left RS trans |
|
395 val neg_exchanges = false |
|
396 ) |
|
397 |
|
398 structure EqCancelNumeralFactor = CancelNumeralFactorFun |
|
399 (open CancelNumeralFactorCommon |
|
400 val prove_conv = Bin_Simprocs.prove_conv |
|
401 val mk_bal = HOLogic.mk_eq |
|
402 val dest_bal = HOLogic.dest_bin "op =" hyprealT |
|
403 val cancel = mult_cancel_left RS trans |
|
404 val neg_exchanges = false |
|
405 ) |
|
406 |
|
407 structure LessCancelNumeralFactor = CancelNumeralFactorFun |
|
408 (open CancelNumeralFactorCommon |
|
409 val prove_conv = Bin_Simprocs.prove_conv |
|
410 val mk_bal = HOLogic.mk_binrel "op <" |
|
411 val dest_bal = HOLogic.dest_bin "op <" hyprealT |
|
412 val cancel = mult_less_cancel_left RS trans |
|
413 val neg_exchanges = true |
|
414 ) |
|
415 |
|
416 structure LeCancelNumeralFactor = CancelNumeralFactorFun |
|
417 (open CancelNumeralFactorCommon |
|
418 val prove_conv = Bin_Simprocs.prove_conv |
|
419 val mk_bal = HOLogic.mk_binrel "op <=" |
|
420 val dest_bal = HOLogic.dest_bin "op <=" hyprealT |
|
421 val cancel = mult_le_cancel_left RS trans |
|
422 val neg_exchanges = true |
|
423 ) |
|
424 |
|
425 val hypreal_cancel_numeral_factors_relations = |
|
426 map prep_simproc |
|
427 [("hyprealeq_cancel_numeral_factor", |
|
428 ["(l::hypreal) * m = n", "(l::hypreal) = m * n"], |
|
429 EqCancelNumeralFactor.proc), |
|
430 ("hyprealless_cancel_numeral_factor", |
|
431 ["(l::hypreal) * m < n", "(l::hypreal) < m * n"], |
|
432 LessCancelNumeralFactor.proc), |
|
433 ("hyprealle_cancel_numeral_factor", |
|
434 ["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"], |
|
435 LeCancelNumeralFactor.proc)]; |
|
436 |
|
437 val hypreal_cancel_numeral_factors_divide = prep_simproc |
|
438 ("hyprealdiv_cancel_numeral_factor", |
|
439 ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)", |
|
440 "((number_of v)::hypreal) / (number_of w)"], |
|
441 DivCancelNumeralFactor.proc); |
|
442 |
|
443 val hypreal_cancel_numeral_factors = |
|
444 hypreal_cancel_numeral_factors_relations @ |
|
445 [hypreal_cancel_numeral_factors_divide]; |
|
446 |
|
447 end; |
|
448 |
|
449 Addsimprocs hypreal_cancel_numeral_factors; |
|
450 |
|
451 |
|
452 |
|
453 (** Declarations for ExtractCommonTerm **) |
|
454 |
|
455 local |
|
456 open Hyperreal_Numeral_Simprocs |
|
457 in |
|
458 |
|
459 structure CancelFactorCommon = |
|
460 struct |
|
461 val mk_sum = long_mk_prod |
|
462 val dest_sum = dest_prod |
|
463 val mk_coeff = mk_coeff |
|
464 val dest_coeff = dest_coeff |
|
465 val find_first = find_first [] |
|
466 val trans_tac = Real_Numeral_Simprocs.trans_tac |
|
467 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac)) |
|
468 end; |
|
469 |
|
470 structure EqCancelFactor = ExtractCommonTermFun |
|
471 (open CancelFactorCommon |
|
472 val prove_conv = Bin_Simprocs.prove_conv |
|
473 val mk_bal = HOLogic.mk_eq |
|
474 val dest_bal = HOLogic.dest_bin "op =" hyprealT |
|
475 val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left |
|
476 ); |
|
477 |
|
478 |
|
479 structure DivideCancelFactor = ExtractCommonTermFun |
|
480 (open CancelFactorCommon |
|
481 val prove_conv = Bin_Simprocs.prove_conv |
|
482 val mk_bal = HOLogic.mk_binop "HOL.divide" |
|
483 val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT |
|
484 val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if |
|
485 ); |
|
486 |
|
487 val hypreal_cancel_factor = |
|
488 map prep_simproc |
|
489 [("hypreal_eq_cancel_factor", ["(l::hypreal) * m = n", "(l::hypreal) = m * n"], |
|
490 EqCancelFactor.proc), |
|
491 ("hypreal_divide_cancel_factor", ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"], |
|
492 DivideCancelFactor.proc)]; |
|
493 |
|
494 end; |
|
495 |
|
496 Addsimprocs hypreal_cancel_factor; |
|
497 |
|
498 |
|
499 |
|
500 |
|
501 (****Instantiation of the generic linear arithmetic package****) |
18 (****Instantiation of the generic linear arithmetic package****) |
502 |
19 |
503 |
20 |
504 local |
21 local |
505 |
|
506 (* reduce contradictory <= to False *) |
|
507 val add_rules = |
|
508 [hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1, |
|
509 add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, |
|
510 mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of]; |
|
511 |
|
512 val simprocs = [Hyperreal_Times_Assoc.conv, |
|
513 Hyperreal_Numeral_Simprocs.combine_numerals, |
|
514 hypreal_cancel_numeral_factors_divide]@ |
|
515 Hyperreal_Numeral_Simprocs.cancel_numerals @ |
|
516 Hyperreal_Numeral_Simprocs.eval_numerals; |
|
517 |
22 |
518 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
23 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
519 |
24 |
520 val hypreal_mult_mono_thms = |
25 val hypreal_mult_mono_thms = |
521 [(rotate_prems 1 hypreal_mult_less_mono2, |
26 [(rotate_prems 1 hypreal_mult_less_mono2, |