src/Pure/Isar/old_locale.ML
changeset 29600 0182b65e4ad0
parent 29599 c369feeb6bbc
parent 29586 4f9803829625
child 29602 f1583c12b5d0
     1.1 --- a/src/Pure/Isar/old_locale.ML	Wed Jan 21 15:26:02 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,2485 +0,0 @@
     1.4 -(*  Title:      Pure/Isar/locale.ML
     1.5 -    Author:     Clemens Ballarin, TU Muenchen
     1.6 -    Author:     Markus Wenzel, LMU/TU Muenchen
     1.7 -
     1.8 -Locales -- Isar proof contexts as meta-level predicates, with local
     1.9 -syntax and implicit structures.
    1.10 -
    1.11 -Draws basic ideas from Florian Kammueller's original version of
    1.12 -locales, but uses the richer infrastructure of Isar instead of the raw
    1.13 -meta-logic.  Furthermore, structured import of contexts (with merge
    1.14 -and rename operations) are provided, as well as type-inference of the
    1.15 -signature parts, and predicate definitions of the specification text.
    1.16 -
    1.17 -Interpretation enables the reuse of theorems of locales in other
    1.18 -contexts, namely those defined by theories, structured proofs and
    1.19 -locales themselves.
    1.20 -
    1.21 -See also:
    1.22 -
    1.23 -[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    1.24 -    In Stefano Berardi et al., Types for Proofs and Programs: International
    1.25 -    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    1.26 -[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    1.27 -    Dependencies between Locales. Technical Report TUM-I0607, Technische
    1.28 -    Universitaet Muenchen, 2006.
    1.29 -[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    1.30 -    Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    1.31 -    pages 31-43, 2006.
    1.32 -*)
    1.33 -
    1.34 -(* TODO:
    1.35 -- beta-eta normalisation of interpretation parameters
    1.36 -- dangling type frees in locales
    1.37 -- test subsumption of interpretations when merging theories
    1.38 -*)
    1.39 -
    1.40 -signature OLD_LOCALE =
    1.41 -sig
    1.42 -  datatype expr =
    1.43 -    Locale of string |
    1.44 -    Rename of expr * (string * mixfix option) option list |
    1.45 -    Merge of expr list
    1.46 -  val empty: expr
    1.47 -
    1.48 -  val intern: theory -> xstring -> string
    1.49 -  val intern_expr: theory -> expr -> expr
    1.50 -  val extern: theory -> string -> xstring
    1.51 -  val init: string -> theory -> Proof.context
    1.52 -
    1.53 -  (* The specification of a locale *)
    1.54 -  val parameters_of: theory -> string -> ((string * typ) * mixfix) list
    1.55 -  val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
    1.56 -  val local_asms_of: theory -> string -> (Attrib.binding * term list) list
    1.57 -  val global_asms_of: theory -> string -> (Attrib.binding * term list) list
    1.58 -
    1.59 -  (* Theorems *)
    1.60 -  val intros: theory -> string -> thm list * thm list
    1.61 -  val dests: theory -> string -> thm list
    1.62 -  (* Not part of the official interface.  DO NOT USE *)
    1.63 -  val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
    1.64 -
    1.65 -  (* Not part of the official interface.  DO NOT USE *)
    1.66 -  val declarations_of: theory -> string -> declaration list * declaration list;
    1.67 -
    1.68 -  (* Processing of locale statements *)
    1.69 -  val read_context_statement: string option -> Element.context list ->
    1.70 -    (string * string list) list list -> Proof.context ->
    1.71 -    string option * Proof.context * Proof.context * (term * term list) list list
    1.72 -  val read_context_statement_cmd: xstring option -> Element.context list ->
    1.73 -    (string * string list) list list -> Proof.context ->
    1.74 -    string option * Proof.context * Proof.context * (term * term list) list list
    1.75 -  val cert_context_statement: string option -> Element.context_i list ->
    1.76 -    (term * term list) list list -> Proof.context ->
    1.77 -    string option * Proof.context * Proof.context * (term * term list) list list
    1.78 -  val read_expr: expr -> Element.context list -> Proof.context ->
    1.79 -    Element.context_i list * Proof.context
    1.80 -  val cert_expr: expr -> Element.context_i list -> Proof.context ->
    1.81 -    Element.context_i list * Proof.context
    1.82 -
    1.83 -  (* Diagnostic functions *)
    1.84 -  val print_locales: theory -> unit
    1.85 -  val print_locale: theory -> bool -> expr -> Element.context list -> unit
    1.86 -  val print_registrations: bool -> string -> Proof.context -> unit
    1.87 -
    1.88 -  val add_locale: string -> bstring -> expr -> Element.context_i list -> theory
    1.89 -    -> string * Proof.context
    1.90 -  val add_locale_cmd: bstring -> expr -> Element.context list -> theory
    1.91 -    -> string * Proof.context
    1.92 -
    1.93 -  (* Tactics *)
    1.94 -  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    1.95 -
    1.96 -  (* Storing results *)
    1.97 -  val global_note_qualified: string ->
    1.98 -    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
    1.99 -    theory -> (string * thm list) list * theory
   1.100 -  val local_note_qualified: string ->
   1.101 -    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
   1.102 -    Proof.context -> (string * thm list) list * Proof.context
   1.103 -  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   1.104 -    Proof.context -> Proof.context
   1.105 -  val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   1.106 -  val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   1.107 -  val add_declaration: string -> declaration -> Proof.context -> Proof.context
   1.108 -
   1.109 -  (* Interpretation *)
   1.110 -  val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string ->
   1.111 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   1.112 -    string -> term list -> Morphism.morphism
   1.113 -  val interpretation: (Proof.context -> Proof.context) ->
   1.114 -    (Binding.T -> Binding.T) -> expr ->
   1.115 -    term option list * (Attrib.binding * term) list ->
   1.116 -    theory ->
   1.117 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   1.118 -  val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   1.119 -    theory -> Proof.state
   1.120 -  val interpretation_in_locale: (Proof.context -> Proof.context) ->
   1.121 -    xstring * expr -> theory -> Proof.state
   1.122 -  val interpret: (Proof.state -> Proof.state) ->
   1.123 -    (Binding.T -> Binding.T) -> expr ->
   1.124 -    term option list * (Attrib.binding * term) list ->
   1.125 -    bool -> Proof.state ->
   1.126 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   1.127 -  val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   1.128 -    bool -> Proof.state -> Proof.state
   1.129 -end;
   1.130 -
   1.131 -structure Old_Locale: OLD_LOCALE =
   1.132 -struct
   1.133 -
   1.134 -(* legacy operations *)
   1.135 -
   1.136 -fun merge_lists _ xs [] = xs
   1.137 -  | merge_lists _ [] ys = ys
   1.138 -  | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   1.139 -
   1.140 -fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
   1.141 -
   1.142 -
   1.143 -(* auxiliary: noting name bindings with qualified base names *)
   1.144 -
   1.145 -fun global_note_qualified kind facts thy =
   1.146 -  thy
   1.147 -  |> Sign.qualified_names
   1.148 -  |> PureThy.note_thmss kind facts
   1.149 -  ||> Sign.restore_naming thy;
   1.150 -
   1.151 -fun local_note_qualified kind facts ctxt =
   1.152 -  ctxt
   1.153 -  |> ProofContext.qualified_names
   1.154 -  |> ProofContext.note_thmss_i kind facts
   1.155 -  ||> ProofContext.restore_naming ctxt;
   1.156 -
   1.157 -
   1.158 -(** locale elements and expressions **)
   1.159 -
   1.160 -datatype ctxt = datatype Element.ctxt;
   1.161 -
   1.162 -datatype expr =
   1.163 -  Locale of string |
   1.164 -  Rename of expr * (string * mixfix option) option list |
   1.165 -  Merge of expr list;
   1.166 -
   1.167 -val empty = Merge [];
   1.168 -
   1.169 -datatype 'a element =
   1.170 -  Elem of 'a | Expr of expr;
   1.171 -
   1.172 -fun map_elem f (Elem e) = Elem (f e)
   1.173 -  | map_elem _ (Expr e) = Expr e;
   1.174 -
   1.175 -type decl = declaration * stamp;
   1.176 -
   1.177 -type locale =
   1.178 - {axiom: Element.witness list,
   1.179 -    (* For locales that define predicates this is [A [A]], where A is the locale
   1.180 -       specification.  Otherwise [].
   1.181 -       Only required to generate the right witnesses for locales with predicates. *)
   1.182 -  elems: (Element.context_i * stamp) list,
   1.183 -    (* Static content, neither Fixes nor Constrains elements *)
   1.184 -  params: ((string * typ) * mixfix) list,                        (*all term params*)
   1.185 -  decls: decl list * decl list,                    (*type/term_syntax declarations*)
   1.186 -  regs: ((string * string list) * Element.witness list) list,
   1.187 -    (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
   1.188 -  intros: thm list * thm list,
   1.189 -    (* Introduction rules: of delta predicate and locale predicate. *)
   1.190 -  dests: thm list}
   1.191 -    (* Destruction rules: projections from locale predicate to predicates of fragments. *)
   1.192 -
   1.193 -(* CB: an internal (Int) locale element was either imported or included,
   1.194 -   an external (Ext) element appears directly in the locale text. *)
   1.195 -
   1.196 -datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   1.197 -
   1.198 -
   1.199 -
   1.200 -(** substitutions on Vars -- clone from element.ML **)
   1.201 -
   1.202 -(* instantiate types *)
   1.203 -
   1.204 -fun var_instT_type env =
   1.205 -  if Vartab.is_empty env then I
   1.206 -  else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x));
   1.207 -
   1.208 -fun var_instT_term env =
   1.209 -  if Vartab.is_empty env then I
   1.210 -  else Term.map_types (var_instT_type env);
   1.211 -
   1.212 -fun var_inst_term (envT, env) =
   1.213 -  if Vartab.is_empty env then var_instT_term envT
   1.214 -  else
   1.215 -    let
   1.216 -      val instT = var_instT_type envT;
   1.217 -      fun inst (Const (x, T)) = Const (x, instT T)
   1.218 -        | inst (Free (x, T)) = Free(x, instT T)
   1.219 -        | inst (Var (xi, T)) =
   1.220 -            (case Vartab.lookup env xi of
   1.221 -              NONE => Var (xi, instT T)
   1.222 -            | SOME t => t)
   1.223 -        | inst (b as Bound _) = b
   1.224 -        | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
   1.225 -        | inst (t $ u) = inst t $ inst u;
   1.226 -    in Envir.beta_norm o inst end;
   1.227 -
   1.228 -
   1.229 -(** management of registrations in theories and proof contexts **)
   1.230 -
   1.231 -type registration =
   1.232 -  {prfx: (Binding.T -> Binding.T) * (string * string),
   1.233 -      (* first component: interpretation name morphism;
   1.234 -         second component: parameter prefix *)
   1.235 -    exp: Morphism.morphism,
   1.236 -      (* maps content to its originating context *)
   1.237 -    imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
   1.238 -      (* inverse of exp *)
   1.239 -    wits: Element.witness list,
   1.240 -      (* witnesses of the registration *)
   1.241 -    eqns: thm Termtab.table,
   1.242 -      (* theorems (equations) interpreting derived concepts and indexed by lhs *)
   1.243 -    morph: unit
   1.244 -      (* interpreting morphism *)
   1.245 -  }
   1.246 -
   1.247 -structure Registrations :
   1.248 -  sig
   1.249 -    type T
   1.250 -    val empty: T
   1.251 -    val join: T * T -> T
   1.252 -    val dest: theory -> T ->
   1.253 -      (term list *
   1.254 -        (((Binding.T -> Binding.T) * (string * string)) *
   1.255 -         (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
   1.256 -         Element.witness list *
   1.257 -         thm Termtab.table)) list
   1.258 -    val test: theory -> T * term list -> bool
   1.259 -    val lookup: theory ->
   1.260 -      T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   1.261 -      (((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option
   1.262 -    val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) ->
   1.263 -      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   1.264 -      T ->
   1.265 -      T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list
   1.266 -    val add_witness: term list -> Element.witness -> T -> T
   1.267 -    val add_equation: term list -> thm -> T -> T
   1.268 -(*
   1.269 -    val update_morph: term list -> Morphism.morphism -> T -> T
   1.270 -    val get_morph: theory -> T ->
   1.271 -      term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
   1.272 -      Morphism.morphism
   1.273 -*)
   1.274 -  end =
   1.275 -struct
   1.276 -  (* A registration is indexed by parameter instantiation.
   1.277 -     NB: index is exported whereas content is internalised. *)
   1.278 -  type T = registration Termtab.table;
   1.279 -
   1.280 -  fun mk_reg prfx exp imp wits eqns morph =
   1.281 -    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph};
   1.282 -
   1.283 -  fun map_reg f reg =
   1.284 -    let
   1.285 -      val {prfx, exp, imp, wits, eqns, morph} = reg;
   1.286 -      val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph);
   1.287 -    in mk_reg prfx' exp' imp' wits' eqns' morph' end;
   1.288 -
   1.289 -  val empty = Termtab.empty;
   1.290 -
   1.291 -  (* term list represented as single term, for simultaneous matching *)
   1.292 -  fun termify ts =
   1.293 -    Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
   1.294 -  fun untermify t =
   1.295 -    let fun ut (Const _) ts = ts
   1.296 -          | ut (s $ t) ts = ut s (t::ts)
   1.297 -    in ut t [] end;
   1.298 -
   1.299 -  (* joining of registrations:
   1.300 -     - prefix and morphisms of right theory;
   1.301 -     - witnesses are equal, no attempt to subsumption testing;
   1.302 -     - union of equalities, if conflicting (i.e. two eqns with equal lhs)
   1.303 -       eqn of right theory takes precedence *)
   1.304 -  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) =>
   1.305 -      mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2);
   1.306 -
   1.307 -  fun dest_transfer thy regs =
   1.308 -    Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) =>
   1.309 -      (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m))));
   1.310 -
   1.311 -  fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
   1.312 -    map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns)));
   1.313 -
   1.314 -  (* registrations that subsume t *)
   1.315 -  fun subsumers thy t regs =
   1.316 -    filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
   1.317 -
   1.318 -  (* test if registration that subsumes the query is present *)
   1.319 -  fun test thy (regs, ts) =
   1.320 -    not (null (subsumers thy (termify ts) regs));
   1.321 -      
   1.322 -  (* look up registration, pick one that subsumes the query *)
   1.323 -  fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) =
   1.324 -    let
   1.325 -      val t = termify ts;
   1.326 -      val subs = subsumers thy t regs;
   1.327 -    in
   1.328 -      (case subs of
   1.329 -        [] => NONE
   1.330 -        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) =>
   1.331 -          let
   1.332 -            val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   1.333 -            val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
   1.334 -                (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst
   1.335 -                      |> var_instT_type impT)) |> Symtab.make;
   1.336 -            val inst' = dom' |> map (fn (t as Free (x, _)) =>
   1.337 -                (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
   1.338 -                      |> var_inst_term (impT, imp))) |> Symtab.make;
   1.339 -            val inst'_morph = Element.inst_morphism thy (tinst', inst');
   1.340 -          in SOME (prfx,
   1.341 -            map (Element.morph_witness inst'_morph) wits,
   1.342 -            Termtab.map (Morphism.thm inst'_morph) eqns)
   1.343 -          end)
   1.344 -    end;
   1.345 -
   1.346 -  (* add registration if not subsumed by ones already present,
   1.347 -     additionally returns registrations that are strictly subsumed *)
   1.348 -  fun insert thy ts prfx (exp, imp) regs =
   1.349 -    let
   1.350 -      val t = termify ts;
   1.351 -      val subs = subsumers thy t regs ;
   1.352 -    in (case subs of
   1.353 -        [] => let
   1.354 -                val sups =
   1.355 -                  filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   1.356 -                val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
   1.357 -              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end
   1.358 -      | _ => (regs, []))
   1.359 -    end;
   1.360 -
   1.361 -  fun gen_add f ts regs =
   1.362 -    let
   1.363 -      val t = termify ts;
   1.364 -    in
   1.365 -      Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs
   1.366 -    end;
   1.367 -
   1.368 -  (* add witness theorem to registration,
   1.369 -     only if instantiation is exact, otherwise exception Option raised *)
   1.370 -  fun add_witness ts wit regs =
   1.371 -    gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m))
   1.372 -      ts regs;
   1.373 -
   1.374 -  (* add equation to registration, replaces previous equation with same lhs;
   1.375 -     only if instantiation is exact, otherwise exception Option raised;
   1.376 -     exception TERM raised if not a meta equality *)
   1.377 -  fun add_equation ts thm regs =
   1.378 -    gen_add (fn (x, e, i, thms, eqns, m) =>
   1.379 -      (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
   1.380 -      ts regs;
   1.381 -
   1.382 -end;
   1.383 -
   1.384 -
   1.385 -(** theory data : locales **)
   1.386 -
   1.387 -structure LocalesData = TheoryDataFun
   1.388 -(
   1.389 -  type T = NameSpace.T * locale Symtab.table;
   1.390 -    (* 1st entry: locale namespace,
   1.391 -       2nd entry: locales of the theory *)
   1.392 -
   1.393 -  val empty = NameSpace.empty_table;
   1.394 -  val copy = I;
   1.395 -  val extend = I;
   1.396 -
   1.397 -  fun join_locales _
   1.398 -    ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,
   1.399 -      {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
   1.400 -     {axiom = axiom,
   1.401 -      elems = merge_lists (eq_snd (op =)) elems elems',
   1.402 -      params = params,
   1.403 -      decls =
   1.404 -       (Library.merge (eq_snd (op =)) (decls1, decls1'),
   1.405 -        Library.merge (eq_snd (op =)) (decls2, decls2')),
   1.406 -      regs = merge_alists (op =) regs regs',
   1.407 -      intros = intros,
   1.408 -      dests = dests};
   1.409 -  fun merge _ = NameSpace.join_tables join_locales;
   1.410 -);
   1.411 -
   1.412 -
   1.413 -
   1.414 -(** context data : registrations **)
   1.415 -
   1.416 -structure RegistrationsData = GenericDataFun
   1.417 -(
   1.418 -  type T = Registrations.T Symtab.table;  (*registrations, indexed by locale name*)
   1.419 -  val empty = Symtab.empty;
   1.420 -  val extend = I;
   1.421 -  fun merge _ = Symtab.join (K Registrations.join);
   1.422 -);
   1.423 -
   1.424 -
   1.425 -(** access locales **)
   1.426 -
   1.427 -val intern = NameSpace.intern o #1 o LocalesData.get;
   1.428 -val extern = NameSpace.extern o #1 o LocalesData.get;
   1.429 -
   1.430 -fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   1.431 -
   1.432 -fun the_locale thy name = case get_locale thy name
   1.433 - of SOME loc => loc
   1.434 -  | NONE => error ("Unknown locale " ^ quote name);
   1.435 -
   1.436 -fun register_locale bname loc thy =
   1.437 -  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy)
   1.438 -    (Binding.name bname, loc) #> snd);
   1.439 -
   1.440 -fun change_locale name f thy =
   1.441 -  let
   1.442 -    val {axiom, elems, params, decls, regs, intros, dests} =
   1.443 -        the_locale thy name;
   1.444 -    val (axiom', elems', params', decls', regs', intros', dests') =
   1.445 -      f (axiom, elems, params, decls, regs, intros, dests);
   1.446 -  in
   1.447 -    thy
   1.448 -    |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
   1.449 -          elems = elems', params = params',
   1.450 -          decls = decls', regs = regs', intros = intros', dests = dests'}))
   1.451 -  end;
   1.452 -
   1.453 -fun print_locales thy =
   1.454 -  let val (space, locs) = LocalesData.get thy in
   1.455 -    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   1.456 -    |> Pretty.writeln
   1.457 -  end;
   1.458 -
   1.459 -
   1.460 -(* access registrations *)
   1.461 -
   1.462 -(* retrieve registration from theory or context *)
   1.463 -
   1.464 -fun get_registrations ctxt name =
   1.465 -  case Symtab.lookup (RegistrationsData.get ctxt) name of
   1.466 -      NONE => []
   1.467 -    | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;
   1.468 -
   1.469 -fun get_global_registrations thy = get_registrations (Context.Theory thy);
   1.470 -fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
   1.471 -
   1.472 -
   1.473 -fun get_registration ctxt imprt (name, ps) =
   1.474 -  case Symtab.lookup (RegistrationsData.get ctxt) name of
   1.475 -      NONE => NONE
   1.476 -    | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));
   1.477 -
   1.478 -fun get_global_registration thy = get_registration (Context.Theory thy);
   1.479 -fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
   1.480 -
   1.481 -
   1.482 -fun test_registration ctxt (name, ps) =
   1.483 -  case Symtab.lookup (RegistrationsData.get ctxt) name of
   1.484 -      NONE => false
   1.485 -    | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps);
   1.486 -
   1.487 -fun test_global_registration thy = test_registration (Context.Theory thy);
   1.488 -fun test_local_registration ctxt = test_registration (Context.Proof ctxt);
   1.489 -
   1.490 -
   1.491 -(* add registration to theory or context, ignored if subsumed *)
   1.492 -
   1.493 -fun put_registration (name, ps) prfx morphs ctxt =
   1.494 -  RegistrationsData.map (fn regs =>
   1.495 -    let
   1.496 -      val thy = Context.theory_of ctxt;
   1.497 -      val reg = the_default Registrations.empty (Symtab.lookup regs name);
   1.498 -      val (reg', sups) = Registrations.insert thy ps prfx morphs reg;
   1.499 -      val _ = if not (null sups) then warning
   1.500 -                ("Subsumed interpretation(s) of locale " ^
   1.501 -                 quote (extern thy name) ^
   1.502 -                 "\nwith the following prefix(es):" ^
   1.503 -                  commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups))
   1.504 -              else ();
   1.505 -    in Symtab.update (name, reg') regs end) ctxt;
   1.506 -
   1.507 -fun put_global_registration id prfx morphs =
   1.508 -  Context.theory_map (put_registration id prfx morphs);
   1.509 -fun put_local_registration id prfx morphs =
   1.510 -  Context.proof_map (put_registration id prfx morphs);
   1.511 -
   1.512 -fun put_registration_in_locale name id =
   1.513 -  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   1.514 -    (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
   1.515 -
   1.516 -
   1.517 -(* add witness theorem to registration, ignored if registration not present *)
   1.518 -
   1.519 -fun add_witness (name, ps) thm =
   1.520 -  RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));
   1.521 -
   1.522 -fun add_global_witness id thm = Context.theory_map (add_witness id thm);
   1.523 -fun add_local_witness id thm = Context.proof_map (add_witness id thm);
   1.524 -
   1.525 -
   1.526 -fun add_witness_in_locale name id thm =
   1.527 -  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   1.528 -    let
   1.529 -      fun add (id', thms) =
   1.530 -        if id = id' then (id', thm :: thms) else (id', thms);
   1.531 -    in (axiom, elems, params, decls, map add regs, intros, dests) end);
   1.532 -
   1.533 -
   1.534 -(* add equation to registration, ignored if registration not present *)
   1.535 -
   1.536 -fun add_equation (name, ps) thm =
   1.537 -  RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));
   1.538 -
   1.539 -fun add_global_equation id thm = Context.theory_map (add_equation id thm);
   1.540 -fun add_local_equation id thm = Context.proof_map (add_equation id thm);
   1.541 -
   1.542 -(*
   1.543 -(* update morphism of registration, ignored if registration not present *)
   1.544 -
   1.545 -fun update_morph (name, ps) morph =
   1.546 -  RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph));
   1.547 -
   1.548 -fun update_global_morph id morph = Context.theory_map (update_morph id morph);
   1.549 -fun update_local_morph id morph = Context.proof_map (update_morph id morph);
   1.550 -*)
   1.551 -
   1.552 -
   1.553 -(* printing of registrations *)
   1.554 -
   1.555 -fun print_registrations show_wits loc ctxt =
   1.556 -  let
   1.557 -    val thy = ProofContext.theory_of ctxt;
   1.558 -    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   1.559 -    fun prt_term' t = if !show_types
   1.560 -          then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   1.561 -            Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   1.562 -          else prt_term t;
   1.563 -    val prt_thm = prt_term o prop_of;
   1.564 -    fun prt_inst ts =
   1.565 -        Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
   1.566 -    fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx]
   1.567 -      | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx];
   1.568 -    fun prt_eqns [] = Pretty.str "no equations."
   1.569 -      | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   1.570 -          Pretty.breaks (map prt_thm eqns));
   1.571 -    fun prt_core ts eqns =
   1.572 -          [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
   1.573 -    fun prt_witns [] = Pretty.str "no witnesses."
   1.574 -      | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   1.575 -          Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   1.576 -    fun prt_reg (ts, (_, _, witns, eqns)) =
   1.577 -        if show_wits
   1.578 -          then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   1.579 -          else Pretty.block (prt_core ts eqns)
   1.580 -
   1.581 -    val loc_int = intern thy loc;
   1.582 -    val regs = RegistrationsData.get (Context.Proof ctxt);
   1.583 -    val loc_regs = Symtab.lookup regs loc_int;
   1.584 -  in
   1.585 -    (case loc_regs of
   1.586 -        NONE => Pretty.str ("no interpretations")
   1.587 -      | SOME r => let
   1.588 -            val r' = Registrations.dest thy r;
   1.589 -            val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r';
   1.590 -          in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
   1.591 -    |> Pretty.writeln
   1.592 -  end;
   1.593 -
   1.594 -
   1.595 -(* diagnostics *)
   1.596 -
   1.597 -fun err_in_locale ctxt msg ids =
   1.598 -  let
   1.599 -    val thy = ProofContext.theory_of ctxt;
   1.600 -    fun prt_id (name, parms) =
   1.601 -      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   1.602 -    val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   1.603 -    val err_msg =
   1.604 -      if forall (fn (s, _) => s = "") ids then msg
   1.605 -      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   1.606 -        (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   1.607 -  in error err_msg end;
   1.608 -
   1.609 -fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   1.610 -
   1.611 -
   1.612 -fun pretty_ren NONE = Pretty.str "_"
   1.613 -  | pretty_ren (SOME (x, NONE)) = Pretty.str x
   1.614 -  | pretty_ren (SOME (x, SOME syn)) =
   1.615 -      Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
   1.616 -
   1.617 -fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
   1.618 -  | pretty_expr thy (Rename (expr, xs)) =
   1.619 -      Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
   1.620 -  | pretty_expr thy (Merge es) =
   1.621 -      Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
   1.622 -
   1.623 -fun err_in_expr _ msg (Merge []) = error msg
   1.624 -  | err_in_expr ctxt msg expr =
   1.625 -    error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
   1.626 -      [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
   1.627 -       pretty_expr (ProofContext.theory_of ctxt) expr]));
   1.628 -
   1.629 -
   1.630 -(** structured contexts: rename + merge + implicit type instantiation **)
   1.631 -
   1.632 -(* parameter types *)
   1.633 -
   1.634 -fun frozen_tvars ctxt Ts =
   1.635 -  #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   1.636 -  |> map (fn ((xi, S), T) => (xi, (S, T)));
   1.637 -
   1.638 -fun unify_frozen ctxt maxidx Ts Us =
   1.639 -  let
   1.640 -    fun paramify NONE i = (NONE, i)
   1.641 -      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   1.642 -
   1.643 -    val (Ts', maxidx') = fold_map paramify Ts maxidx;
   1.644 -    val (Us', maxidx'') = fold_map paramify Us maxidx';
   1.645 -    val thy = ProofContext.theory_of ctxt;
   1.646 -
   1.647 -    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   1.648 -          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   1.649 -      | unify _ env = env;
   1.650 -    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   1.651 -    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   1.652 -    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
   1.653 -  in map (Option.map (Envir.norm_type unifier')) Vs end;
   1.654 -
   1.655 -fun params_of elemss =
   1.656 -  distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
   1.657 -
   1.658 -fun params_of' elemss =
   1.659 -  distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   1.660 -
   1.661 -fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
   1.662 -
   1.663 -
   1.664 -(* CB: param_types has the following type:
   1.665 -  ('a * 'b option) list -> ('a * 'b) list *)
   1.666 -fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   1.667 -
   1.668 -
   1.669 -fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
   1.670 -  handle Symtab.DUP x => err_in_locale ctxt
   1.671 -    ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
   1.672 -
   1.673 -
   1.674 -(* Distinction of assumed vs. derived identifiers.
   1.675 -   The former may have axioms relating assumptions of the context to
   1.676 -   assumptions of the specification fragment (for locales with
   1.677 -   predicates).  The latter have witnesses relating assumptions of the
   1.678 -   specification fragment to assumptions of other (assumed) specification
   1.679 -   fragments. *)
   1.680 -
   1.681 -datatype 'a mode = Assumed of 'a | Derived of 'a;
   1.682 -
   1.683 -fun map_mode f (Assumed x) = Assumed (f x)
   1.684 -  | map_mode f (Derived x) = Derived (f x);
   1.685 -
   1.686 -
   1.687 -(* flatten expressions *)
   1.688 -
   1.689 -local
   1.690 -
   1.691 -fun unify_parms ctxt fixed_parms raw_parmss =
   1.692 -  let
   1.693 -    val thy = ProofContext.theory_of ctxt;
   1.694 -    val maxidx = length raw_parmss;
   1.695 -    val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   1.696 -
   1.697 -    fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   1.698 -    fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   1.699 -    val parms = fixed_parms @ maps varify_parms idx_parmss;
   1.700 -
   1.701 -    fun unify T U envir = Sign.typ_unify thy (U, T) envir
   1.702 -      handle Type.TUNIFY =>
   1.703 -        let
   1.704 -          val T' = Envir.norm_type (fst envir) T;
   1.705 -          val U' = Envir.norm_type (fst envir) U;
   1.706 -          val prt = Syntax.string_of_typ ctxt;
   1.707 -        in
   1.708 -          raise TYPE ("unify_parms: failed to unify types " ^
   1.709 -            prt U' ^ " and " ^ prt T', [U', T'], [])
   1.710 -        end;
   1.711 -    fun unify_list (T :: Us) = fold (unify T) Us
   1.712 -      | unify_list [] = I;
   1.713 -    val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
   1.714 -      (Vartab.empty, maxidx);
   1.715 -
   1.716 -    val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
   1.717 -    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
   1.718 -
   1.719 -    fun inst_parms (i, ps) =
   1.720 -      List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps)
   1.721 -      |> map_filter (fn (a, S) =>
   1.722 -          let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   1.723 -          in if T = TFree (a, S) then NONE else SOME (a, T) end)
   1.724 -      |> Symtab.make;
   1.725 -  in map inst_parms idx_parmss end;
   1.726 -
   1.727 -in
   1.728 -
   1.729 -fun unify_elemss _ _ [] = []
   1.730 -  | unify_elemss _ [] [elems] = [elems]
   1.731 -  | unify_elemss ctxt fixed_parms elemss =
   1.732 -      let
   1.733 -        val thy = ProofContext.theory_of ctxt;
   1.734 -        val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
   1.735 -          |> map (Element.instT_morphism thy);
   1.736 -        fun inst ((((name, ps), mode), elems), phi) =
   1.737 -          (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
   1.738 -              map_mode (map (Element.morph_witness phi)) mode),
   1.739 -            map (Element.morph_ctxt phi) elems);
   1.740 -      in map inst (elemss ~~ phis) end;
   1.741 -
   1.742 -
   1.743 -fun renaming xs parms = zip_options parms xs
   1.744 -  handle Library.UnequalLengths =>
   1.745 -    error ("Too many arguments in renaming: " ^
   1.746 -      commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
   1.747 -
   1.748 -
   1.749 -(* params_of_expr:
   1.750 -   Compute parameters (with types and syntax) of locale expression.
   1.751 -*)
   1.752 -
   1.753 -fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
   1.754 -  let
   1.755 -    val thy = ProofContext.theory_of ctxt;
   1.756 -
   1.757 -    fun merge_tenvs fixed tenv1 tenv2 =
   1.758 -        let
   1.759 -          val [env1, env2] = unify_parms ctxt fixed
   1.760 -                [tenv1 |> Symtab.dest |> map (apsnd SOME),
   1.761 -                 tenv2 |> Symtab.dest |> map (apsnd SOME)]
   1.762 -        in
   1.763 -          Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
   1.764 -            Symtab.map (Element.instT_type env2) tenv2)
   1.765 -        end;
   1.766 -
   1.767 -    fun merge_syn expr syn1 syn2 =
   1.768 -        Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
   1.769 -        handle Symtab.DUP x => err_in_expr ctxt
   1.770 -          ("Conflicting syntax for parameter: " ^ quote x) expr;
   1.771 -
   1.772 -    fun params_of (expr as Locale name) =
   1.773 -          let
   1.774 -            val {params, ...} = the_locale thy name;
   1.775 -          in (map (fst o fst) params, params |> map fst |> Symtab.make,
   1.776 -               params |> map (apfst fst) |> Symtab.make) end
   1.777 -      | params_of (expr as Rename (e, xs)) =
   1.778 -          let
   1.779 -            val (parms', types', syn') = params_of e;
   1.780 -            val ren = renaming xs parms';
   1.781 -            (* renaming may reduce number of parameters *)
   1.782 -            val new_parms = map (Element.rename ren) parms' |> distinct (op =);
   1.783 -            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
   1.784 -            val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
   1.785 -                handle Symtab.DUP x =>
   1.786 -                  err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
   1.787 -            val syn_types = map (apsnd (fn mx =>
   1.788 -                SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0)))))
   1.789 -              (Symtab.dest new_syn);
   1.790 -            val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
   1.791 -            val (env :: _) = unify_parms ctxt []
   1.792 -                ((ren_types |> map (apsnd SOME)) :: map single syn_types);
   1.793 -            val new_types = fold (Symtab.insert (op =))
   1.794 -                (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
   1.795 -          in (new_parms, new_types, new_syn) end
   1.796 -      | params_of (Merge es) =
   1.797 -          fold (fn e => fn (parms, types, syn) =>
   1.798 -                   let
   1.799 -                     val (parms', types', syn') = params_of e
   1.800 -                   in
   1.801 -                     (merge_lists (op =) parms parms', merge_tenvs [] types types',
   1.802 -                      merge_syn e syn syn')
   1.803 -                   end)
   1.804 -            es ([], Symtab.empty, Symtab.empty)
   1.805 -
   1.806 -      val (parms, types, syn) = params_of expr;
   1.807 -    in
   1.808 -      (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
   1.809 -       merge_syn expr prev_syn syn)
   1.810 -    end;
   1.811 -
   1.812 -fun make_params_ids params = [(("", params), ([], Assumed []))];
   1.813 -fun make_raw_params_elemss (params, tenv, syn) =
   1.814 -    [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   1.815 -      Int [Fixes (map (fn p =>
   1.816 -        (Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   1.817 -
   1.818 -
   1.819 -(* flatten_expr:
   1.820 -   Extend list of identifiers by those new in locale expression expr.
   1.821 -   Compute corresponding list of lists of locale elements (one entry per
   1.822 -   identifier).
   1.823 -
   1.824 -   Identifiers represent locale fragments and are in an extended form:
   1.825 -     ((name, ps), (ax_ps, axs))
   1.826 -   (name, ps) is the locale name with all its parameters.
   1.827 -   (ax_ps, axs) is the locale axioms with its parameters;
   1.828 -     axs are always taken from the top level of the locale hierarchy,
   1.829 -     hence axioms may contain additional parameters from later fragments:
   1.830 -     ps subset of ax_ps.  axs is either singleton or empty.
   1.831 -
   1.832 -   Elements are enriched by identifier-like information:
   1.833 -     (((name, ax_ps), axs), elems)
   1.834 -   The parameters in ax_ps are the axiom parameters, but enriched by type
   1.835 -   info: now each entry is a pair of string and typ option.  Axioms are
   1.836 -   type-instantiated.
   1.837 -
   1.838 -*)
   1.839 -
   1.840 -fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
   1.841 -  let
   1.842 -    val thy = ProofContext.theory_of ctxt;
   1.843 -
   1.844 -    fun rename_parms top ren ((name, ps), (parms, mode)) =
   1.845 -        ((name, map (Element.rename ren) ps),
   1.846 -         if top
   1.847 -         then (map (Element.rename ren) parms,
   1.848 -               map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
   1.849 -         else (parms, mode));
   1.850 -
   1.851 -    (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *)
   1.852 -
   1.853 -    fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
   1.854 -        if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
   1.855 -        then (wits, ids, visited)
   1.856 -        else
   1.857 -          let
   1.858 -            val {params, regs, ...} = the_locale thy name;
   1.859 -            val pTs' = map #1 params;
   1.860 -            val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
   1.861 -              (* dummy syntax, since required by rename *)
   1.862 -            val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
   1.863 -            val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
   1.864 -              (* propagate parameter types, to keep them consistent *)
   1.865 -            val regs' = map (fn ((name, ps), wits) =>
   1.866 -                ((name, map (Element.rename ren) ps),
   1.867 -                 map (Element.transfer_witness thy) wits)) regs;
   1.868 -            val new_regs = regs';
   1.869 -            val new_ids = map fst new_regs;
   1.870 -            val new_idTs =
   1.871 -              map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
   1.872 -
   1.873 -            val new_wits = new_regs |> map (#2 #> map
   1.874 -              (Element.morph_witness
   1.875 -                (Element.instT_morphism thy env $>
   1.876 -                  Element.rename_morphism ren $>
   1.877 -                  Element.satisfy_morphism wits)
   1.878 -                #> Element.close_witness));
   1.879 -            val new_ids' = map (fn (id, wits) =>
   1.880 -                (id, ([], Derived wits))) (new_ids ~~ new_wits);
   1.881 -            val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
   1.882 -                ((n, pTs), mode)) (new_idTs ~~ new_ids');
   1.883 -            val new_id = ((name, map #1 pTs), ([], mode));
   1.884 -            val (wits', ids', visited') = fold add_with_regs new_idTs'
   1.885 -              (wits @ flat new_wits, ids, visited @ [new_id]);
   1.886 -          in
   1.887 -            (wits', ids' @ [new_id], visited')
   1.888 -          end;
   1.889 -
   1.890 -    (* distribute top-level axioms over assumed ids *)
   1.891 -
   1.892 -    fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
   1.893 -        let
   1.894 -          val {elems, ...} = the_locale thy name;
   1.895 -          val ts = maps
   1.896 -            (fn (Assumes asms, _) => maps (map #1 o #2) asms
   1.897 -              | _ => [])
   1.898 -            elems;
   1.899 -          val (axs1, axs2) = chop (length ts) axioms;
   1.900 -        in (((name, parms), (all_ps, Assumed axs1)), axs2) end
   1.901 -      | axiomify all_ps (id, (_, Derived ths)) axioms =
   1.902 -          ((id, (all_ps, Derived ths)), axioms);
   1.903 -
   1.904 -    (* identifiers of an expression *)
   1.905 -
   1.906 -    fun identify top (Locale name) =
   1.907 -    (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
   1.908 -       where name is a locale name, ps a list of parameter names and axs
   1.909 -       a list of axioms relating to the identifier, axs is empty unless
   1.910 -       identify at top level (top = true);
   1.911 -       parms is accumulated list of parameters *)
   1.912 -          let
   1.913 -            val {axiom, params, ...} = the_locale thy name;
   1.914 -            val ps = map (#1 o #1) params;
   1.915 -            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);
   1.916 -            val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
   1.917 -            in (ids_ax, ps) end
   1.918 -      | identify top (Rename (e, xs)) =
   1.919 -          let
   1.920 -            val (ids', parms') = identify top e;
   1.921 -            val ren = renaming xs parms'
   1.922 -              handle ERROR msg => err_in_locale' ctxt msg ids';
   1.923 -
   1.924 -            val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   1.925 -            val parms'' = distinct (op =) (maps (#2 o #1) ids'');
   1.926 -          in (ids'', parms'') end
   1.927 -      | identify top (Merge es) =
   1.928 -          fold (fn e => fn (ids, parms) =>
   1.929 -                   let
   1.930 -                     val (ids', parms') = identify top e
   1.931 -                   in
   1.932 -                     (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
   1.933 -                   end)
   1.934 -            es ([], []);
   1.935 -
   1.936 -    fun inst_wit all_params (t, th) = let
   1.937 -         val {hyps, prop, ...} = Thm.rep_thm th;
   1.938 -         val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
   1.939 -         val [env] = unify_parms ctxt all_params [ps];
   1.940 -         val t' = Element.instT_term env t;
   1.941 -         val th' = Element.instT_thm thy env th;
   1.942 -       in (t', th') end;
   1.943 -
   1.944 -    fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
   1.945 -      let
   1.946 -        val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
   1.947 -        val elems = map fst elems_stamped;
   1.948 -        val ps = map fst ps_mx;
   1.949 -        fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
   1.950 -        val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
   1.951 -        val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
   1.952 -        val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
   1.953 -        val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   1.954 -        val (lprfx, pprfx) = param_prefix name params;
   1.955 -        val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
   1.956 -          #> Binding.add_prefix false lprfx;
   1.957 -        val elem_morphism =
   1.958 -          Element.rename_morphism ren $>
   1.959 -          Morphism.binding_morphism add_prefices $>
   1.960 -          Element.instT_morphism thy env;
   1.961 -        val elems' = map (Element.morph_ctxt elem_morphism) elems;
   1.962 -      in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   1.963 -
   1.964 -    (* parameters, their types and syntax *)
   1.965 -    val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
   1.966 -    val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
   1.967 -    (* compute identifiers and syntax, merge with previous ones *)
   1.968 -    val (ids, _) = identify true expr;
   1.969 -    val idents = subtract (eq_fst (op =)) prev_idents ids;
   1.970 -    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   1.971 -    (* type-instantiate elements *)
   1.972 -    val final_elemss = map (eval all_params tenv syntax) idents;
   1.973 -  in ((prev_idents @ idents, syntax), final_elemss) end;
   1.974 -
   1.975 -end;
   1.976 -
   1.977 -
   1.978 -(* activate elements *)
   1.979 -
   1.980 -local
   1.981 -
   1.982 -fun axioms_export axs _ As =
   1.983 -  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
   1.984 -
   1.985 -
   1.986 -(* NB: derived ids contain only facts at this stage *)
   1.987 -
   1.988 -fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
   1.989 -      ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
   1.990 -  | activate_elem _ _ (Constrains _) (ctxt, mode) =
   1.991 -      ([], (ctxt, mode))
   1.992 -  | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
   1.993 -      let
   1.994 -        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   1.995 -        val ts = maps (map #1 o #2) asms';
   1.996 -        val (ps, qs) = chop (length ts) axs;
   1.997 -        val (_, ctxt') =
   1.998 -          ctxt |> fold Variable.auto_fixes ts
   1.999 -          |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
  1.1000 -      in ([], (ctxt', Assumed qs)) end
  1.1001 -  | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
  1.1002 -      ([], (ctxt, Derived ths))
  1.1003 -  | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
  1.1004 -      let
  1.1005 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  1.1006 -        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  1.1007 -            let val ((c, _), t') = LocalDefs.cert_def ctxt t
  1.1008 -            in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  1.1009 -        val (_, ctxt') =
  1.1010 -          ctxt |> fold (Variable.auto_fixes o #1) asms
  1.1011 -          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  1.1012 -      in ([], (ctxt', Assumed axs)) end
  1.1013 -  | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
  1.1014 -      ([], (ctxt, Derived ths))
  1.1015 -  | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
  1.1016 -      let
  1.1017 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
  1.1018 -        val (res, ctxt') = ctxt |> local_note_qualified kind facts';
  1.1019 -      in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
  1.1020 -
  1.1021 -fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  1.1022 -  let
  1.1023 -    val thy = ProofContext.theory_of ctxt;
  1.1024 -    val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
  1.1025 -        elems (ProofContext.qualified_names ctxt, mode)
  1.1026 -      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
  1.1027 -    val ctxt'' = if name = "" then ctxt'
  1.1028 -          else let
  1.1029 -              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
  1.1030 -            in if test_local_registration ctxt' (name, ps') then ctxt'
  1.1031 -              else let
  1.1032 -                  val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, ""))
  1.1033 -                    (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
  1.1034 -                in case mode of
  1.1035 -                    Assumed axs =>
  1.1036 -                      fold (add_local_witness (name, ps') o
  1.1037 -                        Element.assume_witness thy o Element.witness_prop) axs ctxt''
  1.1038 -                  | Derived ths =>
  1.1039 -                     fold (add_local_witness (name, ps')) ths ctxt''
  1.1040 -                end
  1.1041 -            end
  1.1042 -  in (ProofContext.restore_naming ctxt ctxt'', res) end;
  1.1043 -
  1.1044 -fun activate_elemss ax_in_ctxt prep_facts =
  1.1045 -    fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
  1.1046 -      let
  1.1047 -        val elems = map (prep_facts ctxt) raw_elems;
  1.1048 -        val (ctxt', res) = apsnd flat
  1.1049 -            (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
  1.1050 -        val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
  1.1051 -      in (((((name, ps), mode), elems'), res), ctxt') end);
  1.1052 -
  1.1053 -in
  1.1054 -
  1.1055 -(* CB: activate_facts prep_facts elemss ctxt,
  1.1056 -   where elemss is a list of pairs consisting of identifiers and
  1.1057 -   context elements, extends ctxt by the context elements yielding
  1.1058 -   ctxt' and returns ((elemss', facts), ctxt').
  1.1059 -   Identifiers in the argument are of the form ((name, ps), axs) and
  1.1060 -   assumptions use the axioms in the identifiers to set up exporters
  1.1061 -   in ctxt'.  elemss' does not contain identifiers and is obtained
  1.1062 -   from elemss and the intermediate context with prep_facts.
  1.1063 -   If read_facts or cert_facts is used for prep_facts, these also remove
  1.1064 -   the internal/external markers from elemss. *)
  1.1065 -
  1.1066 -fun activate_facts ax_in_ctxt prep_facts args =
  1.1067 -  activate_elemss ax_in_ctxt prep_facts args
  1.1068 -  #>> (apsnd flat o split_list);
  1.1069 -
  1.1070 -end;
  1.1071 -
  1.1072 -
  1.1073 -
  1.1074 -(** prepare locale elements **)
  1.1075 -
  1.1076 -(* expressions *)
  1.1077 -
  1.1078 -fun intern_expr thy (Locale xname) = Locale (intern thy xname)
  1.1079 -  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
  1.1080 -  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
  1.1081 -
  1.1082 -
  1.1083 -(* propositions and bindings *)
  1.1084 -
  1.1085 -(* flatten (ctxt, prep_expr) ((ids, syn), expr)
  1.1086 -   normalises expr (which is either a locale
  1.1087 -   expression or a single context element) wrt.
  1.1088 -   to the list ids of already accumulated identifiers.
  1.1089 -   It returns ((ids', syn'), elemss) where ids' is an extension of ids
  1.1090 -   with identifiers generated for expr, and elemss is the list of
  1.1091 -   context elements generated from expr.
  1.1092 -   syn and syn' are symtabs mapping parameter names to their syntax.  syn'
  1.1093 -   is an extension of syn.
  1.1094 -   For details, see flatten_expr.
  1.1095 -
  1.1096 -   Additionally, for a locale expression, the elems are grouped into a single
  1.1097 -   Int; individual context elements are marked Ext.  In this case, the
  1.1098 -   identifier-like information of the element is as follows:
  1.1099 -   - for Fixes: (("", ps), []) where the ps have type info NONE
  1.1100 -   - for other elements: (("", []), []).
  1.1101 -   The implementation of activate_facts relies on identifier names being
  1.1102 -   empty strings for external elements.
  1.1103 -*)
  1.1104 -
  1.1105 -fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
  1.1106 -        val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
  1.1107 -      in
  1.1108 -        ((ids',
  1.1109 -         merge_syntax ctxt ids'
  1.1110 -           (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
  1.1111 -           handle Symtab.DUP x => err_in_locale ctxt
  1.1112 -             ("Conflicting syntax for parameter: " ^ quote x)
  1.1113 -             (map #1 ids')),
  1.1114 -         [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
  1.1115 -      end
  1.1116 -  | flatten _ ((ids, syn), Elem elem) =
  1.1117 -      ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  1.1118 -  | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
  1.1119 -      apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
  1.1120 -
  1.1121 -local
  1.1122 -
  1.1123 -local
  1.1124 -
  1.1125 -fun declare_int_elem (Fixes fixes) ctxt =
  1.1126 -      ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  1.1127 -        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
  1.1128 -  | declare_int_elem _ ctxt = ([], ctxt);
  1.1129 -
  1.1130 -fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
  1.1131 -      let val (vars, _) = prep_vars fixes ctxt
  1.1132 -      in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
  1.1133 -  | declare_ext_elem prep_vars (Constrains csts) ctxt =
  1.1134 -      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt
  1.1135 -      in ([], ctxt') end
  1.1136 -  | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
  1.1137 -  | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
  1.1138 -  | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
  1.1139 -
  1.1140 -fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
  1.1141 -     of Int es => fold_map declare_int_elem es ctxt
  1.1142 -      | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
  1.1143 -          handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
  1.1144 -  | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
  1.1145 -
  1.1146 -in
  1.1147 -
  1.1148 -fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
  1.1149 -  let
  1.1150 -    (* CB: fix of type bug of goal in target with context elements.
  1.1151 -       Parameters new in context elements must receive types that are
  1.1152 -       distinct from types of parameters in target (fixed_params).  *)
  1.1153 -    val ctxt_with_fixed = 
  1.1154 -      fold Variable.declare_term (map Free fixed_params) ctxt;
  1.1155 -    val int_elemss =
  1.1156 -      raw_elemss
  1.1157 -      |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  1.1158 -      |> unify_elemss ctxt_with_fixed fixed_params;
  1.1159 -    val (raw_elemss', _) =
  1.1160 -      fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
  1.1161 -        raw_elemss int_elemss;
  1.1162 -  in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
  1.1163 -
  1.1164 -end;
  1.1165 -
  1.1166 -local
  1.1167 -
  1.1168 -val norm_term = Envir.beta_norm oo Term.subst_atomic;
  1.1169 -
  1.1170 -fun abstract_thm thy eq =
  1.1171 -  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
  1.1172 -
  1.1173 -fun bind_def ctxt (name, ps) eq (xs, env, ths) =
  1.1174 -  let
  1.1175 -    val ((y, T), b) = LocalDefs.abs_def eq;
  1.1176 -    val b' = norm_term env b;
  1.1177 -    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
  1.1178 -    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  1.1179 -  in
  1.1180 -    exists (fn (x, _) => x = y) xs andalso
  1.1181 -      err "Attempt to define previously specified variable";
  1.1182 -    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
  1.1183 -      err "Attempt to redefine variable";
  1.1184 -    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  1.1185 -  end;
  1.1186 -
  1.1187 -
  1.1188 -(* CB: for finish_elems (Int and Ext),
  1.1189 -   extracts specification, only of assumed elements *)
  1.1190 -
  1.1191 -fun eval_text _ _ _ (Fixes _) text = text
  1.1192 -  | eval_text _ _ _ (Constrains _) text = text
  1.1193 -  | eval_text _ (_, Assumed _) is_ext (Assumes asms)
  1.1194 -        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  1.1195 -      let
  1.1196 -        val ts = maps (map #1 o #2) asms;
  1.1197 -        val ts' = map (norm_term env) ts;
  1.1198 -        val spec' =
  1.1199 -          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  1.1200 -          else ((exts, exts'), (ints @ ts, ints' @ ts'));
  1.1201 -      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  1.1202 -  | eval_text _ (_, Derived _) _ (Assumes _) text = text
  1.1203 -  | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
  1.1204 -      (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
  1.1205 -  | eval_text _ (_, Derived _) _ (Defines _) text = text
  1.1206 -  | eval_text _ _ _ (Notes _) text = text;
  1.1207 -
  1.1208 -
  1.1209 -(* for finish_elems (Int),
  1.1210 -   remove redundant elements of derived identifiers,
  1.1211 -   turn assumptions and definitions into facts,
  1.1212 -   satisfy hypotheses of facts *)
  1.1213 -
  1.1214 -fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  1.1215 -  | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  1.1216 -  | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  1.1217 -  | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
  1.1218 -
  1.1219 -  | finish_derived _ _ (Derived _) (Fixes _) = NONE
  1.1220 -  | finish_derived _ _ (Derived _) (Constrains _) = NONE
  1.1221 -  | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
  1.1222 -      |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
  1.1223 -      |> pair Thm.assumptionK |> Notes
  1.1224 -      |> Element.morph_ctxt satisfy |> SOME
  1.1225 -  | finish_derived sign satisfy (Derived _) (Defines defs) = defs
  1.1226 -      |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
  1.1227 -      |> pair Thm.definitionK |> Notes
  1.1228 -      |> Element.morph_ctxt satisfy |> SOME
  1.1229 -
  1.1230 -  | finish_derived _ satisfy _ (Notes facts) = Notes facts
  1.1231 -      |> Element.morph_ctxt satisfy |> SOME;
  1.1232 -
  1.1233 -(* CB: for finish_elems (Ext) *)
  1.1234 -
  1.1235 -fun closeup _ false elem = elem
  1.1236 -  | closeup ctxt true elem =
  1.1237 -      let
  1.1238 -        fun close_frees t =
  1.1239 -          let
  1.1240 -            val rev_frees =
  1.1241 -              Term.fold_aterms (fn Free (x, T) =>
  1.1242 -                if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
  1.1243 -          in Term.list_all_free (rev rev_frees, t) end;
  1.1244 -
  1.1245 -        fun no_binds [] = []
  1.1246 -          | no_binds _ = error "Illegal term bindings in locale element";
  1.1247 -      in
  1.1248 -        (case elem of
  1.1249 -          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
  1.1250 -            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
  1.1251 -        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
  1.1252 -            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
  1.1253 -        | e => e)
  1.1254 -      end;
  1.1255 -
  1.1256 -
  1.1257 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
  1.1258 -      let val x = Binding.base_name b
  1.1259 -      in (b, AList.lookup (op =) parms x, mx) end) fixes)
  1.1260 -  | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  1.1261 -  | finish_ext_elem _ close (Assumes asms, propp) =
  1.1262 -      close (Assumes (map #1 asms ~~ propp))
  1.1263 -  | finish_ext_elem _ close (Defines defs, propp) =
  1.1264 -      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
  1.1265 -  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
  1.1266 -
  1.1267 -
  1.1268 -(* CB: finish_parms introduces type info from parms to identifiers *)
  1.1269 -(* CB: only needed for types that have been NONE so far???
  1.1270 -   If so, which are these??? *)
  1.1271 -
  1.1272 -fun finish_parms parms (((name, ps), mode), elems) =
  1.1273 -  (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
  1.1274 -
  1.1275 -fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
  1.1276 -      let
  1.1277 -        val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
  1.1278 -        val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
  1.1279 -        val text' = fold (eval_text ctxt id' false) es text;
  1.1280 -        val es' = map_filter
  1.1281 -          (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
  1.1282 -      in ((text', wits'), (id', map Int es')) end
  1.1283 -  | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
  1.1284 -      let
  1.1285 -        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
  1.1286 -        val text' = eval_text ctxt id true e' text;
  1.1287 -      in ((text', wits), (id, [Ext e'])) end
  1.1288 -
  1.1289 -in
  1.1290 -
  1.1291 -(* CB: only called by prep_elemss *)
  1.1292 -
  1.1293 -fun finish_elemss ctxt parms do_close =
  1.1294 -  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
  1.1295 -
  1.1296 -end;
  1.1297 -
  1.1298 -
  1.1299 -(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
  1.1300 -
  1.1301 -fun defs_ord (defs1, defs2) =
  1.1302 -    list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
  1.1303 -      TermOrd.fast_term_ord (d1, d2)) (defs1, defs2);
  1.1304 -structure Defstab =
  1.1305 -    TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
  1.1306 -
  1.1307 -fun rem_dup_defs es ds =
  1.1308 -    fold_map (fn e as (Defines defs) => (fn ds =>
  1.1309 -                 if Defstab.defined ds defs
  1.1310 -                 then (Defines [], ds)
  1.1311 -                 else (e, Defstab.update (defs, ()) ds))
  1.1312 -               | e => (fn ds => (e, ds))) es ds;
  1.1313 -fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
  1.1314 -  | rem_dup_elemss (Ext e) ds = (Ext e, ds);
  1.1315 -fun rem_dup_defines raw_elemss =
  1.1316 -    fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
  1.1317 -                     apfst (pair id) (rem_dup_elemss es ds))
  1.1318 -               | (id as (_, (Derived _)), es) => (fn ds =>
  1.1319 -                     ((id, es), ds))) raw_elemss Defstab.empty |> #1;
  1.1320 -
  1.1321 -(* CB: type inference and consistency checks for locales.
  1.1322 -
  1.1323 -   Works by building a context (through declare_elemss), extracting the
  1.1324 -   required information and adjusting the context elements (finish_elemss).
  1.1325 -   Can also universally close free vars in assms and defs.  This is only
  1.1326 -   needed for Ext elements and controlled by parameter do_close.
  1.1327 -
  1.1328 -   Only elements of assumed identifiers are considered.
  1.1329 -*)
  1.1330 -
  1.1331 -fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
  1.1332 -  let
  1.1333 -    (* CB: contexts computed in the course of this function are discarded.
  1.1334 -       They are used for type inference and consistency checks only. *)
  1.1335 -    (* CB: fixed_params are the parameters (with types) of the target locale,
  1.1336 -       empty list if there is no target. *)
  1.1337 -    (* CB: raw_elemss are list of pairs consisting of identifiers and
  1.1338 -       context elements, the latter marked as internal or external. *)
  1.1339 -    val raw_elemss = rem_dup_defines raw_elemss;
  1.1340 -    val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
  1.1341 -    (* CB: raw_ctxt is context with additional fixed variables derived from
  1.1342 -       the fixes elements in raw_elemss,
  1.1343 -       raw_proppss contains assumptions and definitions from the
  1.1344 -       external elements in raw_elemss. *)
  1.1345 -    fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
  1.1346 -      let
  1.1347 -        (* CB: add type information from fixed_params to context (declare_term) *)
  1.1348 -        (* CB: process patterns (conclusion and external elements only) *)
  1.1349 -        val (ctxt, all_propp) =
  1.1350 -          prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  1.1351 -        (* CB: add type information from conclusion and external elements to context *)
  1.1352 -        val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
  1.1353 -        (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
  1.1354 -        val all_propp' = map2 (curry (op ~~))
  1.1355 -          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
  1.1356 -        val (concl, propp) = chop (length raw_concl) all_propp';
  1.1357 -      in (propp, (ctxt, concl)) end
  1.1358 -
  1.1359 -    val (proppss, (ctxt, concl)) =
  1.1360 -      (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
  1.1361 -
  1.1362 -    (* CB: obtain all parameters from identifier part of raw_elemss *)
  1.1363 -    val xs = map #1 (params_of' raw_elemss);
  1.1364 -    val typing = unify_frozen ctxt 0
  1.1365 -      (map (Variable.default_type raw_ctxt) xs)
  1.1366 -      (map (Variable.default_type ctxt) xs);
  1.1367 -    val parms = param_types (xs ~~ typing);
  1.1368 -    (* CB: parms are the parameters from raw_elemss, with correct typing. *)
  1.1369 -
  1.1370 -    (* CB: extract information from assumes and defines elements
  1.1371 -       (fixes, constrains and notes in raw_elemss don't have an effect on
  1.1372 -       text and elemss), compute final form of context elements. *)
  1.1373 -    val ((text, _), elemss) = finish_elemss ctxt parms do_close
  1.1374 -      ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
  1.1375 -    (* CB: text has the following structure:
  1.1376 -           (((exts, exts'), (ints, ints')), (xs, env, defs))
  1.1377 -       where
  1.1378 -         exts: external assumptions (terms in external assumes elements)
  1.1379 -         exts': dito, normalised wrt. env
  1.1380 -         ints: internal assumptions (terms in internal assumes elements)
  1.1381 -         ints': dito, normalised wrt. env
  1.1382 -         xs: the free variables in exts' and ints' and rhss of definitions,
  1.1383 -           this includes parameters except defined parameters
  1.1384 -         env: list of term pairs encoding substitutions, where the first term
  1.1385 -           is a free variable; substitutions represent defines elements and
  1.1386 -           the rhs is normalised wrt. the previous env
  1.1387 -         defs: theorems representing the substitutions from defines elements
  1.1388 -           (thms are normalised wrt. env).
  1.1389 -       elemss is an updated version of raw_elemss:
  1.1390 -         - type info added to Fixes and modified in Constrains
  1.1391 -         - axiom and definition statement replaced by corresponding one
  1.1392 -           from proppss in Assumes and Defines
  1.1393 -         - Facts unchanged
  1.1394 -       *)
  1.1395 -  in ((parms, elemss, concl), text) end;
  1.1396 -
  1.1397 -in
  1.1398 -
  1.1399 -fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
  1.1400 -fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
  1.1401 -
  1.1402 -end;
  1.1403 -
  1.1404 -
  1.1405 -(* facts and attributes *)
  1.1406 -
  1.1407 -local
  1.1408 -
  1.1409 -fun check_name name =
  1.1410 -  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
  1.1411 -  else name;
  1.1412 -
  1.1413 -fun prep_facts _ _ _ ctxt (Int elem) = elem
  1.1414 -      |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
  1.1415 -  | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  1.1416 -     {var = I, typ = I, term = I,
  1.1417 -      binding = Binding.map_base prep_name,
  1.1418 -      fact = get ctxt,
  1.1419 -      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  1.1420 -
  1.1421 -in
  1.1422 -
  1.1423 -fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
  1.1424 -fun cert_facts x = prep_facts I (K I) (K I) x;
  1.1425 -
  1.1426 -end;
  1.1427 -
  1.1428 -
  1.1429 -(* Get the specification of a locale *)
  1.1430 -
  1.1431 -(*The global specification is made from the parameters and global
  1.1432 -  assumptions, the local specification from the parameters and the
  1.1433 -  local assumptions.*)
  1.1434 -
  1.1435 -local
  1.1436 -
  1.1437 -fun gen_asms_of get thy name =
  1.1438 -  let
  1.1439 -    val ctxt = ProofContext.init thy;
  1.1440 -    val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
  1.1441 -    val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
  1.1442 -  in
  1.1443 -    elemss |> get
  1.1444 -      |> maps (fn (_, es) => map (fn Int e => e) es)
  1.1445 -      |> maps (fn Assumes asms => asms | _ => [])
  1.1446 -      |> map (apsnd (map fst))
  1.1447 -  end;
  1.1448 -
  1.1449 -in
  1.1450 -
  1.1451 -fun parameters_of thy = #params o the_locale thy;
  1.1452 -
  1.1453 -fun intros thy = #intros o the_locale thy;
  1.1454 -  (*returns introduction rule for delta predicate and locale predicate
  1.1455 -    as a pair of singleton lists*)
  1.1456 -
  1.1457 -fun dests thy = #dests o the_locale thy;
  1.1458 -
  1.1459 -fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts
  1.1460 -  | _ => NONE) o #elems o the_locale thy;
  1.1461 -
  1.1462 -fun parameters_of_expr thy expr =
  1.1463 -  let
  1.1464 -    val ctxt = ProofContext.init thy;
  1.1465 -    val pts = params_of_expr ctxt [] (intern_expr thy expr)
  1.1466 -        ([], Symtab.empty, Symtab.empty);
  1.1467 -    val raw_params_elemss = make_raw_params_elemss pts;
  1.1468 -    val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  1.1469 -        (([], Symtab.empty), Expr expr);
  1.1470 -    val ((parms, _, _), _) =
  1.1471 -        read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
  1.1472 -  in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
  1.1473 -
  1.1474 -fun local_asms_of thy name =
  1.1475 -  gen_asms_of (single o Library.last_elem) thy name;
  1.1476 -
  1.1477 -fun global_asms_of thy name =
  1.1478 -  gen_asms_of I thy name;
  1.1479 -
  1.1480 -end;
  1.1481 -
  1.1482 -
  1.1483 -(* full context statements: imports + elements + conclusion *)
  1.1484 -
  1.1485 -local
  1.1486 -
  1.1487 -fun prep_context_statement prep_expr prep_elemss prep_facts
  1.1488 -    do_close fixed_params imports elements raw_concl context =
  1.1489 -  let
  1.1490 -    val thy = ProofContext.theory_of context;
  1.1491 -
  1.1492 -    val (import_params, import_tenv, import_syn) =
  1.1493 -      params_of_expr context fixed_params (prep_expr thy imports)
  1.1494 -        ([], Symtab.empty, Symtab.empty);
  1.1495 -    val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
  1.1496 -    val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
  1.1497 -      (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
  1.1498 -
  1.1499 -    val ((import_ids, _), raw_import_elemss) =
  1.1500 -      flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
  1.1501 -    (* CB: normalise "includes" among elements *)
  1.1502 -    val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
  1.1503 -      ((import_ids, incl_syn), elements);
  1.1504 -
  1.1505 -    val raw_elemss = flat raw_elemsss;
  1.1506 -    (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  1.1507 -       context elements obtained from import and elements. *)
  1.1508 -    (* Now additional elements for parameters are inserted. *)
  1.1509 -    val import_params_ids = make_params_ids import_params;
  1.1510 -    val incl_params_ids =
  1.1511 -        make_params_ids (incl_params \\ import_params);
  1.1512 -    val raw_import_params_elemss =
  1.1513 -        make_raw_params_elemss (import_params, incl_tenv, incl_syn);
  1.1514 -    val raw_incl_params_elemss =
  1.1515 -        make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
  1.1516 -    val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  1.1517 -      context fixed_params
  1.1518 -      (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
  1.1519 -
  1.1520 -    (* replace extended ids (for axioms) by ids *)
  1.1521 -    val (import_ids', incl_ids) = chop (length import_ids) ids;
  1.1522 -    val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
  1.1523 -    val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
  1.1524 -        (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
  1.1525 -      (all_ids ~~ all_elemss);
  1.1526 -    (* CB: all_elemss and parms contain the correct parameter types *)
  1.1527 -
  1.1528 -    val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  1.1529 -    val ((import_elemss, _), import_ctxt) =
  1.1530 -      activate_facts false prep_facts ps context;
  1.1531 -
  1.1532 -    val ((elemss, _), ctxt) =
  1.1533 -      activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
  1.1534 -  in
  1.1535 -    ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  1.1536 -      (parms, spec, defs)), concl)
  1.1537 -  end;
  1.1538 -
  1.1539 -fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  1.1540 -  let
  1.1541 -    val thy = ProofContext.theory_of ctxt;
  1.1542 -    val locale = Option.map (prep_locale thy) raw_locale;
  1.1543 -    val (fixed_params, imports) =
  1.1544 -      (case locale of
  1.1545 -        NONE => ([], empty)
  1.1546 -      | SOME name =>
  1.1547 -          let val {params = ps, ...} = the_locale thy name
  1.1548 -          in (map fst ps, Locale name) end);
  1.1549 -    val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
  1.1550 -      prep_ctxt false fixed_params imports (map Elem elems) concl ctxt;
  1.1551 -  in (locale, locale_ctxt, elems_ctxt, concl') end;
  1.1552 -
  1.1553 -fun prep_expr prep imports body ctxt =
  1.1554 -  let
  1.1555 -    val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
  1.1556 -    val all_elems = maps snd (import_elemss @ elemss);
  1.1557 -  in (all_elems, ctxt') end;
  1.1558 -
  1.1559 -in
  1.1560 -
  1.1561 -val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
  1.1562 -val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
  1.1563 -
  1.1564 -fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
  1.1565 -fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
  1.1566 -
  1.1567 -val read_expr = prep_expr read_context;
  1.1568 -val cert_expr = prep_expr cert_context;
  1.1569 -
  1.1570 -fun read_context_statement loc = prep_statement (K I) read_ctxt loc;
  1.1571 -fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc;
  1.1572 -fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
  1.1573 -
  1.1574 -end;
  1.1575 -
  1.1576 -
  1.1577 -(* init *)
  1.1578 -
  1.1579 -fun init loc =
  1.1580 -  ProofContext.init
  1.1581 -  #> #2 o cert_context_statement (SOME loc) [] [];
  1.1582 -
  1.1583 -
  1.1584 -(* print locale *)
  1.1585 -
  1.1586 -fun print_locale thy show_facts imports body =
  1.1587 -  let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
  1.1588 -    Pretty.big_list "locale elements:" (all_elems
  1.1589 -      |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
  1.1590 -      |> map (Element.pretty_ctxt ctxt) |> filter_out null
  1.1591 -      |> map Pretty.chunks)
  1.1592 -    |> Pretty.writeln
  1.1593 -  end;
  1.1594 -
  1.1595 -
  1.1596 -
  1.1597 -(** store results **)
  1.1598 -
  1.1599 -(* join equations of an id with already accumulated ones *)
  1.1600 -
  1.1601 -fun join_eqns get_reg id eqns =
  1.1602 -  let
  1.1603 -    val eqns' = case get_reg id
  1.1604 -      of NONE => eqns
  1.1605 -        | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns')
  1.1606 -            (* prefer equations from eqns' *)
  1.1607 -  in ((id, eqns'), eqns') end;
  1.1608 -
  1.1609 -
  1.1610 -(* collect witnesses and equations up to a particular target for a
  1.1611 -   registration; requires parameters and flattened list of identifiers
  1.1612 -   instead of recomputing it from the target *)
  1.1613 -
  1.1614 -fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let
  1.1615 -
  1.1616 -    val thy = ProofContext.theory_of ctxt;
  1.1617 -
  1.1618 -    val ts = map (var_inst_term (impT, imp)) ext_ts;
  1.1619 -    val (parms, parmTs) = split_list parms;
  1.1620 -    val parmvTs = map Logic.varifyT parmTs;
  1.1621 -    val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
  1.1622 -    val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
  1.1623 -        |> Symtab.make;
  1.1624 -    val inst = Symtab.make (parms ~~ ts);
  1.1625 -
  1.1626 -    (* instantiate parameter names in ids *)
  1.1627 -    val ext_inst = Symtab.make (parms ~~ ext_ts);
  1.1628 -    fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps;
  1.1629 -    val inst_ids = map (apfst (apsnd ext_inst_names)) ids;
  1.1630 -    val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
  1.1631 -    val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids;
  1.1632 -    val eqns =
  1.1633 -      fold_map (join_eqns (get_local_registration ctxt imprt))
  1.1634 -        (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd;
  1.1635 -  in ((tinst, inst), wits, eqns) end;
  1.1636 -
  1.1637 -
  1.1638 -(* compute and apply morphism *)
  1.1639 -
  1.1640 -fun name_morph phi_name (lprfx, pprfx) b =
  1.1641 -  b
  1.1642 -  |> (if not (Binding.is_empty b) andalso pprfx <> ""
  1.1643 -        then Binding.add_prefix false pprfx else I)
  1.1644 -  |> (if not (Binding.is_empty b)
  1.1645 -        then Binding.add_prefix false lprfx else I)
  1.1646 -  |> phi_name;
  1.1647 -
  1.1648 -fun inst_morph thy phi_name param_prfx insts prems eqns export =
  1.1649 -  let
  1.1650 -    (* standardise export morphism *)
  1.1651 -    val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
  1.1652 -    val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
  1.1653 -      (* FIXME sync with exp_fact *)
  1.1654 -    val exp_typ = Logic.type_map exp_term;
  1.1655 -    val export' =
  1.1656 -      Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  1.1657 -  in
  1.1658 -    Morphism.binding_morphism (name_morph phi_name param_prfx) $>
  1.1659 -      Element.inst_morphism thy insts $>
  1.1660 -      Element.satisfy_morphism prems $>
  1.1661 -      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
  1.1662 -      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
  1.1663 -      export'
  1.1664 -  end;
  1.1665 -
  1.1666 -fun activate_note thy phi_name param_prfx attrib insts prems eqns exp =
  1.1667 -  (Element.facts_map o Element.morph_ctxt)
  1.1668 -      (inst_morph thy phi_name param_prfx insts prems eqns exp)
  1.1669 -  #> Attrib.map_facts attrib;
  1.1670 -
  1.1671 -
  1.1672 -(* public interface to interpretation morphism *)
  1.1673 -
  1.1674 -fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts =
  1.1675 -  let
  1.1676 -    val parms = the_locale thy target |> #params |> map fst;
  1.1677 -    val ids = flatten (ProofContext.init thy, intern_expr thy)
  1.1678 -      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  1.1679 -    val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  1.1680 -  in
  1.1681 -    inst_morph thy phi_name param_prfx insts prems eqns exp
  1.1682 -  end;
  1.1683 -
  1.1684 -(* store instantiations of args for all registered interpretations
  1.1685 -   of the theory *)
  1.1686 -
  1.1687 -fun note_thmss_registrations target (kind, args) thy =
  1.1688 -  let
  1.1689 -    val parms = the_locale thy target |> #params |> map fst;
  1.1690 -    val ids = flatten (ProofContext.init thy, intern_expr thy)
  1.1691 -      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  1.1692 -
  1.1693 -    val regs = get_global_registrations thy target;
  1.1694 -    (* add args to thy for all registrations *)
  1.1695 -
  1.1696 -    fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  1.1697 -      let
  1.1698 -        val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  1.1699 -        val args' = args
  1.1700 -          |> activate_note thy phi_name param_prfx
  1.1701 -               (Attrib.attribute_i thy) insts prems eqns exp;
  1.1702 -      in
  1.1703 -        thy
  1.1704 -        |> global_note_qualified kind args'
  1.1705 -        |> snd
  1.1706 -      end;
  1.1707 -  in fold activate regs thy end;
  1.1708 -
  1.1709 -
  1.1710 -(* locale results *)
  1.1711 -
  1.1712 -fun add_thmss loc kind args ctxt =
  1.1713 -  let
  1.1714 -    val (([(_, [Notes args'])], _), ctxt') =
  1.1715 -      activate_facts true cert_facts
  1.1716 -        [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
  1.1717 -    val ctxt'' = ctxt' |> ProofContext.theory
  1.1718 -      (change_locale loc
  1.1719 -        (fn (axiom, elems, params, decls, regs, intros, dests) =>
  1.1720 -          (axiom, elems @ [(Notes args', stamp ())],
  1.1721 -            params, decls, regs, intros, dests))
  1.1722 -      #> note_thmss_registrations loc args');
  1.1723 -  in ctxt'' end;
  1.1724 -
  1.1725 -
  1.1726 -(* declarations *)
  1.1727 -
  1.1728 -local
  1.1729 -
  1.1730 -fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
  1.1731 -
  1.1732 -fun add_decls add loc decl =
  1.1733 -  ProofContext.theory (change_locale loc
  1.1734 -    (fn (axiom, elems, params, decls, regs, intros, dests) =>
  1.1735 -      (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
  1.1736 -  add_thmss loc Thm.internalK
  1.1737 -    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  1.1738 -
  1.1739 -in
  1.1740 -
  1.1741 -val add_type_syntax = add_decls (apfst o cons);
  1.1742 -val add_term_syntax = add_decls (apsnd o cons);
  1.1743 -val add_declaration = add_decls (K I);
  1.1744 -
  1.1745 -fun declarations_of thy loc =
  1.1746 -  the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst);
  1.1747 -
  1.1748 -end;
  1.1749 -
  1.1750 -
  1.1751 -
  1.1752 -(** define locales **)
  1.1753 -
  1.1754 -(* predicate text *)
  1.1755 -(* CB: generate locale predicates and delta predicates *)
  1.1756 -
  1.1757 -local
  1.1758 -
  1.1759 -(* introN: name of theorems for introduction rules of locale and
  1.1760 -     delta predicates;
  1.1761 -   axiomsN: name of theorem set with destruct rules for locale predicates,
  1.1762 -     also name suffix of delta predicates. *)
  1.1763 -
  1.1764 -val introN = "intro";
  1.1765 -val axiomsN = "axioms";
  1.1766 -
  1.1767 -fun atomize_spec thy ts =
  1.1768 -  let
  1.1769 -    val t = Logic.mk_conjunction_balanced ts;
  1.1770 -    val body = ObjectLogic.atomize_term thy t;
  1.1771 -    val bodyT = Term.fastype_of body;
  1.1772 -  in
  1.1773 -    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
  1.1774 -    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
  1.1775 -  end;
  1.1776 -
  1.1777 -fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
  1.1778 -  if length args = n then
  1.1779 -    Syntax.const "_aprop" $
  1.1780 -      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
  1.1781 -  else raise Match);
  1.1782 -
  1.1783 -(* CB: define one predicate including its intro rule and axioms
  1.1784 -   - bname: predicate name
  1.1785 -   - parms: locale parameters
  1.1786 -   - defs: thms representing substitutions from defines elements
  1.1787 -   - ts: terms representing locale assumptions (not normalised wrt. defs)
  1.1788 -   - norm_ts: terms representing locale assumptions (normalised wrt. defs)
  1.1789 -   - thy: the theory
  1.1790 -*)
  1.1791 -
  1.1792 -fun def_pred bname parms defs ts norm_ts thy =
  1.1793 -  let
  1.1794 -    val name = Sign.full_bname thy bname;
  1.1795 -
  1.1796 -    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  1.1797 -    val env = Term.add_free_names body [];
  1.1798 -    val xs = filter (member (op =) env o #1) parms;
  1.1799 -    val Ts = map #2 xs;
  1.1800 -    val extraTs =
  1.1801 -      (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
  1.1802 -      |> Library.sort_wrt #1 |> map TFree;
  1.1803 -    val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
  1.1804 -
  1.1805 -    val args = map Logic.mk_type extraTs @ map Free xs;
  1.1806 -    val head = Term.list_comb (Const (name, predT), args);
  1.1807 -    val statement = ObjectLogic.ensure_propT thy head;
  1.1808 -
  1.1809 -    val ([pred_def], defs_thy) =
  1.1810 -      thy
  1.1811 -      |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
  1.1812 -      |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
  1.1813 -      |> PureThy.add_defs false
  1.1814 -        [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
  1.1815 -    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  1.1816 -
  1.1817 -    val cert = Thm.cterm_of defs_thy;
  1.1818 -
  1.1819 -    val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
  1.1820 -      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
  1.1821 -      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
  1.1822 -      Tactic.compose_tac (false,
  1.1823 -        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
  1.1824 -
  1.1825 -    val conjuncts =
  1.1826 -      (Drule.equal_elim_rule2 OF [body_eq,
  1.1827 -        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
  1.1828 -      |> Conjunction.elim_balanced (length ts);
  1.1829 -    val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
  1.1830 -      Element.prove_witness defs_ctxt t
  1.1831 -       (MetaSimplifier.rewrite_goals_tac defs THEN
  1.1832 -        Tactic.compose_tac (false, ax, 0) 1));
  1.1833 -  in ((statement, intro, axioms), defs_thy) end;
  1.1834 -
  1.1835 -fun assumes_to_notes (Assumes asms) axms =
  1.1836 -      fold_map (fn (a, spec) => fn axs =>
  1.1837 -          let val (ps, qs) = chop (length spec) axs
  1.1838 -          in ((a, [(ps, [])]), qs) end) asms axms
  1.1839 -      |> apfst (curry Notes Thm.assumptionK)
  1.1840 -  | assumes_to_notes e axms = (e, axms);
  1.1841 -
  1.1842 -(* CB: the following two change only "new" elems, these have identifier ("", _). *)
  1.1843 -
  1.1844 -(* turn Assumes into Notes elements *)
  1.1845 -
  1.1846 -fun change_assumes_elemss axioms elemss =
  1.1847 -  let
  1.1848 -    val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1.1849 -    fun change (id as ("", _), es) =
  1.1850 -          fold_map assumes_to_notes (map satisfy es)
  1.1851 -          #-> (fn es' => pair (id, es'))
  1.1852 -      | change e = pair e;
  1.1853 -  in
  1.1854 -    fst (fold_map change elemss (map Element.conclude_witness axioms))
  1.1855 -  end;
  1.1856 -
  1.1857 -(* adjust hyps of Notes elements *)
  1.1858 -
  1.1859 -fun change_elemss_hyps axioms elemss =
  1.1860 -  let
  1.1861 -    val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  1.1862 -    fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
  1.1863 -      | change e = e;
  1.1864 -  in map change elemss end;
  1.1865 -
  1.1866 -in
  1.1867 -
  1.1868 -(* CB: main predicate definition function *)
  1.1869 -
  1.1870 -fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  1.1871 -  let
  1.1872 -    val ((elemss', more_ts), a_elem, a_intro, thy'') =
  1.1873 -      if null exts then ((elemss, []), [], [], thy)
  1.1874 -      else
  1.1875 -        let
  1.1876 -          val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
  1.1877 -          val ((statement, intro, axioms), thy') =
  1.1878 -            thy
  1.1879 -            |> def_pred aname parms defs exts exts';
  1.1880 -          val elemss' = change_assumes_elemss axioms elemss;
  1.1881 -          val a_elem = [(("", []),
  1.1882 -            [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  1.1883 -          val (_, thy'') =
  1.1884 -            thy'
  1.1885 -            |> Sign.add_path aname
  1.1886 -            |> Sign.no_base_names
  1.1887 -            |> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])]
  1.1888 -            ||> Sign.restore_naming thy';
  1.1889 -        in ((elemss', [statement]), a_elem, [intro], thy'') end;
  1.1890 -    val (predicate, stmt', elemss'', b_intro, thy'''') =
  1.1891 -      if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
  1.1892 -      else
  1.1893 -        let
  1.1894 -          val ((statement, intro, axioms), thy''') =
  1.1895 -            thy''
  1.1896 -            |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts);
  1.1897 -          val cstatement = Thm.cterm_of thy''' statement;
  1.1898 -          val elemss'' = change_elemss_hyps axioms elemss';
  1.1899 -          val b_elem = [(("", []),
  1.1900 -               [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  1.1901 -          val (_, thy'''') =
  1.1902 -            thy'''
  1.1903 -            |> Sign.add_path pname
  1.1904 -            |> Sign.no_base_names
  1.1905 -            |> PureThy.note_thmss Thm.internalK
  1.1906 -                 [((Binding.name introN, []), [([intro], [])]),
  1.1907 -                  ((Binding.name axiomsN, []),
  1.1908 -                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  1.1909 -            ||> Sign.restore_naming thy''';
  1.1910 -        in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
  1.1911 -  in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
  1.1912 -
  1.1913 -end;
  1.1914 -
  1.1915 -
  1.1916 -(* add_locale(_i) *)
  1.1917 -
  1.1918 -local
  1.1919 -
  1.1920 -(* turn Defines into Notes elements, accumulate definition terms *)
  1.1921 -
  1.1922 -fun defines_to_notes is_ext thy (Defines defs) defns =
  1.1923 -    let
  1.1924 -      val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs
  1.1925 -      val notes = map (fn (a, (def, _)) =>
  1.1926 -        (a, [([assume (cterm_of thy def)], [])])) defs
  1.1927 -    in
  1.1928 -      (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
  1.1929 -    end
  1.1930 -  | defines_to_notes _ _ e defns = (SOME e, defns);
  1.1931 -
  1.1932 -fun change_defines_elemss thy elemss defns =
  1.1933 -  let
  1.1934 -    fun change (id as (n, _), es) defns =
  1.1935 -        let
  1.1936 -          val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
  1.1937 -        in ((id, map_filter I es'), defns') end
  1.1938 -  in fold_map change elemss defns end;
  1.1939 -
  1.1940 -fun gen_add_locale prep_ctxt prep_expr
  1.1941 -    predicate_name bname raw_imports raw_body thy =
  1.1942 -    (* predicate_name: "" - locale with predicate named as locale
  1.1943 -        "name" - locale with predicate named "name" *)
  1.1944 -  let
  1.1945 -    val thy_ctxt = ProofContext.init thy;
  1.1946 -    val name = Sign.full_bname thy bname;
  1.1947 -    val _ = is_some (get_locale thy name) andalso
  1.1948 -      error ("Duplicate definition of locale " ^ quote name);
  1.1949 -
  1.1950 -    val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  1.1951 -      text as (parms, ((_, exts'), _), defs)) =
  1.1952 -        prep_ctxt raw_imports raw_body thy_ctxt;
  1.1953 -    val elemss = import_elemss @ body_elemss |>
  1.1954 -      map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  1.1955 -
  1.1956 -    val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\
  1.1957 -      List.foldr OldTerm.add_typ_tfrees [] (map snd parms);
  1.1958 -    val _ = if null extraTs then ()
  1.1959 -      else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  1.1960 -
  1.1961 -    val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
  1.1962 -    val (elemss', defns) = change_defines_elemss thy elemss [];
  1.1963 -    val elemss'' = elemss' @ [(("", []), defns)];
  1.1964 -    val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
  1.1965 -      define_preds predicate_name' text elemss'' thy;
  1.1966 -    val regs = pred_axioms
  1.1967 -      |> fold_map (fn (id, elems) => fn wts => let
  1.1968 -             val ts = flat (map_filter (fn (Assumes asms) =>
  1.1969 -               SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1.1970 -             val (wts1, wts2) = chop (length ts) wts;
  1.1971 -           in ((apsnd (map fst) id, wts1), wts2) end) elemss'''
  1.1972 -      |> fst
  1.1973 -      |> map_filter (fn (("", _), _) => NONE | e => SOME e);
  1.1974 -    fun axiomify axioms elemss =
  1.1975 -      (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  1.1976 -                   val ts = flat (map_filter (fn (Assumes asms) =>
  1.1977 -                     SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1.1978 -                   val (axs1, axs2) = chop (length ts) axs;
  1.1979 -                 in (axs2, ((id, Assumed axs1), elems)) end)
  1.1980 -      |> snd;
  1.1981 -    val ((_, facts), ctxt) = activate_facts true (K I)
  1.1982 -      (axiomify pred_axioms elemss''') (ProofContext.init thy');
  1.1983 -    val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
  1.1984 -    val export = Thm.close_derivation o Goal.norm_result o
  1.1985 -      singleton (ProofContext.export view_ctxt thy_ctxt);
  1.1986 -    val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  1.1987 -    val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss''');
  1.1988 -    val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  1.1989 -    val axs' = map (Element.assume_witness thy') stmt';
  1.1990 -    val loc_ctxt = thy'
  1.1991 -      |> Sign.add_path bname
  1.1992 -      |> Sign.no_base_names
  1.1993 -      |> PureThy.note_thmss Thm.assumptionK facts' |> snd
  1.1994 -      |> Sign.restore_naming thy'
  1.1995 -      |> register_locale bname {axiom = axs',
  1.1996 -        elems = map (fn e => (e, stamp ())) elems'',
  1.1997 -        params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  1.1998 -        decls = ([], []),
  1.1999 -        regs = regs,
  1.2000 -        intros = intros,
  1.2001 -        dests = map Element.conclude_witness pred_axioms}
  1.2002 -      |> init name;
  1.2003 -  in (name, loc_ctxt) end;
  1.2004 -
  1.2005 -in
  1.2006 -
  1.2007 -val add_locale = gen_add_locale cert_context (K I);
  1.2008 -val add_locale_cmd = gen_add_locale read_context intern_expr "";
  1.2009 -
  1.2010 -end;
  1.2011 -
  1.2012 -val _ = Context.>> (Context.map_theory
  1.2013 - (add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #>
  1.2014 -  snd #> ProofContext.theory_of #>
  1.2015 -  add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #>
  1.2016 -  snd #> ProofContext.theory_of));
  1.2017 -
  1.2018 -
  1.2019 -
  1.2020 -
  1.2021 -(** Normalisation of locale statements ---
  1.2022 -    discharges goals implied by interpretations **)
  1.2023 -
  1.2024 -local
  1.2025 -
  1.2026 -fun locale_assm_intros thy =
  1.2027 -  Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
  1.2028 -    (#2 (LocalesData.get thy)) [];
  1.2029 -fun locale_base_intros thy =
  1.2030 -  Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
  1.2031 -    (#2 (LocalesData.get thy)) [];
  1.2032 -
  1.2033 -fun all_witnesses ctxt =
  1.2034 -  let
  1.2035 -    val thy = ProofContext.theory_of ctxt;
  1.2036 -    fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
  1.2037 -        (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) =>
  1.2038 -          map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms)
  1.2039 -      registrations [];
  1.2040 -  in get (RegistrationsData.get (Context.Proof ctxt)) end;
  1.2041 -
  1.2042 -in
  1.2043 -
  1.2044 -fun intro_locales_tac eager ctxt facts st =
  1.2045 -  let
  1.2046 -    val wits = all_witnesses ctxt;
  1.2047 -    val thy = ProofContext.theory_of ctxt;
  1.2048 -    val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
  1.2049 -  in
  1.2050 -    Method.intros_tac (wits @ intros) facts st
  1.2051 -  end;
  1.2052 -
  1.2053 -end;
  1.2054 -
  1.2055 -
  1.2056 -(** Interpretation commands **)
  1.2057 -
  1.2058 -local
  1.2059 -
  1.2060 -(* extract proof obligations (assms and defs) from elements *)
  1.2061 -
  1.2062 -fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
  1.2063 -  | extract_asms_elems ((id, Derived _), _) = (id, []);
  1.2064 -
  1.2065 -
  1.2066 -(* activate instantiated facts in theory or context *)
  1.2067 -
  1.2068 -fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn
  1.2069 -        phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
  1.2070 -  let
  1.2071 -    val ctxt = mk_ctxt thy_ctxt;
  1.2072 -    fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
  1.2073 -    fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt);
  1.2074 -
  1.2075 -    val (all_propss, eq_props) = chop (length all_elemss) propss;
  1.2076 -    val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
  1.2077 -
  1.2078 -    (* Filter out fragments already registered. *)
  1.2079 -
  1.2080 -    val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
  1.2081 -          test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss))));
  1.2082 -    val (new_pss, ys) = split_list xs;
  1.2083 -    val (new_propss, new_thmss) = split_list ys;
  1.2084 -
  1.2085 -    val thy_ctxt' = thy_ctxt
  1.2086 -      (* add registrations *)
  1.2087 -      |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp))
  1.2088 -           new_elemss new_pss
  1.2089 -      (* add witnesses of Assumed elements (only those generate proof obligations) *)
  1.2090 -      |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss
  1.2091 -      (* add equations *)
  1.2092 -      |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props
  1.2093 -          ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
  1.2094 -            Element.conclude_witness) eq_thms);
  1.2095 -
  1.2096 -    val prems = flat (map_filter
  1.2097 -          (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
  1.2098 -            | ((_, Derived _), _) => NONE) all_elemss);
  1.2099 -
  1.2100 -    val thy_ctxt'' = thy_ctxt'
  1.2101 -      (* add witnesses of Derived elements *)
  1.2102 -      |> fold (fn (id, thms) => fold
  1.2103 -           (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
  1.2104 -         (map_filter (fn ((_, Assumed _), _) => NONE
  1.2105 -            | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
  1.2106 -
  1.2107 -    fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
  1.2108 -        let
  1.2109 -          val ctxt = mk_ctxt thy_ctxt;
  1.2110 -          val thy = ProofContext.theory_of ctxt;
  1.2111 -          val facts' = facts
  1.2112 -            |> activate_note thy phi_name param_prfx
  1.2113 -                 (attrib thy_ctxt) insts prems eqns exp;
  1.2114 -        in 
  1.2115 -          thy_ctxt
  1.2116 -          |> note kind facts'
  1.2117 -          |> snd
  1.2118 -        end
  1.2119 -      | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
  1.2120 -
  1.2121 -    fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt =
  1.2122 -      let
  1.2123 -        val ctxt = mk_ctxt thy_ctxt;
  1.2124 -        val thy = ProofContext.theory_of ctxt;
  1.2125 -        val {params, elems, ...} = the_locale thy loc;
  1.2126 -        val parms = map fst params;
  1.2127 -        val param_prfx = param_prefix loc ps;
  1.2128 -        val ids = flatten (ProofContext.init thy, intern_expr thy)
  1.2129 -          (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
  1.2130 -        val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
  1.2131 -      in
  1.2132 -        thy_ctxt
  1.2133 -        |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems
  1.2134 -      end;
  1.2135 -
  1.2136 -  in
  1.2137 -    thy_ctxt''
  1.2138 -    (* add equations as lemmas to context *)
  1.2139 -    |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
  1.2140 -         ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
  1.2141 -            (unflat eq_thms eq_attns) eq_thms
  1.2142 -    (* add interpreted facts *)
  1.2143 -    |> fold2 activate_elems new_elemss new_pss
  1.2144 -  end;
  1.2145 -
  1.2146 -fun global_activate_facts_elemss x = gen_activate_facts_elemss
  1.2147 -  ProofContext.init
  1.2148 -  global_note_qualified
  1.2149 -  Attrib.attribute_i
  1.2150 -  put_global_registration
  1.2151 -  add_global_witness
  1.2152 -  add_global_equation
  1.2153 -  x;
  1.2154 -
  1.2155 -fun local_activate_facts_elemss x = gen_activate_facts_elemss
  1.2156 -  I
  1.2157 -  local_note_qualified
  1.2158 -  (Attrib.attribute_i o ProofContext.theory_of)
  1.2159 -  put_local_registration
  1.2160 -  add_local_witness
  1.2161 -  add_local_equation
  1.2162 -  x;
  1.2163 -
  1.2164 -fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
  1.2165 -  let
  1.2166 -    (* parameters *)
  1.2167 -    val (parm_names, parm_types) = parms |> split_list
  1.2168 -      ||> map (TypeInfer.paramify_vars o Logic.varifyT);
  1.2169 -    val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar);
  1.2170 -    val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
  1.2171 -
  1.2172 -    (* parameter instantiations *)
  1.2173 -    val d = length parms - length insts;
  1.2174 -    val insts =
  1.2175 -      if d < 0 then error "More arguments than parameters in instantiation."
  1.2176 -      else insts @ replicate d NONE;
  1.2177 -    val (given_ps, given_insts) =
  1.2178 -      ((parm_names ~~ parm_types) ~~ insts) |> map_filter
  1.2179 -          (fn (_, NONE) => NONE
  1.2180 -            | ((n, T), SOME inst) => SOME ((n, T), inst))
  1.2181 -        |> split_list;
  1.2182 -    val (given_parm_names, given_parm_types) = given_ps |> split_list;
  1.2183 -
  1.2184 -    (* parse insts / eqns *)
  1.2185 -    val given_insts' = map (parse_term ctxt) given_insts;
  1.2186 -    val eqns' = map (parse_prop ctxt) eqns;
  1.2187 -
  1.2188 -    (* type inference and contexts *)
  1.2189 -    val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns';
  1.2190 -    val res = Syntax.check_terms ctxt arg;
  1.2191 -    val ctxt' = ctxt |> fold Variable.auto_fixes res;
  1.2192 -
  1.2193 -    (* instantiation *)
  1.2194 -    val (type_parms'', res') = chop (length type_parms) res;
  1.2195 -    val (given_insts'', eqns'') = chop (length given_insts) res';
  1.2196 -    val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
  1.2197 -    val inst = Symtab.make (given_parm_names ~~ given_insts'');
  1.2198 -
  1.2199 -    (* export from eigencontext *)
  1.2200 -    val export = Variable.export_morphism ctxt' ctxt;
  1.2201 -
  1.2202 -    (* import, its inverse *)
  1.2203 -    val domT = fold Term.add_tfrees res [] |> map TFree;
  1.2204 -    val importT = domT |> map (fn x => (Morphism.typ export x, x))
  1.2205 -      |> map_filter (fn (TFree _, _) => NONE  (* fixed point of export *)
  1.2206 -               | (TVar y, x) => SOME (fst y, x)
  1.2207 -               | _ => error "internal: illegal export in interpretation")
  1.2208 -      |> Vartab.make;
  1.2209 -    val dom = fold Term.add_frees res [] |> map Free;
  1.2210 -    val imprt = dom |> map (fn x => (Morphism.term export x, x))
  1.2211 -      |> map_filter (fn (Free _, _) => NONE  (* fixed point of export *)
  1.2212 -               | (Var y, x) => SOME (fst y, x)
  1.2213 -               | _ => error "internal: illegal export in interpretation")
  1.2214 -      |> Vartab.make;
  1.2215 -  in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end;
  1.2216 -
  1.2217 -val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
  1.2218 -val check_instantiations = prep_instantiations (K I) (K I);
  1.2219 -
  1.2220 -fun gen_prep_registration mk_ctxt test_reg activate
  1.2221 -    prep_attr prep_expr prep_insts
  1.2222 -    thy_ctxt phi_name raw_expr raw_insts =
  1.2223 -  let
  1.2224 -    val ctxt = mk_ctxt thy_ctxt;
  1.2225 -    val thy = ProofContext.theory_of ctxt;
  1.2226 -    val ctxt' = ProofContext.init thy;
  1.2227 -    fun prep_attn attn = (apsnd o map)
  1.2228 -      (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
  1.2229 -
  1.2230 -    val expr = prep_expr thy raw_expr;
  1.2231 -
  1.2232 -    val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
  1.2233 -    val params_ids = make_params_ids (#1 pts);
  1.2234 -    val raw_params_elemss = make_raw_params_elemss pts;
  1.2235 -    val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr);
  1.2236 -    val ((parms, all_elemss, _), (_, (_, defs, _))) =
  1.2237 -      read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
  1.2238 -
  1.2239 -    (** compute instantiation **)
  1.2240 -
  1.2241 -    (* consistency check: equations need to be stored in a particular locale,
  1.2242 -       therefore if equations are present locale expression must be a name *)
  1.2243 -
  1.2244 -    val _ = case (expr, snd raw_insts) of
  1.2245 -        (Locale _, _) => () | (_, []) => ()
  1.2246 -      | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
  1.2247 -
  1.2248 -    (* read or certify instantiation *)
  1.2249 -    val (raw_insts', raw_eqns) = raw_insts;
  1.2250 -    val (raw_eq_attns, raw_eqns') = split_list raw_eqns;
  1.2251 -    val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns');
  1.2252 -    val eq_attns = map prep_attn raw_eq_attns;
  1.2253 -
  1.2254 -    (* defined params without given instantiation *)
  1.2255 -    val not_given = filter_out (Symtab.defined inst1 o fst) parms;
  1.2256 -    fun add_def (p, pT) inst =
  1.2257 -      let
  1.2258 -        val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  1.2259 -               NONE => error ("Instance missing for parameter " ^ quote p)
  1.2260 -             | SOME (Free (_, T), t) => (t, T);
  1.2261 -        val d = Element.inst_term (instT, inst) t;
  1.2262 -      in Symtab.update_new (p, d) inst end;
  1.2263 -    val inst2 = fold add_def not_given inst1;
  1.2264 -    val inst_morphism = Element.inst_morphism thy (instT, inst2);
  1.2265 -    (* Note: insts contain no vars. *)
  1.2266 -
  1.2267 -    (** compute proof obligations **)
  1.2268 -
  1.2269 -    (* restore "small" ids *)
  1.2270 -    val ids' = map (fn ((n, ps), (_, mode)) =>
  1.2271 -          ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
  1.2272 -        ids;
  1.2273 -    val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
  1.2274 -    (* instantiate ids and elements *)
  1.2275 -    val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  1.2276 -      ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
  1.2277 -        map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
  1.2278 -      |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
  1.2279 -
  1.2280 -    (* equations *)
  1.2281 -    val eqn_elems = if null eqns then []
  1.2282 -      else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
  1.2283 -
  1.2284 -    val propss = map extract_asms_elems inst_elemss @ eqn_elems;
  1.2285 -
  1.2286 -  in
  1.2287 -    (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
  1.2288 -  end;
  1.2289 -
  1.2290 -fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
  1.2291 -  test_global_registration
  1.2292 -  global_activate_facts_elemss mk_ctxt;
  1.2293 -
  1.2294 -fun gen_prep_local_registration mk_ctxt = gen_prep_registration I
  1.2295 -  test_local_registration
  1.2296 -  local_activate_facts_elemss mk_ctxt;
  1.2297 -
  1.2298 -val prep_global_registration = gen_prep_global_registration
  1.2299 -  (K I) (K I) check_instantiations;
  1.2300 -val prep_global_registration_cmd = gen_prep_global_registration
  1.2301 -  Attrib.intern_src intern_expr read_instantiations;
  1.2302 -
  1.2303 -val prep_local_registration = gen_prep_local_registration
  1.2304 -  (K I) (K I) check_instantiations;
  1.2305 -val prep_local_registration_cmd = gen_prep_local_registration
  1.2306 -  Attrib.intern_src intern_expr read_instantiations;
  1.2307 -
  1.2308 -fun prep_registration_in_locale target expr thy =
  1.2309 -  (* target already in internal form *)
  1.2310 -  let
  1.2311 -    val ctxt = ProofContext.init thy;
  1.2312 -    val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
  1.2313 -        (([], Symtab.empty), Expr (Locale target));
  1.2314 -    val fixed = the_locale thy target |> #params |> map #1;
  1.2315 -    val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  1.2316 -        ((raw_target_ids, target_syn), Expr expr);
  1.2317 -    val (target_ids, ids) = chop (length raw_target_ids) all_ids;
  1.2318 -    val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
  1.2319 -
  1.2320 -    (** compute proof obligations **)
  1.2321 -
  1.2322 -    (* restore "small" ids, with mode *)
  1.2323 -    val ids' = map (apsnd snd) ids;
  1.2324 -    (* remove Int markers *)
  1.2325 -    val elemss' = map (fn (_, es) =>
  1.2326 -        map (fn Int e => e) es) elemss
  1.2327 -    (* extract assumptions and defs *)
  1.2328 -    val ids_elemss = ids' ~~ elemss';
  1.2329 -    val propss = map extract_asms_elems ids_elemss;
  1.2330 -
  1.2331 -    (** activation function:
  1.2332 -        - add registrations to the target locale
  1.2333 -        - add induced registrations for all global registrations of
  1.2334 -          the target, unless already present
  1.2335 -        - add facts of induced registrations to theory **)
  1.2336 -
  1.2337 -    fun activate thmss thy =
  1.2338 -      let
  1.2339 -        val satisfy = Element.satisfy_thm (flat thmss);
  1.2340 -        val ids_elemss_thmss = ids_elemss ~~ thmss;
  1.2341 -        val regs = get_global_registrations thy target;
  1.2342 -
  1.2343 -        fun activate_id (((id, Assumed _), _), thms) thy =
  1.2344 -            thy |> put_registration_in_locale target id
  1.2345 -                |> fold (add_witness_in_locale target id) thms
  1.2346 -          | activate_id _ thy = thy;
  1.2347 -
  1.2348 -        fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  1.2349 -          let
  1.2350 -            val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
  1.2351 -            val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts));
  1.2352 -            val disch = Element.satisfy_thm wits;
  1.2353 -            val new_elemss = filter (fn (((name, ps), _), _) =>
  1.2354 -                not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
  1.2355 -            fun activate_assumed_id (((_, Derived _), _), _) thy = thy
  1.2356 -              | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
  1.2357 -                val ps' = inst_parms ps;
  1.2358 -              in
  1.2359 -                if test_global_registration thy (name, ps')
  1.2360 -                then thy
  1.2361 -                else thy
  1.2362 -                  |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  1.2363 -                  |> fold (fn witn => fn thy => add_global_witness (name, ps')
  1.2364 -                     (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
  1.2365 -              end;
  1.2366 -
  1.2367 -            fun activate_derived_id ((_, Assumed _), _) thy = thy
  1.2368 -              | activate_derived_id (((name, ps), Derived ths), _) thy = let
  1.2369 -                val ps' = inst_parms ps;
  1.2370 -              in
  1.2371 -                if test_global_registration thy (name, ps')
  1.2372 -                then thy
  1.2373 -                else thy
  1.2374 -                  |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  1.2375 -                  |> fold (fn witn => fn thy => add_global_witness (name, ps')
  1.2376 -                       (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
  1.2377 -                       (Element.inst_term insts t,
  1.2378 -                        disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
  1.2379 -              end;
  1.2380 -
  1.2381 -            fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
  1.2382 -                let
  1.2383 -                  val att_morphism =
  1.2384 -                    Morphism.binding_morphism (name_morph phi_name param_prfx) $>
  1.2385 -                    Morphism.thm_morphism satisfy $>
  1.2386 -                    Element.inst_morphism thy insts $>
  1.2387 -                    Morphism.thm_morphism disch;
  1.2388 -                  val facts' = facts
  1.2389 -                    |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
  1.2390 -                    |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
  1.2391 -                    |> (map o apfst o apfst) (name_morph phi_name param_prfx);
  1.2392 -                in
  1.2393 -                  thy
  1.2394 -                  |> global_note_qualified kind facts'
  1.2395 -                  |> snd
  1.2396 -                end
  1.2397 -              | activate_elem _ _ thy = thy;
  1.2398 -
  1.2399 -            fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
  1.2400 -
  1.2401 -          in thy |> fold activate_assumed_id ids_elemss_thmss
  1.2402 -                 |> fold activate_derived_id ids_elemss
  1.2403 -                 |> fold activate_elems new_elemss end;
  1.2404 -      in
  1.2405 -        thy |> fold activate_id ids_elemss_thmss
  1.2406 -            |> fold activate_reg regs
  1.2407 -      end;
  1.2408 -
  1.2409 -  in (propss, activate) end;
  1.2410 -
  1.2411 -fun prep_propp propss = propss |> map (fn (_, props) =>
  1.2412 -  map (rpair [] o Element.mark_witness) props);
  1.2413 -
  1.2414 -fun prep_result propps thmss =
  1.2415 -  ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
  1.2416 -
  1.2417 -fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
  1.2418 -  let
  1.2419 -    val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
  1.2420 -    fun after_qed' results =
  1.2421 -      ProofContext.theory (activate (prep_result propss results))
  1.2422 -      #> after_qed;
  1.2423 -  in
  1.2424 -    thy
  1.2425 -    |> ProofContext.init
  1.2426 -    |> Proof.theorem_i NONE after_qed' (prep_propp propss)
  1.2427 -    |> Element.refine_witness
  1.2428 -    |> Seq.hd
  1.2429 -    |> pair morphs
  1.2430 -  end;
  1.2431 -
  1.2432 -fun gen_interpret prep_registration after_qed name_morph expr insts int state =
  1.2433 -  let
  1.2434 -    val _ = Proof.assert_forward_or_chain state;
  1.2435 -    val ctxt = Proof.context_of state;
  1.2436 -    val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts;
  1.2437 -    fun after_qed' results =
  1.2438 -      Proof.map_context (K (ctxt |> activate (prep_result propss results)))
  1.2439 -      #> Proof.put_facts NONE
  1.2440 -      #> after_qed;
  1.2441 -  in
  1.2442 -    state
  1.2443 -    |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  1.2444 -      "interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss))
  1.2445 -    |> Element.refine_witness |> Seq.hd
  1.2446 -    |> pair morphs
  1.2447 -  end;
  1.2448 -
  1.2449 -fun standard_name_morph interp_prfx b =
  1.2450 -  if Binding.is_empty b then b
  1.2451 -  else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
  1.2452 -    fold (Binding.add_prefix false o fst) pprfx
  1.2453 -    #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
  1.2454 -    #> Binding.add_prefix false lprfx
  1.2455 -  ) b;
  1.2456 -
  1.2457 -in
  1.2458 -
  1.2459 -val interpretation = gen_interpretation prep_global_registration;
  1.2460 -fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd
  1.2461 -  I (standard_name_morph interp_prfx);
  1.2462 -
  1.2463 -fun interpretation_in_locale after_qed (raw_target, expr) thy =
  1.2464 -  let
  1.2465 -    val target = intern thy raw_target;
  1.2466 -    val (propss, activate) = prep_registration_in_locale target expr thy;
  1.2467 -    val raw_propp = prep_propp propss;
  1.2468 -
  1.2469 -    val (_, _, goal_ctxt, propp) = thy
  1.2470 -      |> ProofContext.init
  1.2471 -      |> cert_context_statement (SOME target) [] raw_propp;
  1.2472 -
  1.2473 -    fun after_qed' results =
  1.2474 -      ProofContext.theory (activate (prep_result propss results))
  1.2475 -      #> after_qed;
  1.2476 -  in
  1.2477 -    goal_ctxt
  1.2478 -    |> Proof.theorem_i NONE after_qed' propp
  1.2479 -    |> Element.refine_witness |> Seq.hd
  1.2480 -  end;
  1.2481 -
  1.2482 -val interpret = gen_interpret prep_local_registration;
  1.2483 -fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
  1.2484 -  I (standard_name_morph interp_prfx);
  1.2485 -
  1.2486 -end;
  1.2487 -
  1.2488 -end;