equal
deleted
inserted
replaced
1 (* Title: Provers/Arith/cancel_factor.ML |
1 (* Title: Provers/Arith/cancel_factor.ML |
2 ID: $Id$ |
|
3 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
2 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
4 |
3 |
5 Cancel common constant factor from balanced exression (e.g. =, <=, < of sums). |
4 Cancel common constant factor from balanced exression (e.g. =, <=, < of sums). |
6 *) |
5 *) |
7 |
6 |
34 fun ins_term (t, []) = [(t, 1)] |
33 fun ins_term (t, []) = [(t, 1)] |
35 | ins_term (t, (u, k) :: uks) = |
34 | ins_term (t, (u, k) :: uks) = |
36 if t aconv u then (u, k + 1) :: uks |
35 if t aconv u then (u, k + 1) :: uks |
37 else (t, 1) :: (u, k) :: uks; |
36 else (t, 1) :: (u, k) :: uks; |
38 |
37 |
39 fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []); |
38 fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []); |
40 |
39 |
41 |
40 |
42 (* divide sum *) |
41 (* divide sum *) |
43 |
42 |
44 fun div_sum d = |
43 fun div_sum d = |