author | paulson |
Fri, 17 Jul 1998 10:50:28 +0200 | |
changeset 5155 | 21177b8a4d7f |
parent 5090 | 75ac9b451ae0 |
child 5346 | bc9748ad8491 |
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 |
|
3627 | 8 |
signature THM_DATABASE = |
4023 | 9 |
sig |
10 |
val store_thm: string * thm -> thm |
|
11 |
val qed_thm: thm option ref |
|
12 |
val bind_thm: string * thm -> unit |
|
13 |
val qed: string -> unit |
|
14 |
val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
|
15 |
val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit |
|
16 |
(*these peek at the proof state!*) |
|
4287 | 17 |
val thms_containing: xstring list -> (string * thm) list |
4023 | 18 |
val findI: int -> (string * thm) list |
19 |
val findEs: int -> (string * thm) list |
|
20 |
val findE: int -> int -> (string * thm) list |
|
21 |
end; |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
22 |
|
3627 | 23 |
structure ThmDatabase: THM_DATABASE = |
1221 | 24 |
struct |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
25 |
|
4023 | 26 |
(** store theorems **) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
27 |
|
4023 | 28 |
(* store in theory and generate HTML *) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
29 |
|
4023 | 30 |
fun store_thm (name, thm) = |
31 |
let val thm' = PureThy.smart_store_thm (name, thm) in |
|
32 |
BrowserInfo.thm_to_html thm' name; thm' |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
33 |
end; |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
34 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
35 |
|
4023 | 36 |
(* store on ML toplevel *) |
37 |
||
38 |
val qed_thm: thm option ref = ref None; |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
39 |
|
4023 | 40 |
val ml_reserved = |
41 |
["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", |
|
42 |
"end", "exception", "fn", "fun", "handle", "if", "in", "infix", |
|
43 |
"infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", |
|
44 |
"raise", "rec", "then", "type", "val", "with", "withtype", "while", |
|
45 |
"eqtype", "functor", "include", "sharing", "sig", "signature", |
|
46 |
"struct", "structure", "where"]; |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
47 |
|
4023 | 48 |
fun is_ml_identifier name = |
49 |
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
|
50 |
|
4023 | 51 |
fun ml_store_thm (name, thm) = |
52 |
let val thm' = store_thm (name, thm) in |
|
53 |
if is_ml_identifier name then |
|
54 |
(qed_thm := Some thm'; |
|
5090 | 55 |
use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);")) |
4023 | 56 |
else warning ("Cannot bind thm " ^ quote name ^ " as ML value") |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
57 |
end; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
58 |
|
4023 | 59 |
fun bind_thm (name, thm) = ml_store_thm (name, standard thm); |
60 |
fun qed name = ml_store_thm (name, result ()); |
|
61 |
fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf); |
|
62 |
fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf); |
|
63 |
||
64 |
||
65 |
||
4037 | 66 |
(** retrieve theorems **) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
67 |
|
4037 | 68 |
(*get theorems that contain all of given constants*) |
4023 | 69 |
fun thms_containing raw_consts = |
70 |
let |
|
71 |
val sign = sign_of_thm (topthm ()); |
|
72 |
val consts = map (Sign.intern_const sign) raw_consts; |
|
73 |
val thy = ThyInfo.theory_of_sign sign; |
|
4037 | 74 |
in PureThy.thms_containing thy consts end; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
75 |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
76 |
|
4023 | 77 |
(*top_const: main constant, ignoring Trueprop*) |
78 |
fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None) |
|
79 |
| top_const _ = None; |
|
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
80 |
|
1221 | 81 |
val intro_const = top_const o concl_of; |
82 |
||
4023 | 83 |
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p; |
1221 | 84 |
|
85 |
(* In case faster access is necessary, the thm db should provide special |
|
86 |
functions |
|
87 |
||
88 |
index_intros, index_elims: string -> (string * thm) list |
|
89 |
||
90 |
where thm [| A1 ; ...; An |] ==> B is returned by |
|
91 |
- index_intros c if B is of the form c t1 ... tn |
|
92 |
- index_elims c if A1 is of the form c t1 ... tn |
|
93 |
*) |
|
94 |
||
95 |
(* could be provided by thm db *) |
|
96 |
fun index_intros c = |
|
97 |
let fun topc(_,thm) = intro_const thm = Some(c); |
|
98 |
val named_thms = thms_containing [c] |
|
99 |
in filter topc named_thms end; |
|
100 |
||
101 |
(* could be provided by thm db *) |
|
102 |
fun index_elims c = |
|
103 |
let fun topc(_,thm) = elim_const thm = Some(c); |
|
104 |
val named_thms = thms_containing [c] |
|
105 |
in filter topc named_thms end; |
|
106 |
||
107 |
(*assume that parameters have unique names*) |
|
108 |
fun goal_params i = |
|
109 |
let val gi = getgoal i |
|
110 |
val frees = map Free (Logic.strip_params gi) |
|
111 |
in (gi,frees) end; |
|
112 |
||
113 |
fun concl_of_goal i = |
|
114 |
let val (gi,frees) = goal_params i |
|
115 |
val B = Logic.strip_assums_concl gi |
|
116 |
in subst_bounds(frees,B) end; |
|
117 |
||
118 |
fun prems_of_goal i = |
|
119 |
let val (gi,frees) = goal_params i |
|
120 |
val As = Logic.strip_assums_hyp gi |
|
121 |
in map (fn A => subst_bounds(frees,A)) As end; |
|
122 |
||
5155 | 123 |
(*returns all those named_thms whose subterm extracted by extract can be |
124 |
instantiated to obj; the list is sorted according to the number of premises |
|
125 |
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
|
126 |
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
|
127 |
let fun matches(prop, tsig) = |
1221 | 128 |
case extract prop of |
129 |
None => false |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
130 |
| Some pat => Pattern.matches tsig (pat, obj); |
1221 | 131 |
|
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
132 |
fun substsize(prop, tsig) = |
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
133 |
let val Some pat = extract prop |
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
134 |
val (_,subst) = Pattern.match tsig (pat,obj) |
2150 | 135 |
in foldl op+ |
136 |
(0, map (fn (_,t) => size_of_term t) subst) |
|
137 |
end |
|
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
138 |
|
4546 | 139 |
fun thm_ord ((p0,s0,_),(p1,s1,_)) = |
140 |
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
|
141 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
142 |
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
|
143 |
let val {prop, sign, ...} = rep_thm thm |
1221 | 144 |
in select(named_thms, |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
145 |
if Sign.subsig(sign, signobj) andalso |
1230 | 146 |
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
|
147 |
then |
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
148 |
(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels |
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset
|
149 |
else sels) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
150 |
end |
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
151 |
| select([],sels) = sels |
1221 | 152 |
|
4546 | 153 |
in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; |
1221 | 154 |
|
155 |
fun find_matching(prop,sign,index,extract) = |
|
156 |
(case top_const prop of |
|
157 |
Some c => select_match(prop,sign,index c,extract) |
|
158 |
| _ => []); |
|
159 |
||
160 |
fun find_intros(prop,sign) = |
|
161 |
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
|
162 |
|
1221 | 163 |
fun find_elims sign prop = |
164 |
let fun major prop = case Logic.strip_imp_prems prop of |
|
165 |
[] => None | p::_ => Some p |
|
166 |
in find_matching(prop,sign,index_elims,major) end; |
|
167 |
||
168 |
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm()))); |
|
169 |
||
170 |
fun findEs i = |
|
1230 | 171 |
let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2); |
172 |
val sign = #sign(rep_thm(topthm())) |
|
173 |
val thmss = map (find_elims sign) (prems_of_goal i) |
|
174 |
in foldl (gen_union eq_nth) ([],thmss) end; |
|
1221 | 175 |
|
176 |
fun findE i j = |
|
177 |
let val sign = #sign(rep_thm(topthm())) |
|
178 |
in find_elims sign (nth_elem(j-1, prems_of_goal i)) end; |
|
179 |
||
3601
43c7912aac8d
Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
berghofe
parents:
2150
diff
changeset
|
180 |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
181 |
end; |