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