src/Pure/Isar/locale.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 21602 cb13024d0e36
child 21665 ba07e24dc941
permissions -rw-r--r--
Attrib.internal: morphism;
     1 (*  Title:      Pure/Isar/locale.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
     4 
     5 Locales -- Isar proof contexts as meta-level predicates, with local
     6 syntax and implicit structures.
     7 
     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.
    13 
    14 Interpretation enables the reuse of theorems of locales in other
    15 contexts, namely those defined by theories, structured proofs and
    16 locales themselves.
    17 
    18 See also:
    19 
    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,
    28     pages 31-43, 2006.
    29 *)
    30 
    31 (* TODO:
    32 - beta-eta normalisation of interpretation parameters
    33 - dangling type frees in locales
    34 - test subsumption of interpretations when merging theories
    35 *)
    36 
    37 signature LOCALE =
    38 sig
    39   datatype expr =
    40     Locale of string |
    41     Rename of expr * (string * mixfix option) option list |
    42     Merge of expr list
    43   val empty: expr
    44   datatype 'a element = Elem of 'a | Expr of expr
    45   val map_elem: ('a -> 'b) -> 'a element -> 'b element
    46 
    47   val intern: theory -> xstring -> string
    48   val extern: theory -> string -> xstring
    49   val init: string -> theory -> Proof.context
    50 
    51   (* The specification of a locale *)
    52 
    53   val parameters_of: theory -> string ->
    54     ((string * typ) * mixfix) list
    55   val parameters_of_expr: theory -> expr ->
    56     ((string * typ) * mixfix) list
    57   val local_asms_of: theory -> string ->
    58     ((string * Attrib.src list) * term list) list
    59   val global_asms_of: theory -> string ->
    60     ((string * Attrib.src list) * term list) list
    61 
    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
    76 
    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
    83 
    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
    88 
    89   (* Tactics *)
    90   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    91 
    92   (* Storing results *)
    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 -> Proof.context -> Proof.context) ->
    97     Proof.context -> Proof.context
    98   val add_term_syntax: string -> (morphism -> Proof.context -> Proof.context) ->
    99     Proof.context -> Proof.context
   100   val add_declaration: string -> (morphism -> Proof.context -> Proof.context) ->
   101     Proof.context -> Proof.context
   102 
   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
   111 end;
   112 
   113 structure Locale: LOCALE =
   114 struct
   115 
   116 fun legacy_unvarifyT thm =
   117   let
   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;
   122 
   123 fun legacy_unvarify raw_thm =
   124   let
   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;
   130 
   131 
   132 (** locale elements and expressions **)
   133 
   134 datatype ctxt = datatype Element.ctxt;
   135 
   136 datatype expr =
   137   Locale of string |
   138   Rename of expr * (string * mixfix option) option list |
   139   Merge of expr list;
   140 
   141 val empty = Merge [];
   142 
   143 datatype 'a element =
   144   Elem of 'a | Expr of expr;
   145 
   146 fun map_elem f (Elem e) = Elem (f e)
   147   | map_elem _ (Expr e) = Expr e;
   148 
   149 type decl = (morphism -> Proof.context -> Proof.context) * stamp;
   150 
   151 type locale =
   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 * decl list,          (*type/term/fact 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. *)
   166 
   167 (* CB: an internal (Int) locale element was either imported or included,
   168    an external (Ext) element appears directly in the locale text. *)
   169 
   170 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   171 
   172 
   173 
   174 (** management of registrations in theories and proof contexts **)
   175 
   176 structure Registrations :
   177   sig
   178     type T
   179     val empty: T
   180     val join: T * T -> T
   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
   188   end =
   189 struct
   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;
   193 
   194   val empty = Termtab.empty;
   195 
   196   (* term list represented as single term, for simultaneous matching *)
   197   fun termify ts =
   198     Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
   199   fun untermify t =
   200     let fun ut (Const _) ts = ts
   201           | ut (s $ t) ts = ut s (t::ts)
   202     in ut t [] end;
   203 
   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);
   207 
   208   fun dest_transfer thy regs =
   209     Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy))));
   210 
   211   fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
   212 
   213   (* registrations that subsume t *)
   214   fun subsumers thy t regs =
   215     filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
   216 
   217   (* look up registration, pick one that subsumes the query *)
   218   fun lookup thy (regs, ts) =
   219     let
   220       val t = termify ts;
   221       val subs = subsumers thy t regs;
   222     in
   223       (case subs of
   224         [] => NONE
   225       | ((t', (attn, thms)) :: _) =>
   226           let
   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 Symtab.map (!?) *)
   230                  |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
   231                  |> Symtab.make;
   232             val inst' = inst |> Vartab.dest
   233                  |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
   234                  |> Symtab.make;
   235             val inst_witness = Element.morph_witness (Element.inst_morphism thy (tinst', inst'));
   236           in SOME (attn, map inst_witness thms) end)
   237     end;
   238 
   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 =
   242     let
   243       val t = termify ts;
   244       val subs = subsumers thy t regs ;
   245     in (case subs of
   246         [] => let
   247                 val sups =
   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
   251       | _ => (regs, []))
   252     end;
   253 
   254   (* add witness theorem to registration,
   255      only if instantiation is exact, otherwise exception Option raised *)
   256   fun add_witness ts thm regs =
   257     let
   258       val t = termify ts;
   259       val (x, thms) = the (Termtab.lookup regs t);
   260     in
   261       Termtab.update (t, (x, thm::thms)) regs
   262     end;
   263 end;
   264 
   265 
   266 (** theory data **)
   267 
   268 structure GlobalLocalesData = TheoryDataFun
   269 (struct
   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 *)
   275 
   276   val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
   277   val copy = I;
   278   val extend = I;
   279 
   280   fun merge_decls which (decls, decls') : decl list =
   281     Library.merge (eq_snd (op =)) (which decls, which decls');
   282 
   283   fun join_locales _ ({axiom, import, elems, params, lparams, decls, regs, intros}: locale,
   284       {elems = elems', decls = decls', regs = regs', ...}: locale) =
   285      {axiom = axiom,
   286       import = import,
   287       elems = gen_merge_lists (eq_snd (op =)) elems elems',
   288       params = params,
   289       lparams = lparams,
   290       decls =
   291        (merge_decls #1 (decls, decls'),
   292         merge_decls #2 (decls, decls'),
   293         merge_decls #3 (decls, decls')),
   294       regs = merge_alists regs regs',
   295       intros = intros};
   296   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
   297     (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
   298      Symtab.join (K Registrations.join) (regs1, regs2));
   299 
   300   fun print _ (space, locs, _) =
   301     Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   302     |> Pretty.writeln;
   303 end);
   304 
   305 val _ = Context.add_setup GlobalLocalesData.init;
   306 
   307 
   308 
   309 (** context data **)
   310 
   311 structure LocalLocalesData = ProofDataFun
   312 (struct
   313   val name = "Isar/locales";
   314   type T = Registrations.T Symtab.table;
   315     (* registrations, indexed by locale name *)
   316   fun init _ = Symtab.empty;
   317   fun print _ _ = ();
   318 end);
   319 
   320 val _ = Context.add_setup LocalLocalesData.init;
   321 
   322 
   323 (* access locales *)
   324 
   325 val print_locales = GlobalLocalesData.print;
   326 
   327 val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
   328 val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
   329 
   330 fun declare_locale name thy =
   331   thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
   332     (Sign.declare_name thy name space, locs, regs));
   333 
   334 fun put_locale name loc =
   335   GlobalLocalesData.map (fn (space, locs, regs) =>
   336     (space, Symtab.update (name, loc) locs, regs));
   337 
   338 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;
   339 
   340 fun the_locale thy name =
   341   (case get_locale thy name of
   342     SOME loc => loc
   343   | NONE => error ("Unknown locale " ^ quote name));
   344 
   345 fun change_locale name f thy =
   346   let
   347     val {axiom, import, elems, params, lparams, decls, regs, intros} =
   348         the_locale thy name;
   349     val (axiom', import', elems', params', lparams', decls', regs', intros') =
   350       f (axiom, import, elems, params, lparams, decls, regs, intros);
   351   in
   352     put_locale name {axiom = axiom', import = import', elems = elems',
   353       params = params', lparams = lparams', decls = decls', regs = regs',
   354       intros = intros'} thy
   355   end;
   356 
   357 
   358 (* access registrations *)
   359 
   360 (* Ids of global registrations are varified,
   361    Ids of local registrations are not.
   362    Thms of registrations are never varified. *)
   363 
   364 (* retrieve registration from theory or context *)
   365 
   366 fun gen_get_registrations get thy_of thy_ctxt name =
   367   case Symtab.lookup (get thy_ctxt) name of
   368       NONE => []
   369     | SOME reg => Registrations.dest (thy_of thy_ctxt) reg;
   370 
   371 val get_global_registrations =
   372      gen_get_registrations (#3 o GlobalLocalesData.get) I;
   373 val get_local_registrations =
   374      gen_get_registrations LocalLocalesData.get ProofContext.theory_of;
   375 
   376 fun gen_get_registration get thy_of thy_ctxt (name, ps) =
   377   case Symtab.lookup (get thy_ctxt) name of
   378       NONE => NONE
   379     | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
   380 
   381 val get_global_registration =
   382      gen_get_registration (#3 o GlobalLocalesData.get) I;
   383 val get_local_registration =
   384      gen_get_registration LocalLocalesData.get ProofContext.theory_of;
   385 
   386 val test_global_registration = is_some oo get_global_registration;
   387 val test_local_registration = is_some oo get_local_registration;
   388 fun smart_test_registration ctxt id =
   389   let
   390     val thy = ProofContext.theory_of ctxt;
   391   in
   392     test_global_registration thy id orelse test_local_registration ctxt id
   393   end;
   394 
   395 
   396 (* add registration to theory or context, ignored if subsumed *)
   397 
   398 fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
   399   map_data (fn regs =>
   400     let
   401       val thy = thy_of thy_ctxt;
   402       val reg = the_default Registrations.empty (Symtab.lookup regs name);
   403       val (reg', sups) = Registrations.insert thy (ps, attn) reg;
   404       val _ = if not (null sups) then warning
   405                 ("Subsumed interpretation(s) of locale " ^
   406                  quote (extern thy name) ^
   407                  "\nby interpretation(s) with the following prefix(es):\n" ^
   408                   commas_quote (map (fn (_, ((s, _), _)) => s) sups))
   409               else ();
   410     in Symtab.update (name, reg') regs end) thy_ctxt;
   411 
   412 val put_global_registration =
   413      gen_put_registration (fn f =>
   414        GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
   415 val put_local_registration =
   416      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
   417 
   418 fun put_registration_in_locale name id =
   419   change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
   420     (axiom, import, elems, params, lparams, decls, regs @ [(id, [])], intros));
   421 
   422 
   423 (* add witness theorem to registration in theory or context,
   424    ignored if registration not present *)
   425 
   426 fun add_witness (name, ps) thm =
   427   Symtab.map_entry name (Registrations.add_witness ps thm);
   428 
   429 fun add_global_witness id thm =
   430   GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
   431 
   432 val add_local_witness = LocalLocalesData.map oo add_witness;
   433 
   434 fun add_witness_in_locale name id thm =
   435   change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
   436     let
   437       fun add (id', thms) =
   438         if id = id' then (id', thm :: thms) else (id', thms);
   439     in (axiom, import, elems, params, lparams, decls, map add regs, intros) end);
   440 
   441 
   442 (* printing of registrations *)
   443 
   444 fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
   445   let
   446     val ctxt = mk_ctxt thy_ctxt;
   447     val thy = ProofContext.theory_of ctxt;
   448 
   449     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   450     fun prt_inst ts =
   451         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
   452     fun prt_attn (prfx, atts) =
   453         Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
   454     fun prt_witns witns = Pretty.enclose "[" "]"
   455       (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
   456     fun prt_reg (ts, (("", []), witns)) =
   457         if show_wits
   458           then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
   459           else prt_inst ts
   460       | prt_reg (ts, (attn, witns)) =
   461         if show_wits
   462           then Pretty.block ((prt_attn attn @
   463             [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
   464               prt_witns witns]))
   465           else Pretty.block ((prt_attn attn @
   466             [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
   467 
   468     val loc_int = intern thy loc;
   469     val regs = get_regs thy_ctxt;
   470     val loc_regs = Symtab.lookup regs loc_int;
   471   in
   472     (case loc_regs of
   473         NONE => Pretty.str ("no interpretations in " ^ msg)
   474       | SOME r => let
   475             val r' = Registrations.dest thy r;
   476             val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
   477           in Pretty.big_list ("interpretations in " ^ msg ^ ":")
   478             (map prt_reg r'')
   479           end)
   480     |> Pretty.writeln
   481   end;
   482 
   483 val print_global_registrations =
   484      gen_print_registrations (#3 o GlobalLocalesData.get)
   485        ProofContext.init "theory";
   486 val print_local_registrations' =
   487      gen_print_registrations LocalLocalesData.get
   488        I "context";
   489 fun print_local_registrations show_wits loc ctxt =
   490   (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
   491    print_local_registrations' show_wits loc ctxt);
   492 
   493 
   494 (* diagnostics *)
   495 
   496 fun err_in_locale ctxt msg ids =
   497   let
   498     val thy = ProofContext.theory_of ctxt;
   499     fun prt_id (name, parms) =
   500       [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   501     val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   502     val err_msg =
   503       if forall (equal "" o #1) ids then msg
   504       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   505         (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   506   in error err_msg end;
   507 
   508 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   509 
   510 
   511 fun pretty_ren NONE = Pretty.str "_"
   512   | pretty_ren (SOME (x, NONE)) = Pretty.str x
   513   | pretty_ren (SOME (x, SOME syn)) =
   514       Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
   515 
   516 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
   517   | pretty_expr thy (Rename (expr, xs)) =
   518       Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
   519   | pretty_expr thy (Merge es) =
   520       Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
   521 
   522 fun err_in_expr _ msg (Merge []) = error msg
   523   | err_in_expr ctxt msg expr =
   524     error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
   525       [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
   526        pretty_expr (ProofContext.theory_of ctxt) expr]));
   527 
   528 
   529 (** structured contexts: rename + merge + implicit type instantiation **)
   530 
   531 (* parameter types *)
   532 
   533 fun frozen_tvars ctxt Ts =
   534   #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   535   |> map (fn ((xi, S), T) => (xi, (S, T)));
   536 
   537 fun unify_frozen ctxt maxidx Ts Us =
   538   let
   539     fun paramify NONE i = (NONE, i)
   540       | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   541 
   542     val (Ts', maxidx') = fold_map paramify Ts maxidx;
   543     val (Us', maxidx'') = fold_map paramify Us maxidx';
   544     val thy = ProofContext.theory_of ctxt;
   545 
   546     fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   547           handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   548       | unify _ env = env;
   549     val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   550     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   551     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   552   in map (Option.map (Envir.norm_type unifier')) Vs end;
   553 
   554 fun params_of elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
   555 fun params_of' elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   556 
   557 
   558 (* CB: param_types has the following type:
   559   ('a * 'b option) list -> ('a * 'b) list *)
   560 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   561 
   562 
   563 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
   564   handle Symtab.DUPS xs => err_in_locale ctxt
   565     ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
   566 
   567 
   568 (* Distinction of assumed vs. derived identifiers.
   569    The former may have axioms relating assumptions of the context to
   570    assumptions of the specification fragment (for locales with
   571    predicates).  The latter have witnesses relating assumptions of the
   572    specification fragment to assumptions of other (assumed) specification
   573    fragments. *)
   574 
   575 datatype 'a mode = Assumed of 'a | Derived of 'a;
   576 
   577 fun map_mode f (Assumed x) = Assumed (f x)
   578   | map_mode f (Derived x) = Derived (f x);
   579 
   580 
   581 (* flatten expressions *)
   582 
   583 local
   584 
   585 fun unify_parms ctxt fixed_parms raw_parmss =
   586   let
   587     val thy = ProofContext.theory_of ctxt;
   588     val maxidx = length raw_parmss;
   589     val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   590 
   591     fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   592     fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   593     val parms = fixed_parms @ maps varify_parms idx_parmss;
   594 
   595     fun unify T U envir = Sign.typ_unify thy (U, T) envir
   596       handle Type.TUNIFY =>
   597         let val prt = Sign.string_of_typ thy in
   598           raise TYPE ("unify_parms: failed to unify types " ^
   599             prt U ^ " and " ^ prt T, [U, T], [])
   600         end;
   601     fun unify_list (T :: Us) = fold (unify T) Us
   602       | unify_list [] = I;
   603     val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
   604       (Vartab.empty, maxidx);
   605 
   606     val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
   607     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   608 
   609     fun inst_parms (i, ps) =
   610       foldr Term.add_typ_tfrees [] (map_filter snd ps)
   611       |> map_filter (fn (a, S) =>
   612           let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   613           in if T = TFree (a, S) then NONE else SOME (a, T) end)
   614       |> Symtab.make;
   615   in map inst_parms idx_parmss end;
   616 
   617 in
   618 
   619 fun unify_elemss _ _ [] = []
   620   | unify_elemss _ [] [elems] = [elems]
   621   | unify_elemss ctxt fixed_parms elemss =
   622       let
   623         val thy = ProofContext.theory_of ctxt;
   624         val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
   625           |> map (Element.instT_morphism thy);
   626         fun inst ((((name, ps), mode), elems), phi) =
   627           (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
   628               map_mode (map (Element.morph_witness phi)) mode),
   629             map (Element.morph_ctxt phi) elems);
   630       in map inst (elemss ~~ phis) end;
   631 
   632 
   633 fun renaming xs parms = zip_options parms xs
   634   handle Library.UnequalLengths =>
   635     error ("Too many arguments in renaming: " ^
   636       commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
   637 
   638 
   639 (* params_of_expr:
   640    Compute parameters (with types and syntax) of locale expression.
   641 *)
   642 
   643 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
   644   let
   645     val thy = ProofContext.theory_of ctxt;
   646 
   647     fun merge_tenvs fixed tenv1 tenv2 =
   648         let
   649           val [env1, env2] = unify_parms ctxt fixed
   650                 [tenv1 |> Symtab.dest |> map (apsnd SOME),
   651                  tenv2 |> Symtab.dest |> map (apsnd SOME)]
   652         in
   653           Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
   654             Symtab.map (Element.instT_type env2) tenv2)
   655         end;
   656 
   657     fun merge_syn expr syn1 syn2 =
   658         Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
   659         handle Symtab.DUPS xs => err_in_expr ctxt
   660           ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
   661 
   662     fun params_of (expr as Locale name) =
   663           let
   664             val {import, params, ...} = the_locale thy name;
   665             val parms = map (fst o fst) params;
   666             val (parms', types', syn') = params_of import;
   667             val all_parms = merge_lists parms' parms;
   668             val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
   669             val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
   670           in (all_parms, all_types, all_syn) end
   671       | params_of (expr as Rename (e, xs)) =
   672           let
   673             val (parms', types', syn') = params_of e;
   674             val ren = renaming xs parms';
   675             (* renaming may reduce number of parameters *)
   676             val new_parms = map (Element.rename ren) parms' |> distinct (op =);
   677             val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
   678             val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
   679                 handle Symtab.DUP x =>
   680                   err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
   681             val syn_types = map (apsnd (fn mx => SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))))) (Symtab.dest new_syn);
   682             val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
   683             val (env :: _) = unify_parms ctxt []
   684                 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
   685             val new_types = fold (Symtab.insert (op =))
   686                 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
   687           in (new_parms, new_types, new_syn) end
   688       | params_of (Merge es) =
   689           fold (fn e => fn (parms, types, syn) =>
   690                    let
   691                      val (parms', types', syn') = params_of e
   692                    in
   693                      (merge_lists parms parms', merge_tenvs [] types types',
   694                       merge_syn e syn syn')
   695                    end)
   696             es ([], Symtab.empty, Symtab.empty)
   697 
   698       val (parms, types, syn) = params_of expr;
   699     in
   700       (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
   701        merge_syn expr prev_syn syn)
   702     end;
   703 
   704 fun make_params_ids params = [(("", params), ([], Assumed []))];
   705 fun make_raw_params_elemss (params, tenv, syn) =
   706     [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   707       Int [Fixes (map (fn p =>
   708         (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   709 
   710 
   711 (* flatten_expr:
   712    Extend list of identifiers by those new in locale expression expr.
   713    Compute corresponding list of lists of locale elements (one entry per
   714    identifier).
   715 
   716    Identifiers represent locale fragments and are in an extended form:
   717      ((name, ps), (ax_ps, axs))
   718    (name, ps) is the locale name with all its parameters.
   719    (ax_ps, axs) is the locale axioms with its parameters;
   720      axs are always taken from the top level of the locale hierarchy,
   721      hence axioms may contain additional parameters from later fragments:
   722      ps subset of ax_ps.  axs is either singleton or empty.
   723 
   724    Elements are enriched by identifier-like information:
   725      (((name, ax_ps), axs), elems)
   726    The parameters in ax_ps are the axiom parameters, but enriched by type
   727    info: now each entry is a pair of string and typ option.  Axioms are
   728    type-instantiated.
   729 
   730 *)
   731 
   732 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
   733   let
   734     val thy = ProofContext.theory_of ctxt;
   735 
   736     fun rename_parms top ren ((name, ps), (parms, mode)) =
   737         ((name, map (Element.rename ren) ps),
   738          if top
   739          then (map (Element.rename ren) parms,
   740                map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
   741          else (parms, mode));
   742 
   743     (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
   744 
   745     fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
   746         if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
   747         then (wits, ids, visited)
   748         else
   749           let
   750             val {params, regs, ...} = the_locale thy name;
   751             val pTs' = map #1 params;
   752             val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
   753               (* dummy syntax, since required by rename *)
   754             val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
   755             val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
   756               (* propagate parameter types, to keep them consistent *)
   757             val regs' = map (fn ((name, ps), wits) =>
   758                 ((name, map (Element.rename ren) ps),
   759                  map (Element.transfer_witness thy) wits)) regs;
   760             val new_regs = regs';
   761             val new_ids = map fst new_regs;
   762             val new_idTs =
   763               map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
   764 
   765             val new_wits = new_regs |> map (#2 #> map
   766               (Element.morph_witness
   767                 (Element.instT_morphism thy env $>
   768                   Element.rename_morphism ren $>
   769                   Element.satisfy_morphism wits)));
   770             val new_ids' = map (fn (id, wits) =>
   771                 (id, ([], Derived wits))) (new_ids ~~ new_wits);
   772             val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
   773                 ((n, pTs), mode)) (new_idTs ~~ new_ids');
   774             val new_id = ((name, map #1 pTs), ([], mode));
   775             val (wits', ids', visited') = fold add_with_regs new_idTs'
   776               (wits @ flat new_wits, ids, visited @ [new_id]);
   777           in
   778             (wits', ids' @ [new_id], visited')
   779           end;
   780 
   781     (* distribute top-level axioms over assumed ids *)
   782 
   783     fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
   784         let
   785           val {elems, ...} = the_locale thy name;
   786           val ts = maps
   787             (fn (Assumes asms, _) => maps (map #1 o #2) asms
   788               | _ => [])
   789             elems;
   790           val (axs1, axs2) = chop (length ts) axioms;
   791         in (((name, parms), (all_ps, Assumed axs1)), axs2) end
   792       | axiomify all_ps (id, (_, Derived ths)) axioms =
   793           ((id, (all_ps, Derived ths)), axioms);
   794 
   795     (* identifiers of an expression *)
   796 
   797     fun identify top (Locale name) =
   798     (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
   799        where name is a locale name, ps a list of parameter names and axs
   800        a list of axioms relating to the identifier, axs is empty unless
   801        identify at top level (top = true);
   802        parms is accumulated list of parameters *)
   803           let
   804             val {axiom, import, params, ...} = the_locale thy name;
   805             val ps = map (#1 o #1) params;
   806             val (ids', parms') = identify false import;
   807                 (* acyclic import dependencies *)
   808 
   809             val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
   810             val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
   811             in (ids_ax, merge_lists parms' ps) end
   812       | identify top (Rename (e, xs)) =
   813           let
   814             val (ids', parms') = identify top e;
   815             val ren = renaming xs parms'
   816               handle ERROR msg => err_in_locale' ctxt msg ids';
   817 
   818             val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   819             val parms'' = distinct (op =) (maps (#2 o #1) ids'');
   820           in (ids'', parms'') end
   821       | identify top (Merge es) =
   822           fold (fn e => fn (ids, parms) =>
   823                    let
   824                      val (ids', parms') = identify top e
   825                    in
   826                      (merge_alists ids ids', merge_lists parms parms')
   827                    end)
   828             es ([], []);
   829 
   830     fun inst_wit all_params (t, th) = let
   831          val {hyps, prop, ...} = Thm.rep_thm th;
   832          val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
   833          val [env] = unify_parms ctxt all_params [ps];
   834          val t' = Element.instT_term env t;
   835          val th' = Element.instT_thm thy env th;
   836        in (t', th') end;
   837 
   838     fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
   839       let
   840         val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
   841         val elems = map fst elems_stamped;
   842         val ps = map fst ps_mx;
   843         fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
   844         val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
   845         val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
   846         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
   847         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   848         val elem_morphism =
   849           Element.rename_morphism ren $>
   850           Morphism.name_morphism (NameSpace.qualified (space_implode "_" params)) $>
   851           Element.instT_morphism thy env;
   852         val elems' = map (Element.morph_ctxt elem_morphism) elems;
   853       in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   854 
   855     (* parameters, their types and syntax *)
   856     val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
   857     val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
   858     (* compute identifiers and syntax, merge with previous ones *)
   859     val (ids, _) = identify true expr;
   860     val idents = subtract (eq_fst (op =)) prev_idents ids;
   861     val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   862     (* type-instantiate elements *)
   863     val final_elemss = map (eval all_params tenv syntax) idents;
   864   in ((prev_idents @ idents, syntax), final_elemss) end;
   865 
   866 end;
   867 
   868 
   869 (* activate elements *)
   870 
   871 local
   872 
   873 fun axioms_export axs _ hyps =
   874   Element.satisfy_thm axs
   875   #> Drule.implies_intr_list (Library.drop (length axs, hyps));
   876 
   877 
   878 (* NB: derived ids contain only facts at this stage *)
   879 
   880 fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
   881       ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
   882   | activate_elem _ _ ((ctxt, mode), Constrains _) =
   883       ((ctxt, mode), [])
   884   | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
   885       let
   886         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   887         val ts = maps (map #1 o #2) asms';
   888         val (ps, qs) = chop (length ts) axs;
   889         val (_, ctxt') =
   890           ctxt |> fold Variable.auto_fixes ts
   891           |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
   892       in ((ctxt', Assumed qs), []) end
   893   | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
   894       ((ctxt, Derived ths), [])
   895   | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
   896       let
   897         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   898         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
   899             let val ((c, _), t') = LocalDefs.cert_def ctxt t
   900             in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
   901         val (_, ctxt') =
   902           ctxt |> fold (Variable.auto_fixes o #1) asms
   903           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
   904       in ((ctxt', Assumed axs), []) end
   905   | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
   906       ((ctxt, Derived ths), [])
   907   | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
   908       let
   909         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
   910         val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
   911       in ((ctxt', mode), if is_ext then res else []) end;
   912 
   913 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
   914   let
   915     val thy = ProofContext.theory_of ctxt;
   916     val ((ctxt', _), res) =
   917       foldl_map (activate_elem ax_in_ctxt (name = ""))
   918         ((ProofContext.qualified_names ctxt, mode), elems)
   919       handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
   920     val ctxt'' = if name = "" then ctxt'
   921           else let
   922               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   923               val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
   924             in case mode of
   925                 Assumed axs =>
   926                   fold (add_local_witness (name, ps') o
   927                     Element.assume_witness thy o Element.witness_prop) axs ctxt''
   928               | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
   929             end
   930   in (ProofContext.restore_naming ctxt ctxt'', res) end;
   931 
   932 fun activate_elemss ax_in_ctxt prep_facts =
   933     fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
   934       let
   935         val elems = map (prep_facts ctxt) raw_elems;
   936         val (ctxt', res) = apsnd flat
   937             (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
   938         val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
   939       in (((((name, ps), mode), elems'), res), ctxt') end);
   940 
   941 in
   942 
   943 (* CB: activate_facts prep_facts (ctxt, elemss),
   944    where elemss is a list of pairs consisting of identifiers and
   945    context elements, extends ctxt by the context elements yielding
   946    ctxt' and returns (ctxt', (elemss', facts)).
   947    Identifiers in the argument are of the form ((name, ps), axs) and
   948    assumptions use the axioms in the identifiers to set up exporters
   949    in ctxt'.  elemss' does not contain identifiers and is obtained
   950    from elemss and the intermediate context with prep_facts.
   951    If read_facts or cert_facts is used for prep_facts, these also remove
   952    the internal/external markers from elemss. *)
   953 
   954 fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
   955   let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
   956   in (ctxt', (elemss, flat factss)) end;
   957 
   958 end;
   959 
   960 
   961 
   962 (** prepare locale elements **)
   963 
   964 (* expressions *)
   965 
   966 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
   967   | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
   968   | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
   969 
   970 
   971 (* propositions and bindings *)
   972 
   973 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
   974    normalises expr (which is either a locale
   975    expression or a single context element) wrt.
   976    to the list ids of already accumulated identifiers.
   977    It returns ((ids', syn'), elemss) where ids' is an extension of ids
   978    with identifiers generated for expr, and elemss is the list of
   979    context elements generated from expr.
   980    syn and syn' are symtabs mapping parameter names to their syntax.  syn'
   981    is an extension of syn.
   982    For details, see flatten_expr.
   983 
   984    Additionally, for a locale expression, the elems are grouped into a single
   985    Int; individual context elements are marked Ext.  In this case, the
   986    identifier-like information of the element is as follows:
   987    - for Fixes: (("", ps), []) where the ps have type info NONE
   988    - for other elements: (("", []), []).
   989    The implementation of activate_facts relies on identifier names being
   990    empty strings for external elements.
   991 *)
   992 
   993 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
   994         val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
   995       in
   996         ((ids',
   997          merge_syntax ctxt ids'
   998            (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
   999            handle Symtab.DUPS xs => err_in_locale ctxt
  1000              ("Conflicting syntax for parameters: " ^ commas_quote xs)
  1001              (map #1 ids')),
  1002          [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
  1003       end
  1004   | flatten _ ((ids, syn), Elem elem) =
  1005       ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  1006   | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
  1007       apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
  1008 
  1009 local
  1010 
  1011 local
  1012 
  1013 fun declare_int_elem (ctxt, Fixes fixes) =
  1014       (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  1015         (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
  1016   | declare_int_elem (ctxt, _) = (ctxt, []);
  1017 
  1018 fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
  1019       let val (vars, _) = prep_vars fixes ctxt
  1020       in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
  1021   | declare_ext_elem prep_vars (ctxt, Constrains csts) =
  1022       let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
  1023       in (ctxt', []) end
  1024   | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
  1025   | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
  1026   | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
  1027 
  1028 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
  1029     let val (ctxt', propps) =
  1030       (case elems of
  1031         Int es => foldl_map declare_int_elem (ctxt, es)
  1032       | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
  1033       handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
  1034     in (ctxt', propps) end
  1035   | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
  1036 
  1037 in
  1038 
  1039 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
  1040   let
  1041     (* CB: fix of type bug of goal in target with context elements.
  1042        Parameters new in context elements must receive types that are
  1043        distinct from types of parameters in target (fixed_params).  *)
  1044     val ctxt_with_fixed =
  1045       fold Variable.declare_term (map Free fixed_params) ctxt;
  1046     val int_elemss =
  1047       raw_elemss
  1048       |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  1049       |> unify_elemss ctxt_with_fixed fixed_params;
  1050     val (_, raw_elemss') =
  1051       foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
  1052         (int_elemss, raw_elemss);
  1053   in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
  1054 
  1055 end;
  1056 
  1057 local
  1058 
  1059 val norm_term = Envir.beta_norm oo Term.subst_atomic;
  1060 
  1061 fun abstract_thm thy eq =
  1062   Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
  1063 
  1064 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
  1065   let
  1066     val ((y, T), b) = LocalDefs.abs_def eq;
  1067     val b' = norm_term env b;
  1068     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
  1069     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  1070   in
  1071     conditional (exists (equal y o #1) xs) (fn () =>
  1072       err "Attempt to define previously specified variable");
  1073     conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
  1074       err "Attempt to redefine variable");
  1075     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  1076   end;
  1077 
  1078 
  1079 (* CB: for finish_elems (Int and Ext),
  1080    extracts specification, only of assumed elements *)
  1081 
  1082 fun eval_text _ _ _ (Fixes _) text = text
  1083   | eval_text _ _ _ (Constrains _) text = text
  1084   | eval_text _ (_, Assumed _) is_ext (Assumes asms)
  1085         (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  1086       let
  1087         val ts = maps (map #1 o #2) asms;
  1088         val ts' = map (norm_term env) ts;
  1089         val spec' =
  1090           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  1091           else ((exts, exts'), (ints @ ts, ints' @ ts'));
  1092       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  1093   | eval_text _ (_, Derived _) _ (Assumes _) text = text
  1094   | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
  1095       (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
  1096   | eval_text _ (_, Derived _) _ (Defines _) text = text
  1097   | eval_text _ _ _ (Notes _) text = text;
  1098 
  1099 
  1100 (* for finish_elems (Int),
  1101    remove redundant elements of derived identifiers,
  1102    turn assumptions and definitions into facts,
  1103    satisfy hypotheses of facts *)
  1104 
  1105 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  1106   | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  1107   | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  1108   | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
  1109 
  1110   | finish_derived _ _ (Derived _) (Fixes _) = NONE
  1111   | finish_derived _ _ (Derived _) (Constrains _) = NONE
  1112   | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
  1113       |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
  1114       |> pair Thm.assumptionK |> Notes
  1115       |> Element.morph_ctxt satisfy |> SOME
  1116   | finish_derived sign satisfy (Derived _) (Defines defs) = defs
  1117       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
  1118       |> pair Thm.definitionK |> Notes
  1119       |> Element.morph_ctxt satisfy |> SOME
  1120 
  1121   | finish_derived _ satisfy _ (Notes facts) = Notes facts
  1122       |> Element.morph_ctxt satisfy |> SOME;
  1123 
  1124 (* CB: for finish_elems (Ext) *)
  1125 
  1126 fun closeup _ false elem = elem
  1127   | closeup ctxt true elem =
  1128       let
  1129         fun close_frees t =
  1130           let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
  1131           in Term.list_all_free (frees, t) end;
  1132 
  1133         fun no_binds [] = []
  1134           | no_binds _ = error "Illegal term bindings in locale element";
  1135       in
  1136         (case elem of
  1137           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
  1138             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
  1139         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
  1140             (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
  1141         | e => e)
  1142       end;
  1143 
  1144 
  1145 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
  1146       (x, AList.lookup (op =) parms x, mx)) fixes)
  1147   | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  1148   | finish_ext_elem _ close (Assumes asms, propp) =
  1149       close (Assumes (map #1 asms ~~ propp))
  1150   | finish_ext_elem _ close (Defines defs, propp) =
  1151       close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
  1152   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
  1153 
  1154 
  1155 (* CB: finish_parms introduces type info from parms to identifiers *)
  1156 (* CB: only needed for types that have been NONE so far???
  1157    If so, which are these??? *)
  1158 
  1159 fun finish_parms parms (((name, ps), mode), elems) =
  1160   (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
  1161 
  1162 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
  1163       let
  1164         val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
  1165         val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
  1166         val text' = fold (eval_text ctxt id' false) es text;
  1167         val es' = map_filter
  1168           (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
  1169       in ((text', wits'), (id', map Int es')) end
  1170   | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
  1171       let
  1172         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
  1173         val text' = eval_text ctxt id true e' text;
  1174       in ((text', wits), (id, [Ext e'])) end
  1175 
  1176 in
  1177 
  1178 (* CB: only called by prep_elemss *)
  1179 
  1180 fun finish_elemss ctxt parms do_close =
  1181   foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
  1182 
  1183 end;
  1184 
  1185 
  1186 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
  1187 
  1188 fun defs_ord (defs1, defs2) =
  1189     list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
  1190       Term.fast_term_ord (d1, d2)) (defs1, defs2);
  1191 structure Defstab =
  1192     TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
  1193         val ord = defs_ord);
  1194 
  1195 fun rem_dup_defs es ds =
  1196     fold_map (fn e as (Defines defs) => (fn ds =>
  1197                  if Defstab.defined ds defs
  1198                  then (Defines [], ds)
  1199                  else (e, Defstab.update (defs, ()) ds))
  1200                | e => (fn ds => (e, ds))) es ds;
  1201 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
  1202   | rem_dup_elemss (Ext e) ds = (Ext e, ds);
  1203 fun rem_dup_defines raw_elemss =
  1204     fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
  1205                      apfst (pair id) (rem_dup_elemss es ds))
  1206                | (id as (_, (Derived _)), es) => (fn ds =>
  1207                      ((id, es), ds))) raw_elemss Defstab.empty |> #1;
  1208 
  1209 (* CB: type inference and consistency checks for locales.
  1210 
  1211    Works by building a context (through declare_elemss), extracting the
  1212    required information and adjusting the context elements (finish_elemss).
  1213    Can also universally close free vars in assms and defs.  This is only
  1214    needed for Ext elements and controlled by parameter do_close.
  1215 
  1216    Only elements of assumed identifiers are considered.
  1217 *)
  1218 
  1219 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
  1220   let
  1221     (* CB: contexts computed in the course of this function are discarded.
  1222        They are used for type inference and consistency checks only. *)
  1223     (* CB: fixed_params are the parameters (with types) of the target locale,
  1224        empty list if there is no target. *)
  1225     (* CB: raw_elemss are list of pairs consisting of identifiers and
  1226        context elements, the latter marked as internal or external. *)
  1227     val raw_elemss = rem_dup_defines raw_elemss;
  1228     val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
  1229     (* CB: raw_ctxt is context with additional fixed variables derived from
  1230        the fixes elements in raw_elemss,
  1231        raw_proppss contains assumptions and definitions from the
  1232        external elements in raw_elemss. *)
  1233     fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
  1234       let
  1235         (* CB: add type information from fixed_params to context (declare_term) *)
  1236         (* CB: process patterns (conclusion and external elements only) *)
  1237         val (ctxt, all_propp) =
  1238           prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  1239         (* CB: add type information from conclusion and external elements to context *)
  1240         val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
  1241         (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
  1242         val all_propp' = map2 (curry (op ~~))
  1243           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
  1244         val (concl, propp) = chop (length raw_concl) all_propp';
  1245       in (propp, (ctxt, concl)) end
  1246 
  1247     val (proppss, (ctxt, concl)) =
  1248       (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
  1249 
  1250     (* CB: obtain all parameters from identifier part of raw_elemss *)
  1251     val xs = map #1 (params_of' raw_elemss);
  1252     val typing = unify_frozen ctxt 0
  1253       (map (Variable.default_type raw_ctxt) xs)
  1254       (map (Variable.default_type ctxt) xs);
  1255     val parms = param_types (xs ~~ typing);
  1256     (* CB: parms are the parameters from raw_elemss, with correct typing. *)
  1257 
  1258     (* CB: extract information from assumes and defines elements
  1259        (fixes, constrains and notes in raw_elemss don't have an effect on
  1260        text and elemss), compute final form of context elements. *)
  1261     val ((text, _), elemss) = finish_elemss ctxt parms do_close
  1262       ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
  1263     (* CB: text has the following structure:
  1264            (((exts, exts'), (ints, ints')), (xs, env, defs))
  1265        where
  1266          exts: external assumptions (terms in external assumes elements)
  1267          exts': dito, normalised wrt. env
  1268          ints: internal assumptions (terms in internal assumes elements)
  1269          ints': dito, normalised wrt. env
  1270          xs: the free variables in exts' and ints' and rhss of definitions,
  1271            this includes parameters except defined parameters
  1272          env: list of term pairs encoding substitutions, where the first term
  1273            is a free variable; substitutions represent defines elements and
  1274            the rhs is normalised wrt. the previous env
  1275          defs: theorems representing the substitutions from defines elements
  1276            (thms are normalised wrt. env).
  1277        elemss is an updated version of raw_elemss:
  1278          - type info added to Fixes and modified in Constrains
  1279          - axiom and definition statement replaced by corresponding one
  1280            from proppss in Assumes and Defines
  1281          - Facts unchanged
  1282        *)
  1283   in ((parms, elemss, concl), text) end;
  1284 
  1285 in
  1286 
  1287 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
  1288 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
  1289 
  1290 end;
  1291 
  1292 
  1293 (* facts and attributes *)
  1294 
  1295 local
  1296 
  1297 fun check_name name =
  1298   if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
  1299   else name;
  1300 
  1301 fun prep_facts _ _ _ ctxt (Int elem) = elem
  1302       |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
  1303   | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  1304      {var = I, typ = I, term = I,
  1305       name = prep_name,
  1306       fact = get ctxt,
  1307       attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  1308 
  1309 in
  1310 
  1311 fun read_facts x = prep_facts check_name ProofContext.get_thms Attrib.intern_src x;
  1312 fun cert_facts x = prep_facts I (K I) (K I) x;
  1313 
  1314 end;
  1315 
  1316 
  1317 (* Get the specification of a locale *)
  1318 
  1319 (*The global specification is made from the parameters and global
  1320   assumptions, the local specification from the parameters and the
  1321   local assumptions.*)
  1322 
  1323 local
  1324 
  1325 fun gen_asms_of get thy name =
  1326   let
  1327     val ctxt = ProofContext.init thy;
  1328     val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
  1329     val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
  1330   in
  1331     elemss |> get
  1332       |> maps (fn (_, es) => map (fn Int e => e) es)
  1333       |> maps (fn Assumes asms => asms | _ => [])
  1334       |> map (apsnd (map fst))
  1335   end;
  1336 
  1337 in
  1338 
  1339 fun parameters_of thy name =
  1340   the_locale thy name |> #params;
  1341 
  1342 fun parameters_of_expr thy expr =
  1343   let
  1344     val ctxt = ProofContext.init thy;
  1345     val pts = params_of_expr ctxt [] (intern_expr thy expr)
  1346         ([], Symtab.empty, Symtab.empty);
  1347     val raw_params_elemss = make_raw_params_elemss pts;
  1348     val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  1349         (([], Symtab.empty), Expr expr);
  1350     val ((parms, _, _), _) =
  1351         read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
  1352   in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
  1353 
  1354 fun local_asms_of thy name =
  1355   gen_asms_of (single o Library.last_elem) thy name;
  1356 
  1357 fun global_asms_of thy name =
  1358   gen_asms_of I thy name;
  1359 
  1360 end;
  1361 
  1362 
  1363 (* full context statements: import + elements + conclusion *)
  1364 
  1365 local
  1366 
  1367 fun prep_context_statement prep_expr prep_elemss prep_facts
  1368     do_close fixed_params import elements raw_concl context =
  1369   let
  1370     val thy = ProofContext.theory_of context;
  1371 
  1372     val (import_params, import_tenv, import_syn) =
  1373       params_of_expr context fixed_params (prep_expr thy import)
  1374         ([], Symtab.empty, Symtab.empty);
  1375     val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
  1376     val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
  1377       (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
  1378 
  1379     val ((import_ids, _), raw_import_elemss) =
  1380       flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
  1381     (* CB: normalise "includes" among elements *)
  1382     val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
  1383       ((import_ids, incl_syn), elements);
  1384 
  1385     val raw_elemss = flat raw_elemsss;
  1386     (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  1387        context elements obtained from import and elements. *)
  1388     (* Now additional elements for parameters are inserted. *)
  1389     val import_params_ids = make_params_ids import_params;
  1390     val incl_params_ids =
  1391         make_params_ids (incl_params \\ import_params);
  1392     val raw_import_params_elemss =
  1393         make_raw_params_elemss (import_params, incl_tenv, incl_syn);
  1394     val raw_incl_params_elemss =
  1395         make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
  1396     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  1397       context fixed_params
  1398       (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
  1399 
  1400     (* replace extended ids (for axioms) by ids *)
  1401     val (import_ids', incl_ids) = chop (length import_ids) ids;
  1402     val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
  1403     val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
  1404         (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
  1405       (all_ids ~~ all_elemss);
  1406     (* CB: all_elemss and parms contain the correct parameter types *)
  1407 
  1408     val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  1409     val (import_ctxt, (import_elemss, _)) =
  1410       activate_facts false prep_facts (context, ps);
  1411 
  1412     val (ctxt, (elemss, _)) =
  1413       activate_facts false prep_facts (ProofContext.set_stmt true import_ctxt, qs);
  1414   in
  1415     ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  1416       (parms, spec, defs)), concl)
  1417   end;
  1418 
  1419 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  1420   let
  1421     val thy = ProofContext.theory_of ctxt;
  1422     val locale = Option.map (prep_locale thy) raw_locale;
  1423     val (fixed_params, import) =
  1424       (case locale of
  1425         NONE => ([], empty)
  1426       | SOME name =>
  1427           let val {params = ps, ...} = the_locale thy name
  1428           in (map fst ps, Locale name) end);
  1429     val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
  1430       prep_ctxt false fixed_params import elems concl ctxt;
  1431   in (locale, locale_ctxt, elems_ctxt, concl') end;
  1432 
  1433 fun prep_expr prep import body ctxt =
  1434   let
  1435     val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt;
  1436     val all_elems = maps snd (import_elemss @ elemss);
  1437   in (all_elems, ctxt') end;
  1438 
  1439 in
  1440 
  1441 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
  1442 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
  1443 
  1444 fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt);
  1445 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
  1446 
  1447 val read_expr = prep_expr read_context;
  1448 val cert_expr = prep_expr cert_context;
  1449 
  1450 fun read_context_statement loc = prep_statement intern read_ctxt loc;
  1451 fun read_context_statement_i loc = prep_statement (K I) read_ctxt loc;
  1452 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
  1453 
  1454 end;
  1455 
  1456 
  1457 (* print locale *)
  1458 
  1459 fun print_locale thy show_facts import body =
  1460   let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in
  1461     Pretty.big_list "locale elements:" (all_elems
  1462       |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
  1463       |> map (Pretty.chunks o Element.pretty_ctxt ctxt))
  1464     |> Pretty.writeln
  1465   end;
  1466 
  1467 
  1468 
  1469 (** store results **)
  1470 
  1471 (* naming of interpreted theorems *)
  1472 
  1473 fun global_note_prefix_i kind prfx args thy =
  1474   thy
  1475   |> Theory.qualified_names
  1476   |> Theory.sticky_prefix prfx
  1477   |> PureThy.note_thmss_i kind args
  1478   ||> Theory.restore_naming thy;
  1479 
  1480 fun local_note_prefix_i kind prfx args ctxt =
  1481   ctxt
  1482   |> ProofContext.qualified_names
  1483   |> ProofContext.sticky_prefix prfx
  1484   |> ProofContext.note_thmss_i kind args
  1485   ||> ProofContext.restore_naming ctxt;
  1486 
  1487 
  1488 (* collect witnesses for global registration;
  1489    requires parameters and flattened list of (assumed!) identifiers
  1490    instead of recomputing it from the target *)
  1491 
  1492 fun collect_global_witnesses thy parms ids vts = let
  1493     val ts = map Logic.unvarify vts;
  1494     val (parms, parmTs) = split_list parms;
  1495     val parmvTs = map Logic.varifyT parmTs;
  1496     val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
  1497     val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
  1498         |> Symtab.make;
  1499     (* replace parameter names in ids by instantiations *)
  1500     val vinst = Symtab.make (parms ~~ vts);
  1501     fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
  1502     val inst = Symtab.make (parms ~~ ts);
  1503     val ids' = map (apsnd vinst_names) ids;
  1504     val wits = maps (snd o the o get_global_registration thy) ids';
  1505   in ((tinst, inst), wits) end;
  1506 
  1507 
  1508 (* store instantiations of args for all registered interpretations
  1509    of the theory *)
  1510 
  1511 fun note_thmss_registrations target (kind, args) thy =
  1512   let
  1513     val parms = the_locale thy target |> #params |> map fst;
  1514     val ids = flatten (ProofContext.init thy, intern_expr thy)
  1515       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
  1516       |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
  1517 
  1518     val regs = get_global_registrations thy target;
  1519 
  1520     (* add args to thy for all registrations *)
  1521 
  1522     fun activate (vts, ((prfx, atts2), _)) thy =
  1523       let
  1524         val (insts, prems) = collect_global_witnesses thy parms ids vts;
  1525         val attrib = Attrib.attribute_i thy;
  1526         val inst_atts = Args.morph_values (Element.inst_morphism thy insts);
  1527         val inst_thm =
  1528           Drule.standard o Element.satisfy_thm prems o Element.inst_thm thy insts;
  1529         val args' = args |> map (fn ((name, atts), bs) =>
  1530             ((name, map (attrib o inst_atts) atts),
  1531               bs |> map (fn (ths, more_atts) =>
  1532                 (map inst_thm ths, map attrib (map inst_atts more_atts @ atts2)))));
  1533       in global_note_prefix_i kind prfx args' thy |> snd end;
  1534   in fold activate regs thy end;
  1535 
  1536 
  1537 (* init *)
  1538 
  1539 fun init_decls loc ctxt =
  1540   let
  1541     val (type_syntax, term_syntax, declarations) =
  1542       #decls (the_locale (ProofContext.theory_of ctxt) loc)
  1543     fun app (f, _) = f Morphism.identity;
  1544   in
  1545     ctxt
  1546     |> fold_rev app type_syntax
  1547     |> fold_rev app term_syntax
  1548     |> fold_rev app declarations
  1549   end;
  1550 
  1551 fun init loc =
  1552   ProofContext.init
  1553   #> init_decls loc
  1554   #> (#2 o cert_context_statement (SOME loc) [] []);
  1555 
  1556 
  1557 (* declarations *)
  1558 
  1559 fun add_decls which loc decl =
  1560   decl Morphism.identity #>
  1561   ProofContext.theory (change_locale loc
  1562     (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
  1563       (axiom, import, elems, params, lparams, which (decl, stamp ()) decls, regs, intros)));
  1564 
  1565 val add_type_syntax = add_decls (fn d => fn (ds1, ds2, ds3) => (d :: ds1, ds2, ds3));
  1566 val add_term_syntax = add_decls (fn d => fn (ds1, ds2, ds3) => (ds1, d :: ds2, ds3));
  1567 val add_declaration = add_decls (fn d => fn (ds1, ds2, ds3) => (ds1, ds2, d :: ds3));
  1568 
  1569 
  1570 (* locale results *)
  1571 
  1572 fun add_thmss loc kind args ctxt =
  1573   let
  1574     val (ctxt', ([(_, [Notes args'])], _)) =
  1575       activate_facts true cert_facts
  1576         (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
  1577     val ctxt'' = ctxt' |> ProofContext.theory
  1578       (change_locale loc
  1579         (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
  1580           (axiom, import, elems @ [(Notes args', stamp ())],
  1581             params, lparams, decls, regs, intros))
  1582       #> note_thmss_registrations loc args');
  1583   in ctxt'' end;
  1584 
  1585 
  1586 
  1587 (** define locales **)
  1588 
  1589 (* predicate text *)
  1590 (* CB: generate locale predicates and delta predicates *)
  1591 
  1592 local
  1593 
  1594 (* introN: name of theorems for introduction rules of locale and
  1595      delta predicates;
  1596    axiomsN: name of theorem set with destruct rules for locale predicates,
  1597      also name suffix of delta predicates. *)
  1598 
  1599 val introN = "intro";
  1600 val axiomsN = "axioms";
  1601 
  1602 fun atomize_spec thy ts =
  1603   let
  1604     val t = Logic.mk_conjunction_list ts;
  1605     val body = ObjectLogic.atomize_term thy t;
  1606     val bodyT = Term.fastype_of body;
  1607   in
  1608     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
  1609     else (body, bodyT, ObjectLogic.atomize_cterm (Thm.cterm_of thy t))
  1610   end;
  1611 
  1612 fun aprop_tr' n c = (c, fn args =>
  1613   if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
  1614   else raise Match);
  1615 
  1616 (* CB: define one predicate including its intro rule and axioms
  1617    - bname: predicate name
  1618    - parms: locale parameters
  1619    - defs: thms representing substitutions from defines elements
  1620    - ts: terms representing locale assumptions (not normalised wrt. defs)
  1621    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
  1622    - thy: the theory
  1623 *)
  1624 
  1625 fun def_pred bname parms defs ts norm_ts thy =
  1626   let
  1627     val name = Sign.full_name thy bname;
  1628 
  1629     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  1630     val env = Term.add_term_free_names (body, []);
  1631     val xs = filter (member (op =) env o #1) parms;
  1632     val Ts = map #2 xs;
  1633     val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
  1634       |> Library.sort_wrt #1 |> map TFree;
  1635     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
  1636 
  1637     val args = map Logic.mk_type extraTs @ map Free xs;
  1638     val head = Term.list_comb (Const (name, predT), args);
  1639     val statement = ObjectLogic.ensure_propT thy head;
  1640 
  1641     val ([pred_def], defs_thy) =
  1642       thy
  1643       |> (if bodyT <> propT then I else
  1644         Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
  1645       |> Theory.add_consts_i [(bname, predT, NoSyn)]
  1646       |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
  1647     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  1648 
  1649     val cert = Thm.cterm_of defs_thy;
  1650 
  1651     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
  1652       Tactic.rewrite_goals_tac [pred_def] THEN
  1653       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
  1654       Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
  1655 
  1656     val conjuncts =
  1657       (Drule.equal_elim_rule2 OF [body_eq,
  1658         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
  1659       |> Conjunction.elim_precise [length ts] |> hd;
  1660     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
  1661       Element.prove_witness defs_ctxt t
  1662        (Tactic.rewrite_goals_tac defs THEN
  1663         Tactic.compose_tac (false, ax, 0) 1));
  1664   in ((statement, intro, axioms), defs_thy) end;
  1665 
  1666 fun assumes_to_notes (Assumes asms) axms =
  1667       fold_map (fn (a, spec) => fn axs =>
  1668           let val (ps, qs) = chop (length spec) axs
  1669           in ((a, [(ps, [])]), qs) end) asms axms
  1670       |> apfst (curry Notes Thm.assumptionK)
  1671   | assumes_to_notes e axms = (e, axms);
  1672 
  1673 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
  1674 
  1675 (* turn Assumes into Notes elements *)
  1676 
  1677 fun change_assumes_elemss axioms elemss =
  1678   let
  1679     val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1680     fun change (id as ("", _), es) =
  1681           fold_map assumes_to_notes (map satisfy es)
  1682           #-> (fn es' => pair (id, es'))
  1683       | change e = pair e;
  1684   in
  1685     fst (fold_map change elemss (map Element.conclude_witness axioms))
  1686   end;
  1687 
  1688 (* adjust hyps of Notes elements *)
  1689 
  1690 fun change_elemss_hyps axioms elemss =
  1691   let
  1692     val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1693     fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
  1694       | change e = e;
  1695   in map change elemss end;
  1696 
  1697 in
  1698 
  1699 (* CB: main predicate definition function *)
  1700 
  1701 fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  1702   let
  1703     val ((elemss', more_ts), a_elem, a_intro, thy') =
  1704       if null exts then ((elemss, []), [], [], thy)
  1705       else
  1706         let
  1707           val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
  1708           val ((statement, intro, axioms), def_thy) =
  1709             thy |> def_pred aname parms defs exts exts';
  1710           val elemss' = change_assumes_elemss axioms elemss;
  1711           val def_thy' = def_thy
  1712             |> PureThy.note_thmss_qualified Thm.internalK
  1713               aname [((introN, []), [([intro], [])])]
  1714             |> snd;
  1715           val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  1716         in ((elemss', [statement]), a_elem, [intro], def_thy') end;
  1717     val (predicate, stmt', elemss'', b_intro, thy'') =
  1718       if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy')
  1719       else
  1720         let
  1721           val ((statement, intro, axioms), def_thy) =
  1722             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
  1723           val cstatement = Thm.cterm_of def_thy statement;
  1724           val elemss'' = change_elemss_hyps axioms elemss';
  1725           val def_thy' =
  1726           def_thy
  1727           |> PureThy.note_thmss_qualified Thm.internalK bname
  1728               [((introN, []), [([intro], [])]),
  1729                 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  1730           |> snd;
  1731           val b_elem = [(("", []),
  1732                [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  1733         in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], def_thy') end;
  1734   in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'') end;
  1735 
  1736 end;
  1737 
  1738 
  1739 (* add_locale(_i) *)
  1740 
  1741 local
  1742 
  1743 (* turn Defines into Notes elements, accumulate definition terms *)
  1744 
  1745 fun defines_to_notes is_ext thy (Defines defs) defns =
  1746     let
  1747       val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
  1748       val notes = map (fn (a, (def, _)) =>
  1749         (a, [([assume (cterm_of thy def)], [])])) defs
  1750     in
  1751       (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
  1752     end
  1753   | defines_to_notes _ _ e defns = (SOME e, defns);
  1754 
  1755 fun change_defines_elemss thy elemss defns =
  1756   let
  1757     fun change (id as (n, _), es) defns =
  1758         let
  1759           val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
  1760         in ((id, map_filter I es'), defns') end
  1761   in fold_map change elemss defns end;
  1762 
  1763 fun gen_add_locale prep_ctxt prep_expr
  1764     do_predicate bname raw_import raw_body thy =
  1765   let
  1766     val name = Sign.full_name thy bname;
  1767     val _ = conditional (is_some (get_locale thy name)) (fn () =>
  1768       error ("Duplicate definition of locale " ^ quote name));
  1769 
  1770     val thy_ctxt = ProofContext.init thy;
  1771     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  1772       text as (parms, ((_, exts'), _), defs)) =
  1773       prep_ctxt raw_import raw_body thy_ctxt;
  1774     val elemss = import_elemss @ body_elemss |>
  1775         map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  1776     val import = prep_expr thy raw_import;
  1777 
  1778     val extraTs = foldr Term.add_term_tfrees [] exts' \\
  1779       foldr Term.add_typ_tfrees [] (map snd parms);
  1780     val _ = if null extraTs then ()
  1781       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  1782 
  1783     val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
  1784           pred_thy), (import, regs)) =
  1785       if do_predicate then
  1786         let
  1787           val (elemss', defns) = change_defines_elemss thy elemss [];
  1788           val elemss'' = elemss' @ [(("", []), defns)];
  1789           val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
  1790             define_preds bname text elemss'' thy;
  1791           fun mk_regs elemss wits =
  1792             fold_map (fn (id, elems) => fn wts => let
  1793                 val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
  1794                   SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
  1795                 val (wts1, wts2) = chop (length ts) wts
  1796               in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
  1797           val regs = mk_regs elemss''' axioms |>
  1798                 map_filter (fn (("", _), _) => NONE | e => SOME e);
  1799         in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
  1800       else ((((elemss, ([], []), []), ([], [])), thy), (import, []));
  1801 
  1802     fun axiomify axioms elemss =
  1803       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  1804                    val ts = flat (map_filter (fn (Assumes asms) =>
  1805                      SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1806                    val (axs1, axs2) = chop (length ts) axs;
  1807                  in (axs2, ((id, Assumed axs1), elems)) end)
  1808         |> snd;
  1809     val (ctxt, (_, facts)) = activate_facts true (K I)
  1810       (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
  1811     val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
  1812     val export = Goal.close_result o Goal.norm_result o
  1813       singleton (ProofContext.export view_ctxt thy_ctxt);
  1814     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  1815     val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
  1816     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  1817     val axs' = map (Element.assume_witness pred_thy) stmt';
  1818     val loc_ctxt = pred_thy
  1819       |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
  1820       |> declare_locale name
  1821       |> put_locale name
  1822        {axiom = axs',
  1823         import = import,
  1824         elems = map (fn e => (e, stamp ())) elems'',
  1825         params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  1826         lparams = map #1 (params_of' body_elemss),
  1827         decls = ([], [], []),
  1828         regs = regs,
  1829         intros = intros}
  1830       |> init name;
  1831   in (name, loc_ctxt) end;
  1832 
  1833 in
  1834 
  1835 val add_locale = gen_add_locale read_context intern_expr;
  1836 val add_locale_i = gen_add_locale cert_context (K I);
  1837 
  1838 end;
  1839 
  1840 val _ = Context.add_setup
  1841  (add_locale_i true "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
  1842   snd #> ProofContext.theory_of #>
  1843   add_locale_i true "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
  1844   snd #> ProofContext.theory_of);
  1845 
  1846 
  1847 
  1848 
  1849 (** Normalisation of locale statements ---
  1850     discharges goals implied by interpretations **)
  1851 
  1852 local
  1853 
  1854 fun locale_assm_intros thy =
  1855   Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
  1856     (#2 (GlobalLocalesData.get thy)) [];
  1857 fun locale_base_intros thy =
  1858   Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
  1859     (#2 (GlobalLocalesData.get thy)) [];
  1860 
  1861 fun all_witnesses ctxt =
  1862   let
  1863     val thy = ProofContext.theory_of ctxt;
  1864     fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
  1865         (Registrations.dest thy regs |> map (fn (_, (_, wits)) =>
  1866           map Element.conclude_witness wits) |> flat) @ thms)
  1867       registrations [];
  1868     val globals = get (#3 (GlobalLocalesData.get thy));
  1869     val locals = get (LocalLocalesData.get ctxt);
  1870   in globals @ locals end;
  1871 (* FIXME: proper varification *)
  1872 
  1873 in
  1874 
  1875 fun intro_locales_tac eager ctxt facts st =
  1876   let
  1877     val wits = all_witnesses ctxt |> map Thm.varifyT;
  1878     val thy = ProofContext.theory_of ctxt;
  1879     val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
  1880   in
  1881     (ALLGOALS (Method.insert_tac facts THEN'
  1882         REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
  1883       THEN Tactic.distinct_subgoals_tac) st
  1884   end;
  1885 
  1886 val _ = Context.add_setup (Method.add_methods
  1887   [("intro_locales",
  1888     Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
  1889     "back-chain introduction rules of locales without unfolding predicates"),
  1890    ("unfold_locales",
  1891     Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
  1892     "back-chain all introduction rules of locales")]);
  1893 
  1894 end;
  1895 
  1896 
  1897 (** Interpretation commands **)
  1898 
  1899 local
  1900 
  1901 (* extract proof obligations (assms and defs) from elements *)
  1902 
  1903 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
  1904   | extract_asms_elems ((id, Derived _), _) = (id, []);
  1905 
  1906 
  1907 (* activate instantiated facts in theory or context *)
  1908 
  1909 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
  1910         attn all_elemss new_elemss propss thmss thy_ctxt =
  1911   let
  1912     fun activate_elem disch (prfx, atts) (Notes (kind, facts)) thy_ctxt =
  1913         let
  1914           val facts' = facts
  1915             (* discharge hyps in attributes *)
  1916             |> Attrib.map_facts (attrib thy_ctxt o Args.morph_values (Morphism.thm_morphism disch))
  1917             (* append interpretation attributes *)
  1918             |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
  1919             (* discharge hyps *)
  1920             |> map (apsnd (map (apfst (map disch))));
  1921         in snd (note kind prfx facts' thy_ctxt) end
  1922       | activate_elem _ _ _ thy_ctxt = thy_ctxt;
  1923 
  1924     fun activate_elems disch ((id, _), elems) thy_ctxt =
  1925       let
  1926         val ((prfx, atts2), _) = the (get_reg thy_ctxt id)
  1927           handle Option => sys_error ("Unknown registration of " ^
  1928             quote (fst id) ^ " while activating facts.");
  1929       in fold (activate_elem disch (prfx, atts2)) elems thy_ctxt end;
  1930 
  1931     val thy_ctxt' = thy_ctxt
  1932       (* add registrations *)
  1933       |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
  1934       (* add witnesses of Assumed elements *)
  1935       |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
  1936 
  1937     val prems = flat (map_filter
  1938           (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
  1939             | ((_, Derived _), _) => NONE) all_elemss);
  1940     val satisfy = Element.satisfy_morphism prems;
  1941     val thy_ctxt'' = thy_ctxt'
  1942       (* add witnesses of Derived elements *)
  1943       |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness satisfy) thms)
  1944          (map_filter (fn ((_, Assumed _), _) => NONE
  1945             | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
  1946 
  1947     val disch' = std o Morphism.thm satisfy;  (* FIXME *)
  1948   in
  1949     thy_ctxt''
  1950     (* add facts to theory or context *)
  1951     |> fold (activate_elems disch') new_elemss
  1952   end;
  1953 
  1954 fun global_activate_facts_elemss x = gen_activate_facts_elemss
  1955       (fn thy => fn (name, ps) =>
  1956         get_global_registration thy (name, map Logic.varify ps))
  1957       global_note_prefix_i
  1958       Attrib.attribute_i Drule.standard
  1959       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
  1960       (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
  1961         Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
  1962         (* FIXME *)) x;
  1963 
  1964 fun local_activate_facts_elemss x = gen_activate_facts_elemss
  1965       get_local_registration
  1966       local_note_prefix_i
  1967       (Attrib.attribute_i o ProofContext.theory_of) I
  1968       put_local_registration
  1969       add_local_witness x;
  1970 
  1971 fun gen_prep_registration mk_ctxt is_local read_terms test_reg activate
  1972     attn expr insts thy_ctxt =
  1973   let
  1974     val ctxt = mk_ctxt thy_ctxt;
  1975     val thy = ProofContext.theory_of ctxt;
  1976 
  1977     val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
  1978     val pts = params_of_expr ctxt' [] (intern_expr thy expr)
  1979           ([], Symtab.empty, Symtab.empty);
  1980     val params_ids = make_params_ids (#1 pts);
  1981     val raw_params_elemss = make_raw_params_elemss pts;
  1982     val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
  1983           (([], Symtab.empty), Expr expr);
  1984     val ((parms, all_elemss, _), (_, (_, defs, _))) =
  1985           read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
  1986 
  1987     (** compute instantiation **)
  1988 
  1989     (* user input *)
  1990     val insts = if length parms < length insts
  1991          then error "More arguments than parameters in instantiation."
  1992          else insts @ replicate (length parms - length insts) NONE;
  1993     val (ps, pTs) = split_list parms;
  1994     val pvTs = map Logic.legacy_varifyT pTs;
  1995 
  1996     (* instantiations given by user *)
  1997     val given = map_filter (fn (_, (NONE, _)) => NONE
  1998          | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
  1999     val (given_ps, given_insts) = split_list given;
  2000     val tvars = foldr Term.add_typ_tvars [] pvTs;
  2001     val used = foldr Term.add_typ_varnames [] pvTs;
  2002     fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
  2003     val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
  2004     val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
  2005     val vars' = fold Term.add_varnames vs vars;
  2006     val _ = if null vars' then ()
  2007          else error ("Illegal schematic variable(s) in instantiation: " ^
  2008            commas_quote (map Syntax.string_of_vname vars'));
  2009     (* replace new types (which are TFrees) by ones with new names *)
  2010     val new_Tnames = foldr Term.add_term_tfree_names [] vs;
  2011     val new_Tnames' = Name.invent_list used "'a" (length new_Tnames);
  2012     val renameT =
  2013           if is_local then I
  2014           else Logic.legacy_unvarifyT o Term.map_type_tfree (fn (a, s) =>
  2015             TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
  2016     val rename =
  2017           if is_local then I
  2018           else Term.map_types renameT;
  2019 
  2020     val tinst = Symtab.make (map
  2021                 (fn ((x, 0), T) => (x, T |> renameT)
  2022                   | ((_, n), _) => sys_error "Internal error var in prep_registration") vinst);
  2023     val inst = Symtab.make (given_ps ~~ map rename vs);
  2024 
  2025     (* defined params without user input *)
  2026     val not_given = map_filter (fn (x, (NONE, T)) => SOME (x, T)
  2027          | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
  2028     fun add_def (p, pT) inst =
  2029       let
  2030         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  2031                NONE => error ("Instance missing for parameter " ^ quote p)
  2032              | SOME (Free (_, T), t) => (t, T);
  2033         val d = Element.inst_term (tinst, inst) t;
  2034       in Symtab.update_new (p, d) inst end;
  2035     val inst = fold add_def not_given inst;
  2036     val insts = (tinst, inst);
  2037     val inst_morphism = Element.inst_morphism thy insts;
  2038     (* Note: insts contain no vars. *)
  2039 
  2040 
  2041     (** compute proof obligations **)
  2042 
  2043     (* restore "small" ids *)
  2044     val ids' = map (fn ((n, ps), (_, mode)) =>
  2045           ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
  2046         ids;
  2047     val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
  2048     (* instantiate ids and elements *)
  2049     val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  2050       ((n, map (Morphism.term inst_morphism) ps),
  2051         map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
  2052       |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
  2053 
  2054     (* remove fragments already registered with theory or context *)
  2055     val new_inst_elemss = filter (fn ((id, _), _) =>
  2056           not (test_reg thy_ctxt id)) inst_elemss;
  2057     val new_ids = map #1 new_inst_elemss;
  2058 
  2059     val propss = map extract_asms_elems new_inst_elemss;
  2060 
  2061     val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
  2062     val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
  2063 
  2064   in (propss, activate attn' inst_elemss new_inst_elemss propss) end;
  2065 
  2066 val prep_global_registration = gen_prep_registration
  2067      ProofContext.init false
  2068      (fn thy => fn sorts => fn used =>
  2069        Sign.read_def_terms (thy, K NONE, sorts) used true)
  2070      (fn thy => fn (name, ps) =>
  2071        test_global_registration thy (name, map Logic.varify ps))
  2072      global_activate_facts_elemss;
  2073 
  2074 val prep_local_registration = gen_prep_registration
  2075      I true
  2076      (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
  2077      smart_test_registration
  2078      local_activate_facts_elemss;
  2079 
  2080 fun prep_registration_in_locale target expr thy =
  2081   (* target already in internal form *)
  2082   let
  2083     val ctxt = ProofContext.init thy;
  2084     val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
  2085         (([], Symtab.empty), Expr (Locale target));
  2086     val fixed = the_locale thy target |> #params |> map #1;
  2087     val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  2088         ((raw_target_ids, target_syn), Expr expr);
  2089     val (target_ids, ids) = chop (length raw_target_ids) all_ids;
  2090     val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
  2091 
  2092     (** compute proof obligations **)
  2093 
  2094     (* restore "small" ids, with mode *)
  2095     val ids' = map (apsnd snd) ids;
  2096     (* remove Int markers *)
  2097     val elemss' = map (fn (_, es) =>
  2098         map (fn Int e => e) es) elemss
  2099     (* extract assumptions and defs *)
  2100     val ids_elemss = ids' ~~ elemss';
  2101     val propss = map extract_asms_elems ids_elemss;
  2102 
  2103     (** activation function:
  2104         - add registrations to the target locale
  2105         - add induced registrations for all global registrations of
  2106           the target, unless already present
  2107         - add facts of induced registrations to theory **)
  2108 
  2109     val t_ids = map_filter
  2110         (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
  2111 
  2112     fun activate thmss thy = let
  2113         val satisfy = Element.satisfy_thm (flat thmss);
  2114         val ids_elemss_thmss = ids_elemss ~~ thmss;
  2115         val regs = get_global_registrations thy target;
  2116 
  2117         fun activate_id (((id, Assumed _), _), thms) thy =
  2118             thy |> put_registration_in_locale target id
  2119                 |> fold (add_witness_in_locale target id) thms
  2120           | activate_id _ thy = thy;
  2121 
  2122         fun activate_reg (vts, ((prfx, atts2), _)) thy =
  2123           let
  2124             val (insts, wits) = collect_global_witnesses thy fixed t_ids vts;
  2125             fun inst_parms ps = map
  2126                   (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
  2127             val disch = Element.satisfy_thm wits;
  2128             val new_elemss = filter (fn (((name, ps), _), _) =>
  2129                 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
  2130             fun activate_assumed_id (((_, Derived _), _), _) thy = thy
  2131               | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
  2132                 val ps' = inst_parms ps;
  2133               in
  2134                 if test_global_registration thy (name, ps')
  2135                 then thy
  2136                 else thy
  2137                   |> put_global_registration (name, ps') (prfx, atts2)
  2138                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2139                      (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
  2140               end;
  2141 
  2142             fun activate_derived_id ((_, Assumed _), _) thy = thy
  2143               | activate_derived_id (((name, ps), Derived ths), _) thy = let
  2144                 val ps' = inst_parms ps;
  2145               in
  2146                 if test_global_registration thy (name, ps')
  2147                 then thy
  2148                 else thy
  2149                   |> put_global_registration (name, ps') (prfx, atts2)
  2150                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2151                        (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
  2152                        (Element.inst_term insts t,
  2153                         disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
  2154               end;
  2155 
  2156             fun activate_elem (Notes (kind, facts)) thy =
  2157                 let
  2158                   val att_morphism =
  2159                     Morphism.thm_morphism satisfy $>
  2160                     Element.inst_morphism thy insts $>
  2161                     Morphism.thm_morphism disch;
  2162                   val facts' = facts
  2163                     |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
  2164                     |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
  2165                     |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
  2166                 in
  2167                   thy
  2168                   |> global_note_prefix_i kind prfx facts'
  2169                   |> snd
  2170                 end
  2171               | activate_elem _ thy = thy;
  2172 
  2173             fun activate_elems (_, elems) thy = fold activate_elem elems thy;
  2174 
  2175           in thy |> fold activate_assumed_id ids_elemss_thmss
  2176                  |> fold activate_derived_id ids_elemss
  2177                  |> fold activate_elems new_elemss end;
  2178       in
  2179         thy |> fold activate_id ids_elemss_thmss
  2180             |> fold activate_reg regs
  2181       end;
  2182 
  2183   in (propss, activate) end;
  2184 
  2185 fun prep_propp propss = propss |> map (fn (_, props) =>
  2186   map (rpair [] o Element.mark_witness) props);
  2187 
  2188 fun prep_result propps thmss =
  2189   ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
  2190 
  2191 in
  2192 
  2193 fun interpretation after_qed (prfx, atts) expr insts thy =
  2194   let
  2195     val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
  2196     fun after_qed' results =
  2197       ProofContext.theory (activate (prep_result propss results))
  2198       #> after_qed;
  2199   in
  2200     ProofContext.init thy
  2201     |> Proof.theorem_i NONE after_qed' (prep_propp propss)
  2202     |> Element.refine_witness |> Seq.hd
  2203   end;
  2204 
  2205 fun interpretation_in_locale after_qed (raw_target, expr) thy =
  2206   let
  2207     val target = intern thy raw_target;
  2208     val (propss, activate) = prep_registration_in_locale target expr thy;
  2209     val raw_propp = prep_propp propss;
  2210 
  2211     val (_, _, goal_ctxt, propp) = thy
  2212       |> ProofContext.init |> init_decls target
  2213       |> cert_context_statement (SOME target) [] raw_propp;
  2214 
  2215     fun after_qed' results =
  2216       ProofContext.theory (activate (prep_result propss results))
  2217       #> after_qed;
  2218   in
  2219     goal_ctxt
  2220     |> Proof.theorem_i NONE after_qed' propp
  2221     |> Element.refine_witness |> Seq.hd
  2222   end;
  2223 
  2224 fun interpret after_qed (prfx, atts) expr insts int state =
  2225   let
  2226     val _ = Proof.assert_forward_or_chain state;
  2227     val ctxt = Proof.context_of state;
  2228     val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;
  2229     fun after_qed' results =
  2230       Proof.map_context (K (ctxt |> activate (prep_result propss results)))
  2231       #> Proof.put_facts NONE
  2232       #> after_qed;
  2233   in
  2234     state
  2235     |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  2236       "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
  2237     |> Element.refine_witness |> Seq.hd
  2238   end;
  2239 
  2240 end;
  2241 
  2242 end;