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