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