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 

4346

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

4291

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


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


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

4452

45 
(case Term.term_ord (t, u) of

4346

46 
EQUAL => cancel ts us (t :: vs)

4291

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


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


49 


50 


51 
(* uncancel *)


52 


53 
fun uncancel_sums_tac _ [] = all_tac


54 
 uncancel_sums_tac sg (t :: ts) =


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


56 
uncancel_sums_tac sg ts;


57 


58 


59 
(* the simplification procedure *)


60 


61 
fun proc sg _ t =


62 
(case try Data.dest_bal t of


63 
None => None


64 
 Some bal =>


65 
let

4452

66 
val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;

4291

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


68 
in


69 
if null vs then None


70 
else Some


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


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


73 
end);


74 


75 


76 
end;
