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
     4 
     5 Cancel common summands of balanced expressions:
     6 
     7   A + x + B ~~ A' + x + B'  ==  A + B ~~ A' + B'
     8 
     9 where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, -).
    10 *)
    11 
    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;
    24 
    25 signature CANCEL_SUMS =
    26 sig
    27   val proc: Sign.sg -> thm list -> term -> thm option
    28 end;
    29 
    30 
    31 functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS =
    32 struct
    33 
    34 
    35 (* cancel *)
    36 
    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);
    40 
    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));
    49 
    50 
    51 (* uncancel *)
    52 
    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;
    57 
    58 
    59 (* the simplification procedure *)
    60 
    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);
    74 
    75 
    76 end;