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