8760

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

8736

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 2000 University of Cambridge


5 

8760

6 
Cancel common coefficients in balanced expressions:

8736

7 

8760

8 
i + #m*u + j ~~ i' + #m'*u + j' == #(mm')*u + i + j ~~ i' + j'

8736

9 


10 
where ~~ is an appropriate balancing operation (e.g. =, <=, <, ).

8760

11 


12 
It works by (a) massaging both sides to bring the selected term to the front:


13 


14 
#m*u + (i + j) ~~ #m'*u + (i' + j')


15 


16 
(b) then using bal_add1 or bal_add2 to reach


17 


18 
#(mm')*u + i + j ~~ i' + j' (if m'<=m)


19 


20 
or


21 


22 
i + j ~~ #(m'm)*u + i' + j' (otherwise)

8736

23 
*)


24 


25 
signature CANCEL_NUMERALS_DATA =


26 
sig


27 
(*abstract syntax*)


28 
val mk_sum: term list > term


29 
val dest_sum: term > term list


30 
val mk_bal: term * term > term


31 
val dest_bal: term > term * term

8760

32 
val mk_coeff: int * term > term


33 
val dest_coeff: term > int * term


34 
val find_first_coeff: term > term list > int * term list


35 
(*rules*)


36 
val bal_add1: thm


37 
val bal_add2: thm

8736

38 
(*proof tools*)


39 
val prove_conv: tactic list > Sign.sg > term * term > thm option

8760

40 
val norm_tac: tactic


41 
val numeral_simp_tac: tactic

8736

42 
end;


43 


44 

8760

45 
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):


46 
sig


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


48 
end


49 
=

8736

50 
struct


51 

8760

52 
fun listof None = []


53 
 listof (Some x) = [x];


54 


55 
(*If t = #n*u then put u in the table*)


56 
fun update_by_coeff (tab, t) =


57 
Termtab.update ((#2 (Data.dest_coeff t), ()), tab)


58 
handle TERM _ => tab;


59 


60 
(*a lefttoright scan of terms1, seeking a term of the form #n*u, where


61 
#m*u is in terms2 for some m*)


62 
fun find_common (terms1,terms2) =


63 
let val tab2 = foldl update_by_coeff (Termtab.empty, terms2)


64 
fun seek [] = raise TERM("find_common", [])


65 
 seek (t::terms) =


66 
let val (_,u) = Data.dest_coeff t


67 
in if is_some (Termtab.lookup (tab2, u)) then u


68 
else seek terms


69 
end


70 
handle TERM _ => seek terms


71 
in seek terms1 end;

8736

72 


73 
(*the simplification procedure*)


74 
fun proc sg _ t =


75 
let val (t1,t2) = Data.dest_bal t

8760

76 
val terms1 = Data.dest_sum t1


77 
and terms2 = Data.dest_sum t2


78 
val u = find_common (terms1,terms2)


79 
val (n1, terms1') = Data.find_first_coeff u terms1


80 
and (n2, terms2') = Data.find_first_coeff u terms2


81 
fun newshape (i,terms) = Data.mk_sum (Data.mk_coeff(i,u)::terms)


82 
val reshapes = (*Move i*u to the front and put j*u into standard form


83 
i + #m + j + k == #m + i + (j + k) *)


84 
listof (Data.prove_conv [Data.norm_tac] sg


85 
(t,


86 
Data.mk_bal (newshape(n1,terms1'),


87 
newshape(n2,terms2'))))

8736

88 
in

8760

89 


90 
if n2<=n1 then


91 
Data.prove_conv


92 
[rewrite_goals_tac reshapes, rtac Data.bal_add1 1,


93 
Data.numeral_simp_tac] sg


94 
(t, Data.mk_bal (newshape(n1n2,terms1'), Data.mk_sum terms2'))


95 
else


96 
Data.prove_conv


97 
[rewrite_goals_tac reshapes, rtac Data.bal_add2 1,


98 
Data.numeral_simp_tac] sg


99 
(t, Data.mk_bal (Data.mk_sum terms1', newshape(n2n1,terms2')))

8736

100 
end

8760

101 
handle TERM _ => None;

8736

102 


103 
end;
