author | wenzelm |
Fri, 03 Aug 2007 16:28:22 +0200 | |
changeset 24143 | 90a9a6fe0d01 |
parent 23261 | 85f27f79232f |
child 24630 | 351a308ab58d |
permissions | -rw-r--r-- |
(* Title: Provers/Arith/cancel_factor.ML ID: $Id$ Author: Markus Wenzel and Stefan Berghofer, TU Muenchen Cancel common constant factor from balanced exression (e.g. =, <=, < of sums). *) signature CANCEL_FACTOR_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 -> tactic -> Proof.context -> term * term -> thm val norm_tac: tactic (*AC0 etc.*) val multiply_tac: integer -> tactic (*apply a ~~ b == k * a ~~ k * b (for k > 0)*) end; signature CANCEL_FACTOR = sig val proc: simpset -> term -> thm option end; functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR = struct (* count terms *) fun ins_term (t, []) = [(t, 1)] | ins_term (t, (u, k) :: uks) = if t aconv u then (u, k + 1) :: uks else (t, 1) :: (u, k) :: uks; fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []); (* divide sum *) fun div_sum d = Data.mk_sum o maps (fn (t, k) => replicate (k div d) t); (* the simplification procedure *) fun proc ss t = (case try Data.dest_bal t of NONE => NONE | SOME bal => (case pairself Data.dest_sum bal of ([_], _) => NONE | (_, [_]) => NONE | ts_us => let val (tks, uks) = pairself count_terms ts_us; val d = 0 |> fold (Integer.gcd o snd) tks |> fold (Integer.gcd o snd) uks; val d' = Integer.machine_int d; in if d = 0 orelse d = 1 then NONE else SOME (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss) (t, Data.mk_bal (div_sum d' tks, div_sum d' uks))) end)); end;