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