4291

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


2 
ID: $Id$


3 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen


4 


5 
Cancel common summands of balanced expressions:


6 


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


8 


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


10 
*)


11 


12 
signature CANCEL_SUMS_DATA =


13 
sig


14 
(*abstract syntax*)


15 
val mk_sum: term list > term


16 
val dest_sum: term > term list


17 
val mk_bal: term * term > term


18 
val dest_bal: term > term * term


19 
(*rules*)


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


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


22 
val uncancel_tac: cterm > tactic (*apply A ~~ B == x + A ~~ x + B*)


23 
end;


24 


25 
signature CANCEL_SUMS =


26 
sig


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


28 
end;


29 


30 


31 
functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS =


32 
struct


33 


34 


35 
(* cancel *)


36 


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


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


39 
fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);


40 


41 
(*symmetric difference of multisets  assumed to be sorted wrt. Logic.termord*)


42 
fun cancel ts [] vs = (ts, [], vs)


43 
 cancel [] us vs = ([], us, vs)


44 
 cancel (t :: ts) (u :: us) vs =


45 
(case Logic.termord (t, u) of


46 
EQUAL =>


47 
if t aconv u then cancel ts us (t :: vs)


48 
else cons12 t u (cancel ts us vs)


49 
(*potential incompleteness!  termord not strictly antisymmetric*)


50 
 LESS => cons1 t (cancel ts (u :: us) vs)


51 
 GREATER => cons2 u (cancel (t :: ts) us vs));


52 


53 


54 
(* uncancel *)


55 


56 
fun uncancel_sums_tac _ [] = all_tac


57 
 uncancel_sums_tac sg (t :: ts) =


58 
Data.uncancel_tac (Thm.cterm_of sg t) THEN


59 
uncancel_sums_tac sg ts;


60 


61 


62 
(* the simplification procedure *)


63 


64 
fun proc sg _ t =


65 
(case try Data.dest_bal t of


66 
None => None


67 
 Some bal =>


68 
let


69 
val (ts, us) = pairself (sort Logic.termless o Data.dest_sum) bal;


70 
val (ts', us', vs) = cancel ts us [];


71 
in


72 
if null vs then None


73 
else Some


74 
(Data.prove_conv (uncancel_sums_tac sg vs) Data.norm_tac sg


75 
(t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))


76 
end);


77 


78 


79 
end;
