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 extern: theory -> string -> xstring
49 val init: string -> theory -> Proof.context
51 (* 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
62 (* Processing of locale statements *)
63 val read_context_statement: xstring option -> Element.context element list ->
64 (string * string list) list list -> Proof.context ->
65 string option * Proof.context * Proof.context * (term * term list) list list
66 val read_context_statement_i: string option -> Element.context element list ->
67 (string * string list) list list -> Proof.context ->
68 string option * Proof.context * Proof.context * (term * term list) list list
69 val cert_context_statement: string option -> Element.context_i element list ->
70 (term * term list) list list -> Proof.context ->
71 string option * Proof.context * Proof.context * (term * term list) list list
72 val read_expr: expr -> Element.context list -> Proof.context ->
73 Element.context_i list * Proof.context
74 val cert_expr: expr -> Element.context_i list -> Proof.context ->
75 Element.context_i list * Proof.context
77 (* Diagnostic functions *)
78 val print_locales: theory -> unit
79 val print_locale: theory -> bool -> expr -> Element.context list -> unit
80 val print_global_registrations: bool -> string -> theory -> unit
81 val print_local_registrations': bool -> string -> Proof.context -> unit
82 val print_local_registrations: bool -> string -> Proof.context -> unit
84 val add_locale: bool -> bstring -> expr -> Element.context list -> theory
85 -> string * Proof.context
86 val add_locale_i: bool -> 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 -> (morphism -> Context.generic -> Context.generic) ->
97 Proof.context -> Proof.context
98 val add_term_syntax: string -> (morphism -> Context.generic -> Context.generic) ->
99 Proof.context -> Proof.context
100 val add_declaration: string -> (morphism -> Context.generic -> Context.generic) ->
101 Proof.context -> Proof.context
103 val interpretation: (Proof.context -> Proof.context) ->
104 string * Attrib.src list -> expr -> string option list ->
105 theory -> Proof.state
106 val interpretation_in_locale: (Proof.context -> Proof.context) ->
107 xstring * expr -> theory -> Proof.state
108 val interpret: (Proof.state -> Proof.state Seq.seq) ->
109 string * Attrib.src list -> expr -> string option list ->
110 bool -> Proof.state -> Proof.state
113 structure Locale: LOCALE =
116 fun legacy_unvarifyT thm =
118 val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
119 val tvars = rev (Drule.fold_terms Term.add_tvars thm []);
120 val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
121 in Drule.instantiate' tfrees [] thm end;
123 fun legacy_unvarify raw_thm =
125 val thm = legacy_unvarifyT raw_thm;
126 val ct = Thm.cterm_of (Thm.theory_of_thm thm);
127 val vars = rev (Drule.fold_terms Term.add_vars thm []);
128 val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
129 in Drule.instantiate' [] frees thm end;
132 (** locale elements and expressions **)
134 datatype ctxt = datatype Element.ctxt;
138 Rename of expr * (string * mixfix option) option list |
141 val empty = Merge [];
143 datatype 'a element =
144 Elem of 'a | Expr of expr;
146 fun map_elem f (Elem e) = Elem (f e)
147 | map_elem _ (Expr e) = Expr e;
149 type decl = (morphism -> Context.generic -> Context.generic) * stamp;
152 {axiom: Element.witness list,
153 (* For locales that define predicates this is [A [A]], where A is the locale
154 specification. Otherwise [].
155 Only required to generate the right witnesses for locales with predicates. *)
156 import: expr, (*dynamic import*)
157 elems: (Element.context_i * stamp) list,
158 (* Static content, neither Fixes nor Constrains elements *)
159 params: ((string * typ) * mixfix) list, (*all params*)
160 lparams: string list, (*local params*)
161 decls: decl list * decl list, (*type/term_syntax declarations*)
162 regs: ((string * string list) * Element.witness list) list,
163 (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
164 intros: thm list * thm list}
165 (* Introduction rules: of delta predicate and locale predicate. *)
167 (* CB: an internal (Int) locale element was either imported or included,
168 an external (Ext) element appears directly in the locale text. *)
170 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
174 (** management of registrations in theories and proof contexts **)
176 structure Registrations :
181 val dest: theory -> T ->
182 (term list * ((string * Attrib.src list) * Element.witness list)) list
183 val lookup: theory -> T * term list ->
184 ((string * Attrib.src list) * Element.witness list) option
185 val insert: theory -> term list * (string * Attrib.src list) -> T ->
186 T * (term list * ((string * Attrib.src list) * Element.witness list)) list
187 val add_witness: term list -> Element.witness -> T -> T
190 (* a registration consists of theorems (actually, witnesses) instantiating locale
191 assumptions and prefix and attributes, indexed by parameter instantiation *)
192 type T = ((string * Attrib.src list) * Element.witness list) Termtab.table;
194 val empty = Termtab.empty;
196 (* term list represented as single term, for simultaneous matching *)
198 Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
200 let fun ut (Const _) ts = ts
201 | ut (s $ t) ts = ut s (t::ts)
204 (* joining of registrations: prefix and attributes of left theory,
205 thms are equal, no attempt to subsumption testing *)
206 fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);
208 fun dest_transfer thy regs =
209 Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy))));
211 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
213 (* registrations that subsume t *)
214 fun subsumers thy t regs =
215 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
217 (* look up registration, pick one that subsumes the query *)
218 fun lookup thy (regs, ts) =
221 val subs = subsumers thy t regs;
225 | ((t', (attn, thms)) :: _) =>
227 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
228 (* thms contain Frees, not Vars *)
229 val tinst' = tinst |> Vartab.dest (* FIXME Vartab.map (!?) *)
230 |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
232 val inst' = inst |> Vartab.dest
233 |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
235 val inst_witness = Element.morph_witness (Element.inst_morphism thy (tinst', inst'));
236 in SOME (attn, map inst_witness thms) end)
239 (* add registration if not subsumed by ones already present,
240 additionally returns registrations that are strictly subsumed *)
241 fun insert thy (ts, attn) regs =
244 val subs = subsumers thy t regs ;
248 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
249 val sups' = map (apfst untermify) sups
250 in (Termtab.update (t, (attn, [])) regs, sups') end
254 (* add witness theorem to registration,
255 only if instantiation is exact, otherwise exception Option raised *)
256 fun add_witness ts thm regs =
259 val (x, thms) = the (Termtab.lookup regs t);
261 Termtab.update (t, (x, thm::thms)) regs
268 structure GlobalLocalesData = TheoryDataFun
270 val name = "Isar/locales";
271 type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
272 (* 1st entry: locale namespace,
273 2nd entry: locales of the theory,
274 3rd entry: registrations, indexed by locale name *)
276 val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
281 ({axiom, import, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale,
282 {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
285 elems = gen_merge_lists (eq_snd (op =)) elems elems',
289 (Library.merge (eq_snd (op =)) (decls1, decls1'),
290 Library.merge (eq_snd (op =)) (decls2, decls2')),
291 regs = merge_alists regs regs',
293 fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
294 (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
295 Symtab.join (K Registrations.join) (regs1, regs2));
297 fun print _ (space, locs, _) =
298 Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
302 val _ = Context.add_setup GlobalLocalesData.init;
308 structure LocalLocalesData = ProofDataFun
310 val name = "Isar/locales";
311 type T = Registrations.T Symtab.table;
312 (* registrations, indexed by locale name *)
313 fun init _ = Symtab.empty;
317 val _ = Context.add_setup LocalLocalesData.init;
322 val print_locales = GlobalLocalesData.print;
324 val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
325 val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
327 fun declare_locale name thy =
328 thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
329 (Sign.declare_name thy name space, locs, regs));
331 fun put_locale name loc =
332 GlobalLocalesData.map (fn (space, locs, regs) =>
333 (space, Symtab.update (name, loc) locs, regs));
335 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;
337 fun the_locale thy name =
338 (case get_locale thy name of
340 | NONE => error ("Unknown locale " ^ quote name));
342 fun change_locale name f thy =
344 val {axiom, import, elems, params, lparams, decls, regs, intros} =
346 val (axiom', import', elems', params', lparams', decls', regs', intros') =
347 f (axiom, import, elems, params, lparams, decls, regs, intros);
349 put_locale name {axiom = axiom', import = import', elems = elems',
350 params = params', lparams = lparams', decls = decls', regs = regs',
351 intros = intros'} thy
355 (* access registrations *)
357 (* Ids of global registrations are varified,
358 Ids of local registrations are not.
359 Thms of registrations are never varified. *)
361 (* retrieve registration from theory or context *)
363 fun gen_get_registrations get thy_of thy_ctxt name =
364 case Symtab.lookup (get thy_ctxt) name of
366 | SOME reg => Registrations.dest (thy_of thy_ctxt) reg;
368 val get_global_registrations =
369 gen_get_registrations (#3 o GlobalLocalesData.get) I;
370 val get_local_registrations =
371 gen_get_registrations LocalLocalesData.get ProofContext.theory_of;
373 fun gen_get_registration get thy_of thy_ctxt (name, ps) =
374 case Symtab.lookup (get thy_ctxt) name of
376 | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
378 val get_global_registration =
379 gen_get_registration (#3 o GlobalLocalesData.get) I;
380 val get_local_registration =
381 gen_get_registration LocalLocalesData.get ProofContext.theory_of;
383 val test_global_registration = is_some oo get_global_registration;
384 val test_local_registration = is_some oo get_local_registration;
385 fun smart_test_registration ctxt id =
387 val thy = ProofContext.theory_of ctxt;
389 test_global_registration thy id orelse test_local_registration ctxt id
393 (* add registration to theory or context, ignored if subsumed *)
395 fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
398 val thy = thy_of thy_ctxt;
399 val reg = the_default Registrations.empty (Symtab.lookup regs name);
400 val (reg', sups) = Registrations.insert thy (ps, attn) reg;
401 val _ = if not (null sups) then warning
402 ("Subsumed interpretation(s) of locale " ^
403 quote (extern thy name) ^
404 "\nby interpretation(s) with the following prefix(es):\n" ^
405 commas_quote (map (fn (_, ((s, _), _)) => s) sups))
407 in Symtab.update (name, reg') regs end) thy_ctxt;
409 val put_global_registration =
410 gen_put_registration (fn f =>
411 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
412 val put_local_registration =
413 gen_put_registration LocalLocalesData.map ProofContext.theory_of;
415 fun put_registration_in_locale name id =
416 change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
417 (axiom, import, elems, params, lparams, decls, regs @ [(id, [])], intros));
420 (* add witness theorem to registration in theory or context,
421 ignored if registration not present *)
423 fun add_witness (name, ps) thm =
424 Symtab.map_entry name (Registrations.add_witness ps thm);
426 fun add_global_witness id thm =
427 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
429 val add_local_witness = LocalLocalesData.map oo add_witness;
431 fun add_witness_in_locale name id thm =
432 change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
434 fun add (id', thms) =
435 if id = id' then (id', thm :: thms) else (id', thms);
436 in (axiom, import, elems, params, lparams, decls, map add regs, intros) end);
439 (* printing of registrations *)
441 fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
443 val ctxt = mk_ctxt thy_ctxt;
444 val thy = ProofContext.theory_of ctxt;
446 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
448 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
449 fun prt_attn (prfx, atts) =
450 Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
451 fun prt_witns witns = Pretty.enclose "[" "]"
452 (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
453 fun prt_reg (ts, (("", []), witns)) =
455 then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
457 | prt_reg (ts, (attn, witns)) =
459 then Pretty.block ((prt_attn attn @
460 [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
462 else Pretty.block ((prt_attn attn @
463 [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
465 val loc_int = intern thy loc;
466 val regs = get_regs thy_ctxt;
467 val loc_regs = Symtab.lookup regs loc_int;
470 NONE => Pretty.str ("no interpretations in " ^ msg)
472 val r' = Registrations.dest thy r;
473 val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
474 in Pretty.big_list ("interpretations in " ^ msg ^ ":")
480 val print_global_registrations =
481 gen_print_registrations (#3 o GlobalLocalesData.get)
482 ProofContext.init "theory";
483 val print_local_registrations' =
484 gen_print_registrations LocalLocalesData.get
486 fun print_local_registrations show_wits loc ctxt =
487 (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
488 print_local_registrations' show_wits loc ctxt);
493 fun err_in_locale ctxt msg ids =
495 val thy = ProofContext.theory_of ctxt;
496 fun prt_id (name, parms) =
497 [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
498 val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
500 if forall (equal "" o #1) ids then msg
501 else msg ^ "\n" ^ Pretty.string_of (Pretty.block
502 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
503 in error err_msg end;
505 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
508 fun pretty_ren NONE = Pretty.str "_"
509 | pretty_ren (SOME (x, NONE)) = Pretty.str x
510 | pretty_ren (SOME (x, SOME syn)) =
511 Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
513 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
514 | pretty_expr thy (Rename (expr, xs)) =
515 Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
516 | pretty_expr thy (Merge es) =
517 Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
519 fun err_in_expr _ msg (Merge []) = error msg
520 | err_in_expr ctxt msg expr =
521 error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
522 [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
523 pretty_expr (ProofContext.theory_of ctxt) expr]));
526 (** structured contexts: rename + merge + implicit type instantiation **)
528 (* parameter types *)
530 fun frozen_tvars ctxt Ts =
531 #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
532 |> map (fn ((xi, S), T) => (xi, (S, T)));
534 fun unify_frozen ctxt maxidx Ts Us =
536 fun paramify NONE i = (NONE, i)
537 | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
539 val (Ts', maxidx') = fold_map paramify Ts maxidx;
540 val (Us', maxidx'') = fold_map paramify Us maxidx';
541 val thy = ProofContext.theory_of ctxt;
543 fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
544 handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
546 val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
547 val Vs = map (Option.map (Envir.norm_type unifier)) Us';
548 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
549 in map (Option.map (Envir.norm_type unifier')) Vs end;
551 fun params_of elemss =
552 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
554 fun params_of' elemss =
555 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
558 fun params_prefix params = space_implode "_" params;
561 (* CB: param_types has the following type:
562 ('a * 'b option) list -> ('a * 'b) list *)
563 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
566 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
567 handle Symtab.DUPS xs => err_in_locale ctxt
568 ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
571 (* Distinction of assumed vs. derived identifiers.
572 The former may have axioms relating assumptions of the context to
573 assumptions of the specification fragment (for locales with
574 predicates). The latter have witnesses relating assumptions of the
575 specification fragment to assumptions of other (assumed) specification
578 datatype 'a mode = Assumed of 'a | Derived of 'a;
580 fun map_mode f (Assumed x) = Assumed (f x)
581 | map_mode f (Derived x) = Derived (f x);
584 (* flatten expressions *)
588 fun unify_parms ctxt fixed_parms raw_parmss =
590 val thy = ProofContext.theory_of ctxt;
591 val maxidx = length raw_parmss;
592 val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
594 fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
595 fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
596 val parms = fixed_parms @ maps varify_parms idx_parmss;
598 fun unify T U envir = Sign.typ_unify thy (U, T) envir
599 handle Type.TUNIFY =>
600 let val prt = Sign.string_of_typ thy in
601 raise TYPE ("unify_parms: failed to unify types " ^
602 prt U ^ " and " ^ prt T, [U, T], [])
604 fun unify_list (T :: Us) = fold (unify T) Us
606 val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
607 (Vartab.empty, maxidx);
609 val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
610 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
612 fun inst_parms (i, ps) =
613 foldr Term.add_typ_tfrees [] (map_filter snd ps)
614 |> map_filter (fn (a, S) =>
615 let val T = Envir.norm_type unifier' (TVar ((a, i), S))
616 in if T = TFree (a, S) then NONE else SOME (a, T) end)
618 in map inst_parms idx_parmss end;
622 fun unify_elemss _ _ [] = []
623 | unify_elemss _ [] [elems] = [elems]
624 | unify_elemss ctxt fixed_parms elemss =
626 val thy = ProofContext.theory_of ctxt;
627 val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
628 |> map (Element.instT_morphism thy);
629 fun inst ((((name, ps), mode), elems), phi) =
630 (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
631 map_mode (map (Element.morph_witness phi)) mode),
632 map (Element.morph_ctxt phi) elems);
633 in map inst (elemss ~~ phis) end;
636 fun renaming xs parms = zip_options parms xs
637 handle Library.UnequalLengths =>
638 error ("Too many arguments in renaming: " ^
639 commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
643 Compute parameters (with types and syntax) of locale expression.
646 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
648 val thy = ProofContext.theory_of ctxt;
650 fun merge_tenvs fixed tenv1 tenv2 =
652 val [env1, env2] = unify_parms ctxt fixed
653 [tenv1 |> Symtab.dest |> map (apsnd SOME),
654 tenv2 |> Symtab.dest |> map (apsnd SOME)]
656 Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
657 Symtab.map (Element.instT_type env2) tenv2)
660 fun merge_syn expr syn1 syn2 =
661 Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
662 handle Symtab.DUPS xs => err_in_expr ctxt
663 ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
665 fun params_of (expr as Locale name) =
667 val {import, params, ...} = the_locale thy name;
668 val parms = map (fst o fst) params;
669 val (parms', types', syn') = params_of import;
670 val all_parms = merge_lists parms' parms;
671 val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
672 val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
673 in (all_parms, all_types, all_syn) end
674 | params_of (expr as Rename (e, xs)) =
676 val (parms', types', syn') = params_of e;
677 val ren = renaming xs parms';
678 (* renaming may reduce number of parameters *)
679 val new_parms = map (Element.rename ren) parms' |> distinct (op =);
680 val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
681 val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
682 handle Symtab.DUP x =>
683 err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
684 val syn_types = map (apsnd (fn mx => SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))))) (Symtab.dest new_syn);
685 val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
686 val (env :: _) = unify_parms ctxt []
687 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
688 val new_types = fold (Symtab.insert (op =))
689 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
690 in (new_parms, new_types, new_syn) end
691 | params_of (Merge es) =
692 fold (fn e => fn (parms, types, syn) =>
694 val (parms', types', syn') = params_of e
696 (merge_lists parms parms', merge_tenvs [] types types',
697 merge_syn e syn syn')
699 es ([], Symtab.empty, Symtab.empty)
701 val (parms, types, syn) = params_of expr;
703 (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
704 merge_syn expr prev_syn syn)
707 fun make_params_ids params = [(("", params), ([], Assumed []))];
708 fun make_raw_params_elemss (params, tenv, syn) =
709 [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
710 Int [Fixes (map (fn p =>
711 (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
715 Extend list of identifiers by those new in locale expression expr.
716 Compute corresponding list of lists of locale elements (one entry per
719 Identifiers represent locale fragments and are in an extended form:
720 ((name, ps), (ax_ps, axs))
721 (name, ps) is the locale name with all its parameters.
722 (ax_ps, axs) is the locale axioms with its parameters;
723 axs are always taken from the top level of the locale hierarchy,
724 hence axioms may contain additional parameters from later fragments:
725 ps subset of ax_ps. axs is either singleton or empty.
727 Elements are enriched by identifier-like information:
728 (((name, ax_ps), axs), elems)
729 The parameters in ax_ps are the axiom parameters, but enriched by type
730 info: now each entry is a pair of string and typ option. Axioms are
735 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
737 val thy = ProofContext.theory_of ctxt;
739 fun rename_parms top ren ((name, ps), (parms, mode)) =
740 ((name, map (Element.rename ren) ps),
742 then (map (Element.rename ren) parms,
743 map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
746 (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
748 fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
749 if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
750 then (wits, ids, visited)
753 val {params, regs, ...} = the_locale thy name;
754 val pTs' = map #1 params;
755 val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
756 (* dummy syntax, since required by rename *)
757 val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
758 val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
759 (* propagate parameter types, to keep them consistent *)
760 val regs' = map (fn ((name, ps), wits) =>
761 ((name, map (Element.rename ren) ps),
762 map (Element.transfer_witness thy) wits)) regs;
763 val new_regs = regs';
764 val new_ids = map fst new_regs;
766 map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
768 val new_wits = new_regs |> map (#2 #> map
769 (Element.morph_witness
770 (Element.instT_morphism thy env $>
771 Element.rename_morphism ren $>
772 Element.satisfy_morphism wits)));
773 val new_ids' = map (fn (id, wits) =>
774 (id, ([], Derived wits))) (new_ids ~~ new_wits);
775 val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
776 ((n, pTs), mode)) (new_idTs ~~ new_ids');
777 val new_id = ((name, map #1 pTs), ([], mode));
778 val (wits', ids', visited') = fold add_with_regs new_idTs'
779 (wits @ flat new_wits, ids, visited @ [new_id]);
781 (wits', ids' @ [new_id], visited')
784 (* distribute top-level axioms over assumed ids *)
786 fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
788 val {elems, ...} = the_locale thy name;
790 (fn (Assumes asms, _) => maps (map #1 o #2) asms
793 val (axs1, axs2) = chop (length ts) axioms;
794 in (((name, parms), (all_ps, Assumed axs1)), axs2) end
795 | axiomify all_ps (id, (_, Derived ths)) axioms =
796 ((id, (all_ps, Derived ths)), axioms);
798 (* identifiers of an expression *)
800 fun identify top (Locale name) =
801 (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
802 where name is a locale name, ps a list of parameter names and axs
803 a list of axioms relating to the identifier, axs is empty unless
804 identify at top level (top = true);
805 parms is accumulated list of parameters *)
807 val {axiom, import, params, ...} = the_locale thy name;
808 val ps = map (#1 o #1) params;
809 val (ids', parms') = identify false import;
810 (* acyclic import dependencies *)
812 val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
813 val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
814 in (ids_ax, merge_lists parms' ps) end
815 | identify top (Rename (e, xs)) =
817 val (ids', parms') = identify top e;
818 val ren = renaming xs parms'
819 handle ERROR msg => err_in_locale' ctxt msg ids';
821 val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
822 val parms'' = distinct (op =) (maps (#2 o #1) ids'');
823 in (ids'', parms'') end
824 | identify top (Merge es) =
825 fold (fn e => fn (ids, parms) =>
827 val (ids', parms') = identify top e
829 (merge_alists ids ids', merge_lists parms parms')
833 fun inst_wit all_params (t, th) = let
834 val {hyps, prop, ...} = Thm.rep_thm th;
835 val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
836 val [env] = unify_parms ctxt all_params [ps];
837 val t' = Element.instT_term env t;
838 val th' = Element.instT_thm thy env th;
841 fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
843 val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
844 val elems = map fst elems_stamped;
845 val ps = map fst ps_mx;
846 fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
847 val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
848 val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
849 val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
850 val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
852 Element.rename_morphism ren $>
853 Morphism.name_morphism (NameSpace.qualified (params_prefix params)) $>
854 Element.instT_morphism thy env;
855 val elems' = map (Element.morph_ctxt elem_morphism) elems;
856 in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
858 (* parameters, their types and syntax *)
859 val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
860 val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
861 (* compute identifiers and syntax, merge with previous ones *)
862 val (ids, _) = identify true expr;
863 val idents = subtract (eq_fst (op =)) prev_idents ids;
864 val syntax = merge_syntax ctxt ids (syn, prev_syntax);
865 (* type-instantiate elements *)
866 val final_elemss = map (eval all_params tenv syntax) idents;
867 in ((prev_idents @ idents, syntax), final_elemss) end;
872 (* activate elements *)
876 fun axioms_export axs _ As =
877 (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
880 (* NB: derived ids contain only facts at this stage *)
882 fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
883 ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
884 | activate_elem _ _ ((ctxt, mode), Constrains _) =
886 | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
888 val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
889 val ts = maps (map #1 o #2) asms';
890 val (ps, qs) = chop (length ts) axs;
892 ctxt |> fold Variable.auto_fixes ts
893 |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
894 in ((ctxt', Assumed qs), []) end
895 | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
896 ((ctxt, Derived ths), [])
897 | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
899 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
900 val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
901 let val ((c, _), t') = LocalDefs.cert_def ctxt t
902 in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
904 ctxt |> fold (Variable.auto_fixes o #1) asms
905 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
906 in ((ctxt', Assumed axs), []) end
907 | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
908 ((ctxt, Derived ths), [])
909 | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
911 val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
912 val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
913 in ((ctxt', mode), if is_ext then res else []) end;
915 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
917 val thy = ProofContext.theory_of ctxt;
918 val ((ctxt', _), res) =
919 foldl_map (activate_elem ax_in_ctxt (name = ""))
920 ((ProofContext.qualified_names ctxt, mode), elems)
921 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
922 val ctxt'' = if name = "" then ctxt'
924 val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
925 val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
928 fold (add_local_witness (name, ps') o
929 Element.assume_witness thy o Element.witness_prop) axs ctxt''
930 | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
932 in (ProofContext.restore_naming ctxt ctxt'', res) end;
934 fun activate_elemss ax_in_ctxt prep_facts =
935 fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
937 val elems = map (prep_facts ctxt) raw_elems;
938 val (ctxt', res) = apsnd flat
939 (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
940 val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
941 in (((((name, ps), mode), elems'), res), ctxt') end);
945 (* CB: activate_facts prep_facts (ctxt, elemss),
946 where elemss is a list of pairs consisting of identifiers and
947 context elements, extends ctxt by the context elements yielding
948 ctxt' and returns (ctxt', (elemss', facts)).
949 Identifiers in the argument are of the form ((name, ps), axs) and
950 assumptions use the axioms in the identifiers to set up exporters
951 in ctxt'. elemss' does not contain identifiers and is obtained
952 from elemss and the intermediate context with prep_facts.
953 If read_facts or cert_facts is used for prep_facts, these also remove
954 the internal/external markers from elemss. *)
956 fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
957 let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
958 in (ctxt', (elemss, flat factss)) end;
964 (** prepare locale elements **)
968 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
969 | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
970 | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
973 (* propositions and bindings *)
975 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
976 normalises expr (which is either a locale
977 expression or a single context element) wrt.
978 to the list ids of already accumulated identifiers.
979 It returns ((ids', syn'), elemss) where ids' is an extension of ids
980 with identifiers generated for expr, and elemss is the list of
981 context elements generated from expr.
982 syn and syn' are symtabs mapping parameter names to their syntax. syn'
983 is an extension of syn.
984 For details, see flatten_expr.
986 Additionally, for a locale expression, the elems are grouped into a single
987 Int; individual context elements are marked Ext. In this case, the
988 identifier-like information of the element is as follows:
989 - for Fixes: (("", ps), []) where the ps have type info NONE
990 - for other elements: (("", []), []).
991 The implementation of activate_facts relies on identifier names being
992 empty strings for external elements.
995 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
996 val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
999 merge_syntax ctxt ids'
1000 (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
1001 handle Symtab.DUPS xs => err_in_locale ctxt
1002 ("Conflicting syntax for parameters: " ^ commas_quote xs)
1004 [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
1006 | flatten _ ((ids, syn), Elem elem) =
1007 ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
1008 | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
1009 apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
1015 fun declare_int_elem (ctxt, Fixes fixes) =
1016 (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
1017 (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
1018 | declare_int_elem (ctxt, _) = (ctxt, []);
1020 fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
1021 let val (vars, _) = prep_vars fixes ctxt
1022 in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
1023 | declare_ext_elem prep_vars (ctxt, Constrains csts) =
1024 let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
1026 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
1027 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
1028 | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
1030 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
1031 let val (ctxt', propps) =
1033 Int es => foldl_map declare_int_elem (ctxt, es)
1034 | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
1035 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
1036 in (ctxt', propps) end
1037 | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
1041 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
1043 (* CB: fix of type bug of goal in target with context elements.
1044 Parameters new in context elements must receive types that are
1045 distinct from types of parameters in target (fixed_params). *)
1046 val ctxt_with_fixed =
1047 fold Variable.declare_term (map Free fixed_params) ctxt;
1050 |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
1051 |> unify_elemss ctxt_with_fixed fixed_params;
1052 val (_, raw_elemss') =
1053 foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
1054 (int_elemss, raw_elemss);
1055 in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
1061 val norm_term = Envir.beta_norm oo Term.subst_atomic;
1063 fun abstract_thm thy eq =
1064 Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
1066 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
1068 val ((y, T), b) = LocalDefs.abs_def eq;
1069 val b' = norm_term env b;
1070 val th = abstract_thm (ProofContext.theory_of ctxt) eq;
1071 fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
1073 conditional (exists (equal y o #1) xs) (fn () =>
1074 err "Attempt to define previously specified variable");
1075 conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
1076 err "Attempt to redefine variable");
1077 (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
1081 (* CB: for finish_elems (Int and Ext),
1082 extracts specification, only of assumed elements *)
1084 fun eval_text _ _ _ (Fixes _) text = text
1085 | eval_text _ _ _ (Constrains _) text = text
1086 | eval_text _ (_, Assumed _) is_ext (Assumes asms)
1087 (((exts, exts'), (ints, ints')), (xs, env, defs)) =
1089 val ts = maps (map #1 o #2) asms;
1090 val ts' = map (norm_term env) ts;
1092 if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
1093 else ((exts, exts'), (ints @ ts, ints' @ ts'));
1094 in (spec', (fold Term.add_frees ts' xs, env, defs)) end
1095 | eval_text _ (_, Derived _) _ (Assumes _) text = text
1096 | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
1097 (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
1098 | eval_text _ (_, Derived _) _ (Defines _) text = text
1099 | eval_text _ _ _ (Notes _) text = text;
1102 (* for finish_elems (Int),
1103 remove redundant elements of derived identifiers,
1104 turn assumptions and definitions into facts,
1105 satisfy hypotheses of facts *)
1107 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
1108 | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
1109 | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
1110 | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
1112 | finish_derived _ _ (Derived _) (Fixes _) = NONE
1113 | finish_derived _ _ (Derived _) (Constrains _) = NONE
1114 | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
1115 |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
1116 |> pair Thm.assumptionK |> Notes
1117 |> Element.morph_ctxt satisfy |> SOME
1118 | finish_derived sign satisfy (Derived _) (Defines defs) = defs
1119 |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
1120 |> pair Thm.definitionK |> Notes
1121 |> Element.morph_ctxt satisfy |> SOME
1123 | finish_derived _ satisfy _ (Notes facts) = Notes facts
1124 |> Element.morph_ctxt satisfy |> SOME;
1126 (* CB: for finish_elems (Ext) *)
1128 fun closeup _ false elem = elem
1129 | closeup ctxt true elem =
1132 let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
1133 in Term.list_all_free (frees, t) end;
1135 fun no_binds [] = []
1136 | no_binds _ = error "Illegal term bindings in locale element";
1139 Assumes asms => Assumes (asms |> map (fn (a, propps) =>
1140 (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
1141 | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
1142 (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
1147 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
1148 (x, AList.lookup (op =) parms x, mx)) fixes)
1149 | finish_ext_elem parms _ (Constrains _, _) = Constrains []
1150 | finish_ext_elem _ close (Assumes asms, propp) =
1151 close (Assumes (map #1 asms ~~ propp))
1152 | finish_ext_elem _ close (Defines defs, propp) =
1153 close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
1154 | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
1157 (* CB: finish_parms introduces type info from parms to identifiers *)
1158 (* CB: only needed for types that have been NONE so far???
1159 If so, which are these??? *)
1161 fun finish_parms parms (((name, ps), mode), elems) =
1162 (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
1164 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
1166 val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
1167 val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
1168 val text' = fold (eval_text ctxt id' false) es text;
1169 val es' = map_filter
1170 (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
1171 in ((text', wits'), (id', map Int es')) end
1172 | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
1174 val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
1175 val text' = eval_text ctxt id true e' text;
1176 in ((text', wits), (id, [Ext e'])) end
1180 (* CB: only called by prep_elemss *)
1182 fun finish_elemss ctxt parms do_close =
1183 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
1188 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
1190 fun defs_ord (defs1, defs2) =
1191 list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
1192 Term.fast_term_ord (d1, d2)) (defs1, defs2);
1194 TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
1195 val ord = defs_ord);
1197 fun rem_dup_defs es ds =
1198 fold_map (fn e as (Defines defs) => (fn ds =>
1199 if Defstab.defined ds defs
1200 then (Defines [], ds)
1201 else (e, Defstab.update (defs, ()) ds))
1202 | e => (fn ds => (e, ds))) es ds;
1203 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
1204 | rem_dup_elemss (Ext e) ds = (Ext e, ds);
1205 fun rem_dup_defines raw_elemss =
1206 fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
1207 apfst (pair id) (rem_dup_elemss es ds))
1208 | (id as (_, (Derived _)), es) => (fn ds =>
1209 ((id, es), ds))) raw_elemss Defstab.empty |> #1;
1211 (* CB: type inference and consistency checks for locales.
1213 Works by building a context (through declare_elemss), extracting the
1214 required information and adjusting the context elements (finish_elemss).
1215 Can also universally close free vars in assms and defs. This is only
1216 needed for Ext elements and controlled by parameter do_close.
1218 Only elements of assumed identifiers are considered.
1221 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
1223 (* CB: contexts computed in the course of this function are discarded.
1224 They are used for type inference and consistency checks only. *)
1225 (* CB: fixed_params are the parameters (with types) of the target locale,
1226 empty list if there is no target. *)
1227 (* CB: raw_elemss are list of pairs consisting of identifiers and
1228 context elements, the latter marked as internal or external. *)
1229 val raw_elemss = rem_dup_defines raw_elemss;
1230 val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
1231 (* CB: raw_ctxt is context with additional fixed variables derived from
1232 the fixes elements in raw_elemss,
1233 raw_proppss contains assumptions and definitions from the
1234 external elements in raw_elemss. *)
1235 fun prep_prop raw_propp (raw_ctxt, raw_concl) =
1237 (* CB: add type information from fixed_params to context (declare_term) *)
1238 (* CB: process patterns (conclusion and external elements only) *)
1239 val (ctxt, all_propp) =
1240 prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
1241 (* CB: add type information from conclusion and external elements to context *)
1242 val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
1243 (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
1244 val all_propp' = map2 (curry (op ~~))
1245 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
1246 val (concl, propp) = chop (length raw_concl) all_propp';
1247 in (propp, (ctxt, concl)) end
1249 val (proppss, (ctxt, concl)) =
1250 (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
1252 (* CB: obtain all parameters from identifier part of raw_elemss *)
1253 val xs = map #1 (params_of' raw_elemss);
1254 val typing = unify_frozen ctxt 0
1255 (map (Variable.default_type raw_ctxt) xs)
1256 (map (Variable.default_type ctxt) xs);
1257 val parms = param_types (xs ~~ typing);
1258 (* CB: parms are the parameters from raw_elemss, with correct typing. *)
1260 (* CB: extract information from assumes and defines elements
1261 (fixes, constrains and notes in raw_elemss don't have an effect on
1262 text and elemss), compute final form of context elements. *)
1263 val ((text, _), elemss) = finish_elemss ctxt parms do_close
1264 ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
1265 (* CB: text has the following structure:
1266 (((exts, exts'), (ints, ints')), (xs, env, defs))
1268 exts: external assumptions (terms in external assumes elements)
1269 exts': dito, normalised wrt. env
1270 ints: internal assumptions (terms in internal assumes elements)
1271 ints': dito, normalised wrt. env
1272 xs: the free variables in exts' and ints' and rhss of definitions,
1273 this includes parameters except defined parameters
1274 env: list of term pairs encoding substitutions, where the first term
1275 is a free variable; substitutions represent defines elements and
1276 the rhs is normalised wrt. the previous env
1277 defs: theorems representing the substitutions from defines elements
1278 (thms are normalised wrt. env).
1279 elemss is an updated version of raw_elemss:
1280 - type info added to Fixes and modified in Constrains
1281 - axiom and definition statement replaced by corresponding one
1282 from proppss in Assumes and Defines
1285 in ((parms, elemss, concl), text) end;
1289 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
1290 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
1295 (* facts and attributes *)
1299 fun check_name name =
1300 if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
1303 fun prep_facts _ _ _ ctxt (Int elem) = elem
1304 |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
1305 | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
1306 {var = I, typ = I, term = I,
1309 attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
1313 fun read_facts x = prep_facts check_name ProofContext.get_thms Attrib.intern_src x;
1314 fun cert_facts x = prep_facts I (K I) (K I) x;
1319 (* Get the specification of a locale *)
1321 (*The global specification is made from the parameters and global
1322 assumptions, the local specification from the parameters and the
1323 local assumptions.*)
1327 fun gen_asms_of get thy name =
1329 val ctxt = ProofContext.init thy;
1330 val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
1331 val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
1334 |> maps (fn (_, es) => map (fn Int e => e) es)
1335 |> maps (fn Assumes asms => asms | _ => [])
1336 |> map (apsnd (map fst))
1341 fun parameters_of thy name =
1342 the_locale thy name |> #params;
1344 fun parameters_of_expr thy expr =
1346 val ctxt = ProofContext.init thy;
1347 val pts = params_of_expr ctxt [] (intern_expr thy expr)
1348 ([], Symtab.empty, Symtab.empty);
1349 val raw_params_elemss = make_raw_params_elemss pts;
1350 val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
1351 (([], Symtab.empty), Expr expr);
1352 val ((parms, _, _), _) =
1353 read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
1354 in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
1356 fun local_asms_of thy name =
1357 gen_asms_of (single o Library.last_elem) thy name;
1359 fun global_asms_of thy name =
1360 gen_asms_of I thy name;
1365 (* full context statements: import + elements + conclusion *)
1369 fun prep_context_statement prep_expr prep_elemss prep_facts
1370 do_close fixed_params import elements raw_concl context =
1372 val thy = ProofContext.theory_of context;
1374 val (import_params, import_tenv, import_syn) =
1375 params_of_expr context fixed_params (prep_expr thy import)
1376 ([], Symtab.empty, Symtab.empty);
1377 val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
1378 val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
1379 (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
1381 val ((import_ids, _), raw_import_elemss) =
1382 flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
1383 (* CB: normalise "includes" among elements *)
1384 val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
1385 ((import_ids, incl_syn), elements);
1387 val raw_elemss = flat raw_elemsss;
1388 (* CB: raw_import_elemss @ raw_elemss is the normalised list of
1389 context elements obtained from import and elements. *)
1390 (* Now additional elements for parameters are inserted. *)
1391 val import_params_ids = make_params_ids import_params;
1392 val incl_params_ids =
1393 make_params_ids (incl_params \\ import_params);
1394 val raw_import_params_elemss =
1395 make_raw_params_elemss (import_params, incl_tenv, incl_syn);
1396 val raw_incl_params_elemss =
1397 make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
1398 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
1399 context fixed_params
1400 (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
1402 (* replace extended ids (for axioms) by ids *)
1403 val (import_ids', incl_ids) = chop (length import_ids) ids;
1404 val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
1405 val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
1406 (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
1407 (all_ids ~~ all_elemss);
1408 (* CB: all_elemss and parms contain the correct parameter types *)
1410 val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
1411 val (import_ctxt, (import_elemss, _)) =
1412 activate_facts false prep_facts (context, ps);
1414 val (ctxt, (elemss, _)) =
1415 activate_facts false prep_facts (ProofContext.set_stmt true import_ctxt, qs);
1417 ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
1418 (parms, spec, defs)), concl)
1421 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
1423 val thy = ProofContext.theory_of ctxt;
1424 val locale = Option.map (prep_locale thy) raw_locale;
1425 val (fixed_params, import) =
1429 let val {params = ps, ...} = the_locale thy name
1430 in (map fst ps, Locale name) end);
1431 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
1432 prep_ctxt false fixed_params import elems concl ctxt;
1433 in (locale, locale_ctxt, elems_ctxt, concl') end;
1435 fun prep_expr prep import body ctxt =
1437 val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt;
1438 val all_elems = maps snd (import_elemss @ elemss);
1439 in (all_elems, ctxt') end;
1443 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
1444 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
1446 fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt);
1447 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
1449 val read_expr = prep_expr read_context;
1450 val cert_expr = prep_expr cert_context;
1452 fun read_context_statement loc = prep_statement intern read_ctxt loc;
1453 fun read_context_statement_i loc = prep_statement (K I) read_ctxt loc;
1454 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
1463 #> (#2 o cert_context_statement (SOME loc) [] []);
1468 fun print_locale thy show_facts import body =
1469 let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in
1470 Pretty.big_list "locale elements:" (all_elems
1471 |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
1472 |> map (Pretty.chunks o Element.pretty_ctxt ctxt))
1478 (** store results **)
1480 (* naming of interpreted theorems *)
1482 fun global_note_prefix_i kind prfx args thy =
1484 |> Theory.qualified_names
1485 |> Theory.sticky_prefix prfx
1486 |> PureThy.note_thmss_i kind args
1487 ||> Theory.restore_naming thy;
1489 fun local_note_prefix_i kind prfx args ctxt =
1491 |> ProofContext.qualified_names
1492 |> ProofContext.sticky_prefix prfx
1493 |> ProofContext.note_thmss_i kind args
1494 ||> ProofContext.restore_naming ctxt;
1497 (* collect witnesses for global registration;
1498 requires parameters and flattened list of (assumed!) identifiers
1499 instead of recomputing it from the target *)
1501 fun collect_global_witnesses thy parms ids vts = let
1502 val ts = map Logic.unvarify vts;
1503 val (parms, parmTs) = split_list parms;
1504 val parmvTs = map Logic.varifyT parmTs;
1505 val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
1506 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
1508 (* replace parameter names in ids by instantiations *)
1509 val vinst = Symtab.make (parms ~~ vts);
1510 fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
1511 val inst = Symtab.make (parms ~~ ts);
1512 val ids' = map (apsnd vinst_names) ids;
1513 val wits = maps (snd o the o get_global_registration thy) ids';
1514 in ((tinst, inst), wits) end;
1517 (* store instantiations of args for all registered interpretations
1520 fun note_thmss_registrations target (kind, args) thy =
1522 val parms = the_locale thy target |> #params |> map fst;
1523 val ids = flatten (ProofContext.init thy, intern_expr thy)
1524 (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
1525 |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
1527 val regs = get_global_registrations thy target;
1529 (* add args to thy for all registrations *)
1531 fun activate (vts, ((prfx, atts2), _)) thy =
1533 val (insts, prems) = collect_global_witnesses thy parms ids vts;
1534 val attrib = Attrib.attribute_i thy;
1535 val inst_atts = Args.morph_values (Element.inst_morphism thy insts);
1537 Drule.standard o Element.satisfy_thm prems o Element.inst_thm thy insts;
1538 val args' = args |> map (fn ((name, atts), bs) =>
1539 ((name, map (attrib o inst_atts) atts),
1540 bs |> map (fn (ths, more_atts) =>
1541 (map inst_thm ths, map attrib (map inst_atts more_atts @ atts2)))));
1542 in global_note_prefix_i kind prfx args' thy |> snd end;
1543 in fold activate regs thy end;
1546 (* locale results *)
1548 fun add_thmss loc kind args ctxt =
1550 val (ctxt', ([(_, [Notes args'])], _)) =
1551 activate_facts true cert_facts
1552 (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
1553 val ctxt'' = ctxt' |> ProofContext.theory
1555 (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
1556 (axiom, import, elems @ [(Notes args', stamp ())],
1557 params, lparams, decls, regs, intros))
1558 #> note_thmss_registrations loc args');
1566 val dummy_thm = Drule.mk_term (Thm.cterm_of ProtoPure.thy (Term.dummy_pattern propT));
1567 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
1569 fun add_decls add loc decl =
1570 ProofContext.theory (change_locale loc
1571 (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
1572 (axiom, import, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
1573 add_thmss loc "" [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
1577 val add_type_syntax = add_decls (apfst o cons);
1578 val add_term_syntax = add_decls (apsnd o cons);
1579 val add_declaration = add_decls (K I);
1585 (** define locales **)
1587 (* predicate text *)
1588 (* CB: generate locale predicates and delta predicates *)
1592 (* introN: name of theorems for introduction rules of locale and
1594 axiomsN: name of theorem set with destruct rules for locale predicates,
1595 also name suffix of delta predicates. *)
1597 val introN = "intro";
1598 val axiomsN = "axioms";
1600 fun atomize_spec thy ts =
1602 val t = Logic.mk_conjunction_list ts;
1603 val body = ObjectLogic.atomize_term thy t;
1604 val bodyT = Term.fastype_of body;
1606 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
1607 else (body, bodyT, ObjectLogic.atomize_cterm (Thm.cterm_of thy t))
1610 fun aprop_tr' n c = (c, fn args =>
1611 if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
1614 (* CB: define one predicate including its intro rule and axioms
1615 - bname: predicate name
1616 - parms: locale parameters
1617 - defs: thms representing substitutions from defines elements
1618 - ts: terms representing locale assumptions (not normalised wrt. defs)
1619 - norm_ts: terms representing locale assumptions (normalised wrt. defs)
1623 fun def_pred bname parms defs ts norm_ts thy =
1625 val name = Sign.full_name thy bname;
1627 val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
1628 val env = Term.add_term_free_names (body, []);
1629 val xs = filter (member (op =) env o #1) parms;
1631 val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
1632 |> Library.sort_wrt #1 |> map TFree;
1633 val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
1635 val args = map Logic.mk_type extraTs @ map Free xs;
1636 val head = Term.list_comb (Const (name, predT), args);
1637 val statement = ObjectLogic.ensure_propT thy head;
1639 val ([pred_def], defs_thy) =
1641 |> (if bodyT <> propT then I else
1642 Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
1643 |> Theory.add_consts_i [(bname, predT, NoSyn)]
1644 |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
1645 val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
1647 val cert = Thm.cterm_of defs_thy;
1649 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
1650 Tactic.rewrite_goals_tac [pred_def] THEN
1651 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
1652 Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
1655 (Drule.equal_elim_rule2 OF [body_eq,
1656 Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
1657 |> Conjunction.elim_precise [length ts] |> hd;
1658 val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
1659 Element.prove_witness defs_ctxt t
1660 (Tactic.rewrite_goals_tac defs THEN
1661 Tactic.compose_tac (false, ax, 0) 1));
1662 in ((statement, intro, axioms), defs_thy) end;
1664 fun assumes_to_notes (Assumes asms) axms =
1665 fold_map (fn (a, spec) => fn axs =>
1666 let val (ps, qs) = chop (length spec) axs
1667 in ((a, [(ps, [])]), qs) end) asms axms
1668 |> apfst (curry Notes Thm.assumptionK)
1669 | assumes_to_notes e axms = (e, axms);
1671 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
1673 (* turn Assumes into Notes elements *)
1675 fun change_assumes_elemss axioms elemss =
1677 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
1678 fun change (id as ("", _), es) =
1679 fold_map assumes_to_notes (map satisfy es)
1680 #-> (fn es' => pair (id, es'))
1681 | change e = pair e;
1683 fst (fold_map change elemss (map Element.conclude_witness axioms))
1686 (* adjust hyps of Notes elements *)
1688 fun change_elemss_hyps axioms elemss =
1690 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
1691 fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
1693 in map change elemss end;
1697 (* CB: main predicate definition function *)
1699 fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
1701 val ((elemss', more_ts), a_elem, a_intro, thy') =
1702 if null exts then ((elemss, []), [], [], thy)
1705 val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
1706 val ((statement, intro, axioms), def_thy) =
1707 thy |> def_pred aname parms defs exts exts';
1708 val elemss' = change_assumes_elemss axioms elemss;
1709 val def_thy' = def_thy
1710 |> PureThy.note_thmss_qualified Thm.internalK
1711 aname [((introN, []), [([intro], [])])]
1713 val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1714 in ((elemss', [statement]), a_elem, [intro], def_thy') end;
1715 val (predicate, stmt', elemss'', b_intro, thy'') =
1716 if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy')
1719 val ((statement, intro, axioms), def_thy) =
1720 thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
1721 val cstatement = Thm.cterm_of def_thy statement;
1722 val elemss'' = change_elemss_hyps axioms elemss';
1725 |> PureThy.note_thmss_qualified Thm.internalK bname
1726 [((introN, []), [([intro], [])]),
1727 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
1729 val b_elem = [(("", []),
1730 [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1731 in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], def_thy') end;
1732 in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'') end;
1737 (* add_locale(_i) *)
1741 (* turn Defines into Notes elements, accumulate definition terms *)
1743 fun defines_to_notes is_ext thy (Defines defs) defns =
1745 val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
1746 val notes = map (fn (a, (def, _)) =>
1747 (a, [([assume (cterm_of thy def)], [])])) defs
1749 (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
1751 | defines_to_notes _ _ e defns = (SOME e, defns);
1753 fun change_defines_elemss thy elemss defns =
1755 fun change (id as (n, _), es) defns =
1757 val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
1758 in ((id, map_filter I es'), defns') end
1759 in fold_map change elemss defns end;
1761 fun gen_add_locale prep_ctxt prep_expr
1762 do_predicate bname raw_import raw_body thy =
1764 val name = Sign.full_name thy bname;
1765 val _ = conditional (is_some (get_locale thy name)) (fn () =>
1766 error ("Duplicate definition of locale " ^ quote name));
1768 val thy_ctxt = ProofContext.init thy;
1769 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
1770 text as (parms, ((_, exts'), _), defs)) =
1771 prep_ctxt raw_import raw_body thy_ctxt;
1772 val elemss = import_elemss @ body_elemss |>
1773 map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
1774 val import = prep_expr thy raw_import;
1776 val extraTs = foldr Term.add_term_tfrees [] exts' \\
1777 foldr Term.add_typ_tfrees [] (map snd parms);
1778 val _ = if null extraTs then ()
1779 else warning ("Additional type variable(s) in locale specification " ^ quote bname);
1781 val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
1782 pred_thy), (import, regs)) =
1783 if do_predicate then
1785 val (elemss', defns) = change_defines_elemss thy elemss [];
1786 val elemss'' = elemss' @ [(("", []), defns)];
1787 val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
1788 define_preds bname text elemss'' thy;
1789 fun mk_regs elemss wits =
1790 fold_map (fn (id, elems) => fn wts => let
1791 val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
1792 SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
1793 val (wts1, wts2) = chop (length ts) wts
1794 in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
1795 val regs = mk_regs elemss''' axioms |>
1796 map_filter (fn (("", _), _) => NONE | e => SOME e);
1797 in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
1798 else ((((elemss, ([], []), []), ([], [])), thy), (import, []));
1800 fun axiomify axioms elemss =
1801 (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
1802 val ts = flat (map_filter (fn (Assumes asms) =>
1803 SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
1804 val (axs1, axs2) = chop (length ts) axs;
1805 in (axs2, ((id, Assumed axs1), elems)) end)
1807 val (ctxt, (_, facts)) = activate_facts true (K I)
1808 (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
1809 val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
1810 val export = Goal.close_result o Goal.norm_result o
1811 singleton (ProofContext.export view_ctxt thy_ctxt);
1812 val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
1813 val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
1814 val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
1815 val axs' = map (Element.assume_witness pred_thy) stmt';
1816 val loc_ctxt = pred_thy
1817 |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
1818 |> declare_locale name
1822 elems = map (fn e => (e, stamp ())) elems'',
1823 params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
1824 lparams = map #1 (params_of' body_elemss),
1829 in (name, loc_ctxt) end;
1833 val add_locale = gen_add_locale read_context intern_expr;
1834 val add_locale_i = gen_add_locale cert_context (K I);
1838 val _ = Context.add_setup
1839 (add_locale_i true "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
1840 snd #> ProofContext.theory_of #>
1841 add_locale_i true "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
1842 snd #> ProofContext.theory_of);
1847 (** Normalisation of locale statements ---
1848 discharges goals implied by interpretations **)
1852 fun locale_assm_intros thy =
1853 Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
1854 (#2 (GlobalLocalesData.get thy)) [];
1855 fun locale_base_intros thy =
1856 Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
1857 (#2 (GlobalLocalesData.get thy)) [];
1859 fun all_witnesses ctxt =
1861 val thy = ProofContext.theory_of ctxt;
1862 fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
1863 (Registrations.dest thy regs |> map (fn (_, (_, wits)) =>
1864 map Element.conclude_witness wits) |> flat) @ thms)
1866 val globals = get (#3 (GlobalLocalesData.get thy));
1867 val locals = get (LocalLocalesData.get ctxt);
1868 in globals @ locals end;
1869 (* FIXME: proper varification *)
1873 fun intro_locales_tac eager ctxt facts st =
1875 val wits = all_witnesses ctxt |> map Thm.varifyT;
1876 val thy = ProofContext.theory_of ctxt;
1877 val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
1879 (ALLGOALS (Method.insert_tac facts THEN'
1880 REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
1881 THEN Tactic.distinct_subgoals_tac) st
1884 val _ = Context.add_setup (Method.add_methods
1886 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
1887 "back-chain introduction rules of locales without unfolding predicates"),
1889 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
1890 "back-chain all introduction rules of locales")]);
1895 (** Interpretation commands **)
1899 (* extract proof obligations (assms and defs) from elements *)
1901 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
1902 | extract_asms_elems ((id, Derived _), _) = (id, []);
1905 (* activate instantiated facts in theory or context *)
1907 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
1908 attn all_elemss new_elemss propss thmss thy_ctxt =
1910 fun activate_elem disch (prfx, atts) (Notes (kind, facts)) thy_ctxt =
1913 (* discharge hyps in attributes *)
1914 |> Attrib.map_facts (attrib thy_ctxt o Args.morph_values (Morphism.thm_morphism disch))
1915 (* append interpretation attributes *)
1916 |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
1917 (* discharge hyps *)
1918 |> map (apsnd (map (apfst (map disch))));
1919 in snd (note kind prfx facts' thy_ctxt) end
1920 | activate_elem _ _ _ thy_ctxt = thy_ctxt;
1922 fun activate_elems disch ((id, _), elems) thy_ctxt =
1924 val ((prfx, atts2), _) = the (get_reg thy_ctxt id)
1925 handle Option => sys_error ("Unknown registration of " ^
1926 quote (fst id) ^ " while activating facts.");
1927 in fold (activate_elem disch (prfx, atts2)) elems thy_ctxt end;
1929 val thy_ctxt' = thy_ctxt
1930 (* add registrations *)
1931 |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
1932 (* add witnesses of Assumed elements *)
1933 |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
1935 val prems = flat (map_filter
1936 (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
1937 | ((_, Derived _), _) => NONE) all_elemss);
1938 val satisfy = Element.satisfy_morphism prems;
1939 val thy_ctxt'' = thy_ctxt'
1940 (* add witnesses of Derived elements *)
1941 |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness satisfy) thms)
1942 (map_filter (fn ((_, Assumed _), _) => NONE
1943 | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
1945 val disch' = std o Morphism.thm satisfy; (* FIXME *)
1948 (* add facts to theory or context *)
1949 |> fold (activate_elems disch') new_elemss
1952 fun global_activate_facts_elemss x = gen_activate_facts_elemss
1953 (fn thy => fn (name, ps) =>
1954 get_global_registration thy (name, map Logic.varify ps))
1955 global_note_prefix_i
1956 Attrib.attribute_i Drule.standard
1957 (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
1958 (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
1959 Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
1962 fun local_activate_facts_elemss x = gen_activate_facts_elemss
1963 get_local_registration
1965 (Attrib.attribute_i o ProofContext.theory_of) I
1966 put_local_registration
1967 add_local_witness x;
1969 fun gen_prep_registration mk_ctxt is_local read_terms test_reg activate
1970 attn expr insts thy_ctxt =
1972 val ctxt = mk_ctxt thy_ctxt;
1973 val thy = ProofContext.theory_of ctxt;
1975 val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
1976 val pts = params_of_expr ctxt' [] (intern_expr thy expr)
1977 ([], Symtab.empty, Symtab.empty);
1978 val params_ids = make_params_ids (#1 pts);
1979 val raw_params_elemss = make_raw_params_elemss pts;
1980 val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
1981 (([], Symtab.empty), Expr expr);
1982 val ((parms, all_elemss, _), (_, (_, defs, _))) =
1983 read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
1985 (** compute instantiation **)
1988 val insts = if length parms < length insts
1989 then error "More arguments than parameters in instantiation."
1990 else insts @ replicate (length parms - length insts) NONE;
1991 val (ps, pTs) = split_list parms;
1992 val pvTs = map Logic.legacy_varifyT pTs;
1994 (* instantiations given by user *)
1995 val given = map_filter (fn (_, (NONE, _)) => NONE
1996 | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
1997 val (given_ps, given_insts) = split_list given;
1998 val tvars = foldr Term.add_typ_tvars [] pvTs;
1999 val used = foldr Term.add_typ_varnames [] pvTs;
2000 fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
2001 val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
2002 val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
2003 val vars' = fold Term.add_varnames vs vars;
2004 val _ = if null vars' then ()
2005 else error ("Illegal schematic variable(s) in instantiation: " ^
2006 commas_quote (map Syntax.string_of_vname vars'));
2007 (* replace new types (which are TFrees) by ones with new names *)
2008 val new_Tnames = foldr Term.add_term_tfree_names [] vs;
2009 val new_Tnames' = Name.invent_list used "'a" (length new_Tnames);
2012 else Logic.legacy_unvarifyT o Term.map_type_tfree (fn (a, s) =>
2013 TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
2016 else Term.map_types renameT;
2018 val tinst = Symtab.make (map
2019 (fn ((x, 0), T) => (x, T |> renameT)
2020 | ((_, n), _) => sys_error "Internal error var in prep_registration") vinst);
2021 val inst = Symtab.make (given_ps ~~ map rename vs);
2023 (* defined params without user input *)
2024 val not_given = map_filter (fn (x, (NONE, T)) => SOME (x, T)
2025 | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
2026 fun add_def (p, pT) inst =
2028 val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
2029 NONE => error ("Instance missing for parameter " ^ quote p)
2030 | SOME (Free (_, T), t) => (t, T);
2031 val d = Element.inst_term (tinst, inst) t;
2032 in Symtab.update_new (p, d) inst end;
2033 val inst = fold add_def not_given inst;
2034 val insts = (tinst, inst);
2035 val inst_morphism = Element.inst_morphism thy insts;
2036 (* Note: insts contain no vars. *)
2039 (** compute proof obligations **)
2041 (* restore "small" ids *)
2042 val ids' = map (fn ((n, ps), (_, mode)) =>
2043 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
2045 val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
2046 (* instantiate ids and elements *)
2047 val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
2048 ((n, map (Morphism.term inst_morphism) ps),
2049 map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
2050 |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
2052 (* remove fragments already registered with theory or context *)
2053 val new_inst_elemss = filter (fn ((id, _), _) =>
2054 not (test_reg thy_ctxt id)) inst_elemss;
2055 val new_ids = map #1 new_inst_elemss;
2057 val propss = map extract_asms_elems new_inst_elemss;
2059 val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
2060 val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
2062 in (propss, activate attn' inst_elemss new_inst_elemss propss) end;
2064 val prep_global_registration = gen_prep_registration
2065 ProofContext.init false
2066 (fn thy => fn sorts => fn used =>
2067 Sign.read_def_terms (thy, K NONE, sorts) used true)
2068 (fn thy => fn (name, ps) =>
2069 test_global_registration thy (name, map Logic.varify ps))
2070 global_activate_facts_elemss;
2072 val prep_local_registration = gen_prep_registration
2074 (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
2075 smart_test_registration
2076 local_activate_facts_elemss;
2078 fun prep_registration_in_locale target expr thy =
2079 (* target already in internal form *)
2081 val ctxt = ProofContext.init thy;
2082 val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
2083 (([], Symtab.empty), Expr (Locale target));
2084 val fixed = the_locale thy target |> #params |> map #1;
2085 val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
2086 ((raw_target_ids, target_syn), Expr expr);
2087 val (target_ids, ids) = chop (length raw_target_ids) all_ids;
2088 val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
2090 (** compute proof obligations **)
2092 (* restore "small" ids, with mode *)
2093 val ids' = map (apsnd snd) ids;
2094 (* remove Int markers *)
2095 val elemss' = map (fn (_, es) =>
2096 map (fn Int e => e) es) elemss
2097 (* extract assumptions and defs *)
2098 val ids_elemss = ids' ~~ elemss';
2099 val propss = map extract_asms_elems ids_elemss;
2101 (** activation function:
2102 - add registrations to the target locale
2103 - add induced registrations for all global registrations of
2104 the target, unless already present
2105 - add facts of induced registrations to theory **)
2107 val t_ids = map_filter
2108 (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
2110 fun activate thmss thy = let
2111 val satisfy = Element.satisfy_thm (flat thmss);
2112 val ids_elemss_thmss = ids_elemss ~~ thmss;
2113 val regs = get_global_registrations thy target;
2115 fun activate_id (((id, Assumed _), _), thms) thy =
2116 thy |> put_registration_in_locale target id
2117 |> fold (add_witness_in_locale target id) thms
2118 | activate_id _ thy = thy;
2120 fun activate_reg (vts, ((prfx, atts2), _)) thy =
2122 val (insts, wits) = collect_global_witnesses thy fixed t_ids vts;
2123 fun inst_parms ps = map
2124 (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
2125 val disch = Element.satisfy_thm wits;
2126 val new_elemss = filter (fn (((name, ps), _), _) =>
2127 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
2128 fun activate_assumed_id (((_, Derived _), _), _) thy = thy
2129 | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
2130 val ps' = inst_parms ps;
2132 if test_global_registration thy (name, ps')
2135 |> put_global_registration (name, ps') (prfx, atts2)
2136 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2137 (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
2140 fun activate_derived_id ((_, Assumed _), _) thy = thy
2141 | activate_derived_id (((name, ps), Derived ths), _) thy = let
2142 val ps' = inst_parms ps;
2144 if test_global_registration thy (name, ps')
2147 |> put_global_registration (name, ps') (prfx, atts2)
2148 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2149 (witn |> Element.map_witness (fn (t, th) => (* FIXME *)
2150 (Element.inst_term insts t,
2151 disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
2154 fun activate_elem (Notes (kind, facts)) thy =
2157 Morphism.thm_morphism satisfy $>
2158 Element.inst_morphism thy insts $>
2159 Morphism.thm_morphism disch;
2161 |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
2162 |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
2163 |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
2166 |> global_note_prefix_i kind prfx facts'
2169 | activate_elem _ thy = thy;
2171 fun activate_elems (_, elems) thy = fold activate_elem elems thy;
2173 in thy |> fold activate_assumed_id ids_elemss_thmss
2174 |> fold activate_derived_id ids_elemss
2175 |> fold activate_elems new_elemss end;
2177 thy |> fold activate_id ids_elemss_thmss
2178 |> fold activate_reg regs
2181 in (propss, activate) end;
2183 fun prep_propp propss = propss |> map (fn (_, props) =>
2184 map (rpair [] o Element.mark_witness) props);
2186 fun prep_result propps thmss =
2187 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
2191 fun interpretation after_qed (prfx, atts) expr insts thy =
2193 val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
2194 fun after_qed' results =
2195 ProofContext.theory (activate (prep_result propss results))
2198 ProofContext.init thy
2199 |> Proof.theorem_i NONE after_qed' (prep_propp propss)
2200 |> Element.refine_witness |> Seq.hd
2203 fun interpretation_in_locale after_qed (raw_target, expr) thy =
2205 val target = intern thy raw_target;
2206 val (propss, activate) = prep_registration_in_locale target expr thy;
2207 val raw_propp = prep_propp propss;
2209 val (_, _, goal_ctxt, propp) = thy
2210 |> ProofContext.init
2211 |> cert_context_statement (SOME target) [] raw_propp;
2213 fun after_qed' results =
2214 ProofContext.theory (activate (prep_result propss results))
2218 |> Proof.theorem_i NONE after_qed' propp
2219 |> Element.refine_witness |> Seq.hd
2222 fun interpret after_qed (prfx, atts) expr insts int state =
2224 val _ = Proof.assert_forward_or_chain state;
2225 val ctxt = Proof.context_of state;
2226 val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;
2227 fun after_qed' results =
2228 Proof.map_context (K (ctxt |> activate (prep_result propss results)))
2229 #> Proof.put_facts NONE
2233 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
2234 "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
2235 |> Element.refine_witness |> Seq.hd