4 |
4 |
5 Cancel div and mod terms: |
5 Cancel div and mod terms: |
6 |
6 |
7 A + n*(m div n) + B + (m mod n) + C == A + B + C + m |
7 A + n*(m div n) + B + (m mod n) + C == A + B + C + m |
8 |
8 |
9 Is parameterized but assumes for simplicity that + and * are called |
9 FIXME: Is parameterized but assumes for simplicity that + and * are called |
10 "op +" and "op *" |
10 "HOL.plus" and "HOL.minus" |
11 *) |
11 *) |
12 |
12 |
13 signature CANCEL_DIV_MOD_DATA = |
13 signature CANCEL_DIV_MOD_DATA = |
14 sig |
14 sig |
15 (*abstract syntax*) |
15 (*abstract syntax*) |
33 |
33 |
34 |
34 |
35 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = |
35 functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = |
36 struct |
36 struct |
37 |
37 |
38 fun coll_div_mod (Const("op +",_) $ s $ t) dms = |
38 fun coll_div_mod (Const("HOL.plus",_) $ s $ t) dms = |
39 coll_div_mod t (coll_div_mod s dms) |
39 coll_div_mod t (coll_div_mod s dms) |
40 | coll_div_mod (Const("op *",_) $ m $ (Const(d,_) $ s $ n)) |
40 | coll_div_mod (Const("HOL.times",_) $ m $ (Const(d,_) $ s $ n)) |
41 (dms as (divs,mods)) = |
41 (dms as (divs,mods)) = |
42 if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms |
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) |
43 | coll_div_mod (Const("HOL.times",_) $ (Const(d,_) $ s $ n) $ m) |
44 (dms as (divs,mods)) = |
44 (dms as (divs,mods)) = |
45 if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms |
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)) = |
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 |
47 if m = Data.mod_name then (divs,(s,n)::mods) else dms |
48 | coll_div_mod _ dms = dms; |
48 | coll_div_mod _ dms = dms; |
54 2. (div + mod) + ?x = d + ?x |
54 2. (div + mod) + ?x = d + ?x |
55 Data.div_mod_eq |
55 Data.div_mod_eq |
56 ==> thesis by transitivity |
56 ==> thesis by transitivity |
57 *) |
57 *) |
58 |
58 |
59 val mk_plus = Data.mk_binop "op +" |
59 val mk_plus = Data.mk_binop "HOL.plus" |
60 val mk_times = Data.mk_binop "op *" |
60 val mk_times = Data.mk_binop "HOL.times" |
61 |
61 |
62 fun rearrange t pq = |
62 fun rearrange t pq = |
63 let val ts = Data.dest_sum t; |
63 let val ts = Data.dest_sum t; |
64 val dpq = Data.mk_binop Data.div_name pq |
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) |
65 val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq) |