author | skalberg |
Sun, 13 Feb 2005 17:15:14 +0100 | |
changeset 15531 | 08c8dad8e399 |
parent 11869 | 66d4f20eb3fc |
permissions | -rw-r--r-- |
11869
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
1 |
(* Title: Provers/Arith/abstract_numerals.ML |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
4 |
Copyright 2001 University of Cambridge |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
5 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
6 |
Simproc to extend simplification of numeric literals to cover abstract 0 and |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
7 |
1. For example, in the two-operand case, it eliminates the need to declare |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
8 |
separate rules for the 9 combinations of 0, 1, numeral. Given a term, it |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
9 |
replaces all abstract 0s and 1s by the corresponding numerals. |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
10 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
11 |
The resulting equality should immediately be combined with an equation to |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
12 |
force numerical evaluation, since otherwise the literal 0s and 1s will |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
13 |
probably be written back to their abstract forms. |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
14 |
*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
15 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
16 |
signature ABSTRACT_NUMERALS_DATA = |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
17 |
sig |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
18 |
(*abstract syntax*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
19 |
val dest_eq: thm -> term * term |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
20 |
val is_numeral: term -> bool |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
21 |
(*rules*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
22 |
val numeral_0_eq_0: thm |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
23 |
val numeral_1_eq_1: thm |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
24 |
(*proof tools*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
25 |
val prove_conv: tactic list -> Sign.sg -> term * term -> thm option |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
26 |
val norm_tac: thm list -> tactic (*proves the initial lemma*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
27 |
val simplify_meta_eq: thm -> thm -> thm (*simplifies the final theorem*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
28 |
end; |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
29 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
30 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
31 |
(*The returned simproc requires as its first argument a theorem |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
32 |
of the form f(number_of x, ...) = ...x... *) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
33 |
functor AbstractNumeralsFun(Data: ABSTRACT_NUMERALS_DATA): |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
34 |
sig |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
35 |
val proc: thm -> Sign.sg -> thm list -> term -> thm option |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
36 |
end |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
37 |
= |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
38 |
struct |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
39 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
40 |
val (numeral0, abstract0) = Data.dest_eq Data.numeral_0_eq_0 |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
41 |
val (numeral1, abstract1) = Data.dest_eq Data.numeral_1_eq_1 |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
42 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
43 |
(*convert abstract numbers to numerals, leave other numerals alone, |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
44 |
reject other terms*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
45 |
fun convert x = |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
46 |
if Data.is_numeral x then x |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
47 |
else if x = abstract0 then numeral0 |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
48 |
else if x = abstract1 then numeral1 |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
49 |
else raise TERM("abstract_numerals", []) ; |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
50 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
51 |
(*the simplification procedure*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
52 |
fun proc f_number_of_eq sg _ t = |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
53 |
let val (f,args) = strip_comb t |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
54 |
val t' = list_comb(f, map convert args) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
55 |
in |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
56 |
if t aconv t' then (*trivial, so do nothing*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
57 |
raise TERM("abstract_numerals", []) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
58 |
else |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
59 |
apsome (Data.simplify_meta_eq f_number_of_eq) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
60 |
(Data.prove_conv |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
61 |
[Data.norm_tac [Data.numeral_0_eq_0, Data.numeral_1_eq_1]] sg |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
62 |
(t, t')) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
63 |
end |
15531 | 64 |
handle TERM _ => NONE |
65 |
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
|
11869
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
66 |
Undeclared type constructor "Numeral.bin"*) |
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
67 |
|
66d4f20eb3fc
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
paulson
parents:
diff
changeset
|
68 |
end; |