src/Provers/Arith/cancel_sums.ML
 author blanchet Tue, 07 Dec 2010 11:56:01 +0100 changeset 41051 2ed1b971fc20 parent 38052 04a8de29e8f7 child 42361 23f352990944 permissions -rw-r--r--
give the inner timeout mechanism a chance, since it gives more precise information to the user
```
(*  Title:      Provers/Arith/cancel_sums.ML
Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen

Cancel common summands of balanced expressions:

A + x + B ~~ A' + x + B'  ==  A + B ~~ A' + B'

where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, -).
*)

signature CANCEL_SUMS_DATA =
sig
(*abstract syntax*)
val mk_sum: term list -> term
val dest_sum: term -> term list
val mk_bal: term * term -> term
val dest_bal: term -> term * term
(*rules*)
val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
val norm_tac: simpset -> tactic            (*AC0 etc.*)
val uncancel_tac: cterm -> tactic          (*apply A ~~ B  ==  x + A ~~ x + B*)
end;

signature CANCEL_SUMS =
sig
val proc: simpset -> term -> thm option
end;

functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS =
struct

(* cancel *)

fun cons1 x (xs, y, z) = (x :: xs, y, z);
fun cons2 y (x, ys, z) = (x, y :: ys, z);

(*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*)
fun cancel ts [] vs = (ts, [], vs)
| cancel [] us vs = ([], us, vs)
| cancel (t :: ts) (u :: us) vs =
(case Term_Ord.term_ord (t, u) of
EQUAL => cancel ts us (t :: vs)
| LESS => cons1 t (cancel ts (u :: us) vs)
| GREATER => cons2 u (cancel (t :: ts) us vs));

(* uncancel *)

fun uncancel_sums_tac _ [] = all_tac
| uncancel_sums_tac thy (t :: ts) =
Data.uncancel_tac (Thm.cterm_of thy t) THEN
uncancel_sums_tac thy ts;

(* the simplification procedure *)

fun proc ss t =
(case try Data.dest_bal t of
NONE => NONE
| SOME bal =>
let
val thy = ProofContext.theory_of (Simplifier.the_context ss);
val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal;
val (ts', us', vs) = cancel ts us [];
in
if null vs then NONE
else SOME
(Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss
(t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
end);

end;
```