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