author | paulson |
Fri, 05 May 2000 17:49:54 +0200 | |
changeset 8799 | 89e9deef4bcb |
parent 8774 | ad5026ff0c16 |
child 8816 | 31b4fb3d8d60 |
permissions | -rw-r--r-- |
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
1 |
(* Title: Provers/Arith/combine_numerals.ML |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
4 |
Copyright 2000 University of Cambridge |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
5 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
6 |
Combine coefficients in expressions: |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
7 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
8 |
i + #m*u + j ... + #n*u + k == #(m+n)*u + (i + (j + k)) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
9 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
10 |
It works by (a) massaging the sum to bring the selected terms to the front: |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
11 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
12 |
#m*u + (#n*u + (i + (j + k))) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
13 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
14 |
(b) then using left_distrib to reach |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
15 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
16 |
#(m+n)*u + (i + (j + k)) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
17 |
*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
18 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
19 |
signature COMBINE_NUMERALS_DATA = |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
20 |
sig |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
21 |
(*abstract syntax*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
22 |
val mk_sum: term list -> term |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
23 |
val dest_sum: term -> term list |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
24 |
val mk_coeff: int * term -> term |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
25 |
val dest_coeff: term -> int * term |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
26 |
(*rules*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
27 |
val left_distrib: thm |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
28 |
(*proof tools*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
29 |
val prove_conv: tactic list -> Sign.sg -> term * term -> thm option |
8799 | 30 |
val trans_tac: thm option -> tactic (*applies the initial lemma*) |
31 |
val norm_tac: tactic (*proves the initial lemma*) |
|
32 |
val numeral_simp_tac: tactic (*proves the final theorem*) |
|
33 |
val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) |
|
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
34 |
end; |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
35 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
36 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
37 |
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
38 |
sig |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
39 |
val proc: Sign.sg -> thm list -> term -> thm option |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
40 |
end |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
41 |
= |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
42 |
struct |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
43 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
44 |
fun listof None = [] |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
45 |
| listof (Some x) = [x]; |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
46 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
47 |
(*Remove the first occurrence of #m*u from the term list*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
48 |
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
49 |
raise TERM("combine_numerals: remove", []) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
50 |
| remove (m, u, t::terms) = |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
51 |
let val (n,v) = Data.dest_coeff t |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
52 |
in if m=n andalso u aconv v then terms |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
53 |
else t :: remove (m, u, terms) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
54 |
end; |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
55 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
56 |
(*a left-to-right scan of terms, seeking another term of the form #n*u, where |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
57 |
#m*u is already in terms for some m*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
58 |
fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
59 |
| find_repeated (tab, past, t::terms) = |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
60 |
let val (n,u) = Data.dest_coeff t |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
61 |
in |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
62 |
case Termtab.lookup (tab, u) of |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
63 |
Some m => (u, m, n, rev (remove (m,u,past)) @ terms) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
64 |
| None => find_repeated (Termtab.update ((u,n), tab), |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
65 |
t::past, terms) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
66 |
end; |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
67 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
68 |
(*the simplification procedure*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
69 |
fun proc sg _ t = |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
70 |
let val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
71 |
val reshape = (*Move i*u to the front and put j*u into standard form |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
72 |
i + #m + j + k == #m + i + (j + k) *) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
73 |
if m=0 orelse n=0 then (*trivial, so do nothing*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
74 |
raise TERM("combine_numerals", []) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
75 |
else Data.prove_conv [Data.norm_tac] sg |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
76 |
(t, |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
77 |
Data.mk_sum ([Data.mk_coeff(m,u), |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
78 |
Data.mk_coeff(n,u)] @ terms)) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
79 |
in |
8799 | 80 |
apsome Data.simplify_meta_eq |
81 |
(Data.prove_conv |
|
82 |
[Data.trans_tac reshape, rtac Data.left_distrib 1, |
|
83 |
Data.numeral_simp_tac] sg |
|
84 |
(t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms))) |
|
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
85 |
end |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
86 |
handle TERM _ => None |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
87 |
| TYPE _ => None; (*Typically (if thy doesn't include Numeral) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
88 |
Undeclared type constructor "Numeral.bin"*) |
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
89 |
|
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset
|
90 |
end; |