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 ac0-equivalence of sums *)
|
|
27 |
end;
|
|
28 |
|
|
29 |
signature CANCEL_DIV_MOD =
|
|
30 |
sig
|
15027
|
31 |
val proc: Sign.sg -> simpset -> term -> thm option
|
13516
|
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 ([],[])
|
15531
|
76 |
in if null divs orelse null mods then NONE
|
13516
|
77 |
else case divs inter mods of
|
15531
|
78 |
pq :: _ => SOME(cancel sg t pq)
|
|
79 |
| [] => NONE
|
13516
|
80 |
end
|
|
81 |
|
|
82 |
end |