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