src/Provers/Arith/cancel_sums.ML
author wenzelm
Wed, 31 Dec 2008 15:30:10 +0100
changeset 29269 5c25a2012975
parent 20044 92cc2f4c7335
child 35408 b48ab741683b
permissions -rw-r--r--
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     1
(*  Title:      Provers/Arith/cancel_sums.ML
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     3
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     4
Cancel common summands of balanced expressions:
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     5
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     6
  A + x + B ~~ A' + x + B'  ==  A + B ~~ A' + B'
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     7
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     8
where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, -).
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
     9
*)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    10
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    11
signature CANCEL_SUMS_DATA =
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    12
sig
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    13
  (*abstract syntax*)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    14
  val mk_sum: term list -> term
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    15
  val dest_sum: term -> term list
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    16
  val mk_bal: term * term -> term
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    17
  val dest_bal: term -> term * term
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    18
  (*rules*)
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17613
diff changeset
    19
  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
17613
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    20
  val norm_tac: simpset -> tactic            (*AC0 etc.*)
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    21
  val uncancel_tac: cterm -> tactic          (*apply A ~~ B  ==  x + A ~~ x + B*)
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    22
end;
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    23
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    24
signature CANCEL_SUMS =
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    25
sig
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17613
diff changeset
    26
  val proc: simpset -> term -> thm option
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    27
end;
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    28
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    29
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    30
functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS =
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    31
struct
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    32
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    33
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    34
(* cancel *)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    35
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    36
fun cons1 x (xs, y, z) = (x :: xs, y, z);
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    37
fun cons2 y (x, ys, z) = (x, y :: ys, z);
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    38
fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    39
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 20044
diff changeset
    40
(*symmetric difference of multisets -- assumed to be sorted wrt. TermOrd.term_ord*)
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    41
fun cancel ts [] vs = (ts, [], vs)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    42
  | cancel [] us vs = ([], us, vs)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    43
  | cancel (t :: ts) (u :: us) vs =
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 20044
diff changeset
    44
      (case TermOrd.term_ord (t, u) of
4346
15fab62268c3 adapted to new term order;
wenzelm
parents: 4291
diff changeset
    45
        EQUAL => cancel ts us (t :: vs)
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    46
      | LESS => cons1 t (cancel ts (u :: us) vs)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    47
      | GREATER => cons2 u (cancel (t :: ts) us vs));
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    48
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    49
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    50
(* uncancel *)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    51
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    52
fun uncancel_sums_tac _ [] = all_tac
17613
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    53
  | uncancel_sums_tac thy (t :: ts) =
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    54
      Data.uncancel_tac (Thm.cterm_of thy t) THEN
072c21e31b42 Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    55
      uncancel_sums_tac thy ts;
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    56
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    57
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    58
(* the simplification procedure *)
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    59
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17613
diff changeset
    60
fun proc ss t =
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    61
  (case try Data.dest_bal t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    62
    NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    63
  | SOME bal =>
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    64
      let
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17613
diff changeset
    65
        val thy = ProofContext.theory_of (Simplifier.the_context ss);
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 20044
diff changeset
    66
        val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal;
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    67
        val (ts', us', vs) = cancel ts us [];
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    68
      in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    69
        if null vs then NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    70
        else SOME
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17613
diff changeset
    71
          (Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss
4291
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    72
            (t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    73
      end);
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    74
6e13b5427de0 Cancel common summands of balanced expressions.
wenzelm
parents:
diff changeset
    75
end;