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