author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 69593 | 3dda49e08b9d |
child 78800 | 0b3700d31758 |
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 |
|
66810 | 18 |
val mk_sum: typ -> term list -> term |
13516 | 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 *) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset
|
24 |
val prove_eq_sums: Proof.context -> term * term -> thm |
13516 | 25 |
(* must prove ac0-equivalence of sums *) |
26 |
end; |
|
27 |
||
28 |
signature CANCEL_DIV_MOD = |
|
29 |
sig |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset
|
30 |
val proc: Proof.context -> 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 |
||
69593 | 37 |
fun coll_div_mod (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ s $ t) dms = |
13516 | 38 |
coll_div_mod t (coll_div_mod s dms) |
69593 | 39 |
| coll_div_mod (Const (\<^const_name>\<open>Groups.times\<close>, _) $ m $ (Const (d, _) $ s $ n)) |
66810 | 40 |
(dms as (divs, mods)) = |
41 |
if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms |
|
69593 | 42 |
| coll_div_mod (Const (\<^const_name>\<open>Groups.times\<close>, _) $ (Const (d, _) $ s $ n) $ m) |
66810 | 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 |
|
13516 | 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 |
||
69593 | 58 |
val mk_plus = Data.mk_binop \<^const_name>\<open>Groups.plus\<close>; |
59 |
val mk_times = Data.mk_binop \<^const_name>\<open>Groups.times\<close>; |
|
13516 | 60 |
|
66810 | 61 |
fun rearrange T t pq = |
62 |
let |
|
63 |
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 member (op =) ts d1 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 T (ts |> remove (op =) d |> remove (op =) m)) end |
|
13516 | 69 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset
|
70 |
fun cancel ctxt t pq = |
66810 | 71 |
let |
72 |
val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq); |
|
30937 | 73 |
in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end; |
13516 | 74 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset
|
75 |
fun proc ctxt ct = |
43594 | 76 |
let |
59582 | 77 |
val t = Thm.term_of ct; |
43594 | 78 |
val (divs, mods) = coll_div_mod t ([], []); |
79 |
in |
|
80 |
if null divs orelse null mods then NONE |
|
81 |
else |
|
82 |
(case inter (op =) mods divs of |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset
|
83 |
pq :: _ => SOME (cancel ctxt t pq) |
43594 | 84 |
| [] => NONE) |
85 |
end; |
|
13516 | 86 |
|
17613 | 87 |
end |