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