1 (* Title: Pure/Isar/locale.ML
3 Author: Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
5 Locales -- Isar proof contexts as meta-level predicates, with local
6 syntax and implicit structures.
8 Draws basic ideas from Florian Kammueller's original version of
9 locales, but uses the richer infrastructure of Isar instead of the raw
10 meta-logic. Furthermore, structured import of contexts (with merge
11 and rename operations) are provided, as well as type-inference of the
12 signature parts, and predicate definitions of the specification text.
14 Interpretation enables the reuse of theorems of locales in other
15 contexts, namely those defined by theories, structured proofs and
20 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
21 In Stefano Berardi et al., Types for Proofs and Programs: International
22 Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
23 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
24 Dependencies between Locales. Technical Report TUM-I0607, Technische
25 Universitaet Muenchen, 2006.
26 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
27 Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
32 - beta-eta normalisation of interpretation parameters
33 - dangling type frees in locales
34 - test subsumption of interpretations when merging theories
41 Rename of expr * (string * mixfix option) option list |
44 datatype 'a element = Elem of 'a | Expr of expr
45 val map_elem: ('a -> 'b) -> 'a element -> 'b element
47 val intern: theory -> xstring -> string
48 val intern_expr: theory -> expr -> expr
49 val extern: theory -> string -> xstring
50 val init: string -> theory -> Proof.context
52 (* The specification of a locale *)
53 val parameters_of: theory -> string ->
54 ((string * typ) * mixfix) list
55 val parameters_of_expr: theory -> expr ->
56 ((string * typ) * mixfix) list
57 val local_asms_of: theory -> string ->
58 ((string * Attrib.src list) * term list) list
59 val global_asms_of: theory -> string ->
60 ((string * Attrib.src list) * term list) list
61 val intros: theory -> string ->
64 (* Processing of locale statements *)
65 val read_context_statement: xstring option -> Element.context element list ->
66 (string * string list) list list -> Proof.context ->
67 string option * Proof.context * Proof.context * (term * term list) list list
68 val read_context_statement_i: string option -> Element.context element list ->
69 (string * string list) list list -> Proof.context ->
70 string option * Proof.context * Proof.context * (term * term list) list list
71 val cert_context_statement: string option -> Element.context_i element list ->
72 (term * term list) list list -> Proof.context ->
73 string option * Proof.context * Proof.context * (term * term list) list list
74 val read_expr: expr -> Element.context list -> Proof.context ->
75 Element.context_i list * Proof.context
76 val cert_expr: expr -> Element.context_i list -> Proof.context ->
77 Element.context_i list * Proof.context
79 (* Diagnostic functions *)
80 val print_locales: theory -> unit
81 val print_locale: theory -> bool -> expr -> Element.context list -> unit
82 val print_registrations: bool -> string -> Proof.context -> unit
84 val add_locale: string option -> bstring -> expr -> Element.context list -> theory
85 -> string * Proof.context
86 val add_locale_i: string option -> bstring -> expr -> Element.context_i list -> theory
87 -> string * Proof.context
90 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
93 val add_thmss: string -> string ->
94 ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
95 Proof.context -> Proof.context
96 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
97 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
98 val add_declaration: string -> declaration -> Proof.context -> Proof.context
100 val interpretation_i: (Proof.context -> Proof.context) ->
101 (bool * string) * Attrib.src list -> expr ->
102 (typ Symtab.table * term Symtab.table) * term list ->
103 theory -> Proof.state
104 val interpretation: (Proof.context -> Proof.context) ->
105 (bool * string) * Attrib.src list -> expr ->
106 string option list * string list ->
107 theory -> Proof.state
108 val interpretation_in_locale: (Proof.context -> Proof.context) ->
109 xstring * expr -> theory -> Proof.state
110 val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
111 (bool * string) * Attrib.src list -> expr ->
112 (typ Symtab.table * term Symtab.table) * term list ->
113 bool -> Proof.state -> Proof.state
114 val interpret: (Proof.state -> Proof.state Seq.seq) ->
115 (bool * string) * Attrib.src list -> expr ->
116 string option list * string list ->
117 bool -> Proof.state -> Proof.state
120 structure Locale: LOCALE =
123 (* legacy operations *)
125 fun gen_merge_lists _ xs [] = xs
126 | gen_merge_lists _ [] ys = ys
127 | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
129 fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
130 fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
132 fun legacy_unvarifyT thm =
134 val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
135 val tvars = rev (Thm.fold_terms Term.add_tvars thm []);
136 val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
137 in Drule.instantiate' tfrees [] thm end;
139 fun legacy_unvarify raw_thm =
141 val thm = legacy_unvarifyT raw_thm;
142 val ct = Thm.cterm_of (Thm.theory_of_thm thm);
143 val vars = rev (Thm.fold_terms Term.add_vars thm []);
144 val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
145 in Drule.instantiate' [] frees thm end;
148 (** locale elements and expressions **)
150 datatype ctxt = datatype Element.ctxt;
154 Rename of expr * (string * mixfix option) option list |
157 val empty = Merge [];
159 datatype 'a element =
160 Elem of 'a | Expr of expr;
162 fun map_elem f (Elem e) = Elem (f e)
163 | map_elem _ (Expr e) = Expr e;
165 type decl = declaration * stamp;
168 {axiom: Element.witness list,
169 (* For locales that define predicates this is [A [A]], where A is the locale
170 specification. Otherwise [].
171 Only required to generate the right witnesses for locales with predicates. *)
172 imports: expr, (*dynamic imports*)
173 elems: (Element.context_i * stamp) list,
174 (* Static content, neither Fixes nor Constrains elements *)
175 params: ((string * typ) * mixfix) list, (*all params*)
176 lparams: string list, (*local params*)
177 decls: decl list * decl list, (*type/term_syntax declarations*)
178 regs: ((string * string list) * Element.witness list) list,
179 (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
180 intros: thm list * thm list}
181 (* Introduction rules: of delta predicate and locale predicate. *)
183 (* CB: an internal (Int) locale element was either imported or included,
184 an external (Ext) element appears directly in the locale text. *)
186 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
190 (** management of registrations in theories and proof contexts **)
192 structure Registrations :
197 val dest: theory -> T ->
199 (((bool * string) * Attrib.src list) * Element.witness list *
200 Thm.thm Termtab.table)) list
201 val lookup: theory -> T * term list ->
202 (((bool * string) * Attrib.src list) * Element.witness list *
203 Thm.thm Termtab.table) option
204 val insert: theory -> term list * ((bool * string) * Attrib.src list) -> T ->
205 T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
206 val add_witness: term list -> Element.witness -> T -> T
207 val add_equation: term list -> Thm.thm -> T -> T
210 (* A registration is indexed by parameter instantiation. Its components are:
211 - parameters and prefix
212 (if the Boolean flag is set, only accesses containing the prefix are generated,
213 otherwise the prefix may be omitted when accessing theorems etc.)
214 - theorems (actually witnesses) instantiating locale assumptions
215 - theorems (equations) interpreting derived concepts and indexed by lhs
217 type T = (((bool * string) * Attrib.src list) * Element.witness list *
218 Thm.thm Termtab.table) Termtab.table;
220 val empty = Termtab.empty;
222 (* term list represented as single term, for simultaneous matching *)
224 Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
226 let fun ut (Const _) ts = ts
227 | ut (s $ t) ts = ut s (t::ts)
230 (* joining of registrations:
231 - prefix and attributes of right theory;
232 - witnesses are equal, no attempt to subsumption testing;
233 - union of equalities, if conflicting (i.e. two eqns with equal lhs)
234 eqn of right theory takes precedence *)
235 fun join (r1, r2) = Termtab.join (fn _ => fn ((_, _, e1), (n, w, e2)) =>
236 (n, w, Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
238 fun dest_transfer thy regs =
239 Termtab.dest regs |> map (apsnd (fn (n, ws, es) =>
240 (n, map (Element.transfer_witness thy) ws, Termtab.map (Thm.transfer thy) es)));
242 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
244 (* registrations that subsume t *)
245 fun subsumers thy t regs =
246 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
248 (* look up registration, pick one that subsumes the query *)
249 fun lookup thy (regs, ts) =
252 val subs = subsumers thy t regs;
256 | ((t', (attn, thms, eqns)) :: _) =>
258 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
259 (* thms contain Frees, not Vars *)
260 val tinst' = tinst |> Vartab.dest (* FIXME Vartab.map (!?) *)
261 |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
263 val inst' = inst |> Vartab.dest
264 |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
266 val inst_morph = Element.inst_morphism thy (tinst', inst');
267 in SOME (attn, map (Element.morph_witness inst_morph) thms,
268 Termtab.map (Morphism.thm inst_morph) eqns)
272 (* add registration if not subsumed by ones already present,
273 additionally returns registrations that are strictly subsumed *)
274 fun insert thy (ts, attn) regs =
277 val subs = subsumers thy t regs ;
281 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
282 val sups' = map (apfst untermify) sups |> map (fn (ts, (n, w, d)) => (ts, (n, w)))
283 in (Termtab.update (t, (attn, [], Termtab.empty)) regs, sups') end
287 fun gen_add f ts thm regs =
291 Termtab.update (t, f thm (the (Termtab.lookup regs t))) regs
294 (* add witness theorem to registration,
295 only if instantiation is exact, otherwise exception Option raised *)
296 fun add_witness ts thm regs =
297 gen_add (fn thm => fn (x, thms, eqns) => (x, thm::thms, eqns)) ts thm regs;
299 (* add equation to registration, replaces previous equation with same lhs;
300 only if instantiation is exact, otherwise exception Option raised;
301 exception TERM raised if not a meta equality *)
302 fun add_equation ts thm regs =
303 gen_add (fn thm => fn (x, thms, eqns) =>
304 (x, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, thm) eqns))
309 (** theory data : locales **)
311 structure LocalesData = TheoryDataFun
313 type T = NameSpace.T * locale Symtab.table;
314 (* 1st entry: locale namespace,
315 2nd entry: locales of the theory *)
317 val empty = (NameSpace.empty, Symtab.empty);
322 ({axiom, imports, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale,
323 {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
326 elems = gen_merge_lists (eq_snd (op =)) elems elems',
330 (Library.merge (eq_snd (op =)) (decls1, decls1'),
331 Library.merge (eq_snd (op =)) (decls2, decls2')),
332 regs = merge_alists regs regs',
334 fun merge _ ((space1, locs1), (space2, locs2)) =
335 (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
340 (** context data : registrations **)
342 structure RegistrationsData = GenericDataFun
344 type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*)
345 val empty = Symtab.empty;
347 fun merge _ = Symtab.join (K Registrations.join);
351 (** access locales **)
353 fun print_locales thy =
354 let val (space, locs) = LocalesData.get thy in
355 Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
359 val intern = NameSpace.intern o #1 o LocalesData.get;
360 val extern = NameSpace.extern o #1 o LocalesData.get;
362 fun declare_locale name thy =
363 thy |> LocalesData.map (fn (space, locs) =>
364 (Sign.declare_name thy name space, locs));
366 fun put_locale name loc =
367 LocalesData.map (fn (space, locs) =>
368 (space, Symtab.update (name, loc) locs));
370 fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
372 fun the_locale thy name =
373 (case get_locale thy name of
375 | NONE => error ("Unknown locale " ^ quote name));
377 fun change_locale name f thy =
379 val {axiom, imports, elems, params, lparams, decls, regs, intros} =
381 val (axiom', imports', elems', params', lparams', decls', regs', intros') =
382 f (axiom, imports, elems, params, lparams, decls, regs, intros);
384 put_locale name {axiom = axiom', imports = imports', elems = elems',
385 params = params', lparams = lparams', decls = decls', regs = regs',
386 intros = intros'} thy
390 (* access registrations *)
392 (* Ids of global registrations are varified,
393 Ids of local registrations are not.
394 Witness thms of registrations are never varified.
395 Varification of eqns as varification of ids. *)
397 (* retrieve registration from theory or context *)
399 fun get_registrations ctxt name =
400 case Symtab.lookup (RegistrationsData.get ctxt) name of
402 | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;
404 fun get_global_registrations thy = get_registrations (Context.Theory thy);
405 fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
408 fun get_registration ctxt (name, ps) =
409 case Symtab.lookup (RegistrationsData.get ctxt) name of
411 | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, ps);
413 fun get_global_registration thy = get_registration (Context.Theory thy);
414 fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
416 val test_global_registration = is_some oo get_global_registration;
417 val test_local_registration = is_some oo get_local_registration;
419 (* add registration to theory or context, ignored if subsumed *)
421 fun put_registration (name, ps) attn ctxt =
422 RegistrationsData.map (fn regs =>
424 val thy = Context.theory_of ctxt;
425 val reg = the_default Registrations.empty (Symtab.lookup regs name);
426 val (reg', sups) = Registrations.insert thy (ps, attn) reg;
427 val _ = if not (null sups) then warning
428 ("Subsumed interpretation(s) of locale " ^
429 quote (extern thy name) ^
430 "\nwith the following prefix(es):" ^
431 commas_quote (map (fn (_, (((_, s), _), _)) => s) sups))
433 in Symtab.update (name, reg') regs end) ctxt;
435 fun put_global_registration id attn = Context.theory_map (put_registration id attn);
436 fun put_local_registration id attn = Context.proof_map (put_registration id attn);
439 fun put_registration_in_locale name id =
440 change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
441 (axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros));
444 (* add witness theorem to registration, ignored if registration not present *)
446 fun add_witness (name, ps) thm =
447 RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));
449 fun add_global_witness id thm = Context.theory_map (add_witness id thm);
450 fun add_local_witness id thm = Context.proof_map (add_witness id thm);
453 fun add_witness_in_locale name id thm =
454 change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
456 fun add (id', thms) =
457 if id = id' then (id', thm :: thms) else (id', thms);
458 in (axiom, imports, elems, params, lparams, decls, map add regs, intros) end);
461 (* add equation to registration, ignored if registration not present *)
463 fun add_equation (name, ps) thm =
464 RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));
466 fun add_global_equation id thm = Context.theory_map (add_equation id thm);
467 fun add_local_equation id thm = Context.proof_map (add_equation id thm);
470 (* printing of registrations *)
472 fun print_registrations show_wits loc ctxt =
474 val thy = ProofContext.theory_of ctxt;
475 val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
476 val prt_thm = prt_term o prop_of;
478 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
479 fun prt_attn ((false, prfx), atts) =
480 Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" ::
481 Attrib.pretty_attribs ctxt atts)
482 | prt_attn ((true, prfx), atts) =
483 Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
484 fun prt_eqns [] = Pretty.str "no equations."
485 | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
486 Pretty.breaks (map prt_thm eqns));
487 fun prt_core ts eqns =
488 [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
489 fun prt_witns [] = Pretty.str "no witnesses."
490 | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
491 Pretty.breaks (map (Element.pretty_witness ctxt) witns))
492 fun prt_reg (ts, (((_, ""), []), witns, eqns)) =
494 then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
495 else Pretty.block (prt_core ts eqns)
496 | prt_reg (ts, (attn, witns, eqns)) =
498 then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @
499 prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))
500 else Pretty.block ((prt_attn attn @
501 [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));
503 val loc_int = intern thy loc;
504 val regs = RegistrationsData.get (Context.Proof ctxt);
505 val loc_regs = Symtab.lookup regs loc_int;
508 NONE => Pretty.str ("no interpretations")
510 val r' = Registrations.dest thy r;
511 val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _)) => prfx) r';
512 in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
519 fun err_in_locale ctxt msg ids =
521 val thy = ProofContext.theory_of ctxt;
522 fun prt_id (name, parms) =
523 [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
524 val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
526 if forall (equal "" o #1) ids then msg
527 else msg ^ "\n" ^ Pretty.string_of (Pretty.block
528 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
529 in error err_msg end;
531 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
534 fun pretty_ren NONE = Pretty.str "_"
535 | pretty_ren (SOME (x, NONE)) = Pretty.str x
536 | pretty_ren (SOME (x, SOME syn)) =
537 Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
539 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
540 | pretty_expr thy (Rename (expr, xs)) =
541 Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
542 | pretty_expr thy (Merge es) =
543 Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
545 fun err_in_expr _ msg (Merge []) = error msg
546 | err_in_expr ctxt msg expr =
547 error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
548 [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
549 pretty_expr (ProofContext.theory_of ctxt) expr]));
552 (** structured contexts: rename + merge + implicit type instantiation **)
554 (* parameter types *)
556 fun frozen_tvars ctxt Ts =
557 #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
558 |> map (fn ((xi, S), T) => (xi, (S, T)));
560 fun unify_frozen ctxt maxidx Ts Us =
562 fun paramify NONE i = (NONE, i)
563 | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
565 val (Ts', maxidx') = fold_map paramify Ts maxidx;
566 val (Us', maxidx'') = fold_map paramify Us maxidx';
567 val thy = ProofContext.theory_of ctxt;
569 fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
570 handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
572 val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
573 val Vs = map (Option.map (Envir.norm_type unifier)) Us';
574 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
575 in map (Option.map (Envir.norm_type unifier')) Vs end;
577 fun params_of elemss =
578 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
580 fun params_of' elemss =
581 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
584 fun params_prefix params = space_implode "_" params;
587 (* CB: param_types has the following type:
588 ('a * 'b option) list -> ('a * 'b) list *)
589 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
592 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
593 handle Symtab.DUP x => err_in_locale ctxt
594 ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
597 (* Distinction of assumed vs. derived identifiers.
598 The former may have axioms relating assumptions of the context to
599 assumptions of the specification fragment (for locales with
600 predicates). The latter have witnesses relating assumptions of the
601 specification fragment to assumptions of other (assumed) specification
604 datatype 'a mode = Assumed of 'a | Derived of 'a;
606 fun map_mode f (Assumed x) = Assumed (f x)
607 | map_mode f (Derived x) = Derived (f x);
610 (* flatten expressions *)
614 fun unify_parms ctxt fixed_parms raw_parmss =
616 val thy = ProofContext.theory_of ctxt;
617 val maxidx = length raw_parmss;
618 val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
620 fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
621 fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
622 val parms = fixed_parms @ maps varify_parms idx_parmss;
624 fun unify T U envir = Sign.typ_unify thy (U, T) envir
625 handle Type.TUNIFY =>
627 val T' = Envir.norm_type (fst envir) T;
628 val U' = Envir.norm_type (fst envir) U;
629 val prt = Sign.string_of_typ thy;
631 raise TYPE ("unify_parms: failed to unify types " ^
632 prt U' ^ " and " ^ prt T', [U', T'], [])
634 fun unify_list (T :: Us) = fold (unify T) Us
636 val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
637 (Vartab.empty, maxidx);
639 val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
640 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
642 fun inst_parms (i, ps) =
643 List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
644 |> map_filter (fn (a, S) =>
645 let val T = Envir.norm_type unifier' (TVar ((a, i), S))
646 in if T = TFree (a, S) then NONE else SOME (a, T) end)
648 in map inst_parms idx_parmss end;
652 fun unify_elemss _ _ [] = []
653 | unify_elemss _ [] [elems] = [elems]
654 | unify_elemss ctxt fixed_parms elemss =
656 val thy = ProofContext.theory_of ctxt;
657 val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
658 |> map (Element.instT_morphism thy);
659 fun inst ((((name, ps), mode), elems), phi) =
660 (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
661 map_mode (map (Element.morph_witness phi)) mode),
662 map (Element.morph_ctxt phi) elems);
663 in map inst (elemss ~~ phis) end;
666 fun renaming xs parms = zip_options parms xs
667 handle Library.UnequalLengths =>
668 error ("Too many arguments in renaming: " ^
669 commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
673 Compute parameters (with types and syntax) of locale expression.
676 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
678 val thy = ProofContext.theory_of ctxt;
680 fun merge_tenvs fixed tenv1 tenv2 =
682 val [env1, env2] = unify_parms ctxt fixed
683 [tenv1 |> Symtab.dest |> map (apsnd SOME),
684 tenv2 |> Symtab.dest |> map (apsnd SOME)]
686 Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
687 Symtab.map (Element.instT_type env2) tenv2)
690 fun merge_syn expr syn1 syn2 =
691 Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
692 handle Symtab.DUP x => err_in_expr ctxt
693 ("Conflicting syntax for parameter: " ^ quote x) expr;
695 fun params_of (expr as Locale name) =
697 val {imports, params, ...} = the_locale thy name;
698 val parms = map (fst o fst) params;
699 val (parms', types', syn') = params_of imports;
700 val all_parms = merge_lists parms' parms;
701 val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
702 val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
703 in (all_parms, all_types, all_syn) end
704 | params_of (expr as Rename (e, xs)) =
706 val (parms', types', syn') = params_of e;
707 val ren = renaming xs parms';
708 (* renaming may reduce number of parameters *)
709 val new_parms = map (Element.rename ren) parms' |> distinct (op =);
710 val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
711 val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
712 handle Symtab.DUP x =>
713 err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
714 val syn_types = map (apsnd (fn mx =>
715 SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0)))))
716 (Symtab.dest new_syn);
717 val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
718 val (env :: _) = unify_parms ctxt []
719 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
720 val new_types = fold (Symtab.insert (op =))
721 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
722 in (new_parms, new_types, new_syn) end
723 | params_of (Merge es) =
724 fold (fn e => fn (parms, types, syn) =>
726 val (parms', types', syn') = params_of e
728 (merge_lists parms parms', merge_tenvs [] types types',
729 merge_syn e syn syn')
731 es ([], Symtab.empty, Symtab.empty)
733 val (parms, types, syn) = params_of expr;
735 (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
736 merge_syn expr prev_syn syn)
739 fun make_params_ids params = [(("", params), ([], Assumed []))];
740 fun make_raw_params_elemss (params, tenv, syn) =
741 [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
742 Int [Fixes (map (fn p =>
743 (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
747 Extend list of identifiers by those new in locale expression expr.
748 Compute corresponding list of lists of locale elements (one entry per
751 Identifiers represent locale fragments and are in an extended form:
752 ((name, ps), (ax_ps, axs))
753 (name, ps) is the locale name with all its parameters.
754 (ax_ps, axs) is the locale axioms with its parameters;
755 axs are always taken from the top level of the locale hierarchy,
756 hence axioms may contain additional parameters from later fragments:
757 ps subset of ax_ps. axs is either singleton or empty.
759 Elements are enriched by identifier-like information:
760 (((name, ax_ps), axs), elems)
761 The parameters in ax_ps are the axiom parameters, but enriched by type
762 info: now each entry is a pair of string and typ option. Axioms are
767 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
769 val thy = ProofContext.theory_of ctxt;
771 fun rename_parms top ren ((name, ps), (parms, mode)) =
772 ((name, map (Element.rename ren) ps),
774 then (map (Element.rename ren) parms,
775 map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
778 (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
780 fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
781 if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
782 then (wits, ids, visited)
785 val {params, regs, ...} = the_locale thy name;
786 val pTs' = map #1 params;
787 val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
788 (* dummy syntax, since required by rename *)
789 val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
790 val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
791 (* propagate parameter types, to keep them consistent *)
792 val regs' = map (fn ((name, ps), wits) =>
793 ((name, map (Element.rename ren) ps),
794 map (Element.transfer_witness thy) wits)) regs;
795 val new_regs = regs';
796 val new_ids = map fst new_regs;
798 map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
800 val new_wits = new_regs |> map (#2 #> map
801 (Element.morph_witness
802 (Element.instT_morphism thy env $>
803 Element.rename_morphism ren $>
804 Element.satisfy_morphism wits)));
805 val new_ids' = map (fn (id, wits) =>
806 (id, ([], Derived wits))) (new_ids ~~ new_wits);
807 val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
808 ((n, pTs), mode)) (new_idTs ~~ new_ids');
809 val new_id = ((name, map #1 pTs), ([], mode));
810 val (wits', ids', visited') = fold add_with_regs new_idTs'
811 (wits @ flat new_wits, ids, visited @ [new_id]);
813 (wits', ids' @ [new_id], visited')
816 (* distribute top-level axioms over assumed ids *)
818 fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
820 val {elems, ...} = the_locale thy name;
822 (fn (Assumes asms, _) => maps (map #1 o #2) asms
825 val (axs1, axs2) = chop (length ts) axioms;
826 in (((name, parms), (all_ps, Assumed axs1)), axs2) end
827 | axiomify all_ps (id, (_, Derived ths)) axioms =
828 ((id, (all_ps, Derived ths)), axioms);
830 (* identifiers of an expression *)
832 fun identify top (Locale name) =
833 (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
834 where name is a locale name, ps a list of parameter names and axs
835 a list of axioms relating to the identifier, axs is empty unless
836 identify at top level (top = true);
837 parms is accumulated list of parameters *)
839 val {axiom, imports, params, ...} = the_locale thy name;
840 val ps = map (#1 o #1) params;
841 val (ids', parms') = identify false imports;
842 (* acyclic import dependencies *)
844 val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
845 val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
846 in (ids_ax, merge_lists parms' ps) end
847 | identify top (Rename (e, xs)) =
849 val (ids', parms') = identify top e;
850 val ren = renaming xs parms'
851 handle ERROR msg => err_in_locale' ctxt msg ids';
853 val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
854 val parms'' = distinct (op =) (maps (#2 o #1) ids'');
855 in (ids'', parms'') end
856 | identify top (Merge es) =
857 fold (fn e => fn (ids, parms) =>
859 val (ids', parms') = identify top e
861 (merge_alists ids ids', merge_lists parms parms')
865 fun inst_wit all_params (t, th) = let
866 val {hyps, prop, ...} = Thm.rep_thm th;
867 val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
868 val [env] = unify_parms ctxt all_params [ps];
869 val t' = Element.instT_term env t;
870 val th' = Element.instT_thm thy env th;
873 fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
875 val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
876 val elems = map fst elems_stamped;
877 val ps = map fst ps_mx;
878 fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
879 val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
880 val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
881 val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
882 val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
884 Element.rename_morphism ren $>
885 Morphism.name_morphism (NameSpace.qualified (params_prefix params)) $>
886 Element.instT_morphism thy env;
887 val elems' = map (Element.morph_ctxt elem_morphism) elems;
888 in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
890 (* parameters, their types and syntax *)
891 val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
892 val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
893 (* compute identifiers and syntax, merge with previous ones *)
894 val (ids, _) = identify true expr;
895 val idents = subtract (eq_fst (op =)) prev_idents ids;
896 val syntax = merge_syntax ctxt ids (syn, prev_syntax);
897 (* type-instantiate elements *)
898 val final_elemss = map (eval all_params tenv syntax) idents;
899 in ((prev_idents @ idents, syntax), final_elemss) end;
904 (* activate elements *)
908 fun axioms_export axs _ As =
909 (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
912 (* NB: derived ids contain only facts at this stage *)
914 fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
915 ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
916 | activate_elem _ _ ((ctxt, mode), Constrains _) =
918 | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
920 val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
921 val ts = maps (map #1 o #2) asms';
922 val (ps, qs) = chop (length ts) axs;
924 ctxt |> fold Variable.auto_fixes ts
925 |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
926 in ((ctxt', Assumed qs), []) end
927 | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
928 ((ctxt, Derived ths), [])
929 | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
931 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
932 val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
933 let val ((c, _), t') = LocalDefs.cert_def ctxt t
934 in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
936 ctxt |> fold (Variable.auto_fixes o #1) asms
937 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
938 in ((ctxt', Assumed axs), []) end
939 | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
940 ((ctxt, Derived ths), [])
941 | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
943 val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
944 val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
945 in ((ctxt', mode), if is_ext then res else []) end;
947 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
949 val thy = ProofContext.theory_of ctxt;
950 val ((ctxt', _), res) =
951 foldl_map (activate_elem ax_in_ctxt (name = ""))
952 ((ProofContext.qualified_names ctxt, mode), elems)
953 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
954 val ctxt'' = if name = "" then ctxt'
956 val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
957 in if test_local_registration ctxt' (name, ps') then ctxt'
959 val ctxt'' = put_local_registration (name, ps') ((true, ""), []) ctxt'
962 fold (add_local_witness (name, ps') o
963 Element.assume_witness thy o Element.witness_prop) axs ctxt''
964 | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
967 in (ProofContext.restore_naming ctxt ctxt'', res) end;
969 fun activate_elemss ax_in_ctxt prep_facts =
970 fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
972 val elems = map (prep_facts ctxt) raw_elems;
973 val (ctxt', res) = apsnd flat
974 (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
975 val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
976 in (((((name, ps), mode), elems'), res), ctxt') end);
980 (* CB: activate_facts prep_facts (ctxt, elemss),
981 where elemss is a list of pairs consisting of identifiers and
982 context elements, extends ctxt by the context elements yielding
983 ctxt' and returns (ctxt', (elemss', facts)).
984 Identifiers in the argument are of the form ((name, ps), axs) and
985 assumptions use the axioms in the identifiers to set up exporters
986 in ctxt'. elemss' does not contain identifiers and is obtained
987 from elemss and the intermediate context with prep_facts.
988 If read_facts or cert_facts is used for prep_facts, these also remove
989 the internal/external markers from elemss. *)
991 fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
992 let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
993 in (ctxt', (elemss, flat factss)) end;
999 (** prepare locale elements **)
1003 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
1004 | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
1005 | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
1008 (* propositions and bindings *)
1010 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
1011 normalises expr (which is either a locale
1012 expression or a single context element) wrt.
1013 to the list ids of already accumulated identifiers.
1014 It returns ((ids', syn'), elemss) where ids' is an extension of ids
1015 with identifiers generated for expr, and elemss is the list of
1016 context elements generated from expr.
1017 syn and syn' are symtabs mapping parameter names to their syntax. syn'
1018 is an extension of syn.
1019 For details, see flatten_expr.
1021 Additionally, for a locale expression, the elems are grouped into a single
1022 Int; individual context elements are marked Ext. In this case, the
1023 identifier-like information of the element is as follows:
1024 - for Fixes: (("", ps), []) where the ps have type info NONE
1025 - for other elements: (("", []), []).
1026 The implementation of activate_facts relies on identifier names being
1027 empty strings for external elements.
1030 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
1031 val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
1034 merge_syntax ctxt ids'
1035 (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
1036 handle Symtab.DUP x => err_in_locale ctxt
1037 ("Conflicting syntax for parameter: " ^ quote x)
1039 [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
1041 | flatten _ ((ids, syn), Elem elem) =
1042 ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
1043 | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
1044 apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
1050 fun declare_int_elem (ctxt, Fixes fixes) =
1051 (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
1052 (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
1053 | declare_int_elem (ctxt, _) = (ctxt, []);
1055 fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
1056 let val (vars, _) = prep_vars fixes ctxt
1057 in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
1058 | declare_ext_elem prep_vars (ctxt, Constrains csts) =
1059 let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
1061 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
1062 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
1063 | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
1065 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
1066 let val (ctxt', propps) =
1068 Int es => foldl_map declare_int_elem (ctxt, es)
1069 | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
1070 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
1071 in (ctxt', propps) end
1072 | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
1076 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
1078 (* CB: fix of type bug of goal in target with context elements.
1079 Parameters new in context elements must receive types that are
1080 distinct from types of parameters in target (fixed_params). *)
1081 val ctxt_with_fixed =
1082 fold Variable.declare_term (map Free fixed_params) ctxt;
1085 |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
1086 |> unify_elemss ctxt_with_fixed fixed_params;
1087 val (_, raw_elemss') =
1088 foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
1089 (int_elemss, raw_elemss);
1090 in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
1096 val norm_term = Envir.beta_norm oo Term.subst_atomic;
1098 fun abstract_thm thy eq =
1099 Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
1101 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
1103 val ((y, T), b) = LocalDefs.abs_def eq;
1104 val b' = norm_term env b;
1105 val th = abstract_thm (ProofContext.theory_of ctxt) eq;
1106 fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
1108 exists (equal y o #1) xs andalso
1109 err "Attempt to define previously specified variable";
1110 exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
1111 err "Attempt to redefine variable";
1112 (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
1116 (* CB: for finish_elems (Int and Ext),
1117 extracts specification, only of assumed elements *)
1119 fun eval_text _ _ _ (Fixes _) text = text
1120 | eval_text _ _ _ (Constrains _) text = text
1121 | eval_text _ (_, Assumed _) is_ext (Assumes asms)
1122 (((exts, exts'), (ints, ints')), (xs, env, defs)) =
1124 val ts = maps (map #1 o #2) asms;
1125 val ts' = map (norm_term env) ts;
1127 if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
1128 else ((exts, exts'), (ints @ ts, ints' @ ts'));
1129 in (spec', (fold Term.add_frees ts' xs, env, defs)) end
1130 | eval_text _ (_, Derived _) _ (Assumes _) text = text
1131 | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
1132 (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
1133 | eval_text _ (_, Derived _) _ (Defines _) text = text
1134 | eval_text _ _ _ (Notes _) text = text;
1137 (* for finish_elems (Int),
1138 remove redundant elements of derived identifiers,
1139 turn assumptions and definitions into facts,
1140 satisfy hypotheses of facts *)
1142 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
1143 | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
1144 | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
1145 | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
1147 | finish_derived _ _ (Derived _) (Fixes _) = NONE
1148 | finish_derived _ _ (Derived _) (Constrains _) = NONE
1149 | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
1150 |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
1151 |> pair Thm.assumptionK |> Notes
1152 |> Element.morph_ctxt satisfy |> SOME
1153 | finish_derived sign satisfy (Derived _) (Defines defs) = defs
1154 |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
1155 |> pair Thm.definitionK |> Notes
1156 |> Element.morph_ctxt satisfy |> SOME
1158 | finish_derived _ satisfy _ (Notes facts) = Notes facts
1159 |> Element.morph_ctxt satisfy |> SOME;
1161 (* CB: for finish_elems (Ext) *)
1163 fun closeup _ false elem = elem
1164 | closeup ctxt true elem =
1167 let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
1168 in Term.list_all_free (frees, t) end;
1170 fun no_binds [] = []
1171 | no_binds _ = error "Illegal term bindings in locale element";
1174 Assumes asms => Assumes (asms |> map (fn (a, propps) =>
1175 (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
1176 | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
1177 (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
1182 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
1183 (x, AList.lookup (op =) parms x, mx)) fixes)
1184 | finish_ext_elem parms _ (Constrains _, _) = Constrains []
1185 | finish_ext_elem _ close (Assumes asms, propp) =
1186 close (Assumes (map #1 asms ~~ propp))
1187 | finish_ext_elem _ close (Defines defs, propp) =
1188 close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
1189 | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
1192 (* CB: finish_parms introduces type info from parms to identifiers *)
1193 (* CB: only needed for types that have been NONE so far???
1194 If so, which are these??? *)
1196 fun finish_parms parms (((name, ps), mode), elems) =
1197 (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
1199 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
1201 val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
1202 val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
1203 val text' = fold (eval_text ctxt id' false) es text;
1204 val es' = map_filter
1205 (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
1206 in ((text', wits'), (id', map Int es')) end
1207 | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
1209 val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
1210 val text' = eval_text ctxt id true e' text;
1211 in ((text', wits), (id, [Ext e'])) end
1215 (* CB: only called by prep_elemss *)
1217 fun finish_elemss ctxt parms do_close =
1218 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
1223 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
1225 fun defs_ord (defs1, defs2) =
1226 list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
1227 Term.fast_term_ord (d1, d2)) (defs1, defs2);
1229 TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
1230 val ord = defs_ord);
1232 fun rem_dup_defs es ds =
1233 fold_map (fn e as (Defines defs) => (fn ds =>
1234 if Defstab.defined ds defs
1235 then (Defines [], ds)
1236 else (e, Defstab.update (defs, ()) ds))
1237 | e => (fn ds => (e, ds))) es ds;
1238 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
1239 | rem_dup_elemss (Ext e) ds = (Ext e, ds);
1240 fun rem_dup_defines raw_elemss =
1241 fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
1242 apfst (pair id) (rem_dup_elemss es ds))
1243 | (id as (_, (Derived _)), es) => (fn ds =>
1244 ((id, es), ds))) raw_elemss Defstab.empty |> #1;
1246 (* CB: type inference and consistency checks for locales.
1248 Works by building a context (through declare_elemss), extracting the
1249 required information and adjusting the context elements (finish_elemss).
1250 Can also universally close free vars in assms and defs. This is only
1251 needed for Ext elements and controlled by parameter do_close.
1253 Only elements of assumed identifiers are considered.
1256 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
1258 (* CB: contexts computed in the course of this function are discarded.
1259 They are used for type inference and consistency checks only. *)
1260 (* CB: fixed_params are the parameters (with types) of the target locale,
1261 empty list if there is no target. *)
1262 (* CB: raw_elemss are list of pairs consisting of identifiers and
1263 context elements, the latter marked as internal or external. *)
1264 val raw_elemss = rem_dup_defines raw_elemss;
1265 val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
1266 (* CB: raw_ctxt is context with additional fixed variables derived from
1267 the fixes elements in raw_elemss,
1268 raw_proppss contains assumptions and definitions from the
1269 external elements in raw_elemss. *)
1270 fun prep_prop raw_propp (raw_ctxt, raw_concl) =
1272 (* CB: add type information from fixed_params to context (declare_term) *)
1273 (* CB: process patterns (conclusion and external elements only) *)
1274 val (ctxt, all_propp) =
1275 prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
1276 (* CB: add type information from conclusion and external elements to context *)
1277 val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
1278 (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
1279 val all_propp' = map2 (curry (op ~~))
1280 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
1281 val (concl, propp) = chop (length raw_concl) all_propp';
1282 in (propp, (ctxt, concl)) end
1284 val (proppss, (ctxt, concl)) =
1285 (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
1287 (* CB: obtain all parameters from identifier part of raw_elemss *)
1288 val xs = map #1 (params_of' raw_elemss);
1289 val typing = unify_frozen ctxt 0
1290 (map (Variable.default_type raw_ctxt) xs)
1291 (map (Variable.default_type ctxt) xs);
1292 val parms = param_types (xs ~~ typing);
1293 (* CB: parms are the parameters from raw_elemss, with correct typing. *)
1295 (* CB: extract information from assumes and defines elements
1296 (fixes, constrains and notes in raw_elemss don't have an effect on
1297 text and elemss), compute final form of context elements. *)
1298 val ((text, _), elemss) = finish_elemss ctxt parms do_close
1299 ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
1300 (* CB: text has the following structure:
1301 (((exts, exts'), (ints, ints')), (xs, env, defs))
1303 exts: external assumptions (terms in external assumes elements)
1304 exts': dito, normalised wrt. env
1305 ints: internal assumptions (terms in internal assumes elements)
1306 ints': dito, normalised wrt. env
1307 xs: the free variables in exts' and ints' and rhss of definitions,
1308 this includes parameters except defined parameters
1309 env: list of term pairs encoding substitutions, where the first term
1310 is a free variable; substitutions represent defines elements and
1311 the rhs is normalised wrt. the previous env
1312 defs: theorems representing the substitutions from defines elements
1313 (thms are normalised wrt. env).
1314 elemss is an updated version of raw_elemss:
1315 - type info added to Fixes and modified in Constrains
1316 - axiom and definition statement replaced by corresponding one
1317 from proppss in Assumes and Defines
1320 in ((parms, elemss, concl), text) end;
1324 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
1325 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
1330 (* facts and attributes *)
1334 fun check_name name =
1335 if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
1338 fun prep_facts _ _ _ ctxt (Int elem) = elem
1339 |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
1340 | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
1341 {var = I, typ = I, term = I,
1344 attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
1348 fun read_facts x = prep_facts check_name ProofContext.get_thms Attrib.intern_src x;
1349 fun cert_facts x = prep_facts I (K I) (K I) x;
1354 (* Get the specification of a locale *)
1356 (*The global specification is made from the parameters and global
1357 assumptions, the local specification from the parameters and the
1358 local assumptions.*)
1362 fun gen_asms_of get thy name =
1364 val ctxt = ProofContext.init thy;
1365 val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
1366 val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
1369 |> maps (fn (_, es) => map (fn Int e => e) es)
1370 |> maps (fn Assumes asms => asms | _ => [])
1371 |> map (apsnd (map fst))
1376 fun parameters_of thy name =
1377 the_locale thy name |> #params;
1379 fun parameters_of_expr thy expr =
1381 val ctxt = ProofContext.init thy;
1382 val pts = params_of_expr ctxt [] (intern_expr thy expr)
1383 ([], Symtab.empty, Symtab.empty);
1384 val raw_params_elemss = make_raw_params_elemss pts;
1385 val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
1386 (([], Symtab.empty), Expr expr);
1387 val ((parms, _, _), _) =
1388 read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
1389 in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
1391 fun local_asms_of thy name =
1392 gen_asms_of (single o Library.last_elem) thy name;
1394 fun global_asms_of thy name =
1395 gen_asms_of I thy name;
1400 #intros o the o Symtab.lookup (#2 (LocalesData.get thy));
1401 (*returns introduction rule for delta predicate and locale predicate
1402 as a pair of singleton lists*)
1405 (* full context statements: imports + elements + conclusion *)
1409 fun prep_context_statement prep_expr prep_elemss prep_facts
1410 do_close fixed_params imports elements raw_concl context =
1412 val thy = ProofContext.theory_of context;
1414 val (import_params, import_tenv, import_syn) =
1415 params_of_expr context fixed_params (prep_expr thy imports)
1416 ([], Symtab.empty, Symtab.empty);
1417 val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
1418 val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
1419 (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
1421 val ((import_ids, _), raw_import_elemss) =
1422 flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
1423 (* CB: normalise "includes" among elements *)
1424 val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
1425 ((import_ids, incl_syn), elements);
1427 val raw_elemss = flat raw_elemsss;
1428 (* CB: raw_import_elemss @ raw_elemss is the normalised list of
1429 context elements obtained from import and elements. *)
1430 (* Now additional elements for parameters are inserted. *)
1431 val import_params_ids = make_params_ids import_params;
1432 val incl_params_ids =
1433 make_params_ids (incl_params \\ import_params);
1434 val raw_import_params_elemss =
1435 make_raw_params_elemss (import_params, incl_tenv, incl_syn);
1436 val raw_incl_params_elemss =
1437 make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
1438 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
1439 context fixed_params
1440 (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
1442 (* replace extended ids (for axioms) by ids *)
1443 val (import_ids', incl_ids) = chop (length import_ids) ids;
1444 val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
1445 val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
1446 (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
1447 (all_ids ~~ all_elemss);
1448 (* CB: all_elemss and parms contain the correct parameter types *)
1450 val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
1451 val (import_ctxt, (import_elemss, _)) =
1452 activate_facts false prep_facts (context, ps);
1454 val (ctxt, (elemss, _)) =
1455 activate_facts false prep_facts (ProofContext.set_stmt true import_ctxt, qs);
1457 ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
1458 (parms, spec, defs)), concl)
1461 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
1463 val thy = ProofContext.theory_of ctxt;
1464 val locale = Option.map (prep_locale thy) raw_locale;
1465 val (fixed_params, imports) =
1469 let val {params = ps, ...} = the_locale thy name
1470 in (map fst ps, Locale name) end);
1471 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
1472 prep_ctxt false fixed_params imports elems concl ctxt;
1473 in (locale, locale_ctxt, elems_ctxt, concl') end;
1475 fun prep_expr prep imports body ctxt =
1477 val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
1478 val all_elems = maps snd (import_elemss @ elemss);
1479 in (all_elems, ctxt') end;
1483 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
1484 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
1486 fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
1487 fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
1489 val read_expr = prep_expr read_context;
1490 val cert_expr = prep_expr cert_context;
1492 fun read_context_statement loc = prep_statement intern read_ctxt loc;
1493 fun read_context_statement_i loc = prep_statement (K I) read_ctxt loc;
1494 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
1503 #> (#2 o cert_context_statement (SOME loc) [] []);
1508 fun print_locale thy show_facts imports body =
1509 let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
1510 Pretty.big_list "locale elements:" (all_elems
1511 |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
1512 |> map (Element.pretty_ctxt ctxt) |> filter_out null
1513 |> map Pretty.chunks)
1519 (** store results **)
1521 (* naming of interpreted theorems *)
1523 fun global_note_prefix_i kind (fully_qualified, prfx) args thy =
1525 |> Sign.qualified_names
1526 |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
1527 |> PureThy.note_thmss_i kind args
1528 ||> Sign.restore_naming thy;
1530 fun local_note_prefix_i kind (fully_qualified, prfx) args ctxt =
1532 |> ProofContext.qualified_names
1533 |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
1534 |> ProofContext.note_thmss_i kind args
1535 ||> ProofContext.restore_naming ctxt;
1538 (* join equations of an id with already accumulated ones *)
1540 fun join_eqns get_reg prep_id ctxt id eqns =
1542 val id' = prep_id id
1543 val eqns' = case get_reg id'
1545 | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
1546 handle Termtab.DUP t =>
1547 error ("Conflicting interpreting equations for term " ^
1548 quote (Syntax.string_of_term ctxt t))
1549 in ((id', eqns'), eqns') end;
1552 (* collect witnesses and equations up to a particular target for global
1553 registration; requires parameters and flattened list of identifiers
1554 instead of recomputing it from the target *)
1556 fun collect_global_witnesses thy parms ids vts = let
1557 val ts = map Logic.unvarify vts;
1558 val (parms, parmTs) = split_list parms;
1559 val parmvTs = map Logic.varifyT parmTs;
1560 val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
1561 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
1563 (* replace parameter names in ids by instantiations *)
1564 val vinst = Symtab.make (parms ~~ vts);
1565 fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
1566 val inst = Symtab.make (parms ~~ ts);
1567 val inst_ids = map (apfst (apsnd vinst_names)) ids;
1568 val assumed_ids' = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
1569 val wits = maps (#2 o the o get_global_registration thy) assumed_ids';
1571 val ids' = map fst inst_ids;
1573 fold_map (join_eqns (get_global_registration thy) I (ProofContext.init thy))
1574 ids' Termtab.empty |> snd |> Termtab.dest |> map snd;
1576 val tinst' = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of vts) Vartab.empty
1577 |> Vartab.dest |> map (fn ((x, 0), (_, T)) => (x, T)) |> Symtab.make;
1578 in ((tinst', vinst), (tinst, inst), wits, eqns) end;
1581 (* store instantiations of args for all registered interpretations
1584 fun note_thmss_registrations target (kind, args) thy =
1586 val parms = the_locale thy target |> #params |> map fst;
1587 val ids = flatten (ProofContext.init thy, intern_expr thy)
1588 (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
1590 val regs = get_global_registrations thy target;
1592 (* add args to thy for all registrations *)
1594 fun activate (vts, (((fully_qualified, prfx), atts2), _, _)) thy =
1596 val (vinsts, insts, prems, eqns) = collect_global_witnesses thy parms ids vts;
1597 val attrib = Attrib.attribute_i thy;
1598 val inst_atts = Args.morph_values
1599 (Morphism.name_morphism (NameSpace.qualified prfx) $>
1600 Element.inst_morphism' thy vinsts insts $>
1601 Element.satisfy_morphism prems $>
1602 Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
1603 Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns #> Drule.standard));
1605 Element.inst_thm thy insts #> Element.satisfy_thm prems #>
1606 MetaSimplifier.rewrite_rule eqns #>
1608 val args' = args |> map (fn ((name, atts), bs) =>
1609 ((name, map (attrib o inst_atts) atts),
1610 bs |> map (fn (ths, more_atts) =>
1611 (map inst_thm ths, map attrib (map inst_atts more_atts @ atts2)))));
1612 in global_note_prefix_i kind (fully_qualified, prfx) args' thy |> snd end;
1613 in fold activate regs thy end;
1616 (* locale results *)
1618 fun add_thmss loc kind args ctxt =
1620 val (ctxt', ([(_, [Notes args'])], _)) =
1621 activate_facts true cert_facts
1622 (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
1623 val ctxt'' = ctxt' |> ProofContext.theory
1625 (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
1626 (axiom, imports, elems @ [(Notes args', stamp ())],
1627 params, lparams, decls, regs, intros))
1628 #> note_thmss_registrations loc args');
1636 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
1638 fun add_decls add loc decl =
1639 ProofContext.theory (change_locale loc
1640 (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
1641 (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
1642 add_thmss loc Thm.internalK
1643 [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
1647 val add_type_syntax = add_decls (apfst o cons);
1648 val add_term_syntax = add_decls (apsnd o cons);
1649 val add_declaration = add_decls (K I);
1655 (** define locales **)
1657 (* predicate text *)
1658 (* CB: generate locale predicates and delta predicates *)
1662 (* introN: name of theorems for introduction rules of locale and
1664 axiomsN: name of theorem set with destruct rules for locale predicates,
1665 also name suffix of delta predicates. *)
1667 val introN = "intro";
1668 val axiomsN = "axioms";
1670 fun atomize_spec thy ts =
1672 val t = Logic.mk_conjunction_balanced ts;
1673 val body = ObjectLogic.atomize_term thy t;
1674 val bodyT = Term.fastype_of body;
1676 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
1677 else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
1680 fun aprop_tr' n c = (c, fn args =>
1681 if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
1684 (* CB: define one predicate including its intro rule and axioms
1685 - bname: predicate name
1686 - parms: locale parameters
1687 - defs: thms representing substitutions from defines elements
1688 - ts: terms representing locale assumptions (not normalised wrt. defs)
1689 - norm_ts: terms representing locale assumptions (normalised wrt. defs)
1693 fun def_pred bname parms defs ts norm_ts thy =
1695 val name = Sign.full_name thy bname;
1697 val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
1698 val env = Term.add_term_free_names (body, []);
1699 val xs = filter (member (op =) env o #1) parms;
1701 val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
1702 |> Library.sort_wrt #1 |> map TFree;
1703 val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
1705 val args = map Logic.mk_type extraTs @ map Free xs;
1706 val head = Term.list_comb (Const (name, predT), args);
1707 val statement = ObjectLogic.ensure_propT thy head;
1709 val ([pred_def], defs_thy) =
1711 |> (if bodyT <> propT then I else
1712 Sign.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
1713 |> Sign.add_consts_i [(bname, predT, NoSyn)]
1714 |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
1715 val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
1717 val cert = Thm.cterm_of defs_thy;
1719 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
1720 MetaSimplifier.rewrite_goals_tac [pred_def] THEN
1721 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
1722 Tactic.compose_tac (false,
1723 Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
1726 (Drule.equal_elim_rule2 OF [body_eq,
1727 MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
1728 |> Conjunction.elim_balanced (length ts);
1729 val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
1730 Element.prove_witness defs_ctxt t
1731 (MetaSimplifier.rewrite_goals_tac defs THEN
1732 Tactic.compose_tac (false, ax, 0) 1));
1733 in ((statement, intro, axioms), defs_thy) end;
1735 fun assumes_to_notes (Assumes asms) axms =
1736 fold_map (fn (a, spec) => fn axs =>
1737 let val (ps, qs) = chop (length spec) axs
1738 in ((a, [(ps, [])]), qs) end) asms axms
1739 |> apfst (curry Notes Thm.assumptionK)
1740 | assumes_to_notes e axms = (e, axms);
1742 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
1744 (* turn Assumes into Notes elements *)
1746 fun change_assumes_elemss axioms elemss =
1748 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
1749 fun change (id as ("", _), es) =
1750 fold_map assumes_to_notes (map satisfy es)
1751 #-> (fn es' => pair (id, es'))
1752 | change e = pair e;
1754 fst (fold_map change elemss (map Element.conclude_witness axioms))
1757 (* adjust hyps of Notes elements *)
1759 fun change_elemss_hyps axioms elemss =
1761 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
1762 fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
1764 in map change elemss end;
1768 (* CB: main predicate definition function *)
1770 fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
1772 val ((elemss', more_ts), a_elem, a_intro, thy'') =
1773 if null exts then ((elemss, []), [], [], thy)
1776 val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
1777 val ((statement, intro, axioms), thy') =
1779 |> def_pred aname parms defs exts exts';
1780 val elemss' = change_assumes_elemss axioms elemss;
1781 val a_elem = [(("", []), [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1784 |> PureThy.note_thmss_qualified Thm.internalK aname [((introN, []), [([intro], [])])];
1785 in ((elemss', [statement]), a_elem, [intro], thy'') end;
1786 val (predicate, stmt', elemss'', b_intro, thy'''') =
1787 if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
1790 val ((statement, intro, axioms), thy''') =
1792 |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts);
1793 val cstatement = Thm.cterm_of thy''' statement;
1794 val elemss'' = change_elemss_hyps axioms elemss';
1795 val b_elem = [(("", []),
1796 [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1799 |> PureThy.note_thmss_qualified Thm.internalK pname
1800 [((introN, []), [([intro], [])]),
1801 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])];
1802 in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
1803 in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
1808 (* add_locale(_i) *)
1812 (* turn Defines into Notes elements, accumulate definition terms *)
1814 fun defines_to_notes is_ext thy (Defines defs) defns =
1816 val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
1817 val notes = map (fn (a, (def, _)) =>
1818 (a, [([assume (cterm_of thy def)], [])])) defs
1820 (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
1822 | defines_to_notes _ _ e defns = (SOME e, defns);
1824 fun change_defines_elemss thy elemss defns =
1826 fun change (id as (n, _), es) defns =
1828 val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
1829 in ((id, map_filter I es'), defns') end
1830 in fold_map change elemss defns end;
1832 fun gen_add_locale prep_ctxt prep_expr
1833 predicate_name bname raw_imports raw_body thy =
1834 (* predicate_name: NONE - open locale without predicate
1835 SOME "" - locale with predicate named as locale
1836 SOME "name" - locale with predicate named "name" *)
1838 val name = Sign.full_name thy bname;
1839 val _ = is_some (get_locale thy name) andalso
1840 error ("Duplicate definition of locale " ^ quote name);
1842 val thy_ctxt = ProofContext.init thy;
1843 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
1844 text as (parms, ((_, exts'), _), defs)) =
1845 prep_ctxt raw_imports raw_body thy_ctxt;
1846 val elemss = import_elemss @ body_elemss |>
1847 map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
1848 val imports = prep_expr thy raw_imports;
1850 val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
1851 List.foldr Term.add_typ_tfrees [] (map snd parms);
1852 val _ = if null extraTs then ()
1853 else warning ("Additional type variable(s) in locale specification " ^ quote bname);
1855 val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
1856 pred_thy), (imports, regs)) =
1858 of SOME predicate_name =>
1860 val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
1861 val (elemss', defns) = change_defines_elemss thy elemss [];
1862 val elemss'' = elemss' @ [(("", []), defns)];
1863 val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
1864 define_preds predicate_name' text elemss'' thy;
1865 fun mk_regs elemss wits =
1866 fold_map (fn (id, elems) => fn wts => let
1867 val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
1868 SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
1869 val (wts1, wts2) = chop (length ts) wts
1870 in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
1871 val regs = mk_regs elemss''' axioms |>
1872 map_filter (fn (("", _), _) => NONE | e => SOME e);
1873 in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
1874 | NONE => ((((elemss, ([], []), []), ([], [])), thy), (imports, []));
1876 fun axiomify axioms elemss =
1877 (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
1878 val ts = flat (map_filter (fn (Assumes asms) =>
1879 SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
1880 val (axs1, axs2) = chop (length ts) axs;
1881 in (axs2, ((id, Assumed axs1), elems)) end)
1883 val (ctxt, (_, facts)) = activate_facts true (K I)
1884 (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
1885 val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
1886 val export = Goal.close_result o Goal.norm_result o
1887 singleton (ProofContext.export view_ctxt thy_ctxt);
1888 val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
1889 val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
1890 val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
1891 val axs' = map (Element.assume_witness pred_thy) stmt';
1892 val loc_ctxt = pred_thy
1893 |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
1894 |> declare_locale name
1898 elems = map (fn e => (e, stamp ())) elems'',
1899 params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
1900 lparams = map #1 (params_of' body_elemss),
1905 in (name, loc_ctxt) end;
1909 val add_locale = gen_add_locale read_context intern_expr;
1910 val add_locale_i = gen_add_locale cert_context (K I);
1914 val _ = Context.add_setup
1915 (add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
1916 snd #> ProofContext.theory_of #>
1917 add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
1918 snd #> ProofContext.theory_of);
1923 (** Normalisation of locale statements ---
1924 discharges goals implied by interpretations **)
1928 fun locale_assm_intros thy =
1929 Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
1930 (#2 (LocalesData.get thy)) [];
1931 fun locale_base_intros thy =
1932 Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
1933 (#2 (LocalesData.get thy)) [];
1935 fun all_witnesses ctxt =
1937 val thy = ProofContext.theory_of ctxt;
1938 fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
1939 (Registrations.dest thy regs |> map (fn (_, (_, wits, _)) =>
1940 map Element.conclude_witness wits) |> flat) @ thms)
1942 in get (RegistrationsData.get (Context.Proof ctxt)) end;
1943 (* FIXME: proper varification *)
1947 fun intro_locales_tac eager ctxt facts st =
1949 val wits = all_witnesses ctxt |> map Thm.varifyT;
1950 val thy = ProofContext.theory_of ctxt;
1951 val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
1953 (ALLGOALS (Method.insert_tac facts THEN'
1954 REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
1955 THEN Tactic.distinct_subgoals_tac) st
1958 val _ = Context.add_setup (Method.add_methods
1960 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
1961 "back-chain introduction rules of locales without unfolding predicates"),
1963 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
1964 "back-chain all introduction rules of locales")]);
1969 (** Interpretation commands **)
1973 (* extract proof obligations (assms and defs) from elements *)
1975 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
1976 | extract_asms_elems ((id, Derived _), _) = (id, []);
1979 (* activate instantiated facts in theory or context *)
1982 TableFun(type key = string * term list
1983 val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
1985 (* abstraction of equations *)
1987 (* maps f(t1,...,tn) to (f(t1,...,tk), [tk+1,...,tn]) where tk is not a variable and all ti with i>k are *)
1990 fun stripc (p as (ct, cts)) =
1991 let val (ct1, ct2) = Thm.dest_comb ct
1993 case Thm.term_of ct2 of
1994 Var _ => stripc (ct1, ct2 :: cts)
1995 | Free _ => stripc (ct1, ct2 :: cts)
1996 | _ => raise CTERM ("", [])
1997 end handle CTERM _ => p
1998 in stripc (ct, []) end;
2002 fun contract_lhs th =
2003 Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion
2004 (fst (Thm.dest_equals (cprop_of th))))) th;
2005 fun abstract cx th = Thm.abstract_rule
2006 (case Thm.term_of cx of Var ((x, _), _) => x | Free (x, _) => x | _ => "x") cx th
2007 handle THM _ => raise THM ("Malformed definitional equation", 0, [th]);
2010 |> `(snd o strip_vars o fst o Thm.dest_equals o cprop_of)
2011 |-> fold_rev abstract
2015 fun gen_activate_facts_elemss mk_ctxt get_reg note attrib std put_reg add_wit add_eqn
2016 attn all_elemss new_elemss propss thmss thy_ctxt =
2018 val ctxt = mk_ctxt thy_ctxt;
2019 val (propss, eq_props) = chop (length new_elemss) propss;
2020 val (thmss, eq_thms) = chop (length new_elemss) thmss;
2022 fun activate_elem eqns disch ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
2024 val ctxt = mk_ctxt thy_ctxt;
2026 Morphism.name_morphism (NameSpace.qualified prfx)
2027 $> Morphism.term_morphism (MetaSimplifier.rewrite_term
2028 (ProofContext.theory_of ctxt) eqns [])
2029 $> Morphism.thm_morphism (disch #> MetaSimplifier.rewrite_rule eqns);
2031 (* discharge hyps in attributes *)
2033 (attrib thy_ctxt o Args.morph_values fact_morphism)
2034 (* append interpretation attributes *)
2035 |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
2036 (* discharge hyps *)
2037 |> map (apsnd (map (apfst (map disch))))
2039 |> map (apsnd (map (apfst (map (MetaSimplifier.rewrite_rule eqns)))))
2040 in snd (note kind (fully_qualified, prfx) facts' thy_ctxt) end
2041 | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
2043 fun activate_elems eqns disch ((id, _), elems) thy_ctxt =
2045 val (prfx_atts, _, _) = case get_reg thy_ctxt id
2047 | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
2048 ^ " while activating facts.");
2049 in fold (activate_elem (the (Idtab.lookup eqns id)) disch prfx_atts) elems thy_ctxt end;
2051 val thy_ctxt' = thy_ctxt
2052 (* add registrations *)
2053 |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
2054 (* add witnesses of Assumed elements (only those generate proof obligations) *)
2055 |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss)
2057 |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
2058 (map o map) (abs_eqn o LocalDefs.meta_rewrite_rule ctxt o
2059 Element.conclude_witness) eq_thms);
2061 val prems = flat (map_filter
2062 (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' id)
2063 | ((_, Derived _), _) => NONE) all_elemss);
2064 val satisfy = Element.satisfy_morphism prems;
2065 val thy_ctxt'' = thy_ctxt'
2066 (* add witnesses of Derived elements *)
2067 |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness satisfy) thms)
2068 (map_filter (fn ((_, Assumed _), _) => NONE
2069 | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
2071 (* Accumulate equations *)
2073 fold_map (join_eqns (get_reg thy_ctxt'') (fst o fst) ctxt) all_elemss Termtab.empty
2075 |> map (apsnd (map snd o Termtab.dest))
2076 |> (fn xs => fold Idtab.update xs Idtab.empty)
2077 (* Idtab.make wouldn't work here: can have conflicting duplicates,
2078 because instantiation may equate ids and equations are accumulated! *)
2080 val disch' = std o Morphism.thm satisfy; (* FIXME *)
2083 (* add facts to theory or context *)
2084 |> fold (activate_elems all_eqns disch') new_elemss
2087 fun global_activate_facts_elemss x = gen_activate_facts_elemss
2089 (fn thy => fn (name, ps) =>
2090 get_global_registration thy (name, map Logic.varify ps))
2091 global_note_prefix_i
2092 Attrib.attribute_i Drule.standard
2093 (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
2094 (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
2095 Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
2097 (fn (n, ps) => add_global_equation (n, map Logic.varify ps))
2100 fun local_activate_facts_elemss x = gen_activate_facts_elemss
2102 get_local_registration
2104 (Attrib.attribute_i o ProofContext.theory_of) I
2105 put_local_registration
2110 fun read_termT ctxt (t, T) =
2111 Syntax.parse_term ctxt t |> TypeInfer.constrain (TypeInfer.paramify_vars T);
2113 fun read_instantiations ctxt parms (insts, eqns) =
2115 val thy = ProofContext.theory_of ctxt;
2117 (* parameter instantiations *)
2118 val parms' = map (apsnd Logic.varifyT) parms;
2119 val d = length parms - length insts;
2121 if d < 0 then error "More arguments than parameters in instantiation."
2122 else insts @ replicate d NONE;
2124 val given = (parms' ~~ insts) |> map_filter
2125 (fn (_, NONE) => NONE
2126 | ((x, T), SOME inst) => SOME (x, (inst, T)));
2127 val (given_ps, given_insts) = split_list given;
2129 (* read given insts / eqns *)
2130 val all_vs = (map (read_termT ctxt) given_insts @ map (Syntax.read_prop ctxt) eqns)
2131 |> Syntax.check_terms ctxt;
2132 val ctxt' = ctxt |> fold Variable.declare_term all_vs;
2133 val (vs, eqns') = all_vs |> chop (length given_insts);
2135 (* infer parameter types *)
2136 val tyenv = fold (fn ((_, T), t) => Sign.typ_match thy (T, Term.fastype_of t))
2137 (given_insts ~~ vs) Vartab.empty;
2138 val looseTs = fold (Term.add_tvarsT o Envir.typ_subst_TVars tyenv o #2) parms' [];
2139 val (fixedTs, _) = Variable.invent_types (map #2 looseTs) ctxt';
2141 fold (fn ((xi, S), v) => Vartab.update_new (xi, (S, TFree v))) (looseTs ~~ fixedTs) tyenv;
2144 val instT = Vartab.fold (fn ((a, 0), (S, T)) =>
2145 if T = TFree (a, S) then I else Symtab.update (a, T)) tyenv' Symtab.empty;
2146 val inst = Symtab.make (given_ps ~~ vs);
2147 in ((instT, inst), eqns') end;
2150 fun gen_prep_registration mk_ctxt test_reg activate
2151 prep_attr prep_expr prep_insts
2152 thy_ctxt raw_attn raw_expr raw_insts =
2154 val ctxt = mk_ctxt thy_ctxt;
2155 val thy = ProofContext.theory_of ctxt;
2156 val ctxt' = ProofContext.init thy;
2158 val attn = (apsnd o map)
2159 (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) raw_attn;
2160 val expr = prep_expr thy raw_expr;
2162 val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
2163 val params_ids = make_params_ids (#1 pts);
2164 val raw_params_elemss = make_raw_params_elemss pts;
2165 val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr);
2166 val ((parms, all_elemss, _), (_, (_, defs, _))) =
2167 read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
2169 (** compute instantiation **)
2171 (* consistency check: equations need to be stored in a particular locale,
2172 therefore if equations are present locale expression must be a name *)
2174 val _ = case (expr, snd raw_insts) of
2175 (Locale _, _) => () | (_, []) => ()
2176 | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
2178 (* read or certify instantiation *)
2179 val ((instT, inst1), eqns) = prep_insts ctxt parms raw_insts;
2181 (* defined params without given instantiation *)
2182 val not_given = filter_out (Symtab.defined inst1 o fst) parms;
2183 fun add_def (p, pT) inst =
2185 val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
2186 NONE => error ("Instance missing for parameter " ^ quote p)
2187 | SOME (Free (_, T), t) => (t, T);
2188 val d = Element.inst_term (instT, inst) t;
2189 in Symtab.update_new (p, d) inst end;
2190 val inst2 = fold add_def not_given inst1;
2191 val inst_morphism = Element.inst_morphism thy (instT, inst2);
2192 (* Note: insts contain no vars. *)
2194 (** compute proof obligations **)
2196 (* restore "small" ids *)
2197 val ids' = map (fn ((n, ps), (_, mode)) =>
2198 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
2200 val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
2201 (* instantiate ids and elements *)
2202 val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
2203 ((n, map (Morphism.term inst_morphism) ps),
2204 map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
2205 |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
2207 (* remove fragments already registered with theory or context *)
2208 val new_inst_elemss = filter_out (fn ((id, _), _) =>
2209 test_reg thy_ctxt id) inst_elemss;
2210 (* val new_ids = map #1 new_inst_elemss; *)
2213 val eqn_elems = if null eqns then []
2214 else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
2216 val propss = map extract_asms_elems new_inst_elemss @ eqn_elems;
2218 in (propss, activate attn inst_elemss new_inst_elemss propss) end;
2220 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
2221 (fn thy => fn (name, ps) => test_global_registration thy (name, map Logic.varify ps))
2222 global_activate_facts_elemss mk_ctxt;
2224 fun gen_prep_local_registration mk_ctxt = gen_prep_registration I
2225 test_local_registration
2226 local_activate_facts_elemss mk_ctxt;
2228 val prep_global_registration = gen_prep_global_registration
2229 Attrib.intern_src intern_expr read_instantiations;
2230 val prep_global_registration_i = gen_prep_global_registration
2231 (K I) (K I) ((K o K) I);
2233 val prep_local_registration = gen_prep_local_registration
2234 Attrib.intern_src intern_expr read_instantiations;
2235 val prep_local_registration_i = gen_prep_local_registration
2236 (K I) (K I) ((K o K) I);
2238 fun prep_registration_in_locale target expr thy =
2239 (* target already in internal form *)
2241 val ctxt = ProofContext.init thy;
2242 val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
2243 (([], Symtab.empty), Expr (Locale target));
2244 val fixed = the_locale thy target |> #params |> map #1;
2245 val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
2246 ((raw_target_ids, target_syn), Expr expr);
2247 val (target_ids, ids) = chop (length raw_target_ids) all_ids;
2248 val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
2250 (** compute proof obligations **)
2252 (* restore "small" ids, with mode *)
2253 val ids' = map (apsnd snd) ids;
2254 (* remove Int markers *)
2255 val elemss' = map (fn (_, es) =>
2256 map (fn Int e => e) es) elemss
2257 (* extract assumptions and defs *)
2258 val ids_elemss = ids' ~~ elemss';
2259 val propss = map extract_asms_elems ids_elemss;
2261 (** activation function:
2262 - add registrations to the target locale
2263 - add induced registrations for all global registrations of
2264 the target, unless already present
2265 - add facts of induced registrations to theory **)
2267 (* val t_ids = map_filter
2268 (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids; *)
2270 fun activate thmss thy = let
2271 val satisfy = Element.satisfy_thm (flat thmss);
2272 val ids_elemss_thmss = ids_elemss ~~ thmss;
2273 val regs = get_global_registrations thy target;
2275 fun activate_id (((id, Assumed _), _), thms) thy =
2276 thy |> put_registration_in_locale target id
2277 |> fold (add_witness_in_locale target id) thms
2278 | activate_id _ thy = thy;
2280 fun activate_reg (vts, (((fully_qualified, prfx), atts2), _, _)) thy =
2282 val (vinsts, insts, wits, _) = collect_global_witnesses thy fixed target_ids vts;
2283 fun inst_parms ps = map
2284 (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
2285 val disch = Element.satisfy_thm wits;
2286 val new_elemss = filter (fn (((name, ps), _), _) =>
2287 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
2288 fun activate_assumed_id (((_, Derived _), _), _) thy = thy
2289 | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
2290 val ps' = inst_parms ps;
2292 if test_global_registration thy (name, ps')
2295 |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2)
2296 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2297 (Element.morph_witness (Element.inst_morphism' thy vinsts insts) witn) thy) thms
2300 fun activate_derived_id ((_, Assumed _), _) thy = thy
2301 | activate_derived_id (((name, ps), Derived ths), _) thy = let
2302 val ps' = inst_parms ps;
2304 if test_global_registration thy (name, ps')
2307 |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2)
2308 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2309 (witn |> Element.map_witness (fn (t, th) => (* FIXME *)
2310 (Element.inst_term insts t,
2311 disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
2314 fun activate_elem (Notes (kind, facts)) thy =
2317 Morphism.name_morphism (NameSpace.qualified prfx) $>
2318 Morphism.thm_morphism satisfy $>
2319 Element.inst_morphism thy insts $>
2320 Morphism.thm_morphism disch;
2322 |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
2323 |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
2324 |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
2327 |> global_note_prefix_i kind (fully_qualified, prfx) facts'
2330 | activate_elem _ thy = thy;
2332 fun activate_elems (_, elems) thy = fold activate_elem elems thy;
2334 in thy |> fold activate_assumed_id ids_elemss_thmss
2335 |> fold activate_derived_id ids_elemss
2336 |> fold activate_elems new_elemss end;
2338 thy |> fold activate_id ids_elemss_thmss
2339 |> fold activate_reg regs
2342 in (propss, activate) end;
2344 fun prep_propp propss = propss |> map (fn (_, props) =>
2345 map (rpair [] o Element.mark_witness) props);
2347 fun prep_result propps thmss =
2348 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
2350 fun gen_interpretation prep_registration after_qed (prfx, raw_atts) raw_expr raw_insts thy =
2351 (* prfx = (flag indicating full qualification, name prefix) *)
2353 val (propss, activate) = prep_registration thy (prfx, raw_atts) raw_expr raw_insts;
2354 fun after_qed' results =
2355 ProofContext.theory (activate (prep_result propss results))
2359 |> ProofContext.init
2360 |> Proof.theorem_i NONE after_qed' (prep_propp propss)
2361 |> Element.refine_witness
2365 fun gen_interpret prep_registration after_qed (prfx, atts) expr insts int state =
2366 (* prfx = (flag indicating full qualification, name prefix) *)
2368 val _ = Proof.assert_forward_or_chain state;
2369 val ctxt = Proof.context_of state;
2370 val (propss, activate) = prep_registration ctxt (prfx, atts) expr insts;
2371 fun after_qed' results =
2372 Proof.map_context (K (ctxt |> activate (prep_result propss results)))
2373 #> Proof.put_facts NONE
2377 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
2378 "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
2379 |> Element.refine_witness |> Seq.hd
2384 val interpretation_i = gen_interpretation prep_global_registration_i;
2385 val interpretation = gen_interpretation prep_global_registration;
2388 fun interpretation_in_locale after_qed (raw_target, expr) thy =
2390 val target = intern thy raw_target;
2391 val (propss, activate) = prep_registration_in_locale target expr thy;
2392 val raw_propp = prep_propp propss;
2394 val (_, _, goal_ctxt, propp) = thy
2395 |> ProofContext.init
2396 |> cert_context_statement (SOME target) [] raw_propp;
2398 fun after_qed' results =
2399 ProofContext.theory (activate (prep_result propss results))
2403 |> Proof.theorem_i NONE after_qed' propp
2404 |> Element.refine_witness |> Seq.hd
2407 val interpret_i = gen_interpret prep_local_registration_i;
2408 val interpret = gen_interpret prep_local_registration;