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
63 val intros: theory -> string -> thm list * thm list
64 val dests: theory -> string -> thm list
65 (* Not part of the official interface. DO NOT USE *)
66 val facts_of: theory -> string
67 -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list list
69 (* Processing of locale statements *)
70 val read_context_statement: xstring option -> Element.context element list ->
71 (string * string list) list list -> Proof.context ->
72 string option * Proof.context * Proof.context * (term * term list) list list
73 val read_context_statement_i: string option -> Element.context element list ->
74 (string * string list) list list -> Proof.context ->
75 string option * Proof.context * Proof.context * (term * term list) list list
76 val cert_context_statement: string option -> Element.context_i element list ->
77 (term * term list) list list -> Proof.context ->
78 string option * Proof.context * Proof.context * (term * term list) list list
79 val read_expr: expr -> Element.context list -> Proof.context ->
80 Element.context_i list * Proof.context
81 val cert_expr: expr -> Element.context_i list -> Proof.context ->
82 Element.context_i list * Proof.context
84 (* Diagnostic functions *)
85 val print_locales: theory -> unit
86 val print_locale: theory -> bool -> expr -> Element.context list -> unit
87 val print_registrations: bool -> string -> Proof.context -> unit
89 val add_locale: string -> bstring -> expr -> Element.context list -> theory
90 -> string * Proof.context
91 val add_locale_i: string -> bstring -> expr -> Element.context_i list -> theory
92 -> string * Proof.context
95 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
98 val add_thmss: string -> string ->
99 ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
100 Proof.context -> Proof.context
101 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
102 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
103 val add_declaration: string -> declaration -> Proof.context -> Proof.context
105 val interpretation_i: (Proof.context -> Proof.context) ->
106 (bool * string) * Attrib.src list -> expr ->
107 term option list * ((bstring * Attrib.src list) * term) list ->
108 theory -> Proof.state
109 val interpretation: (Proof.context -> Proof.context) ->
110 (bool * string) * Attrib.src list -> expr ->
111 string option list * ((bstring * Attrib.src list) * string) list ->
112 theory -> Proof.state
113 val interpretation_in_locale: (Proof.context -> Proof.context) ->
114 xstring * expr -> theory -> Proof.state
115 val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
116 (bool * string) * Attrib.src list -> expr ->
117 term option list * ((bstring * Attrib.src list) * term) list ->
118 bool -> Proof.state -> Proof.state
119 val interpret: (Proof.state -> Proof.state Seq.seq) ->
120 (bool * string) * Attrib.src list -> expr ->
121 string option list * ((bstring * Attrib.src list) * string) list ->
122 bool -> Proof.state -> Proof.state
125 structure Locale: LOCALE =
128 (* legacy operations *)
130 fun merge_lists _ xs [] = xs
131 | merge_lists _ [] ys = ys
132 | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
134 fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
137 (** locale elements and expressions **)
139 datatype ctxt = datatype Element.ctxt;
143 Rename of expr * (string * mixfix option) option list |
146 val empty = Merge [];
148 datatype 'a element =
149 Elem of 'a | Expr of expr;
151 fun map_elem f (Elem e) = Elem (f e)
152 | map_elem _ (Expr e) = Expr e;
154 type decl = declaration * stamp;
157 {axiom: Element.witness list,
158 (* For locales that define predicates this is [A [A]], where A is the locale
159 specification. Otherwise [].
160 Only required to generate the right witnesses for locales with predicates. *)
161 elems: (Element.context_i * stamp) list,
162 (* Static content, neither Fixes nor Constrains elements *)
163 params: ((string * typ) * mixfix) list, (*all params*)
164 decls: decl list * decl list, (*type/term_syntax declarations*)
165 regs: ((string * string list) * Element.witness list) list,
166 (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
167 intros: thm list * thm list,
168 (* Introduction rules: of delta predicate and locale predicate. *)
170 (* Destruction rules: projections from locale predicate to predicates of fragments. *)
172 (* CB: an internal (Int) locale element was either imported or included,
173 an external (Ext) element appears directly in the locale text. *)
175 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
179 (** substitutions on Vars -- clone from element.ML **)
181 (* instantiate types *)
183 fun var_instT_type env =
184 if Vartab.is_empty env then I
185 else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x));
187 fun var_instT_term env =
188 if Vartab.is_empty env then I
189 else Term.map_types (var_instT_type env);
191 fun var_inst_term (envT, env) =
192 if Vartab.is_empty env then var_instT_term envT
195 val instT = var_instT_type envT;
196 fun inst (Const (x, T)) = Const (x, instT T)
197 | inst (Free (x, T)) = Free(x, instT T)
198 | inst (Var (xi, T)) =
199 (case Vartab.lookup env xi of
200 NONE => Var (xi, instT T)
202 | inst (b as Bound _) = b
203 | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
204 | inst (t $ u) = inst t $ inst u;
205 in Envir.beta_norm o inst end;
208 (** management of registrations in theories and proof contexts **)
211 {attn: (bool * string) * Attrib.src list,
212 (* parameters and prefix
213 (if the Boolean flag is set, only accesses containing the prefix are generated,
214 otherwise the prefix may be omitted when accessing theorems etc.) *)
215 exp: Morphism.morphism,
216 (* maps content to its originating context *)
217 imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
219 wits: Element.witness list,
220 (* witnesses of the registration *)
221 eqns: thm Termtab.table
222 (* theorems (equations) interpreting derived concepts and indexed by lhs *)
225 structure Registrations :
230 val dest: theory -> T ->
232 (((bool * string) * Attrib.src list) *
233 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
234 Element.witness list *
235 thm Termtab.table)) list
236 val test: theory -> T * term list -> bool
237 val lookup: theory ->
238 T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
239 (((bool * string) * Attrib.src list) *
240 Element.witness list *
241 thm Termtab.table) option
242 val insert: theory -> term list -> ((bool * string) * Attrib.src list) ->
243 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
245 T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
246 val add_witness: term list -> Element.witness -> T -> T
247 val add_equation: term list -> thm -> T -> T
250 (* A registration is indexed by parameter instantiation.
251 NB: index is exported whereas content is internalised. *)
252 type T = registration Termtab.table;
254 fun mk_reg attn exp imp wits eqns =
255 {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns};
259 val {attn, exp, imp, wits, eqns} = reg;
260 val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns);
261 in mk_reg attn' exp' imp' wits' eqns' end;
263 val empty = Termtab.empty;
265 (* term list represented as single term, for simultaneous matching *)
267 Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
269 let fun ut (Const _) ts = ts
270 | ut (s $ t) ts = ut s (t::ts)
273 (* joining of registrations:
274 - prefix, attributes and morphisms of right theory;
275 - witnesses are equal, no attempt to subsumption testing;
276 - union of equalities, if conflicting (i.e. two eqns with equal lhs)
277 eqn of right theory takes precedence *)
278 fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) =>
279 mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
281 fun dest_transfer thy regs =
282 Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es) =>
283 (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));
285 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
286 map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns)));
288 (* registrations that subsume t *)
289 fun subsumers thy t regs =
290 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
292 (* test if registration that subsumes the query is present *)
293 fun test thy (regs, ts) =
294 not (null (subsumers thy (termify ts) regs));
296 (* look up registration, pick one that subsumes the query *)
297 fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) =
300 val subs = subsumers thy t regs;
304 | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
306 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
307 val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
308 (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst
309 |> var_instT_type impT)) |> Symtab.make;
310 val inst' = dom' |> map (fn (t as Free (x, _)) =>
311 (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
312 |> var_inst_term (impT, imp))) |> Symtab.make;
313 val inst'_morph = Element.inst_morphism thy (tinst', inst');
314 in SOME ((prfx, map (Args.morph_values inst'_morph) atts),
315 map (Element.morph_witness inst'_morph) wits,
316 Termtab.map (Morphism.thm inst'_morph) eqns)
320 (* add registration if not subsumed by ones already present,
321 additionally returns registrations that are strictly subsumed *)
322 fun insert thy ts attn (exp, imp) regs =
325 val subs = subsumers thy t regs ;
329 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
330 val sups' = map (apfst untermify) sups |> map (fn (ts, {attn, wits, ...}) => (ts, (attn, wits)))
331 in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end
335 fun gen_add f ts regs =
339 Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs
342 (* add witness theorem to registration,
343 only if instantiation is exact, otherwise exception Option raised *)
344 fun add_witness ts wit regs =
345 gen_add (fn (x, e, i, wits, eqns) => (x, e, i, Element.close_witness wit :: wits, eqns))
348 (* add equation to registration, replaces previous equation with same lhs;
349 only if instantiation is exact, otherwise exception Option raised;
350 exception TERM raised if not a meta equality *)
351 fun add_equation ts thm regs =
352 gen_add (fn (x, e, i, thms, eqns) =>
353 (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns))
358 (** theory data : locales **)
360 structure LocalesData = TheoryDataFun
362 type T = NameSpace.T * locale Symtab.table;
363 (* 1st entry: locale namespace,
364 2nd entry: locales of the theory *)
366 val empty = (NameSpace.empty, Symtab.empty);
371 ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,
372 {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
374 elems = merge_lists (eq_snd (op =)) elems elems',
377 (Library.merge (eq_snd (op =)) (decls1, decls1'),
378 Library.merge (eq_snd (op =)) (decls2, decls2')),
379 regs = merge_alists (op =) regs regs',
382 fun merge _ ((space1, locs1), (space2, locs2)) =
383 (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
388 (** context data : registrations **)
390 structure RegistrationsData = GenericDataFun
392 type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*)
393 val empty = Symtab.empty;
395 fun merge _ = Symtab.join (K Registrations.join);
399 (** access locales **)
401 val intern = NameSpace.intern o #1 o LocalesData.get;
402 val extern = NameSpace.extern o #1 o LocalesData.get;
404 fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
406 fun the_locale thy name = case get_locale thy name
408 | NONE => error ("Unknown locale " ^ quote name);
410 fun register_locale name loc thy =
411 thy |> LocalesData.map (fn (space, locs) =>
412 (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
414 fun change_locale name f thy =
416 val {axiom, elems, params, decls, regs, intros, dests} =
418 val (axiom', elems', params', decls', regs', intros', dests') =
419 f (axiom, elems, params, decls, regs, intros, dests);
422 |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
423 elems = elems', params = params',
424 decls = decls', regs = regs', intros = intros', dests = dests'}))
427 fun print_locales thy =
428 let val (space, locs) = LocalesData.get thy in
429 Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
434 (* access registrations *)
436 (* retrieve registration from theory or context *)
438 fun get_registrations ctxt name =
439 case Symtab.lookup (RegistrationsData.get ctxt) name of
441 | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;
443 fun get_global_registrations thy = get_registrations (Context.Theory thy);
444 fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
447 fun get_registration ctxt imprt (name, ps) =
448 case Symtab.lookup (RegistrationsData.get ctxt) name of
450 | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));
452 fun get_global_registration thy = get_registration (Context.Theory thy);
453 fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
456 fun test_registration ctxt (name, ps) =
457 case Symtab.lookup (RegistrationsData.get ctxt) name of
459 | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps);
461 fun test_global_registration thy = test_registration (Context.Theory thy);
462 fun test_local_registration ctxt = test_registration (Context.Proof ctxt);
465 (* add registration to theory or context, ignored if subsumed *)
467 fun put_registration (name, ps) attn morphs (* wits *) ctxt =
468 RegistrationsData.map (fn regs =>
470 val thy = Context.theory_of ctxt;
471 val reg = the_default Registrations.empty (Symtab.lookup regs name);
472 val (reg', sups) = Registrations.insert thy ps attn morphs (* wits *) reg;
473 val _ = if not (null sups) then warning
474 ("Subsumed interpretation(s) of locale " ^
475 quote (extern thy name) ^
476 "\nwith the following prefix(es):" ^
477 commas_quote (map (fn (_, (((_, s), _), _)) => s) sups))
479 in Symtab.update (name, reg') regs end) ctxt;
481 fun put_global_registration id attn morphs =
482 Context.theory_map (put_registration id attn morphs);
483 fun put_local_registration id attn morphs =
484 Context.proof_map (put_registration id attn morphs);
487 fun put_registration_in_locale name id =
488 change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
489 (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
492 (* add witness theorem to registration, ignored if registration not present *)
494 fun add_witness (name, ps) thm =
495 RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));
497 fun add_global_witness id thm = Context.theory_map (add_witness id thm);
498 fun add_local_witness id thm = Context.proof_map (add_witness id thm);
501 fun add_witness_in_locale name id thm =
502 change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
504 fun add (id', thms) =
505 if id = id' then (id', thm :: thms) else (id', thms);
506 in (axiom, elems, params, decls, map add regs, intros, dests) end);
509 (* add equation to registration, ignored if registration not present *)
511 fun add_equation (name, ps) thm =
512 RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));
514 fun add_global_equation id thm = Context.theory_map (add_equation id thm);
515 fun add_local_equation id thm = Context.proof_map (add_equation id thm);
518 (* printing of registrations *)
520 fun print_registrations show_wits loc ctxt =
522 val thy = ProofContext.theory_of ctxt;
523 val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
524 fun prt_term' t = if !show_types
525 then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
526 Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
528 val prt_thm = prt_term o prop_of;
530 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
531 fun prt_attn ((false, prfx), atts) =
532 Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" ::
533 Attrib.pretty_attribs ctxt atts)
534 | prt_attn ((true, prfx), atts) =
535 Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
536 fun prt_eqns [] = Pretty.str "no equations."
537 | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
538 Pretty.breaks (map prt_thm eqns));
539 fun prt_core ts eqns =
540 [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
541 fun prt_witns [] = Pretty.str "no witnesses."
542 | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
543 Pretty.breaks (map (Element.pretty_witness ctxt) witns))
544 fun prt_reg (ts, (((_, ""), []), _, witns, eqns)) =
546 then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
547 else Pretty.block (prt_core ts eqns)
548 | prt_reg (ts, (attn, _, witns, eqns)) =
550 then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @
551 prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))
552 else Pretty.block ((prt_attn attn @
553 [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));
555 val loc_int = intern thy loc;
556 val regs = RegistrationsData.get (Context.Proof ctxt);
557 val loc_regs = Symtab.lookup regs loc_int;
560 NONE => Pretty.str ("no interpretations")
562 val r' = Registrations.dest thy r;
563 val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _, _)) => prfx) r';
564 in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
571 fun err_in_locale ctxt msg ids =
573 val thy = ProofContext.theory_of ctxt;
574 fun prt_id (name, parms) =
575 [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
576 val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
578 if forall (equal "" o #1) ids then msg
579 else msg ^ "\n" ^ Pretty.string_of (Pretty.block
580 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
581 in error err_msg end;
583 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
586 fun pretty_ren NONE = Pretty.str "_"
587 | pretty_ren (SOME (x, NONE)) = Pretty.str x
588 | pretty_ren (SOME (x, SOME syn)) =
589 Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
591 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
592 | pretty_expr thy (Rename (expr, xs)) =
593 Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
594 | pretty_expr thy (Merge es) =
595 Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
597 fun err_in_expr _ msg (Merge []) = error msg
598 | err_in_expr ctxt msg expr =
599 error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
600 [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
601 pretty_expr (ProofContext.theory_of ctxt) expr]));
604 (** structured contexts: rename + merge + implicit type instantiation **)
606 (* parameter types *)
608 fun frozen_tvars ctxt Ts =
609 #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
610 |> map (fn ((xi, S), T) => (xi, (S, T)));
612 fun unify_frozen ctxt maxidx Ts Us =
614 fun paramify NONE i = (NONE, i)
615 | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
617 val (Ts', maxidx') = fold_map paramify Ts maxidx;
618 val (Us', maxidx'') = fold_map paramify Us maxidx';
619 val thy = ProofContext.theory_of ctxt;
621 fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
622 handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
624 val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
625 val Vs = map (Option.map (Envir.norm_type unifier)) Us';
626 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
627 in map (Option.map (Envir.norm_type unifier')) Vs end;
629 fun params_of elemss =
630 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
632 fun params_of' elemss =
633 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
636 fun params_qualified params name =
637 NameSpace.qualified (space_implode "_" params) name;
640 (* CB: param_types has the following type:
641 ('a * 'b option) list -> ('a * 'b) list *)
642 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
645 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
646 handle Symtab.DUP x => err_in_locale ctxt
647 ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
650 (* Distinction of assumed vs. derived identifiers.
651 The former may have axioms relating assumptions of the context to
652 assumptions of the specification fragment (for locales with
653 predicates). The latter have witnesses relating assumptions of the
654 specification fragment to assumptions of other (assumed) specification
657 datatype 'a mode = Assumed of 'a | Derived of 'a;
659 fun map_mode f (Assumed x) = Assumed (f x)
660 | map_mode f (Derived x) = Derived (f x);
663 (* flatten expressions *)
667 fun unify_parms ctxt fixed_parms raw_parmss =
669 val thy = ProofContext.theory_of ctxt;
670 val maxidx = length raw_parmss;
671 val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
673 fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
674 fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
675 val parms = fixed_parms @ maps varify_parms idx_parmss;
677 fun unify T U envir = Sign.typ_unify thy (U, T) envir
678 handle Type.TUNIFY =>
680 val T' = Envir.norm_type (fst envir) T;
681 val U' = Envir.norm_type (fst envir) U;
682 val prt = Syntax.string_of_typ ctxt;
684 raise TYPE ("unify_parms: failed to unify types " ^
685 prt U' ^ " and " ^ prt T', [U', T'], [])
687 fun unify_list (T :: Us) = fold (unify T) Us
689 val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
690 (Vartab.empty, maxidx);
692 val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
693 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
695 fun inst_parms (i, ps) =
696 List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
697 |> map_filter (fn (a, S) =>
698 let val T = Envir.norm_type unifier' (TVar ((a, i), S))
699 in if T = TFree (a, S) then NONE else SOME (a, T) end)
701 in map inst_parms idx_parmss end;
705 fun unify_elemss _ _ [] = []
706 | unify_elemss _ [] [elems] = [elems]
707 | unify_elemss ctxt fixed_parms elemss =
709 val thy = ProofContext.theory_of ctxt;
710 val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
711 |> map (Element.instT_morphism thy);
712 fun inst ((((name, ps), mode), elems), phi) =
713 (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
714 map_mode (map (Element.morph_witness phi)) mode),
715 map (Element.morph_ctxt phi) elems);
716 in map inst (elemss ~~ phis) end;
719 fun renaming xs parms = zip_options parms xs
720 handle Library.UnequalLengths =>
721 error ("Too many arguments in renaming: " ^
722 commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
726 Compute parameters (with types and syntax) of locale expression.
729 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
731 val thy = ProofContext.theory_of ctxt;
733 fun merge_tenvs fixed tenv1 tenv2 =
735 val [env1, env2] = unify_parms ctxt fixed
736 [tenv1 |> Symtab.dest |> map (apsnd SOME),
737 tenv2 |> Symtab.dest |> map (apsnd SOME)]
739 Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
740 Symtab.map (Element.instT_type env2) tenv2)
743 fun merge_syn expr syn1 syn2 =
744 Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
745 handle Symtab.DUP x => err_in_expr ctxt
746 ("Conflicting syntax for parameter: " ^ quote x) expr;
748 fun params_of (expr as Locale name) =
750 val {params, ...} = the_locale thy name;
751 in (map (fst o fst) params, params |> map fst |> Symtab.make,
752 params |> map (apfst fst) |> Symtab.make) end
753 | params_of (expr as Rename (e, xs)) =
755 val (parms', types', syn') = params_of e;
756 val ren = renaming xs parms';
757 (* renaming may reduce number of parameters *)
758 val new_parms = map (Element.rename ren) parms' |> distinct (op =);
759 val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
760 val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
761 handle Symtab.DUP x =>
762 err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
763 val syn_types = map (apsnd (fn mx =>
764 SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0)))))
765 (Symtab.dest new_syn);
766 val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
767 val (env :: _) = unify_parms ctxt []
768 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
769 val new_types = fold (Symtab.insert (op =))
770 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
771 in (new_parms, new_types, new_syn) end
772 | params_of (Merge es) =
773 fold (fn e => fn (parms, types, syn) =>
775 val (parms', types', syn') = params_of e
777 (merge_lists (op =) parms parms', merge_tenvs [] types types',
778 merge_syn e syn syn')
780 es ([], Symtab.empty, Symtab.empty)
782 val (parms, types, syn) = params_of expr;
784 (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
785 merge_syn expr prev_syn syn)
788 fun make_params_ids params = [(("", params), ([], Assumed []))];
789 fun make_raw_params_elemss (params, tenv, syn) =
790 [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
791 Int [Fixes (map (fn p =>
792 (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
796 Extend list of identifiers by those new in locale expression expr.
797 Compute corresponding list of lists of locale elements (one entry per
800 Identifiers represent locale fragments and are in an extended form:
801 ((name, ps), (ax_ps, axs))
802 (name, ps) is the locale name with all its parameters.
803 (ax_ps, axs) is the locale axioms with its parameters;
804 axs are always taken from the top level of the locale hierarchy,
805 hence axioms may contain additional parameters from later fragments:
806 ps subset of ax_ps. axs is either singleton or empty.
808 Elements are enriched by identifier-like information:
809 (((name, ax_ps), axs), elems)
810 The parameters in ax_ps are the axiom parameters, but enriched by type
811 info: now each entry is a pair of string and typ option. Axioms are
816 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
818 val thy = ProofContext.theory_of ctxt;
820 fun rename_parms top ren ((name, ps), (parms, mode)) =
821 ((name, map (Element.rename ren) ps),
823 then (map (Element.rename ren) parms,
824 map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
827 (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *)
829 fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
830 if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
831 then (wits, ids, visited)
834 val {params, regs, ...} = the_locale thy name;
835 val pTs' = map #1 params;
836 val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
837 (* dummy syntax, since required by rename *)
838 val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
839 val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
840 (* propagate parameter types, to keep them consistent *)
841 val regs' = map (fn ((name, ps), wits) =>
842 ((name, map (Element.rename ren) ps),
843 map (Element.transfer_witness thy) wits)) regs;
844 val new_regs = regs';
845 val new_ids = map fst new_regs;
847 map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
849 val new_wits = new_regs |> map (#2 #> map
850 (Element.morph_witness
851 (Element.instT_morphism thy env $>
852 Element.rename_morphism ren $>
853 Element.satisfy_morphism wits)
854 #> Element.close_witness));
855 val new_ids' = map (fn (id, wits) =>
856 (id, ([], Derived wits))) (new_ids ~~ new_wits);
857 val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
858 ((n, pTs), mode)) (new_idTs ~~ new_ids');
859 val new_id = ((name, map #1 pTs), ([], mode));
860 val (wits', ids', visited') = fold add_with_regs new_idTs'
861 (wits @ flat new_wits, ids, visited @ [new_id]);
863 (wits', ids' @ [new_id], visited')
866 (* distribute top-level axioms over assumed ids *)
868 fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
870 val {elems, ...} = the_locale thy name;
872 (fn (Assumes asms, _) => maps (map #1 o #2) asms
875 val (axs1, axs2) = chop (length ts) axioms;
876 in (((name, parms), (all_ps, Assumed axs1)), axs2) end
877 | axiomify all_ps (id, (_, Derived ths)) axioms =
878 ((id, (all_ps, Derived ths)), axioms);
880 (* identifiers of an expression *)
882 fun identify top (Locale name) =
883 (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
884 where name is a locale name, ps a list of parameter names and axs
885 a list of axioms relating to the identifier, axs is empty unless
886 identify at top level (top = true);
887 parms is accumulated list of parameters *)
889 val {axiom, params, ...} = the_locale thy name;
890 val ps = map (#1 o #1) params;
891 val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);
892 val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
894 | identify top (Rename (e, xs)) =
896 val (ids', parms') = identify top e;
897 val ren = renaming xs parms'
898 handle ERROR msg => err_in_locale' ctxt msg ids';
900 val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
901 val parms'' = distinct (op =) (maps (#2 o #1) ids'');
902 in (ids'', parms'') end
903 | identify top (Merge es) =
904 fold (fn e => fn (ids, parms) =>
906 val (ids', parms') = identify top e
908 (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
912 fun inst_wit all_params (t, th) = let
913 val {hyps, prop, ...} = Thm.rep_thm th;
914 val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
915 val [env] = unify_parms ctxt all_params [ps];
916 val t' = Element.instT_term env t;
917 val th' = Element.instT_thm thy env th;
920 fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
922 val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
923 val elems = map fst elems_stamped;
924 val ps = map fst ps_mx;
925 fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
926 val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
927 val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
928 val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
929 val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
931 Element.rename_morphism ren $>
932 Morphism.name_morphism (params_qualified params) $>
933 Element.instT_morphism thy env;
934 val elems' = map (Element.morph_ctxt elem_morphism) elems;
935 in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
937 (* parameters, their types and syntax *)
938 val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
939 val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
940 (* compute identifiers and syntax, merge with previous ones *)
941 val (ids, _) = identify true expr;
942 val idents = subtract (eq_fst (op =)) prev_idents ids;
943 val syntax = merge_syntax ctxt ids (syn, prev_syntax);
944 (* type-instantiate elements *)
945 val final_elemss = map (eval all_params tenv syntax) idents;
946 in ((prev_idents @ idents, syntax), final_elemss) end;
951 (* activate elements *)
955 fun axioms_export axs _ As =
956 (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
959 (* NB: derived ids contain only facts at this stage *)
961 fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
962 ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
963 | activate_elem _ _ (Constrains _) (ctxt, mode) =
965 | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
967 val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
968 val ts = maps (map #1 o #2) asms';
969 val (ps, qs) = chop (length ts) axs;
971 ctxt |> fold Variable.auto_fixes ts
972 |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
973 in ([], (ctxt', Assumed qs)) end
974 | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
975 ([], (ctxt, Derived ths))
976 | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
978 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
979 val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
980 let val ((c, _), t') = LocalDefs.cert_def ctxt t
981 in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
983 ctxt |> fold (Variable.auto_fixes o #1) asms
984 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
985 in ([], (ctxt', Assumed axs)) end
986 | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
987 ([], (ctxt, Derived ths))
988 | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
990 val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
991 val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
992 in (if is_ext then res else [], (ctxt', mode)) end;
994 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
996 val thy = ProofContext.theory_of ctxt;
997 val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
998 elems (ProofContext.qualified_names ctxt, mode)
999 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
1000 val ctxt'' = if name = "" then ctxt'
1002 val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
1003 in if test_local_registration ctxt' (name, ps') then ctxt'
1005 val ctxt'' = put_local_registration (name, ps') ((true, ""), [])
1006 (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
1009 fold (add_local_witness (name, ps') o
1010 Element.assume_witness thy o Element.witness_prop) axs ctxt''
1012 fold (add_local_witness (name, ps')) ths ctxt''
1015 in (ProofContext.restore_naming ctxt ctxt'', res) end;
1017 fun activate_elemss ax_in_ctxt prep_facts =
1018 fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
1020 val elems = map (prep_facts ctxt) raw_elems;
1021 val (ctxt', res) = apsnd flat
1022 (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
1023 val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
1024 in (((((name, ps), mode), elems'), res), ctxt') end);
1028 (* CB: activate_facts prep_facts elemss ctxt,
1029 where elemss is a list of pairs consisting of identifiers and
1030 context elements, extends ctxt by the context elements yielding
1031 ctxt' and returns ((elemss', facts), ctxt').
1032 Identifiers in the argument are of the form ((name, ps), axs) and
1033 assumptions use the axioms in the identifiers to set up exporters
1034 in ctxt'. elemss' does not contain identifiers and is obtained
1035 from elemss and the intermediate context with prep_facts.
1036 If read_facts or cert_facts is used for prep_facts, these also remove
1037 the internal/external markers from elemss. *)
1039 fun activate_facts ax_in_ctxt prep_facts args =
1040 activate_elemss ax_in_ctxt prep_facts args
1041 #>> (apsnd flat o split_list);
1047 (** prepare locale elements **)
1051 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
1052 | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
1053 | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
1056 (* propositions and bindings *)
1058 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
1059 normalises expr (which is either a locale
1060 expression or a single context element) wrt.
1061 to the list ids of already accumulated identifiers.
1062 It returns ((ids', syn'), elemss) where ids' is an extension of ids
1063 with identifiers generated for expr, and elemss is the list of
1064 context elements generated from expr.
1065 syn and syn' are symtabs mapping parameter names to their syntax. syn'
1066 is an extension of syn.
1067 For details, see flatten_expr.
1069 Additionally, for a locale expression, the elems are grouped into a single
1070 Int; individual context elements are marked Ext. In this case, the
1071 identifier-like information of the element is as follows:
1072 - for Fixes: (("", ps), []) where the ps have type info NONE
1073 - for other elements: (("", []), []).
1074 The implementation of activate_facts relies on identifier names being
1075 empty strings for external elements.
1078 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
1079 val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
1082 merge_syntax ctxt ids'
1083 (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
1084 handle Symtab.DUP x => err_in_locale ctxt
1085 ("Conflicting syntax for parameter: " ^ quote x)
1087 [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
1089 | flatten _ ((ids, syn), Elem elem) =
1090 ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
1091 | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
1092 apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
1098 fun declare_int_elem (Fixes fixes) ctxt =
1099 ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
1100 (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
1101 | declare_int_elem _ ctxt = ([], ctxt);
1103 fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
1104 let val (vars, _) = prep_vars fixes ctxt
1105 in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
1106 | declare_ext_elem prep_vars (Constrains csts) ctxt =
1107 let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
1109 | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
1110 | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
1111 | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
1113 fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
1114 of Int es => fold_map declare_int_elem es ctxt
1115 | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
1116 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
1117 | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
1121 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
1123 (* CB: fix of type bug of goal in target with context elements.
1124 Parameters new in context elements must receive types that are
1125 distinct from types of parameters in target (fixed_params). *)
1126 val ctxt_with_fixed =
1127 fold Variable.declare_term (map Free fixed_params) ctxt;
1130 |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
1131 |> unify_elemss ctxt_with_fixed fixed_params;
1132 val (raw_elemss', _) =
1133 fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
1134 raw_elemss int_elemss;
1135 in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
1141 val norm_term = Envir.beta_norm oo Term.subst_atomic;
1143 fun abstract_thm thy eq =
1144 Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
1146 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
1148 val ((y, T), b) = LocalDefs.abs_def eq;
1149 val b' = norm_term env b;
1150 val th = abstract_thm (ProofContext.theory_of ctxt) eq;
1151 fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
1153 exists (equal y o #1) xs andalso
1154 err "Attempt to define previously specified variable";
1155 exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
1156 err "Attempt to redefine variable";
1157 (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
1161 (* CB: for finish_elems (Int and Ext),
1162 extracts specification, only of assumed elements *)
1164 fun eval_text _ _ _ (Fixes _) text = text
1165 | eval_text _ _ _ (Constrains _) text = text
1166 | eval_text _ (_, Assumed _) is_ext (Assumes asms)
1167 (((exts, exts'), (ints, ints')), (xs, env, defs)) =
1169 val ts = maps (map #1 o #2) asms;
1170 val ts' = map (norm_term env) ts;
1172 if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
1173 else ((exts, exts'), (ints @ ts, ints' @ ts'));
1174 in (spec', (fold Term.add_frees ts' xs, env, defs)) end
1175 | eval_text _ (_, Derived _) _ (Assumes _) text = text
1176 | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
1177 (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
1178 | eval_text _ (_, Derived _) _ (Defines _) text = text
1179 | eval_text _ _ _ (Notes _) text = text;
1182 (* for finish_elems (Int),
1183 remove redundant elements of derived identifiers,
1184 turn assumptions and definitions into facts,
1185 satisfy hypotheses of facts *)
1187 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
1188 | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
1189 | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
1190 | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
1192 | finish_derived _ _ (Derived _) (Fixes _) = NONE
1193 | finish_derived _ _ (Derived _) (Constrains _) = NONE
1194 | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
1195 |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
1196 |> pair Thm.assumptionK |> Notes
1197 |> Element.morph_ctxt satisfy |> SOME
1198 | finish_derived sign satisfy (Derived _) (Defines defs) = defs
1199 |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
1200 |> pair Thm.definitionK |> Notes
1201 |> Element.morph_ctxt satisfy |> SOME
1203 | finish_derived _ satisfy _ (Notes facts) = Notes facts
1204 |> Element.morph_ctxt satisfy |> SOME;
1206 (* CB: for finish_elems (Ext) *)
1208 fun closeup _ false elem = elem
1209 | closeup ctxt true elem =
1214 Term.fold_aterms (fn Free (x, T) =>
1215 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
1216 in Term.list_all_free (rev rev_frees, t) end;
1218 fun no_binds [] = []
1219 | no_binds _ = error "Illegal term bindings in locale element";
1222 Assumes asms => Assumes (asms |> map (fn (a, propps) =>
1223 (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
1224 | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
1225 (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
1230 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
1231 (x, AList.lookup (op =) parms x, mx)) fixes)
1232 | finish_ext_elem parms _ (Constrains _, _) = Constrains []
1233 | finish_ext_elem _ close (Assumes asms, propp) =
1234 close (Assumes (map #1 asms ~~ propp))
1235 | finish_ext_elem _ close (Defines defs, propp) =
1236 close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
1237 | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
1240 (* CB: finish_parms introduces type info from parms to identifiers *)
1241 (* CB: only needed for types that have been NONE so far???
1242 If so, which are these??? *)
1244 fun finish_parms parms (((name, ps), mode), elems) =
1245 (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
1247 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
1249 val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
1250 val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
1251 val text' = fold (eval_text ctxt id' false) es text;
1252 val es' = map_filter
1253 (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
1254 in ((text', wits'), (id', map Int es')) end
1255 | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
1257 val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
1258 val text' = eval_text ctxt id true e' text;
1259 in ((text', wits), (id, [Ext e'])) end
1263 (* CB: only called by prep_elemss *)
1265 fun finish_elemss ctxt parms do_close =
1266 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
1271 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
1273 fun defs_ord (defs1, defs2) =
1274 list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
1275 Term.fast_term_ord (d1, d2)) (defs1, defs2);
1277 TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
1278 val ord = defs_ord);
1280 fun rem_dup_defs es ds =
1281 fold_map (fn e as (Defines defs) => (fn ds =>
1282 if Defstab.defined ds defs
1283 then (Defines [], ds)
1284 else (e, Defstab.update (defs, ()) ds))
1285 | e => (fn ds => (e, ds))) es ds;
1286 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
1287 | rem_dup_elemss (Ext e) ds = (Ext e, ds);
1288 fun rem_dup_defines raw_elemss =
1289 fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
1290 apfst (pair id) (rem_dup_elemss es ds))
1291 | (id as (_, (Derived _)), es) => (fn ds =>
1292 ((id, es), ds))) raw_elemss Defstab.empty |> #1;
1294 (* CB: type inference and consistency checks for locales.
1296 Works by building a context (through declare_elemss), extracting the
1297 required information and adjusting the context elements (finish_elemss).
1298 Can also universally close free vars in assms and defs. This is only
1299 needed for Ext elements and controlled by parameter do_close.
1301 Only elements of assumed identifiers are considered.
1304 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
1306 (* CB: contexts computed in the course of this function are discarded.
1307 They are used for type inference and consistency checks only. *)
1308 (* CB: fixed_params are the parameters (with types) of the target locale,
1309 empty list if there is no target. *)
1310 (* CB: raw_elemss are list of pairs consisting of identifiers and
1311 context elements, the latter marked as internal or external. *)
1312 val raw_elemss = rem_dup_defines raw_elemss;
1313 val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
1314 (* CB: raw_ctxt is context with additional fixed variables derived from
1315 the fixes elements in raw_elemss,
1316 raw_proppss contains assumptions and definitions from the
1317 external elements in raw_elemss. *)
1318 fun prep_prop raw_propp (raw_ctxt, raw_concl) =
1320 (* CB: add type information from fixed_params to context (declare_term) *)
1321 (* CB: process patterns (conclusion and external elements only) *)
1322 val (ctxt, all_propp) =
1323 prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
1324 (* CB: add type information from conclusion and external elements to context *)
1325 val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
1326 (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
1327 val all_propp' = map2 (curry (op ~~))
1328 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
1329 val (concl, propp) = chop (length raw_concl) all_propp';
1330 in (propp, (ctxt, concl)) end
1332 val (proppss, (ctxt, concl)) =
1333 (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
1335 (* CB: obtain all parameters from identifier part of raw_elemss *)
1336 val xs = map #1 (params_of' raw_elemss);
1337 val typing = unify_frozen ctxt 0
1338 (map (Variable.default_type raw_ctxt) xs)
1339 (map (Variable.default_type ctxt) xs);
1340 val parms = param_types (xs ~~ typing);
1341 (* CB: parms are the parameters from raw_elemss, with correct typing. *)
1343 (* CB: extract information from assumes and defines elements
1344 (fixes, constrains and notes in raw_elemss don't have an effect on
1345 text and elemss), compute final form of context elements. *)
1346 val ((text, _), elemss) = finish_elemss ctxt parms do_close
1347 ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
1348 (* CB: text has the following structure:
1349 (((exts, exts'), (ints, ints')), (xs, env, defs))
1351 exts: external assumptions (terms in external assumes elements)
1352 exts': dito, normalised wrt. env
1353 ints: internal assumptions (terms in internal assumes elements)
1354 ints': dito, normalised wrt. env
1355 xs: the free variables in exts' and ints' and rhss of definitions,
1356 this includes parameters except defined parameters
1357 env: list of term pairs encoding substitutions, where the first term
1358 is a free variable; substitutions represent defines elements and
1359 the rhs is normalised wrt. the previous env
1360 defs: theorems representing the substitutions from defines elements
1361 (thms are normalised wrt. env).
1362 elemss is an updated version of raw_elemss:
1363 - type info added to Fixes and modified in Constrains
1364 - axiom and definition statement replaced by corresponding one
1365 from proppss in Assumes and Defines
1368 in ((parms, elemss, concl), text) end;
1372 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
1373 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
1378 (* facts and attributes *)
1382 fun check_name name =
1383 if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
1386 fun prep_facts _ _ _ ctxt (Int elem) = elem
1387 |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
1388 | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
1389 {var = I, typ = I, term = I,
1392 attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
1396 fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
1397 fun cert_facts x = prep_facts I (K I) (K I) x;
1402 (* Get the specification of a locale *)
1404 (*The global specification is made from the parameters and global
1405 assumptions, the local specification from the parameters and the
1406 local assumptions.*)
1410 fun gen_asms_of get thy name =
1412 val ctxt = ProofContext.init thy;
1413 val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
1414 val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
1417 |> maps (fn (_, es) => map (fn Int e => e) es)
1418 |> maps (fn Assumes asms => asms | _ => [])
1419 |> map (apsnd (map fst))
1424 fun parameters_of thy = #params o the_locale thy;
1426 fun intros thy = #intros o the_locale thy;
1427 (*returns introduction rule for delta predicate and locale predicate
1428 as a pair of singleton lists*)
1430 fun dests thy = #dests o the_locale thy;
1432 fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts
1433 | _ => NONE) o #elems o the_locale thy;
1435 fun parameters_of_expr thy expr =
1437 val ctxt = ProofContext.init thy;
1438 val pts = params_of_expr ctxt [] (intern_expr thy expr)
1439 ([], Symtab.empty, Symtab.empty);
1440 val raw_params_elemss = make_raw_params_elemss pts;
1441 val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
1442 (([], Symtab.empty), Expr expr);
1443 val ((parms, _, _), _) =
1444 read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
1445 in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
1447 fun local_asms_of thy name =
1448 gen_asms_of (single o Library.last_elem) thy name;
1450 fun global_asms_of thy name =
1451 gen_asms_of I thy name;
1456 (* full context statements: imports + elements + conclusion *)
1460 fun prep_context_statement prep_expr prep_elemss prep_facts
1461 do_close fixed_params imports elements raw_concl context =
1463 val thy = ProofContext.theory_of context;
1465 val (import_params, import_tenv, import_syn) =
1466 params_of_expr context fixed_params (prep_expr thy imports)
1467 ([], Symtab.empty, Symtab.empty);
1468 val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
1469 val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
1470 (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
1472 val ((import_ids, _), raw_import_elemss) =
1473 flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
1474 (* CB: normalise "includes" among elements *)
1475 val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
1476 ((import_ids, incl_syn), elements);
1478 val raw_elemss = flat raw_elemsss;
1479 (* CB: raw_import_elemss @ raw_elemss is the normalised list of
1480 context elements obtained from import and elements. *)
1481 (* Now additional elements for parameters are inserted. *)
1482 val import_params_ids = make_params_ids import_params;
1483 val incl_params_ids =
1484 make_params_ids (incl_params \\ import_params);
1485 val raw_import_params_elemss =
1486 make_raw_params_elemss (import_params, incl_tenv, incl_syn);
1487 val raw_incl_params_elemss =
1488 make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
1489 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
1490 context fixed_params
1491 (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
1493 (* replace extended ids (for axioms) by ids *)
1494 val (import_ids', incl_ids) = chop (length import_ids) ids;
1495 val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
1496 val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
1497 (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
1498 (all_ids ~~ all_elemss);
1499 (* CB: all_elemss and parms contain the correct parameter types *)
1501 val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
1502 val ((import_elemss, _), import_ctxt) =
1503 activate_facts false prep_facts ps context;
1505 val ((elemss, _), ctxt) =
1506 activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
1508 ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
1509 (parms, spec, defs)), concl)
1512 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
1514 val thy = ProofContext.theory_of ctxt;
1515 val locale = Option.map (prep_locale thy) raw_locale;
1516 val (fixed_params, imports) =
1520 let val {params = ps, ...} = the_locale thy name
1521 in (map fst ps, Locale name) end);
1522 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
1523 prep_ctxt false fixed_params imports elems concl ctxt;
1524 in (locale, locale_ctxt, elems_ctxt, concl') end;
1526 fun prep_expr prep imports body ctxt =
1528 val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
1529 val all_elems = maps snd (import_elemss @ elemss);
1530 in (all_elems, ctxt') end;
1534 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
1535 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
1537 fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
1538 fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
1540 val read_expr = prep_expr read_context;
1541 val cert_expr = prep_expr cert_context;
1543 fun read_context_statement loc = prep_statement intern read_ctxt loc;
1544 fun read_context_statement_i loc = prep_statement (K I) read_ctxt loc;
1545 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
1554 #> #2 o cert_context_statement (SOME loc) [] [];
1559 fun print_locale thy show_facts imports body =
1560 let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
1561 Pretty.big_list "locale elements:" (all_elems
1562 |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
1563 |> map (Element.pretty_ctxt ctxt) |> filter_out null
1564 |> map Pretty.chunks)
1570 (** store results **)
1572 (* naming of interpreted theorems *)
1574 fun add_param_prefixss s =
1575 (map o apfst o apfst) (NameSpace.qualified s);
1576 fun drop_param_prefixss args = (map o apfst o apfst)
1577 (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
1579 fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
1581 |> Sign.qualified_names
1582 |> Sign.add_path (NameSpace.base loc ^ "_locale")
1583 |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
1584 |> PureThy.note_thmss kind (if fully_qualified then args else drop_param_prefixss args)
1585 ||> Sign.restore_naming thy;
1587 fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
1589 |> ProofContext.qualified_names
1590 |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
1591 |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
1592 |> ProofContext.note_thmss_i kind (if fully_qualified then args else drop_param_prefixss args)
1593 ||> ProofContext.restore_naming ctxt;
1596 (* join equations of an id with already accumulated ones *)
1598 fun join_eqns get_reg prep_id ctxt id eqns =
1600 val id' = prep_id id
1601 val eqns' = case get_reg id'
1603 | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
1604 handle Termtab.DUP t =>
1605 error ("Conflicting interpreting equations for term " ^
1606 quote (Syntax.string_of_term ctxt t))
1607 in ((id', eqns'), eqns') end;
1610 (* collect witnesses and equations up to a particular target for global
1611 registration; requires parameters and flattened list of identifiers
1612 instead of recomputing it from the target *)
1614 fun collect_global_witnesses thy imprt parms ids vts = let
1615 val ts = map Logic.unvarify vts;
1616 val (parms, parmTs) = split_list parms;
1617 val parmvTs = map Logic.varifyT parmTs;
1618 val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
1619 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
1621 (* replace parameter names in ids by instantiations *)
1622 val vinst = Symtab.make (parms ~~ vts);
1623 fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
1624 val inst = Symtab.make (parms ~~ ts);
1625 val inst_ids = map (apfst (apsnd vinst_names)) ids;
1626 val assumed_ids' = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
1627 val wits = maps (#2 o the o get_global_registration thy imprt) assumed_ids';
1629 val ids' = map fst inst_ids;
1631 fold_map (join_eqns (get_global_registration thy imprt) I (ProofContext.init thy))
1632 ids' Termtab.empty |> snd |> Termtab.dest |> map snd;
1633 in ((tinst, inst), wits, eqns) end;
1636 (* standardise export morphism *)
1638 (* clone from Element.generalize_facts *)
1639 fun standardize thy export facts =
1641 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
1642 val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
1643 (* FIXME sync with exp_fact *)
1644 val exp_typ = Logic.type_map exp_term;
1646 Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
1647 in Element.facts_map (Element.morph_ctxt morphism) facts end;
1650 fun morph_ctxt' phi = Element.map_ctxt
1652 var = Morphism.var phi,
1653 typ = Morphism.typ phi,
1654 term = Morphism.term phi,
1655 fact = Morphism.fact phi,
1656 attrib = Args.morph_values phi};
1659 (* compute morphism and apply to args *)
1661 fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
1663 val inst = Morphism.name_morphism (NameSpace.qualified prfx) $>
1664 (* need to add parameter prefix *) (* FIXME *)
1665 Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
1666 Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
1667 Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns)
1669 args |> Element.facts_map (morph_ctxt' inst) |>
1670 (* suppresses application of name morphism: workaroud for class package *) (* FIXME *)
1671 map (fn (attn, bs) => (attn,
1672 bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |>
1673 standardize thy exp |> Attrib.map_facts attrib
1677 (* store instantiations of args for all registered interpretations
1680 fun note_thmss_registrations target (kind, args) thy =
1682 val parms = the_locale thy target |> #params |> map fst;
1683 val ids = flatten (ProofContext.init thy, intern_expr thy)
1684 (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
1686 val regs = get_global_registrations thy target;
1687 (* add args to thy for all registrations *)
1689 fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
1691 val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
1692 val attrib = Attrib.attribute_i thy;
1694 |> interpret_args thy prfx insts prems eqns atts2 exp attrib
1695 |> add_param_prefixss (space_implode "_" (map fst parms));
1696 in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
1697 in fold activate regs thy end;
1700 (* locale results *)
1702 fun add_thmss loc kind args ctxt =
1704 val (([(_, [Notes args'])], _), ctxt') =
1705 activate_facts true cert_facts
1706 [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
1707 val ctxt'' = ctxt' |> ProofContext.theory
1709 (fn (axiom, elems, params, decls, regs, intros, dests) =>
1710 (axiom, elems @ [(Notes args', stamp ())],
1711 params, decls, regs, intros, dests))
1712 #> note_thmss_registrations loc args');
1720 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
1722 fun add_decls add loc decl =
1723 ProofContext.theory (change_locale loc
1724 (fn (axiom, elems, params, decls, regs, intros, dests) =>
1725 (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
1726 add_thmss loc Thm.internalK
1727 [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
1731 val add_type_syntax = add_decls (apfst o cons);
1732 val add_term_syntax = add_decls (apsnd o cons);
1733 val add_declaration = add_decls (K I);
1739 (** define locales **)
1741 (* predicate text *)
1742 (* CB: generate locale predicates and delta predicates *)
1746 (* introN: name of theorems for introduction rules of locale and
1748 axiomsN: name of theorem set with destruct rules for locale predicates,
1749 also name suffix of delta predicates. *)
1751 val introN = "intro";
1752 val axiomsN = "axioms";
1754 fun atomize_spec thy ts =
1756 val t = Logic.mk_conjunction_balanced ts;
1757 val body = ObjectLogic.atomize_term thy t;
1758 val bodyT = Term.fastype_of body;
1760 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
1761 else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
1764 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
1765 if length args = n then
1766 Syntax.const "_aprop" $
1767 Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
1770 (* CB: define one predicate including its intro rule and axioms
1771 - bname: predicate name
1772 - parms: locale parameters
1773 - defs: thms representing substitutions from defines elements
1774 - ts: terms representing locale assumptions (not normalised wrt. defs)
1775 - norm_ts: terms representing locale assumptions (normalised wrt. defs)
1779 fun def_pred bname parms defs ts norm_ts thy =
1781 val name = Sign.full_name thy bname;
1783 val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
1784 val env = Term.add_term_free_names (body, []);
1785 val xs = filter (member (op =) env o #1) parms;
1787 val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
1788 |> Library.sort_wrt #1 |> map TFree;
1789 val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
1791 val args = map Logic.mk_type extraTs @ map Free xs;
1792 val head = Term.list_comb (Const (name, predT), args);
1793 val statement = ObjectLogic.ensure_propT thy head;
1795 val ([pred_def], defs_thy) =
1797 |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
1798 |> Sign.declare_const [] (bname, predT, NoSyn) |> snd
1799 |> PureThy.add_defs false
1800 [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
1801 val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
1803 val cert = Thm.cterm_of defs_thy;
1805 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
1806 MetaSimplifier.rewrite_goals_tac [pred_def] THEN
1807 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
1808 Tactic.compose_tac (false,
1809 Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
1812 (Drule.equal_elim_rule2 OF [body_eq,
1813 MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
1814 |> Conjunction.elim_balanced (length ts);
1815 val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
1816 Element.prove_witness defs_ctxt t
1817 (MetaSimplifier.rewrite_goals_tac defs THEN
1818 Tactic.compose_tac (false, ax, 0) 1));
1819 in ((statement, intro, axioms), defs_thy) end;
1821 fun assumes_to_notes (Assumes asms) axms =
1822 fold_map (fn (a, spec) => fn axs =>
1823 let val (ps, qs) = chop (length spec) axs
1824 in ((a, [(ps, [])]), qs) end) asms axms
1825 |> apfst (curry Notes Thm.assumptionK)
1826 | assumes_to_notes e axms = (e, axms);
1828 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
1830 (* turn Assumes into Notes elements *)
1832 fun change_assumes_elemss axioms elemss =
1834 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
1835 fun change (id as ("", _), es) =
1836 fold_map assumes_to_notes (map satisfy es)
1837 #-> (fn es' => pair (id, es'))
1838 | change e = pair e;
1840 fst (fold_map change elemss (map Element.conclude_witness axioms))
1843 (* adjust hyps of Notes elements *)
1845 fun change_elemss_hyps axioms elemss =
1847 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
1848 fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
1850 in map change elemss end;
1854 (* CB: main predicate definition function *)
1856 fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
1858 val ((elemss', more_ts), a_elem, a_intro, thy'') =
1859 if null exts then ((elemss, []), [], [], thy)
1862 val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
1863 val ((statement, intro, axioms), thy') =
1865 |> def_pred aname parms defs exts exts';
1866 val elemss' = change_assumes_elemss axioms elemss;
1867 val a_elem = [(("", []), [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1870 |> Sign.add_path aname
1871 |> Sign.no_base_names
1872 |> PureThy.note_thmss Thm.internalK [((introN, []), [([intro], [])])]
1873 ||> Sign.restore_naming thy';
1874 in ((elemss', [statement]), a_elem, [intro], thy'') end;
1875 val (predicate, stmt', elemss'', b_intro, thy'''') =
1876 if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
1879 val ((statement, intro, axioms), thy''') =
1881 |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts);
1882 val cstatement = Thm.cterm_of thy''' statement;
1883 val elemss'' = change_elemss_hyps axioms elemss';
1884 val b_elem = [(("", []),
1885 [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1888 |> Sign.add_path pname
1889 |> Sign.no_base_names
1890 |> PureThy.note_thmss Thm.internalK
1891 [((introN, []), [([intro], [])]),
1892 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
1893 ||> Sign.restore_naming thy''';
1894 in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
1895 in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
1900 (* add_locale(_i) *)
1904 (* turn Defines into Notes elements, accumulate definition terms *)
1906 fun defines_to_notes is_ext thy (Defines defs) defns =
1908 val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
1909 val notes = map (fn (a, (def, _)) =>
1910 (a, [([assume (cterm_of thy def)], [])])) defs
1912 (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
1914 | defines_to_notes _ _ e defns = (SOME e, defns);
1916 fun change_defines_elemss thy elemss defns =
1918 fun change (id as (n, _), es) defns =
1920 val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
1921 in ((id, map_filter I es'), defns') end
1922 in fold_map change elemss defns end;
1924 fun gen_add_locale prep_ctxt prep_expr
1925 predicate_name bname raw_imports raw_body thy =
1926 (* predicate_name: "" - locale with predicate named as locale
1927 "name" - locale with predicate named "name" *)
1929 val thy_ctxt = ProofContext.init thy;
1930 val name = Sign.full_name thy bname;
1931 val _ = is_some (get_locale thy name) andalso
1932 error ("Duplicate definition of locale " ^ quote name);
1934 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
1935 text as (parms, ((_, exts'), _), defs)) =
1936 prep_ctxt raw_imports raw_body thy_ctxt;
1937 val elemss = import_elemss @ body_elemss |>
1938 map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
1940 val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
1941 List.foldr Term.add_typ_tfrees [] (map snd parms);
1942 val _ = if null extraTs then ()
1943 else warning ("Additional type variable(s) in locale specification " ^ quote bname);
1945 val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
1946 val (elemss', defns) = change_defines_elemss thy elemss [];
1947 val elemss'' = elemss' @ [(("", []), defns)];
1948 val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
1949 define_preds predicate_name' text elemss'' thy;
1950 val regs = pred_axioms
1951 |> fold_map (fn (id, elems) => fn wts => let
1952 val ts = flat (map_filter (fn (Assumes asms) =>
1953 SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
1954 val (wts1, wts2) = chop (length ts) wts;
1955 in ((apsnd (map fst) id, wts1), wts2) end) elemss'''
1957 |> map_filter (fn (("", _), _) => NONE | e => SOME e);
1958 fun axiomify axioms elemss =
1959 (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
1960 val ts = flat (map_filter (fn (Assumes asms) =>
1961 SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
1962 val (axs1, axs2) = chop (length ts) axs;
1963 in (axs2, ((id, Assumed axs1), elems)) end)
1965 val ((_, facts), ctxt) = activate_facts true (K I)
1966 (axiomify pred_axioms elemss''') (ProofContext.init thy');
1967 val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
1968 val export = Thm.close_derivation o Goal.norm_result o
1969 singleton (ProofContext.export view_ctxt thy_ctxt);
1970 val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
1971 val elems' = maps #2 (filter (equal "" o #1 o #1) elemss''');
1972 val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
1973 val axs' = map (Element.assume_witness thy') stmt';
1975 |> Sign.add_path bname
1976 |> Sign.no_base_names
1977 |> PureThy.note_thmss Thm.assumptionK facts' |> snd
1978 |> Sign.restore_naming thy'
1979 |> register_locale name {axiom = axs',
1980 elems = map (fn e => (e, stamp ())) elems'',
1981 params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
1985 dests = map Element.conclude_witness pred_axioms}
1987 in (name, loc_ctxt) end;
1991 val add_locale = gen_add_locale read_context intern_expr;
1992 val add_locale_i = gen_add_locale cert_context (K I);
1996 val _ = Context.>> (Context.map_theory
1997 (add_locale_i "" "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
1998 snd #> ProofContext.theory_of #>
1999 add_locale_i "" "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
2000 snd #> ProofContext.theory_of));
2005 (** Normalisation of locale statements ---
2006 discharges goals implied by interpretations **)
2010 fun locale_assm_intros thy =
2011 Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
2012 (#2 (LocalesData.get thy)) [];
2013 fun locale_base_intros thy =
2014 Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
2015 (#2 (LocalesData.get thy)) [];
2017 fun all_witnesses ctxt =
2019 val thy = ProofContext.theory_of ctxt;
2020 fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
2021 (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) =>
2022 map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms)
2024 in get (RegistrationsData.get (Context.Proof ctxt)) end;
2028 fun intro_locales_tac eager ctxt facts st =
2030 val wits = all_witnesses ctxt;
2031 val thy = ProofContext.theory_of ctxt;
2032 val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
2034 Method.intros_tac (wits @ intros) facts st
2037 val _ = Context.>> (Context.map_theory
2040 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
2041 "back-chain introduction rules of locales without unfolding predicates"),
2043 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
2044 "back-chain all introduction rules of locales")]));
2049 (** Interpretation commands **)
2053 (* extract proof obligations (assms and defs) from elements *)
2055 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
2056 | extract_asms_elems ((id, Derived _), _) = (id, []);
2059 (* activate instantiated facts in theory or context *)
2062 TableFun(type key = string * term list
2063 val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
2065 fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn
2066 attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
2068 val ctxt = mk_ctxt thy_ctxt;
2069 val (all_propss, eq_props) = chop (length all_elemss) propss;
2070 val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
2072 (* Filter out fragments already registered. *)
2074 val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
2075 test_reg thy_ctxt id) (all_elemss ~~ (all_propss ~~ all_thmss)));
2076 val (new_propss, new_thmss) = split_list xs;
2078 val thy_ctxt' = thy_ctxt
2079 (* add registrations *)
2080 (* |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *)
2081 |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss
2082 (* add witnesses of Assumed elements (only those generate proof obligations) *)
2083 |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
2085 |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
2086 (map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
2087 Element.conclude_witness) eq_thms);
2089 val prems = flat (map_filter
2090 (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
2091 | ((_, Derived _), _) => NONE) all_elemss);
2093 fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
2095 val ctxt = mk_ctxt thy_ctxt;
2096 val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
2097 (Symtab.empty, Symtab.empty) prems eqns atts
2098 exp (attrib thy_ctxt) facts;
2099 in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
2100 | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
2102 fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
2104 val (prfx_atts, _, _) = case get_reg thy_ctxt imp id
2106 | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
2107 ^ " while activating facts.");
2108 in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end;
2110 val thy_ctxt'' = thy_ctxt'
2111 (* add witnesses of Derived elements *)
2112 |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
2113 (map_filter (fn ((_, Assumed _), _) => NONE
2114 | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
2116 (* Accumulate equations *)
2118 fold_map (join_eqns (get_reg thy_ctxt'' imp) fst ctxt) all_propss Termtab.empty
2120 |> map (apsnd (map snd o Termtab.dest))
2121 |> (fn xs => fold Idtab.update xs Idtab.empty)
2122 (* Idtab.make wouldn't work here: can have conflicting duplicates,
2123 because instantiation may equate ids and equations are accumulated! *)
2128 |> fold (fn (attns, thms) =>
2129 fold (fn (attn, thm) => note "lemma"
2130 [(apsnd (map (attrib thy_ctxt'')) attn,
2131 [([Element.conclude_witness thm], [])])] #> snd)
2132 (attns ~~ thms)) (unflat eq_thms eq_attns ~~ eq_thms)
2134 |> fold (activate_elems all_eqns) new_elemss
2137 fun global_activate_facts_elemss x = gen_activate_facts_elemss
2139 get_global_registration
2141 global_note_prefix_i
2143 put_global_registration test_global_registration add_global_witness add_global_equation
2146 fun local_activate_facts_elemss x = gen_activate_facts_elemss
2148 get_local_registration
2149 ProofContext.note_thmss_i
2151 (Attrib.attribute_i o ProofContext.theory_of)
2152 put_local_registration
2153 test_local_registration
2158 fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
2161 val (parm_names, parm_types) = parms |> split_list
2162 ||> map (TypeInfer.paramify_vars o Logic.varifyT);
2163 val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar);
2164 val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
2166 (* parameter instantiations *)
2167 val d = length parms - length insts;
2169 if d < 0 then error "More arguments than parameters in instantiation."
2170 else insts @ replicate d NONE;
2171 val (given_ps, given_insts) =
2172 ((parm_names ~~ parm_types) ~~ insts) |> map_filter
2173 (fn (_, NONE) => NONE
2174 | ((n, T), SOME inst) => SOME ((n, T), inst))
2176 val (given_parm_names, given_parm_types) = given_ps |> split_list;
2178 (* parse insts / eqns *)
2179 val given_insts' = map (parse_term ctxt) given_insts;
2180 val eqns' = map (parse_prop ctxt) eqns;
2182 (* type inference and contexts *)
2183 val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns';
2184 val res = Syntax.check_terms ctxt arg;
2185 val ctxt' = ctxt |> fold Variable.auto_fixes res;
2188 val (type_parms'', res') = chop (length type_parms) res;
2189 val (given_insts'', eqns'') = chop (length given_insts) res';
2190 val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
2191 val inst = Symtab.make (given_parm_names ~~ given_insts'');
2193 (* export from eigencontext *)
2194 val export = Variable.export_morphism ctxt' ctxt;
2196 (* import, its inverse *)
2197 val domT = fold Term.add_tfrees res [] |> map TFree;
2198 val importT = domT |> map (fn x => (Morphism.typ export x, x))
2199 |> map_filter (fn (TFree _, _) => NONE (* fixed point of export *)
2200 | (TVar y, x) => SOME (fst y, x)
2201 | _ => error "internal: illegal export in interpretation")
2203 val dom = fold Term.add_frees res [] |> map Free;
2204 val imprt = dom |> map (fn x => (Morphism.term export x, x))
2205 |> map_filter (fn (Free _, _) => NONE (* fixed point of export *)
2206 | (Var y, x) => SOME (fst y, x)
2207 | _ => error "internal: illegal export in interpretation")
2209 in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end;
2211 val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
2212 val check_instantiations = prep_instantiations (K I) (K I);
2214 fun gen_prep_registration mk_ctxt test_reg activate
2215 prep_attr prep_expr prep_insts
2216 thy_ctxt raw_attn raw_expr raw_insts =
2218 val ctxt = mk_ctxt thy_ctxt;
2219 val thy = ProofContext.theory_of ctxt;
2220 val ctxt' = ProofContext.init thy;
2221 fun prep_attn attn = (apsnd o map)
2222 (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
2224 val attn = prep_attn raw_attn;
2225 val expr = prep_expr thy raw_expr;
2227 val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
2228 val params_ids = make_params_ids (#1 pts);
2229 val raw_params_elemss = make_raw_params_elemss pts;
2230 val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr);
2231 val ((parms, all_elemss, _), (_, (_, defs, _))) =
2232 read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
2234 (** compute instantiation **)
2236 (* consistency check: equations need to be stored in a particular locale,
2237 therefore if equations are present locale expression must be a name *)
2239 val _ = case (expr, snd raw_insts) of
2240 (Locale _, _) => () | (_, []) => ()
2241 | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
2243 (* read or certify instantiation *)
2244 val (raw_insts', raw_eqns) = raw_insts;
2245 val (raw_eq_attns, raw_eqns') = split_list raw_eqns;
2246 val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns');
2247 val eq_attns = map prep_attn raw_eq_attns;
2249 (* defined params without given instantiation *)
2250 val not_given = filter_out (Symtab.defined inst1 o fst) parms;
2251 fun add_def (p, pT) inst =
2253 val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
2254 NONE => error ("Instance missing for parameter " ^ quote p)
2255 | SOME (Free (_, T), t) => (t, T);
2256 val d = Element.inst_term (instT, inst) t;
2257 in Symtab.update_new (p, d) inst end;
2258 val inst2 = fold add_def not_given inst1;
2259 val inst_morphism = Element.inst_morphism thy (instT, inst2);
2260 (* Note: insts contain no vars. *)
2262 (** compute proof obligations **)
2264 (* restore "small" ids *)
2265 val ids' = map (fn ((n, ps), (_, mode)) =>
2266 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
2268 val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
2269 (* instantiate ids and elements *)
2270 val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
2271 ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
2272 map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
2273 |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
2276 val eqn_elems = if null eqns then []
2277 else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
2279 val propss = map extract_asms_elems inst_elemss @ eqn_elems;
2281 in (propss, activate attn inst_elemss propss eq_attns morphs) end;
2283 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
2284 test_global_registration
2285 global_activate_facts_elemss mk_ctxt;
2287 fun gen_prep_local_registration mk_ctxt = gen_prep_registration I
2288 test_local_registration
2289 local_activate_facts_elemss mk_ctxt;
2291 val prep_global_registration = gen_prep_global_registration
2292 Attrib.intern_src intern_expr read_instantiations;
2293 val prep_global_registration_i = gen_prep_global_registration
2294 (K I) (K I) check_instantiations;
2296 val prep_local_registration = gen_prep_local_registration
2297 Attrib.intern_src intern_expr read_instantiations;
2298 val prep_local_registration_i = gen_prep_local_registration
2299 (K I) (K I) check_instantiations;
2301 fun prep_registration_in_locale target expr thy =
2302 (* target already in internal form *)
2304 val ctxt = ProofContext.init thy;
2305 val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
2306 (([], Symtab.empty), Expr (Locale target));
2307 val fixed = the_locale thy target |> #params |> map #1;
2308 val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
2309 ((raw_target_ids, target_syn), Expr expr);
2310 val (target_ids, ids) = chop (length raw_target_ids) all_ids;
2311 val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
2313 (** compute proof obligations **)
2315 (* restore "small" ids, with mode *)
2316 val ids' = map (apsnd snd) ids;
2317 (* remove Int markers *)
2318 val elemss' = map (fn (_, es) =>
2319 map (fn Int e => e) es) elemss
2320 (* extract assumptions and defs *)
2321 val ids_elemss = ids' ~~ elemss';
2322 val propss = map extract_asms_elems ids_elemss;
2324 (** activation function:
2325 - add registrations to the target locale
2326 - add induced registrations for all global registrations of
2327 the target, unless already present
2328 - add facts of induced registrations to theory **)
2330 fun activate thmss thy = let
2331 val satisfy = Element.satisfy_thm (flat thmss);
2332 val ids_elemss_thmss = ids_elemss ~~ thmss;
2333 val regs = get_global_registrations thy target;
2335 fun activate_id (((id, Assumed _), _), thms) thy =
2336 thy |> put_registration_in_locale target id
2337 |> fold (add_witness_in_locale target id) thms
2338 | activate_id _ thy = thy;
2340 fun activate_reg (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy =
2342 val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts;
2343 fun inst_parms ps = map
2344 (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
2345 val disch = Element.satisfy_thm wits;
2346 val new_elemss = filter (fn (((name, ps), _), _) =>
2347 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
2348 fun activate_assumed_id (((_, Derived _), _), _) thy = thy
2349 | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
2350 val ps' = inst_parms ps;
2352 if test_global_registration thy (name, ps')
2355 |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
2356 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2357 (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
2360 fun activate_derived_id ((_, Assumed _), _) thy = thy
2361 | activate_derived_id (((name, ps), Derived ths), _) thy = let
2362 val ps' = inst_parms ps;
2364 if test_global_registration thy (name, ps')
2367 |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp)
2368 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2369 (witn |> Element.map_witness (fn (t, th) => (* FIXME *)
2370 (Element.inst_term insts t,
2371 disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
2374 fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
2377 Morphism.name_morphism (NameSpace.qualified prfx) $>
2378 Morphism.thm_morphism satisfy $>
2379 Element.inst_morphism thy insts $>
2380 Morphism.thm_morphism disch;
2382 |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
2383 |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
2384 |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
2387 |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
2390 | activate_elem _ _ thy = thy;
2392 fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
2394 in thy |> fold activate_assumed_id ids_elemss_thmss
2395 |> fold activate_derived_id ids_elemss
2396 |> fold activate_elems new_elemss end;
2398 thy |> fold activate_id ids_elemss_thmss
2399 |> fold activate_reg regs
2402 in (propss, activate) end;
2404 fun prep_propp propss = propss |> map (fn (_, props) =>
2405 map (rpair [] o Element.mark_witness) props);
2407 fun prep_result propps thmss =
2408 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
2410 fun gen_interpretation prep_registration after_qed (prfx, raw_atts) raw_expr raw_insts thy =
2411 (* prfx = (flag indicating full qualification, name prefix) *)
2413 val (propss, activate) = prep_registration thy (prfx, raw_atts) raw_expr raw_insts;
2414 fun after_qed' results =
2415 ProofContext.theory (activate (prep_result propss results))
2419 |> ProofContext.init
2420 |> Proof.theorem_i NONE after_qed' (prep_propp propss)
2421 |> Element.refine_witness
2425 fun gen_interpret prep_registration after_qed (prfx, atts) expr insts int state =
2426 (* prfx = (flag indicating full qualification, name prefix) *)
2428 val _ = Proof.assert_forward_or_chain state;
2429 val ctxt = Proof.context_of state;
2430 val (propss, activate) = prep_registration ctxt (prfx, atts) expr insts;
2431 fun after_qed' results =
2432 Proof.map_context (K (ctxt |> activate (prep_result propss results)))
2433 #> Proof.put_facts NONE
2437 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
2438 "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
2439 |> Element.refine_witness |> Seq.hd
2444 val interpretation_i = gen_interpretation prep_global_registration_i;
2445 val interpretation = gen_interpretation prep_global_registration;
2448 fun interpretation_in_locale after_qed (raw_target, expr) thy =
2450 val target = intern thy raw_target;
2451 val (propss, activate) = prep_registration_in_locale target expr thy;
2452 val raw_propp = prep_propp propss;
2454 val (_, _, goal_ctxt, propp) = thy
2455 |> ProofContext.init
2456 |> cert_context_statement (SOME target) [] raw_propp;
2458 fun after_qed' results =
2459 ProofContext.theory (activate (prep_result propss results))
2463 |> Proof.theorem_i NONE after_qed' propp
2464 |> Element.refine_witness |> Seq.hd
2467 val interpret_i = gen_interpret prep_local_registration_i;
2468 val interpret = gen_interpret prep_local_registration;