author | nipkow |
Tue, 07 Dec 1999 11:01:48 +0100 | |
changeset 8049 | 61eea7c23c5b |
parent 7854 | fe7b7e3c3ddc |
child 10894 | ce58d2de6ea8 |
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$ |
4023 | 3 |
Author: Carsten Clasohm and Tobias Nipkow and Markus Wenzel, TU Muenchen |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
4 |
|
4023 | 5 |
User level interface to thm database (see also Pure/pure_thy.ML). |
6 |
*) |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
7 |
|
6204 | 8 |
signature BASIC_THM_DATABASE = |
4023 | 9 |
sig |
10 |
val store_thm: string * thm -> thm |
|
7410 | 11 |
val store_thms: string * thm list -> thm list |
4023 | 12 |
val bind_thm: string * thm -> unit |
7410 | 13 |
val bind_thms: string * thm list -> unit |
4023 | 14 |
val qed: string -> unit |
15 |
val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
|
16 |
val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit |
|
7446 | 17 |
val no_qed: unit -> unit |
4023 | 18 |
(*these peek at the proof state!*) |
4287 | 19 |
val thms_containing: xstring list -> (string * thm) list |
4023 | 20 |
val findI: int -> (string * thm) list |
21 |
val findEs: int -> (string * thm) list |
|
22 |
val findE: int -> int -> (string * thm) list |
|
23 |
end; |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
24 |
|
6204 | 25 |
signature THM_DATABASE = |
26 |
sig |
|
27 |
include BASIC_THM_DATABASE |
|
7410 | 28 |
val qed_thms: thm list ref |
6204 | 29 |
val ml_store_thm: string * thm -> unit |
7410 | 30 |
val ml_store_thms: string * thm list -> unit |
6204 | 31 |
val is_ml_identifier: string -> bool |
7609 | 32 |
val print_thms_containing: theory -> xstring list -> unit |
6204 | 33 |
end; |
34 |
||
3627 | 35 |
structure ThmDatabase: THM_DATABASE = |
1221 | 36 |
struct |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
37 |
|
4023 | 38 |
(** store theorems **) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
39 |
|
4023 | 40 |
(* store in theory and generate HTML *) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
41 |
|
4023 | 42 |
fun store_thm (name, thm) = |
7410 | 43 |
let val thm' = hd (PureThy.smart_store_thms (name, [thm])) |
6327 | 44 |
in Present.theorem name thm'; thm' end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
45 |
|
7410 | 46 |
fun store_thms (name, thms) = |
47 |
let val thms' = PureThy.smart_store_thms (name, thms) |
|
48 |
in Present.theorems name thms'; thms' end; |
|
49 |
||
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
50 |
|
4023 | 51 |
(* store on ML toplevel *) |
52 |
||
7410 | 53 |
val qed_thms: thm list ref = ref []; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
54 |
|
4023 | 55 |
val ml_reserved = |
56 |
["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", |
|
57 |
"end", "exception", "fn", "fun", "handle", "if", "in", "infix", |
|
58 |
"infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", |
|
59 |
"raise", "rec", "then", "type", "val", "with", "withtype", "while", |
|
60 |
"eqtype", "functor", "include", "sharing", "sig", "signature", |
|
61 |
"struct", "structure", "where"]; |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
62 |
|
4023 | 63 |
fun is_ml_identifier name = |
64 |
Syntax.is_identifier name andalso not (name mem ml_reserved); |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
65 |
|
7410 | 66 |
fun warn_ml name = |
67 |
if is_ml_identifier name then false |
|
7573 | 68 |
else if name = "" then true |
7410 | 69 |
else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
70 |
||
7854 | 71 |
val use_text_verbose = use_text writeln true; |
72 |
||
4023 | 73 |
fun ml_store_thm (name, thm) = |
74 |
let val thm' = store_thm (name, thm) in |
|
7410 | 75 |
if warn_ml name then () |
7854 | 76 |
else (qed_thms := [thm']; use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")) |
7410 | 77 |
end; |
78 |
||
79 |
fun ml_store_thms (name, thms) = |
|
80 |
let val thms' = store_thms (name, thms) in |
|
81 |
if warn_ml name then () |
|
7854 | 82 |
else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
83 |
end; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
84 |
|
4023 | 85 |
fun bind_thm (name, thm) = ml_store_thm (name, standard thm); |
7410 | 86 |
fun bind_thms (name, thms) = ml_store_thms (name, map standard thms); |
7446 | 87 |
|
7410 | 88 |
fun qed name = ml_store_thm (name, Goals.result ()); |
4023 | 89 |
fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf); |
90 |
fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf); |
|
91 |
||
7446 | 92 |
fun no_qed () = (); |
93 |
||
4023 | 94 |
|
95 |
||
4037 | 96 |
(** retrieve theorems **) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
97 |
|
4037 | 98 |
(*get theorems that contain all of given constants*) |
7609 | 99 |
fun thms_containing_thy thy raw_consts = |
100 |
let val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts; |
|
7182
090723b5024d
now catches exn THEORY and prints an error message
paulson
parents:
6327
diff
changeset
|
101 |
in PureThy.thms_containing thy consts end |
090723b5024d
now catches exn THEORY and prints an error message
paulson
parents:
6327
diff
changeset
|
102 |
handle THEORY (msg,_) => error msg; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
103 |
|
7609 | 104 |
fun thms_containing cs = |
105 |
thms_containing_thy (ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()))) cs; |
|
106 |
||
107 |
fun prt_thm (a, th) = |
|
108 |
Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, |
|
109 |
Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))]; |
|
110 |
||
111 |
fun print_thms_containing thy cs = |
|
112 |
Pretty.writeln (Pretty.blk (0, Pretty.fbreaks (map prt_thm (thms_containing_thy thy cs)))); |
|
113 |
||
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
114 |
|
4023 | 115 |
(*top_const: main constant, ignoring Trueprop*) |
116 |
fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None) |
|
117 |
| top_const _ = None; |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
118 |
|
1221 | 119 |
val intro_const = top_const o concl_of; |
120 |
||
4023 | 121 |
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p; |
1221 | 122 |
|
123 |
(* In case faster access is necessary, the thm db should provide special |
|
124 |
functions |
|
125 |
||
126 |
index_intros, index_elims: string -> (string * thm) list |
|
127 |
||
128 |
where thm [| A1 ; ...; An |] ==> B is returned by |
|
129 |
- index_intros c if B is of the form c t1 ... tn |
|
130 |
- index_elims c if A1 is of the form c t1 ... tn |
|
131 |
*) |
|
132 |
||
133 |
(* could be provided by thm db *) |
|
134 |
fun index_intros c = |
|
135 |
let fun topc(_,thm) = intro_const thm = Some(c); |
|
136 |
val named_thms = thms_containing [c] |
|
137 |
in filter topc named_thms end; |
|
138 |
||
139 |
(* could be provided by thm db *) |
|
140 |
fun index_elims c = |
|
141 |
let fun topc(_,thm) = elim_const thm = Some(c); |
|
142 |
val named_thms = thms_containing [c] |
|
143 |
in filter topc named_thms end; |
|
144 |
||
8049
61eea7c23c5b
Fixed bug in find-functions: list of parameters must be reversed before
nipkow
parents:
7854
diff
changeset
|
145 |
(*assume that parameters have unique names; reverse them for substitution*) |
1221 | 146 |
fun goal_params i = |
147 |
let val gi = getgoal i |
|
8049
61eea7c23c5b
Fixed bug in find-functions: list of parameters must be reversed before
nipkow
parents:
7854
diff
changeset
|
148 |
val rfrees = rev(map Free (Logic.strip_params gi)) |
61eea7c23c5b
Fixed bug in find-functions: list of parameters must be reversed before
nipkow
parents:
7854
diff
changeset
|
149 |
in (gi,rfrees) end; |
1221 | 150 |
|
151 |
fun concl_of_goal i = |
|
8049
61eea7c23c5b
Fixed bug in find-functions: list of parameters must be reversed before
nipkow
parents:
7854
diff
changeset
|
152 |
let val (gi,rfrees) = goal_params i |
1221 | 153 |
val B = Logic.strip_assums_concl gi |
8049
61eea7c23c5b
Fixed bug in find-functions: list of parameters must be reversed before
nipkow
parents:
7854
diff
changeset
|
154 |
in subst_bounds(rfrees,B) end; |
1221 | 155 |
|
156 |
fun prems_of_goal i = |
|
8049
61eea7c23c5b
Fixed bug in find-functions: list of parameters must be reversed before
nipkow
parents:
7854
diff
changeset
|
157 |
let val (gi,rfrees) = goal_params i |
1221 | 158 |
val As = Logic.strip_assums_hyp gi |
8049
61eea7c23c5b
Fixed bug in find-functions: list of parameters must be reversed before
nipkow
parents:
7854
diff
changeset
|
159 |
in map (fn A => subst_bounds(rfrees,A)) As end; |
1221 | 160 |
|
5155 | 161 |
(*returns all those named_thms whose subterm extracted by extract can be |
162 |
instantiated to obj; the list is sorted according to the number of premises |
|
163 |
and the size of the required substitution.*) |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
164 |
fun select_match(obj, signobj, named_thms, extract) = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
165 |
let fun matches(prop, tsig) = |
1221 | 166 |
case extract prop of |
167 |
None => false |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
168 |
| Some pat => Pattern.matches tsig (pat, obj); |
1221 | 169 |
|
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
170 |
fun substsize(prop, tsig) = |
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
171 |
let val Some pat = extract prop |
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
172 |
val (_,subst) = Pattern.match tsig (pat,obj) |
2150 | 173 |
in foldl op+ |
7410 | 174 |
(0, map (fn (_,t) => size_of_term t) subst) |
2150 | 175 |
end |
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
176 |
|
4546 | 177 |
fun thm_ord ((p0,s0,_),(p1,s1,_)) = |
178 |
prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1)); |
|
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
179 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
180 |
fun select((p as (_,thm))::named_thms, sels) = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
181 |
let val {prop, sign, ...} = rep_thm thm |
1221 | 182 |
in select(named_thms, |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
183 |
if Sign.subsig(sign, signobj) andalso |
1230 | 184 |
matches(prop,#tsig(Sign.rep_sg signobj)) |
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
185 |
then |
7410 | 186 |
(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels |
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
187 |
else sels) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
188 |
end |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
189 |
| select([],sels) = sels |
1221 | 190 |
|
7410 | 191 |
in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; |
1221 | 192 |
|
193 |
fun find_matching(prop,sign,index,extract) = |
|
194 |
(case top_const prop of |
|
195 |
Some c => select_match(prop,sign,index c,extract) |
|
196 |
| _ => []); |
|
197 |
||
198 |
fun find_intros(prop,sign) = |
|
199 |
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
|
200 |
|
1221 | 201 |
fun find_elims sign prop = |
202 |
let fun major prop = case Logic.strip_imp_prems prop of |
|
203 |
[] => None | p::_ => Some p |
|
204 |
in find_matching(prop,sign,index_elims,major) end; |
|
205 |
||
206 |
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm()))); |
|
207 |
||
208 |
fun findEs i = |
|
1230 | 209 |
let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2); |
210 |
val sign = #sign(rep_thm(topthm())) |
|
211 |
val thmss = map (find_elims sign) (prems_of_goal i) |
|
212 |
in foldl (gen_union eq_nth) ([],thmss) end; |
|
1221 | 213 |
|
214 |
fun findE i j = |
|
215 |
let val sign = #sign(rep_thm(topthm())) |
|
216 |
in find_elims sign (nth_elem(j-1, prems_of_goal i)) end; |
|
217 |
||
3601
43c7912aac8d
Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
berghofe
parents:
2150
diff
changeset
|
218 |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
219 |
end; |
6204 | 220 |
|
221 |
||
222 |
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase; |
|
223 |
open BasicThmDatabase; |