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

8779

40 
val subst_tac: thm option > tactic

8760

41 
val norm_tac: tactic


42 
val numeral_simp_tac: tactic

8736

43 
end;


44 


45 

8760

46 
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):


47 
sig


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


49 
end


50 
=

8736

51 
struct


52 

8779

53 
(*For t = #n*u then put u in the table*)

8760

54 
fun update_by_coeff (tab, t) =

8779

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

8760

56 


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


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


59 
fun find_common (terms1,terms2) =


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


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


62 
 seek (t::terms) =


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


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


65 
else seek terms


66 
end


67 
in seek terms1 end;

8736

68 


69 
(*the simplification procedure*)


70 
fun proc sg _ t =


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

8760

72 
val terms1 = Data.dest_sum t1


73 
and terms2 = Data.dest_sum t2


74 
val u = find_common (terms1,terms2)


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


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


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

8779

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


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

8772

80 
if n1=0 orelse n2=0 then (*trivial, so do nothing*)


81 
raise TERM("cancel_numerals", [])

8779

82 
else Data.prove_conv [Data.norm_tac] sg

8772

83 
(t,


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

8779

85 
newshape(n2,terms2')))

8736

86 
in

8760

87 


88 
if n2<=n1 then


89 
Data.prove_conv

8779

90 
[Data.subst_tac reshape, rtac Data.bal_add1 1,

8760

91 
Data.numeral_simp_tac] sg


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


93 
else


94 
Data.prove_conv

8779

95 
[Data.subst_tac reshape, rtac Data.bal_add2 1,

8760

96 
Data.numeral_simp_tac] sg


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

8736

98 
end

8779

99 
handle TERM _ => None


100 
 TYPE _ => None; (*Typically (if thy doesn't include Numeral)


101 
Undeclared type constructor "Numeral.bin"*)

8736

102 


103 
end;
