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