4292

1 
(* Title: Provers/Arith/cancel_factor.ML


2 
ID: $Id$


3 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen


4 


5 
Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).


6 
*)


7 


8 
signature CANCEL_FACTOR_DATA =


9 
sig


10 
(*abstract syntax*)


11 
val mk_sum: term list > term


12 
val dest_sum: term > term list


13 
val mk_bal: term * term > term


14 
val dest_bal: term > term * term


15 
(*rules*)


16 
val prove_conv: tactic > tactic > Sign.sg > term * term > thm


17 
val norm_tac: tactic (*AC0 etc.*)


18 
val multiply_tac: int > tactic (*apply a ~~ b == k * a ~~ k * b (for k > 0)*)


19 
end;


20 


21 
signature CANCEL_FACTOR =


22 
sig


23 
val proc: Sign.sg > thm list > term > thm option


24 
end;


25 


26 


27 
functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR =


28 
struct


29 


30 


31 
(* greatest common divisor *)


32 


33 
fun gcd (0, n) = n


34 
 gcd (m, n) = gcd (n mod m, m);


35 


36 
val gcds = foldl gcd;


37 


38 


39 
(* count terms *)


40 


41 
fun ins_term (t, []) = [(t, 1)]


42 
 ins_term (t, (u, k) :: uks) =


43 
if t aconv u then (u, k + 1) :: uks


44 
else (t, 1) :: (u, k) :: uks;


45 

4452

46 
fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);

4292

47 


48 


49 
(* divide sum *)


50 


51 
fun div_sum d tks =


52 
Data.mk_sum (flat (map (fn (t, k) => replicate (k div d) t) tks));


53 


54 


55 
(* the simplification procedure *)


56 


57 
fun proc sg _ t =


58 
(case try Data.dest_bal t of


59 
None => None


60 
 Some bal =>


61 
(case pairself Data.dest_sum bal of


62 
([_], _) => None


63 
 (_, [_]) => None


64 
 ts_us =>


65 
let


66 
val (tks, uks) = pairself count_terms ts_us;


67 
val d = gcds (gcds (0, map snd tks), map snd uks);


68 
in


69 
if d = 0 orelse d = 1 then None


70 
else Some


71 
(Data.prove_conv (Data.multiply_tac d) Data.norm_tac sg


72 
(t, Data.mk_bal (div_sum d tks, div_sum d uks)))


73 
end));


74 


75 


76 
end;
