11 (*FIXME DELETE*) |
11 (*FIXME DELETE*) |
12 val rat_mult_strict_left_mono = |
12 val rat_mult_strict_left_mono = |
13 read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono; |
13 read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono; |
14 |
14 |
15 val rat_mult_left_mono = |
15 val rat_mult_left_mono = |
16 read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono; |
16 read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono; |
17 |
17 |
18 |
18 val le_number_of_eq = thm"le_number_of_eq"; |
19 val rat_number_of_def = thm "rat_number_of_def"; |
|
20 val diff_rat_def = thm "diff_rat_def"; |
|
21 |
|
22 val rat_numeral_0_eq_0 = thm "rat_numeral_0_eq_0"; |
|
23 val rat_numeral_1_eq_1 = thm "rat_numeral_1_eq_1"; |
|
24 val add_rat_number_of = thm "add_rat_number_of"; |
|
25 val minus_rat_number_of = thm "minus_rat_number_of"; |
|
26 val diff_rat_number_of = thm "diff_rat_number_of"; |
|
27 val mult_rat_number_of = thm "mult_rat_number_of"; |
|
28 val rat_mult_2 = thm "rat_mult_2"; |
|
29 val rat_mult_2_right = thm "rat_mult_2_right"; |
|
30 val eq_rat_number_of = thm "eq_rat_number_of"; |
|
31 val less_rat_number_of = thm "less_rat_number_of"; |
|
32 val rat_minus_1_eq_m1 = thm "rat_minus_1_eq_m1"; |
|
33 val rat_mult_minus1 = thm "rat_mult_minus1"; |
|
34 val rat_mult_minus1_right = thm "rat_mult_minus1_right"; |
|
35 val rat_add_number_of_left = thm "rat_add_number_of_left"; |
|
36 val rat_mult_number_of_left = thm "rat_mult_number_of_left"; |
|
37 val rat_add_number_of_diff1 = thm "rat_add_number_of_diff1"; |
|
38 val rat_add_number_of_diff2 = thm "rat_add_number_of_diff2"; |
|
39 |
|
40 val rat_add_0_left = thm "rat_add_0_left"; |
|
41 val rat_add_0_right = thm "rat_add_0_right"; |
|
42 val rat_mult_1_left = thm "rat_mult_1_left"; |
|
43 val rat_mult_1_right = thm "rat_mult_1_right"; |
|
44 |
|
45 (*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*) |
|
46 val rat_numeral_ss = |
|
47 HOL_ss addsimps [rat_numeral_0_eq_0 RS sym, rat_numeral_1_eq_1 RS sym, |
|
48 rat_minus_1_eq_m1]; |
|
49 |
|
50 fun rename_numerals th = |
|
51 asm_full_simplify rat_numeral_ss (Thm.transfer (the_context ()) th); |
|
52 |
|
53 |
|
54 structure Rat_Numeral_Simprocs = |
|
55 struct |
|
56 |
|
57 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs |
|
58 isn't complicated by the abstract 0 and 1.*) |
|
59 val numeral_syms = [rat_numeral_0_eq_0 RS sym, rat_numeral_1_eq_1 RS sym]; |
|
60 |
|
61 (*Utilities*) |
|
62 |
|
63 val ratT = Type("Rational.rat", []); |
|
64 |
|
65 fun mk_numeral n = HOLogic.number_of_const ratT $ HOLogic.mk_bin n; |
|
66 |
|
67 (*Decodes a binary rat constant, or 0, 1*) |
|
68 val dest_numeral = Int_Numeral_Simprocs.dest_numeral; |
|
69 val find_first_numeral = Int_Numeral_Simprocs.find_first_numeral; |
|
70 |
|
71 val zero = mk_numeral 0; |
|
72 val mk_plus = HOLogic.mk_binop "op +"; |
|
73 |
|
74 val uminus_const = Const ("uminus", ratT --> ratT); |
|
75 |
|
76 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
|
77 fun mk_sum [] = zero |
|
78 | mk_sum [t,u] = mk_plus (t, u) |
|
79 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
80 |
|
81 (*this version ALWAYS includes a trailing zero*) |
|
82 fun long_mk_sum [] = zero |
|
83 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
84 |
|
85 val dest_plus = HOLogic.dest_bin "op +" ratT; |
|
86 |
|
87 (*decompose additions AND subtractions as a sum*) |
|
88 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = |
|
89 dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
90 | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = |
|
91 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
92 | dest_summing (pos, t, ts) = |
|
93 if pos then t::ts else uminus_const$t :: ts; |
|
94 |
|
95 fun dest_sum t = dest_summing (true, t, []); |
|
96 |
|
97 val mk_diff = HOLogic.mk_binop "op -"; |
|
98 val dest_diff = HOLogic.dest_bin "op -" ratT; |
|
99 |
|
100 val one = mk_numeral 1; |
|
101 val mk_times = HOLogic.mk_binop "op *"; |
|
102 |
|
103 fun mk_prod [] = one |
|
104 | mk_prod [t] = t |
|
105 | mk_prod (t :: ts) = if t = one then mk_prod ts |
|
106 else mk_times (t, mk_prod ts); |
|
107 |
|
108 val dest_times = HOLogic.dest_bin "op *" ratT; |
|
109 |
|
110 fun dest_prod t = |
|
111 let val (t,u) = dest_times t |
|
112 in dest_prod t @ dest_prod u end |
|
113 handle TERM _ => [t]; |
|
114 |
|
115 (*DON'T do the obvious simplifications; that would create special cases*) |
|
116 fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); |
|
117 |
|
118 (*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
119 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t |
|
120 | dest_coeff sign t = |
|
121 let val ts = sort Term.term_ord (dest_prod t) |
|
122 val (n, ts') = find_first_numeral [] ts |
|
123 handle TERM _ => (1, ts) |
|
124 in (sign*n, mk_prod ts') end; |
|
125 |
|
126 (*Find first coefficient-term THAT MATCHES u*) |
|
127 fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
128 | find_first_coeff past u (t::terms) = |
|
129 let val (n,u') = dest_coeff 1 t |
|
130 in if u aconv u' then (n, rev past @ terms) |
|
131 else find_first_coeff (t::past) u terms |
|
132 end |
|
133 handle TERM _ => find_first_coeff (t::past) u terms; |
|
134 |
|
135 |
|
136 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*) |
|
137 val add_0s = map rename_numerals [rat_add_0_left, rat_add_0_right]; |
|
138 val mult_1s = map rename_numerals [rat_mult_1_left, rat_mult_1_right] @ |
|
139 [rat_mult_minus1, rat_mult_minus1_right]; |
|
140 |
|
141 (*To perform binary arithmetic*) |
|
142 val bin_simps = |
|
143 [rat_numeral_0_eq_0 RS sym, rat_numeral_1_eq_1 RS sym, |
|
144 add_rat_number_of, rat_add_number_of_left, minus_rat_number_of, |
|
145 diff_rat_number_of, mult_rat_number_of, rat_mult_number_of_left] @ |
|
146 bin_arith_simps @ bin_rel_simps; |
|
147 |
|
148 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms |
|
149 during re-arrangement*) |
|
150 val non_add_bin_simps = |
|
151 bin_simps \\ [rat_add_number_of_left, add_rat_number_of]; |
|
152 |
|
153 (*To evaluate binary negations of coefficients*) |
|
154 val rat_minus_simps = NCons_simps @ |
|
155 [rat_minus_1_eq_m1, minus_rat_number_of, |
|
156 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
|
157 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; |
|
158 |
|
159 (*To let us treat subtraction as addition*) |
|
160 val diff_simps = [diff_rat_def, minus_add_distrib, minus_minus]; |
|
161 |
|
162 (*to extract again any uncancelled minuses*) |
|
163 val rat_minus_from_mult_simps = |
|
164 [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym]; |
|
165 |
|
166 (*combine unary minus with numeric literals, however nested within a product*) |
|
167 val rat_mult_minus_simps = |
|
168 [mult_assoc, minus_mult_left, minus_mult_commute]; |
|
169 |
|
170 (*Apply the given rewrite (if present) just once*) |
|
171 fun trans_tac None = all_tac |
|
172 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
|
173 |
|
174 (*Final simplification: cancel + and * *) |
|
175 val simplify_meta_eq = |
|
176 Int_Numeral_Simprocs.simplify_meta_eq |
|
177 [add_0, add_0_right, |
|
178 mult_zero_left, mult_zero_right, mult_1, mult_1_right]; |
|
179 |
|
180 fun prep_simproc (name, pats, proc) = |
|
181 Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc; |
|
182 |
|
183 structure CancelNumeralsCommon = |
|
184 struct |
|
185 val mk_sum = mk_sum |
|
186 val dest_sum = dest_sum |
|
187 val mk_coeff = mk_coeff |
|
188 val dest_coeff = dest_coeff 1 |
|
189 val find_first_coeff = find_first_coeff [] |
|
190 val trans_tac = trans_tac |
|
191 val norm_tac = |
|
192 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
|
193 rat_minus_simps@add_ac)) |
|
194 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@rat_mult_minus_simps)) |
|
195 THEN ALLGOALS |
|
196 (simp_tac (HOL_ss addsimps rat_minus_from_mult_simps@ |
|
197 add_ac@mult_ac)) |
|
198 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
|
199 val simplify_meta_eq = simplify_meta_eq |
|
200 end; |
|
201 |
|
202 |
|
203 structure EqCancelNumerals = CancelNumeralsFun |
|
204 (open CancelNumeralsCommon |
|
205 val prove_conv = Bin_Simprocs.prove_conv |
|
206 val mk_bal = HOLogic.mk_eq |
|
207 val dest_bal = HOLogic.dest_bin "op =" ratT |
|
208 val bal_add1 = eq_add_iff1 RS trans |
|
209 val bal_add2 = eq_add_iff2 RS trans |
|
210 ); |
|
211 |
|
212 structure LessCancelNumerals = CancelNumeralsFun |
|
213 (open CancelNumeralsCommon |
|
214 val prove_conv = Bin_Simprocs.prove_conv |
|
215 val mk_bal = HOLogic.mk_binrel "op <" |
|
216 val dest_bal = HOLogic.dest_bin "op <" ratT |
|
217 val bal_add1 = less_add_iff1 RS trans |
|
218 val bal_add2 = less_add_iff2 RS trans |
|
219 ); |
|
220 |
|
221 structure LeCancelNumerals = CancelNumeralsFun |
|
222 (open CancelNumeralsCommon |
|
223 val prove_conv = Bin_Simprocs.prove_conv |
|
224 val mk_bal = HOLogic.mk_binrel "op <=" |
|
225 val dest_bal = HOLogic.dest_bin "op <=" ratT |
|
226 val bal_add1 = le_add_iff1 RS trans |
|
227 val bal_add2 = le_add_iff2 RS trans |
|
228 ); |
|
229 |
|
230 val cancel_numerals = |
|
231 map prep_simproc |
|
232 [("rateq_cancel_numerals", |
|
233 ["(l::rat) + m = n", "(l::rat) = m + n", |
|
234 "(l::rat) - m = n", "(l::rat) = m - n", |
|
235 "(l::rat) * m = n", "(l::rat) = m * n"], |
|
236 EqCancelNumerals.proc), |
|
237 ("ratless_cancel_numerals", |
|
238 ["(l::rat) + m < n", "(l::rat) < m + n", |
|
239 "(l::rat) - m < n", "(l::rat) < m - n", |
|
240 "(l::rat) * m < n", "(l::rat) < m * n"], |
|
241 LessCancelNumerals.proc), |
|
242 ("ratle_cancel_numerals", |
|
243 ["(l::rat) + m <= n", "(l::rat) <= m + n", |
|
244 "(l::rat) - m <= n", "(l::rat) <= m - n", |
|
245 "(l::rat) * m <= n", "(l::rat) <= m * n"], |
|
246 LeCancelNumerals.proc)]; |
|
247 |
|
248 |
|
249 structure CombineNumeralsData = |
|
250 struct |
|
251 val add = op + : int*int -> int |
|
252 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) |
|
253 val dest_sum = dest_sum |
|
254 val mk_coeff = mk_coeff |
|
255 val dest_coeff = dest_coeff 1 |
|
256 val left_distrib = combine_common_factor RS trans |
|
257 val prove_conv = Bin_Simprocs.prove_conv_nohyps |
|
258 val trans_tac = trans_tac |
|
259 val norm_tac = |
|
260 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ |
|
261 diff_simps@rat_minus_simps@add_ac)) |
|
262 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@rat_mult_minus_simps)) |
|
263 THEN ALLGOALS (simp_tac (HOL_ss addsimps rat_minus_from_mult_simps@ |
|
264 add_ac@mult_ac)) |
|
265 val numeral_simp_tac = ALLGOALS |
|
266 (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
|
267 val simplify_meta_eq = |
|
268 Int_Numeral_Simprocs.simplify_meta_eq (add_0s@mult_1s) |
|
269 end; |
|
270 |
|
271 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
272 |
|
273 val combine_numerals = |
|
274 prep_simproc ("rat_combine_numerals", ["(i::rat) + j", "(i::rat) - j"], CombineNumerals.proc); |
|
275 |
|
276 |
|
277 (** Declarations for ExtractCommonTerm **) |
|
278 |
|
279 (*this version ALWAYS includes a trailing one*) |
|
280 fun long_mk_prod [] = one |
|
281 | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); |
|
282 |
|
283 (*Find first term that matches u*) |
|
284 fun find_first past u [] = raise TERM("find_first", []) |
|
285 | find_first past u (t::terms) = |
|
286 if u aconv t then (rev past @ terms) |
|
287 else find_first (t::past) u terms |
|
288 handle TERM _ => find_first (t::past) u terms; |
|
289 |
|
290 (*Final simplification: cancel + and * *) |
|
291 fun cancel_simplify_meta_eq cancel_th th = |
|
292 Int_Numeral_Simprocs.simplify_meta_eq |
|
293 [rat_mult_1_left, rat_mult_1_right] |
|
294 (([th, cancel_th]) MRS trans); |
|
295 |
|
296 (*** Making constant folding work for 0 and 1 too ***) |
|
297 |
|
298 structure RatAbstractNumeralsData = |
|
299 struct |
|
300 val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of |
|
301 val is_numeral = Bin_Simprocs.is_numeral |
|
302 val numeral_0_eq_0 = rat_numeral_0_eq_0 |
|
303 val numeral_1_eq_1 = rat_numeral_1_eq_1 |
|
304 val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars |
|
305 fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) |
|
306 val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq |
|
307 end |
|
308 |
|
309 structure RatAbstractNumerals = AbstractNumeralsFun (RatAbstractNumeralsData) |
|
310 |
|
311 (*For addition, we already have rules for the operand 0. |
|
312 Multiplication is omitted because there are already special rules for |
|
313 both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1. |
|
314 For the others, having three patterns is a compromise between just having |
|
315 one (many spurious calls) and having nine (just too many!) *) |
|
316 val eval_numerals = |
|
317 map prep_simproc |
|
318 [("rat_add_eval_numerals", |
|
319 ["(m::rat) + 1", "(m::rat) + number_of v"], |
|
320 RatAbstractNumerals.proc add_rat_number_of), |
|
321 ("rat_diff_eval_numerals", |
|
322 ["(m::rat) - 1", "(m::rat) - number_of v"], |
|
323 RatAbstractNumerals.proc diff_rat_number_of), |
|
324 ("rat_eq_eval_numerals", |
|
325 ["(m::rat) = 0", "(m::rat) = 1", "(m::rat) = number_of v"], |
|
326 RatAbstractNumerals.proc eq_rat_number_of), |
|
327 ("rat_less_eval_numerals", |
|
328 ["(m::rat) < 0", "(m::rat) < 1", "(m::rat) < number_of v"], |
|
329 RatAbstractNumerals.proc less_rat_number_of), |
|
330 ("rat_le_eval_numerals", |
|
331 ["(m::rat) <= 0", "(m::rat) <= 1", "(m::rat) <= number_of v"], |
|
332 RatAbstractNumerals.proc le_number_of_eq_not_less)] |
|
333 |
|
334 end; |
|
335 |
|
336 |
|
337 Addsimprocs Rat_Numeral_Simprocs.eval_numerals; |
|
338 Addsimprocs Rat_Numeral_Simprocs.cancel_numerals; |
|
339 Addsimprocs [Rat_Numeral_Simprocs.combine_numerals]; |
|
340 |
|
341 |
|
342 |
|
343 (** Constant folding for rat plus and times **) |
|
344 |
|
345 (*We do not need |
|
346 structure Rat_Plus_Assoc = Assoc_Fold (Rat_Plus_Assoc_Data); |
|
347 because combine_numerals does the same thing*) |
|
348 |
|
349 structure Rat_Times_Assoc_Data : ASSOC_FOLD_DATA = |
|
350 struct |
|
351 val ss = HOL_ss |
|
352 val eq_reflection = eq_reflection |
|
353 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
|
354 val T = Rat_Numeral_Simprocs.ratT |
|
355 val plus = Const ("op *", [Rat_Numeral_Simprocs.ratT,Rat_Numeral_Simprocs.ratT] ---> Rat_Numeral_Simprocs.ratT) |
|
356 val add_ac = mult_ac |
|
357 end; |
|
358 |
|
359 structure Rat_Times_Assoc = Assoc_Fold (Rat_Times_Assoc_Data); |
|
360 |
|
361 Addsimprocs [Rat_Times_Assoc.conv]; |
|
362 |
19 |
363 |
20 |
364 (****Common factor cancellation****) |
21 (****Common factor cancellation****) |
365 |
22 |
366 (*To quote from Provers/Arith/cancel_numeral_factor.ML: |
23 (*To quote from Provers/Arith/cancel_numeral_factor.ML: |
371 |
28 |
372 where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) |
29 where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) |
373 and d = gcd(m,m') and n=m/d and n'=m'/d. |
30 and d = gcd(m,m') and n=m/d and n'=m'/d. |
374 *) |
31 *) |
375 |
32 |
376 local |
33 val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq] |
377 open Rat_Numeral_Simprocs |
34 |
|
35 local open Int_Numeral_Simprocs |
378 in |
36 in |
379 |
|
380 val rel_rat_number_of = [eq_rat_number_of, less_rat_number_of, |
|
381 le_number_of_eq_not_less] |
|
382 |
37 |
383 structure CancelNumeralFactorCommon = |
38 structure CancelNumeralFactorCommon = |
384 struct |
39 struct |
385 val mk_coeff = mk_coeff |
40 val mk_coeff = mk_coeff |
386 val dest_coeff = dest_coeff 1 |
41 val dest_coeff = dest_coeff 1 |
387 val trans_tac = trans_tac |
42 val trans_tac = trans_tac |
388 val norm_tac = |
43 val norm_tac = |
389 ALLGOALS (simp_tac (HOL_ss addsimps rat_minus_from_mult_simps @ mult_1s)) |
44 ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s)) |
390 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@rat_mult_minus_simps)) |
45 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps)) |
391 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac)) |
46 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac)) |
392 val numeral_simp_tac = |
47 val numeral_simp_tac = |
393 ALLGOALS (simp_tac (HOL_ss addsimps rel_rat_number_of@bin_simps)) |
48 ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps)) |
394 val simplify_meta_eq = simplify_meta_eq |
49 val simplify_meta_eq = |
|
50 Int_Numeral_Simprocs.simplify_meta_eq |
|
51 [add_0, add_0_right, |
|
52 mult_zero_left, mult_zero_right, mult_1, mult_1_right]; |
395 end |
53 end |
396 |
54 |
397 structure DivCancelNumeralFactor = CancelNumeralFactorFun |
55 structure DivCancelNumeralFactor = CancelNumeralFactorFun |
398 (open CancelNumeralFactorCommon |
56 (open CancelNumeralFactorCommon |
399 val prove_conv = Bin_Simprocs.prove_conv |
57 val prove_conv = Bin_Simprocs.prove_conv |
400 val mk_bal = HOLogic.mk_binop "HOL.divide" |
58 val mk_bal = HOLogic.mk_binop "HOL.divide" |
401 val dest_bal = HOLogic.dest_bin "HOL.divide" Rat_Numeral_Simprocs.ratT |
59 val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT |
402 val cancel = mult_divide_cancel_left RS trans |
60 val cancel = mult_divide_cancel_left RS trans |
403 val neg_exchanges = false |
61 val neg_exchanges = false |
404 ) |
62 ) |
405 |
63 |
406 structure EqCancelNumeralFactor = CancelNumeralFactorFun |
64 structure EqCancelNumeralFactor = CancelNumeralFactorFun |
407 (open CancelNumeralFactorCommon |
65 (open CancelNumeralFactorCommon |
408 val prove_conv = Bin_Simprocs.prove_conv |
66 val prove_conv = Bin_Simprocs.prove_conv |
409 val mk_bal = HOLogic.mk_eq |
67 val mk_bal = HOLogic.mk_eq |
410 val dest_bal = HOLogic.dest_bin "op =" Rat_Numeral_Simprocs.ratT |
68 val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
411 val cancel = mult_cancel_left RS trans |
69 val cancel = field_mult_cancel_left RS trans |
412 val neg_exchanges = false |
70 val neg_exchanges = false |
413 ) |
71 ) |
414 |
72 |
415 structure LessCancelNumeralFactor = CancelNumeralFactorFun |
73 structure LessCancelNumeralFactor = CancelNumeralFactorFun |
416 (open CancelNumeralFactorCommon |
74 (open CancelNumeralFactorCommon |
417 val prove_conv = Bin_Simprocs.prove_conv |
75 val prove_conv = Bin_Simprocs.prove_conv |
418 val mk_bal = HOLogic.mk_binrel "op <" |
76 val mk_bal = HOLogic.mk_binrel "op <" |
419 val dest_bal = HOLogic.dest_bin "op <" Rat_Numeral_Simprocs.ratT |
77 val dest_bal = HOLogic.dest_bin "op <" Term.dummyT |
420 val cancel = mult_less_cancel_left RS trans |
78 val cancel = mult_less_cancel_left RS trans |
421 val neg_exchanges = true |
79 val neg_exchanges = true |
422 ) |
80 ) |
423 |
81 |
424 structure LeCancelNumeralFactor = CancelNumeralFactorFun |
82 structure LeCancelNumeralFactor = CancelNumeralFactorFun |
425 (open CancelNumeralFactorCommon |
83 (open CancelNumeralFactorCommon |
426 val prove_conv = Bin_Simprocs.prove_conv |
84 val prove_conv = Bin_Simprocs.prove_conv |
427 val mk_bal = HOLogic.mk_binrel "op <=" |
85 val mk_bal = HOLogic.mk_binrel "op <=" |
428 val dest_bal = HOLogic.dest_bin "op <=" Rat_Numeral_Simprocs.ratT |
86 val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT |
429 val cancel = mult_le_cancel_left RS trans |
87 val cancel = mult_le_cancel_left RS trans |
430 val neg_exchanges = true |
88 val neg_exchanges = true |
431 ) |
89 ) |
432 |
90 |
433 val rat_cancel_numeral_factors_relations = |
91 val field_cancel_numeral_factors_relations = |
434 map prep_simproc |
92 map Bin_Simprocs.prep_simproc |
435 [("rateq_cancel_numeral_factor", |
93 [("field_eq_cancel_numeral_factor", |
436 ["(l::rat) * m = n", "(l::rat) = m * n"], |
94 ["(l::'a::{field,number_ring}) * m = n", |
|
95 "(l::'a::{field,number_ring}) = m * n"], |
437 EqCancelNumeralFactor.proc), |
96 EqCancelNumeralFactor.proc), |
438 ("ratless_cancel_numeral_factor", |
97 ("field_less_cancel_numeral_factor", |
439 ["(l::rat) * m < n", "(l::rat) < m * n"], |
98 ["(l::'a::{ordered_field,number_ring}) * m < n", |
|
99 "(l::'a::{ordered_field,number_ring}) < m * n"], |
440 LessCancelNumeralFactor.proc), |
100 LessCancelNumeralFactor.proc), |
441 ("ratle_cancel_numeral_factor", |
101 ("field_le_cancel_numeral_factor", |
442 ["(l::rat) * m <= n", "(l::rat) <= m * n"], |
102 ["(l::'a::{ordered_field,number_ring}) * m <= n", |
|
103 "(l::'a::{ordered_field,number_ring}) <= m * n"], |
443 LeCancelNumeralFactor.proc)] |
104 LeCancelNumeralFactor.proc)] |
444 |
105 |
445 val rat_cancel_numeral_factors_divide = prep_simproc |
106 val field_cancel_numeral_factors_divide = |
446 ("ratdiv_cancel_numeral_factor", |
107 Bin_Simprocs.prep_simproc |
447 ["((l::rat) * m) / n", "(l::rat) / (m * n)", |
108 ("field_cancel_numeral_factor", |
448 "((number_of v)::rat) / (number_of w)"], |
109 ["((l::'a::{field,number_ring}) * m) / n", |
|
110 "(l::'a::{field,number_ring}) / (m * n)", |
|
111 "((number_of v)::'a::{field,number_ring}) / (number_of w)"], |
449 DivCancelNumeralFactor.proc) |
112 DivCancelNumeralFactor.proc) |
450 |
113 |
451 val rat_cancel_numeral_factors = |
114 val field_cancel_numeral_factors = |
452 rat_cancel_numeral_factors_relations @ |
115 field_cancel_numeral_factors_relations @ |
453 [rat_cancel_numeral_factors_divide] |
116 [field_cancel_numeral_factors_divide] |
454 |
117 |
455 end; |
118 end; |
456 |
119 |
457 Addsimprocs rat_cancel_numeral_factors; |
120 Addsimprocs field_cancel_numeral_factors; |
458 |
121 |
459 |
122 |
460 (*examples: |
123 (*examples: |
461 print_depth 22; |
124 print_depth 22; |
462 set timing; |
125 set timing; |
598 [(rat_mult_strict_left_mono, |
257 [(rat_mult_strict_left_mono, |
599 cvar(rat_mult_strict_left_mono, hd(tl(prems_of rat_mult_strict_left_mono)))), |
258 cvar(rat_mult_strict_left_mono, hd(tl(prems_of rat_mult_strict_left_mono)))), |
600 (rat_mult_left_mono, |
259 (rat_mult_left_mono, |
601 cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))] |
260 cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))] |
602 |
261 |
603 val simps = [True_implies_equals, |
262 val simps = [order_less_irrefl, True_implies_equals, |
604 inst "a" "(number_of ?v)" right_distrib, |
263 inst "a" "(number_of ?v)" right_distrib, |
605 divide_1, times_divide_eq_right, times_divide_eq_left, |
264 divide_1, divide_zero_left, |
|
265 times_divide_eq_right, times_divide_eq_left, |
606 of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff, |
266 of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff, |
607 of_int_mult, of_int_of_nat_eq, rat_number_of_def]; |
267 of_int_mult, of_int_of_nat_eq]; |
608 |
268 |
609 in |
269 in |
610 |
270 |
611 val fast_rat_arith_simproc = Simplifier.simproc (Theory.sign_of(the_context())) |
271 val fast_rat_arith_simproc = |
|
272 Simplifier.simproc (Theory.sign_of(the_context())) |
612 "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"] |
273 "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"] |
613 Fast_Arith.lin_arith_prover; |
274 Fast_Arith.lin_arith_prover; |
614 |
275 |
615 val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2, |
276 val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2, |
616 of_nat_eq_iff RS iffD2]; |
277 of_nat_eq_iff RS iffD2]; |
617 |
278 |
618 val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2, |
279 val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2, |
619 of_int_eq_iff RS iffD2]; |
280 of_int_eq_iff RS iffD2]; |
|
281 |
|
282 val ratT = Type("Rational.rat", []); |
620 |
283 |
621 val rat_arith_setup = |
284 val rat_arith_setup = |
622 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
285 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
623 {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_field, |
286 {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_field, |
624 mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms, |
287 mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms, |
625 inj_thms = int_inj_thms @ inj_thms, |
288 inj_thms = int_inj_thms @ inj_thms, |
626 lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*) |
289 lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*) |
627 simpset = simpset addsimps add_rules |
290 simpset = simpset addsimps simps |
628 addsimps simps |
|
629 addsimprocs simprocs}), |
291 addsimprocs simprocs}), |
630 arith_inj_const("IntDef.of_nat", HOLogic.natT --> Rat_Numeral_Simprocs.ratT), |
292 arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT), |
631 arith_inj_const("IntDef.of_int", HOLogic.intT --> Rat_Numeral_Simprocs.ratT), |
293 arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT), |
632 arith_discrete ("Rational.rat",false), |
294 arith_discrete ("Rational.rat",false), |
633 Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]]; |
295 Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]]; |
634 |
296 |
635 |
|
636 end; |
297 end; |
637 |
|
638 |
|