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