5819
|
1 |
(* Title: Pure/Isar/proof_context.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Proof context information.
|
|
6 |
|
|
7 |
TODO:
|
|
8 |
- pretty_bind: use syntax (!?) (show_types etc.);
|
|
9 |
- smash_unifiers: ever invents new vars (???);
|
|
10 |
*)
|
|
11 |
|
|
12 |
(* FIXME tmp *)
|
|
13 |
val proof_debug = ref false;
|
|
14 |
|
|
15 |
signature PROOF_CONTEXT =
|
|
16 |
sig
|
|
17 |
type context
|
|
18 |
exception CONTEXT of string * context
|
|
19 |
val theory_of: context -> theory
|
|
20 |
val sign_of: context -> Sign.sg
|
|
21 |
val print_binds: context -> unit
|
|
22 |
val print_thms: context -> unit
|
|
23 |
val print_context: context -> unit
|
|
24 |
val print_proof_data: theory -> unit
|
5874
|
25 |
val init: theory -> context
|
5819
|
26 |
val read_typ: context -> string -> typ
|
|
27 |
val cert_typ: context -> typ -> typ
|
5874
|
28 |
val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
|
5819
|
29 |
val read_term: context -> string -> term
|
|
30 |
val read_prop: context -> string -> term
|
|
31 |
val read_pat: context -> string -> term
|
|
32 |
val cert_term: context -> term -> term
|
|
33 |
val cert_prop: context -> term -> term
|
|
34 |
val declare_term: term -> context -> context
|
|
35 |
val declare_terms: term list -> context -> context
|
5874
|
36 |
val declare_thm: thm -> context -> context
|
5819
|
37 |
val add_binds: (indexname * string) list -> context -> context
|
|
38 |
val add_binds_i: (indexname * term) list -> context -> context
|
|
39 |
val match_binds: (string * string) list -> context -> context
|
|
40 |
val match_binds_i: (term * term) list -> context -> context
|
|
41 |
val thms_closure: context -> xstring -> tthm list option
|
|
42 |
val get_tthm: context -> string -> tthm
|
|
43 |
val get_tthms: context -> string -> tthm list
|
|
44 |
val get_tthmss: context -> string list -> tthm list
|
|
45 |
val put_tthm: string * tthm -> context -> context
|
|
46 |
val put_tthms: string * tthm list -> context -> context
|
|
47 |
val put_tthmss: (string * tthm list) list -> context -> context
|
|
48 |
val have_tthms: string -> context attribute list
|
|
49 |
-> (tthm * context attribute list) list -> context -> context * (string * tthm list)
|
|
50 |
val assumptions: context -> tthm list
|
|
51 |
val fixed_names: context -> string list
|
|
52 |
val assume: string -> context attribute list -> string list -> context
|
|
53 |
-> context * (string * tthm list)
|
|
54 |
val assume_i: string -> context attribute list -> term list -> context
|
|
55 |
-> context * (string * tthm list)
|
|
56 |
val fix: (string * string option) list -> context -> context
|
|
57 |
val fix_i: (string * typ) list -> context -> context
|
|
58 |
val setup: (theory -> theory) list
|
|
59 |
end;
|
|
60 |
|
|
61 |
signature PROOF_CONTEXT_PRIVATE =
|
|
62 |
sig
|
|
63 |
include PROOF_CONTEXT
|
|
64 |
val init_data: Object.kind -> (theory -> Object.T) * (context -> Object.T -> unit)
|
|
65 |
-> theory -> theory
|
|
66 |
val print_data: Object.kind -> context -> unit
|
|
67 |
val get_data: Object.kind -> (Object.T -> 'a) -> context -> 'a
|
|
68 |
val put_data: Object.kind -> ('a -> Object.T) -> 'a -> context -> context
|
|
69 |
end;
|
|
70 |
|
|
71 |
structure ProofContext: PROOF_CONTEXT_PRIVATE =
|
|
72 |
struct
|
|
73 |
|
|
74 |
|
|
75 |
(** datatype context **)
|
|
76 |
|
|
77 |
datatype context =
|
|
78 |
Context of
|
|
79 |
{thy: theory, (*current theory*)
|
|
80 |
data: Object.T Symtab.table, (*user data*)
|
|
81 |
asms:
|
|
82 |
(string * tthm list) list * (*assumes: A ==> _*)
|
|
83 |
((string * string) list * string list), (*fixes: !!x. _*)
|
|
84 |
binds: (term * typ) Vartab.table, (*term bindings*)
|
|
85 |
thms: tthm list Symtab.table, (*local thms*)
|
|
86 |
defs:
|
|
87 |
typ Vartab.table * (*type constraints*)
|
|
88 |
sort Vartab.table * (*default sorts*)
|
|
89 |
int * (*maxidx*)
|
|
90 |
string list}; (*used type variable names*)
|
|
91 |
|
|
92 |
exception CONTEXT of string * context;
|
|
93 |
|
|
94 |
|
|
95 |
fun make_context (thy, data, asms, binds, thms, defs) =
|
|
96 |
Context {thy = thy, data = data, asms = asms, binds = binds, thms = thms, defs = defs};
|
|
97 |
|
|
98 |
fun map_context f (Context {thy, data, asms, binds, thms, defs}) =
|
|
99 |
make_context (f (thy, data, asms, binds, thms, defs));
|
|
100 |
|
|
101 |
fun theory_of (Context {thy, ...}) = thy;
|
|
102 |
val sign_of = Theory.sign_of o theory_of;
|
|
103 |
|
|
104 |
|
|
105 |
|
|
106 |
(** print context information **)
|
|
107 |
|
|
108 |
(* FIXME tmp*)
|
|
109 |
fun debug f x = if ! proof_debug then f x else ();
|
|
110 |
|
|
111 |
fun print_items prt name items =
|
|
112 |
let
|
|
113 |
fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
|
|
114 |
| pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs);
|
|
115 |
in Pretty.writeln (Pretty.big_list name (map pretty_itms items)) end;
|
|
116 |
|
|
117 |
|
|
118 |
(* term bindings *)
|
|
119 |
|
|
120 |
fun print_binds (Context {thy, binds, ...}) =
|
|
121 |
let
|
|
122 |
val prt_term = Sign.pretty_term (Theory.sign_of thy);
|
|
123 |
|
|
124 |
fun fix_var (x, i) =
|
|
125 |
(case try Syntax.dest_binding x of
|
|
126 |
None => Syntax.string_of_vname (x, i)
|
|
127 |
| Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i));
|
|
128 |
fun pretty_bind (xi, (t, T)) = Pretty.block
|
|
129 |
[Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t];
|
|
130 |
in Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds))) end;
|
|
131 |
|
|
132 |
|
|
133 |
(* local theorems *)
|
|
134 |
|
|
135 |
fun print_thms (Context {thms, ...}) =
|
|
136 |
print_items Attribute.pretty_tthm "Local theorems:" (Symtab.dest thms);
|
|
137 |
|
|
138 |
|
|
139 |
(* main context *)
|
|
140 |
|
|
141 |
fun print_context (ctxt as Context {thy, data = _, asms = (assumes, (fixes, _)), binds = _,
|
|
142 |
thms = _, defs = (types, sorts, maxidx, used)}) =
|
|
143 |
let
|
|
144 |
val sign = Theory.sign_of thy;
|
|
145 |
|
|
146 |
val term_of_tthm = #prop o Thm.rep_thm o Attribute.thm_of;
|
|
147 |
val prt_term = Sign.pretty_term sign;
|
|
148 |
val prt_typ = Sign.pretty_typ sign;
|
|
149 |
val prt_sort = Sign.pretty_sort sign;
|
|
150 |
|
|
151 |
(*theory*)
|
|
152 |
val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
|
|
153 |
|
|
154 |
(*fixes*)
|
|
155 |
fun prt_fix (x, x') = Pretty.str (x ^ " = " ^ x');
|
|
156 |
|
|
157 |
(* defaults *)
|
|
158 |
|
|
159 |
fun prt_atom prt prtT (x, X) = Pretty.block
|
|
160 |
[prt x, Pretty.str " ::", Pretty.brk 1, prtT X];
|
|
161 |
|
|
162 |
fun prt_var (x, ~1) = prt_term (Syntax.free x)
|
|
163 |
| prt_var xi = prt_term (Syntax.var xi);
|
|
164 |
|
|
165 |
fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
|
|
166 |
| prt_varT xi = prt_typ (TVar (xi, []));
|
|
167 |
|
|
168 |
val prt_defT = prt_atom prt_var prt_typ;
|
|
169 |
val prt_defS = prt_atom prt_varT prt_sort;
|
|
170 |
in
|
|
171 |
debug Pretty.writeln pretty_thy;
|
|
172 |
Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
|
|
173 |
print_items (prt_term o term_of_tthm) "Assumptions:" assumes;
|
|
174 |
debug print_binds ctxt;
|
|
175 |
debug print_thms ctxt;
|
|
176 |
debug Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
|
|
177 |
debug Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts)));
|
|
178 |
debug writeln ("Maxidx: " ^ string_of_int maxidx);
|
|
179 |
debug Pretty.writeln (Pretty.strs ("Used type variable names:" :: used))
|
|
180 |
end;
|
|
181 |
|
|
182 |
|
|
183 |
|
|
184 |
(** user data **)
|
|
185 |
|
|
186 |
(* errors *)
|
|
187 |
|
|
188 |
fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy);
|
|
189 |
|
|
190 |
fun err_inconsistent kinds =
|
|
191 |
error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
|
|
192 |
|
|
193 |
fun err_dup_init thy kind =
|
|
194 |
error ("Duplicate initialization of " ^ quote kind ^ " proof data" ^ of_theory thy);
|
|
195 |
|
|
196 |
fun err_undef ctxt kind =
|
|
197 |
raise CONTEXT ("Tried to access undefined " ^ quote kind ^ " proof data", ctxt);
|
|
198 |
|
|
199 |
fun err_uninit ctxt kind =
|
|
200 |
raise CONTEXT ("Tried to access uninitialized " ^ quote kind ^ " proof data" ^
|
|
201 |
of_theory (theory_of ctxt), ctxt);
|
|
202 |
|
|
203 |
fun err_access ctxt kind =
|
|
204 |
raise CONTEXT ("Unauthorized access to " ^ quote kind ^ " proof data" ^
|
|
205 |
of_theory (theory_of ctxt), ctxt);
|
|
206 |
|
|
207 |
|
|
208 |
(* data kind 'Isar/proof_data' *)
|
|
209 |
|
|
210 |
structure ProofDataDataArgs =
|
|
211 |
struct
|
|
212 |
val name = "Isar/proof_data";
|
|
213 |
type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
|
|
214 |
|
|
215 |
val empty = Symtab.empty;
|
|
216 |
val prep_ext = I;
|
|
217 |
fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
|
|
218 |
handle Symtab.DUPS kinds => err_inconsistent kinds;
|
|
219 |
fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
|
|
220 |
end;
|
|
221 |
|
|
222 |
structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
|
|
223 |
val print_proof_data = ProofDataData.print;
|
|
224 |
|
|
225 |
|
|
226 |
(* init proof data *)
|
|
227 |
|
|
228 |
fun init_data kind meths thy =
|
|
229 |
let
|
|
230 |
val name = Object.name_of_kind kind;
|
|
231 |
val tab = Symtab.update_new ((name, (kind, meths)), ProofDataData.get thy)
|
|
232 |
handle Symtab.DUP _ => err_dup_init thy name;
|
|
233 |
in thy |> ProofDataData.put tab end;
|
|
234 |
|
|
235 |
|
|
236 |
(* access data *)
|
|
237 |
|
|
238 |
fun lookup_data (ctxt as Context {data, ...}) kind =
|
|
239 |
let
|
|
240 |
val thy = theory_of ctxt;
|
|
241 |
val name = Object.name_of_kind kind;
|
|
242 |
in
|
|
243 |
(case Symtab.lookup (ProofDataData.get thy, name) of
|
|
244 |
Some (k, meths) =>
|
|
245 |
if Object.eq_kind (kind, k) then
|
|
246 |
(case Symtab.lookup (data, name) of
|
|
247 |
Some x => (x, meths)
|
|
248 |
| None => err_undef ctxt name)
|
|
249 |
else err_access ctxt name
|
|
250 |
| None => err_uninit ctxt name)
|
|
251 |
end;
|
|
252 |
|
|
253 |
fun get_data kind f ctxt =
|
|
254 |
let val (x, _) = lookup_data ctxt kind
|
|
255 |
in f x handle Match => Object.kind_error kind end;
|
|
256 |
|
|
257 |
fun print_data kind ctxt =
|
|
258 |
let val (x, (_, prt)) = lookup_data ctxt kind
|
|
259 |
in prt ctxt x end;
|
|
260 |
|
|
261 |
fun put_data kind f x ctxt =
|
|
262 |
(lookup_data ctxt kind;
|
|
263 |
ctxt |> map_context (fn (thy, data, asms, binds, thms, defs) =>
|
|
264 |
(thy, Symtab.update ((Object.name_of_kind kind, f x), data), asms, binds, thms, defs)));
|
|
265 |
|
|
266 |
|
|
267 |
(* init context *)
|
|
268 |
|
5874
|
269 |
fun init thy =
|
|
270 |
let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
|
5819
|
271 |
make_context (thy, data, ([], ([], [])), Vartab.empty, Symtab.empty,
|
|
272 |
(Vartab.empty, Vartab.empty, ~1, []))
|
|
273 |
end;
|
|
274 |
|
|
275 |
|
|
276 |
|
|
277 |
(** prepare types **)
|
|
278 |
|
|
279 |
fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s =
|
|
280 |
let
|
|
281 |
val sign = sign_of ctxt;
|
|
282 |
fun def_sort xi = Vartab.lookup (sorts, xi);
|
|
283 |
in
|
|
284 |
transform_error (Sign.read_typ (sign, def_sort)) s
|
|
285 |
handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)
|
|
286 |
end;
|
|
287 |
|
|
288 |
fun cert_typ ctxt raw_T =
|
|
289 |
Sign.certify_typ (sign_of ctxt) raw_T
|
|
290 |
handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
|
|
291 |
|
|
292 |
|
|
293 |
|
|
294 |
(** prepare terms and propositions **)
|
|
295 |
|
|
296 |
(*
|
|
297 |
(1) read / certify wrt. signature of context
|
|
298 |
(2) intern Skolem constants
|
|
299 |
(3) expand term bindings
|
|
300 |
*)
|
|
301 |
|
|
302 |
|
|
303 |
(* read / certify wrt. signature *) (*exception ERROR*) (*exception TERM*)
|
|
304 |
|
5874
|
305 |
fun read_def_termTs freeze sg (types, sorts, used) sTs =
|
|
306 |
let val (cts, env) = Thm.read_def_cterms (sg, types, sorts) used freeze sTs
|
|
307 |
in (map Thm.term_of cts, env) end;
|
|
308 |
|
|
309 |
fun read_def_termT freeze sg defs sT = apfst hd (read_def_termTs freeze sg defs [sT]);
|
|
310 |
|
5819
|
311 |
|
|
312 |
fun read_term_sg sg (defs as (_, _, used)) s =
|
5874
|
313 |
#1 (read_def_termT true sg defs (s, TVar ((variant used "'z", 0), logicS)));
|
5819
|
314 |
|
5874
|
315 |
fun read_prop_sg sg defs s =
|
|
316 |
#1 (read_def_termT true sg defs (s, propT));
|
5819
|
317 |
|
|
318 |
|
|
319 |
fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t);
|
|
320 |
|
|
321 |
fun cert_prop_sg sg tm =
|
|
322 |
let
|
|
323 |
val ctm = Thm.cterm_of sg tm;
|
|
324 |
val {t, T, ...} = Thm.rep_cterm ctm;
|
|
325 |
in
|
|
326 |
if T = propT then t
|
|
327 |
else raise TERM ("Term not of type prop", [t])
|
|
328 |
end;
|
|
329 |
|
|
330 |
|
|
331 |
(* intern_skolem *)
|
|
332 |
|
|
333 |
fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x);
|
|
334 |
|
|
335 |
fun check_skolem ctxt check x =
|
|
336 |
if check andalso can Syntax.dest_skolem x then
|
|
337 |
raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
|
|
338 |
else x;
|
|
339 |
|
|
340 |
fun intern_skolem ctxt check =
|
|
341 |
let
|
|
342 |
fun intern (t as Free (x, T)) =
|
|
343 |
(case get_skolem ctxt (check_skolem ctxt check x) of
|
|
344 |
Some x' => Free (x', T)
|
|
345 |
| None => t)
|
|
346 |
| intern (t $ u) = intern t $ intern u
|
|
347 |
| intern (Abs (x, T, t)) = Abs (x, T, intern t)
|
|
348 |
| intern a = a;
|
|
349 |
in intern end;
|
|
350 |
|
|
351 |
|
|
352 |
(* norm_term *)
|
|
353 |
|
|
354 |
(*beta normal form for terms (not eta normal form), chase variables in
|
|
355 |
bindings environment (code taken from Pure/envir.ML)*)
|
|
356 |
|
|
357 |
fun norm_term (ctxt as Context {binds, ...}) =
|
|
358 |
let
|
|
359 |
(*raised when norm has no effect on a term, to do sharing instead of copying*)
|
|
360 |
exception SAME;
|
|
361 |
|
|
362 |
fun norm (t as Var (xi, T)) =
|
|
363 |
(case Vartab.lookup (binds, xi) of
|
|
364 |
Some (u, U) =>
|
|
365 |
if T = U then (norm u handle SAME => u)
|
|
366 |
else raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u])
|
|
367 |
| None =>
|
|
368 |
if can Syntax.dest_binding (#1 xi) then
|
|
369 |
raise CONTEXT ("Unbound binding: " ^ Syntax.string_of_vname xi, ctxt)
|
|
370 |
else raise SAME)
|
|
371 |
| norm (Abs (a, T, body)) = Abs (a, T, norm body)
|
|
372 |
| norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
|
|
373 |
| norm (f $ t) =
|
|
374 |
((case norm f of
|
|
375 |
Abs (_, _, body) => normh (subst_bound (t, body))
|
|
376 |
| nf => nf $ (norm t handle SAME => t)) handle SAME => f $ norm t)
|
|
377 |
| norm _ = raise SAME
|
|
378 |
and normh t = norm t handle SAME => t
|
|
379 |
in normh end;
|
|
380 |
|
|
381 |
|
|
382 |
(* read terms *)
|
|
383 |
|
5874
|
384 |
fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
|
5819
|
385 |
let
|
|
386 |
val sign = sign_of ctxt;
|
|
387 |
|
|
388 |
fun def_type xi =
|
|
389 |
(case Vartab.lookup (types, xi) of
|
|
390 |
None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi))
|
|
391 |
| some => some);
|
|
392 |
|
|
393 |
fun def_sort xi = Vartab.lookup (sorts, xi);
|
|
394 |
in
|
|
395 |
(transform_error (read sign (def_type, def_sort, used)) s
|
|
396 |
handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
|
|
397 |
| ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
|
5874
|
398 |
|> app (intern_skolem ctxt true)
|
|
399 |
|> app (if is_pat then I else norm_term ctxt)
|
5819
|
400 |
end;
|
|
401 |
|
5874
|
402 |
val read_termTs = gen_read (read_def_termTs false) (apfst o map) false;
|
|
403 |
val read_term = gen_read read_term_sg I false;
|
|
404 |
val read_prop = gen_read read_prop_sg I false;
|
|
405 |
val read_pat = gen_read read_term_sg I true;
|
5819
|
406 |
|
|
407 |
|
|
408 |
(* certify terms *)
|
|
409 |
|
|
410 |
fun gen_cert cert is_pat ctxt t =
|
|
411 |
(cert (sign_of ctxt) t handle TERM (msg, _) => raise CONTEXT (msg, ctxt))
|
|
412 |
|> intern_skolem ctxt false
|
|
413 |
|> (if is_pat then I else norm_term ctxt);
|
|
414 |
|
|
415 |
val cert_term = gen_cert cert_term_sg false;
|
|
416 |
val cert_prop = gen_cert cert_prop_sg false;
|
|
417 |
val cert_pat = gen_cert cert_term_sg true;
|
|
418 |
|
|
419 |
|
|
420 |
(* declare terms *)
|
|
421 |
|
|
422 |
val ins_types = foldl_aterms
|
|
423 |
(fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types)
|
|
424 |
| (types, Var v) => Vartab.update (v, types)
|
|
425 |
| (types, _) => types);
|
|
426 |
|
|
427 |
val ins_sorts = foldl_types (foldl_atyps
|
|
428 |
(fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts)
|
|
429 |
| (sorts, TVar v) => Vartab.update (v, sorts)
|
|
430 |
| (sorts, _) => sorts));
|
|
431 |
|
|
432 |
val ins_used = foldl_types (foldl_atyps
|
|
433 |
(fn (used, TFree (x, _)) => x ins used
|
|
434 |
| (used, TVar ((x, _), _)) => x ins used
|
|
435 |
| (used, _) => used));
|
|
436 |
|
|
437 |
fun map_defaults f = map_context
|
|
438 |
(fn (thy, data, asms, binds, thms, defs) => (thy, data, asms, binds, thms, f defs));
|
|
439 |
|
|
440 |
fun declare (ctxt, t) =
|
|
441 |
ctxt
|
|
442 |
|> map_defaults (fn (types, sorts, maxidx, used) => (ins_types (types, t), sorts, maxidx, used))
|
|
443 |
|> map_defaults (fn (types, sorts, maxidx, used) => (types, ins_sorts (sorts, t), maxidx, used))
|
|
444 |
|> map_defaults (fn (types, sorts, maxidx, used) => (types, sorts, maxidx, ins_used (used, t)))
|
|
445 |
|> map_defaults (fn (types, sorts, maxidx, used) =>
|
|
446 |
(types, sorts, Int.max (maxidx, Term.maxidx_of_term t), used));
|
|
447 |
|
|
448 |
|
|
449 |
fun declare_term t ctxt = declare (ctxt, t);
|
|
450 |
fun declare_terms ts ctxt = foldl declare (ctxt, ts);
|
|
451 |
|
5874
|
452 |
fun declare_thm thm ctxt =
|
|
453 |
let val {prop, hyps, ...} = Thm.rep_thm thm
|
|
454 |
in ctxt |> declare_terms (prop :: hyps) end;
|
|
455 |
|
5819
|
456 |
fun prep_declare prep (ctxt, s) =
|
|
457 |
let val t = prep ctxt s
|
|
458 |
in (ctxt |> declare_term t, t) end;
|
|
459 |
|
|
460 |
|
|
461 |
|
|
462 |
(** bindings **)
|
|
463 |
|
|
464 |
(* update_binds *)
|
|
465 |
|
|
466 |
fun upd_bind (ctxt, (xi, t)) =
|
|
467 |
let val T = fastype_of t in
|
|
468 |
ctxt
|
|
469 |
|> declare_term t
|
|
470 |
|> map_context (fn (thy, data, asms, binds, thms, defs) =>
|
|
471 |
(thy, data, asms, Vartab.update ((xi, (t, T)), binds), thms, defs))
|
|
472 |
end;
|
|
473 |
|
|
474 |
fun update_binds bs ctxt = foldl upd_bind (ctxt, bs);
|
|
475 |
fun update_binds_env env = update_binds (Envir.alist_of env);
|
|
476 |
|
|
477 |
|
|
478 |
(* add_binds(_i) -- sequential *)
|
|
479 |
|
|
480 |
fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) =
|
|
481 |
let val t = prep ctxt raw_t in
|
|
482 |
if can Syntax.dest_binding x then ctxt |> update_binds [(xi, t)]
|
|
483 |
else raise CONTEXT ("Illegal variable name for term binding: " ^
|
|
484 |
quote (Syntax.string_of_vname xi), ctxt)
|
|
485 |
end;
|
|
486 |
|
|
487 |
fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds);
|
|
488 |
|
|
489 |
val add_binds = gen_binds read_term;
|
|
490 |
val add_binds_i = gen_binds cert_term;
|
|
491 |
|
|
492 |
|
|
493 |
(* match_binds(_i) -- parallel *)
|
|
494 |
|
|
495 |
fun prep_pair prep_pat prep (ctxt, (raw_pat, raw_t)) =
|
|
496 |
let
|
|
497 |
val pat = prep_pat ctxt raw_pat;
|
|
498 |
val (ctxt', t) = prep_declare prep (ctxt, raw_t);
|
|
499 |
in (ctxt', (pat, t)) end;
|
|
500 |
|
|
501 |
fun gen_match_binds prep_pat prep raw_pairs ctxt =
|
|
502 |
let
|
|
503 |
val (ctxt', pairs) = foldl_map (prep_pair prep_pat prep) (ctxt, raw_pairs);
|
|
504 |
val Context {defs = (_, _, maxidx, _), ...} = ctxt';
|
|
505 |
val envs = Unify.smash_unifiers (sign_of ctxt', Envir.empty maxidx, pairs);
|
|
506 |
val env =
|
|
507 |
(case Seq.pull envs of
|
|
508 |
None => raise CONTEXT ("Pattern match failed!", ctxt')
|
|
509 |
| Some (env, _) => env);
|
|
510 |
in ctxt' |> update_binds_env env end;
|
|
511 |
|
|
512 |
val match_binds = gen_match_binds read_pat read_term;
|
|
513 |
val match_binds_i = gen_match_binds cert_pat cert_term;
|
|
514 |
|
|
515 |
|
|
516 |
|
|
517 |
(** theorems **)
|
|
518 |
|
|
519 |
(* thms_closure *)
|
|
520 |
|
|
521 |
fun thms_closure (Context {thy, thms, ...}) =
|
|
522 |
let
|
|
523 |
val global_closure = PureThy.thms_closure thy;
|
|
524 |
fun get name =
|
|
525 |
(case global_closure name of
|
|
526 |
None => Symtab.lookup (thms, name)
|
|
527 |
| some => some);
|
|
528 |
in get end;
|
|
529 |
|
|
530 |
|
|
531 |
(* get_tthm(s) *)
|
|
532 |
|
|
533 |
fun get_tthm (ctxt as Context {thy, thms, ...}) name =
|
|
534 |
(case Symtab.lookup (thms, name) of
|
|
535 |
Some [th] => th
|
|
536 |
| Some _ => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt)
|
|
537 |
| None => (PureThy.get_tthm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
|
|
538 |
|
|
539 |
fun get_tthms (ctxt as Context {thy, thms, ...}) name =
|
|
540 |
(case Symtab.lookup (thms, name) of
|
|
541 |
Some ths => ths
|
|
542 |
| None => (PureThy.get_tthms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
|
|
543 |
|
|
544 |
fun get_tthmss ctxt names = flat (map (get_tthms ctxt) names);
|
|
545 |
|
|
546 |
|
|
547 |
(* put_tthm(s) *)
|
|
548 |
|
|
549 |
fun put_tthms (name, ths) = map_context
|
|
550 |
(fn (thy, data, asms, binds, thms, defs) =>
|
|
551 |
(thy, data, asms, binds, Symtab.update ((name, ths), thms), defs));
|
|
552 |
|
|
553 |
fun put_tthm (name, th) = put_tthms (name, [th]);
|
|
554 |
|
|
555 |
fun put_tthmss [] ctxt = ctxt
|
|
556 |
| put_tthmss (th :: ths) ctxt = ctxt |> put_tthms th |> put_tthmss ths;
|
|
557 |
|
|
558 |
|
|
559 |
(* have_tthms *)
|
|
560 |
|
|
561 |
fun have_tthms name more_attrs ths_attrs ctxt =
|
|
562 |
let
|
|
563 |
fun app ((ct, ths), (th, attrs)) =
|
|
564 |
let val (ct', th') = Attribute.apply ((ct, th), attrs @ more_attrs)
|
|
565 |
in (ct', th' :: ths) end
|
|
566 |
val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
|
|
567 |
val thms = rev rev_thms;
|
|
568 |
in (ctxt' |> put_tthms (name, thms), (name, thms)) end;
|
|
569 |
|
|
570 |
|
|
571 |
|
|
572 |
(** assumptions **)
|
|
573 |
|
|
574 |
(* get assumptions *)
|
|
575 |
|
|
576 |
fun assumptions (Context {asms = (asms, _), ...}) = flat (map #2 asms);
|
|
577 |
fun fixed_names (Context {asms = (_, (fixes, _)), ...}) = map #2 fixes;
|
|
578 |
|
|
579 |
|
|
580 |
(* assume *)
|
|
581 |
|
|
582 |
fun gen_assume prep name attrs raw_props ctxt =
|
|
583 |
let
|
|
584 |
val (ctxt', props) = foldl_map prep (ctxt, raw_props);
|
|
585 |
val sign = sign_of ctxt';
|
|
586 |
val ths = map (fn t => ((Thm.assume (Thm.cterm_of sign t), []), [])) props;
|
|
587 |
|
|
588 |
val (ctxt'', (_, tthms)) =
|
|
589 |
ctxt'
|
|
590 |
|> have_tthms name (Attribute.tag_assumption :: attrs) ths
|
|
591 |
|
|
592 |
val ctxt''' =
|
|
593 |
ctxt''
|
|
594 |
|> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) =>
|
|
595 |
(thy, data, (assumes @ [(name, tthms)], fixes), binds, thms, defs));
|
|
596 |
in (ctxt''', (name, tthms)) end;
|
|
597 |
|
|
598 |
val assume = gen_assume (prep_declare read_prop);
|
|
599 |
val assume_i = gen_assume (prep_declare cert_prop);
|
|
600 |
|
|
601 |
|
|
602 |
(* fix *)
|
|
603 |
|
|
604 |
fun read_skolemT (Context {defs = (_, _, _, used), ...}) None = Type.param used ("'z", logicS)
|
|
605 |
| read_skolemT ctxt (Some s) = read_typ ctxt s;
|
|
606 |
|
|
607 |
fun gen_fix prep check (ctxt, (x, raw_T)) =
|
|
608 |
ctxt
|
|
609 |
|> declare_term (Free (check_skolem ctxt check x, prep ctxt raw_T))
|
|
610 |
|> map_context (fn (thy, data, (assumes, (fixes, names)), binds, thms, defs) =>
|
|
611 |
let val x' = variant names x in
|
|
612 |
(thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs)
|
|
613 |
end);
|
|
614 |
|
|
615 |
fun gen_fixs prep check xs ctxt = foldl (gen_fix prep check) (ctxt, xs);
|
|
616 |
|
|
617 |
|
|
618 |
val fix = gen_fixs read_skolemT true;
|
|
619 |
val fix_i = gen_fixs cert_typ false;
|
|
620 |
|
|
621 |
|
|
622 |
|
|
623 |
(** theory setup **)
|
|
624 |
|
|
625 |
val setup = [ProofDataData.init];
|
|
626 |
|
|
627 |
|
|
628 |
end;
|