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