src/Pure/Isar/locale.ML

Interpretation in locales: extended back end;
Printing of interpretations: option to show witness theorems;

(*  Title:      Pure/Isar/locale.ML
    ID:         $Id$
    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen

Locales -- Isar proof contexts as meta-level predicates, with local
syntax and implicit structures.

Draws some basic ideas from Florian Kammueller's original version of
locales, but uses the richer infrastructure of Isar instead of the raw
meta-logic.  Furthermore, we provide structured import of contexts
(with merge and rename operations), as well as type-inference of the
signature parts, and predicate definitions of the specification text.

See also:

[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    In Stefano Berardi et al., Types for Proofs and Programs: International
    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
*)

(* TODO:
- beta-eta normalisation of interpretation parameters
- dangling type frees in locales
- test subsumption of interpretations when merging theories
- var vs. fixes in locale to be interpreted (interpretation in locale)
  (implicit locale expressions generated by multiple registrations)
- current finish_global adds unwanted lemmas to theory/locale
*)

signature LOCALE =
sig
  type context
  datatype ('typ, 'term, 'fact) elem =
    Fixes of (string * 'typ option * mixfix option) list |
    Constrains of (string * 'typ) list |
    Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
  datatype expr =
    Locale of string |
    Rename of expr * (string * mixfix option) option list |
    Merge of expr list
  val empty: expr
  datatype 'a elem_expr = Elem of 'a | Expr of expr

  (* Abstract interface to locales *)
  type element
  type element_i
  type locale
  val intern: theory -> xstring -> string
  val extern: theory -> string -> xstring
  val the_locale: theory -> string -> locale
  val intern_attrib_elem: theory ->
    ('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem
  val intern_attrib_elem_expr: theory ->
    ('typ, 'term, 'fact) elem elem_expr -> ('typ, 'term, 'fact) elem elem_expr

  (* Processing of locale statements *)
  val read_context_statement: xstring option -> element elem_expr list ->
    (string * (string list * string list)) list list -> context ->
    string option * (cterm list * cterm list) * context * context * 
      (term * (term list * term list)) list list
  val cert_context_statement: string option -> element_i elem_expr list ->
    (term * (term list * term list)) list list -> context ->
    string option * (cterm list * cterm list) * context * context *
      (term * (term list * term list)) list list

  (* Diagnostic functions *)
  val print_locales: theory -> unit
  val print_locale: theory -> expr -> element list -> unit
  val print_global_registrations: bool -> string -> theory -> unit
  val print_local_registrations': bool -> string -> context -> unit
  val print_local_registrations: bool -> string -> context -> unit

  (* Storing results *)
  val add_locale_context: bool -> bstring -> expr -> element list -> theory
    -> theory * ProofContext.context
  val add_locale_context_i: bool -> bstring -> expr -> element_i list -> theory
    -> theory * ProofContext.context
  val add_locale: bool -> bstring -> expr -> element list -> theory -> theory
  val add_locale_i: bool -> bstring -> expr -> element_i list -> theory -> theory
  val smart_note_thmss: string -> string option ->
    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
    theory -> theory * (bstring * thm list) list
  val note_thmss: string -> xstring ->
    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    theory -> (theory * ProofContext.context) * (bstring * thm list) list
  val note_thmss_i: string -> string ->
    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    theory -> (theory * ProofContext.context) * (bstring * thm list) list
  val add_thmss: string -> string -> ((string * thm list) * Attrib.src list) list ->
    theory * context -> (theory * context) * (string * thm list) list

  (* Locale interpretation *)
  val prep_global_registration:
    string * Attrib.src list -> expr -> string option list -> theory ->
    ((string * term list) * term list) list * (thm list -> theory -> theory)
  val prep_local_registration:
    string * Attrib.src list -> expr -> string option list -> context ->
    ((string * term list) * term list) list * (thm list -> context -> context)
  val prep_registration_in_locale:
    string -> expr -> theory ->
    ((string * string list) * term list) list * (thm list -> theory -> theory)
end;

structure Locale: LOCALE =
struct

(** locale elements and expressions **)

type context = ProofContext.context;

datatype ('typ, 'term, 'fact) elem =
  Fixes of (string * 'typ option * mixfix option) list |
  Constrains of (string * 'typ) list |
  Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
  Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
  Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;

datatype expr =
  Locale of string |
  Rename of expr * (string * mixfix option) option list |
  Merge of expr list;

val empty = Merge [];

datatype 'a elem_expr =
  Elem of 'a | Expr of expr;

type element = (string, string, thmref) elem;
type element_i = (typ, term, thm list) elem;

type locale =
 {predicate: cterm list * thm list,
    (* CB: For locales with "(open)" this entry is ([], []).
       For new-style locales, which declare predicates, if the locale declares
       no predicates, this is also ([], []).
       If the locale declares predicates, the record field is
       ([statement], axioms), where statement is the locale predicate applied
       to the (assumed) locale parameters.  Axioms contains the projections
       from the locale predicate to the normalised assumptions of the locale
       (cf. [1], normalisation of locale expressions.)
    *)
  import: expr,                                       (*dynamic import*)
  elems: (element_i * stamp) list,                    (*static content*)
  params: ((string * typ) * mixfix option) list * string list,
                                                      (*all/local params*)
  regs: ((string * string list) * thm list) list}
    (* Registrations: indentifiers and witness theorems of locales interpreted
       in the locale.
    *)


(* CB: an internal (Int) locale element was either imported or included,
   an external (Ext) element appears directly in the locale text. *)

datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;



(** term and type instantiation, using symbol tables **)
(** functions for term instantiation beta-reduce the result
    unless the instantiation table is empty (inst_tab_term)
    or the instantiation has no effect (inst_tab_thm) **)

(* instantiate TFrees *)

fun tinst_tab_type tinst T = if Symtab.is_empty tinst
      then T
      else Term.map_type_tfree
        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;

fun tinst_tab_term tinst t = if Symtab.is_empty tinst
      then t
      else Term.map_term_types (tinst_tab_type tinst) t;

fun tinst_tab_thm thy tinst thm = if Symtab.is_empty tinst
      then thm
      else let
          val cert = Thm.cterm_of thy;
          val certT = Thm.ctyp_of thy;
          val {hyps, prop, ...} = Thm.rep_thm thm;
          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
          val tinst' = Symtab.dest tinst |>
                List.filter (fn (a, _) => a mem_string tfrees);
        in
          if null tinst' then thm
          else thm |> Drule.implies_intr_list (map cert hyps)
            |> Drule.tvars_intr_list (map #1 tinst')
            |> (fn (th, al) => th |> Thm.instantiate
                ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
                  []))
            |> (fn th => Drule.implies_elim_list th
                 (map (Thm.assume o cert o tinst_tab_term tinst) hyps))
        end;

(* instantiate TFrees and Frees *)

fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
      then tinst_tab_term tinst
      else (* instantiate terms and types simultaneously *)
        let
          fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T)
            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
                 NONE => Free (x, tinst_tab_type tinst T)
               | SOME t => t)
            | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T)
            | instf (b as Bound _) = b
            | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t)
            | instf (s $ t) = instf s $ instf t
        in Envir.beta_norm o instf end;

fun inst_tab_thm thy (inst, tinst) thm = if Symtab.is_empty inst
      then tinst_tab_thm thy tinst thm
      else let
          val cert = Thm.cterm_of thy;
          val certT = Thm.ctyp_of thy;
          val {hyps, prop, ...} = Thm.rep_thm thm;
          (* type instantiations *)
          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
          val tinst' = Symtab.dest tinst |>
                List.filter (fn (a, _) => a mem_string tfrees);
          (* term instantiations;
             note: lhss are type instantiated, because
                   type insts will be done first*)
          val frees = foldr Term.add_term_frees [] (prop :: hyps);
          val inst' = Symtab.dest inst |>
                List.mapPartial (fn (a, t) =>
                  get_first (fn (Free (x, T)) => 
                    if a = x then SOME (Free (x, tinst_tab_type tinst T), t)
                    else NONE) frees);
        in
          if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm
          else thm |> Drule.implies_intr_list (map cert hyps)
            |> Drule.tvars_intr_list (map #1 tinst')
            |> (fn (th, al) => th |> Thm.instantiate
                ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
                  []))
            |> Drule.forall_intr_list (map (cert o #1) inst')
            |> Drule.forall_elim_list (map (cert o #2) inst') 
            |> Drule.fconv_rule (Thm.beta_conversion true)
            |> (fn th => Drule.implies_elim_list th
                 (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps))
        end;


fun inst_tab_att thy (inst as (_, tinst)) =
    Args.map_values I (tinst_tab_type tinst)
    (inst_tab_term inst) (inst_tab_thm thy inst);

fun inst_tab_atts thy inst = map (inst_tab_att thy inst);


(** management of registrations in theories and proof contexts **)

structure Registrations :
  sig
    type T
    val empty: T
    val join: T * T -> T
    val dest: T -> (term list * ((string * Attrib.src list) * thm list)) list
    val lookup: theory -> T * term list ->
      ((string * Attrib.src list) * thm list) option
    val insert: theory -> term list * (string * Attrib.src list) -> T ->
      T * (term list * ((string * Attrib.src list) * thm list)) list
    val add_witness: term list -> thm -> T -> T
  end =
struct
  (* a registration consists of theorems instantiating locale assumptions
     and prefix and attributes, indexed by parameter instantiation *)
  type T = ((string * Attrib.src list) * thm list) Termtab.table;

  val empty = Termtab.empty;

  (* term list represented as single term, for simultaneous matching *)
  fun termify ts =
    Library.foldl (op $) (Const ("", map fastype_of ts ---> propT), ts);
  fun untermify t =
    let fun ut (Const _) ts = ts
          | ut (s $ t) ts = ut s (t::ts)
    in ut t [] end;

  (* joining of registrations: prefix and attributes of left theory,
     thms are equal, no attempt to subsumption testing *)
  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2);

  fun dest regs = map (apfst untermify) (Termtab.dest regs);

  (* registrations that subsume t *)
  fun subsumers tsig t regs =
    List.filter (fn (t', _) => Pattern.matches tsig (t', t)) (Termtab.dest regs);

  (* look up registration, pick one that subsumes the query *)
  fun lookup sign (regs, ts) =
    let
      val tsig = Sign.tsig_of sign;
      val t = termify ts;
      val subs = subsumers tsig t regs;
    in (case subs of
        [] => NONE
      | ((t', (attn, thms)) :: _) => let
            val (tinst, inst) = Pattern.match tsig (t', t);
            (* thms contain Frees, not Vars *)
            val tinst' = tinst |> Vartab.dest
                 |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T))
                 |> Symtab.make;
            val inst' = inst |> Vartab.dest
                 |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t))
                 |> Symtab.make;
          in
            SOME (attn, map (inst_tab_thm sign (inst', tinst')) thms)
          end)
    end;

  (* add registration if not subsumed by ones already present,
     additionally returns registrations that are strictly subsumed *)
  fun insert sign (ts, attn) regs =
    let
      val tsig = Sign.tsig_of sign;
      val t = termify ts;
      val subs = subsumers tsig t regs ;
    in (case subs of
        [] => let
                val sups =
                  List.filter (fn (t', _) => Pattern.matches tsig (t, t')) (Termtab.dest regs);
                val sups' = map (apfst untermify) sups
              in (Termtab.update ((t, (attn, [])), regs), sups') end
      | _ => (regs, []))
    end;

  (* add witness theorem to registration,
     only if instantiation is exact, otherwise exception Option raised *)
  fun add_witness ts thm regs =
    let
      val t = termify ts;
      val (x, thms) = valOf (Termtab.lookup (regs, t));
    in
      Termtab.update ((t, (x, thm::thms)), regs)
    end;
end;


(** theory data **)

structure GlobalLocalesData = TheoryDataFun
(struct
  val name = "Isar/locales";
  type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
    (* 1st entry: locale namespace,
       2nd entry: locales of the theory,
       3rd entry: registrations, indexed by locale name *)

  val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
  val copy = I;
  val extend = I;

  fun join_locs _ ({predicate, import, elems, params, regs}: locale,
      {elems = elems', regs = regs', ...}: locale) =
    SOME {predicate = predicate, import = import,
      elems = gen_merge_lists eq_snd elems elems',
      params = params,
      regs = merge_alists regs regs'};
  fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
    (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
     Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));

  fun print _ (space, locs, _) =
    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
    |> Pretty.writeln;
end);

val _ = Context.add_setup [GlobalLocalesData.init];



(** context data **)

structure LocalLocalesData = ProofDataFun
(struct
  val name = "Isar/locales";
  type T = Registrations.T Symtab.table;
    (* registrations, indexed by locale name *)
  fun init _ = Symtab.empty;
  fun print _ _ = ();
end);

val _ = Context.add_setup [LocalLocalesData.init];


(* access locales *)

val print_locales = GlobalLocalesData.print;

val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
val extern = NameSpace.extern o #1 o GlobalLocalesData.get;

fun declare_locale name thy =
  thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
    (Sign.declare_name thy name space, locs, regs));

fun put_locale name loc =
  GlobalLocalesData.map (fn (space, locs, regs) =>
    (space, Symtab.update ((name, loc), locs), regs));

fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name);

fun the_locale thy name =
  (case get_locale thy name of
    SOME loc => loc
  | NONE => error ("Unknown locale " ^ quote name));


(* access registrations *)

(* Ids of global registrations are varified,
   Ids of local registrations are not.
   Thms of registrations are never varified. *)

(* retrieve registration from theory or context *)

fun gen_get_registrations get thy_ctxt name =
  case Symtab.lookup (get thy_ctxt, name) of
      NONE => []
    | SOME reg => Registrations.dest reg;

val get_global_registrations =
     gen_get_registrations (#3 o GlobalLocalesData.get);
val get_local_registrations =
     gen_get_registrations LocalLocalesData.get;

fun gen_get_registration get thy_of thy_ctxt (name, ps) =
  case Symtab.lookup (get thy_ctxt, name) of
      NONE => NONE
    | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);

val get_global_registration =
     gen_get_registration (#3 o GlobalLocalesData.get) I;
val get_local_registration =
     gen_get_registration LocalLocalesData.get ProofContext.theory_of;

val test_global_registration = isSome oo get_global_registration;
val test_local_registration = isSome oo get_local_registration;
fun smart_test_registration ctxt id =
  let
    val thy = ProofContext.theory_of ctxt;
  in
    test_global_registration thy id orelse test_local_registration ctxt id
  end;


(* add registration to theory or context, ignored if subsumed *)

fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
  map_data (fn regs =>
    let
      val thy = thy_of thy_ctxt;
      val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty);
      val (reg', sups) = Registrations.insert thy (ps, attn) reg;
      val _ = if not (null sups) then warning
                ("Subsumed interpretation(s) of locale " ^
                 quote (extern thy name) ^
                 "\nby interpretation(s) with the following prefix(es):\n" ^
                  commas_quote (map (fn (_, ((s, _), _)) => s) sups))
              else ();
    in Symtab.update ((name, reg'), regs) end) thy_ctxt;

val put_global_registration =
     gen_put_registration (fn f =>
       GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
val put_local_registration =
     gen_put_registration LocalLocalesData.map ProofContext.theory_of;

fun put_registration_in_locale name id thy =
    let
      val {predicate, import, elems, params, regs} = the_locale thy name;
    in
      put_locale name {predicate = predicate, import = import,
        elems = elems, params = params, regs = regs @ [(id, [])]} thy
    end;


(* add witness theorem to registration in theory or context,
   ignored if registration not present *)

fun gen_add_witness map (name, ps) thm =
  map (fn regs =>
      let
        val reg = valOf (Symtab.lookup (regs, name));
      in
        Symtab.update ((name, Registrations.add_witness ps thm reg), regs)
      end handle Option => regs);

val add_global_witness =
     gen_add_witness (fn f =>
       GlobalLocalesData.map (fn (space, locs, regs) =>
         (space, locs, f regs)));
val add_local_witness = gen_add_witness LocalLocalesData.map;

fun add_witness_in_locale name id thm thy =
    let
      val {predicate, import, elems, params, regs} = the_locale thy name;
      fun add (id', thms) =
          if id = id' then (id', thm :: thms) else (id', thms);
    in
      put_locale name {predicate = predicate, import = import,
	elems = elems, params = params, regs = map add regs} thy
    end;

(* import hierarchy
   implementation could be more efficient, eg. by maintaining a database
   of dependencies *)

fun imports thy (upper, lower) =
  let
    fun imps (Locale name) low = (name = low) orelse
      (case get_locale thy name of
           NONE => false
         | SOME {import, ...} => imps import low)
      | imps (Rename (expr, _)) low = imps expr low
      | imps (Merge es) low = exists (fn e => imps e low) es;
  in
    imps (Locale (intern thy upper)) (intern thy lower)
  end;


(* printing of registrations *)

fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
  let
    val ctxt = mk_ctxt thy_ctxt;
    val thy = ProofContext.theory_of ctxt;

    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
    fun prt_inst ts =
        Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
    fun prt_attn (prfx, atts) =
        Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
    val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
    fun prt_thms thms =
        Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms));
    fun prt_reg (ts, (("", []), thms)) =
        if show_wits
          then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms]
          else prt_inst ts
      | prt_reg (ts, (attn, thms)) =
        if show_wits
          then Pretty.block ((prt_attn attn @
            [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
              prt_thms thms]))
          else Pretty.block ((prt_attn attn @
            [Pretty.str ":", Pretty.brk 1, prt_inst ts]));

    val loc_int = intern thy loc;
    val regs = get_regs thy_ctxt;
    val loc_regs = Symtab.lookup (regs, loc_int);
  in
    (case loc_regs of
        NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
      | SOME r => let
            val r' = Registrations.dest r;
            val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
          in Pretty.big_list ("Interpretations in " ^ msg ^ ":")
            (map prt_reg r'')
          end)
    |> Pretty.writeln
  end;

val print_global_registrations =
     gen_print_registrations (#3 o GlobalLocalesData.get)
       ProofContext.init "theory";
val print_local_registrations' =
     gen_print_registrations LocalLocalesData.get
       I "context";
fun print_local_registrations show_wits loc ctxt =
  (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
   print_local_registrations' show_wits loc ctxt);


(* diagnostics *)

fun err_in_locale ctxt msg ids =
  let
    val thy = ProofContext.theory_of ctxt;
    fun prt_id (name, parms) =
      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
    val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
    val err_msg =
      if forall (equal "" o #1) ids then msg
      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
        (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
  in raise ProofContext.CONTEXT (err_msg, ctxt) end;

(* Version for identifiers with axioms *)

fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');


(** primitives **)

(* map elements *)

fun map_elem {name, var, typ, term, fact, attrib} =
  fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
       let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
   | Constrains csts => Constrains (csts |> map (fn (x, T) =>
       let val (x', _) = var (x, SOME Syntax.NoSyn) in (x', typ T) end))
   | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
      ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
        (term t, (map term ps, map term qs))))))
   | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
      ((name a, map attrib atts), (term t, map term ps))))
   | Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
      ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));

fun map_values typ term thm = map_elem
  {name = I, var = I, typ = typ, term = term, fact = map thm,
    attrib = Args.map_values I typ term thm};


(* map attributes *)

fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f};

fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src thy);

fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem)
  | intern_attrib_elem_expr _ (Expr expr) = Expr expr;


(* renaming *)

(* ren maps names to (new) names and syntax; represented as association list *)

fun rename_var ren (x, mx) =
  case assoc_string (ren, x) of
      NONE => (x, mx)
    | SOME (x', NONE) =>
        (x', if mx = NONE then mx else SOME Syntax.NoSyn)     (*drop syntax*)
    | SOME (x', SOME mx') =>
        if mx = NONE then raise ERROR_MESSAGE
          ("Attempt to change syntax of structure parameter " ^ quote x)
        else (x', SOME mx');                                (*change syntax*)

fun rename ren x =
  case assoc_string (ren, x) of
      NONE => x
    | SOME (x', _) => x';                                   (*ignore syntax*)

fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
  | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
  | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
  | rename_term _ a = a;

fun rename_thm ren th =
  let
    val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th;
    val cert = Thm.cterm_of thy;
    val (xs, Ts) = Library.split_list (fold Term.add_frees (prop :: hyps) []);
    val xs' = map (rename ren) xs;
    fun cert_frees names = map (cert o Free) (names ~~ Ts);
    fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts);
  in
    if xs = xs' then th
    else
      th
      |> Drule.implies_intr_list (map cert hyps)
      |> Drule.forall_intr_list (cert_frees xs)
      |> Drule.forall_elim_list (cert_vars xs)
      |> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs')
      |> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps))
  end;

fun rename_elem ren =
  map_values I (rename_term ren) (rename_thm ren) o
  map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};

fun rename_facts prfx =
  map_elem {var = I, typ = I, term = I, fact = I, attrib = I, name = NameSpace.qualified prfx};


(* type instantiation *)

fun inst_type [] T = T
  | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;

fun inst_term [] t = t
  | inst_term env t = Term.map_term_types (inst_type env) t;

fun inst_thm _ [] th = th
  | inst_thm ctxt env th =
      let
        val thy = ProofContext.theory_of ctxt;
        val cert = Thm.cterm_of thy;
        val certT = Thm.ctyp_of thy;
        val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
        val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
        val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;
      in
        if null env' then th
        else
          th
          |> Drule.implies_intr_list (map cert hyps)
          |> Drule.tvars_intr_list (map (#1 o #1) env')
          |> (fn (th', al) => th' |>
            Thm.instantiate ((map (fn ((a, _), T) =>
              (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), []))
          |> (fn th'' => Drule.implies_elim_list th''
              (map (Thm.assume o cert o inst_term env') hyps))
      end;

fun inst_elem ctxt env =
  map_values (inst_type env) (inst_term env) (inst_thm ctxt env);


(* term and type instantiation, variant using symbol tables *)

(* instantiate TFrees *)

fun tinst_tab_elem thy tinst =
  map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm thy tinst);

(* instantiate TFrees and Frees *)

fun inst_tab_elem thy (inst as (_, tinst)) =
  map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm thy inst);

fun inst_tab_elems thy inst ((n, ps), elems) =
      ((n, map (inst_tab_term inst) ps), map (inst_tab_elem thy inst) elems);


(** structured contexts: rename + merge + implicit type instantiation **)

(* parameter types *)

(* CB: frozen_tvars has the following type:
  ProofContext.context -> Term.typ list -> (Term.indexname * (sort * Term.typ)) list *)

fun frozen_tvars ctxt Ts =
  let
    val tvars = rev (fold Term.add_tvarsT Ts []);
    val tfrees = map TFree
      (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
  in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end;

fun unify_frozen ctxt maxidx Ts Us =
  let
    fun paramify (i, NONE) = (i, NONE)
      | paramify (i, SOME T) = apsnd SOME (TypeInfer.paramify_dummies (i, T));

    val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
    val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
    val thy = ProofContext.theory_of ctxt;

    fun unify (env, (SOME T, SOME U)) = (Sign.typ_unify thy (U, T) env
          handle Type.TUNIFY =>
            raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
      | unify (env, _) = env;
    val (unifier, _) = Library.foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us');
    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
  in map (Option.map (Envir.norm_type unifier')) Vs end;

fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));
fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
fun params_syn_of syn elemss =
  gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
    map (apfst (fn x => (x, valOf (Symtab.lookup (syn, x)))));


(* CB: param_types has the following type:
  ('a * 'b option) list -> ('a * 'b) list *)
fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;


fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss
  handle Symtab.DUPS xs => err_in_locale ctxt
    ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);


(* Distinction of assumed vs. derived identifiers.
   The former may have axioms relating assumptions of the context to
   assumptions of the specification fragment (for locales with
   predicates).  The latter have witness theorems relating assumptions of the
   specification fragment to assumptions of other (assumed) specification
   fragments. *)

datatype 'a mode = Assumed of 'a | Derived of 'a;

fun map_mode f (Assumed x) = Assumed (f x)
  | map_mode f (Derived x) = Derived (f x);

(* flatten expressions *)

local

(* CB: OUTDATED unique_parms has the following type:
     'a ->
     (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
     (('b * ('c * 'd) list) * 'e) list  *)

fun unique_parms ctxt elemss =
  let
    val param_decls =
      List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss)
      |> Symtab.make_multi |> Symtab.dest;
  in
    (case find_first (fn (_, ids) => length ids > 1) param_decls of
      SOME (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q)
          (map (apsnd (map fst)) ids)
    | NONE => map (apfst (apfst (apsnd #1))) elemss)
  end;

fun unify_parms ctxt (fixed_parms : (string * typ) list)
  (raw_parmss : (string * typ option) list list) =
  let
    val thy = ProofContext.theory_of ctxt;
    val maxidx = length raw_parmss;
    val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;

    fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
    fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
    val parms = fixed_parms @ List.concat (map varify_parms idx_parmss);

    fun unify T ((env, maxidx), U) =
      Sign.typ_unify thy (U, T) (env, maxidx)
      handle Type.TUNIFY =>
        let val prt = Sign.string_of_typ thy
        in raise TYPE ("unify_parms: failed to unify types " ^
          prt U ^ " and " ^ prt T, [U, T], [])
        end
    fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us)
      | unify_list (envir, []) = envir;
    val (unifier, _) = Library.foldl unify_list
      ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms)));

    val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms);
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));

    fun inst_parms (i, ps) =
      foldr Term.add_typ_tfrees [] (List.mapPartial snd ps)
      |> List.mapPartial (fn (a, S) =>
          let val T = Envir.norm_type unifier' (TVar ((a, i), S))
          in if T = TFree (a, S) then NONE else SOME ((a, S), T) end)
  in map inst_parms idx_parmss end : ((string * Term.sort) * Term.typ) list list;

in

fun unify_elemss _ _ [] = []
  | unify_elemss _ [] [elems] = [elems]
  | unify_elemss ctxt fixed_parms elemss =
      let
        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
        fun inst ((((name, ps), mode), elems), env) =
          (((name, map (apsnd (Option.map (inst_type env))) ps), 
              map_mode (map (inst_thm ctxt env)) mode),
            map (inst_elem ctxt env) elems);
      in map inst (elemss ~~ envs) end;

(* like unify_elemss, but does not touch mode, additional
   parameter c_parms for enforcing further constraints (eg. syntax) *)

fun unify_elemss' _ _ [] [] = []
  | unify_elemss' _ [] [elems] [] = [elems]
  | unify_elemss' ctxt fixed_parms elemss c_parms =
      let
        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss @ map single c_parms);
        fun inst ((((name, ps), (ps', mode)), elems), env) =
          (((name, map (apsnd (Option.map (inst_type env))) ps),
              (ps', mode)),
           map (inst_elem ctxt env) elems);
      in map inst (elemss ~~ (Library.take (length elemss, envs))) end;


(* flatten_expr:
   Extend list of identifiers by those new in locale expression expr.
   Compute corresponding list of lists of locale elements (one entry per
   identifier).

   Identifiers represent locale fragments and are in an extended form:
     ((name, ps), (ax_ps, axs))
   (name, ps) is the locale name with all its parameters.
   (ax_ps, axs) is the locale axioms with its parameters;
     axs are always taken from the top level of the locale hierarchy,
     hence axioms may contain additional parameters from later fragments:
     ps subset of ax_ps.  axs is either singleton or empty.

   Elements are enriched by identifier-like information:
     (((name, ax_ps), axs), elems)
   The parameters in ax_ps are the axiom parameters, but enriched by type
   info: now each entry is a pair of string and typ option.  Axioms are
   type-instantiated.

*)

fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
  let
    val thy = ProofContext.theory_of ctxt;
    (* thy used for retrieval of locale info,
       ctxt for error messages, parameter unification and instantiation
       of axioms *)

    fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
      | renaming (NONE :: xs) (y :: ys) = renaming xs ys
      | renaming [] _ = []
      | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
          commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));

    fun rename_parms top ren ((name, ps), (parms, mode)) =
      let val ps' = map (rename ren) ps in
        (case duplicates ps' of
          [] => ((name, ps'),
                 if top then (map (rename ren) parms,
                   map_mode (map (rename_thm ren)) mode)
                 else (parms, mode))
        | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])
      end;

    (* add registrations of (name, ps), recursively;
       adjust hyps of witness theorems *)

    fun add_regs (name, ps) (ths, ids) =
        let
          val {params, regs, ...} = the_locale thy name;
          val ps' = map #1 (#1 params);
          val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps;
            (* dummy syntax, since required by rename *)
          val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps');
          val [env] = unify_parms ctxt ps [map (apsnd SOME) ps''];
            (* propagate parameter types, to keep them consistent *)
          val regs' = map (fn ((name, ps), ths) =>
              ((name, map (rename ren) ps), ths)) regs;
          val new_regs = gen_rems eq_fst (regs', ids);
          val new_ids = map fst new_regs;
          val new_idTs = map (apsnd (map (fn p => (p, valOf (assoc (ps, p)))))) new_ids;

          val new_ths = map (fn (_, ths') =>
              map (Drule.satisfy_hyps ths o rename_thm ren o inst_thm ctxt env) ths') new_regs;
          val new_ids' = map (fn (id, ths) =>
              (id, ([], Derived ths))) (new_ids ~~ new_ths);
        in
          fold add_regs new_idTs (ths @ List.concat new_ths, ids @ new_ids')
        end;

    (* distribute top-level axioms over assumed ids *)

    fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
        let
          val {elems, ...} = the_locale thy name;
          val ts = List.concat (map
            (fn (Assumes asms, _) => List.concat (map (map #1 o #2) asms)
              | _ => [])
            elems);
          val (axs1, axs2) = splitAt (length ts, axioms);
        in (((name, parms), (all_ps, Assumed axs1)), axs2) end
      | axiomify all_ps (id, (_, Derived ths)) axioms =
          ((id, (all_ps, Derived ths)), axioms);

    (* identifiers of an expression *)

    fun identify top (Locale name) =
    (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
       where name is a locale name, ps a list of parameter names and axs
       a list of axioms relating to the identifier, axs is empty unless
       identify at top level (top = true);
       parms is accumulated list of parameters *)
          let
            val {predicate = (_, axioms), import, params, ...} =
              the_locale thy name;
            val ps = map (#1 o #1) (#1 params);
            val (ids', parms', _) = identify false import;
                (* acyclic import dependencies *)
            val ids'' = ids' @ [((name, ps), ([], Assumed []))];
            val (_, ids''') = add_regs (name, map #1 (#1 params)) ([], ids'');

            val ids_ax = if top then fst
                 (fold_map (axiomify ps) ids''' axioms)
              else ids''';
            val syn = Symtab.make (map (apfst fst) (#1 params));
            in (ids_ax, merge_lists parms' ps, syn) end
      | identify top (Rename (e, xs)) =
          let
            val (ids', parms', syn') = identify top e;
            val ren = renaming xs parms'
              handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';

            val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
            val parms'' = distinct (List.concat (map (#2 o #1) ids''));
            val syn'' = syn' |> Symtab.dest |> map (rename_var ren) |>
                  Symtab.make;
            (* check for conflicting syntax? *)
          in (ids'', parms'', syn'') end
      | identify top (Merge es) =
          fold (fn e => fn (ids, parms, syn) =>
                   let
                     val (ids', parms', syn') = identify top e
                   in
                     (merge_alists ids ids',
                      merge_lists parms parms',
                      merge_syntax ctxt ids' (syn, syn'))
                   end)
            es ([], [], Symtab.empty);


    (* CB: enrich identifiers by parameter types and 
       the corresponding elements (with renamed parameters),
       also takes care of parameter syntax *)

    fun eval syn ((name, xs), axs) =
      let
        val {params = (ps, qs), elems, ...} = the_locale thy name;
        val ps' = map (apsnd SOME o #1) ps;
        val ren = map #1 ps' ~~
              map (fn x => (x, valOf (Symtab.lookup (syn, x)))) xs;
        val (params', elems') =
          if null ren then ((ps', qs), map #1 elems)
          else ((map (apfst (rename ren)) ps', map (rename ren) qs),
            map (rename_elem ren o #1) elems);
        val elems'' = map (rename_facts (space_implode "_" xs)) elems';
      in (((name, params'), axs), elems'') end;

    (* type constraint for renamed parameter with syntax *)
    fun type_syntax NONE = NONE
      | type_syntax (SOME mx) = let
            val Ts = map (fn x => TFree (x, [])) (Term.invent_names [] "'mxa"
              (Syntax.mixfix_args mx + 1))
          in Ts |> Library.split_last |> op ---> |> SOME end;

    (* compute identifiers and syntax, merge with previous ones *)
    val (ids, _, syn) = identify true expr;
    val idents = gen_rems eq_fst (ids, prev_idents);
    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
    (* add types to params, check for unique params and unify them *)
    val raw_elemss = unique_parms ctxt (map (eval syntax) idents);
    val elemss = unify_elemss' ctxt [] raw_elemss
         (map (apsnd type_syntax) (Symtab.dest syntax));
    (* replace params in ids by params from axioms,
       adjust types in mode *)
    val all_params' = params_of' elemss;
    val all_params = param_types all_params';
    val elemss' = map (fn (((name, _), (ps, mode)), elems) =>
         (((name, map (fn p => (p, assoc (all_params, p))) ps), mode), elems))
         elemss;
    fun inst_th th = let
         val {hyps, prop, ...} = Thm.rep_thm th;
         val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
         val [env] = unify_parms ctxt all_params [ps];
         val th' = inst_thm ctxt env th;
       in th' end;
    val final_elemss = map (fn ((id, mode), elems) =>
         ((id, map_mode (map inst_th) mode), elems)) elemss';

  in ((prev_idents @ idents, syntax), final_elemss) end;

end;


(* activate elements *)

local

fun export_axioms axs _ hyps th =
  th |> Drule.satisfy_hyps axs
     (* CB: replace meta-hyps, using axs, by a single meta-hyp. *)
  |> Drule.implies_intr_list (Library.drop (length axs, hyps))
     (* CB: turn remaining hyps into assumptions. *)
  |> Seq.single


(* NB: derived ids contain only facts at this stage *)

fun activate_elem _ ((ctxt, mode), Fixes fixes) =
      ((ctxt |> ProofContext.add_fixes fixes, mode), [])
  | activate_elem _ ((ctxt, mode), Constrains _) =
      ((ctxt, mode), [])
  | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
      let
        val asms' = Attrib.map_specs (Attrib.context_attribute_i ctxt) asms;
        val ts = List.concat (map (map #1 o #2) asms');
        val (ps, qs) = splitAt (length ts, axs);
        val (ctxt', _) =
          ctxt |> ProofContext.fix_frees ts
          |> ProofContext.assume_i (export_axioms ps) asms';
      in ((ctxt', Assumed qs), []) end
  | activate_elem _ ((ctxt, Derived ths), Assumes asms) =
      ((ctxt, Derived ths), [])
  | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
      let
        val defs' = Attrib.map_specs (Attrib.context_attribute_i ctxt) defs;
        val (ctxt', _) =
        ctxt |> ProofContext.assume_i ProofContext.export_def
          (defs' |> map (fn ((name, atts), (t, ps)) =>
            let val (c, t') = ProofContext.cert_def ctxt t
            in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
      in ((ctxt', Assumed axs), []) end
  | activate_elem _ ((ctxt, Derived ths), Defines defs) =
      ((ctxt, Derived ths), [])
  | activate_elem is_ext ((ctxt, mode), Notes facts) =
      let
        val facts' = Attrib.map_facts (Attrib.context_attribute_i ctxt) facts;
        val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts';
      in ((ctxt', mode), if is_ext then res else []) end;

fun activate_elems (((name, ps), mode), elems) ctxt =
  let
    val ((ctxt', _), res) =
        foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
      handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
    val ctxt'' = if name = "" then ctxt'
          else let
              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
              val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
            in case mode of
                   Assumed axs => fold (fn ax => fn ctxt =>
                      add_local_witness (name, ps')
                       (Thm.assume (Thm.cprop_of ax)) ctxt) axs ctxt''
                 | Derived ths => fold (fn th => fn ctxt =>
                     add_local_witness (name, ps') th ctxt) ths ctxt''
            end
  in (ProofContext.restore_naming ctxt ctxt'', res) end;

fun activate_elemss prep_facts =
    fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
      let
        val elems = map (prep_facts ctxt) raw_elems;
        val (ctxt', res) = apsnd List.concat
            (activate_elems (((name, ps), mode), elems) ctxt);
        val elems' = map (map_attrib_elem Args.closure) elems;
      in ((((name, ps), elems'), res), ctxt') end);

in

(* CB: activate_facts prep_facts (ctxt, elemss),
   where elemss is a list of pairs consisting of identifiers and
   context elements, extends ctxt by the context elements yielding
   ctxt' and returns (ctxt', (elemss', facts)).
   Identifiers in the argument are of the form ((name, ps), axs) and
   assumptions use the axioms in the identifiers to set up exporters
   in ctxt'.  elemss' does not contain identifiers and is obtained
   from elemss and the intermediate context with prep_facts.
   If read_facts or cert_facts is used for prep_facts, these also remove
   the internal/external markers from elemss. *)

fun activate_facts prep_facts (ctxt, args) =
    let
      val (res, ctxt') = activate_elemss prep_facts args ctxt;
    in
      (ctxt', apsnd List.concat (split_list res))
    end;

fun activate_note prep_facts (ctxt, args) =
  let
    val (ctxt', ([(_, [Notes args'])], facts)) =
      activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
  in (ctxt', (args', facts)) end;

end;


(* register elements *)

(* not used
fun register_elems (((_, ps), (((name, ax_ps), axs), _)), ctxt) =
  if name = "" then ctxt
      else let val ps' = map (fn (n, SOME T) => Free (n, T)) ax_ps
          val ctxt' = put_local_registration (name, ps') ("", []) ctxt
        in foldl (fn (ax, ctxt) =>
          add_local_witness (name, ps') ax ctxt) ctxt' axs
        end;

fun register_elemss id_elemss ctxt = 
  foldl register_elems ctxt id_elemss;
*)


(** prepare context elements **)

(* expressions *)

fun intern_expr thy (Locale xname) = Locale (intern thy xname)
  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);


(* parameters *)

local

fun prep_parms prep_vars ctxt parms =
  let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T) => ([x], T)) parms))
  in map (fn ([x'], T') => (x', T')) vars end;

in

fun read_parms x = prep_parms ProofContext.read_vars x;
fun cert_parms x = prep_parms ProofContext.cert_vars x;

end;


(* propositions and bindings *)

(* flatten (ctxt, prep_expr) ((ids, syn), expr)
   normalises expr (which is either a locale
   expression or a single context element) wrt.
   to the list ids of already accumulated identifiers.
   It returns (ids', syn', elemss) where ids' is an extension of ids
   with identifiers generated for expr, and elemss is the list of
   context elements generated from expr.
   syn and syn' are symtabs mapping parameter names to their syntax.  syn'
   is an extension of syn.
   For details, see flatten_expr.

   Additionally, for a locale expression, the elems are grouped into a single
   Int; individual context elements are marked Ext.  In this case, the
   identifier-like information of the element is as follows:
   - for Fixes: (("", ps), []) where the ps have type info NONE
   - for other elements: (("", []), []).
   The implementation of activate_facts relies on identifier names being
   empty strings for external elements.
*)

fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
	val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
      in
	((ids',
	 merge_syntax ctxt ids'
	   (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
	   handle Symtab.DUPS xs => err_in_locale ctxt
	     ("Conflicting syntax for parameters: " ^ commas_quote xs)
             (map #1 ids')),
	 [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
      end
  | flatten _ ((ids, syn), Elem elem) =
      ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
      apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));

local

local

fun declare_int_elem (ctxt, Fixes fixes) =
      (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])
  | declare_int_elem (ctxt, _) = (ctxt, []);

fun declare_ext_elem prep_parms (ctxt, Fixes fixes) =
      let
        val parms = map (fn (x, T, _) => (x, T)) fixes;
        val parms' = prep_parms ctxt parms;
        val fixes' = map (fn ((x, T), (_, _, mx)) => (x, T, mx)) (parms' ~~ fixes);
      in (ctxt |> ProofContext.add_fixes fixes', []) end
  | declare_ext_elem prep_parms (ctxt, Constrains csts) =
      let
        val parms = map (fn (x, T) => (x, SOME T)) csts;
        val parms' = prep_parms ctxt parms;
        val ts = map (fn (x, SOME T) => Free (x, T)) parms';
      in (Library.fold ProofContext.declare_term ts ctxt, []) end
  | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
  | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);

fun declare_elems prep_parms (ctxt, (((name, ps), Assumed _), elems)) =
    let val (ctxt', propps) =
      (case elems of
        Int es => foldl_map declare_int_elem (ctxt, es)
      | Ext e => foldl_map (declare_ext_elem prep_parms) (ctxt, [e]))
      handle ProofContext.CONTEXT (msg, ctxt) =>
        err_in_locale ctxt msg [(name, map fst ps)]
    in (ctxt', propps) end
  | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);

in

(* CB: only called by prep_elemss. *)

fun declare_elemss prep_parms fixed_params raw_elemss ctxt =
  let
    (* CB: fix of type bug of goal in target with context elements.
       Parameters new in context elements must receive types that are
       distinct from types of parameters in target (fixed_params).  *)
    val ctxt_with_fixed =
      fold ProofContext.declare_term (map Free fixed_params) ctxt;
    val int_elemss =
      raw_elemss
      |> List.mapPartial (fn (id, Int es) => SOME (id, es) | _ => NONE)
      |> unify_elemss ctxt_with_fixed fixed_params;
    val (_, raw_elemss') =
      foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
        (int_elemss, raw_elemss);
  in foldl_map (declare_elems prep_parms) (ctxt, raw_elemss') end;

end;

local

(* CB: normalise Assumes and Defines wrt. previous definitions *)

val norm_term = Envir.beta_norm oo Term.subst_atomic;


(* CB: following code (abstract_term, abstract_thm, bind_def)
   used in eval_text for Defines elements. *)

fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
  let
    val body = Term.strip_all_body eq;
    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
    val (f, xs) = Term.strip_comb lhs;
    val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
  in (Term.dest_Free f, eq') end;

fun abstract_thm thy eq =
  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;

fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =
  let
    val ((y, T), b) = abstract_term eq;
    val b' = norm_term env b;
    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  in
    conditional (exists (equal y o #1) xs) (fn () =>
      err "Attempt to define previously specified variable");
    conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
      err "Attempt to redefine variable");
    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  end;


(* CB: for finish_elems (Int and Ext),
   extracts specification, only of assumed elements *)

fun eval_text _ _ _ (text, Fixes _) = text
  | eval_text _ _ _ (text, Constrains _) = text
  | eval_text _ (_, Assumed _) is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
      let
        val ts = List.concat (map (map #1 o #2) asms);
        val ts' = map (norm_term env) ts;
        val spec' =
          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
          else ((exts, exts'), (ints @ ts, ints' @ ts'));
      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  | eval_text _ (_, Derived _) _ (text, Assumes _) = text
  | eval_text ctxt (id, Assumed _) _ ((spec, binds), Defines defs) =
      (spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
  | eval_text _ (_, Derived _) _ (text, Defines _) = text
  | eval_text _ _ _ (text, Notes _) = text;


(* for finish_elems (Int),
   remove redundant elements of derived identifiers,
   turn assumptions and definitions into facts,
   adjust hypotheses of facts using witness theorems *)

fun finish_derived _ wits _ (Notes facts) = (Notes facts)
      |> map_values I I (Drule.satisfy_hyps wits) |> SOME;

fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)

  | finish_derived _ _ (Derived _) (Fixes _) = NONE
  | finish_derived _ _ (Derived _) (Constrains _) = NONE
  | finish_derived sign wits (Derived _) (Assumes asms) = asms
      |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
      |> Notes |> map_values I I (Drule.satisfy_hyps wits) |> SOME
  | finish_derived sign wits (Derived _) (Defines defs) = defs
      |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
      |> Notes |> map_values I I (Drule.satisfy_hyps wits) |> SOME

  | finish_derived _ wits _ (Notes facts) = (Notes facts)
      |> map_values I I (Drule.satisfy_hyps wits) |> SOME;

(* CB: for finish_elems (Ext) *)

fun closeup _ false elem = elem
  | closeup ctxt true elem =
      let
        fun close_frees t =
          let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
            (Term.add_frees t []))
          in Term.list_all_free (frees, t) end;

        fun no_binds [] = []
          | no_binds _ =
              raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
      in
        (case elem of
          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
            (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
            (a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps))))
        | e => e)
      end;


fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
      (x, assoc_string (parms, x), mx)) fixes)
  | finish_ext_elem parms _ (Constrains csts, _) =
      Constrains (map (fn (x, _) => (x, valOf (assoc_string (parms, x)))) csts)
  | finish_ext_elem _ close (Assumes asms, propp) =
      close (Assumes (map #1 asms ~~ propp))
  | finish_ext_elem _ close (Defines defs, propp) =
      close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;


(* CB: finish_parms introduces type info from parms to identifiers *)
(* CB: only needed for types that have been NONE so far???
   If so, which are these??? *)

fun finish_parms parms (((name, ps), mode), elems) =
  (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), mode), elems);

fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
      let
        val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
        val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
        val text' = Library.foldl (eval_text ctxt id' false) (text, es);
        val es' = List.mapPartial
              (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
      in ((text', wits'), (id', map Int es')) end
  | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
      let
        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
        val text' = eval_text ctxt id true (text, e');
      in ((text', wits), (id, [Ext e'])) end

in

(* CB: only called by prep_elemss *)

fun finish_elemss ctxt parms do_close =
  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);

end;


(* CB: type inference and consistency checks for locales.

   Works by building a context (through declare_elemss), extracting the
   required information and adjusting the context elements (finish_elemss).
   Can also universally close free vars in assms and defs.  This is only
   needed for Ext elements and controlled by parameter do_close.

   Only elements of assumed identifiers are considered.
*)

fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl =
  let
    (* CB: contexts computed in the course of this function are discarded.
       They are used for type inference and consistency checks only. *)
    (* CB: fixed_params are the parameters (with types) of the target locale,
       empty list if there is no target. *)
    (* CB: raw_elemss are list of pairs consisting of identifiers and
       context elements, the latter marked as internal or external. *)
    val (raw_ctxt, raw_proppss) = declare_elemss prep_parms fixed_params raw_elemss context;
    (* CB: raw_ctxt is context with additional fixed variables derived from
       the fixes elements in raw_elemss,
       raw_proppss contains assumptions and definitions from the
       external elements in raw_elemss. *)
    val raw_propps = map List.concat raw_proppss;
    val raw_propp = List.concat raw_propps;

    (* CB: add type information from fixed_params to context (declare_term) *)
    (* CB: process patterns (conclusion and external elements only) *)
    val (ctxt, all_propp) =
      prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
    (* CB: add type information from conclusion and external elements
       to context *)
    val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;

    (* CB: resolve schematic variables (patterns) in conclusion and external
       elements. *)
    val all_propp' = map2 (op ~~)
      (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
    val (concl, propp) = splitAt(length raw_concl, all_propp');
    val propps = unflat raw_propps propp;
    val proppss = map (uncurry unflat) (raw_proppss ~~ propps);

    (* CB: obtain all parameters from identifier part of raw_elemss *)
    val xs = map #1 (params_of' raw_elemss);
    val typing = unify_frozen ctxt 0
      (map (ProofContext.default_type raw_ctxt) xs)
      (map (ProofContext.default_type ctxt) xs);
    val parms = param_types (xs ~~ typing);
    (* CB: parms are the parameters from raw_elemss, with correct typing. *)

    (* CB: extract information from assumes and defines elements
       (fixes, constrains and notes in raw_elemss don't have an effect on
       text and elemss), compute final form of context elements. *)
    val ((text, _), elemss) = finish_elemss ctxt parms do_close
      ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
    (* CB: text has the following structure:
           (((exts, exts'), (ints, ints')), (xs, env, defs))
       where
         exts: external assumptions (terms in external assumes elements)
         exts': dito, normalised wrt. env
         ints: internal assumptions (terms in internal assumes elements)
         ints': dito, normalised wrt. env
         xs: the free variables in exts' and ints' and rhss of definitions,
           this includes parameters except defined parameters
         env: list of term pairs encoding substitutions, where the first term
           is a free variable; substitutions represent defines elements and
           the rhs is normalised wrt. the previous env
         defs: theorems representing the substitutions from defines elements
           (thms are normalised wrt. env).
       elemss is an updated version of raw_elemss:
         - type info added to Fixes and modified in Constrains
         - axiom and definition statement replaced by corresponding one
           from proppss in Assumes and Defines
         - Facts unchanged
       *)
  in ((parms, elemss, concl), text) end;

in

fun read_elemss x = prep_elemss read_parms ProofContext.read_propp_schematic x;
fun cert_elemss x = prep_elemss cert_parms ProofContext.cert_propp_schematic x;

end;


(* facts and attributes *)

local

fun prep_name ctxt name =
  (* CB: reject qualified theorem names in locale declarations *)
  if NameSpace.is_qualified name then
    raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
  else name;

fun prep_facts _ _ ctxt (Int elem) =
      map_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
  | prep_facts get intern ctxt (Ext elem) = elem |> map_elem
     {var = I, typ = I, term = I,
      name = prep_name ctxt,
      fact = get ctxt,
      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};

in

fun read_facts x = prep_facts ProofContext.get_thms Attrib.intern_src x;
fun cert_facts x = prep_facts (K I) (K I) x;

end;


(* full context statements: import + elements + conclusion *)

local

fun prep_context_statement prep_expr prep_elemss prep_facts
    do_close fixed_params import elements raw_concl context =
  let
    val thy = ProofContext.theory_of context;

    val ((import_ids, import_syn), raw_import_elemss) =
      flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
    (* CB: normalise "includes" among elements *)
    val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
      ((import_ids, import_syn), elements);

    val raw_elemss = List.concat raw_elemsss;
    (* CB: raw_import_elemss @ raw_elemss is the normalised list of
       context elements obtained from import and elements. *)
    val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
      context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
    (* replace extended ids (for axioms) by ids *)
    val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
        (((n, map (fn p => (p, assoc (ps', p) |> valOf)) ps), mode), elems))
      (ids ~~ all_elemss);

    (* CB: all_elemss and parms contain the correct parameter types *)
    val (ps,qs) = splitAt(length raw_import_elemss, all_elemss')
    val (import_ctxt, (import_elemss, _)) =
      activate_facts prep_facts (context, ps);

    val (ctxt, (elemss, _)) =
      activate_facts prep_facts (import_ctxt, qs);
    val stmt = gen_distinct Term.aconv
       (List.concat (map (fn ((_, Assumed axs), _) =>
         List.concat (map (#hyps o Thm.rep_thm) axs)
                           | ((_, Derived _), _) => []) qs));
    val cstmt = map (cterm_of thy) stmt;
  in
    ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl))
  end;

val gen_context = prep_context_statement intern_expr read_elemss read_facts;
val gen_context_i = prep_context_statement (K I) cert_elemss cert_facts;

fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  let
    val thy = ProofContext.theory_of ctxt;
    val locale = Option.map (prep_locale thy) raw_locale;
    val (target_stmt, fixed_params, import) =
      (case locale of NONE => ([], [], empty)
      | SOME name =>
          let val {predicate = (stmt, _), params = (ps, _), ...} =
            the_locale thy name
          in (stmt, map fst ps, Locale name) end);
    val ((((locale_ctxt, locale_elemss), (elems_ctxt, _, _)), _), (elems_stmt, concl')) =
      prep_ctxt false fixed_params import elems concl ctxt;
  in (locale, (target_stmt, elems_stmt), locale_ctxt, elems_ctxt, concl') end;

in

(* CB: processing of locales for add_locale(_i) and print_locale *)
  (* CB: arguments are: x->import, y->body (elements), z->context *)
fun read_context x y z = #1 (gen_context true [] x (map Elem y) [] z);
fun cert_context x y z = #1 (gen_context_i true [] x (map Elem y) [] z);

(* CB: processing of locales for note_thmss(_i),
   Proof.multi_theorem(_i) and antiquotations with option "locale" *)
val read_context_statement = gen_statement intern gen_context;
val cert_context_statement = gen_statement (K I) gen_context_i;

end;


(** define locales **)

(* print locale *)

fun print_locale thy import body =
  let
    val thy_ctxt = ProofContext.init thy;
    val (((_, import_elemss), (ctxt, elemss, _)), _) = read_context import body thy_ctxt;
    val all_elems = List.concat (map #2 (import_elemss @ elemss));

    val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
    val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
    val prt_atts = Args.pretty_attribs ctxt;

    fun prt_syn syn =
      let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx)
      in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
    fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
          prt_typ T :: Pretty.brk 1 :: prt_syn syn)
      | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
    fun prt_cst (x, T) = Pretty.block [Pretty.str (x ^ " ::"), prt_typ T];

    fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name);
    fun prt_name_atts (name, atts) =
      if name = "" andalso null atts then []
      else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str ":"]))];

    fun prt_asm (a, ts) =
      Pretty.block (Pretty.breaks (prt_name_atts a @ map (prt_term o fst) ts));
    fun prt_def (a, (t, _)) =
      Pretty.block (Pretty.breaks (prt_name_atts a @ [prt_term t]));

    fun prt_fact (ths, []) = map prt_thm ths
      | prt_fact (ths, atts) =
          Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: prt_atts atts;
    fun prt_note (a, ths) =
      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a :: map prt_fact ths)));

    fun items _ [] = []
      | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items "  and" xs;
    fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes)
      | prt_elem (Constrains csts) = items "constrains" (map prt_cst csts)
      | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
      | prt_elem (Defines defs) = items "defines" (map prt_def defs)
      | prt_elem (Notes facts) = items "notes" (map prt_note facts);
  in
    Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
    |> Pretty.writeln
  end;



(** store results **)

(* note_thmss_qualified *)

fun note_thmss_qualified kind name args thy =
  thy
  |> Theory.add_path (Sign.base_name name)
  |> Theory.no_base_names
  |> PureThy.note_thmss_i (Drule.kind kind) args
  |>> Theory.restore_naming thy;


(* accesses of interpreted theorems *)

local

(*fully qualified name in theory is T.p.r.n where
  T: theory name, p: interpretation prefix, r: renaming prefix, n: name*)
fun global_accesses _ [] = []
  | global_accesses "" [T, n] = [[T, n], [n]]
  | global_accesses "" [T, r, n] = [[T, r, n], [T, n], [r, n], [n]]
  | global_accesses _ [T, p, n] = [[T, p, n], [p, n]]
  | global_accesses _ [T, p, r, n] = [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
  | global_accesses _ names = error ("Bad name declaration " ^ quote (NameSpace.pack names));

(*fully qualified name in context is p.r.n where
  p: interpretation prefix, r: renaming prefix, n: name*)
fun local_accesses _ [] = []
  | local_accesses "" [n] = [[n]]
  | local_accesses "" [r, n] = [[r, n], [n]]
  | local_accesses _ [p, n] = [[p, n]]
  | local_accesses _ [p, r, n] = [[p, r, n], [p, n]]
  | local_accesses _ names = error ("Bad name declaration " ^ quote (NameSpace.pack names));

in

fun global_note_accesses_i kind prfx args thy =
  thy
  |> Theory.qualified_names
  |> Theory.custom_accesses (global_accesses prfx)
  |> PureThy.note_thmss_i kind args
  |>> Theory.restore_naming thy;

fun local_note_accesses_i prfx args ctxt =
  ctxt
  |> ProofContext.qualified_names
  |> ProofContext.custom_accesses (local_accesses prfx)
  |> ProofContext.note_thmss_i args
  |>> ProofContext.restore_naming ctxt;

end;


(* collect witness theorems for global registration;
   requires parameters and flattened list of (assumed!) identifiers
   instead of recomputing it from the target *)

fun collect_global_witnesses thy parms ids vts = let
    val ts = map Logic.unvarify vts;
    val (parms, parmTs) = split_list parms;
    val parmvTs = map Type.varifyT parmTs;
    val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
    val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
        |> Symtab.make;            
    (* replace parameter names in ids by instantiations *)
    val vinst = Symtab.make (parms ~~ vts);
    fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
    val inst = Symtab.make (parms ~~ ts);
    val ids' = map (apsnd vinst_names) ids;
    val wits = List.concat (map (snd o valOf o get_global_registration thy) ids');
  in ((inst, tinst), wits) end;


(* store instantiations of args for all registered interpretations
   of the theory *)

fun note_thmss_registrations kind target args thy =
  let
    val parms = the_locale thy target |> #params |> fst |> map fst;
    val ids = flatten (ProofContext.init thy, intern_expr thy)
      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
      |> List.mapPartial (fn (id, (_, Assumed _)) => SOME id | _ => NONE)

    val regs = get_global_registrations thy target;

    (* add args to thy for all registrations *)

    fun activate (thy, (vts, ((prfx, atts2), _))) =
      let
        val ((inst, tinst), prems) = collect_global_witnesses thy parms ids vts;
        val args' = map (fn ((n, atts), [(ths, [])]) =>
            ((NameSpace.qualified prfx n,
              map (Attrib.global_attribute_i thy)
                  (inst_tab_atts thy (inst, tinst) atts @ atts2)),
             [(map (Drule.standard o Drule.satisfy_hyps prems o
                inst_tab_thm thy (inst, tinst)) ths, [])]))
          args;
      in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
  in Library.foldl activate (thy, regs) end;


fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
  | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;


local

(* add facts to locale in theory *)

fun put_facts loc args thy =
  let
    val {predicate, import, elems, params, regs} = the_locale thy loc;
    val note = Notes (map (fn ((a, atts), bs) =>
      ((a, atts), map (apfst (map (curry Thm.name_thm a))) bs)) args);
  in
    thy |> put_locale loc {predicate = predicate, import = import,
      elems = elems @ [(note, stamp ())], params = params, regs = regs}
  end;

(* add theorem to locale and theory,
   base for theorems (in loc) and declare (in loc) *)

fun gen_note_thmss prep_locale prep_facts kind raw_loc args thy =
  let
    val thy_ctxt = ProofContext.init thy;
    val loc = prep_locale thy raw_loc;
    val (_, (stmt, _), loc_ctxt, _, _) = cert_context_statement (SOME loc) [] [] thy_ctxt;
    val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;

    val (ctxt', (args', facts)) = activate_note prep_facts (loc_ctxt, args);
    val facts' =
      map (rpair [] o #1 o #1) args' ~~
      map (single o Thm.no_attributes o map export o #2) facts;

    val (thy', result) =
      thy
      |> put_facts loc args'
      |> note_thmss_registrations kind loc args'
      |> note_thmss_qualified kind loc facts';
  in ((thy', ctxt'), result) end;

in

val note_thmss = gen_note_thmss intern read_facts;
val note_thmss_i = gen_note_thmss (K I) cert_facts;

fun add_thmss kind loc args (thy, ctxt) =
  let
    val (ctxt', (args', facts)) = activate_note cert_facts
      (ctxt, args |> map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])));
    val thy' =
      thy
      |> put_facts loc args'
      |> note_thmss_registrations kind loc args';
  in ((thy', ctxt'), facts) end;

end;


(* predicate text *)
(* CB: generate locale predicates and delta predicates *)

local

(* introN: name of theorems for introduction rules of locale and
     delta predicates;
   axiomsN: name of theorem set with destruct rules for locale predicates,
     also name suffix of delta predicates. *)

val introN = "intro";
val axiomsN = "axioms";

fun atomize_spec thy ts =
  let
    val t = foldr1 Logic.mk_conjunction ts;
    val body = ObjectLogic.atomize_term thy t;
    val bodyT = Term.fastype_of body;
  in
    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
    else (body, bodyT, ObjectLogic.atomize_rule thy (Thm.cterm_of thy t))
  end;

fun aprop_tr' n c = (c, fn args =>
  if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
  else raise Match);

(* CB: define one predicate including its intro rule and axioms
   - bname: predicate name
   - parms: locale parameters
   - defs: thms representing substitutions from defines elements
   - ts: terms representing locale assumptions (not normalised wrt. defs)
   - norm_ts: terms representing locale assumptions (normalised wrt. defs)
   - thy: the theory
*)

fun def_pred bname parms defs ts norm_ts thy =
  let
    val name = Sign.full_name thy bname;

    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
    val env = Term.add_term_free_names (body, []);
    val xs = List.filter (fn (x, _) => x mem_string env) parms;
    val Ts = map #2 xs;
    val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
      |> Library.sort_wrt #1 |> map TFree;
    val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;

    val args = map Logic.mk_type extraTs @ map Free xs;
    val head = Term.list_comb (Const (name, predT), args);
    val statement = ObjectLogic.assert_propT thy head;

    val (defs_thy, [pred_def]) =
      thy
      |> (if bodyT <> propT then I else
        Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
      |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
      |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];

    val cert = Thm.cterm_of defs_thy;

    val intro = Drule.standard (Tactic.prove defs_thy [] norm_ts statement (fn _ =>
      Tactic.rewrite_goals_tac [pred_def] THEN
      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
      Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1));

    val conjuncts =
      Drule.equal_elim_rule1 OF [Thm.symmetric body_eq,
        Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
      |> Drule.conj_elim_precise (length ts);
    val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
      Tactic.prove_plain defs_thy [] [] t (fn _ =>
        Tactic.rewrite_goals_tac defs THEN
        Tactic.compose_tac (false, ax, 0) 1));
  in (defs_thy, (statement, intro, axioms)) end;

(* CB: modify the locale elements:
   - assumes elements become notes elements,
   - notes elements are lifted
*)

fun change_elem (axms, Assumes asms) =
      apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
        let val (ps,qs) = splitAt(length spec, axs)
        in (qs, (a, [(ps, [])])) end))
  | change_elem e = e;

(* CB: changes only "new" elems, these have identifier ("", _). *)

fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map
  (fn (axms, (id as ("", _), es)) =>
    foldl_map change_elem (axms, map (map_values I I (Drule.satisfy_hyps axioms)) es)
    |> apsnd (pair id)
  | x => x) |> #2;

in

(* CB: main predicate definition function *)

fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  let
    val (thy', (elemss', more_ts)) =
      if null exts then (thy, (elemss, []))
      else
        let
          val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
          val (def_thy, (statement, intro, axioms)) =
            thy |> def_pred aname parms defs exts exts';
          val elemss' = change_elemss (map (Drule.zero_var_indexes o Drule.gen_all) axioms) elemss @
            [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
        in
          def_thy |> note_thmss_qualified "" aname
            [((introN, []), [([intro], [])])]
          |> #1 |> rpair (elemss', [statement])
        end;
    val (thy'', predicate) =
      if null ints then (thy', ([], []))
      else
        let
          val (def_thy, (statement, intro, axioms)) =
            thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
          val cstatement = Thm.cterm_of def_thy statement;
        in
          def_thy |> note_thmss_qualified "" bname
            [((introN, []), [([intro], [])]),
             ((axiomsN, []), [(map Drule.standard axioms, [])])]
          |> #1 |> rpair ([cstatement], axioms)
        end;
  in (thy'', (elemss', predicate)) end;

end;


(* add_locale(_i) *)

local

fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy =
  (* CB: do_pred controls generation of predicates.
         true -> with, false -> without predicates. *)
  let
    val name = Sign.full_name thy bname;
    val _ = conditional (isSome (get_locale thy name)) (fn () =>
      error ("Duplicate definition of locale " ^ quote name));

    val thy_ctxt = ProofContext.init thy;
    val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text) =
      prep_ctxt raw_import raw_body thy_ctxt;
    val elemss = import_elemss @ body_elemss;
    val import = prep_expr thy raw_import;

    val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
      if do_pred then thy |> define_preds bname text elemss
      else (thy, (elemss, ([], [])));
    val pred_ctxt = ProofContext.init pred_thy;

    fun axiomify axioms elemss = 
      (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
                   val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
                     SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
                   val (axs1, axs2) = splitAt (length ts, axs);
                 in (axs2, ((id, Assumed axs1), elems)) end)
        |> snd;
    val (ctxt, (_, facts)) = activate_facts (K I)
      (pred_ctxt, axiomify predicate_axioms elemss');
    val export = ProofContext.export_standard predicate_statement ctxt pred_ctxt;
    val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  in
    pred_thy
    |> note_thmss_qualified "" name facts' |> #1
    |> declare_locale name
    |> put_locale name {predicate = predicate, import = import,
        elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))),
        params = (params_of elemss' |>
          map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)),
        regs = []}
    |> rpair body_ctxt
  end;

in

val add_locale_context = gen_add_locale read_context intern_expr;
val add_locale_context_i = gen_add_locale cert_context (K I);
fun add_locale b = #1 oooo add_locale_context b;
fun add_locale_i b = #1 oooo add_locale_context_i b;

end;

val _ = Context.add_setup
 [add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]],
  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]];



(** Interpretation commands **)

local

(* extract proof obligations (assms and defs) from elements *)

fun extract_asms_elem (Fixes _) ts = ts
  | extract_asms_elem (Constrains _) ts = ts
  | extract_asms_elem (Assumes asms) ts =
      ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
  | extract_asms_elem (Defines defs) ts =
      ts @ map (fn (_, (def, _)) => def) defs
  | extract_asms_elem (Notes _) ts = ts;

fun extract_asms_elems ((id, Assumed _), elems) =
      (id, fold extract_asms_elem elems [])
  | extract_asms_elems ((id, Derived _), _) = (id, []);

fun extract_asms_elemss elemss = map extract_asms_elems elemss;

(* activate instantiated facts in theory or context *)

fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
        attn all_elemss new_elemss propss result thy_ctxt =
    let
      fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
          let
            val facts' = facts
              (* discharge hyps in attributes *)
              |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch)
              (* insert interpretation attributes *)
              |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
              (* discharge hyps *)
              |> map (apsnd (map (apfst (map disch))))
              (* prefix names *)
              |> map (apfst (apfst (NameSpace.qualified prfx)))
          in fst (note prfx facts' thy_ctxt) end
        | activate_elem _ _ _ thy_ctxt = thy_ctxt;

      fun activate_elems disch ((id, _), elems) thy_ctxt =
          let
            val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
                handle Option => sys_error ("Unknown registration of " ^
                  quote (fst id) ^ " while activating facts.");
          in
            fold (activate_elem disch (prfx, atts2)) elems thy_ctxt
          end;

      val thmss = unflat (map snd propss) result;

      val thy_ctxt' = thy_ctxt
        (* add registrations *)
        |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
        (* add witnesses of Assumed elements *)
        |> fold (fn (id, thms) => fold (add_wit id) thms)
           (map fst propss ~~ thmss);

      val prems = List.concat (List.mapPartial
            (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
              | ((_, Derived _), _) => NONE) all_elemss);
      val disch = Drule.satisfy_hyps prems;
      val disch' = std o Drule.fconv_rule (Thm.beta_conversion true) o disch;

      val thy_ctxt'' = thy_ctxt'
        (* add witnesses of Derived elements *)
        |> fold (fn (id, thms) => fold (add_wit id o disch) thms)
           (List.mapPartial (fn ((_, Assumed _), _) => NONE
              | ((id, Derived thms), _) => SOME (id, thms)) all_elemss)
    in
      thy_ctxt''
        (* add facts to theory or context *)
        |> fold (activate_elems disch') new_elemss
    end;

val global_activate_facts_elemss = gen_activate_facts_elemss
      (fn thy => fn (name, ps) =>
        get_global_registration thy (name, map Logic.varify ps))
      (global_note_accesses_i (Drule.kind ""))
      Attrib.global_attribute_i Drule.standard
      (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
      (fn (n, ps) => fn thm =>
         add_global_witness (n, map Logic.varify ps) (Drule.freeze_all thm));

val local_activate_facts_elemss = gen_activate_facts_elemss
      get_local_registration
      local_note_accesses_i
      Attrib.context_attribute_i I
      put_local_registration
      add_local_witness;

fun gen_prep_registration mk_ctxt is_local read_terms test_reg activate
    attn expr insts thy_ctxt =
  let
    val ctxt = mk_ctxt thy_ctxt;
    val thy = ProofContext.theory_of ctxt;

    val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
    val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
          (([], Symtab.empty), Expr expr);
    val ((parms, all_elemss, _), (_, (_, defs, _))) =
          read_elemss false ctxt' [] raw_elemss [];

    (** compute instantiation **)

    (* user input *)
    val insts = if length parms < length insts
         then error "More arguments than parameters in instantiation."
         else insts @ replicate (length parms - length insts) NONE;
    val (ps, pTs) = split_list parms;
    val pvTs = map Type.varifyT pTs;

    (* instantiations given by user *)
    val given = List.mapPartial (fn (_, (NONE, _)) => NONE
         | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
    val (given_ps, given_insts) = split_list given;
    val tvars = foldr Term.add_typ_tvars [] pvTs;
    val used = foldr Term.add_typ_varnames [] pvTs;
    fun sorts (a, i) = assoc (tvars, (a, i));
    val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
    val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
    val vars' = fold Term.add_term_varnames vs vars;
    val _ = if null vars' then ()
         else error ("Illegal schematic variable(s) in instantiation: " ^
           commas_quote (map Syntax.string_of_vname vars'));
    (* replace new types (which are TFrees) by ones with new names *)
    val new_Tnames = foldr Term.add_term_tfree_names [] vs;
    val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
    val renameT =
          if is_local then I
          else Type.unvarifyT o Term.map_type_tfree (fn (a, s) =>
            TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
    val rename =
          if is_local then I
          else Term.map_term_types renameT;

    val tinst = Symtab.make (map
                (fn ((x, 0), T) => (x, T |> renameT)
                  | ((_, n), _) => sys_error "Internal error var in prep_registration") vinst);
    val inst = Symtab.make (given_ps ~~ map rename vs);

    (* defined params without user input *)
    val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
         | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
    fun add_def ((inst, tinst), (p, pT)) =
      let
        val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
               NONE => error ("Instance missing for parameter " ^ quote p)
             | SOME (Free (_, T), t) => (t, T);
        val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm;
      in (Symtab.update_new ((p, d), inst), tinst) end;
    val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
    (* Note: inst and tinst contain no vars. *)

    (** compute proof obligations **)

    (* restore "small" ids *)
    val ids' = map (fn ((n, ps), (_, mode)) =>
          ((n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps), mode)) ids;
    (* instantiate ids and elements *)
    val inst_elemss = map
          (fn ((id, _), ((_, mode), elems)) =>
             inst_tab_elems thy (inst, tinst) (id, map (fn Int e => e) elems)
               |> apfst (fn id => (id, map_mode (map (inst_tab_thm thy (inst, tinst))) mode))) 
          (ids' ~~ all_elemss);

    (* remove fragments already registered with theory or context *)
    val new_inst_elemss = List.filter (fn ((id, _), _) =>
          not (test_reg thy_ctxt id)) inst_elemss;
    val new_ids = map #1 new_inst_elemss;

    val propss = extract_asms_elemss new_inst_elemss;

    val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
    val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;

  in (propss, activate attn' inst_elemss new_inst_elemss propss) end;

in

val prep_global_registration = gen_prep_registration
     ProofContext.init false
     (fn thy => fn sorts => fn used =>
       Sign.read_def_terms (thy, K NONE, sorts) used true)
     (fn thy => fn (name, ps) =>
       test_global_registration thy (name, map Logic.varify ps))
     global_activate_facts_elemss;

val prep_local_registration = gen_prep_registration
     I true
     (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
     smart_test_registration
     local_activate_facts_elemss;

fun prep_registration_in_locale target expr thy =
  (* target already in internal form *)
  let
    val ctxt = ProofContext.init thy;
    val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
        (([], Symtab.empty), Expr (Locale target));
    val fixed = the_locale thy target |> #params |> #1 |> map #1;
    val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
        ((raw_target_ids, target_syn), Expr expr);
    val (target_ids, ids) = splitAt (length raw_target_ids, all_ids);
    val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];

    (** compute proof obligations **)

    (* restore "small" ids, with mode *)
    val ids' = map (apsnd snd) ids;
    (* remove Int markers *)
    val elemss' = map (fn (_, es) =>
        map (fn Int e => e) es) elemss
    (* extract assumptions and defs *)
    val ids_elemss = ids' ~~ elemss';
    val propss = extract_asms_elemss ids_elemss;

    (** activation function:
        - add registrations to the target locale
        - add induced registrations for all global registrations of
          the target, unless already present
        - add facts of induced registrations to theory **)

    val t_ids = List.mapPartial
        (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;

    fun activate locale_results thy = let
        val ids_elemss_thmss = ids_elemss ~~
	    unflat (map snd propss) locale_results;
        val regs = get_global_registrations thy target;

        fun activate_id (((id, Assumed _), _), thms) thy =
            thy |> put_registration_in_locale target id
                |> fold (add_witness_in_locale target id) thms
          | activate_id _ thy = thy;

        fun activate_reg (vts, ((prfx, atts2), _)) thy = let
            val ((inst, tinst), wits) =
                collect_global_witnesses thy fixed t_ids vts;
            fun inst_parms ps = map (fn p =>
                  valOf (assoc (map #1 fixed ~~ vts, p))) ps;
            val disch = Drule.fconv_rule (Thm.beta_conversion true) o
                Drule.satisfy_hyps wits;
            val new_elemss = List.filter (fn (((name, ps), _), _) =>
                not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
            fun activate_assumed_id (((_, Derived _), _), _) thy = thy
              | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
                val ps' = inst_parms ps;
              in
                if test_global_registration thy (name, ps')
                then thy
                else thy
                  |> put_global_registration (name, ps') (prfx, atts2)
                  |> fold (fn thm => fn thy => add_global_witness (name, ps')
                       ((disch o inst_tab_thm thy (inst, tinst)) thm) thy) thms
              end;

            fun activate_derived_id ((_, Assumed _), _) thy = thy
              | activate_derived_id (((name, ps), Derived ths), _) thy = let
                val ps' = inst_parms ps;
              in
                if test_global_registration thy (name, ps')
                then thy
                else thy
                  |> put_global_registration (name, ps') (prfx, atts2)
                  |> fold (fn thm => fn thy => add_global_witness (name, ps')
                       ((disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results) thm) thy) ths
              end;

            fun activate_elem (Notes facts) thy =
                let
                  val facts' = facts
                      |> Attrib.map_facts (Attrib.global_attribute_i thy o
                         Args.map_values I (tinst_tab_type tinst)
                           (inst_tab_term (inst, tinst))
                           (disch o inst_tab_thm thy (inst, tinst) o
                            Drule.satisfy_hyps locale_results))
                      |> map (apfst (apsnd (fn a => a @ map (Attrib.global_attribute thy) atts2)))
                      |> map (apsnd (map (apfst (map (disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results)))))
                      |> map (apfst (apfst (NameSpace.qualified prfx)))
                in
                  fst (global_note_accesses_i (Drule.kind "") prfx facts' thy)
                end
              | activate_elem _ thy = thy;

            fun activate_elems (_, elems) thy = fold activate_elem elems thy;

          in thy |> fold activate_assumed_id ids_elemss_thmss
                 |> fold activate_derived_id ids_elemss
                 |> fold activate_elems new_elemss end;
      in
        thy |> fold activate_id ids_elemss_thmss
            |> fold activate_reg regs
      end;

  in (propss, activate) end;

end;  (* local *)


end;