author | wenzelm |
Tue, 13 Sep 2005 22:19:23 +0200 | |
changeset 17339 | ab97ccef124a |
parent 15965 | f422f8283491 |
child 19250 | 932a50e2332f |
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*) |
|
16 |
val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm |
|
17 |
val norm_tac: tactic (*AC0 etc.*) |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15531
diff
changeset
|
18 |
val multiply_tac: IntInf.int -> tactic (*apply a ~~ b == k * a ~~ k * b (for k > 0)*) |
4292 | 19 |
end; |
20 |
||
21 |
signature CANCEL_FACTOR = |
|
22 |
sig |
|
23 |
val proc: Sign.sg -> thm list -> term -> thm option |
|
24 |
end; |
|
25 |
||
26 |
||
27 |
functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR = |
|
28 |
struct |
|
29 |
||
30 |
||
31 |
(* greatest common divisor *) |
|
32 |
||
33 |
fun gcd (0, n) = n |
|
34 |
| gcd (m, n) = gcd (n mod m, m); |
|
35 |
||
36 |
val gcds = foldl gcd; |
|
37 |
||
38 |
||
39 |
(* count terms *) |
|
40 |
||
41 |
fun ins_term (t, []) = [(t, 1)] |
|
42 |
| ins_term (t, (u, k) :: uks) = |
|
43 |
if t aconv u then (u, k + 1) :: uks |
|
44 |
else (t, 1) :: (u, k) :: uks; |
|
45 |
||
4452 | 46 |
fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []); |
4292 | 47 |
|
48 |
||
49 |
(* divide sum *) |
|
50 |
||
51 |
fun div_sum d tks = |
|
52 |
Data.mk_sum (flat (map (fn (t, k) => replicate (k div d) t) tks)); |
|
53 |
||
54 |
||
55 |
(* the simplification procedure *) |
|
56 |
||
57 |
fun proc sg _ t = |
|
58 |
(case try Data.dest_bal t of |
|
15531 | 59 |
NONE => NONE |
60 |
| SOME bal => |
|
4292 | 61 |
(case pairself Data.dest_sum bal of |
15531 | 62 |
([_], _) => NONE |
63 |
| (_, [_]) => NONE |
|
4292 | 64 |
| ts_us => |
65 |
let |
|
66 |
val (tks, uks) = pairself count_terms ts_us; |
|
67 |
val d = gcds (gcds (0, map snd tks), map snd uks); |
|
68 |
in |
|
15531 | 69 |
if d = 0 orelse d = 1 then NONE |
70 |
else SOME |
|
4292 | 71 |
(Data.prove_conv (Data.multiply_tac d) Data.norm_tac sg |
72 |
(t, Data.mk_bal (div_sum d tks, div_sum d uks))) |
|
73 |
end)); |
|
74 |
||
75 |
||
76 |
end; |