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