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