author | nipkow |
Fri, 18 Aug 1995 12:28:02 +0200 | |
changeset 1230 | 87e29e18e970 |
parent 1221 | 19dde7bfcd07 |
child 1236 | b54d51df9065 |
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$ |
1221 | 3 |
Author: Carsten Clasohm and Tobias Nipkow |
1132
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 |
1221 | 14 |
val findI: int -> (string * thm)list |
15 |
val findEs: int -> (string * thm)list |
|
16 |
val findE: int -> int -> (string * thm)list |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
17 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
18 |
|
1221 | 19 |
functor ThmDBFun(): THMDB = |
20 |
struct |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
21 |
|
1221 | 22 |
(*** ignore and top_const could be turned into functor-parameters, but are |
23 |
currently identical for all object logics ***) |
|
24 |
||
25 |
(* Constants not to be used for theorem indexing *) |
|
26 |
val ignore = ["Trueprop", "all", "==>", "=="]; |
|
27 |
||
28 |
(* top_const: main constant, ignoring Trueprop *) |
|
29 |
fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c |
|
30 |
| _ => None); |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
31 |
|
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
32 |
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
|
33 |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
34 |
(*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
|
35 |
constant (theorems are represented as numbers)*) |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
36 |
val thm_db = ref (0, |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
37 |
(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
|
38 |
(*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
|
39 |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
40 |
(*list all relevant constants a term contains*) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
41 |
fun list_consts t = |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
42 |
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
|
43 |
| consts (Free _) = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
44 |
| consts (Var _) = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
45 |
| consts (Bound _) = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
46 |
| consts (Abs (_, _, t)) = consts t |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
47 |
| consts (t1$t2) = (consts t1) union (consts t2); |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
48 |
in distinct (consts t) end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
49 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
50 |
(*store a theorem in database*) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
51 |
fun store_thm_db (named_thm as (name, t)) = |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
52 |
let val {prop, hyps, ...} = rep_thm t; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
53 |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
54 |
val consts = distinct (flat (map list_consts (prop :: hyps))); |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
55 |
|
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
56 |
val (num, db) = !thm_db; |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
57 |
|
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
58 |
val tagged_thm = (num + 1, named_thm); |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
59 |
|
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
60 |
fun update_db [] result = result |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
61 |
| update_db (c :: cs) result = |
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
result)) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
65 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
66 |
in if consts = [] then writeln ("Warning: Theorem " ^ name ^ |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
67 |
" cannot be stored in ThmDB\n\t because it \ |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
68 |
\contains no or only ignored constants.") |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
69 |
else (); |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
70 |
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
|
71 |
t |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
72 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
73 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
74 |
(*intersection of two descending theorem lists*) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
75 |
infix desc_inter; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
76 |
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
|
77 |
| xs desc_inter [] = [] |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
78 |
| (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
|
79 |
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
|
80 |
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
|
81 |
else xss desc_inter ys; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
82 |
|
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
83 |
(*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
|
84 |
fun thms_containing constants = |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
85 |
let fun collect [] _ result = map snd result |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
86 |
| collect (c :: cs) first result = |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset
|
87 |
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
|
88 |
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
|
89 |
else (result desc_inter new_thms)) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
90 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
91 |
|
1134 | 92 |
val look_for = constants \\ ignore; |
93 |
in if null look_for then |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
94 |
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
|
95 |
\database search:\n " ^ commas (map quote ignore)) |
1134 | 96 |
else (); |
97 |
collect look_for true [] end; |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
98 |
|
1221 | 99 |
val intro_const = top_const o concl_of; |
100 |
||
101 |
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p); |
|
102 |
||
103 |
(* In case faster access is necessary, the thm db should provide special |
|
104 |
functions |
|
105 |
||
106 |
index_intros, index_elims: string -> (string * thm) list |
|
107 |
||
108 |
where thm [| A1 ; ...; An |] ==> B is returned by |
|
109 |
- index_intros c if B is of the form c t1 ... tn |
|
110 |
- index_elims c if A1 is of the form c t1 ... tn |
|
111 |
*) |
|
112 |
||
113 |
(* could be provided by thm db *) |
|
114 |
fun index_intros c = |
|
115 |
let fun topc(_,thm) = intro_const thm = Some(c); |
|
116 |
val named_thms = thms_containing [c] |
|
117 |
in filter topc named_thms end; |
|
118 |
||
119 |
(* could be provided by thm db *) |
|
120 |
fun index_elims c = |
|
121 |
let fun topc(_,thm) = elim_const thm = Some(c); |
|
122 |
val named_thms = thms_containing [c] |
|
123 |
in filter topc named_thms end; |
|
124 |
||
125 |
(*assume that parameters have unique names*) |
|
126 |
fun goal_params i = |
|
127 |
let val gi = getgoal i |
|
128 |
val frees = map Free (Logic.strip_params gi) |
|
129 |
in (gi,frees) end; |
|
130 |
||
131 |
fun concl_of_goal i = |
|
132 |
let val (gi,frees) = goal_params i |
|
133 |
val B = Logic.strip_assums_concl gi |
|
134 |
in subst_bounds(frees,B) end; |
|
135 |
||
136 |
fun prems_of_goal i = |
|
137 |
let val (gi,frees) = goal_params i |
|
138 |
val As = Logic.strip_assums_hyp gi |
|
139 |
in map (fn A => subst_bounds(frees,A)) As end; |
|
140 |
||
141 |
fun select_match(obj,signobj,named_thms,extract) = |
|
142 |
let fun matches(prop,tsig) = |
|
143 |
case extract prop of |
|
144 |
None => false |
|
145 |
| Some pat => Pattern.matches tsig (pat,obj); |
|
146 |
||
147 |
fun select((p as (_,thm))::named_thms,sels) = |
|
148 |
let val {prop,sign,...} = rep_thm thm |
|
149 |
in select(named_thms, |
|
150 |
if Sign.subsig(sign,signobj) andalso |
|
1230 | 151 |
matches(prop,#tsig(Sign.rep_sg signobj)) |
1221 | 152 |
then p::sels else sels) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
153 |
end |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
154 |
| select([],sels) = sels |
1221 | 155 |
|
156 |
in select(named_thms,[]) end; |
|
157 |
||
158 |
fun find_matching(prop,sign,index,extract) = |
|
159 |
(case top_const prop of |
|
160 |
Some c => select_match(prop,sign,index c,extract) |
|
161 |
| _ => []); |
|
162 |
||
163 |
fun find_intros(prop,sign) = |
|
164 |
find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl); |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
165 |
|
1221 | 166 |
fun find_elims sign prop = |
167 |
let fun major prop = case Logic.strip_imp_prems prop of |
|
168 |
[] => None | p::_ => Some p |
|
169 |
in find_matching(prop,sign,index_elims,major) end; |
|
170 |
||
171 |
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm()))); |
|
172 |
||
173 |
fun findEs i = |
|
1230 | 174 |
let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2); |
175 |
val sign = #sign(rep_thm(topthm())) |
|
176 |
val thmss = map (find_elims sign) (prems_of_goal i) |
|
177 |
in foldl (gen_union eq_nth) ([],thmss) end; |
|
1221 | 178 |
|
179 |
fun findE i j = |
|
180 |
let val sign = #sign(rep_thm(topthm())) |
|
181 |
in find_elims sign (nth_elem(j-1, prems_of_goal i)) end; |
|
182 |
||
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
183 |
end; |