author | wenzelm |
Fri, 03 Aug 2007 16:28:22 +0200 | |
changeset 24143 | 90a9a6fe0d01 |
parent 20044 | 92cc2f4c7335 |
child 29269 | 5c25a2012975 |
permissions | -rw-r--r-- |
(* Title: Provers/Arith/cancel_sums.ML ID: $Id$ 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); fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z); (*symmetric difference of multisets -- assumed to be sorted wrt. Logic.term_ord*) fun cancel ts [] vs = (ts, [], vs) | cancel [] us vs = ([], us, vs) | cancel (t :: ts) (u :: us) vs = (case Term.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.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;