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