author | clasohm |
Thu, 01 Jun 1995 13:25:06 +0200 | |
changeset 1141 | a94c0ab9a3ed |
parent 1137 | 1a768988f8e3 |
child 1221 | 19dde7bfcd07 |
permissions | -rw-r--r-- |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
1 |
(* Title: Pure/Thy/thm_database.ML |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
3 |
Author: Carsten Clasohm |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
4 |
Copyright 1995 TU Muenchen |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
5 |
*) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
6 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
7 |
signature THMDB = |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
8 |
sig |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
9 |
type thm_db_type |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
10 |
|
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
11 |
val thm_db: thm_db_type |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
12 |
val store_thm_db: string * thm -> thm |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
13 |
val thms_containing: string list -> (string * thm) list |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
14 |
(*val thms_resolving_with: term * Sign.sg -> (string * thm) list*) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
15 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
16 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
17 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
18 |
functor ThmdbFUN(val ignore: string list): THMDB = |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
19 |
(*ignore: constants that must not be used for theorem indexing*) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
20 |
struct |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
21 |
|
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
22 |
type thm_db_type = (int * ((int * (string * thm)) list) Symtab.table) ref; |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
23 |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
24 |
(*Symtab which associates a constant with a list of theorems that contain the |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
25 |
constant (theorems are represented as numbers)*) |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
26 |
val thm_db = ref (0, |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
27 |
(Symtab.make ([] : (string * ((int * (string * thm)) list)) list))); |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
28 |
(*number of next theorem and symtab containing theorems*) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
29 |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
30 |
(*list all relevant constants a term contains*) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
31 |
fun list_consts t = |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
32 |
let fun consts (Const (c, _)) = if c mem ignore then [] else [c] |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
33 |
| consts (Free _) = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
34 |
| consts (Var _) = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
35 |
| consts (Bound _) = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
36 |
| consts (Abs (_, _, t)) = consts t |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
37 |
| consts (t1$t2) = (consts t1) union (consts t2); |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
38 |
in distinct (consts t) end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
39 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
40 |
(*store a theorem in database*) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
41 |
fun store_thm_db (named_thm as (name, t)) = |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
42 |
let val {prop, hyps, ...} = rep_thm t; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
43 |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
44 |
val consts = distinct (flat (map list_consts (prop :: hyps))); |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
45 |
|
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
46 |
val (num, db) = !thm_db; |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
47 |
|
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
48 |
val tagged_thm = (num + 1, named_thm); |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
49 |
|
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
50 |
fun update_db [] result = result |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
51 |
| update_db (c :: cs) result = |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
52 |
let val old_thms = Symtab.lookup_multi (result, c); |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
53 |
in update_db cs (Symtab.update ((c, tagged_thm :: old_thms), |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
54 |
result)) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
55 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
56 |
in if consts = [] then writeln ("Warning: Theorem " ^ name ^ |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
57 |
" cannot be stored in ThmDB\n\t because it \ |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
58 |
\contains no or only ignored constants.") |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
59 |
else (); |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
60 |
thm_db := (num+1, update_db consts db); |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
61 |
t |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
62 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
63 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
64 |
(*intersection of two descending theorem lists*) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
65 |
infix desc_inter; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
66 |
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
67 |
| xs desc_inter [] = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
68 |
| (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) = |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
69 |
if xi = yi then x :: (xs desc_inter ys) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
70 |
else if xi > yi then xs desc_inter yss |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
71 |
else xss desc_inter ys; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
72 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
73 |
(*get all theorems from database that contain a list of constants*) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
74 |
fun thms_containing constants = |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
75 |
let fun collect [] _ result = map snd result |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
76 |
| collect (c :: cs) first result = |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
77 |
let val new_thms = Symtab.lookup_multi (snd (!thm_db), c); |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
78 |
in collect cs false (if first then new_thms |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
79 |
else (result desc_inter new_thms)) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
80 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
81 |
|
1134 | 82 |
val look_for = constants \\ ignore; |
83 |
in if null look_for then |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
84 |
error ("No or only ignored constants were specified for theorem \ |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
85 |
\database search:\n " ^ commas (map quote ignore)) |
1134 | 86 |
else (); |
87 |
collect look_for true [] end; |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
88 |
|
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
89 |
(*This will probably be changed or removed: |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
90 |
(*get all theorems which can be unified with term t*) |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
91 |
fun thms_unifying_with(t:term, signt:Sign.sg, thms:(string*thm) list) = |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
92 |
let val maxt = maxidx_of_term t |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
93 |
fun select((named_thm as (name,thm))::thms,sels) = |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
94 |
let val {prop,maxidx,sign,...} = rep_thm thm |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
95 |
val u = Logic.incr_indexes([],maxidx+1) t |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
96 |
val env = Envir.empty(max[maxt,maxidx]+1) |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
97 |
val seq = Unify.unifiers(sign,env,[(u,prop)]) |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
98 |
in select(thms, |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
99 |
if Sign.subsig(signt,sign) |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
100 |
then case Sequence.pull(seq) of |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
101 |
None => sels |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
102 |
| Some _ => named_thm::sels |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
103 |
else sels) |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
104 |
end |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
105 |
| select([],sels) = sels |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
106 |
in select(thms,[]) end; |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
107 |
|
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
108 |
(*get all theorems which resolve to a given term*) |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
109 |
fun thms_resolving_with (t, sg) = |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
110 |
let val thms = thms_containing (list_consts t); |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
111 |
in thms_unifying_with (t, sg, thms) end; |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
112 |
*) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
113 |
end; |