src/Pure/Isar/locale.ML
author ballarin
Wed Dec 03 15:26:46 2008 +0100 (2008-12-03)
changeset 28950 b2db06eb214d
parent 28941 128459bd72d2
child 28965 1de908189869
permissions -rw-r--r--
Made global_note_qualified public.
     1 (*  Title:      Pure/Isar/locale.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
     4 
     5 Locales -- Isar proof contexts as meta-level predicates, with local
     6 syntax and implicit structures.
     7 
     8 Draws basic ideas from Florian Kammueller's original version of
     9 locales, but uses the richer infrastructure of Isar instead of the raw
    10 meta-logic.  Furthermore, structured import of contexts (with merge
    11 and rename operations) are provided, as well as type-inference of the
    12 signature parts, and predicate definitions of the specification text.
    13 
    14 Interpretation enables the reuse of theorems of locales in other
    15 contexts, namely those defined by theories, structured proofs and
    16 locales themselves.
    17 
    18 See also:
    19 
    20 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    21     In Stefano Berardi et al., Types for Proofs and Programs: International
    22     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    23 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    24     Dependencies between Locales. Technical Report TUM-I0607, Technische
    25     Universitaet Muenchen, 2006.
    26 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    27     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    28     pages 31-43, 2006.
    29 *)
    30 
    31 (* TODO:
    32 - beta-eta normalisation of interpretation parameters
    33 - dangling type frees in locales
    34 - test subsumption of interpretations when merging theories
    35 *)
    36 
    37 signature LOCALE =
    38 sig
    39   datatype expr =
    40     Locale of string |
    41     Rename of expr * (string * mixfix option) option list |
    42     Merge of expr list
    43   val empty: expr
    44 
    45   val intern: theory -> xstring -> string
    46   val intern_expr: theory -> expr -> expr
    47   val extern: theory -> string -> xstring
    48   val init: string -> theory -> Proof.context
    49 
    50   (* The specification of a locale *)
    51   val parameters_of: theory -> string -> ((string * typ) * mixfix) list
    52   val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
    53   val local_asms_of: theory -> string -> (Attrib.binding * term list) list
    54   val global_asms_of: theory -> string -> (Attrib.binding * term list) list
    55 
    56   (* Theorems *)
    57   val intros: theory -> string -> thm list * thm list
    58   val dests: theory -> string -> thm list
    59   (* Not part of the official interface.  DO NOT USE *)
    60   val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
    61 
    62   (* Not part of the official interface.  DO NOT USE *)
    63   val declarations_of: theory -> string -> declaration list * declaration list;
    64 
    65   (* Processing of locale statements *)
    66   val read_context_statement: string option -> Element.context list ->
    67     (string * string list) list list -> Proof.context ->
    68     string option * Proof.context * Proof.context * (term * term list) list list
    69   val read_context_statement_cmd: xstring option -> Element.context list ->
    70     (string * string list) list list -> Proof.context ->
    71     string option * Proof.context * Proof.context * (term * term list) list list
    72   val cert_context_statement: string option -> Element.context_i list ->
    73     (term * term list) list list -> Proof.context ->
    74     string option * Proof.context * Proof.context * (term * term list) list list
    75   val read_expr: expr -> Element.context list -> Proof.context ->
    76     Element.context_i list * Proof.context
    77   val cert_expr: expr -> Element.context_i list -> Proof.context ->
    78     Element.context_i list * Proof.context
    79 
    80   (* Diagnostic functions *)
    81   val print_locales: theory -> unit
    82   val print_locale: theory -> bool -> expr -> Element.context list -> unit
    83   val print_registrations: bool -> string -> Proof.context -> unit
    84 
    85   val add_locale: string -> bstring -> expr -> Element.context_i list -> theory
    86     -> string * Proof.context
    87   val add_locale_cmd: bstring -> expr -> Element.context list -> theory
    88     -> string * Proof.context
    89 
    90   (* Tactics *)
    91   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    92 
    93   (* Storing results *)
    94   val global_note_qualified: string ->
    95     ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    96     theory -> (string * thm list) list * theory
    97   val local_note_qualified: string ->
    98     ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    99     Proof.context -> (string * thm list) list * Proof.context
   100   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   101     Proof.context -> Proof.context
   102   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   103   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   104   val add_declaration: string -> declaration -> Proof.context -> Proof.context
   105 
   106   (* Interpretation *)
   107   val get_interpret_morph: theory -> (Name.binding -> Name.binding) -> string * string ->
   108     (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   109     string -> term list -> Morphism.morphism
   110   val interpretation: (Proof.context -> Proof.context) ->
   111     (Name.binding -> Name.binding) -> expr ->
   112     term option list * (Attrib.binding * term) list ->
   113     theory ->
   114     (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   115   val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   116     theory -> Proof.state
   117   val interpretation_in_locale: (Proof.context -> Proof.context) ->
   118     xstring * expr -> theory -> Proof.state
   119   val interpret: (Proof.state -> Proof.state Seq.seq) ->
   120     (Name.binding -> Name.binding) -> expr ->
   121     term option list * (Attrib.binding * term) list ->
   122     bool -> Proof.state ->
   123     (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   124   val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   125     bool -> Proof.state -> Proof.state
   126 end;
   127 
   128 structure Locale: LOCALE =
   129 struct
   130 
   131 (* legacy operations *)
   132 
   133 fun merge_lists _ xs [] = xs
   134   | merge_lists _ [] ys = ys
   135   | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   136 
   137 fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
   138 
   139 
   140 (* auxiliary: noting name bindings with qualified base names *)
   141 
   142 fun global_note_qualified kind facts thy =
   143   thy
   144   |> Sign.qualified_names
   145   |> PureThy.note_thmss kind facts
   146   ||> Sign.restore_naming thy;
   147 
   148 fun local_note_qualified kind facts ctxt =
   149   ctxt
   150   |> ProofContext.qualified_names
   151   |> ProofContext.note_thmss_i kind facts
   152   ||> ProofContext.restore_naming ctxt;
   153 
   154 
   155 (** locale elements and expressions **)
   156 
   157 datatype ctxt = datatype Element.ctxt;
   158 
   159 datatype expr =
   160   Locale of string |
   161   Rename of expr * (string * mixfix option) option list |
   162   Merge of expr list;
   163 
   164 val empty = Merge [];
   165 
   166 datatype 'a element =
   167   Elem of 'a | Expr of expr;
   168 
   169 fun map_elem f (Elem e) = Elem (f e)
   170   | map_elem _ (Expr e) = Expr e;
   171 
   172 type decl = declaration * stamp;
   173 
   174 type locale =
   175  {axiom: Element.witness list,
   176     (* For locales that define predicates this is [A [A]], where A is the locale
   177        specification.  Otherwise [].
   178        Only required to generate the right witnesses for locales with predicates. *)
   179   elems: (Element.context_i * stamp) list,
   180     (* Static content, neither Fixes nor Constrains elements *)
   181   params: ((string * typ) * mixfix) list,                        (*all term params*)
   182   decls: decl list * decl list,                    (*type/term_syntax declarations*)
   183   regs: ((string * string list) * Element.witness list) list,
   184     (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
   185   intros: thm list * thm list,
   186     (* Introduction rules: of delta predicate and locale predicate. *)
   187   dests: thm list}
   188     (* Destruction rules: projections from locale predicate to predicates of fragments. *)
   189 
   190 (* CB: an internal (Int) locale element was either imported or included,
   191    an external (Ext) element appears directly in the locale text. *)
   192 
   193 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   194 
   195 
   196 
   197 (** substitutions on Vars -- clone from element.ML **)
   198 
   199 (* instantiate types *)
   200 
   201 fun var_instT_type env =
   202   if Vartab.is_empty env then I
   203   else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x));
   204 
   205 fun var_instT_term env =
   206   if Vartab.is_empty env then I
   207   else Term.map_types (var_instT_type env);
   208 
   209 fun var_inst_term (envT, env) =
   210   if Vartab.is_empty env then var_instT_term envT
   211   else
   212     let
   213       val instT = var_instT_type envT;
   214       fun inst (Const (x, T)) = Const (x, instT T)
   215         | inst (Free (x, T)) = Free(x, instT T)
   216         | inst (Var (xi, T)) =
   217             (case Vartab.lookup env xi of
   218               NONE => Var (xi, instT T)
   219             | SOME t => t)
   220         | inst (b as Bound _) = b
   221         | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
   222         | inst (t $ u) = inst t $ inst u;
   223     in Envir.beta_norm o inst end;
   224 
   225 
   226 (** management of registrations in theories and proof contexts **)
   227 
   228 type registration =
   229   {prfx: (Name.binding -> Name.binding) * (string * string),
   230       (* first component: interpretation name morphism;
   231          second component: parameter prefix *)
   232     exp: Morphism.morphism,
   233       (* maps content to its originating context *)
   234     imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
   235       (* inverse of exp *)
   236     wits: Element.witness list,
   237       (* witnesses of the registration *)
   238     eqns: thm Termtab.table,
   239       (* theorems (equations) interpreting derived concepts and indexed by lhs *)
   240     morph: unit
   241       (* interpreting morphism *)
   242   }
   243 
   244 structure Registrations :
   245   sig
   246     type T
   247     val empty: T
   248     val join: T * T -> T
   249     val dest: theory -> T ->
   250       (term list *
   251         (((Name.binding -> Name.binding) * (string * string)) *
   252          (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
   253          Element.witness list *
   254          thm Termtab.table)) list
   255     val test: theory -> T * term list -> bool
   256     val lookup: theory ->
   257       T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   258       (((Name.binding -> Name.binding) * (string * string)) * Element.witness list * thm Termtab.table) option
   259     val insert: theory -> term list -> ((Name.binding -> Name.binding) * (string * string)) ->
   260       (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   261       T ->
   262       T * (term list * (((Name.binding -> Name.binding) * (string * string)) * Element.witness list)) list
   263     val add_witness: term list -> Element.witness -> T -> T
   264     val add_equation: term list -> thm -> T -> T
   265 (*
   266     val update_morph: term list -> Morphism.morphism -> T -> T
   267     val get_morph: theory -> T ->
   268       term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
   269       Morphism.morphism
   270 *)
   271   end =
   272 struct
   273   (* A registration is indexed by parameter instantiation.
   274      NB: index is exported whereas content is internalised. *)
   275   type T = registration Termtab.table;
   276 
   277   fun mk_reg prfx exp imp wits eqns morph =
   278     {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph};
   279 
   280   fun map_reg f reg =
   281     let
   282       val {prfx, exp, imp, wits, eqns, morph} = reg;
   283       val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph);
   284     in mk_reg prfx' exp' imp' wits' eqns' morph' end;
   285 
   286   val empty = Termtab.empty;
   287 
   288   (* term list represented as single term, for simultaneous matching *)
   289   fun termify ts =
   290     Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
   291   fun untermify t =
   292     let fun ut (Const _) ts = ts
   293           | ut (s $ t) ts = ut s (t::ts)
   294     in ut t [] end;
   295 
   296   (* joining of registrations:
   297      - prefix and morphisms of right theory;
   298      - witnesses are equal, no attempt to subsumption testing;
   299      - union of equalities, if conflicting (i.e. two eqns with equal lhs)
   300        eqn of right theory takes precedence *)
   301   fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) =>
   302       mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2);
   303 
   304   fun dest_transfer thy regs =
   305     Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) =>
   306       (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m))));
   307 
   308   fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
   309     map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns)));
   310 
   311   (* registrations that subsume t *)
   312   fun subsumers thy t regs =
   313     filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
   314 
   315   (* test if registration that subsumes the query is present *)
   316   fun test thy (regs, ts) =
   317     not (null (subsumers thy (termify ts) regs));
   318       
   319   (* look up registration, pick one that subsumes the query *)
   320   fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) =
   321     let
   322       val t = termify ts;
   323       val subs = subsumers thy t regs;
   324     in
   325       (case subs of
   326         [] => NONE
   327         | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) =>
   328           let
   329             val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   330             val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
   331                 (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst
   332                       |> var_instT_type impT)) |> Symtab.make;
   333             val inst' = dom' |> map (fn (t as Free (x, _)) =>
   334                 (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
   335                       |> var_inst_term (impT, imp))) |> Symtab.make;
   336             val inst'_morph = Element.inst_morphism thy (tinst', inst');
   337           in SOME (prfx,
   338             map (Element.morph_witness inst'_morph) wits,
   339             Termtab.map (Morphism.thm inst'_morph) eqns)
   340           end)
   341     end;
   342 
   343   (* add registration if not subsumed by ones already present,
   344      additionally returns registrations that are strictly subsumed *)
   345   fun insert thy ts prfx (exp, imp) regs =
   346     let
   347       val t = termify ts;
   348       val subs = subsumers thy t regs ;
   349     in (case subs of
   350         [] => let
   351                 val sups =
   352                   filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   353                 val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
   354               in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end
   355       | _ => (regs, []))
   356     end;
   357 
   358   fun gen_add f ts regs =
   359     let
   360       val t = termify ts;
   361     in
   362       Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs
   363     end;
   364 
   365   (* add witness theorem to registration,
   366      only if instantiation is exact, otherwise exception Option raised *)
   367   fun add_witness ts wit regs =
   368     gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m))
   369       ts regs;
   370 
   371   (* add equation to registration, replaces previous equation with same lhs;
   372      only if instantiation is exact, otherwise exception Option raised;
   373      exception TERM raised if not a meta equality *)
   374   fun add_equation ts thm regs =
   375     gen_add (fn (x, e, i, thms, eqns, m) =>
   376       (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
   377       ts regs;
   378 
   379 end;
   380 
   381 
   382 (** theory data : locales **)
   383 
   384 structure LocalesData = TheoryDataFun
   385 (
   386   type T = NameSpace.T * locale Symtab.table;
   387     (* 1st entry: locale namespace,
   388        2nd entry: locales of the theory *)
   389 
   390   val empty = (NameSpace.empty, Symtab.empty);
   391   val copy = I;
   392   val extend = I;
   393 
   394   fun join_locales _
   395     ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,
   396       {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
   397      {axiom = axiom,
   398       elems = merge_lists (eq_snd (op =)) elems elems',
   399       params = params,
   400       decls =
   401        (Library.merge (eq_snd (op =)) (decls1, decls1'),
   402         Library.merge (eq_snd (op =)) (decls2, decls2')),
   403       regs = merge_alists (op =) regs regs',
   404       intros = intros,
   405       dests = dests};
   406   fun merge _ ((space1, locs1), (space2, locs2)) =
   407     (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
   408 );
   409 
   410 
   411 
   412 (** context data : registrations **)
   413 
   414 structure RegistrationsData = GenericDataFun
   415 (
   416   type T = Registrations.T Symtab.table;  (*registrations, indexed by locale name*)
   417   val empty = Symtab.empty;
   418   val extend = I;
   419   fun merge _ = Symtab.join (K Registrations.join);
   420 );
   421 
   422 
   423 (** access locales **)
   424 
   425 val intern = NameSpace.intern o #1 o LocalesData.get;
   426 val extern = NameSpace.extern o #1 o LocalesData.get;
   427 
   428 fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   429 
   430 fun the_locale thy name = case get_locale thy name
   431  of SOME loc => loc
   432   | NONE => error ("Unknown locale " ^ quote name);
   433 
   434 fun register_locale name loc thy =
   435   thy |> LocalesData.map (fn (space, locs) =>
   436     (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
   437 
   438 fun change_locale name f thy =
   439   let
   440     val {axiom, elems, params, decls, regs, intros, dests} =
   441         the_locale thy name;
   442     val (axiom', elems', params', decls', regs', intros', dests') =
   443       f (axiom, elems, params, decls, regs, intros, dests);
   444   in
   445     thy
   446     |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
   447           elems = elems', params = params',
   448           decls = decls', regs = regs', intros = intros', dests = dests'}))
   449   end;
   450 
   451 fun print_locales thy =
   452   let val (space, locs) = LocalesData.get thy in
   453     Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   454     |> Pretty.writeln
   455   end;
   456 
   457 
   458 (* access registrations *)
   459 
   460 (* retrieve registration from theory or context *)
   461 
   462 fun get_registrations ctxt name =
   463   case Symtab.lookup (RegistrationsData.get ctxt) name of
   464       NONE => []
   465     | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;
   466 
   467 fun get_global_registrations thy = get_registrations (Context.Theory thy);
   468 fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
   469 
   470 
   471 fun get_registration ctxt imprt (name, ps) =
   472   case Symtab.lookup (RegistrationsData.get ctxt) name of
   473       NONE => NONE
   474     | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));
   475 
   476 fun get_global_registration thy = get_registration (Context.Theory thy);
   477 fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
   478 
   479 
   480 fun test_registration ctxt (name, ps) =
   481   case Symtab.lookup (RegistrationsData.get ctxt) name of
   482       NONE => false
   483     | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps);
   484 
   485 fun test_global_registration thy = test_registration (Context.Theory thy);
   486 fun test_local_registration ctxt = test_registration (Context.Proof ctxt);
   487 
   488 
   489 (* add registration to theory or context, ignored if subsumed *)
   490 
   491 fun put_registration (name, ps) prfx morphs ctxt =
   492   RegistrationsData.map (fn regs =>
   493     let
   494       val thy = Context.theory_of ctxt;
   495       val reg = the_default Registrations.empty (Symtab.lookup regs name);
   496       val (reg', sups) = Registrations.insert thy ps prfx morphs reg;
   497       val _ = if not (null sups) then warning
   498                 ("Subsumed interpretation(s) of locale " ^
   499                  quote (extern thy name) ^
   500                  "\nwith the following prefix(es):" ^
   501                   commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups))
   502               else ();
   503     in Symtab.update (name, reg') regs end) ctxt;
   504 
   505 fun put_global_registration id prfx morphs =
   506   Context.theory_map (put_registration id prfx morphs);
   507 fun put_local_registration id prfx morphs =
   508   Context.proof_map (put_registration id prfx morphs);
   509 
   510 fun put_registration_in_locale name id =
   511   change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   512     (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
   513 
   514 
   515 (* add witness theorem to registration, ignored if registration not present *)
   516 
   517 fun add_witness (name, ps) thm =
   518   RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));
   519 
   520 fun add_global_witness id thm = Context.theory_map (add_witness id thm);
   521 fun add_local_witness id thm = Context.proof_map (add_witness id thm);
   522 
   523 
   524 fun add_witness_in_locale name id thm =
   525   change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   526     let
   527       fun add (id', thms) =
   528         if id = id' then (id', thm :: thms) else (id', thms);
   529     in (axiom, elems, params, decls, map add regs, intros, dests) end);
   530 
   531 
   532 (* add equation to registration, ignored if registration not present *)
   533 
   534 fun add_equation (name, ps) thm =
   535   RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));
   536 
   537 fun add_global_equation id thm = Context.theory_map (add_equation id thm);
   538 fun add_local_equation id thm = Context.proof_map (add_equation id thm);
   539 
   540 (*
   541 (* update morphism of registration, ignored if registration not present *)
   542 
   543 fun update_morph (name, ps) morph =
   544   RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph));
   545 
   546 fun update_global_morph id morph = Context.theory_map (update_morph id morph);
   547 fun update_local_morph id morph = Context.proof_map (update_morph id morph);
   548 *)
   549 
   550 
   551 (* printing of registrations *)
   552 
   553 fun print_registrations show_wits loc ctxt =
   554   let
   555     val thy = ProofContext.theory_of ctxt;
   556     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   557     fun prt_term' t = if !show_types
   558           then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   559             Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   560           else prt_term t;
   561     val prt_thm = prt_term o prop_of;
   562     fun prt_inst ts =
   563         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
   564     fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx]
   565       | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx];
   566     fun prt_eqns [] = Pretty.str "no equations."
   567       | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   568           Pretty.breaks (map prt_thm eqns));
   569     fun prt_core ts eqns =
   570           [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
   571     fun prt_witns [] = Pretty.str "no witnesses."
   572       | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   573           Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   574     fun prt_reg (ts, (_, _, witns, eqns)) =
   575         if show_wits
   576           then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   577           else Pretty.block (prt_core ts eqns)
   578 
   579     val loc_int = intern thy loc;
   580     val regs = RegistrationsData.get (Context.Proof ctxt);
   581     val loc_regs = Symtab.lookup regs loc_int;
   582   in
   583     (case loc_regs of
   584         NONE => Pretty.str ("no interpretations")
   585       | SOME r => let
   586             val r' = Registrations.dest thy r;
   587             val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r';
   588           in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
   589     |> Pretty.writeln
   590   end;
   591 
   592 
   593 (* diagnostics *)
   594 
   595 fun err_in_locale ctxt msg ids =
   596   let
   597     val thy = ProofContext.theory_of ctxt;
   598     fun prt_id (name, parms) =
   599       [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   600     val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   601     val err_msg =
   602       if forall (fn (s, _) => s = "") ids then msg
   603       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   604         (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   605   in error err_msg end;
   606 
   607 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   608 
   609 
   610 fun pretty_ren NONE = Pretty.str "_"
   611   | pretty_ren (SOME (x, NONE)) = Pretty.str x
   612   | pretty_ren (SOME (x, SOME syn)) =
   613       Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
   614 
   615 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
   616   | pretty_expr thy (Rename (expr, xs)) =
   617       Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
   618   | pretty_expr thy (Merge es) =
   619       Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
   620 
   621 fun err_in_expr _ msg (Merge []) = error msg
   622   | err_in_expr ctxt msg expr =
   623     error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
   624       [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
   625        pretty_expr (ProofContext.theory_of ctxt) expr]));
   626 
   627 
   628 (** structured contexts: rename + merge + implicit type instantiation **)
   629 
   630 (* parameter types *)
   631 
   632 fun frozen_tvars ctxt Ts =
   633   #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   634   |> map (fn ((xi, S), T) => (xi, (S, T)));
   635 
   636 fun unify_frozen ctxt maxidx Ts Us =
   637   let
   638     fun paramify NONE i = (NONE, i)
   639       | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   640 
   641     val (Ts', maxidx') = fold_map paramify Ts maxidx;
   642     val (Us', maxidx'') = fold_map paramify Us maxidx';
   643     val thy = ProofContext.theory_of ctxt;
   644 
   645     fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   646           handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   647       | unify _ env = env;
   648     val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   649     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   650     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   651   in map (Option.map (Envir.norm_type unifier')) Vs end;
   652 
   653 fun params_of elemss =
   654   distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
   655 
   656 fun params_of' elemss =
   657   distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   658 
   659 fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
   660 
   661 
   662 (* CB: param_types has the following type:
   663   ('a * 'b option) list -> ('a * 'b) list *)
   664 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   665 
   666 
   667 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
   668   handle Symtab.DUP x => err_in_locale ctxt
   669     ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
   670 
   671 
   672 (* Distinction of assumed vs. derived identifiers.
   673    The former may have axioms relating assumptions of the context to
   674    assumptions of the specification fragment (for locales with
   675    predicates).  The latter have witnesses relating assumptions of the
   676    specification fragment to assumptions of other (assumed) specification
   677    fragments. *)
   678 
   679 datatype 'a mode = Assumed of 'a | Derived of 'a;
   680 
   681 fun map_mode f (Assumed x) = Assumed (f x)
   682   | map_mode f (Derived x) = Derived (f x);
   683 
   684 
   685 (* flatten expressions *)
   686 
   687 local
   688 
   689 fun unify_parms ctxt fixed_parms raw_parmss =
   690   let
   691     val thy = ProofContext.theory_of ctxt;
   692     val maxidx = length raw_parmss;
   693     val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   694 
   695     fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   696     fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   697     val parms = fixed_parms @ maps varify_parms idx_parmss;
   698 
   699     fun unify T U envir = Sign.typ_unify thy (U, T) envir
   700       handle Type.TUNIFY =>
   701         let
   702           val T' = Envir.norm_type (fst envir) T;
   703           val U' = Envir.norm_type (fst envir) U;
   704           val prt = Syntax.string_of_typ ctxt;
   705         in
   706           raise TYPE ("unify_parms: failed to unify types " ^
   707             prt U' ^ " and " ^ prt T', [U', T'], [])
   708         end;
   709     fun unify_list (T :: Us) = fold (unify T) Us
   710       | unify_list [] = I;
   711     val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
   712       (Vartab.empty, maxidx);
   713 
   714     val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
   715     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   716 
   717     fun inst_parms (i, ps) =
   718       List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
   719       |> map_filter (fn (a, S) =>
   720           let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   721           in if T = TFree (a, S) then NONE else SOME (a, T) end)
   722       |> Symtab.make;
   723   in map inst_parms idx_parmss end;
   724 
   725 in
   726 
   727 fun unify_elemss _ _ [] = []
   728   | unify_elemss _ [] [elems] = [elems]
   729   | unify_elemss ctxt fixed_parms elemss =
   730       let
   731         val thy = ProofContext.theory_of ctxt;
   732         val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
   733           |> map (Element.instT_morphism thy);
   734         fun inst ((((name, ps), mode), elems), phi) =
   735           (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
   736               map_mode (map (Element.morph_witness phi)) mode),
   737             map (Element.morph_ctxt phi) elems);
   738       in map inst (elemss ~~ phis) end;
   739 
   740 
   741 fun renaming xs parms = zip_options parms xs
   742   handle Library.UnequalLengths =>
   743     error ("Too many arguments in renaming: " ^
   744       commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
   745 
   746 
   747 (* params_of_expr:
   748    Compute parameters (with types and syntax) of locale expression.
   749 *)
   750 
   751 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
   752   let
   753     val thy = ProofContext.theory_of ctxt;
   754 
   755     fun merge_tenvs fixed tenv1 tenv2 =
   756         let
   757           val [env1, env2] = unify_parms ctxt fixed
   758                 [tenv1 |> Symtab.dest |> map (apsnd SOME),
   759                  tenv2 |> Symtab.dest |> map (apsnd SOME)]
   760         in
   761           Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
   762             Symtab.map (Element.instT_type env2) tenv2)
   763         end;
   764 
   765     fun merge_syn expr syn1 syn2 =
   766         Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
   767         handle Symtab.DUP x => err_in_expr ctxt
   768           ("Conflicting syntax for parameter: " ^ quote x) expr;
   769 
   770     fun params_of (expr as Locale name) =
   771           let
   772             val {params, ...} = the_locale thy name;
   773           in (map (fst o fst) params, params |> map fst |> Symtab.make,
   774                params |> map (apfst fst) |> Symtab.make) end
   775       | params_of (expr as Rename (e, xs)) =
   776           let
   777             val (parms', types', syn') = params_of e;
   778             val ren = renaming xs parms';
   779             (* renaming may reduce number of parameters *)
   780             val new_parms = map (Element.rename ren) parms' |> distinct (op =);
   781             val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
   782             val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
   783                 handle Symtab.DUP x =>
   784                   err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
   785             val syn_types = map (apsnd (fn mx =>
   786                 SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0)))))
   787               (Symtab.dest new_syn);
   788             val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
   789             val (env :: _) = unify_parms ctxt []
   790                 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
   791             val new_types = fold (Symtab.insert (op =))
   792                 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
   793           in (new_parms, new_types, new_syn) end
   794       | params_of (Merge es) =
   795           fold (fn e => fn (parms, types, syn) =>
   796                    let
   797                      val (parms', types', syn') = params_of e
   798                    in
   799                      (merge_lists (op =) parms parms', merge_tenvs [] types types',
   800                       merge_syn e syn syn')
   801                    end)
   802             es ([], Symtab.empty, Symtab.empty)
   803 
   804       val (parms, types, syn) = params_of expr;
   805     in
   806       (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
   807        merge_syn expr prev_syn syn)
   808     end;
   809 
   810 fun make_params_ids params = [(("", params), ([], Assumed []))];
   811 fun make_raw_params_elemss (params, tenv, syn) =
   812     [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   813       Int [Fixes (map (fn p =>
   814         (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   815 
   816 
   817 (* flatten_expr:
   818    Extend list of identifiers by those new in locale expression expr.
   819    Compute corresponding list of lists of locale elements (one entry per
   820    identifier).
   821 
   822    Identifiers represent locale fragments and are in an extended form:
   823      ((name, ps), (ax_ps, axs))
   824    (name, ps) is the locale name with all its parameters.
   825    (ax_ps, axs) is the locale axioms with its parameters;
   826      axs are always taken from the top level of the locale hierarchy,
   827      hence axioms may contain additional parameters from later fragments:
   828      ps subset of ax_ps.  axs is either singleton or empty.
   829 
   830    Elements are enriched by identifier-like information:
   831      (((name, ax_ps), axs), elems)
   832    The parameters in ax_ps are the axiom parameters, but enriched by type
   833    info: now each entry is a pair of string and typ option.  Axioms are
   834    type-instantiated.
   835 
   836 *)
   837 
   838 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
   839   let
   840     val thy = ProofContext.theory_of ctxt;
   841 
   842     fun rename_parms top ren ((name, ps), (parms, mode)) =
   843         ((name, map (Element.rename ren) ps),
   844          if top
   845          then (map (Element.rename ren) parms,
   846                map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
   847          else (parms, mode));
   848 
   849     (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *)
   850 
   851     fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
   852         if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
   853         then (wits, ids, visited)
   854         else
   855           let
   856             val {params, regs, ...} = the_locale thy name;
   857             val pTs' = map #1 params;
   858             val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
   859               (* dummy syntax, since required by rename *)
   860             val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
   861             val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
   862               (* propagate parameter types, to keep them consistent *)
   863             val regs' = map (fn ((name, ps), wits) =>
   864                 ((name, map (Element.rename ren) ps),
   865                  map (Element.transfer_witness thy) wits)) regs;
   866             val new_regs = regs';
   867             val new_ids = map fst new_regs;
   868             val new_idTs =
   869               map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
   870 
   871             val new_wits = new_regs |> map (#2 #> map
   872               (Element.morph_witness
   873                 (Element.instT_morphism thy env $>
   874                   Element.rename_morphism ren $>
   875                   Element.satisfy_morphism wits)
   876                 #> Element.close_witness));
   877             val new_ids' = map (fn (id, wits) =>
   878                 (id, ([], Derived wits))) (new_ids ~~ new_wits);
   879             val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
   880                 ((n, pTs), mode)) (new_idTs ~~ new_ids');
   881             val new_id = ((name, map #1 pTs), ([], mode));
   882             val (wits', ids', visited') = fold add_with_regs new_idTs'
   883               (wits @ flat new_wits, ids, visited @ [new_id]);
   884           in
   885             (wits', ids' @ [new_id], visited')
   886           end;
   887 
   888     (* distribute top-level axioms over assumed ids *)
   889 
   890     fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
   891         let
   892           val {elems, ...} = the_locale thy name;
   893           val ts = maps
   894             (fn (Assumes asms, _) => maps (map #1 o #2) asms
   895               | _ => [])
   896             elems;
   897           val (axs1, axs2) = chop (length ts) axioms;
   898         in (((name, parms), (all_ps, Assumed axs1)), axs2) end
   899       | axiomify all_ps (id, (_, Derived ths)) axioms =
   900           ((id, (all_ps, Derived ths)), axioms);
   901 
   902     (* identifiers of an expression *)
   903 
   904     fun identify top (Locale name) =
   905     (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
   906        where name is a locale name, ps a list of parameter names and axs
   907        a list of axioms relating to the identifier, axs is empty unless
   908        identify at top level (top = true);
   909        parms is accumulated list of parameters *)
   910           let
   911             val {axiom, params, ...} = the_locale thy name;
   912             val ps = map (#1 o #1) params;
   913             val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);
   914             val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
   915             in (ids_ax, ps) end
   916       | identify top (Rename (e, xs)) =
   917           let
   918             val (ids', parms') = identify top e;
   919             val ren = renaming xs parms'
   920               handle ERROR msg => err_in_locale' ctxt msg ids';
   921 
   922             val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   923             val parms'' = distinct (op =) (maps (#2 o #1) ids'');
   924           in (ids'', parms'') end
   925       | identify top (Merge es) =
   926           fold (fn e => fn (ids, parms) =>
   927                    let
   928                      val (ids', parms') = identify top e
   929                    in
   930                      (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
   931                    end)
   932             es ([], []);
   933 
   934     fun inst_wit all_params (t, th) = let
   935          val {hyps, prop, ...} = Thm.rep_thm th;
   936          val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
   937          val [env] = unify_parms ctxt all_params [ps];
   938          val t' = Element.instT_term env t;
   939          val th' = Element.instT_thm thy env th;
   940        in (t', th') end;
   941 
   942     fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
   943       let
   944         val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
   945         val elems = map fst elems_stamped;
   946         val ps = map fst ps_mx;
   947         fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
   948         val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
   949         val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
   950         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
   951         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   952         val (lprfx, pprfx) = param_prefix name params;
   953         val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
   954           #> Binding.add_prefix false lprfx;
   955         val elem_morphism =
   956           Element.rename_morphism ren $>
   957           Morphism.name_morphism add_prefices $>
   958           Element.instT_morphism thy env;
   959         val elems' = map (Element.morph_ctxt elem_morphism) elems;
   960       in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   961 
   962     (* parameters, their types and syntax *)
   963     val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
   964     val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
   965     (* compute identifiers and syntax, merge with previous ones *)
   966     val (ids, _) = identify true expr;
   967     val idents = subtract (eq_fst (op =)) prev_idents ids;
   968     val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   969     (* type-instantiate elements *)
   970     val final_elemss = map (eval all_params tenv syntax) idents;
   971   in ((prev_idents @ idents, syntax), final_elemss) end;
   972 
   973 end;
   974 
   975 
   976 (* activate elements *)
   977 
   978 local
   979 
   980 fun axioms_export axs _ As =
   981   (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
   982 
   983 
   984 (* NB: derived ids contain only facts at this stage *)
   985 
   986 fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
   987       ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
   988   | activate_elem _ _ (Constrains _) (ctxt, mode) =
   989       ([], (ctxt, mode))
   990   | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
   991       let
   992         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   993         val ts = maps (map #1 o #2) asms';
   994         val (ps, qs) = chop (length ts) axs;
   995         val (_, ctxt') =
   996           ctxt |> fold Variable.auto_fixes ts
   997           |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
   998       in ([], (ctxt', Assumed qs)) end
   999   | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
  1000       ([], (ctxt, Derived ths))
  1001   | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
  1002       let
  1003         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  1004         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  1005             let val ((c, _), t') = LocalDefs.cert_def ctxt t
  1006             in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  1007         val (_, ctxt') =
  1008           ctxt |> fold (Variable.auto_fixes o #1) asms
  1009           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  1010       in ([], (ctxt', Assumed axs)) end
  1011   | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
  1012       ([], (ctxt, Derived ths))
  1013   | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
  1014       let
  1015         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
  1016         val (res, ctxt') = ctxt |> local_note_qualified kind facts';
  1017       in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
  1018 
  1019 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  1020   let
  1021     val thy = ProofContext.theory_of ctxt;
  1022     val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
  1023         elems (ProofContext.qualified_names ctxt, mode)
  1024       handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
  1025     val ctxt'' = if name = "" then ctxt'
  1026           else let
  1027               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
  1028             in if test_local_registration ctxt' (name, ps') then ctxt'
  1029               else let
  1030                   val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, ""))
  1031                     (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
  1032                 in case mode of
  1033                     Assumed axs =>
  1034                       fold (add_local_witness (name, ps') o
  1035                         Element.assume_witness thy o Element.witness_prop) axs ctxt''
  1036                   | Derived ths =>
  1037                      fold (add_local_witness (name, ps')) ths ctxt''
  1038                 end
  1039             end
  1040   in (ProofContext.restore_naming ctxt ctxt'', res) end;
  1041 
  1042 fun activate_elemss ax_in_ctxt prep_facts =
  1043     fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
  1044       let
  1045         val elems = map (prep_facts ctxt) raw_elems;
  1046         val (ctxt', res) = apsnd flat
  1047             (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
  1048         val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
  1049       in (((((name, ps), mode), elems'), res), ctxt') end);
  1050 
  1051 in
  1052 
  1053 (* CB: activate_facts prep_facts elemss ctxt,
  1054    where elemss is a list of pairs consisting of identifiers and
  1055    context elements, extends ctxt by the context elements yielding
  1056    ctxt' and returns ((elemss', facts), ctxt').
  1057    Identifiers in the argument are of the form ((name, ps), axs) and
  1058    assumptions use the axioms in the identifiers to set up exporters
  1059    in ctxt'.  elemss' does not contain identifiers and is obtained
  1060    from elemss and the intermediate context with prep_facts.
  1061    If read_facts or cert_facts is used for prep_facts, these also remove
  1062    the internal/external markers from elemss. *)
  1063 
  1064 fun activate_facts ax_in_ctxt prep_facts args =
  1065   activate_elemss ax_in_ctxt prep_facts args
  1066   #>> (apsnd flat o split_list);
  1067 
  1068 end;
  1069 
  1070 
  1071 
  1072 (** prepare locale elements **)
  1073 
  1074 (* expressions *)
  1075 
  1076 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
  1077   | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
  1078   | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
  1079 
  1080 
  1081 (* propositions and bindings *)
  1082 
  1083 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
  1084    normalises expr (which is either a locale
  1085    expression or a single context element) wrt.
  1086    to the list ids of already accumulated identifiers.
  1087    It returns ((ids', syn'), elemss) where ids' is an extension of ids
  1088    with identifiers generated for expr, and elemss is the list of
  1089    context elements generated from expr.
  1090    syn and syn' are symtabs mapping parameter names to their syntax.  syn'
  1091    is an extension of syn.
  1092    For details, see flatten_expr.
  1093 
  1094    Additionally, for a locale expression, the elems are grouped into a single
  1095    Int; individual context elements are marked Ext.  In this case, the
  1096    identifier-like information of the element is as follows:
  1097    - for Fixes: (("", ps), []) where the ps have type info NONE
  1098    - for other elements: (("", []), []).
  1099    The implementation of activate_facts relies on identifier names being
  1100    empty strings for external elements.
  1101 *)
  1102 
  1103 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
  1104         val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
  1105       in
  1106         ((ids',
  1107          merge_syntax ctxt ids'
  1108            (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
  1109            handle Symtab.DUP x => err_in_locale ctxt
  1110              ("Conflicting syntax for parameter: " ^ quote x)
  1111              (map #1 ids')),
  1112          [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
  1113       end
  1114   | flatten _ ((ids, syn), Elem elem) =
  1115       ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  1116   | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
  1117       apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
  1118 
  1119 local
  1120 
  1121 local
  1122 
  1123 fun declare_int_elem (Fixes fixes) ctxt =
  1124       ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  1125         (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
  1126   | declare_int_elem _ ctxt = ([], ctxt);
  1127 
  1128 fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
  1129       let val (vars, _) = prep_vars fixes ctxt
  1130       in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
  1131   | declare_ext_elem prep_vars (Constrains csts) ctxt =
  1132       let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
  1133       in ([], ctxt') end
  1134   | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
  1135   | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
  1136   | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
  1137 
  1138 fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
  1139      of Int es => fold_map declare_int_elem es ctxt
  1140       | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
  1141           handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
  1142   | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
  1143 
  1144 in
  1145 
  1146 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
  1147   let
  1148     (* CB: fix of type bug of goal in target with context elements.
  1149        Parameters new in context elements must receive types that are
  1150        distinct from types of parameters in target (fixed_params).  *)
  1151     val ctxt_with_fixed = 
  1152       fold Variable.declare_term (map Free fixed_params) ctxt;
  1153     val int_elemss =
  1154       raw_elemss
  1155       |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  1156       |> unify_elemss ctxt_with_fixed fixed_params;
  1157     val (raw_elemss', _) =
  1158       fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
  1159         raw_elemss int_elemss;
  1160   in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
  1161 
  1162 end;
  1163 
  1164 local
  1165 
  1166 val norm_term = Envir.beta_norm oo Term.subst_atomic;
  1167 
  1168 fun abstract_thm thy eq =
  1169   Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
  1170 
  1171 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
  1172   let
  1173     val ((y, T), b) = LocalDefs.abs_def eq;
  1174     val b' = norm_term env b;
  1175     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
  1176     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  1177   in
  1178     exists (fn (x, _) => x = y) xs andalso
  1179       err "Attempt to define previously specified variable";
  1180     exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
  1181       err "Attempt to redefine variable";
  1182     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  1183   end;
  1184 
  1185 
  1186 (* CB: for finish_elems (Int and Ext),
  1187    extracts specification, only of assumed elements *)
  1188 
  1189 fun eval_text _ _ _ (Fixes _) text = text
  1190   | eval_text _ _ _ (Constrains _) text = text
  1191   | eval_text _ (_, Assumed _) is_ext (Assumes asms)
  1192         (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  1193       let
  1194         val ts = maps (map #1 o #2) asms;
  1195         val ts' = map (norm_term env) ts;
  1196         val spec' =
  1197           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  1198           else ((exts, exts'), (ints @ ts, ints' @ ts'));
  1199       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  1200   | eval_text _ (_, Derived _) _ (Assumes _) text = text
  1201   | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
  1202       (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
  1203   | eval_text _ (_, Derived _) _ (Defines _) text = text
  1204   | eval_text _ _ _ (Notes _) text = text;
  1205 
  1206 
  1207 (* for finish_elems (Int),
  1208    remove redundant elements of derived identifiers,
  1209    turn assumptions and definitions into facts,
  1210    satisfy hypotheses of facts *)
  1211 
  1212 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  1213   | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  1214   | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  1215   | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
  1216 
  1217   | finish_derived _ _ (Derived _) (Fixes _) = NONE
  1218   | finish_derived _ _ (Derived _) (Constrains _) = NONE
  1219   | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
  1220       |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
  1221       |> pair Thm.assumptionK |> Notes
  1222       |> Element.morph_ctxt satisfy |> SOME
  1223   | finish_derived sign satisfy (Derived _) (Defines defs) = defs
  1224       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
  1225       |> pair Thm.definitionK |> Notes
  1226       |> Element.morph_ctxt satisfy |> SOME
  1227 
  1228   | finish_derived _ satisfy _ (Notes facts) = Notes facts
  1229       |> Element.morph_ctxt satisfy |> SOME;
  1230 
  1231 (* CB: for finish_elems (Ext) *)
  1232 
  1233 fun closeup _ false elem = elem
  1234   | closeup ctxt true elem =
  1235       let
  1236         fun close_frees t =
  1237           let
  1238             val rev_frees =
  1239               Term.fold_aterms (fn Free (x, T) =>
  1240                 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
  1241           in Term.list_all_free (rev rev_frees, t) end;
  1242 
  1243         fun no_binds [] = []
  1244           | no_binds _ = error "Illegal term bindings in locale element";
  1245       in
  1246         (case elem of
  1247           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
  1248             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
  1249         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
  1250             (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
  1251         | e => e)
  1252       end;
  1253 
  1254 
  1255 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
  1256       let val x = Name.name_of b
  1257       in (b, AList.lookup (op =) parms x, mx) end) fixes)
  1258   | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  1259   | finish_ext_elem _ close (Assumes asms, propp) =
  1260       close (Assumes (map #1 asms ~~ propp))
  1261   | finish_ext_elem _ close (Defines defs, propp) =
  1262       close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
  1263   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
  1264 
  1265 
  1266 (* CB: finish_parms introduces type info from parms to identifiers *)
  1267 (* CB: only needed for types that have been NONE so far???
  1268    If so, which are these??? *)
  1269 
  1270 fun finish_parms parms (((name, ps), mode), elems) =
  1271   (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
  1272 
  1273 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
  1274       let
  1275         val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
  1276         val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
  1277         val text' = fold (eval_text ctxt id' false) es text;
  1278         val es' = map_filter
  1279           (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
  1280       in ((text', wits'), (id', map Int es')) end
  1281   | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
  1282       let
  1283         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
  1284         val text' = eval_text ctxt id true e' text;
  1285       in ((text', wits), (id, [Ext e'])) end
  1286 
  1287 in
  1288 
  1289 (* CB: only called by prep_elemss *)
  1290 
  1291 fun finish_elemss ctxt parms do_close =
  1292   foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
  1293 
  1294 end;
  1295 
  1296 
  1297 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
  1298 
  1299 fun defs_ord (defs1, defs2) =
  1300     list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
  1301       Term.fast_term_ord (d1, d2)) (defs1, defs2);
  1302 structure Defstab =
  1303     TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
  1304 
  1305 fun rem_dup_defs es ds =
  1306     fold_map (fn e as (Defines defs) => (fn ds =>
  1307                  if Defstab.defined ds defs
  1308                  then (Defines [], ds)
  1309                  else (e, Defstab.update (defs, ()) ds))
  1310                | e => (fn ds => (e, ds))) es ds;
  1311 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
  1312   | rem_dup_elemss (Ext e) ds = (Ext e, ds);
  1313 fun rem_dup_defines raw_elemss =
  1314     fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
  1315                      apfst (pair id) (rem_dup_elemss es ds))
  1316                | (id as (_, (Derived _)), es) => (fn ds =>
  1317                      ((id, es), ds))) raw_elemss Defstab.empty |> #1;
  1318 
  1319 (* CB: type inference and consistency checks for locales.
  1320 
  1321    Works by building a context (through declare_elemss), extracting the
  1322    required information and adjusting the context elements (finish_elemss).
  1323    Can also universally close free vars in assms and defs.  This is only
  1324    needed for Ext elements and controlled by parameter do_close.
  1325 
  1326    Only elements of assumed identifiers are considered.
  1327 *)
  1328 
  1329 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
  1330   let
  1331     (* CB: contexts computed in the course of this function are discarded.
  1332        They are used for type inference and consistency checks only. *)
  1333     (* CB: fixed_params are the parameters (with types) of the target locale,
  1334        empty list if there is no target. *)
  1335     (* CB: raw_elemss are list of pairs consisting of identifiers and
  1336        context elements, the latter marked as internal or external. *)
  1337     val raw_elemss = rem_dup_defines raw_elemss;
  1338     val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
  1339     (* CB: raw_ctxt is context with additional fixed variables derived from
  1340        the fixes elements in raw_elemss,
  1341        raw_proppss contains assumptions and definitions from the
  1342        external elements in raw_elemss. *)
  1343     fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
  1344       let
  1345         (* CB: add type information from fixed_params to context (declare_term) *)
  1346         (* CB: process patterns (conclusion and external elements only) *)
  1347         val (ctxt, all_propp) =
  1348           prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  1349         (* CB: add type information from conclusion and external elements to context *)
  1350         val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
  1351         (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
  1352         val all_propp' = map2 (curry (op ~~))
  1353           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
  1354         val (concl, propp) = chop (length raw_concl) all_propp';
  1355       in (propp, (ctxt, concl)) end
  1356 
  1357     val (proppss, (ctxt, concl)) =
  1358       (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
  1359 
  1360     (* CB: obtain all parameters from identifier part of raw_elemss *)
  1361     val xs = map #1 (params_of' raw_elemss);
  1362     val typing = unify_frozen ctxt 0
  1363       (map (Variable.default_type raw_ctxt) xs)
  1364       (map (Variable.default_type ctxt) xs);
  1365     val parms = param_types (xs ~~ typing);
  1366     (* CB: parms are the parameters from raw_elemss, with correct typing. *)
  1367 
  1368     (* CB: extract information from assumes and defines elements
  1369        (fixes, constrains and notes in raw_elemss don't have an effect on
  1370        text and elemss), compute final form of context elements. *)
  1371     val ((text, _), elemss) = finish_elemss ctxt parms do_close
  1372       ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
  1373     (* CB: text has the following structure:
  1374            (((exts, exts'), (ints, ints')), (xs, env, defs))
  1375        where
  1376          exts: external assumptions (terms in external assumes elements)
  1377          exts': dito, normalised wrt. env
  1378          ints: internal assumptions (terms in internal assumes elements)
  1379          ints': dito, normalised wrt. env
  1380          xs: the free variables in exts' and ints' and rhss of definitions,
  1381            this includes parameters except defined parameters
  1382          env: list of term pairs encoding substitutions, where the first term
  1383            is a free variable; substitutions represent defines elements and
  1384            the rhs is normalised wrt. the previous env
  1385          defs: theorems representing the substitutions from defines elements
  1386            (thms are normalised wrt. env).
  1387        elemss is an updated version of raw_elemss:
  1388          - type info added to Fixes and modified in Constrains
  1389          - axiom and definition statement replaced by corresponding one
  1390            from proppss in Assumes and Defines
  1391          - Facts unchanged
  1392        *)
  1393   in ((parms, elemss, concl), text) end;
  1394 
  1395 in
  1396 
  1397 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
  1398 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
  1399 
  1400 end;
  1401 
  1402 
  1403 (* facts and attributes *)
  1404 
  1405 local
  1406 
  1407 fun check_name name =
  1408   if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
  1409   else name;
  1410 
  1411 fun prep_facts _ _ _ ctxt (Int elem) = elem
  1412       |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
  1413   | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  1414      {var = I, typ = I, term = I,
  1415       name = Name.map_name prep_name,
  1416       fact = get ctxt,
  1417       attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  1418 
  1419 in
  1420 
  1421 fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
  1422 fun cert_facts x = prep_facts I (K I) (K I) x;
  1423 
  1424 end;
  1425 
  1426 
  1427 (* Get the specification of a locale *)
  1428 
  1429 (*The global specification is made from the parameters and global
  1430   assumptions, the local specification from the parameters and the
  1431   local assumptions.*)
  1432 
  1433 local
  1434 
  1435 fun gen_asms_of get thy name =
  1436   let
  1437     val ctxt = ProofContext.init thy;
  1438     val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
  1439     val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
  1440   in
  1441     elemss |> get
  1442       |> maps (fn (_, es) => map (fn Int e => e) es)
  1443       |> maps (fn Assumes asms => asms | _ => [])
  1444       |> map (apsnd (map fst))
  1445   end;
  1446 
  1447 in
  1448 
  1449 fun parameters_of thy = #params o the_locale thy;
  1450 
  1451 fun intros thy = #intros o the_locale thy;
  1452   (*returns introduction rule for delta predicate and locale predicate
  1453     as a pair of singleton lists*)
  1454 
  1455 fun dests thy = #dests o the_locale thy;
  1456 
  1457 fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts
  1458   | _ => NONE) o #elems o the_locale thy;
  1459 
  1460 fun parameters_of_expr thy expr =
  1461   let
  1462     val ctxt = ProofContext.init thy;
  1463     val pts = params_of_expr ctxt [] (intern_expr thy expr)
  1464         ([], Symtab.empty, Symtab.empty);
  1465     val raw_params_elemss = make_raw_params_elemss pts;
  1466     val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  1467         (([], Symtab.empty), Expr expr);
  1468     val ((parms, _, _), _) =
  1469         read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
  1470   in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
  1471 
  1472 fun local_asms_of thy name =
  1473   gen_asms_of (single o Library.last_elem) thy name;
  1474 
  1475 fun global_asms_of thy name =
  1476   gen_asms_of I thy name;
  1477 
  1478 end;
  1479 
  1480 
  1481 (* full context statements: imports + elements + conclusion *)
  1482 
  1483 local
  1484 
  1485 fun prep_context_statement prep_expr prep_elemss prep_facts
  1486     do_close fixed_params imports elements raw_concl context =
  1487   let
  1488     val thy = ProofContext.theory_of context;
  1489 
  1490     val (import_params, import_tenv, import_syn) =
  1491       params_of_expr context fixed_params (prep_expr thy imports)
  1492         ([], Symtab.empty, Symtab.empty);
  1493     val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
  1494     val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
  1495       (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
  1496 
  1497     val ((import_ids, _), raw_import_elemss) =
  1498       flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
  1499     (* CB: normalise "includes" among elements *)
  1500     val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
  1501       ((import_ids, incl_syn), elements);
  1502 
  1503     val raw_elemss = flat raw_elemsss;
  1504     (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  1505        context elements obtained from import and elements. *)
  1506     (* Now additional elements for parameters are inserted. *)
  1507     val import_params_ids = make_params_ids import_params;
  1508     val incl_params_ids =
  1509         make_params_ids (incl_params \\ import_params);
  1510     val raw_import_params_elemss =
  1511         make_raw_params_elemss (import_params, incl_tenv, incl_syn);
  1512     val raw_incl_params_elemss =
  1513         make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
  1514     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  1515       context fixed_params
  1516       (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
  1517 
  1518     (* replace extended ids (for axioms) by ids *)
  1519     val (import_ids', incl_ids) = chop (length import_ids) ids;
  1520     val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
  1521     val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
  1522         (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
  1523       (all_ids ~~ all_elemss);
  1524     (* CB: all_elemss and parms contain the correct parameter types *)
  1525 
  1526     val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  1527     val ((import_elemss, _), import_ctxt) =
  1528       activate_facts false prep_facts ps context;
  1529 
  1530     val ((elemss, _), ctxt) =
  1531       activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
  1532   in
  1533     ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  1534       (parms, spec, defs)), concl)
  1535   end;
  1536 
  1537 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  1538   let
  1539     val thy = ProofContext.theory_of ctxt;
  1540     val locale = Option.map (prep_locale thy) raw_locale;
  1541     val (fixed_params, imports) =
  1542       (case locale of
  1543         NONE => ([], empty)
  1544       | SOME name =>
  1545           let val {params = ps, ...} = the_locale thy name
  1546           in (map fst ps, Locale name) end);
  1547     val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
  1548       prep_ctxt false fixed_params imports (map Elem elems) concl ctxt;
  1549   in (locale, locale_ctxt, elems_ctxt, concl') end;
  1550 
  1551 fun prep_expr prep imports body ctxt =
  1552   let
  1553     val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
  1554     val all_elems = maps snd (import_elemss @ elemss);
  1555   in (all_elems, ctxt') end;
  1556 
  1557 in
  1558 
  1559 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
  1560 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
  1561 
  1562 fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
  1563 fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
  1564 
  1565 val read_expr = prep_expr read_context;
  1566 val cert_expr = prep_expr cert_context;
  1567 
  1568 fun read_context_statement loc = prep_statement (K I) read_ctxt loc;
  1569 fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc;
  1570 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
  1571 
  1572 end;
  1573 
  1574 
  1575 (* init *)
  1576 
  1577 fun init loc =
  1578   ProofContext.init
  1579   #> #2 o cert_context_statement (SOME loc) [] [];
  1580 
  1581 
  1582 (* print locale *)
  1583 
  1584 fun print_locale thy show_facts imports body =
  1585   let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
  1586     Pretty.big_list "locale elements:" (all_elems
  1587       |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
  1588       |> map (Element.pretty_ctxt ctxt) |> filter_out null
  1589       |> map Pretty.chunks)
  1590     |> Pretty.writeln
  1591   end;
  1592 
  1593 
  1594 
  1595 (** store results **)
  1596 
  1597 (* join equations of an id with already accumulated ones *)
  1598 
  1599 fun join_eqns get_reg id eqns =
  1600   let
  1601     val eqns' = case get_reg id
  1602       of NONE => eqns
  1603         | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns')
  1604             (* prefer equations from eqns' *)
  1605   in ((id, eqns'), eqns') end;
  1606 
  1607 
  1608 (* collect witnesses and equations up to a particular target for a
  1609    registration; requires parameters and flattened list of identifiers
  1610    instead of recomputing it from the target *)
  1611 
  1612 fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let
  1613 
  1614     val thy = ProofContext.theory_of ctxt;
  1615 
  1616     val ts = map (var_inst_term (impT, imp)) ext_ts;
  1617     val (parms, parmTs) = split_list parms;
  1618     val parmvTs = map Logic.varifyT parmTs;
  1619     val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
  1620     val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
  1621         |> Symtab.make;
  1622     val inst = Symtab.make (parms ~~ ts);
  1623 
  1624     (* instantiate parameter names in ids *)
  1625     val ext_inst = Symtab.make (parms ~~ ext_ts);
  1626     fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps;
  1627     val inst_ids = map (apfst (apsnd ext_inst_names)) ids;
  1628     val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
  1629     val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids;
  1630     val eqns =
  1631       fold_map (join_eqns (get_local_registration ctxt imprt))
  1632         (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd;
  1633   in ((tinst, inst), wits, eqns) end;
  1634 
  1635 
  1636 (* compute and apply morphism *)
  1637 
  1638 fun name_morph phi_name (lprfx, pprfx) b =
  1639   b
  1640   |> (if not (Binding.is_nothing b) andalso pprfx <> ""
  1641         then Binding.add_prefix false pprfx else I)
  1642   |> (if not (Binding.is_nothing b)
  1643         then Binding.add_prefix false lprfx else I)
  1644   |> phi_name;
  1645 
  1646 fun inst_morph thy phi_name param_prfx insts prems eqns export =
  1647   let
  1648     (* standardise export morphism *)
  1649     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
  1650     val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
  1651       (* FIXME sync with exp_fact *)
  1652     val exp_typ = Logic.type_map exp_term;
  1653     val export' =
  1654       Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  1655   in
  1656     Morphism.name_morphism (name_morph phi_name param_prfx) $>
  1657       Element.inst_morphism thy insts $>
  1658       Element.satisfy_morphism prems $>
  1659       Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
  1660       Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
  1661       export'
  1662   end;
  1663 
  1664 fun activate_note thy phi_name param_prfx attrib insts prems eqns exp =
  1665   (Element.facts_map o Element.morph_ctxt)
  1666       (inst_morph thy phi_name param_prfx insts prems eqns exp)
  1667   #> Attrib.map_facts attrib;
  1668 
  1669 
  1670 (* public interface to interpretation morphism *)
  1671 
  1672 fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts =
  1673   let
  1674     val parms = the_locale thy target |> #params |> map fst;
  1675     val ids = flatten (ProofContext.init thy, intern_expr thy)
  1676       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  1677     val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  1678   in
  1679     inst_morph thy phi_name param_prfx insts prems eqns exp
  1680   end;
  1681 
  1682 (* store instantiations of args for all registered interpretations
  1683    of the theory *)
  1684 
  1685 fun note_thmss_registrations target (kind, args) thy =
  1686   let
  1687     val parms = the_locale thy target |> #params |> map fst;
  1688     val ids = flatten (ProofContext.init thy, intern_expr thy)
  1689       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  1690 
  1691     val regs = get_global_registrations thy target;
  1692     (* add args to thy for all registrations *)
  1693 
  1694     fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  1695       let
  1696         val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  1697         val args' = args
  1698           |> activate_note thy phi_name param_prfx
  1699                (Attrib.attribute_i thy) insts prems eqns exp;
  1700       in
  1701         thy
  1702         |> global_note_qualified kind args'
  1703         |> snd
  1704       end;
  1705   in fold activate regs thy end;
  1706 
  1707 
  1708 (* locale results *)
  1709 
  1710 fun add_thmss loc kind args ctxt =
  1711   let
  1712     val (([(_, [Notes args'])], _), ctxt') =
  1713       activate_facts true cert_facts
  1714         [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
  1715     val ctxt'' = ctxt' |> ProofContext.theory
  1716       (change_locale loc
  1717         (fn (axiom, elems, params, decls, regs, intros, dests) =>
  1718           (axiom, elems @ [(Notes args', stamp ())],
  1719             params, decls, regs, intros, dests))
  1720       #> note_thmss_registrations loc args');
  1721   in ctxt'' end;
  1722 
  1723 
  1724 (* declarations *)
  1725 
  1726 local
  1727 
  1728 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
  1729 
  1730 fun add_decls add loc decl =
  1731   ProofContext.theory (change_locale loc
  1732     (fn (axiom, elems, params, decls, regs, intros, dests) =>
  1733       (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
  1734   add_thmss loc Thm.internalK
  1735     [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  1736 
  1737 in
  1738 
  1739 val add_type_syntax = add_decls (apfst o cons);
  1740 val add_term_syntax = add_decls (apsnd o cons);
  1741 val add_declaration = add_decls (K I);
  1742 
  1743 fun declarations_of thy loc =
  1744   the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst);
  1745 
  1746 end;
  1747 
  1748 
  1749 
  1750 (** define locales **)
  1751 
  1752 (* predicate text *)
  1753 (* CB: generate locale predicates and delta predicates *)
  1754 
  1755 local
  1756 
  1757 (* introN: name of theorems for introduction rules of locale and
  1758      delta predicates;
  1759    axiomsN: name of theorem set with destruct rules for locale predicates,
  1760      also name suffix of delta predicates. *)
  1761 
  1762 val introN = "intro";
  1763 val axiomsN = "axioms";
  1764 
  1765 fun atomize_spec thy ts =
  1766   let
  1767     val t = Logic.mk_conjunction_balanced ts;
  1768     val body = ObjectLogic.atomize_term thy t;
  1769     val bodyT = Term.fastype_of body;
  1770   in
  1771     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
  1772     else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
  1773   end;
  1774 
  1775 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
  1776   if length args = n then
  1777     Syntax.const "_aprop" $
  1778       Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
  1779   else raise Match);
  1780 
  1781 (* CB: define one predicate including its intro rule and axioms
  1782    - bname: predicate name
  1783    - parms: locale parameters
  1784    - defs: thms representing substitutions from defines elements
  1785    - ts: terms representing locale assumptions (not normalised wrt. defs)
  1786    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
  1787    - thy: the theory
  1788 *)
  1789 
  1790 fun def_pred bname parms defs ts norm_ts thy =
  1791   let
  1792     val name = Sign.full_name thy bname;
  1793 
  1794     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  1795     val env = Term.add_term_free_names (body, []);
  1796     val xs = filter (member (op =) env o #1) parms;
  1797     val Ts = map #2 xs;
  1798     val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
  1799       |> Library.sort_wrt #1 |> map TFree;
  1800     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
  1801 
  1802     val args = map Logic.mk_type extraTs @ map Free xs;
  1803     val head = Term.list_comb (Const (name, predT), args);
  1804     val statement = ObjectLogic.ensure_propT thy head;
  1805 
  1806     val ([pred_def], defs_thy) =
  1807       thy
  1808       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
  1809       |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
  1810       |> PureThy.add_defs false
  1811         [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
  1812     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  1813 
  1814     val cert = Thm.cterm_of defs_thy;
  1815 
  1816     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
  1817       MetaSimplifier.rewrite_goals_tac [pred_def] THEN
  1818       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
  1819       Tactic.compose_tac (false,
  1820         Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
  1821 
  1822     val conjuncts =
  1823       (Drule.equal_elim_rule2 OF [body_eq,
  1824         MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
  1825       |> Conjunction.elim_balanced (length ts);
  1826     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
  1827       Element.prove_witness defs_ctxt t
  1828        (MetaSimplifier.rewrite_goals_tac defs THEN
  1829         Tactic.compose_tac (false, ax, 0) 1));
  1830   in ((statement, intro, axioms), defs_thy) end;
  1831 
  1832 fun assumes_to_notes (Assumes asms) axms =
  1833       fold_map (fn (a, spec) => fn axs =>
  1834           let val (ps, qs) = chop (length spec) axs
  1835           in ((a, [(ps, [])]), qs) end) asms axms
  1836       |> apfst (curry Notes Thm.assumptionK)
  1837   | assumes_to_notes e axms = (e, axms);
  1838 
  1839 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
  1840 
  1841 (* turn Assumes into Notes elements *)
  1842 
  1843 fun change_assumes_elemss axioms elemss =
  1844   let
  1845     val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1846     fun change (id as ("", _), es) =
  1847           fold_map assumes_to_notes (map satisfy es)
  1848           #-> (fn es' => pair (id, es'))
  1849       | change e = pair e;
  1850   in
  1851     fst (fold_map change elemss (map Element.conclude_witness axioms))
  1852   end;
  1853 
  1854 (* adjust hyps of Notes elements *)
  1855 
  1856 fun change_elemss_hyps axioms elemss =
  1857   let
  1858     val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1859     fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
  1860       | change e = e;
  1861   in map change elemss end;
  1862 
  1863 in
  1864 
  1865 (* CB: main predicate definition function *)
  1866 
  1867 fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  1868   let
  1869     val ((elemss', more_ts), a_elem, a_intro, thy'') =
  1870       if null exts then ((elemss, []), [], [], thy)
  1871       else
  1872         let
  1873           val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
  1874           val ((statement, intro, axioms), thy') =
  1875             thy
  1876             |> def_pred aname parms defs exts exts';
  1877           val elemss' = change_assumes_elemss axioms elemss;
  1878           val a_elem = [(("", []),
  1879             [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  1880           val (_, thy'') =
  1881             thy'
  1882             |> Sign.add_path aname
  1883             |> Sign.no_base_names
  1884             |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
  1885             ||> Sign.restore_naming thy';
  1886         in ((elemss', [statement]), a_elem, [intro], thy'') end;
  1887     val (predicate, stmt', elemss'', b_intro, thy'''') =
  1888       if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
  1889       else
  1890         let
  1891           val ((statement, intro, axioms), thy''') =
  1892             thy''
  1893             |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts);
  1894           val cstatement = Thm.cterm_of thy''' statement;
  1895           val elemss'' = change_elemss_hyps axioms elemss';
  1896           val b_elem = [(("", []),
  1897                [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  1898           val (_, thy'''') =
  1899             thy'''
  1900             |> Sign.add_path pname
  1901             |> Sign.no_base_names
  1902             |> PureThy.note_thmss Thm.internalK
  1903                  [((Name.binding introN, []), [([intro], [])]),
  1904                   ((Name.binding axiomsN, []),
  1905                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  1906             ||> Sign.restore_naming thy''';
  1907         in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
  1908   in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
  1909 
  1910 end;
  1911 
  1912 
  1913 (* add_locale(_i) *)
  1914 
  1915 local
  1916 
  1917 (* turn Defines into Notes elements, accumulate definition terms *)
  1918 
  1919 fun defines_to_notes is_ext thy (Defines defs) defns =
  1920     let
  1921       val defs' = map (fn (_, (def, _)) => (Attrib.no_binding, (def, []))) defs
  1922       val notes = map (fn (a, (def, _)) =>
  1923         (a, [([assume (cterm_of thy def)], [])])) defs
  1924     in
  1925       (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
  1926     end
  1927   | defines_to_notes _ _ e defns = (SOME e, defns);
  1928 
  1929 fun change_defines_elemss thy elemss defns =
  1930   let
  1931     fun change (id as (n, _), es) defns =
  1932         let
  1933           val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
  1934         in ((id, map_filter I es'), defns') end
  1935   in fold_map change elemss defns end;
  1936 
  1937 fun gen_add_locale prep_ctxt prep_expr
  1938     predicate_name bname raw_imports raw_body thy =
  1939     (* predicate_name: "" - locale with predicate named as locale
  1940         "name" - locale with predicate named "name" *)
  1941   let
  1942     val thy_ctxt = ProofContext.init thy;
  1943     val name = Sign.full_name thy bname;
  1944     val _ = is_some (get_locale thy name) andalso
  1945       error ("Duplicate definition of locale " ^ quote name);
  1946 
  1947     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  1948       text as (parms, ((_, exts'), _), defs)) =
  1949         prep_ctxt raw_imports raw_body thy_ctxt;
  1950     val elemss = import_elemss @ body_elemss |>
  1951       map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  1952 
  1953     val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
  1954       List.foldr Term.add_typ_tfrees [] (map snd parms);
  1955     val _ = if null extraTs then ()
  1956       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  1957 
  1958     val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
  1959     val (elemss', defns) = change_defines_elemss thy elemss [];
  1960     val elemss'' = elemss' @ [(("", []), defns)];
  1961     val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
  1962       define_preds predicate_name' text elemss'' thy;
  1963     val regs = pred_axioms
  1964       |> fold_map (fn (id, elems) => fn wts => let
  1965              val ts = flat (map_filter (fn (Assumes asms) =>
  1966                SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1967              val (wts1, wts2) = chop (length ts) wts;
  1968            in ((apsnd (map fst) id, wts1), wts2) end) elemss'''
  1969       |> fst
  1970       |> map_filter (fn (("", _), _) => NONE | e => SOME e);
  1971     fun axiomify axioms elemss =
  1972       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  1973                    val ts = flat (map_filter (fn (Assumes asms) =>
  1974                      SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1975                    val (axs1, axs2) = chop (length ts) axs;
  1976                  in (axs2, ((id, Assumed axs1), elems)) end)
  1977       |> snd;
  1978     val ((_, facts), ctxt) = activate_facts true (K I)
  1979       (axiomify pred_axioms elemss''') (ProofContext.init thy');
  1980     val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
  1981     val export = Thm.close_derivation o Goal.norm_result o
  1982       singleton (ProofContext.export view_ctxt thy_ctxt);
  1983     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  1984     val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss''');
  1985     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  1986     val axs' = map (Element.assume_witness thy') stmt';
  1987     val loc_ctxt = thy'
  1988       |> Sign.add_path bname
  1989       |> Sign.no_base_names
  1990       |> PureThy.note_thmss Thm.assumptionK facts' |> snd
  1991       |> Sign.restore_naming thy'
  1992       |> register_locale name {axiom = axs',
  1993         elems = map (fn e => (e, stamp ())) elems'',
  1994         params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  1995         decls = ([], []),
  1996         regs = regs,
  1997         intros = intros,
  1998         dests = map Element.conclude_witness pred_axioms}
  1999       |> init name;
  2000   in (name, loc_ctxt) end;
  2001 
  2002 in
  2003 
  2004 val add_locale = gen_add_locale cert_context (K I);
  2005 val add_locale_cmd = gen_add_locale read_context intern_expr "";
  2006 
  2007 end;
  2008 
  2009 val _ = Context.>> (Context.map_theory
  2010  (add_locale "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
  2011   snd #> ProofContext.theory_of #>
  2012   add_locale "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
  2013   snd #> ProofContext.theory_of));
  2014 
  2015 
  2016 
  2017 
  2018 (** Normalisation of locale statements ---
  2019     discharges goals implied by interpretations **)
  2020 
  2021 local
  2022 
  2023 fun locale_assm_intros thy =
  2024   Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
  2025     (#2 (LocalesData.get thy)) [];
  2026 fun locale_base_intros thy =
  2027   Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
  2028     (#2 (LocalesData.get thy)) [];
  2029 
  2030 fun all_witnesses ctxt =
  2031   let
  2032     val thy = ProofContext.theory_of ctxt;
  2033     fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
  2034         (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) =>
  2035           map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms)
  2036       registrations [];
  2037   in get (RegistrationsData.get (Context.Proof ctxt)) end;
  2038 
  2039 in
  2040 
  2041 fun intro_locales_tac eager ctxt facts st =
  2042   let
  2043     val wits = all_witnesses ctxt;
  2044     val thy = ProofContext.theory_of ctxt;
  2045     val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
  2046   in
  2047     Method.intros_tac (wits @ intros) facts st
  2048   end;
  2049 
  2050 end;
  2051 
  2052 
  2053 (** Interpretation commands **)
  2054 
  2055 local
  2056 
  2057 (* extract proof obligations (assms and defs) from elements *)
  2058 
  2059 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
  2060   | extract_asms_elems ((id, Derived _), _) = (id, []);
  2061 
  2062 
  2063 (* activate instantiated facts in theory or context *)
  2064 
  2065 fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn
  2066         phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
  2067   let
  2068     val ctxt = mk_ctxt thy_ctxt;
  2069     fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
  2070     fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt);
  2071 
  2072     val (all_propss, eq_props) = chop (length all_elemss) propss;
  2073     val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
  2074 
  2075     (* Filter out fragments already registered. *)
  2076 
  2077     val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
  2078           test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss))));
  2079     val (new_pss, ys) = split_list xs;
  2080     val (new_propss, new_thmss) = split_list ys;
  2081 
  2082     val thy_ctxt' = thy_ctxt
  2083       (* add registrations *)
  2084       |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp))
  2085            new_elemss new_pss
  2086       (* add witnesses of Assumed elements (only those generate proof obligations) *)
  2087       |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss
  2088       (* add equations *)
  2089       |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props
  2090           ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
  2091             Element.conclude_witness) eq_thms);
  2092 
  2093     val prems = flat (map_filter
  2094           (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
  2095             | ((_, Derived _), _) => NONE) all_elemss);
  2096 
  2097     val thy_ctxt'' = thy_ctxt'
  2098       (* add witnesses of Derived elements *)
  2099       |> fold (fn (id, thms) => fold
  2100            (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
  2101          (map_filter (fn ((_, Assumed _), _) => NONE
  2102             | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
  2103 
  2104     fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
  2105         let
  2106           val ctxt = mk_ctxt thy_ctxt;
  2107           val thy = ProofContext.theory_of ctxt;
  2108           val facts' = facts
  2109             |> activate_note thy phi_name param_prfx
  2110                  (attrib thy_ctxt) insts prems eqns exp;
  2111         in 
  2112           thy_ctxt
  2113           |> note kind facts'
  2114           |> snd
  2115         end
  2116       | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
  2117 
  2118     fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt =
  2119       let
  2120         val ctxt = mk_ctxt thy_ctxt;
  2121         val thy = ProofContext.theory_of ctxt;
  2122         val {params, elems, ...} = the_locale thy loc;
  2123         val parms = map fst params;
  2124         val param_prfx = param_prefix loc ps;
  2125         val ids = flatten (ProofContext.init thy, intern_expr thy)
  2126           (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
  2127         val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
  2128       in
  2129         thy_ctxt
  2130         |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems
  2131       end;
  2132 
  2133   in
  2134     thy_ctxt''
  2135     (* add equations as lemmas to context *)
  2136     |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
  2137          ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
  2138             (unflat eq_thms eq_attns) eq_thms
  2139     (* add interpreted facts *)
  2140     |> fold2 activate_elems new_elemss new_pss
  2141   end;
  2142 
  2143 fun global_activate_facts_elemss x = gen_activate_facts_elemss
  2144   ProofContext.init
  2145   global_note_qualified
  2146   Attrib.attribute_i
  2147   put_global_registration
  2148   add_global_witness
  2149   add_global_equation
  2150   x;
  2151 
  2152 fun local_activate_facts_elemss x = gen_activate_facts_elemss
  2153   I
  2154   local_note_qualified
  2155   (Attrib.attribute_i o ProofContext.theory_of)
  2156   put_local_registration
  2157   add_local_witness
  2158   add_local_equation
  2159   x;
  2160 
  2161 fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
  2162   let
  2163     (* parameters *)
  2164     val (parm_names, parm_types) = parms |> split_list
  2165       ||> map (TypeInfer.paramify_vars o Logic.varifyT);
  2166     val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar);
  2167     val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
  2168 
  2169     (* parameter instantiations *)
  2170     val d = length parms - length insts;
  2171     val insts =
  2172       if d < 0 then error "More arguments than parameters in instantiation."
  2173       else insts @ replicate d NONE;
  2174     val (given_ps, given_insts) =
  2175       ((parm_names ~~ parm_types) ~~ insts) |> map_filter
  2176           (fn (_, NONE) => NONE
  2177             | ((n, T), SOME inst) => SOME ((n, T), inst))
  2178         |> split_list;
  2179     val (given_parm_names, given_parm_types) = given_ps |> split_list;
  2180 
  2181     (* parse insts / eqns *)
  2182     val given_insts' = map (parse_term ctxt) given_insts;
  2183     val eqns' = map (parse_prop ctxt) eqns;
  2184 
  2185     (* type inference and contexts *)
  2186     val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns';
  2187     val res = Syntax.check_terms ctxt arg;
  2188     val ctxt' = ctxt |> fold Variable.auto_fixes res;
  2189 
  2190     (* instantiation *)
  2191     val (type_parms'', res') = chop (length type_parms) res;
  2192     val (given_insts'', eqns'') = chop (length given_insts) res';
  2193     val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
  2194     val inst = Symtab.make (given_parm_names ~~ given_insts'');
  2195 
  2196     (* export from eigencontext *)
  2197     val export = Variable.export_morphism ctxt' ctxt;
  2198 
  2199     (* import, its inverse *)
  2200     val domT = fold Term.add_tfrees res [] |> map TFree;
  2201     val importT = domT |> map (fn x => (Morphism.typ export x, x))
  2202       |> map_filter (fn (TFree _, _) => NONE  (* fixed point of export *)
  2203                | (TVar y, x) => SOME (fst y, x)
  2204                | _ => error "internal: illegal export in interpretation")
  2205       |> Vartab.make;
  2206     val dom = fold Term.add_frees res [] |> map Free;
  2207     val imprt = dom |> map (fn x => (Morphism.term export x, x))
  2208       |> map_filter (fn (Free _, _) => NONE  (* fixed point of export *)
  2209                | (Var y, x) => SOME (fst y, x)
  2210                | _ => error "internal: illegal export in interpretation")
  2211       |> Vartab.make;
  2212   in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end;
  2213 
  2214 val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
  2215 val check_instantiations = prep_instantiations (K I) (K I);
  2216 
  2217 fun gen_prep_registration mk_ctxt test_reg activate
  2218     prep_attr prep_expr prep_insts
  2219     thy_ctxt phi_name raw_expr raw_insts =
  2220   let
  2221     val ctxt = mk_ctxt thy_ctxt;
  2222     val thy = ProofContext.theory_of ctxt;
  2223     val ctxt' = ProofContext.init thy;
  2224     fun prep_attn attn = (apsnd o map)
  2225       (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
  2226 
  2227     val expr = prep_expr thy raw_expr;
  2228 
  2229     val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
  2230     val params_ids = make_params_ids (#1 pts);
  2231     val raw_params_elemss = make_raw_params_elemss pts;
  2232     val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr);
  2233     val ((parms, all_elemss, _), (_, (_, defs, _))) =
  2234       read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
  2235 
  2236     (** compute instantiation **)
  2237 
  2238     (* consistency check: equations need to be stored in a particular locale,
  2239        therefore if equations are present locale expression must be a name *)
  2240 
  2241     val _ = case (expr, snd raw_insts) of
  2242         (Locale _, _) => () | (_, []) => ()
  2243       | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
  2244 
  2245     (* read or certify instantiation *)
  2246     val (raw_insts', raw_eqns) = raw_insts;
  2247     val (raw_eq_attns, raw_eqns') = split_list raw_eqns;
  2248     val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns');
  2249     val eq_attns = map prep_attn raw_eq_attns;
  2250 
  2251     (* defined params without given instantiation *)
  2252     val not_given = filter_out (Symtab.defined inst1 o fst) parms;
  2253     fun add_def (p, pT) inst =
  2254       let
  2255         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  2256                NONE => error ("Instance missing for parameter " ^ quote p)
  2257              | SOME (Free (_, T), t) => (t, T);
  2258         val d = Element.inst_term (instT, inst) t;
  2259       in Symtab.update_new (p, d) inst end;
  2260     val inst2 = fold add_def not_given inst1;
  2261     val inst_morphism = Element.inst_morphism thy (instT, inst2);
  2262     (* Note: insts contain no vars. *)
  2263 
  2264     (** compute proof obligations **)
  2265 
  2266     (* restore "small" ids *)
  2267     val ids' = map (fn ((n, ps), (_, mode)) =>
  2268           ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
  2269         ids;
  2270     val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
  2271     (* instantiate ids and elements *)
  2272     val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  2273       ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
  2274         map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
  2275       |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
  2276 
  2277     (* equations *)
  2278     val eqn_elems = if null eqns then []
  2279       else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
  2280 
  2281     val propss = map extract_asms_elems inst_elemss @ eqn_elems;
  2282 
  2283   in
  2284     (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
  2285   end;
  2286 
  2287 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
  2288   test_global_registration
  2289   global_activate_facts_elemss mk_ctxt;
  2290 
  2291 fun gen_prep_local_registration mk_ctxt = gen_prep_registration I
  2292   test_local_registration
  2293   local_activate_facts_elemss mk_ctxt;
  2294 
  2295 val prep_global_registration = gen_prep_global_registration
  2296   (K I) (K I) check_instantiations;
  2297 val prep_global_registration_cmd = gen_prep_global_registration
  2298   Attrib.intern_src intern_expr read_instantiations;
  2299 
  2300 val prep_local_registration = gen_prep_local_registration
  2301   (K I) (K I) check_instantiations;
  2302 val prep_local_registration_cmd = gen_prep_local_registration
  2303   Attrib.intern_src intern_expr read_instantiations;
  2304 
  2305 fun prep_registration_in_locale target expr thy =
  2306   (* target already in internal form *)
  2307   let
  2308     val ctxt = ProofContext.init thy;
  2309     val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
  2310         (([], Symtab.empty), Expr (Locale target));
  2311     val fixed = the_locale thy target |> #params |> map #1;
  2312     val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  2313         ((raw_target_ids, target_syn), Expr expr);
  2314     val (target_ids, ids) = chop (length raw_target_ids) all_ids;
  2315     val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
  2316 
  2317     (** compute proof obligations **)
  2318 
  2319     (* restore "small" ids, with mode *)
  2320     val ids' = map (apsnd snd) ids;
  2321     (* remove Int markers *)
  2322     val elemss' = map (fn (_, es) =>
  2323         map (fn Int e => e) es) elemss
  2324     (* extract assumptions and defs *)
  2325     val ids_elemss = ids' ~~ elemss';
  2326     val propss = map extract_asms_elems ids_elemss;
  2327 
  2328     (** activation function:
  2329         - add registrations to the target locale
  2330         - add induced registrations for all global registrations of
  2331           the target, unless already present
  2332         - add facts of induced registrations to theory **)
  2333 
  2334     fun activate thmss thy =
  2335       let
  2336         val satisfy = Element.satisfy_thm (flat thmss);
  2337         val ids_elemss_thmss = ids_elemss ~~ thmss;
  2338         val regs = get_global_registrations thy target;
  2339 
  2340         fun activate_id (((id, Assumed _), _), thms) thy =
  2341             thy |> put_registration_in_locale target id
  2342                 |> fold (add_witness_in_locale target id) thms
  2343           | activate_id _ thy = thy;
  2344 
  2345         fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  2346           let
  2347             val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
  2348             val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts));
  2349             val disch = Element.satisfy_thm wits;
  2350             val new_elemss = filter (fn (((name, ps), _), _) =>
  2351                 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
  2352             fun activate_assumed_id (((_, Derived _), _), _) thy = thy
  2353               | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
  2354                 val ps' = inst_parms ps;
  2355               in
  2356                 if test_global_registration thy (name, ps')
  2357                 then thy
  2358                 else thy
  2359                   |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  2360                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2361                      (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
  2362               end;
  2363 
  2364             fun activate_derived_id ((_, Assumed _), _) thy = thy
  2365               | activate_derived_id (((name, ps), Derived ths), _) thy = let
  2366                 val ps' = inst_parms ps;
  2367               in
  2368                 if test_global_registration thy (name, ps')
  2369                 then thy
  2370                 else thy
  2371                   |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  2372                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2373                        (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
  2374                        (Element.inst_term insts t,
  2375                         disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
  2376               end;
  2377 
  2378             fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
  2379                 let
  2380                   val att_morphism =
  2381                     Morphism.name_morphism (name_morph phi_name param_prfx) $>
  2382                     Morphism.thm_morphism satisfy $>
  2383                     Element.inst_morphism thy insts $>
  2384                     Morphism.thm_morphism disch;
  2385                   val facts' = facts
  2386                     |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
  2387                     |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
  2388                     |> (map o apfst o apfst) (name_morph phi_name param_prfx);
  2389                 in
  2390                   thy
  2391                   |> global_note_qualified kind facts'
  2392                   |> snd
  2393                 end
  2394               | activate_elem _ _ thy = thy;
  2395 
  2396             fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
  2397 
  2398           in thy |> fold activate_assumed_id ids_elemss_thmss
  2399                  |> fold activate_derived_id ids_elemss
  2400                  |> fold activate_elems new_elemss end;
  2401       in
  2402         thy |> fold activate_id ids_elemss_thmss
  2403             |> fold activate_reg regs
  2404       end;
  2405 
  2406   in (propss, activate) end;
  2407 
  2408 fun prep_propp propss = propss |> map (fn (_, props) =>
  2409   map (rpair [] o Element.mark_witness) props);
  2410 
  2411 fun prep_result propps thmss =
  2412   ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
  2413 
  2414 fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
  2415   let
  2416     val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
  2417     fun after_qed' results =
  2418       ProofContext.theory (activate (prep_result propss results))
  2419       #> after_qed;
  2420   in
  2421     thy
  2422     |> ProofContext.init
  2423     |> Proof.theorem_i NONE after_qed' (prep_propp propss)
  2424     |> Element.refine_witness
  2425     |> Seq.hd
  2426     |> pair morphs
  2427   end;
  2428 
  2429 fun gen_interpret prep_registration after_qed name_morph expr insts int state =
  2430   let
  2431     val _ = Proof.assert_forward_or_chain state;
  2432     val ctxt = Proof.context_of state;
  2433     val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts;
  2434     fun after_qed' results =
  2435       Proof.map_context (K (ctxt |> activate (prep_result propss results)))
  2436       #> Proof.put_facts NONE
  2437       #> after_qed;
  2438   in
  2439     state
  2440     |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  2441       "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
  2442     |> Element.refine_witness |> Seq.hd
  2443     |> pair morphs
  2444   end;
  2445 
  2446 fun standard_name_morph interp_prfx b =
  2447   if Binding.is_nothing b then b
  2448   else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
  2449     fold (Binding.add_prefix false o fst) pprfx
  2450     #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
  2451     #> Binding.add_prefix false lprfx
  2452   ) b;
  2453 
  2454 in
  2455 
  2456 val interpretation = gen_interpretation prep_global_registration;
  2457 fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd
  2458   I (standard_name_morph interp_prfx);
  2459 
  2460 fun interpretation_in_locale after_qed (raw_target, expr) thy =
  2461   let
  2462     val target = intern thy raw_target;
  2463     val (propss, activate) = prep_registration_in_locale target expr thy;
  2464     val raw_propp = prep_propp propss;
  2465 
  2466     val (_, _, goal_ctxt, propp) = thy
  2467       |> ProofContext.init
  2468       |> cert_context_statement (SOME target) [] raw_propp;
  2469 
  2470     fun after_qed' results =
  2471       ProofContext.theory (activate (prep_result propss results))
  2472       #> after_qed;
  2473   in
  2474     goal_ctxt
  2475     |> Proof.theorem_i NONE after_qed' propp
  2476     |> Element.refine_witness |> Seq.hd
  2477   end;
  2478 
  2479 val interpret = gen_interpret prep_local_registration;
  2480 fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
  2481   Seq.single (standard_name_morph interp_prfx);
  2482 
  2483 end;
  2484 
  2485 end;