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