src/Provers/Arith/cancel_sums.ML
 author paulson Fri Jun 16 13:13:55 2000 +0200 (2000-06-16) changeset 9073 40d8dfac96b8 parent 4452 b2ee34200dab child 15027 d23887300b96 permissions -rw-r--r--
tracing flag for arith_tac
1 (*  Title:      Provers/Arith/cancel_sums.ML
2     ID:         \$Id\$
3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
5 Cancel common summands of balanced expressions:
7   A + x + B ~~ A' + x + B'  ==  A + B ~~ A' + B'
9 where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, -).
10 *)
12 signature CANCEL_SUMS_DATA =
13 sig
14   (*abstract syntax*)
15   val mk_sum: term list -> term
16   val dest_sum: term -> term list
17   val mk_bal: term * term -> term
18   val dest_bal: term -> term * term
19   (*rules*)
20   val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
21   val norm_tac: tactic                   	(*AC0 etc.*)
22   val uncancel_tac: cterm -> tactic      	(*apply A ~~ B  ==  x + A ~~ x + B*)
23 end;
25 signature CANCEL_SUMS =
26 sig
27   val proc: Sign.sg -> thm list -> term -> thm option
28 end;
31 functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS =
32 struct
35 (* cancel *)
37 fun cons1 x (xs, y, z) = (x :: xs, y, z);
38 fun cons2 y (x, ys, z) = (x, y :: ys, z);
39 fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
41 (*symmetric difference of multisets -- assumed to be sorted wrt. Logic.term_ord*)
42 fun cancel ts [] vs = (ts, [], vs)
43   | cancel [] us vs = ([], us, vs)
44   | cancel (t :: ts) (u :: us) vs =
45       (case Term.term_ord (t, u) of
46         EQUAL => cancel ts us (t :: vs)
47       | LESS => cons1 t (cancel ts (u :: us) vs)
48       | GREATER => cons2 u (cancel (t :: ts) us vs));
51 (* uncancel *)
53 fun uncancel_sums_tac _ [] = all_tac
54   | uncancel_sums_tac sg (t :: ts) =
55       Data.uncancel_tac (Thm.cterm_of sg t) THEN
56       uncancel_sums_tac sg ts;
59 (* the simplification procedure *)
61 fun proc sg _ t =
62   (case try Data.dest_bal t of
63     None => None
64   | Some bal =>
65       let
66         val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
67         val (ts', us', vs) = cancel ts us [];
68       in
69         if null vs then None
70         else Some
71           (Data.prove_conv (uncancel_sums_tac sg vs) Data.norm_tac sg
72             (t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
73       end);
76 end;