13516

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


2 
ID: $Id$


3 
Author: Tobias Nipkow, TU Muenchen


4 


5 
Cancel div and mod terms:


6 


7 
A + n*(m div n) + B + (m mod n) + C == A + B + C + m


8 


9 
Is parameterized but assumes for simplicity that + and * are called


10 
"op +" and "op *"


11 
*)


12 


13 
signature CANCEL_DIV_MOD_DATA =


14 
sig


15 
(*abstract syntax*)


16 
val div_name: string


17 
val mod_name: string


18 
val mk_binop: string > term * term > term


19 
val mk_sum: term list > term


20 
val dest_sum: term > term list


21 
(*logic*)


22 
val div_mod_eqs: thm list


23 
(* (n*(m div n) + m mod n) + k == m + k and


24 
((m div n)*n + m mod n) + k == m + k *)


25 
val prove_eq_sums: Sign.sg > term * term > thm


26 
(* must prove ac0equivalence of sums *)


27 
end;


28 


29 
signature CANCEL_DIV_MOD =


30 
sig


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


32 
end;


33 


34 


35 
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =


36 
struct


37 


38 
fun coll_div_mod (Const("op +",_) $ s $ t) dms =


39 
coll_div_mod t (coll_div_mod s dms)


40 
 coll_div_mod (Const("op *",_) $ m $ (Const(d,_) $ s $ n))


41 
(dms as (divs,mods)) =


42 
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms


43 
 coll_div_mod (Const("op *",_) $ (Const(d,_) $ s $ n) $ m)


44 
(dms as (divs,mods)) =


45 
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms


46 
 coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =


47 
if m = Data.mod_name then (divs,(s,n)::mods) else dms


48 
 coll_div_mod _ dms = dms;


49 


50 


51 
(* Proof principle:


52 
1. (...div...)+(...mod...) == (div + mod) + rest


53 
in function rearrange


54 
2. (div + mod) + ?x = d + ?x


55 
Data.div_mod_eq


56 
==> thesis by transitivity


57 
*)


58 


59 
val mk_plus = Data.mk_binop "op +"


60 
val mk_times = Data.mk_binop "op *"


61 


62 
fun rearrange t pq =


63 
let val ts = Data.dest_sum t;


64 
val dpq = Data.mk_binop Data.div_name pq


65 
val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)


66 
val d = if d1 mem ts then d1 else d2


67 
val m = Data.mk_binop Data.mod_name pq


68 
in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end


69 


70 
fun cancel sg t pq =


71 
let val teqt' = Data.prove_eq_sums sg (t, rearrange t pq)


72 
in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;


73 


74 
fun proc sg _ t =


75 
let val (divs,mods) = coll_div_mod t ([],[])


76 
in if null divs orelse null mods then None


77 
else case divs inter mods of


78 
pq :: _ => Some(cancel sg t pq)


79 
 [] => None


80 
end


81 


82 
end 