author | wenzelm |
Wed, 31 Dec 2008 15:30:10 +0100 | |
changeset 29269 | 5c25a2012975 |
parent 24630 | 351a308ab58d |
child 35408 | b48ab741683b |
permissions | -rw-r--r-- |
4292 | 1 |
(* Title: Provers/Arith/cancel_factor.ML |
2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
|
3 |
||
4 |
Cancel common constant factor from balanced exression (e.g. =, <=, < of sums). |
|
5 |
*) |
|
6 |
||
7 |
signature CANCEL_FACTOR_DATA = |
|
8 |
sig |
|
9 |
(*abstract syntax*) |
|
10 |
val mk_sum: term list -> term |
|
11 |
val dest_sum: term -> term list |
|
12 |
val mk_bal: term * term -> term |
|
13 |
val dest_bal: term -> term * term |
|
14 |
(*rules*) |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19250
diff
changeset
|
15 |
val prove_conv: tactic -> tactic -> Proof.context -> term * term -> thm |
23261 | 16 |
val norm_tac: tactic (*AC0 etc.*) |
17 |
val multiply_tac: integer -> tactic |
|
18 |
(*apply a ~~ b == k * a ~~ k * b (for k > 0)*) |
|
4292 | 19 |
end; |
20 |
||
21 |
signature CANCEL_FACTOR = |
|
22 |
sig |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19250
diff
changeset
|
23 |
val proc: simpset -> term -> thm option |
4292 | 24 |
end; |
25 |
||
26 |
||
27 |
functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR = |
|
28 |
struct |
|
29 |
||
30 |
||
31 |
(* count terms *) |
|
32 |
||
33 |
fun ins_term (t, []) = [(t, 1)] |
|
34 |
| ins_term (t, (u, k) :: uks) = |
|
35 |
if t aconv u then (u, k + 1) :: uks |
|
36 |
else (t, 1) :: (u, k) :: uks; |
|
37 |
||
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset
|
38 |
fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []); |
4292 | 39 |
|
40 |
||
41 |
(* divide sum *) |
|
42 |
||
23261 | 43 |
fun div_sum d = |
44 |
Data.mk_sum o maps (fn (t, k) => replicate (k div d) t); |
|
4292 | 45 |
|
46 |
||
47 |
(* the simplification procedure *) |
|
48 |
||
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19250
diff
changeset
|
49 |
fun proc ss t = |
4292 | 50 |
(case try Data.dest_bal t of |
15531 | 51 |
NONE => NONE |
52 |
| SOME bal => |
|
4292 | 53 |
(case pairself Data.dest_sum bal of |
15531 | 54 |
([_], _) => NONE |
55 |
| (_, [_]) => NONE |
|
4292 | 56 |
| ts_us => |
57 |
let |
|
58 |
val (tks, uks) = pairself count_terms ts_us; |
|
23261 | 59 |
val d = 0 |
60 |
|> fold (Integer.gcd o snd) tks |
|
61 |
|> fold (Integer.gcd o snd) uks; |
|
4292 | 62 |
in |
15531 | 63 |
if d = 0 orelse d = 1 then NONE |
64 |
else SOME |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19250
diff
changeset
|
65 |
(Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss) |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23261
diff
changeset
|
66 |
(t, Data.mk_bal (div_sum d tks, div_sum d uks))) |
4292 | 67 |
end)); |
68 |
||
69 |
||
70 |
end; |