1 (* Title: Provers/Arith/inverse_fold.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2000 University of Cambridge |
|
5 |
|
6 For things like (i + #m + j) - #n == #(m-n) + i + j (n<m) |
|
7 == i + j - #(n-m) (m<n) |
|
8 |
|
9 and maybe (i * #m * j) div #n == #(m div n) * i * j (n divides m) |
|
10 |
|
11 This simproc is needed for cancel_numerals.ML |
|
12 *) |
|
13 |
|
14 |
|
15 signature INVERSE_FOLD_DATA = |
|
16 sig |
|
17 (*abstract syntax*) |
|
18 val mk_numeral: int -> term |
|
19 val dest_numeral: term -> int |
|
20 val find_first_numeral: term list -> int * term * term list |
|
21 val mk_sum: term list -> term |
|
22 val dest_sum: term -> term list |
|
23 val mk_diff: term * term -> term |
|
24 val dest_diff: term -> term * term |
|
25 (*rules*) |
|
26 val double_diff_eq: thm |
|
27 val move_diff_eq: thm |
|
28 (*proof tools*) |
|
29 val prove_conv: tactic list -> Sign.sg -> term * term -> thm option |
|
30 val add_norm_tac: tactic |
|
31 val numeral_simp_tac: thm list -> tactic |
|
32 end; |
|
33 |
|
34 |
|
35 functor InverseFoldFun(Data: INVERSE_FOLD_DATA): |
|
36 sig |
|
37 val proc: Sign.sg -> thm list -> term -> thm option |
|
38 end |
|
39 = |
|
40 struct |
|
41 |
|
42 fun proc sg _ t = |
|
43 let val (sum,lit_n) = Data.dest_diff t |
|
44 val terms = Data.dest_sum sum |
|
45 val (m, lit_m, terms') = Data.find_first_numeral terms |
|
46 val n = Data.dest_numeral lit_n |
|
47 and sum' = Data.mk_sum terms' |
|
48 val assocs = (*If needed, rewrite the literal m to the front: |
|
49 i + #m + j + k == #m + i + (j + k) *) |
|
50 [the (Data.prove_conv [Data.add_norm_tac] sg |
|
51 (sum, Data.mk_sum [lit_m, sum']))] |
|
52 handle _ => [] |
|
53 in |
|
54 if m < n then |
|
55 Data.prove_conv |
|
56 [Data.numeral_simp_tac (Data.double_diff_eq::assocs)] sg |
|
57 (t, Data.mk_diff (sum', Data.mk_numeral (n-m))) |
|
58 else (*n < m, since equality would have been cancelled*) |
|
59 Data.prove_conv |
|
60 [Data.numeral_simp_tac (Data.move_diff_eq::assocs)] sg |
|
61 (t, Data.mk_sum [Data.mk_numeral (m-n), sum']) |
|
62 end |
|
63 handle _ => None; |
|
64 |
|
65 end; |
|