author | haftmann |
Sat, 17 Sep 2011 15:08:55 +0200 | |
changeset 44947 | 8ae418dfe561 |
parent 43594 | ef1ddc59b825 |
child 51717 | 9e7d1c139569 |
permissions | -rw-r--r-- |
13516 | 1 |
(* Title: Provers/Arith/cancel_div_mod.ML |
2 |
Author: Tobias Nipkow, TU Muenchen |
|
3 |
||
4 |
Cancel div and mod terms: |
|
5 |
||
6 |
A + n*(m div n) + B + (m mod n) + C == A + B + C + m |
|
7 |
||
22997 | 8 |
FIXME: Is parameterized but assumes for simplicity that + and * are named |
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
33049
diff
changeset
|
9 |
as in HOL |
13516 | 10 |
*) |
11 |
||
12 |
signature CANCEL_DIV_MOD_DATA = |
|
13 |
sig |
|
14 |
(*abstract syntax*) |
|
15 |
val div_name: string |
|
16 |
val mod_name: string |
|
17 |
val mk_binop: string -> term * term -> term |
|
18 |
val mk_sum: term list -> term |
|
19 |
val dest_sum: term -> term list |
|
20 |
(*logic*) |
|
21 |
val div_mod_eqs: thm list |
|
22 |
(* (n*(m div n) + m mod n) + k == m + k and |
|
23 |
((m div n)*n + m mod n) + k == m + k *) |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19233
diff
changeset
|
24 |
val prove_eq_sums: simpset -> term * term -> thm |
13516 | 25 |
(* must prove ac0-equivalence of sums *) |
26 |
end; |
|
27 |
||
28 |
signature CANCEL_DIV_MOD = |
|
29 |
sig |
|
43594 | 30 |
val proc: simpset -> cterm -> thm option |
13516 | 31 |
end; |
32 |
||
33 |
||
43594 | 34 |
functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = |
13516 | 35 |
struct |
36 |
||
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
37 |
fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms = |
13516 | 38 |
coll_div_mod t (coll_div_mod s dms) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
39 |
| coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n)) |
13516 | 40 |
(dms as (divs,mods)) = |
41 |
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
42 |
| coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m) |
13516 | 43 |
(dms as (divs,mods)) = |
44 |
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms |
|
45 |
| coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) = |
|
46 |
if m = Data.mod_name then (divs,(s,n)::mods) else dms |
|
47 |
| coll_div_mod _ dms = dms; |
|
48 |
||
49 |
||
50 |
(* Proof principle: |
|
51 |
1. (...div...)+(...mod...) == (div + mod) + rest |
|
52 |
in function rearrange |
|
53 |
2. (div + mod) + ?x = d + ?x |
|
54 |
Data.div_mod_eq |
|
55 |
==> thesis by transitivity |
|
56 |
*) |
|
57 |
||
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
58 |
val mk_plus = Data.mk_binop @{const_name Groups.plus}; |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
59 |
val mk_times = Data.mk_binop @{const_name Groups.times}; |
13516 | 60 |
|
61 |
fun rearrange t pq = |
|
62 |
let val ts = Data.dest_sum t; |
|
63 |
val dpq = Data.mk_binop Data.div_name pq |
|
64 |
val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq) |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
35267
diff
changeset
|
65 |
val d = if member (op =) ts d1 then d1 else d2 |
13516 | 66 |
val m = Data.mk_binop Data.mod_name pq |
33040 | 67 |
in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end |
13516 | 68 |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19233
diff
changeset
|
69 |
fun cancel ss t pq = |
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19233
diff
changeset
|
70 |
let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq) |
30937 | 71 |
in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end; |
13516 | 72 |
|
43594 | 73 |
fun proc ss ct = |
74 |
let |
|
75 |
val t = term_of ct; |
|
76 |
val (divs, mods) = coll_div_mod t ([], []); |
|
77 |
in |
|
78 |
if null divs orelse null mods then NONE |
|
79 |
else |
|
80 |
(case inter (op =) mods divs of |
|
81 |
pq :: _ => SOME (cancel ss t pq) |
|
82 |
| [] => NONE) |
|
83 |
end; |
|
13516 | 84 |
|
17613 | 85 |
end |