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