src/Provers/Arith/cancel_sums.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 38052 04a8de29e8f7
permissions -rw-r--r--
modernized structure Object_Logic;
     1 (*  Title:      Provers/Arith/cancel_sums.ML
     2     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     3 
     4 Cancel common summands of balanced expressions:
     5 
     6   A + x + B ~~ A' + x + B'  ==  A + B ~~ A' + B'
     7 
     8 where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, -).
     9 *)
    10 
    11 signature CANCEL_SUMS_DATA =
    12 sig
    13   (*abstract syntax*)
    14   val mk_sum: term list -> term
    15   val dest_sum: term -> term list
    16   val mk_bal: term * term -> term
    17   val dest_bal: term -> term * term
    18   (*rules*)
    19   val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    20   val norm_tac: simpset -> tactic            (*AC0 etc.*)
    21   val uncancel_tac: cterm -> tactic          (*apply A ~~ B  ==  x + A ~~ x + B*)
    22 end;
    23 
    24 signature CANCEL_SUMS =
    25 sig
    26   val proc: simpset -> term -> thm option
    27 end;
    28 
    29 
    30 functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS =
    31 struct
    32 
    33 
    34 (* cancel *)
    35 
    36 fun cons1 x (xs, y, z) = (x :: xs, y, z);
    37 fun cons2 y (x, ys, z) = (x, y :: ys, z);
    38 fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
    39 
    40 (*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*)
    41 fun cancel ts [] vs = (ts, [], vs)
    42   | cancel [] us vs = ([], us, vs)
    43   | cancel (t :: ts) (u :: us) vs =
    44       (case Term_Ord.term_ord (t, u) of
    45         EQUAL => cancel ts us (t :: vs)
    46       | LESS => cons1 t (cancel ts (u :: us) vs)
    47       | GREATER => cons2 u (cancel (t :: ts) us vs));
    48 
    49 
    50 (* uncancel *)
    51 
    52 fun uncancel_sums_tac _ [] = all_tac
    53   | uncancel_sums_tac thy (t :: ts) =
    54       Data.uncancel_tac (Thm.cterm_of thy t) THEN
    55       uncancel_sums_tac thy ts;
    56 
    57 
    58 (* the simplification procedure *)
    59 
    60 fun proc ss t =
    61   (case try Data.dest_bal t of
    62     NONE => NONE
    63   | SOME bal =>
    64       let
    65         val thy = ProofContext.theory_of (Simplifier.the_context ss);
    66         val (ts, us) = pairself (sort Term_Ord.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 thy vs) Data.norm_tac ss
    72             (t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
    73       end);
    74 
    75 end;