wrecked old locale package and related modules
authorhaftmann
Wed Jan 21 16:47:03 2009 +0100 (2009-01-21)
changeset 29576669b560fc2b9
parent 29575 41d604e59e93
child 29577 08f783c5fcf0
wrecked old locale package and related modules
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/old_locale.ML
src/Pure/Isar/theory_target.ML
src/Pure/Tools/ROOT.ML
src/Pure/Tools/invoke.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Jan 21 16:47:02 2009 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Wed Jan 21 16:47:03 2009 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4    Isar/expression.ML Isar/find_theorems.ML Isar/isar.ML			\
     1.5    Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML		\
     1.6    Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
     1.7 -  Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/old_locale.ML	\
     1.8 +  Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
     1.9    Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
    1.10    Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
    1.11    Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
    1.12 @@ -75,7 +75,7 @@
    1.13    Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML	\
    1.14    Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML		\
    1.15    Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML	\
    1.16 -  Thy/thy_syntax.ML Tools/ROOT.ML Tools/invoke.ML			\
    1.17 +  Thy/thy_syntax.ML Tools/ROOT.ML			\
    1.18    Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
    1.19    assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
    1.20    consts.ML context.ML context_position.ML conv.ML defs.ML display.ML	\
     2.1 --- a/src/Pure/Isar/ROOT.ML	Wed Jan 21 16:47:02 2009 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Wed Jan 21 16:47:03 2009 +0100
     2.3 @@ -53,7 +53,6 @@
     2.4  (*local theories and targets*)
     2.5  use "local_theory.ML";
     2.6  use "overloading.ML";
     2.7 -use "old_locale.ML";
     2.8  use "locale.ML";
     2.9  use "class_target.ML";
    2.10  use "theory_target.ML";
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jan 21 16:47:02 2009 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 21 16:47:03 2009 +0100
     3.3 @@ -418,45 +418,6 @@
     3.4          >> (fn expr => Toplevel.print o
     3.5              Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
     3.6  
     3.7 -local
     3.8 -
     3.9 -val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
    3.10 -
    3.11 -in
    3.12 -
    3.13 -val locale_val =
    3.14 -  SpecParse.locale_expr --
    3.15 -    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
    3.16 -  Scan.repeat1 SpecParse.context_element >> pair Old_Locale.empty;
    3.17 -
    3.18 -val _ =
    3.19 -  OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
    3.20 -    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Old_Locale.empty, []) -- P.opt_begin
    3.21 -      >> (fn ((name, (expr, elems)), begin) =>
    3.22 -          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    3.23 -            (Old_Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
    3.24 -
    3.25 -val _ =
    3.26 -  OuterSyntax.command "class_interpretation"
    3.27 -    "prove and register interpretation of locale expression in theory or locale" K.thy_goal
    3.28 -    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
    3.29 -      >> (Toplevel.print oo (Toplevel.theory_to_proof o Old_Locale.interpretation_in_locale I)) ||
    3.30 -      opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
    3.31 -        >> (fn ((name, expr), insts) => Toplevel.print o
    3.32 -            Toplevel.theory_to_proof
    3.33 -              (Old_Locale.interpretation_cmd (Binding.base_name name) expr insts)));
    3.34 -
    3.35 -val _ =
    3.36 -  OuterSyntax.command "class_interpret"
    3.37 -    "prove and register interpretation of locale expression in proof context"
    3.38 -    (K.tag_proof K.prf_goal)
    3.39 -    (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
    3.40 -      >> (fn ((name, expr), insts) => Toplevel.print o
    3.41 -          Toplevel.proof'
    3.42 -            (fn int => Old_Locale.interpret_cmd (Binding.base_name name) expr insts int)));
    3.43 -
    3.44 -end;
    3.45 -
    3.46  
    3.47  (* classes *)
    3.48  
    3.49 @@ -857,12 +818,6 @@
    3.50      (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
    3.51  
    3.52  val _ =
    3.53 -  OuterSyntax.improper_command "print_interps"
    3.54 -    "print interpretations of named locale" K.diag
    3.55 -    (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
    3.56 -      >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
    3.57 -
    3.58 -val _ =
    3.59    OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
    3.60      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
    3.61  
     4.1 --- a/src/Pure/Isar/locale.ML	Wed Jan 21 16:47:02 2009 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Wed Jan 21 16:47:03 2009 +0100
     4.3 @@ -29,23 +29,18 @@
     4.4  
     4.5  signature LOCALE =
     4.6  sig
     4.7 -  type locale
     4.8 -
     4.9 +  (* Locale specification *)
    4.10    val register_locale: bstring ->
    4.11 -    (string * sort) list * (Binding.T * typ option * mixfix) list ->
    4.12 +    (string * sort) list * (binding * typ option * mixfix) list ->
    4.13      term option * term list ->
    4.14      thm option * thm option -> thm list ->
    4.15      (declaration * stamp) list * (declaration * stamp) list ->
    4.16      ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
    4.17      ((string * morphism) * stamp) list -> theory -> theory
    4.18 -
    4.19 -  (* Locale name space *)
    4.20    val intern: theory -> xstring -> string
    4.21    val extern: theory -> string -> xstring
    4.22 -
    4.23 -  (* Specification *)
    4.24    val defined: theory -> string -> bool
    4.25 -  val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
    4.26 +  val params_of: theory -> string -> (binding * typ option * mixfix) list
    4.27    val intros_of: theory -> string -> thm option * thm option
    4.28    val axioms_of: theory -> string -> thm list
    4.29    val instance_of: theory -> string -> morphism -> term list
    4.30 @@ -112,13 +107,25 @@
    4.31  
    4.32  datatype ctxt = datatype Element.ctxt;
    4.33  
    4.34 +fun global_note_qualified kind facts thy = (*FIXME*)
    4.35 +  thy
    4.36 +  |> Sign.qualified_names
    4.37 +  |> PureThy.note_thmss kind facts
    4.38 +  ||> Sign.restore_naming thy;
    4.39 +
    4.40 +fun local_note_qualified kind facts ctxt = (*FIXME*)
    4.41 +  ctxt
    4.42 +  |> ProofContext.qualified_names
    4.43 +  |> ProofContext.note_thmss_i kind facts
    4.44 +  ||> ProofContext.restore_naming ctxt;
    4.45 +
    4.46  
    4.47  
    4.48  (*** Theory data ***)
    4.49  
    4.50  datatype locale = Loc of {
    4.51    (** static part **)
    4.52 -  parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
    4.53 +  parameters: (string * sort) list * (binding * typ option * mixfix) list,
    4.54      (* type and term parameters *)
    4.55    spec: term option * term list,
    4.56      (* assumptions (as a single predicate expression) and defines *)
    4.57 @@ -330,7 +337,7 @@
    4.58  fun init_global_elem (Notes (kind, facts)) thy =
    4.59    let
    4.60      val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    4.61 -  in Old_Locale.global_note_qualified kind facts' thy |> snd end
    4.62 +  in global_note_qualified kind facts' thy |> snd end
    4.63  
    4.64  fun init_local_elem (Fixes fixes) ctxt = ctxt |>
    4.65        ProofContext.add_fixes_i fixes |> snd
    4.66 @@ -352,7 +359,7 @@
    4.67    | init_local_elem (Notes (kind, facts)) ctxt =
    4.68        let
    4.69          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
    4.70 -      in Old_Locale.local_note_qualified kind facts' ctxt |> snd end
    4.71 +      in local_note_qualified kind facts' ctxt |> snd end
    4.72  
    4.73  fun cons_elem false (Notes notes) elems = elems
    4.74    | cons_elem _ elem elems = elem :: elems
    4.75 @@ -445,7 +452,7 @@
    4.76              let
    4.77                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
    4.78                  Attrib.map_facts (Attrib.attribute_i thy)
    4.79 -            in Old_Locale.global_note_qualified kind args'' #> snd end)
    4.80 +            in global_note_qualified kind args'' #> snd end)
    4.81          (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
    4.82    in ctxt'' end;
    4.83  
    4.84 @@ -496,12 +503,10 @@
    4.85  val _ = Context.>> (Context.map_theory
    4.86    (Method.add_methods
    4.87      [("intro_locales",
    4.88 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE'
    4.89 -        Old_Locale.intro_locales_tac false ctxt)),
    4.90 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    4.91        "back-chain introduction rules of locales without unfolding predicates"),
    4.92       ("unfold_locales",
    4.93 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE'
    4.94 -        Old_Locale.intro_locales_tac true ctxt)),
    4.95 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    4.96        "back-chain all introduction rules of locales")]));
    4.97  
    4.98  end;
     5.1 --- a/src/Pure/Isar/old_locale.ML	Wed Jan 21 16:47:02 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,2485 +0,0 @@
     5.4 -(*  Title:      Pure/Isar/locale.ML
     5.5 -    Author:     Clemens Ballarin, TU Muenchen
     5.6 -    Author:     Markus Wenzel, LMU/TU Muenchen
     5.7 -
     5.8 -Locales -- Isar proof contexts as meta-level predicates, with local
     5.9 -syntax and implicit structures.
    5.10 -
    5.11 -Draws basic ideas from Florian Kammueller's original version of
    5.12 -locales, but uses the richer infrastructure of Isar instead of the raw
    5.13 -meta-logic.  Furthermore, structured import of contexts (with merge
    5.14 -and rename operations) are provided, as well as type-inference of the
    5.15 -signature parts, and predicate definitions of the specification text.
    5.16 -
    5.17 -Interpretation enables the reuse of theorems of locales in other
    5.18 -contexts, namely those defined by theories, structured proofs and
    5.19 -locales themselves.
    5.20 -
    5.21 -See also:
    5.22 -
    5.23 -[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    5.24 -    In Stefano Berardi et al., Types for Proofs and Programs: International
    5.25 -    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    5.26 -[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    5.27 -    Dependencies between Locales. Technical Report TUM-I0607, Technische
    5.28 -    Universitaet Muenchen, 2006.
    5.29 -[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    5.30 -    Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    5.31 -    pages 31-43, 2006.
    5.32 -*)
    5.33 -
    5.34 -(* TODO:
    5.35 -- beta-eta normalisation of interpretation parameters
    5.36 -- dangling type frees in locales
    5.37 -- test subsumption of interpretations when merging theories
    5.38 -*)
    5.39 -
    5.40 -signature OLD_LOCALE =
    5.41 -sig
    5.42 -  datatype expr =
    5.43 -    Locale of string |
    5.44 -    Rename of expr * (string * mixfix option) option list |
    5.45 -    Merge of expr list
    5.46 -  val empty: expr
    5.47 -
    5.48 -  val intern: theory -> xstring -> string
    5.49 -  val intern_expr: theory -> expr -> expr
    5.50 -  val extern: theory -> string -> xstring
    5.51 -  val init: string -> theory -> Proof.context
    5.52 -
    5.53 -  (* The specification of a locale *)
    5.54 -  val parameters_of: theory -> string -> ((string * typ) * mixfix) list
    5.55 -  val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
    5.56 -  val local_asms_of: theory -> string -> (Attrib.binding * term list) list
    5.57 -  val global_asms_of: theory -> string -> (Attrib.binding * term list) list
    5.58 -
    5.59 -  (* Theorems *)
    5.60 -  val intros: theory -> string -> thm list * thm list
    5.61 -  val dests: theory -> string -> thm list
    5.62 -  (* Not part of the official interface.  DO NOT USE *)
    5.63 -  val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
    5.64 -
    5.65 -  (* Not part of the official interface.  DO NOT USE *)
    5.66 -  val declarations_of: theory -> string -> declaration list * declaration list;
    5.67 -
    5.68 -  (* Processing of locale statements *)
    5.69 -  val read_context_statement: string option -> Element.context list ->
    5.70 -    (string * string list) list list -> Proof.context ->
    5.71 -    string option * Proof.context * Proof.context * (term * term list) list list
    5.72 -  val read_context_statement_cmd: xstring option -> Element.context list ->
    5.73 -    (string * string list) list list -> Proof.context ->
    5.74 -    string option * Proof.context * Proof.context * (term * term list) list list
    5.75 -  val cert_context_statement: string option -> Element.context_i list ->
    5.76 -    (term * term list) list list -> Proof.context ->
    5.77 -    string option * Proof.context * Proof.context * (term * term list) list list
    5.78 -  val read_expr: expr -> Element.context list -> Proof.context ->
    5.79 -    Element.context_i list * Proof.context
    5.80 -  val cert_expr: expr -> Element.context_i list -> Proof.context ->
    5.81 -    Element.context_i list * Proof.context
    5.82 -
    5.83 -  (* Diagnostic functions *)
    5.84 -  val print_locales: theory -> unit
    5.85 -  val print_locale: theory -> bool -> expr -> Element.context list -> unit
    5.86 -  val print_registrations: bool -> string -> Proof.context -> unit
    5.87 -
    5.88 -  val add_locale: string -> bstring -> expr -> Element.context_i list -> theory
    5.89 -    -> string * Proof.context
    5.90 -  val add_locale_cmd: bstring -> expr -> Element.context list -> theory
    5.91 -    -> string * Proof.context
    5.92 -
    5.93 -  (* Tactics *)
    5.94 -  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    5.95 -
    5.96 -  (* Storing results *)
    5.97 -  val global_note_qualified: string ->
    5.98 -    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
    5.99 -    theory -> (string * thm list) list * theory
   5.100 -  val local_note_qualified: string ->
   5.101 -    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
   5.102 -    Proof.context -> (string * thm list) list * Proof.context
   5.103 -  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   5.104 -    Proof.context -> Proof.context
   5.105 -  val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   5.106 -  val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   5.107 -  val add_declaration: string -> declaration -> Proof.context -> Proof.context
   5.108 -
   5.109 -  (* Interpretation *)
   5.110 -  val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string ->
   5.111 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   5.112 -    string -> term list -> Morphism.morphism
   5.113 -  val interpretation: (Proof.context -> Proof.context) ->
   5.114 -    (Binding.T -> Binding.T) -> expr ->
   5.115 -    term option list * (Attrib.binding * term) list ->
   5.116 -    theory ->
   5.117 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   5.118 -  val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   5.119 -    theory -> Proof.state
   5.120 -  val interpretation_in_locale: (Proof.context -> Proof.context) ->
   5.121 -    xstring * expr -> theory -> Proof.state
   5.122 -  val interpret: (Proof.state -> Proof.state) ->
   5.123 -    (Binding.T -> Binding.T) -> expr ->
   5.124 -    term option list * (Attrib.binding * term) list ->
   5.125 -    bool -> Proof.state ->
   5.126 -    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   5.127 -  val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
   5.128 -    bool -> Proof.state -> Proof.state
   5.129 -end;
   5.130 -
   5.131 -structure Old_Locale: OLD_LOCALE =
   5.132 -struct
   5.133 -
   5.134 -(* legacy operations *)
   5.135 -
   5.136 -fun merge_lists _ xs [] = xs
   5.137 -  | merge_lists _ [] ys = ys
   5.138 -  | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   5.139 -
   5.140 -fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
   5.141 -
   5.142 -
   5.143 -(* auxiliary: noting name bindings with qualified base names *)
   5.144 -
   5.145 -fun global_note_qualified kind facts thy =
   5.146 -  thy
   5.147 -  |> Sign.qualified_names
   5.148 -  |> PureThy.note_thmss kind facts
   5.149 -  ||> Sign.restore_naming thy;
   5.150 -
   5.151 -fun local_note_qualified kind facts ctxt =
   5.152 -  ctxt
   5.153 -  |> ProofContext.qualified_names
   5.154 -  |> ProofContext.note_thmss_i kind facts
   5.155 -  ||> ProofContext.restore_naming ctxt;
   5.156 -
   5.157 -
   5.158 -(** locale elements and expressions **)
   5.159 -
   5.160 -datatype ctxt = datatype Element.ctxt;
   5.161 -
   5.162 -datatype expr =
   5.163 -  Locale of string |
   5.164 -  Rename of expr * (string * mixfix option) option list |
   5.165 -  Merge of expr list;
   5.166 -
   5.167 -val empty = Merge [];
   5.168 -
   5.169 -datatype 'a element =
   5.170 -  Elem of 'a | Expr of expr;
   5.171 -
   5.172 -fun map_elem f (Elem e) = Elem (f e)
   5.173 -  | map_elem _ (Expr e) = Expr e;
   5.174 -
   5.175 -type decl = declaration * stamp;
   5.176 -
   5.177 -type locale =
   5.178 - {axiom: Element.witness list,
   5.179 -    (* For locales that define predicates this is [A [A]], where A is the locale
   5.180 -       specification.  Otherwise [].
   5.181 -       Only required to generate the right witnesses for locales with predicates. *)
   5.182 -  elems: (Element.context_i * stamp) list,
   5.183 -    (* Static content, neither Fixes nor Constrains elements *)
   5.184 -  params: ((string * typ) * mixfix) list,                        (*all term params*)
   5.185 -  decls: decl list * decl list,                    (*type/term_syntax declarations*)
   5.186 -  regs: ((string * string list) * Element.witness list) list,
   5.187 -    (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
   5.188 -  intros: thm list * thm list,
   5.189 -    (* Introduction rules: of delta predicate and locale predicate. *)
   5.190 -  dests: thm list}
   5.191 -    (* Destruction rules: projections from locale predicate to predicates of fragments. *)
   5.192 -
   5.193 -(* CB: an internal (Int) locale element was either imported or included,
   5.194 -   an external (Ext) element appears directly in the locale text. *)
   5.195 -
   5.196 -datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   5.197 -
   5.198 -
   5.199 -
   5.200 -(** substitutions on Vars -- clone from element.ML **)
   5.201 -
   5.202 -(* instantiate types *)
   5.203 -
   5.204 -fun var_instT_type env =
   5.205 -  if Vartab.is_empty env then I
   5.206 -  else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x));
   5.207 -
   5.208 -fun var_instT_term env =
   5.209 -  if Vartab.is_empty env then I
   5.210 -  else Term.map_types (var_instT_type env);
   5.211 -
   5.212 -fun var_inst_term (envT, env) =
   5.213 -  if Vartab.is_empty env then var_instT_term envT
   5.214 -  else
   5.215 -    let
   5.216 -      val instT = var_instT_type envT;
   5.217 -      fun inst (Const (x, T)) = Const (x, instT T)
   5.218 -        | inst (Free (x, T)) = Free(x, instT T)
   5.219 -        | inst (Var (xi, T)) =
   5.220 -            (case Vartab.lookup env xi of
   5.221 -              NONE => Var (xi, instT T)
   5.222 -            | SOME t => t)
   5.223 -        | inst (b as Bound _) = b
   5.224 -        | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
   5.225 -        | inst (t $ u) = inst t $ inst u;
   5.226 -    in Envir.beta_norm o inst end;
   5.227 -
   5.228 -
   5.229 -(** management of registrations in theories and proof contexts **)
   5.230 -
   5.231 -type registration =
   5.232 -  {prfx: (Binding.T -> Binding.T) * (string * string),
   5.233 -      (* first component: interpretation name morphism;
   5.234 -         second component: parameter prefix *)
   5.235 -    exp: Morphism.morphism,
   5.236 -      (* maps content to its originating context *)
   5.237 -    imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
   5.238 -      (* inverse of exp *)
   5.239 -    wits: Element.witness list,
   5.240 -      (* witnesses of the registration *)
   5.241 -    eqns: thm Termtab.table,
   5.242 -      (* theorems (equations) interpreting derived concepts and indexed by lhs *)
   5.243 -    morph: unit
   5.244 -      (* interpreting morphism *)
   5.245 -  }
   5.246 -
   5.247 -structure Registrations :
   5.248 -  sig
   5.249 -    type T
   5.250 -    val empty: T
   5.251 -    val join: T * T -> T
   5.252 -    val dest: theory -> T ->
   5.253 -      (term list *
   5.254 -        (((Binding.T -> Binding.T) * (string * string)) *
   5.255 -         (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
   5.256 -         Element.witness list *
   5.257 -         thm Termtab.table)) list
   5.258 -    val test: theory -> T * term list -> bool
   5.259 -    val lookup: theory ->
   5.260 -      T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   5.261 -      (((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option
   5.262 -    val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) ->
   5.263 -      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   5.264 -      T ->
   5.265 -      T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list
   5.266 -    val add_witness: term list -> Element.witness -> T -> T
   5.267 -    val add_equation: term list -> thm -> T -> T
   5.268 -(*
   5.269 -    val update_morph: term list -> Morphism.morphism -> T -> T
   5.270 -    val get_morph: theory -> T ->
   5.271 -      term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
   5.272 -      Morphism.morphism
   5.273 -*)
   5.274 -  end =
   5.275 -struct
   5.276 -  (* A registration is indexed by parameter instantiation.
   5.277 -     NB: index is exported whereas content is internalised. *)
   5.278 -  type T = registration Termtab.table;
   5.279 -
   5.280 -  fun mk_reg prfx exp imp wits eqns morph =
   5.281 -    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph};
   5.282 -
   5.283 -  fun map_reg f reg =
   5.284 -    let
   5.285 -      val {prfx, exp, imp, wits, eqns, morph} = reg;
   5.286 -      val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph);
   5.287 -    in mk_reg prfx' exp' imp' wits' eqns' morph' end;
   5.288 -
   5.289 -  val empty = Termtab.empty;
   5.290 -
   5.291 -  (* term list represented as single term, for simultaneous matching *)
   5.292 -  fun termify ts =
   5.293 -    Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
   5.294 -  fun untermify t =
   5.295 -    let fun ut (Const _) ts = ts
   5.296 -          | ut (s $ t) ts = ut s (t::ts)
   5.297 -    in ut t [] end;
   5.298 -
   5.299 -  (* joining of registrations:
   5.300 -     - prefix and morphisms of right theory;
   5.301 -     - witnesses are equal, no attempt to subsumption testing;
   5.302 -     - union of equalities, if conflicting (i.e. two eqns with equal lhs)
   5.303 -       eqn of right theory takes precedence *)
   5.304 -  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) =>
   5.305 -      mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2);
   5.306 -
   5.307 -  fun dest_transfer thy regs =
   5.308 -    Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) =>
   5.309 -      (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m))));
   5.310 -
   5.311 -  fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
   5.312 -    map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns)));
   5.313 -
   5.314 -  (* registrations that subsume t *)
   5.315 -  fun subsumers thy t regs =
   5.316 -    filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
   5.317 -
   5.318 -  (* test if registration that subsumes the query is present *)
   5.319 -  fun test thy (regs, ts) =
   5.320 -    not (null (subsumers thy (termify ts) regs));
   5.321 -      
   5.322 -  (* look up registration, pick one that subsumes the query *)
   5.323 -  fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) =
   5.324 -    let
   5.325 -      val t = termify ts;
   5.326 -      val subs = subsumers thy t regs;
   5.327 -    in
   5.328 -      (case subs of
   5.329 -        [] => NONE
   5.330 -        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) =>
   5.331 -          let
   5.332 -            val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   5.333 -            val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
   5.334 -                (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst
   5.335 -                      |> var_instT_type impT)) |> Symtab.make;
   5.336 -            val inst' = dom' |> map (fn (t as Free (x, _)) =>
   5.337 -                (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
   5.338 -                      |> var_inst_term (impT, imp))) |> Symtab.make;
   5.339 -            val inst'_morph = Element.inst_morphism thy (tinst', inst');
   5.340 -          in SOME (prfx,
   5.341 -            map (Element.morph_witness inst'_morph) wits,
   5.342 -            Termtab.map (Morphism.thm inst'_morph) eqns)
   5.343 -          end)
   5.344 -    end;
   5.345 -
   5.346 -  (* add registration if not subsumed by ones already present,
   5.347 -     additionally returns registrations that are strictly subsumed *)
   5.348 -  fun insert thy ts prfx (exp, imp) regs =
   5.349 -    let
   5.350 -      val t = termify ts;
   5.351 -      val subs = subsumers thy t regs ;
   5.352 -    in (case subs of
   5.353 -        [] => let
   5.354 -                val sups =
   5.355 -                  filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   5.356 -                val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
   5.357 -              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end
   5.358 -      | _ => (regs, []))
   5.359 -    end;
   5.360 -
   5.361 -  fun gen_add f ts regs =
   5.362 -    let
   5.363 -      val t = termify ts;
   5.364 -    in
   5.365 -      Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs
   5.366 -    end;
   5.367 -
   5.368 -  (* add witness theorem to registration,
   5.369 -     only if instantiation is exact, otherwise exception Option raised *)
   5.370 -  fun add_witness ts wit regs =
   5.371 -    gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m))
   5.372 -      ts regs;
   5.373 -
   5.374 -  (* add equation to registration, replaces previous equation with same lhs;
   5.375 -     only if instantiation is exact, otherwise exception Option raised;
   5.376 -     exception TERM raised if not a meta equality *)
   5.377 -  fun add_equation ts thm regs =
   5.378 -    gen_add (fn (x, e, i, thms, eqns, m) =>
   5.379 -      (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
   5.380 -      ts regs;
   5.381 -
   5.382 -end;
   5.383 -
   5.384 -
   5.385 -(** theory data : locales **)
   5.386 -
   5.387 -structure LocalesData = TheoryDataFun
   5.388 -(
   5.389 -  type T = NameSpace.T * locale Symtab.table;
   5.390 -    (* 1st entry: locale namespace,
   5.391 -       2nd entry: locales of the theory *)
   5.392 -
   5.393 -  val empty = NameSpace.empty_table;
   5.394 -  val copy = I;
   5.395 -  val extend = I;
   5.396 -
   5.397 -  fun join_locales _
   5.398 -    ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,
   5.399 -      {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
   5.400 -     {axiom = axiom,
   5.401 -      elems = merge_lists (eq_snd (op =)) elems elems',
   5.402 -      params = params,
   5.403 -      decls =
   5.404 -       (Library.merge (eq_snd (op =)) (decls1, decls1'),
   5.405 -        Library.merge (eq_snd (op =)) (decls2, decls2')),
   5.406 -      regs = merge_alists (op =) regs regs',
   5.407 -      intros = intros,
   5.408 -      dests = dests};
   5.409 -  fun merge _ = NameSpace.join_tables join_locales;
   5.410 -);
   5.411 -
   5.412 -
   5.413 -
   5.414 -(** context data : registrations **)
   5.415 -
   5.416 -structure RegistrationsData = GenericDataFun
   5.417 -(
   5.418 -  type T = Registrations.T Symtab.table;  (*registrations, indexed by locale name*)
   5.419 -  val empty = Symtab.empty;
   5.420 -  val extend = I;
   5.421 -  fun merge _ = Symtab.join (K Registrations.join);
   5.422 -);
   5.423 -
   5.424 -
   5.425 -(** access locales **)
   5.426 -
   5.427 -val intern = NameSpace.intern o #1 o LocalesData.get;
   5.428 -val extern = NameSpace.extern o #1 o LocalesData.get;
   5.429 -
   5.430 -fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   5.431 -
   5.432 -fun the_locale thy name = case get_locale thy name
   5.433 - of SOME loc => loc
   5.434 -  | NONE => error ("Unknown locale " ^ quote name);
   5.435 -
   5.436 -fun register_locale bname loc thy =
   5.437 -  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy)
   5.438 -    (Binding.name bname, loc) #> snd);
   5.439 -
   5.440 -fun change_locale name f thy =
   5.441 -  let
   5.442 -    val {axiom, elems, params, decls, regs, intros, dests} =
   5.443 -        the_locale thy name;
   5.444 -    val (axiom', elems', params', decls', regs', intros', dests') =
   5.445 -      f (axiom, elems, params, decls, regs, intros, dests);
   5.446 -  in
   5.447 -    thy
   5.448 -    |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
   5.449 -          elems = elems', params = params',
   5.450 -          decls = decls', regs = regs', intros = intros', dests = dests'}))
   5.451 -  end;
   5.452 -
   5.453 -fun print_locales thy =
   5.454 -  let val (space, locs) = LocalesData.get thy in
   5.455 -    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   5.456 -    |> Pretty.writeln
   5.457 -  end;
   5.458 -
   5.459 -
   5.460 -(* access registrations *)
   5.461 -
   5.462 -(* retrieve registration from theory or context *)
   5.463 -
   5.464 -fun get_registrations ctxt name =
   5.465 -  case Symtab.lookup (RegistrationsData.get ctxt) name of
   5.466 -      NONE => []
   5.467 -    | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;
   5.468 -
   5.469 -fun get_global_registrations thy = get_registrations (Context.Theory thy);
   5.470 -fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
   5.471 -
   5.472 -
   5.473 -fun get_registration ctxt imprt (name, ps) =
   5.474 -  case Symtab.lookup (RegistrationsData.get ctxt) name of
   5.475 -      NONE => NONE
   5.476 -    | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));
   5.477 -
   5.478 -fun get_global_registration thy = get_registration (Context.Theory thy);
   5.479 -fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
   5.480 -
   5.481 -
   5.482 -fun test_registration ctxt (name, ps) =
   5.483 -  case Symtab.lookup (RegistrationsData.get ctxt) name of
   5.484 -      NONE => false
   5.485 -    | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps);
   5.486 -
   5.487 -fun test_global_registration thy = test_registration (Context.Theory thy);
   5.488 -fun test_local_registration ctxt = test_registration (Context.Proof ctxt);
   5.489 -
   5.490 -
   5.491 -(* add registration to theory or context, ignored if subsumed *)
   5.492 -
   5.493 -fun put_registration (name, ps) prfx morphs ctxt =
   5.494 -  RegistrationsData.map (fn regs =>
   5.495 -    let
   5.496 -      val thy = Context.theory_of ctxt;
   5.497 -      val reg = the_default Registrations.empty (Symtab.lookup regs name);
   5.498 -      val (reg', sups) = Registrations.insert thy ps prfx morphs reg;
   5.499 -      val _ = if not (null sups) then warning
   5.500 -                ("Subsumed interpretation(s) of locale " ^
   5.501 -                 quote (extern thy name) ^
   5.502 -                 "\nwith the following prefix(es):" ^
   5.503 -                  commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups))
   5.504 -              else ();
   5.505 -    in Symtab.update (name, reg') regs end) ctxt;
   5.506 -
   5.507 -fun put_global_registration id prfx morphs =
   5.508 -  Context.theory_map (put_registration id prfx morphs);
   5.509 -fun put_local_registration id prfx morphs =
   5.510 -  Context.proof_map (put_registration id prfx morphs);
   5.511 -
   5.512 -fun put_registration_in_locale name id =
   5.513 -  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   5.514 -    (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
   5.515 -
   5.516 -
   5.517 -(* add witness theorem to registration, ignored if registration not present *)
   5.518 -
   5.519 -fun add_witness (name, ps) thm =
   5.520 -  RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));
   5.521 -
   5.522 -fun add_global_witness id thm = Context.theory_map (add_witness id thm);
   5.523 -fun add_local_witness id thm = Context.proof_map (add_witness id thm);
   5.524 -
   5.525 -
   5.526 -fun add_witness_in_locale name id thm =
   5.527 -  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
   5.528 -    let
   5.529 -      fun add (id', thms) =
   5.530 -        if id = id' then (id', thm :: thms) else (id', thms);
   5.531 -    in (axiom, elems, params, decls, map add regs, intros, dests) end);
   5.532 -
   5.533 -
   5.534 -(* add equation to registration, ignored if registration not present *)
   5.535 -
   5.536 -fun add_equation (name, ps) thm =
   5.537 -  RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));
   5.538 -
   5.539 -fun add_global_equation id thm = Context.theory_map (add_equation id thm);
   5.540 -fun add_local_equation id thm = Context.proof_map (add_equation id thm);
   5.541 -
   5.542 -(*
   5.543 -(* update morphism of registration, ignored if registration not present *)
   5.544 -
   5.545 -fun update_morph (name, ps) morph =
   5.546 -  RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph));
   5.547 -
   5.548 -fun update_global_morph id morph = Context.theory_map (update_morph id morph);
   5.549 -fun update_local_morph id morph = Context.proof_map (update_morph id morph);
   5.550 -*)
   5.551 -
   5.552 -
   5.553 -(* printing of registrations *)
   5.554 -
   5.555 -fun print_registrations show_wits loc ctxt =
   5.556 -  let
   5.557 -    val thy = ProofContext.theory_of ctxt;
   5.558 -    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   5.559 -    fun prt_term' t = if !show_types
   5.560 -          then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   5.561 -            Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   5.562 -          else prt_term t;
   5.563 -    val prt_thm = prt_term o prop_of;
   5.564 -    fun prt_inst ts =
   5.565 -        Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
   5.566 -    fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx]
   5.567 -      | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx];
   5.568 -    fun prt_eqns [] = Pretty.str "no equations."
   5.569 -      | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   5.570 -          Pretty.breaks (map prt_thm eqns));
   5.571 -    fun prt_core ts eqns =
   5.572 -          [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
   5.573 -    fun prt_witns [] = Pretty.str "no witnesses."
   5.574 -      | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   5.575 -          Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   5.576 -    fun prt_reg (ts, (_, _, witns, eqns)) =
   5.577 -        if show_wits
   5.578 -          then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   5.579 -          else Pretty.block (prt_core ts eqns)
   5.580 -
   5.581 -    val loc_int = intern thy loc;
   5.582 -    val regs = RegistrationsData.get (Context.Proof ctxt);
   5.583 -    val loc_regs = Symtab.lookup regs loc_int;
   5.584 -  in
   5.585 -    (case loc_regs of
   5.586 -        NONE => Pretty.str ("no interpretations")
   5.587 -      | SOME r => let
   5.588 -            val r' = Registrations.dest thy r;
   5.589 -            val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r';
   5.590 -          in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
   5.591 -    |> Pretty.writeln
   5.592 -  end;
   5.593 -
   5.594 -
   5.595 -(* diagnostics *)
   5.596 -
   5.597 -fun err_in_locale ctxt msg ids =
   5.598 -  let
   5.599 -    val thy = ProofContext.theory_of ctxt;
   5.600 -    fun prt_id (name, parms) =
   5.601 -      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   5.602 -    val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   5.603 -    val err_msg =
   5.604 -      if forall (fn (s, _) => s = "") ids then msg
   5.605 -      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   5.606 -        (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   5.607 -  in error err_msg end;
   5.608 -
   5.609 -fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   5.610 -
   5.611 -
   5.612 -fun pretty_ren NONE = Pretty.str "_"
   5.613 -  | pretty_ren (SOME (x, NONE)) = Pretty.str x
   5.614 -  | pretty_ren (SOME (x, SOME syn)) =
   5.615 -      Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
   5.616 -
   5.617 -fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
   5.618 -  | pretty_expr thy (Rename (expr, xs)) =
   5.619 -      Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
   5.620 -  | pretty_expr thy (Merge es) =
   5.621 -      Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
   5.622 -
   5.623 -fun err_in_expr _ msg (Merge []) = error msg
   5.624 -  | err_in_expr ctxt msg expr =
   5.625 -    error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
   5.626 -      [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
   5.627 -       pretty_expr (ProofContext.theory_of ctxt) expr]));
   5.628 -
   5.629 -
   5.630 -(** structured contexts: rename + merge + implicit type instantiation **)
   5.631 -
   5.632 -(* parameter types *)
   5.633 -
   5.634 -fun frozen_tvars ctxt Ts =
   5.635 -  #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   5.636 -  |> map (fn ((xi, S), T) => (xi, (S, T)));
   5.637 -
   5.638 -fun unify_frozen ctxt maxidx Ts Us =
   5.639 -  let
   5.640 -    fun paramify NONE i = (NONE, i)
   5.641 -      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   5.642 -
   5.643 -    val (Ts', maxidx') = fold_map paramify Ts maxidx;
   5.644 -    val (Us', maxidx'') = fold_map paramify Us maxidx';
   5.645 -    val thy = ProofContext.theory_of ctxt;
   5.646 -
   5.647 -    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   5.648 -          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   5.649 -      | unify _ env = env;
   5.650 -    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   5.651 -    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   5.652 -    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
   5.653 -  in map (Option.map (Envir.norm_type unifier')) Vs end;
   5.654 -
   5.655 -fun params_of elemss =
   5.656 -  distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
   5.657 -
   5.658 -fun params_of' elemss =
   5.659 -  distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   5.660 -
   5.661 -fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
   5.662 -
   5.663 -
   5.664 -(* CB: param_types has the following type:
   5.665 -  ('a * 'b option) list -> ('a * 'b) list *)
   5.666 -fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   5.667 -
   5.668 -
   5.669 -fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
   5.670 -  handle Symtab.DUP x => err_in_locale ctxt
   5.671 -    ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
   5.672 -
   5.673 -
   5.674 -(* Distinction of assumed vs. derived identifiers.
   5.675 -   The former may have axioms relating assumptions of the context to
   5.676 -   assumptions of the specification fragment (for locales with
   5.677 -   predicates).  The latter have witnesses relating assumptions of the
   5.678 -   specification fragment to assumptions of other (assumed) specification
   5.679 -   fragments. *)
   5.680 -
   5.681 -datatype 'a mode = Assumed of 'a | Derived of 'a;
   5.682 -
   5.683 -fun map_mode f (Assumed x) = Assumed (f x)
   5.684 -  | map_mode f (Derived x) = Derived (f x);
   5.685 -
   5.686 -
   5.687 -(* flatten expressions *)
   5.688 -
   5.689 -local
   5.690 -
   5.691 -fun unify_parms ctxt fixed_parms raw_parmss =
   5.692 -  let
   5.693 -    val thy = ProofContext.theory_of ctxt;
   5.694 -    val maxidx = length raw_parmss;
   5.695 -    val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   5.696 -
   5.697 -    fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   5.698 -    fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   5.699 -    val parms = fixed_parms @ maps varify_parms idx_parmss;
   5.700 -
   5.701 -    fun unify T U envir = Sign.typ_unify thy (U, T) envir
   5.702 -      handle Type.TUNIFY =>
   5.703 -        let
   5.704 -          val T' = Envir.norm_type (fst envir) T;
   5.705 -          val U' = Envir.norm_type (fst envir) U;
   5.706 -          val prt = Syntax.string_of_typ ctxt;
   5.707 -        in
   5.708 -          raise TYPE ("unify_parms: failed to unify types " ^
   5.709 -            prt U' ^ " and " ^ prt T', [U', T'], [])
   5.710 -        end;
   5.711 -    fun unify_list (T :: Us) = fold (unify T) Us
   5.712 -      | unify_list [] = I;
   5.713 -    val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
   5.714 -      (Vartab.empty, maxidx);
   5.715 -
   5.716 -    val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
   5.717 -    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
   5.718 -
   5.719 -    fun inst_parms (i, ps) =
   5.720 -      List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps)
   5.721 -      |> map_filter (fn (a, S) =>
   5.722 -          let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   5.723 -          in if T = TFree (a, S) then NONE else SOME (a, T) end)
   5.724 -      |> Symtab.make;
   5.725 -  in map inst_parms idx_parmss end;
   5.726 -
   5.727 -in
   5.728 -
   5.729 -fun unify_elemss _ _ [] = []
   5.730 -  | unify_elemss _ [] [elems] = [elems]
   5.731 -  | unify_elemss ctxt fixed_parms elemss =
   5.732 -      let
   5.733 -        val thy = ProofContext.theory_of ctxt;
   5.734 -        val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
   5.735 -          |> map (Element.instT_morphism thy);
   5.736 -        fun inst ((((name, ps), mode), elems), phi) =
   5.737 -          (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
   5.738 -              map_mode (map (Element.morph_witness phi)) mode),
   5.739 -            map (Element.morph_ctxt phi) elems);
   5.740 -      in map inst (elemss ~~ phis) end;
   5.741 -
   5.742 -
   5.743 -fun renaming xs parms = zip_options parms xs
   5.744 -  handle Library.UnequalLengths =>
   5.745 -    error ("Too many arguments in renaming: " ^
   5.746 -      commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
   5.747 -
   5.748 -
   5.749 -(* params_of_expr:
   5.750 -   Compute parameters (with types and syntax) of locale expression.
   5.751 -*)
   5.752 -
   5.753 -fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
   5.754 -  let
   5.755 -    val thy = ProofContext.theory_of ctxt;
   5.756 -
   5.757 -    fun merge_tenvs fixed tenv1 tenv2 =
   5.758 -        let
   5.759 -          val [env1, env2] = unify_parms ctxt fixed
   5.760 -                [tenv1 |> Symtab.dest |> map (apsnd SOME),
   5.761 -                 tenv2 |> Symtab.dest |> map (apsnd SOME)]
   5.762 -        in
   5.763 -          Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
   5.764 -            Symtab.map (Element.instT_type env2) tenv2)
   5.765 -        end;
   5.766 -
   5.767 -    fun merge_syn expr syn1 syn2 =
   5.768 -        Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
   5.769 -        handle Symtab.DUP x => err_in_expr ctxt
   5.770 -          ("Conflicting syntax for parameter: " ^ quote x) expr;
   5.771 -
   5.772 -    fun params_of (expr as Locale name) =
   5.773 -          let
   5.774 -            val {params, ...} = the_locale thy name;
   5.775 -          in (map (fst o fst) params, params |> map fst |> Symtab.make,
   5.776 -               params |> map (apfst fst) |> Symtab.make) end
   5.777 -      | params_of (expr as Rename (e, xs)) =
   5.778 -          let
   5.779 -            val (parms', types', syn') = params_of e;
   5.780 -            val ren = renaming xs parms';
   5.781 -            (* renaming may reduce number of parameters *)
   5.782 -            val new_parms = map (Element.rename ren) parms' |> distinct (op =);
   5.783 -            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
   5.784 -            val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
   5.785 -                handle Symtab.DUP x =>
   5.786 -                  err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
   5.787 -            val syn_types = map (apsnd (fn mx =>
   5.788 -                SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0)))))
   5.789 -              (Symtab.dest new_syn);
   5.790 -            val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
   5.791 -            val (env :: _) = unify_parms ctxt []
   5.792 -                ((ren_types |> map (apsnd SOME)) :: map single syn_types);
   5.793 -            val new_types = fold (Symtab.insert (op =))
   5.794 -                (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
   5.795 -          in (new_parms, new_types, new_syn) end
   5.796 -      | params_of (Merge es) =
   5.797 -          fold (fn e => fn (parms, types, syn) =>
   5.798 -                   let
   5.799 -                     val (parms', types', syn') = params_of e
   5.800 -                   in
   5.801 -                     (merge_lists (op =) parms parms', merge_tenvs [] types types',
   5.802 -                      merge_syn e syn syn')
   5.803 -                   end)
   5.804 -            es ([], Symtab.empty, Symtab.empty)
   5.805 -
   5.806 -      val (parms, types, syn) = params_of expr;
   5.807 -    in
   5.808 -      (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
   5.809 -       merge_syn expr prev_syn syn)
   5.810 -    end;
   5.811 -
   5.812 -fun make_params_ids params = [(("", params), ([], Assumed []))];
   5.813 -fun make_raw_params_elemss (params, tenv, syn) =
   5.814 -    [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   5.815 -      Int [Fixes (map (fn p =>
   5.816 -        (Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   5.817 -
   5.818 -
   5.819 -(* flatten_expr:
   5.820 -   Extend list of identifiers by those new in locale expression expr.
   5.821 -   Compute corresponding list of lists of locale elements (one entry per
   5.822 -   identifier).
   5.823 -
   5.824 -   Identifiers represent locale fragments and are in an extended form:
   5.825 -     ((name, ps), (ax_ps, axs))
   5.826 -   (name, ps) is the locale name with all its parameters.
   5.827 -   (ax_ps, axs) is the locale axioms with its parameters;
   5.828 -     axs are always taken from the top level of the locale hierarchy,
   5.829 -     hence axioms may contain additional parameters from later fragments:
   5.830 -     ps subset of ax_ps.  axs is either singleton or empty.
   5.831 -
   5.832 -   Elements are enriched by identifier-like information:
   5.833 -     (((name, ax_ps), axs), elems)
   5.834 -   The parameters in ax_ps are the axiom parameters, but enriched by type
   5.835 -   info: now each entry is a pair of string and typ option.  Axioms are
   5.836 -   type-instantiated.
   5.837 -
   5.838 -*)
   5.839 -
   5.840 -fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
   5.841 -  let
   5.842 -    val thy = ProofContext.theory_of ctxt;
   5.843 -
   5.844 -    fun rename_parms top ren ((name, ps), (parms, mode)) =
   5.845 -        ((name, map (Element.rename ren) ps),
   5.846 -         if top
   5.847 -         then (map (Element.rename ren) parms,
   5.848 -               map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
   5.849 -         else (parms, mode));
   5.850 -
   5.851 -    (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *)
   5.852 -
   5.853 -    fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
   5.854 -        if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
   5.855 -        then (wits, ids, visited)
   5.856 -        else
   5.857 -          let
   5.858 -            val {params, regs, ...} = the_locale thy name;
   5.859 -            val pTs' = map #1 params;
   5.860 -            val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
   5.861 -              (* dummy syntax, since required by rename *)
   5.862 -            val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
   5.863 -            val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
   5.864 -              (* propagate parameter types, to keep them consistent *)
   5.865 -            val regs' = map (fn ((name, ps), wits) =>
   5.866 -                ((name, map (Element.rename ren) ps),
   5.867 -                 map (Element.transfer_witness thy) wits)) regs;
   5.868 -            val new_regs = regs';
   5.869 -            val new_ids = map fst new_regs;
   5.870 -            val new_idTs =
   5.871 -              map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
   5.872 -
   5.873 -            val new_wits = new_regs |> map (#2 #> map
   5.874 -              (Element.morph_witness
   5.875 -                (Element.instT_morphism thy env $>
   5.876 -                  Element.rename_morphism ren $>
   5.877 -                  Element.satisfy_morphism wits)
   5.878 -                #> Element.close_witness));
   5.879 -            val new_ids' = map (fn (id, wits) =>
   5.880 -                (id, ([], Derived wits))) (new_ids ~~ new_wits);
   5.881 -            val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
   5.882 -                ((n, pTs), mode)) (new_idTs ~~ new_ids');
   5.883 -            val new_id = ((name, map #1 pTs), ([], mode));
   5.884 -            val (wits', ids', visited') = fold add_with_regs new_idTs'
   5.885 -              (wits @ flat new_wits, ids, visited @ [new_id]);
   5.886 -          in
   5.887 -            (wits', ids' @ [new_id], visited')
   5.888 -          end;
   5.889 -
   5.890 -    (* distribute top-level axioms over assumed ids *)
   5.891 -
   5.892 -    fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
   5.893 -        let
   5.894 -          val {elems, ...} = the_locale thy name;
   5.895 -          val ts = maps
   5.896 -            (fn (Assumes asms, _) => maps (map #1 o #2) asms
   5.897 -              | _ => [])
   5.898 -            elems;
   5.899 -          val (axs1, axs2) = chop (length ts) axioms;
   5.900 -        in (((name, parms), (all_ps, Assumed axs1)), axs2) end
   5.901 -      | axiomify all_ps (id, (_, Derived ths)) axioms =
   5.902 -          ((id, (all_ps, Derived ths)), axioms);
   5.903 -
   5.904 -    (* identifiers of an expression *)
   5.905 -
   5.906 -    fun identify top (Locale name) =
   5.907 -    (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
   5.908 -       where name is a locale name, ps a list of parameter names and axs
   5.909 -       a list of axioms relating to the identifier, axs is empty unless
   5.910 -       identify at top level (top = true);
   5.911 -       parms is accumulated list of parameters *)
   5.912 -          let
   5.913 -            val {axiom, params, ...} = the_locale thy name;
   5.914 -            val ps = map (#1 o #1) params;
   5.915 -            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);
   5.916 -            val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
   5.917 -            in (ids_ax, ps) end
   5.918 -      | identify top (Rename (e, xs)) =
   5.919 -          let
   5.920 -            val (ids', parms') = identify top e;
   5.921 -            val ren = renaming xs parms'
   5.922 -              handle ERROR msg => err_in_locale' ctxt msg ids';
   5.923 -
   5.924 -            val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   5.925 -            val parms'' = distinct (op =) (maps (#2 o #1) ids'');
   5.926 -          in (ids'', parms'') end
   5.927 -      | identify top (Merge es) =
   5.928 -          fold (fn e => fn (ids, parms) =>
   5.929 -                   let
   5.930 -                     val (ids', parms') = identify top e
   5.931 -                   in
   5.932 -                     (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
   5.933 -                   end)
   5.934 -            es ([], []);
   5.935 -
   5.936 -    fun inst_wit all_params (t, th) = let
   5.937 -         val {hyps, prop, ...} = Thm.rep_thm th;
   5.938 -         val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
   5.939 -         val [env] = unify_parms ctxt all_params [ps];
   5.940 -         val t' = Element.instT_term env t;
   5.941 -         val th' = Element.instT_thm thy env th;
   5.942 -       in (t', th') end;
   5.943 -
   5.944 -    fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
   5.945 -      let
   5.946 -        val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
   5.947 -        val elems = map fst elems_stamped;
   5.948 -        val ps = map fst ps_mx;
   5.949 -        fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
   5.950 -        val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
   5.951 -        val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
   5.952 -        val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
   5.953 -        val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   5.954 -        val (lprfx, pprfx) = param_prefix name params;
   5.955 -        val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
   5.956 -          #> Binding.add_prefix false lprfx;
   5.957 -        val elem_morphism =
   5.958 -          Element.rename_morphism ren $>
   5.959 -          Morphism.binding_morphism add_prefices $>
   5.960 -          Element.instT_morphism thy env;
   5.961 -        val elems' = map (Element.morph_ctxt elem_morphism) elems;
   5.962 -      in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   5.963 -
   5.964 -    (* parameters, their types and syntax *)
   5.965 -    val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
   5.966 -    val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
   5.967 -    (* compute identifiers and syntax, merge with previous ones *)
   5.968 -    val (ids, _) = identify true expr;
   5.969 -    val idents = subtract (eq_fst (op =)) prev_idents ids;
   5.970 -    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   5.971 -    (* type-instantiate elements *)
   5.972 -    val final_elemss = map (eval all_params tenv syntax) idents;
   5.973 -  in ((prev_idents @ idents, syntax), final_elemss) end;
   5.974 -
   5.975 -end;
   5.976 -
   5.977 -
   5.978 -(* activate elements *)
   5.979 -
   5.980 -local
   5.981 -
   5.982 -fun axioms_export axs _ As =
   5.983 -  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
   5.984 -
   5.985 -
   5.986 -(* NB: derived ids contain only facts at this stage *)
   5.987 -
   5.988 -fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
   5.989 -      ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
   5.990 -  | activate_elem _ _ (Constrains _) (ctxt, mode) =
   5.991 -      ([], (ctxt, mode))
   5.992 -  | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
   5.993 -      let
   5.994 -        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   5.995 -        val ts = maps (map #1 o #2) asms';
   5.996 -        val (ps, qs) = chop (length ts) axs;
   5.997 -        val (_, ctxt') =
   5.998 -          ctxt |> fold Variable.auto_fixes ts
   5.999 -          |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
  5.1000 -      in ([], (ctxt', Assumed qs)) end
  5.1001 -  | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
  5.1002 -      ([], (ctxt, Derived ths))
  5.1003 -  | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
  5.1004 -      let
  5.1005 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  5.1006 -        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  5.1007 -            let val ((c, _), t') = LocalDefs.cert_def ctxt t
  5.1008 -            in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  5.1009 -        val (_, ctxt') =
  5.1010 -          ctxt |> fold (Variable.auto_fixes o #1) asms
  5.1011 -          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  5.1012 -      in ([], (ctxt', Assumed axs)) end
  5.1013 -  | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
  5.1014 -      ([], (ctxt, Derived ths))
  5.1015 -  | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
  5.1016 -      let
  5.1017 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
  5.1018 -        val (res, ctxt') = ctxt |> local_note_qualified kind facts';
  5.1019 -      in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
  5.1020 -
  5.1021 -fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  5.1022 -  let
  5.1023 -    val thy = ProofContext.theory_of ctxt;
  5.1024 -    val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
  5.1025 -        elems (ProofContext.qualified_names ctxt, mode)
  5.1026 -      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
  5.1027 -    val ctxt'' = if name = "" then ctxt'
  5.1028 -          else let
  5.1029 -              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
  5.1030 -            in if test_local_registration ctxt' (name, ps') then ctxt'
  5.1031 -              else let
  5.1032 -                  val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, ""))
  5.1033 -                    (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
  5.1034 -                in case mode of
  5.1035 -                    Assumed axs =>
  5.1036 -                      fold (add_local_witness (name, ps') o
  5.1037 -                        Element.assume_witness thy o Element.witness_prop) axs ctxt''
  5.1038 -                  | Derived ths =>
  5.1039 -                     fold (add_local_witness (name, ps')) ths ctxt''
  5.1040 -                end
  5.1041 -            end
  5.1042 -  in (ProofContext.restore_naming ctxt ctxt'', res) end;
  5.1043 -
  5.1044 -fun activate_elemss ax_in_ctxt prep_facts =
  5.1045 -    fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
  5.1046 -      let
  5.1047 -        val elems = map (prep_facts ctxt) raw_elems;
  5.1048 -        val (ctxt', res) = apsnd flat
  5.1049 -            (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
  5.1050 -        val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
  5.1051 -      in (((((name, ps), mode), elems'), res), ctxt') end);
  5.1052 -
  5.1053 -in
  5.1054 -
  5.1055 -(* CB: activate_facts prep_facts elemss ctxt,
  5.1056 -   where elemss is a list of pairs consisting of identifiers and
  5.1057 -   context elements, extends ctxt by the context elements yielding
  5.1058 -   ctxt' and returns ((elemss', facts), ctxt').
  5.1059 -   Identifiers in the argument are of the form ((name, ps), axs) and
  5.1060 -   assumptions use the axioms in the identifiers to set up exporters
  5.1061 -   in ctxt'.  elemss' does not contain identifiers and is obtained
  5.1062 -   from elemss and the intermediate context with prep_facts.
  5.1063 -   If read_facts or cert_facts is used for prep_facts, these also remove
  5.1064 -   the internal/external markers from elemss. *)
  5.1065 -
  5.1066 -fun activate_facts ax_in_ctxt prep_facts args =
  5.1067 -  activate_elemss ax_in_ctxt prep_facts args
  5.1068 -  #>> (apsnd flat o split_list);
  5.1069 -
  5.1070 -end;
  5.1071 -
  5.1072 -
  5.1073 -
  5.1074 -(** prepare locale elements **)
  5.1075 -
  5.1076 -(* expressions *)
  5.1077 -
  5.1078 -fun intern_expr thy (Locale xname) = Locale (intern thy xname)
  5.1079 -  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
  5.1080 -  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
  5.1081 -
  5.1082 -
  5.1083 -(* propositions and bindings *)
  5.1084 -
  5.1085 -(* flatten (ctxt, prep_expr) ((ids, syn), expr)
  5.1086 -   normalises expr (which is either a locale
  5.1087 -   expression or a single context element) wrt.
  5.1088 -   to the list ids of already accumulated identifiers.
  5.1089 -   It returns ((ids', syn'), elemss) where ids' is an extension of ids
  5.1090 -   with identifiers generated for expr, and elemss is the list of
  5.1091 -   context elements generated from expr.
  5.1092 -   syn and syn' are symtabs mapping parameter names to their syntax.  syn'
  5.1093 -   is an extension of syn.
  5.1094 -   For details, see flatten_expr.
  5.1095 -
  5.1096 -   Additionally, for a locale expression, the elems are grouped into a single
  5.1097 -   Int; individual context elements are marked Ext.  In this case, the
  5.1098 -   identifier-like information of the element is as follows:
  5.1099 -   - for Fixes: (("", ps), []) where the ps have type info NONE
  5.1100 -   - for other elements: (("", []), []).
  5.1101 -   The implementation of activate_facts relies on identifier names being
  5.1102 -   empty strings for external elements.
  5.1103 -*)
  5.1104 -
  5.1105 -fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
  5.1106 -        val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
  5.1107 -      in
  5.1108 -        ((ids',
  5.1109 -         merge_syntax ctxt ids'
  5.1110 -           (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
  5.1111 -           handle Symtab.DUP x => err_in_locale ctxt
  5.1112 -             ("Conflicting syntax for parameter: " ^ quote x)
  5.1113 -             (map #1 ids')),
  5.1114 -         [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
  5.1115 -      end
  5.1116 -  | flatten _ ((ids, syn), Elem elem) =
  5.1117 -      ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  5.1118 -  | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
  5.1119 -      apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
  5.1120 -
  5.1121 -local
  5.1122 -
  5.1123 -local
  5.1124 -
  5.1125 -fun declare_int_elem (Fixes fixes) ctxt =
  5.1126 -      ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  5.1127 -        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
  5.1128 -  | declare_int_elem _ ctxt = ([], ctxt);
  5.1129 -
  5.1130 -fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
  5.1131 -      let val (vars, _) = prep_vars fixes ctxt
  5.1132 -      in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
  5.1133 -  | declare_ext_elem prep_vars (Constrains csts) ctxt =
  5.1134 -      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt
  5.1135 -      in ([], ctxt') end
  5.1136 -  | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
  5.1137 -  | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
  5.1138 -  | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
  5.1139 -
  5.1140 -fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
  5.1141 -     of Int es => fold_map declare_int_elem es ctxt
  5.1142 -      | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
  5.1143 -          handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
  5.1144 -  | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
  5.1145 -
  5.1146 -in
  5.1147 -
  5.1148 -fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
  5.1149 -  let
  5.1150 -    (* CB: fix of type bug of goal in target with context elements.
  5.1151 -       Parameters new in context elements must receive types that are
  5.1152 -       distinct from types of parameters in target (fixed_params).  *)
  5.1153 -    val ctxt_with_fixed = 
  5.1154 -      fold Variable.declare_term (map Free fixed_params) ctxt;
  5.1155 -    val int_elemss =
  5.1156 -      raw_elemss
  5.1157 -      |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  5.1158 -      |> unify_elemss ctxt_with_fixed fixed_params;
  5.1159 -    val (raw_elemss', _) =
  5.1160 -      fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
  5.1161 -        raw_elemss int_elemss;
  5.1162 -  in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
  5.1163 -
  5.1164 -end;
  5.1165 -
  5.1166 -local
  5.1167 -
  5.1168 -val norm_term = Envir.beta_norm oo Term.subst_atomic;
  5.1169 -
  5.1170 -fun abstract_thm thy eq =
  5.1171 -  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
  5.1172 -
  5.1173 -fun bind_def ctxt (name, ps) eq (xs, env, ths) =
  5.1174 -  let
  5.1175 -    val ((y, T), b) = LocalDefs.abs_def eq;
  5.1176 -    val b' = norm_term env b;
  5.1177 -    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
  5.1178 -    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  5.1179 -  in
  5.1180 -    exists (fn (x, _) => x = y) xs andalso
  5.1181 -      err "Attempt to define previously specified variable";
  5.1182 -    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
  5.1183 -      err "Attempt to redefine variable";
  5.1184 -    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  5.1185 -  end;
  5.1186 -
  5.1187 -
  5.1188 -(* CB: for finish_elems (Int and Ext),
  5.1189 -   extracts specification, only of assumed elements *)
  5.1190 -
  5.1191 -fun eval_text _ _ _ (Fixes _) text = text
  5.1192 -  | eval_text _ _ _ (Constrains _) text = text
  5.1193 -  | eval_text _ (_, Assumed _) is_ext (Assumes asms)
  5.1194 -        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  5.1195 -      let
  5.1196 -        val ts = maps (map #1 o #2) asms;
  5.1197 -        val ts' = map (norm_term env) ts;
  5.1198 -        val spec' =
  5.1199 -          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  5.1200 -          else ((exts, exts'), (ints @ ts, ints' @ ts'));
  5.1201 -      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  5.1202 -  | eval_text _ (_, Derived _) _ (Assumes _) text = text
  5.1203 -  | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
  5.1204 -      (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
  5.1205 -  | eval_text _ (_, Derived _) _ (Defines _) text = text
  5.1206 -  | eval_text _ _ _ (Notes _) text = text;
  5.1207 -
  5.1208 -
  5.1209 -(* for finish_elems (Int),
  5.1210 -   remove redundant elements of derived identifiers,
  5.1211 -   turn assumptions and definitions into facts,
  5.1212 -   satisfy hypotheses of facts *)
  5.1213 -
  5.1214 -fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  5.1215 -  | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  5.1216 -  | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  5.1217 -  | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
  5.1218 -
  5.1219 -  | finish_derived _ _ (Derived _) (Fixes _) = NONE
  5.1220 -  | finish_derived _ _ (Derived _) (Constrains _) = NONE
  5.1221 -  | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
  5.1222 -      |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
  5.1223 -      |> pair Thm.assumptionK |> Notes
  5.1224 -      |> Element.morph_ctxt satisfy |> SOME
  5.1225 -  | finish_derived sign satisfy (Derived _) (Defines defs) = defs
  5.1226 -      |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
  5.1227 -      |> pair Thm.definitionK |> Notes
  5.1228 -      |> Element.morph_ctxt satisfy |> SOME
  5.1229 -
  5.1230 -  | finish_derived _ satisfy _ (Notes facts) = Notes facts
  5.1231 -      |> Element.morph_ctxt satisfy |> SOME;
  5.1232 -
  5.1233 -(* CB: for finish_elems (Ext) *)
  5.1234 -
  5.1235 -fun closeup _ false elem = elem
  5.1236 -  | closeup ctxt true elem =
  5.1237 -      let
  5.1238 -        fun close_frees t =
  5.1239 -          let
  5.1240 -            val rev_frees =
  5.1241 -              Term.fold_aterms (fn Free (x, T) =>
  5.1242 -                if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
  5.1243 -          in Term.list_all_free (rev rev_frees, t) end;
  5.1244 -
  5.1245 -        fun no_binds [] = []
  5.1246 -          | no_binds _ = error "Illegal term bindings in locale element";
  5.1247 -      in
  5.1248 -        (case elem of
  5.1249 -          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
  5.1250 -            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
  5.1251 -        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
  5.1252 -            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
  5.1253 -        | e => e)
  5.1254 -      end;
  5.1255 -
  5.1256 -
  5.1257 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
  5.1258 -      let val x = Binding.base_name b
  5.1259 -      in (b, AList.lookup (op =) parms x, mx) end) fixes)
  5.1260 -  | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  5.1261 -  | finish_ext_elem _ close (Assumes asms, propp) =
  5.1262 -      close (Assumes (map #1 asms ~~ propp))
  5.1263 -  | finish_ext_elem _ close (Defines defs, propp) =
  5.1264 -      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
  5.1265 -  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
  5.1266 -
  5.1267 -
  5.1268 -(* CB: finish_parms introduces type info from parms to identifiers *)
  5.1269 -(* CB: only needed for types that have been NONE so far???
  5.1270 -   If so, which are these??? *)
  5.1271 -
  5.1272 -fun finish_parms parms (((name, ps), mode), elems) =
  5.1273 -  (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
  5.1274 -
  5.1275 -fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
  5.1276 -      let
  5.1277 -        val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
  5.1278 -        val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
  5.1279 -        val text' = fold (eval_text ctxt id' false) es text;
  5.1280 -        val es' = map_filter
  5.1281 -          (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
  5.1282 -      in ((text', wits'), (id', map Int es')) end
  5.1283 -  | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
  5.1284 -      let
  5.1285 -        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
  5.1286 -        val text' = eval_text ctxt id true e' text;
  5.1287 -      in ((text', wits), (id, [Ext e'])) end
  5.1288 -
  5.1289 -in
  5.1290 -
  5.1291 -(* CB: only called by prep_elemss *)
  5.1292 -
  5.1293 -fun finish_elemss ctxt parms do_close =
  5.1294 -  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
  5.1295 -
  5.1296 -end;
  5.1297 -
  5.1298 -
  5.1299 -(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
  5.1300 -
  5.1301 -fun defs_ord (defs1, defs2) =
  5.1302 -    list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
  5.1303 -      TermOrd.fast_term_ord (d1, d2)) (defs1, defs2);
  5.1304 -structure Defstab =
  5.1305 -    TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
  5.1306 -
  5.1307 -fun rem_dup_defs es ds =
  5.1308 -    fold_map (fn e as (Defines defs) => (fn ds =>
  5.1309 -                 if Defstab.defined ds defs
  5.1310 -                 then (Defines [], ds)
  5.1311 -                 else (e, Defstab.update (defs, ()) ds))
  5.1312 -               | e => (fn ds => (e, ds))) es ds;
  5.1313 -fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
  5.1314 -  | rem_dup_elemss (Ext e) ds = (Ext e, ds);
  5.1315 -fun rem_dup_defines raw_elemss =
  5.1316 -    fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
  5.1317 -                     apfst (pair id) (rem_dup_elemss es ds))
  5.1318 -               | (id as (_, (Derived _)), es) => (fn ds =>
  5.1319 -                     ((id, es), ds))) raw_elemss Defstab.empty |> #1;
  5.1320 -
  5.1321 -(* CB: type inference and consistency checks for locales.
  5.1322 -
  5.1323 -   Works by building a context (through declare_elemss), extracting the
  5.1324 -   required information and adjusting the context elements (finish_elemss).
  5.1325 -   Can also universally close free vars in assms and defs.  This is only
  5.1326 -   needed for Ext elements and controlled by parameter do_close.
  5.1327 -
  5.1328 -   Only elements of assumed identifiers are considered.
  5.1329 -*)
  5.1330 -
  5.1331 -fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
  5.1332 -  let
  5.1333 -    (* CB: contexts computed in the course of this function are discarded.
  5.1334 -       They are used for type inference and consistency checks only. *)
  5.1335 -    (* CB: fixed_params are the parameters (with types) of the target locale,
  5.1336 -       empty list if there is no target. *)
  5.1337 -    (* CB: raw_elemss are list of pairs consisting of identifiers and
  5.1338 -       context elements, the latter marked as internal or external. *)
  5.1339 -    val raw_elemss = rem_dup_defines raw_elemss;
  5.1340 -    val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
  5.1341 -    (* CB: raw_ctxt is context with additional fixed variables derived from
  5.1342 -       the fixes elements in raw_elemss,
  5.1343 -       raw_proppss contains assumptions and definitions from the
  5.1344 -       external elements in raw_elemss. *)
  5.1345 -    fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
  5.1346 -      let
  5.1347 -        (* CB: add type information from fixed_params to context (declare_term) *)
  5.1348 -        (* CB: process patterns (conclusion and external elements only) *)
  5.1349 -        val (ctxt, all_propp) =
  5.1350 -          prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  5.1351 -        (* CB: add type information from conclusion and external elements to context *)
  5.1352 -        val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
  5.1353 -        (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
  5.1354 -        val all_propp' = map2 (curry (op ~~))
  5.1355 -          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
  5.1356 -        val (concl, propp) = chop (length raw_concl) all_propp';
  5.1357 -      in (propp, (ctxt, concl)) end
  5.1358 -
  5.1359 -    val (proppss, (ctxt, concl)) =
  5.1360 -      (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
  5.1361 -
  5.1362 -    (* CB: obtain all parameters from identifier part of raw_elemss *)
  5.1363 -    val xs = map #1 (params_of' raw_elemss);
  5.1364 -    val typing = unify_frozen ctxt 0
  5.1365 -      (map (Variable.default_type raw_ctxt) xs)
  5.1366 -      (map (Variable.default_type ctxt) xs);
  5.1367 -    val parms = param_types (xs ~~ typing);
  5.1368 -    (* CB: parms are the parameters from raw_elemss, with correct typing. *)
  5.1369 -
  5.1370 -    (* CB: extract information from assumes and defines elements
  5.1371 -       (fixes, constrains and notes in raw_elemss don't have an effect on
  5.1372 -       text and elemss), compute final form of context elements. *)
  5.1373 -    val ((text, _), elemss) = finish_elemss ctxt parms do_close
  5.1374 -      ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
  5.1375 -    (* CB: text has the following structure:
  5.1376 -           (((exts, exts'), (ints, ints')), (xs, env, defs))
  5.1377 -       where
  5.1378 -         exts: external assumptions (terms in external assumes elements)
  5.1379 -         exts': dito, normalised wrt. env
  5.1380 -         ints: internal assumptions (terms in internal assumes elements)
  5.1381 -         ints': dito, normalised wrt. env
  5.1382 -         xs: the free variables in exts' and ints' and rhss of definitions,
  5.1383 -           this includes parameters except defined parameters
  5.1384 -         env: list of term pairs encoding substitutions, where the first term
  5.1385 -           is a free variable; substitutions represent defines elements and
  5.1386 -           the rhs is normalised wrt. the previous env
  5.1387 -         defs: theorems representing the substitutions from defines elements
  5.1388 -           (thms are normalised wrt. env).
  5.1389 -       elemss is an updated version of raw_elemss:
  5.1390 -         - type info added to Fixes and modified in Constrains
  5.1391 -         - axiom and definition statement replaced by corresponding one
  5.1392 -           from proppss in Assumes and Defines
  5.1393 -         - Facts unchanged
  5.1394 -       *)
  5.1395 -  in ((parms, elemss, concl), text) end;
  5.1396 -
  5.1397 -in
  5.1398 -
  5.1399 -fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
  5.1400 -fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
  5.1401 -
  5.1402 -end;
  5.1403 -
  5.1404 -
  5.1405 -(* facts and attributes *)
  5.1406 -
  5.1407 -local
  5.1408 -
  5.1409 -fun check_name name =
  5.1410 -  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
  5.1411 -  else name;
  5.1412 -
  5.1413 -fun prep_facts _ _ _ ctxt (Int elem) = elem
  5.1414 -      |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
  5.1415 -  | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  5.1416 -     {var = I, typ = I, term = I,
  5.1417 -      binding = Binding.map_base prep_name,
  5.1418 -      fact = get ctxt,
  5.1419 -      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  5.1420 -
  5.1421 -in
  5.1422 -
  5.1423 -fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
  5.1424 -fun cert_facts x = prep_facts I (K I) (K I) x;
  5.1425 -
  5.1426 -end;
  5.1427 -
  5.1428 -
  5.1429 -(* Get the specification of a locale *)
  5.1430 -
  5.1431 -(*The global specification is made from the parameters and global
  5.1432 -  assumptions, the local specification from the parameters and the
  5.1433 -  local assumptions.*)
  5.1434 -
  5.1435 -local
  5.1436 -
  5.1437 -fun gen_asms_of get thy name =
  5.1438 -  let
  5.1439 -    val ctxt = ProofContext.init thy;
  5.1440 -    val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
  5.1441 -    val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
  5.1442 -  in
  5.1443 -    elemss |> get
  5.1444 -      |> maps (fn (_, es) => map (fn Int e => e) es)
  5.1445 -      |> maps (fn Assumes asms => asms | _ => [])
  5.1446 -      |> map (apsnd (map fst))
  5.1447 -  end;
  5.1448 -
  5.1449 -in
  5.1450 -
  5.1451 -fun parameters_of thy = #params o the_locale thy;
  5.1452 -
  5.1453 -fun intros thy = #intros o the_locale thy;
  5.1454 -  (*returns introduction rule for delta predicate and locale predicate
  5.1455 -    as a pair of singleton lists*)
  5.1456 -
  5.1457 -fun dests thy = #dests o the_locale thy;
  5.1458 -
  5.1459 -fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts
  5.1460 -  | _ => NONE) o #elems o the_locale thy;
  5.1461 -
  5.1462 -fun parameters_of_expr thy expr =
  5.1463 -  let
  5.1464 -    val ctxt = ProofContext.init thy;
  5.1465 -    val pts = params_of_expr ctxt [] (intern_expr thy expr)
  5.1466 -        ([], Symtab.empty, Symtab.empty);
  5.1467 -    val raw_params_elemss = make_raw_params_elemss pts;
  5.1468 -    val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  5.1469 -        (([], Symtab.empty), Expr expr);
  5.1470 -    val ((parms, _, _), _) =
  5.1471 -        read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
  5.1472 -  in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
  5.1473 -
  5.1474 -fun local_asms_of thy name =
  5.1475 -  gen_asms_of (single o Library.last_elem) thy name;
  5.1476 -
  5.1477 -fun global_asms_of thy name =
  5.1478 -  gen_asms_of I thy name;
  5.1479 -
  5.1480 -end;
  5.1481 -
  5.1482 -
  5.1483 -(* full context statements: imports + elements + conclusion *)
  5.1484 -
  5.1485 -local
  5.1486 -
  5.1487 -fun prep_context_statement prep_expr prep_elemss prep_facts
  5.1488 -    do_close fixed_params imports elements raw_concl context =
  5.1489 -  let
  5.1490 -    val thy = ProofContext.theory_of context;
  5.1491 -
  5.1492 -    val (import_params, import_tenv, import_syn) =
  5.1493 -      params_of_expr context fixed_params (prep_expr thy imports)
  5.1494 -        ([], Symtab.empty, Symtab.empty);
  5.1495 -    val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
  5.1496 -    val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
  5.1497 -      (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
  5.1498 -
  5.1499 -    val ((import_ids, _), raw_import_elemss) =
  5.1500 -      flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
  5.1501 -    (* CB: normalise "includes" among elements *)
  5.1502 -    val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
  5.1503 -      ((import_ids, incl_syn), elements);
  5.1504 -
  5.1505 -    val raw_elemss = flat raw_elemsss;
  5.1506 -    (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  5.1507 -       context elements obtained from import and elements. *)
  5.1508 -    (* Now additional elements for parameters are inserted. *)
  5.1509 -    val import_params_ids = make_params_ids import_params;
  5.1510 -    val incl_params_ids =
  5.1511 -        make_params_ids (incl_params \\ import_params);
  5.1512 -    val raw_import_params_elemss =
  5.1513 -        make_raw_params_elemss (import_params, incl_tenv, incl_syn);
  5.1514 -    val raw_incl_params_elemss =
  5.1515 -        make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
  5.1516 -    val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  5.1517 -      context fixed_params
  5.1518 -      (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
  5.1519 -
  5.1520 -    (* replace extended ids (for axioms) by ids *)
  5.1521 -    val (import_ids', incl_ids) = chop (length import_ids) ids;
  5.1522 -    val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
  5.1523 -    val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
  5.1524 -        (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
  5.1525 -      (all_ids ~~ all_elemss);
  5.1526 -    (* CB: all_elemss and parms contain the correct parameter types *)
  5.1527 -
  5.1528 -    val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  5.1529 -    val ((import_elemss, _), import_ctxt) =
  5.1530 -      activate_facts false prep_facts ps context;
  5.1531 -
  5.1532 -    val ((elemss, _), ctxt) =
  5.1533 -      activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
  5.1534 -  in
  5.1535 -    ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  5.1536 -      (parms, spec, defs)), concl)
  5.1537 -  end;
  5.1538 -
  5.1539 -fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  5.1540 -  let
  5.1541 -    val thy = ProofContext.theory_of ctxt;
  5.1542 -    val locale = Option.map (prep_locale thy) raw_locale;
  5.1543 -    val (fixed_params, imports) =
  5.1544 -      (case locale of
  5.1545 -        NONE => ([], empty)
  5.1546 -      | SOME name =>
  5.1547 -          let val {params = ps, ...} = the_locale thy name
  5.1548 -          in (map fst ps, Locale name) end);
  5.1549 -    val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
  5.1550 -      prep_ctxt false fixed_params imports (map Elem elems) concl ctxt;
  5.1551 -  in (locale, locale_ctxt, elems_ctxt, concl') end;
  5.1552 -
  5.1553 -fun prep_expr prep imports body ctxt =
  5.1554 -  let
  5.1555 -    val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
  5.1556 -    val all_elems = maps snd (import_elemss @ elemss);
  5.1557 -  in (all_elems, ctxt') end;
  5.1558 -
  5.1559 -in
  5.1560 -
  5.1561 -val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
  5.1562 -val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
  5.1563 -
  5.1564 -fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
  5.1565 -fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
  5.1566 -
  5.1567 -val read_expr = prep_expr read_context;
  5.1568 -val cert_expr = prep_expr cert_context;
  5.1569 -
  5.1570 -fun read_context_statement loc = prep_statement (K I) read_ctxt loc;
  5.1571 -fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc;
  5.1572 -fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
  5.1573 -
  5.1574 -end;
  5.1575 -
  5.1576 -
  5.1577 -(* init *)
  5.1578 -
  5.1579 -fun init loc =
  5.1580 -  ProofContext.init
  5.1581 -  #> #2 o cert_context_statement (SOME loc) [] [];
  5.1582 -
  5.1583 -
  5.1584 -(* print locale *)
  5.1585 -
  5.1586 -fun print_locale thy show_facts imports body =
  5.1587 -  let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
  5.1588 -    Pretty.big_list "locale elements:" (all_elems
  5.1589 -      |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
  5.1590 -      |> map (Element.pretty_ctxt ctxt) |> filter_out null
  5.1591 -      |> map Pretty.chunks)
  5.1592 -    |> Pretty.writeln
  5.1593 -  end;
  5.1594 -
  5.1595 -
  5.1596 -
  5.1597 -(** store results **)
  5.1598 -
  5.1599 -(* join equations of an id with already accumulated ones *)
  5.1600 -
  5.1601 -fun join_eqns get_reg id eqns =
  5.1602 -  let
  5.1603 -    val eqns' = case get_reg id
  5.1604 -      of NONE => eqns
  5.1605 -        | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns')
  5.1606 -            (* prefer equations from eqns' *)
  5.1607 -  in ((id, eqns'), eqns') end;
  5.1608 -
  5.1609 -
  5.1610 -(* collect witnesses and equations up to a particular target for a
  5.1611 -   registration; requires parameters and flattened list of identifiers
  5.1612 -   instead of recomputing it from the target *)
  5.1613 -
  5.1614 -fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let
  5.1615 -
  5.1616 -    val thy = ProofContext.theory_of ctxt;
  5.1617 -
  5.1618 -    val ts = map (var_inst_term (impT, imp)) ext_ts;
  5.1619 -    val (parms, parmTs) = split_list parms;
  5.1620 -    val parmvTs = map Logic.varifyT parmTs;
  5.1621 -    val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
  5.1622 -    val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
  5.1623 -        |> Symtab.make;
  5.1624 -    val inst = Symtab.make (parms ~~ ts);
  5.1625 -
  5.1626 -    (* instantiate parameter names in ids *)
  5.1627 -    val ext_inst = Symtab.make (parms ~~ ext_ts);
  5.1628 -    fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps;
  5.1629 -    val inst_ids = map (apfst (apsnd ext_inst_names)) ids;
  5.1630 -    val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
  5.1631 -    val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids;
  5.1632 -    val eqns =
  5.1633 -      fold_map (join_eqns (get_local_registration ctxt imprt))
  5.1634 -        (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd;
  5.1635 -  in ((tinst, inst), wits, eqns) end;
  5.1636 -
  5.1637 -
  5.1638 -(* compute and apply morphism *)
  5.1639 -
  5.1640 -fun name_morph phi_name (lprfx, pprfx) b =
  5.1641 -  b
  5.1642 -  |> (if not (Binding.is_empty b) andalso pprfx <> ""
  5.1643 -        then Binding.add_prefix false pprfx else I)
  5.1644 -  |> (if not (Binding.is_empty b)
  5.1645 -        then Binding.add_prefix false lprfx else I)
  5.1646 -  |> phi_name;
  5.1647 -
  5.1648 -fun inst_morph thy phi_name param_prfx insts prems eqns export =
  5.1649 -  let
  5.1650 -    (* standardise export morphism *)
  5.1651 -    val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
  5.1652 -    val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
  5.1653 -      (* FIXME sync with exp_fact *)
  5.1654 -    val exp_typ = Logic.type_map exp_term;
  5.1655 -    val export' =
  5.1656 -      Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  5.1657 -  in
  5.1658 -    Morphism.binding_morphism (name_morph phi_name param_prfx) $>
  5.1659 -      Element.inst_morphism thy insts $>
  5.1660 -      Element.satisfy_morphism prems $>
  5.1661 -      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
  5.1662 -      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
  5.1663 -      export'
  5.1664 -  end;
  5.1665 -
  5.1666 -fun activate_note thy phi_name param_prfx attrib insts prems eqns exp =
  5.1667 -  (Element.facts_map o Element.morph_ctxt)
  5.1668 -      (inst_morph thy phi_name param_prfx insts prems eqns exp)
  5.1669 -  #> Attrib.map_facts attrib;
  5.1670 -
  5.1671 -
  5.1672 -(* public interface to interpretation morphism *)
  5.1673 -
  5.1674 -fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts =
  5.1675 -  let
  5.1676 -    val parms = the_locale thy target |> #params |> map fst;
  5.1677 -    val ids = flatten (ProofContext.init thy, intern_expr thy)
  5.1678 -      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  5.1679 -    val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  5.1680 -  in
  5.1681 -    inst_morph thy phi_name param_prfx insts prems eqns exp
  5.1682 -  end;
  5.1683 -
  5.1684 -(* store instantiations of args for all registered interpretations
  5.1685 -   of the theory *)
  5.1686 -
  5.1687 -fun note_thmss_registrations target (kind, args) thy =
  5.1688 -  let
  5.1689 -    val parms = the_locale thy target |> #params |> map fst;
  5.1690 -    val ids = flatten (ProofContext.init thy, intern_expr thy)
  5.1691 -      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
  5.1692 -
  5.1693 -    val regs = get_global_registrations thy target;
  5.1694 -    (* add args to thy for all registrations *)
  5.1695 -
  5.1696 -    fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  5.1697 -      let
  5.1698 -        val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
  5.1699 -        val args' = args
  5.1700 -          |> activate_note thy phi_name param_prfx
  5.1701 -               (Attrib.attribute_i thy) insts prems eqns exp;
  5.1702 -      in
  5.1703 -        thy
  5.1704 -        |> global_note_qualified kind args'
  5.1705 -        |> snd
  5.1706 -      end;
  5.1707 -  in fold activate regs thy end;
  5.1708 -
  5.1709 -
  5.1710 -(* locale results *)
  5.1711 -
  5.1712 -fun add_thmss loc kind args ctxt =
  5.1713 -  let
  5.1714 -    val (([(_, [Notes args'])], _), ctxt') =
  5.1715 -      activate_facts true cert_facts
  5.1716 -        [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
  5.1717 -    val ctxt'' = ctxt' |> ProofContext.theory
  5.1718 -      (change_locale loc
  5.1719 -        (fn (axiom, elems, params, decls, regs, intros, dests) =>
  5.1720 -          (axiom, elems @ [(Notes args', stamp ())],
  5.1721 -            params, decls, regs, intros, dests))
  5.1722 -      #> note_thmss_registrations loc args');
  5.1723 -  in ctxt'' end;
  5.1724 -
  5.1725 -
  5.1726 -(* declarations *)
  5.1727 -
  5.1728 -local
  5.1729 -
  5.1730 -fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
  5.1731 -
  5.1732 -fun add_decls add loc decl =
  5.1733 -  ProofContext.theory (change_locale loc
  5.1734 -    (fn (axiom, elems, params, decls, regs, intros, dests) =>
  5.1735 -      (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
  5.1736 -  add_thmss loc Thm.internalK
  5.1737 -    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  5.1738 -
  5.1739 -in
  5.1740 -
  5.1741 -val add_type_syntax = add_decls (apfst o cons);
  5.1742 -val add_term_syntax = add_decls (apsnd o cons);
  5.1743 -val add_declaration = add_decls (K I);
  5.1744 -
  5.1745 -fun declarations_of thy loc =
  5.1746 -  the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst);
  5.1747 -
  5.1748 -end;
  5.1749 -
  5.1750 -
  5.1751 -
  5.1752 -(** define locales **)
  5.1753 -
  5.1754 -(* predicate text *)
  5.1755 -(* CB: generate locale predicates and delta predicates *)
  5.1756 -
  5.1757 -local
  5.1758 -
  5.1759 -(* introN: name of theorems for introduction rules of locale and
  5.1760 -     delta predicates;
  5.1761 -   axiomsN: name of theorem set with destruct rules for locale predicates,
  5.1762 -     also name suffix of delta predicates. *)
  5.1763 -
  5.1764 -val introN = "intro";
  5.1765 -val axiomsN = "axioms";
  5.1766 -
  5.1767 -fun atomize_spec thy ts =
  5.1768 -  let
  5.1769 -    val t = Logic.mk_conjunction_balanced ts;
  5.1770 -    val body = ObjectLogic.atomize_term thy t;
  5.1771 -    val bodyT = Term.fastype_of body;
  5.1772 -  in
  5.1773 -    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
  5.1774 -    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
  5.1775 -  end;
  5.1776 -
  5.1777 -fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
  5.1778 -  if length args = n then
  5.1779 -    Syntax.const "_aprop" $
  5.1780 -      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
  5.1781 -  else raise Match);
  5.1782 -
  5.1783 -(* CB: define one predicate including its intro rule and axioms
  5.1784 -   - bname: predicate name
  5.1785 -   - parms: locale parameters
  5.1786 -   - defs: thms representing substitutions from defines elements
  5.1787 -   - ts: terms representing locale assumptions (not normalised wrt. defs)
  5.1788 -   - norm_ts: terms representing locale assumptions (normalised wrt. defs)
  5.1789 -   - thy: the theory
  5.1790 -*)
  5.1791 -
  5.1792 -fun def_pred bname parms defs ts norm_ts thy =
  5.1793 -  let
  5.1794 -    val name = Sign.full_bname thy bname;
  5.1795 -
  5.1796 -    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  5.1797 -    val env = Term.add_free_names body [];
  5.1798 -    val xs = filter (member (op =) env o #1) parms;
  5.1799 -    val Ts = map #2 xs;
  5.1800 -    val extraTs =
  5.1801 -      (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
  5.1802 -      |> Library.sort_wrt #1 |> map TFree;
  5.1803 -    val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
  5.1804 -
  5.1805 -    val args = map Logic.mk_type extraTs @ map Free xs;
  5.1806 -    val head = Term.list_comb (Const (name, predT), args);
  5.1807 -    val statement = ObjectLogic.ensure_propT thy head;
  5.1808 -
  5.1809 -    val ([pred_def], defs_thy) =
  5.1810 -      thy
  5.1811 -      |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
  5.1812 -      |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
  5.1813 -      |> PureThy.add_defs false
  5.1814 -        [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
  5.1815 -    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  5.1816 -
  5.1817 -    val cert = Thm.cterm_of defs_thy;
  5.1818 -
  5.1819 -    val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
  5.1820 -      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
  5.1821 -      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
  5.1822 -      Tactic.compose_tac (false,
  5.1823 -        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
  5.1824 -
  5.1825 -    val conjuncts =
  5.1826 -      (Drule.equal_elim_rule2 OF [body_eq,
  5.1827 -        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
  5.1828 -      |> Conjunction.elim_balanced (length ts);
  5.1829 -    val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
  5.1830 -      Element.prove_witness defs_ctxt t
  5.1831 -       (MetaSimplifier.rewrite_goals_tac defs THEN
  5.1832 -        Tactic.compose_tac (false, ax, 0) 1));
  5.1833 -  in ((statement, intro, axioms), defs_thy) end;
  5.1834 -
  5.1835 -fun assumes_to_notes (Assumes asms) axms =
  5.1836 -      fold_map (fn (a, spec) => fn axs =>
  5.1837 -          let val (ps, qs) = chop (length spec) axs
  5.1838 -          in ((a, [(ps, [])]), qs) end) asms axms
  5.1839 -      |> apfst (curry Notes Thm.assumptionK)
  5.1840 -  | assumes_to_notes e axms = (e, axms);
  5.1841 -
  5.1842 -(* CB: the following two change only "new" elems, these have identifier ("", _). *)
  5.1843 -
  5.1844 -(* turn Assumes into Notes elements *)
  5.1845 -
  5.1846 -fun change_assumes_elemss axioms elemss =
  5.1847 -  let
  5.1848 -    val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  5.1849 -    fun change (id as ("", _), es) =
  5.1850 -          fold_map assumes_to_notes (map satisfy es)
  5.1851 -          #-> (fn es' => pair (id, es'))
  5.1852 -      | change e = pair e;
  5.1853 -  in
  5.1854 -    fst (fold_map change elemss (map Element.conclude_witness axioms))
  5.1855 -  end;
  5.1856 -
  5.1857 -(* adjust hyps of Notes elements *)
  5.1858 -
  5.1859 -fun change_elemss_hyps axioms elemss =
  5.1860 -  let
  5.1861 -    val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
  5.1862 -    fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
  5.1863 -      | change e = e;
  5.1864 -  in map change elemss end;
  5.1865 -
  5.1866 -in
  5.1867 -
  5.1868 -(* CB: main predicate definition function *)
  5.1869 -
  5.1870 -fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  5.1871 -  let
  5.1872 -    val ((elemss', more_ts), a_elem, a_intro, thy'') =
  5.1873 -      if null exts then ((elemss, []), [], [], thy)
  5.1874 -      else
  5.1875 -        let
  5.1876 -          val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
  5.1877 -          val ((statement, intro, axioms), thy') =
  5.1878 -            thy
  5.1879 -            |> def_pred aname parms defs exts exts';
  5.1880 -          val elemss' = change_assumes_elemss axioms elemss;
  5.1881 -          val a_elem = [(("", []),
  5.1882 -            [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  5.1883 -          val (_, thy'') =
  5.1884 -            thy'
  5.1885 -            |> Sign.add_path aname
  5.1886 -            |> Sign.no_base_names
  5.1887 -            |> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])]
  5.1888 -            ||> Sign.restore_naming thy';
  5.1889 -        in ((elemss', [statement]), a_elem, [intro], thy'') end;
  5.1890 -    val (predicate, stmt', elemss'', b_intro, thy'''') =
  5.1891 -      if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
  5.1892 -      else
  5.1893 -        let
  5.1894 -          val ((statement, intro, axioms), thy''') =
  5.1895 -            thy''
  5.1896 -            |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts);
  5.1897 -          val cstatement = Thm.cterm_of thy''' statement;
  5.1898 -          val elemss'' = change_elemss_hyps axioms elemss';
  5.1899 -          val b_elem = [(("", []),
  5.1900 -               [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  5.1901 -          val (_, thy'''') =
  5.1902 -            thy'''
  5.1903 -            |> Sign.add_path pname
  5.1904 -            |> Sign.no_base_names
  5.1905 -            |> PureThy.note_thmss Thm.internalK
  5.1906 -                 [((Binding.name introN, []), [([intro], [])]),
  5.1907 -                  ((Binding.name axiomsN, []),
  5.1908 -                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  5.1909 -            ||> Sign.restore_naming thy''';
  5.1910 -        in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
  5.1911 -  in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
  5.1912 -
  5.1913 -end;
  5.1914 -
  5.1915 -
  5.1916 -(* add_locale(_i) *)
  5.1917 -
  5.1918 -local
  5.1919 -
  5.1920 -(* turn Defines into Notes elements, accumulate definition terms *)
  5.1921 -
  5.1922 -fun defines_to_notes is_ext thy (Defines defs) defns =
  5.1923 -    let
  5.1924 -      val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs
  5.1925 -      val notes = map (fn (a, (def, _)) =>
  5.1926 -        (a, [([assume (cterm_of thy def)], [])])) defs
  5.1927 -    in
  5.1928 -      (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
  5.1929 -    end
  5.1930 -  | defines_to_notes _ _ e defns = (SOME e, defns);
  5.1931 -
  5.1932 -fun change_defines_elemss thy elemss defns =
  5.1933 -  let
  5.1934 -    fun change (id as (n, _), es) defns =
  5.1935 -        let
  5.1936 -          val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
  5.1937 -        in ((id, map_filter I es'), defns') end
  5.1938 -  in fold_map change elemss defns end;
  5.1939 -
  5.1940 -fun gen_add_locale prep_ctxt prep_expr
  5.1941 -    predicate_name bname raw_imports raw_body thy =
  5.1942 -    (* predicate_name: "" - locale with predicate named as locale
  5.1943 -        "name" - locale with predicate named "name" *)
  5.1944 -  let
  5.1945 -    val thy_ctxt = ProofContext.init thy;
  5.1946 -    val name = Sign.full_bname thy bname;
  5.1947 -    val _ = is_some (get_locale thy name) andalso
  5.1948 -      error ("Duplicate definition of locale " ^ quote name);
  5.1949 -
  5.1950 -    val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  5.1951 -      text as (parms, ((_, exts'), _), defs)) =
  5.1952 -        prep_ctxt raw_imports raw_body thy_ctxt;
  5.1953 -    val elemss = import_elemss @ body_elemss |>
  5.1954 -      map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  5.1955 -
  5.1956 -    val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\
  5.1957 -      List.foldr OldTerm.add_typ_tfrees [] (map snd parms);
  5.1958 -    val _ = if null extraTs then ()
  5.1959 -      else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  5.1960 -
  5.1961 -    val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
  5.1962 -    val (elemss', defns) = change_defines_elemss thy elemss [];
  5.1963 -    val elemss'' = elemss' @ [(("", []), defns)];
  5.1964 -    val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
  5.1965 -      define_preds predicate_name' text elemss'' thy;
  5.1966 -    val regs = pred_axioms
  5.1967 -      |> fold_map (fn (id, elems) => fn wts => let
  5.1968 -             val ts = flat (map_filter (fn (Assumes asms) =>
  5.1969 -               SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  5.1970 -             val (wts1, wts2) = chop (length ts) wts;
  5.1971 -           in ((apsnd (map fst) id, wts1), wts2) end) elemss'''
  5.1972 -      |> fst
  5.1973 -      |> map_filter (fn (("", _), _) => NONE | e => SOME e);
  5.1974 -    fun axiomify axioms elemss =
  5.1975 -      (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  5.1976 -                   val ts = flat (map_filter (fn (Assumes asms) =>
  5.1977 -                     SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  5.1978 -                   val (axs1, axs2) = chop (length ts) axs;
  5.1979 -                 in (axs2, ((id, Assumed axs1), elems)) end)
  5.1980 -      |> snd;
  5.1981 -    val ((_, facts), ctxt) = activate_facts true (K I)
  5.1982 -      (axiomify pred_axioms elemss''') (ProofContext.init thy');
  5.1983 -    val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
  5.1984 -    val export = Thm.close_derivation o Goal.norm_result o
  5.1985 -      singleton (ProofContext.export view_ctxt thy_ctxt);
  5.1986 -    val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  5.1987 -    val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss''');
  5.1988 -    val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  5.1989 -    val axs' = map (Element.assume_witness thy') stmt';
  5.1990 -    val loc_ctxt = thy'
  5.1991 -      |> Sign.add_path bname
  5.1992 -      |> Sign.no_base_names
  5.1993 -      |> PureThy.note_thmss Thm.assumptionK facts' |> snd
  5.1994 -      |> Sign.restore_naming thy'
  5.1995 -      |> register_locale bname {axiom = axs',
  5.1996 -        elems = map (fn e => (e, stamp ())) elems'',
  5.1997 -        params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  5.1998 -        decls = ([], []),
  5.1999 -        regs = regs,
  5.2000 -        intros = intros,
  5.2001 -        dests = map Element.conclude_witness pred_axioms}
  5.2002 -      |> init name;
  5.2003 -  in (name, loc_ctxt) end;
  5.2004 -
  5.2005 -in
  5.2006 -
  5.2007 -val add_locale = gen_add_locale cert_context (K I);
  5.2008 -val add_locale_cmd = gen_add_locale read_context intern_expr "";
  5.2009 -
  5.2010 -end;
  5.2011 -
  5.2012 -val _ = Context.>> (Context.map_theory
  5.2013 - (add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #>
  5.2014 -  snd #> ProofContext.theory_of #>
  5.2015 -  add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #>
  5.2016 -  snd #> ProofContext.theory_of));
  5.2017 -
  5.2018 -
  5.2019 -
  5.2020 -
  5.2021 -(** Normalisation of locale statements ---
  5.2022 -    discharges goals implied by interpretations **)
  5.2023 -
  5.2024 -local
  5.2025 -
  5.2026 -fun locale_assm_intros thy =
  5.2027 -  Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
  5.2028 -    (#2 (LocalesData.get thy)) [];
  5.2029 -fun locale_base_intros thy =
  5.2030 -  Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
  5.2031 -    (#2 (LocalesData.get thy)) [];
  5.2032 -
  5.2033 -fun all_witnesses ctxt =
  5.2034 -  let
  5.2035 -    val thy = ProofContext.theory_of ctxt;
  5.2036 -    fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
  5.2037 -        (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) =>
  5.2038 -          map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms)
  5.2039 -      registrations [];
  5.2040 -  in get (RegistrationsData.get (Context.Proof ctxt)) end;
  5.2041 -
  5.2042 -in
  5.2043 -
  5.2044 -fun intro_locales_tac eager ctxt facts st =
  5.2045 -  let
  5.2046 -    val wits = all_witnesses ctxt;
  5.2047 -    val thy = ProofContext.theory_of ctxt;
  5.2048 -    val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
  5.2049 -  in
  5.2050 -    Method.intros_tac (wits @ intros) facts st
  5.2051 -  end;
  5.2052 -
  5.2053 -end;
  5.2054 -
  5.2055 -
  5.2056 -(** Interpretation commands **)
  5.2057 -
  5.2058 -local
  5.2059 -
  5.2060 -(* extract proof obligations (assms and defs) from elements *)
  5.2061 -
  5.2062 -fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
  5.2063 -  | extract_asms_elems ((id, Derived _), _) = (id, []);
  5.2064 -
  5.2065 -
  5.2066 -(* activate instantiated facts in theory or context *)
  5.2067 -
  5.2068 -fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn
  5.2069 -        phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
  5.2070 -  let
  5.2071 -    val ctxt = mk_ctxt thy_ctxt;
  5.2072 -    fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
  5.2073 -    fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt);
  5.2074 -
  5.2075 -    val (all_propss, eq_props) = chop (length all_elemss) propss;
  5.2076 -    val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
  5.2077 -
  5.2078 -    (* Filter out fragments already registered. *)
  5.2079 -
  5.2080 -    val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
  5.2081 -          test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss))));
  5.2082 -    val (new_pss, ys) = split_list xs;
  5.2083 -    val (new_propss, new_thmss) = split_list ys;
  5.2084 -
  5.2085 -    val thy_ctxt' = thy_ctxt
  5.2086 -      (* add registrations *)
  5.2087 -      |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp))
  5.2088 -           new_elemss new_pss
  5.2089 -      (* add witnesses of Assumed elements (only those generate proof obligations) *)
  5.2090 -      |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss
  5.2091 -      (* add equations *)
  5.2092 -      |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props
  5.2093 -          ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
  5.2094 -            Element.conclude_witness) eq_thms);
  5.2095 -
  5.2096 -    val prems = flat (map_filter
  5.2097 -          (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
  5.2098 -            | ((_, Derived _), _) => NONE) all_elemss);
  5.2099 -
  5.2100 -    val thy_ctxt'' = thy_ctxt'
  5.2101 -      (* add witnesses of Derived elements *)
  5.2102 -      |> fold (fn (id, thms) => fold
  5.2103 -           (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
  5.2104 -         (map_filter (fn ((_, Assumed _), _) => NONE
  5.2105 -            | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
  5.2106 -
  5.2107 -    fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
  5.2108 -        let
  5.2109 -          val ctxt = mk_ctxt thy_ctxt;
  5.2110 -          val thy = ProofContext.theory_of ctxt;
  5.2111 -          val facts' = facts
  5.2112 -            |> activate_note thy phi_name param_prfx
  5.2113 -                 (attrib thy_ctxt) insts prems eqns exp;
  5.2114 -        in 
  5.2115 -          thy_ctxt
  5.2116 -          |> note kind facts'
  5.2117 -          |> snd
  5.2118 -        end
  5.2119 -      | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
  5.2120 -
  5.2121 -    fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt =
  5.2122 -      let
  5.2123 -        val ctxt = mk_ctxt thy_ctxt;
  5.2124 -        val thy = ProofContext.theory_of ctxt;
  5.2125 -        val {params, elems, ...} = the_locale thy loc;
  5.2126 -        val parms = map fst params;
  5.2127 -        val param_prfx = param_prefix loc ps;
  5.2128 -        val ids = flatten (ProofContext.init thy, intern_expr thy)
  5.2129 -          (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
  5.2130 -        val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
  5.2131 -      in
  5.2132 -        thy_ctxt
  5.2133 -        |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems
  5.2134 -      end;
  5.2135 -
  5.2136 -  in
  5.2137 -    thy_ctxt''
  5.2138 -    (* add equations as lemmas to context *)
  5.2139 -    |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
  5.2140 -         ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
  5.2141 -            (unflat eq_thms eq_attns) eq_thms
  5.2142 -    (* add interpreted facts *)
  5.2143 -    |> fold2 activate_elems new_elemss new_pss
  5.2144 -  end;
  5.2145 -
  5.2146 -fun global_activate_facts_elemss x = gen_activate_facts_elemss
  5.2147 -  ProofContext.init
  5.2148 -  global_note_qualified
  5.2149 -  Attrib.attribute_i
  5.2150 -  put_global_registration
  5.2151 -  add_global_witness
  5.2152 -  add_global_equation
  5.2153 -  x;
  5.2154 -
  5.2155 -fun local_activate_facts_elemss x = gen_activate_facts_elemss
  5.2156 -  I
  5.2157 -  local_note_qualified
  5.2158 -  (Attrib.attribute_i o ProofContext.theory_of)
  5.2159 -  put_local_registration
  5.2160 -  add_local_witness
  5.2161 -  add_local_equation
  5.2162 -  x;
  5.2163 -
  5.2164 -fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
  5.2165 -  let
  5.2166 -    (* parameters *)
  5.2167 -    val (parm_names, parm_types) = parms |> split_list
  5.2168 -      ||> map (TypeInfer.paramify_vars o Logic.varifyT);
  5.2169 -    val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar);
  5.2170 -    val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
  5.2171 -
  5.2172 -    (* parameter instantiations *)
  5.2173 -    val d = length parms - length insts;
  5.2174 -    val insts =
  5.2175 -      if d < 0 then error "More arguments than parameters in instantiation."
  5.2176 -      else insts @ replicate d NONE;
  5.2177 -    val (given_ps, given_insts) =
  5.2178 -      ((parm_names ~~ parm_types) ~~ insts) |> map_filter
  5.2179 -          (fn (_, NONE) => NONE
  5.2180 -            | ((n, T), SOME inst) => SOME ((n, T), inst))
  5.2181 -        |> split_list;
  5.2182 -    val (given_parm_names, given_parm_types) = given_ps |> split_list;
  5.2183 -
  5.2184 -    (* parse insts / eqns *)
  5.2185 -    val given_insts' = map (parse_term ctxt) given_insts;
  5.2186 -    val eqns' = map (parse_prop ctxt) eqns;
  5.2187 -
  5.2188 -    (* type inference and contexts *)
  5.2189 -    val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns';
  5.2190 -    val res = Syntax.check_terms ctxt arg;
  5.2191 -    val ctxt' = ctxt |> fold Variable.auto_fixes res;
  5.2192 -
  5.2193 -    (* instantiation *)
  5.2194 -    val (type_parms'', res') = chop (length type_parms) res;
  5.2195 -    val (given_insts'', eqns'') = chop (length given_insts) res';
  5.2196 -    val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
  5.2197 -    val inst = Symtab.make (given_parm_names ~~ given_insts'');
  5.2198 -
  5.2199 -    (* export from eigencontext *)
  5.2200 -    val export = Variable.export_morphism ctxt' ctxt;
  5.2201 -
  5.2202 -    (* import, its inverse *)
  5.2203 -    val domT = fold Term.add_tfrees res [] |> map TFree;
  5.2204 -    val importT = domT |> map (fn x => (Morphism.typ export x, x))
  5.2205 -      |> map_filter (fn (TFree _, _) => NONE  (* fixed point of export *)
  5.2206 -               | (TVar y, x) => SOME (fst y, x)
  5.2207 -               | _ => error "internal: illegal export in interpretation")
  5.2208 -      |> Vartab.make;
  5.2209 -    val dom = fold Term.add_frees res [] |> map Free;
  5.2210 -    val imprt = dom |> map (fn x => (Morphism.term export x, x))
  5.2211 -      |> map_filter (fn (Free _, _) => NONE  (* fixed point of export *)
  5.2212 -               | (Var y, x) => SOME (fst y, x)
  5.2213 -               | _ => error "internal: illegal export in interpretation")
  5.2214 -      |> Vartab.make;
  5.2215 -  in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end;
  5.2216 -
  5.2217 -val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
  5.2218 -val check_instantiations = prep_instantiations (K I) (K I);
  5.2219 -
  5.2220 -fun gen_prep_registration mk_ctxt test_reg activate
  5.2221 -    prep_attr prep_expr prep_insts
  5.2222 -    thy_ctxt phi_name raw_expr raw_insts =
  5.2223 -  let
  5.2224 -    val ctxt = mk_ctxt thy_ctxt;
  5.2225 -    val thy = ProofContext.theory_of ctxt;
  5.2226 -    val ctxt' = ProofContext.init thy;
  5.2227 -    fun prep_attn attn = (apsnd o map)
  5.2228 -      (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
  5.2229 -
  5.2230 -    val expr = prep_expr thy raw_expr;
  5.2231 -
  5.2232 -    val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
  5.2233 -    val params_ids = make_params_ids (#1 pts);
  5.2234 -    val raw_params_elemss = make_raw_params_elemss pts;
  5.2235 -    val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr);
  5.2236 -    val ((parms, all_elemss, _), (_, (_, defs, _))) =
  5.2237 -      read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
  5.2238 -
  5.2239 -    (** compute instantiation **)
  5.2240 -
  5.2241 -    (* consistency check: equations need to be stored in a particular locale,
  5.2242 -       therefore if equations are present locale expression must be a name *)
  5.2243 -
  5.2244 -    val _ = case (expr, snd raw_insts) of
  5.2245 -        (Locale _, _) => () | (_, []) => ()
  5.2246 -      | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
  5.2247 -
  5.2248 -    (* read or certify instantiation *)
  5.2249 -    val (raw_insts', raw_eqns) = raw_insts;
  5.2250 -    val (raw_eq_attns, raw_eqns') = split_list raw_eqns;
  5.2251 -    val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns');
  5.2252 -    val eq_attns = map prep_attn raw_eq_attns;
  5.2253 -
  5.2254 -    (* defined params without given instantiation *)
  5.2255 -    val not_given = filter_out (Symtab.defined inst1 o fst) parms;
  5.2256 -    fun add_def (p, pT) inst =
  5.2257 -      let
  5.2258 -        val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  5.2259 -               NONE => error ("Instance missing for parameter " ^ quote p)
  5.2260 -             | SOME (Free (_, T), t) => (t, T);
  5.2261 -        val d = Element.inst_term (instT, inst) t;
  5.2262 -      in Symtab.update_new (p, d) inst end;
  5.2263 -    val inst2 = fold add_def not_given inst1;
  5.2264 -    val inst_morphism = Element.inst_morphism thy (instT, inst2);
  5.2265 -    (* Note: insts contain no vars. *)
  5.2266 -
  5.2267 -    (** compute proof obligations **)
  5.2268 -
  5.2269 -    (* restore "small" ids *)
  5.2270 -    val ids' = map (fn ((n, ps), (_, mode)) =>
  5.2271 -          ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
  5.2272 -        ids;
  5.2273 -    val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
  5.2274 -    (* instantiate ids and elements *)
  5.2275 -    val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  5.2276 -      ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
  5.2277 -        map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
  5.2278 -      |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
  5.2279 -
  5.2280 -    (* equations *)
  5.2281 -    val eqn_elems = if null eqns then []
  5.2282 -      else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
  5.2283 -
  5.2284 -    val propss = map extract_asms_elems inst_elemss @ eqn_elems;
  5.2285 -
  5.2286 -  in
  5.2287 -    (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
  5.2288 -  end;
  5.2289 -
  5.2290 -fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
  5.2291 -  test_global_registration
  5.2292 -  global_activate_facts_elemss mk_ctxt;
  5.2293 -
  5.2294 -fun gen_prep_local_registration mk_ctxt = gen_prep_registration I
  5.2295 -  test_local_registration
  5.2296 -  local_activate_facts_elemss mk_ctxt;
  5.2297 -
  5.2298 -val prep_global_registration = gen_prep_global_registration
  5.2299 -  (K I) (K I) check_instantiations;
  5.2300 -val prep_global_registration_cmd = gen_prep_global_registration
  5.2301 -  Attrib.intern_src intern_expr read_instantiations;
  5.2302 -
  5.2303 -val prep_local_registration = gen_prep_local_registration
  5.2304 -  (K I) (K I) check_instantiations;
  5.2305 -val prep_local_registration_cmd = gen_prep_local_registration
  5.2306 -  Attrib.intern_src intern_expr read_instantiations;
  5.2307 -
  5.2308 -fun prep_registration_in_locale target expr thy =
  5.2309 -  (* target already in internal form *)
  5.2310 -  let
  5.2311 -    val ctxt = ProofContext.init thy;
  5.2312 -    val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
  5.2313 -        (([], Symtab.empty), Expr (Locale target));
  5.2314 -    val fixed = the_locale thy target |> #params |> map #1;
  5.2315 -    val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  5.2316 -        ((raw_target_ids, target_syn), Expr expr);
  5.2317 -    val (target_ids, ids) = chop (length raw_target_ids) all_ids;
  5.2318 -    val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
  5.2319 -
  5.2320 -    (** compute proof obligations **)
  5.2321 -
  5.2322 -    (* restore "small" ids, with mode *)
  5.2323 -    val ids' = map (apsnd snd) ids;
  5.2324 -    (* remove Int markers *)
  5.2325 -    val elemss' = map (fn (_, es) =>
  5.2326 -        map (fn Int e => e) es) elemss
  5.2327 -    (* extract assumptions and defs *)
  5.2328 -    val ids_elemss = ids' ~~ elemss';
  5.2329 -    val propss = map extract_asms_elems ids_elemss;
  5.2330 -
  5.2331 -    (** activation function:
  5.2332 -        - add registrations to the target locale
  5.2333 -        - add induced registrations for all global registrations of
  5.2334 -          the target, unless already present
  5.2335 -        - add facts of induced registrations to theory **)
  5.2336 -
  5.2337 -    fun activate thmss thy =
  5.2338 -      let
  5.2339 -        val satisfy = Element.satisfy_thm (flat thmss);
  5.2340 -        val ids_elemss_thmss = ids_elemss ~~ thmss;
  5.2341 -        val regs = get_global_registrations thy target;
  5.2342 -
  5.2343 -        fun activate_id (((id, Assumed _), _), thms) thy =
  5.2344 -            thy |> put_registration_in_locale target id
  5.2345 -                |> fold (add_witness_in_locale target id) thms
  5.2346 -          | activate_id _ thy = thy;
  5.2347 -
  5.2348 -        fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
  5.2349 -          let
  5.2350 -            val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
  5.2351 -            val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts));
  5.2352 -            val disch = Element.satisfy_thm wits;
  5.2353 -            val new_elemss = filter (fn (((name, ps), _), _) =>
  5.2354 -                not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
  5.2355 -            fun activate_assumed_id (((_, Derived _), _), _) thy = thy
  5.2356 -              | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
  5.2357 -                val ps' = inst_parms ps;
  5.2358 -              in
  5.2359 -                if test_global_registration thy (name, ps')
  5.2360 -                then thy
  5.2361 -                else thy
  5.2362 -                  |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  5.2363 -                  |> fold (fn witn => fn thy => add_global_witness (name, ps')
  5.2364 -                     (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
  5.2365 -              end;
  5.2366 -
  5.2367 -            fun activate_derived_id ((_, Assumed _), _) thy = thy
  5.2368 -              | activate_derived_id (((name, ps), Derived ths), _) thy = let
  5.2369 -                val ps' = inst_parms ps;
  5.2370 -              in
  5.2371 -                if test_global_registration thy (name, ps')
  5.2372 -                then thy
  5.2373 -                else thy
  5.2374 -                  |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
  5.2375 -                  |> fold (fn witn => fn thy => add_global_witness (name, ps')
  5.2376 -                       (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
  5.2377 -                       (Element.inst_term insts t,
  5.2378 -                        disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
  5.2379 -              end;
  5.2380 -
  5.2381 -            fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
  5.2382 -                let
  5.2383 -                  val att_morphism =
  5.2384 -                    Morphism.binding_morphism (name_morph phi_name param_prfx) $>
  5.2385 -                    Morphism.thm_morphism satisfy $>
  5.2386 -                    Element.inst_morphism thy insts $>
  5.2387 -                    Morphism.thm_morphism disch;
  5.2388 -                  val facts' = facts
  5.2389 -                    |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
  5.2390 -                    |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
  5.2391 -                    |> (map o apfst o apfst) (name_morph phi_name param_prfx);
  5.2392 -                in
  5.2393 -                  thy
  5.2394 -                  |> global_note_qualified kind facts'
  5.2395 -                  |> snd
  5.2396 -                end
  5.2397 -              | activate_elem _ _ thy = thy;
  5.2398 -
  5.2399 -            fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
  5.2400 -
  5.2401 -          in thy |> fold activate_assumed_id ids_elemss_thmss
  5.2402 -                 |> fold activate_derived_id ids_elemss
  5.2403 -                 |> fold activate_elems new_elemss end;
  5.2404 -      in
  5.2405 -        thy |> fold activate_id ids_elemss_thmss
  5.2406 -            |> fold activate_reg regs
  5.2407 -      end;
  5.2408 -
  5.2409 -  in (propss, activate) end;
  5.2410 -
  5.2411 -fun prep_propp propss = propss |> map (fn (_, props) =>
  5.2412 -  map (rpair [] o Element.mark_witness) props);
  5.2413 -
  5.2414 -fun prep_result propps thmss =
  5.2415 -  ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
  5.2416 -
  5.2417 -fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
  5.2418 -  let
  5.2419 -    val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
  5.2420 -    fun after_qed' results =
  5.2421 -      ProofContext.theory (activate (prep_result propss results))
  5.2422 -      #> after_qed;
  5.2423 -  in
  5.2424 -    thy
  5.2425 -    |> ProofContext.init
  5.2426 -    |> Proof.theorem_i NONE after_qed' (prep_propp propss)
  5.2427 -    |> Element.refine_witness
  5.2428 -    |> Seq.hd
  5.2429 -    |> pair morphs
  5.2430 -  end;
  5.2431 -
  5.2432 -fun gen_interpret prep_registration after_qed name_morph expr insts int state =
  5.2433 -  let
  5.2434 -    val _ = Proof.assert_forward_or_chain state;
  5.2435 -    val ctxt = Proof.context_of state;
  5.2436 -    val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts;
  5.2437 -    fun after_qed' results =
  5.2438 -      Proof.map_context (K (ctxt |> activate (prep_result propss results)))
  5.2439 -      #> Proof.put_facts NONE
  5.2440 -      #> after_qed;
  5.2441 -  in
  5.2442 -    state
  5.2443 -    |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  5.2444 -      "interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss))
  5.2445 -    |> Element.refine_witness |> Seq.hd
  5.2446 -    |> pair morphs
  5.2447 -  end;
  5.2448 -
  5.2449 -fun standard_name_morph interp_prfx b =
  5.2450 -  if Binding.is_empty b then b
  5.2451 -  else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
  5.2452 -    fold (Binding.add_prefix false o fst) pprfx
  5.2453 -    #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
  5.2454 -    #> Binding.add_prefix false lprfx
  5.2455 -  ) b;
  5.2456 -
  5.2457 -in
  5.2458 -
  5.2459 -val interpretation = gen_interpretation prep_global_registration;
  5.2460 -fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd
  5.2461 -  I (standard_name_morph interp_prfx);
  5.2462 -
  5.2463 -fun interpretation_in_locale after_qed (raw_target, expr) thy =
  5.2464 -  let
  5.2465 -    val target = intern thy raw_target;
  5.2466 -    val (propss, activate) = prep_registration_in_locale target expr thy;
  5.2467 -    val raw_propp = prep_propp propss;
  5.2468 -
  5.2469 -    val (_, _, goal_ctxt, propp) = thy
  5.2470 -      |> ProofContext.init
  5.2471 -      |> cert_context_statement (SOME target) [] raw_propp;
  5.2472 -
  5.2473 -    fun after_qed' results =
  5.2474 -      ProofContext.theory (activate (prep_result propss results))
  5.2475 -      #> after_qed;
  5.2476 -  in
  5.2477 -    goal_ctxt
  5.2478 -    |> Proof.theorem_i NONE after_qed' propp
  5.2479 -    |> Element.refine_witness |> Seq.hd
  5.2480 -  end;
  5.2481 -
  5.2482 -val interpret = gen_interpret prep_local_registration;
  5.2483 -fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
  5.2484 -  I (standard_name_morph interp_prfx);
  5.2485 -
  5.2486 -end;
  5.2487 -
  5.2488 -end;
     6.1 --- a/src/Pure/Isar/theory_target.ML	Wed Jan 21 16:47:02 2009 +0100
     6.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Jan 21 16:47:03 2009 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  signature THEORY_TARGET =
     6.6  sig
     6.7 -  val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool,
     6.8 +  val peek: local_theory -> {target: string, is_locale: bool,
     6.9      is_class: bool, instantiation: string list * (string * sort) list * sort,
    6.10      overloading: (string * (string * typ) * bool) list}
    6.11    val init: string option -> theory -> local_theory
    6.12 @@ -21,34 +21,17 @@
    6.13  structure TheoryTarget: THEORY_TARGET =
    6.14  struct
    6.15  
    6.16 -(* new locales *)
    6.17 -
    6.18 -fun locale_extern new_locale x = 
    6.19 -  if new_locale then Locale.extern x else Old_Locale.extern x;
    6.20 -fun locale_add_type_syntax new_locale x =
    6.21 -  if new_locale then Locale.add_type_syntax x else Old_Locale.add_type_syntax x;
    6.22 -fun locale_add_term_syntax new_locale x =
    6.23 -  if new_locale then Locale.add_term_syntax x else Old_Locale.add_term_syntax x;
    6.24 -fun locale_add_declaration new_locale x =
    6.25 -  if new_locale then Locale.add_declaration x else Old_Locale.add_declaration x;
    6.26 -fun locale_add_thmss new_locale x =
    6.27 -  if new_locale then Locale.add_thmss x else Old_Locale.add_thmss x;
    6.28 -fun locale_init new_locale x =
    6.29 -  if new_locale then Locale.init x else Old_Locale.init x;
    6.30 -fun locale_intern new_locale x =
    6.31 -  if new_locale then Locale.intern x else Old_Locale.intern x;
    6.32 -
    6.33  (* context data *)
    6.34  
    6.35 -datatype target = Target of {target: string, new_locale: bool, is_locale: bool,
    6.36 +datatype target = Target of {target: string, is_locale: bool,
    6.37    is_class: bool, instantiation: string list * (string * sort) list * sort,
    6.38    overloading: (string * (string * typ) * bool) list};
    6.39  
    6.40 -fun make_target target new_locale is_locale is_class instantiation overloading =
    6.41 -  Target {target = target, new_locale = new_locale, is_locale = is_locale,
    6.42 +fun make_target target is_locale is_class instantiation overloading =
    6.43 +  Target {target = target, is_locale = is_locale,
    6.44      is_class = is_class, instantiation = instantiation, overloading = overloading};
    6.45  
    6.46 -val global_target = make_target "" false false false ([], [], []) [];
    6.47 +val global_target = make_target "" false false ([], [], []) [];
    6.48  
    6.49  structure Data = ProofDataFun
    6.50  (
    6.51 @@ -64,7 +47,7 @@
    6.52  fun pretty_thy ctxt target is_locale is_class =
    6.53    let
    6.54      val thy = ProofContext.theory_of ctxt;
    6.55 -    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
    6.56 +    val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    6.57      val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    6.58        (#1 (ProofContext.inferred_fixes ctxt));
    6.59      val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    6.60 @@ -89,7 +72,7 @@
    6.61  
    6.62  (* target declarations *)
    6.63  
    6.64 -fun target_decl add (Target {target, new_locale, ...}) d lthy =
    6.65 +fun target_decl add (Target {target, ...}) d lthy =
    6.66    let
    6.67      val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
    6.68      val d0 = Morphism.form d';
    6.69 @@ -100,12 +83,12 @@
    6.70        |> LocalTheory.target (Context.proof_map d0)
    6.71      else
    6.72        lthy
    6.73 -      |> LocalTheory.target (add new_locale target d')
    6.74 +      |> LocalTheory.target (add target d')
    6.75    end;
    6.76  
    6.77 -val type_syntax = target_decl locale_add_type_syntax;
    6.78 -val term_syntax = target_decl locale_add_term_syntax;
    6.79 -val declaration = target_decl locale_add_declaration;
    6.80 +val type_syntax = target_decl Locale.add_type_syntax;
    6.81 +val term_syntax = target_decl Locale.add_term_syntax;
    6.82 +val declaration = target_decl Locale.add_declaration;
    6.83  
    6.84  fun class_target (Target {target, ...}) f =
    6.85    LocalTheory.raw_theory f #>
    6.86 @@ -166,7 +149,7 @@
    6.87    |> ProofContext.note_thmss_i kind facts
    6.88    ||> ProofContext.restore_naming ctxt;
    6.89  
    6.90 -fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy =
    6.91 +fun notes (Target {target, is_locale, ...}) kind facts lthy =
    6.92    let
    6.93      val thy = ProofContext.theory_of lthy;
    6.94      val facts' = facts
    6.95 @@ -185,7 +168,7 @@
    6.96          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    6.97          #> Sign.restore_naming thy)
    6.98      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    6.99 -    |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts)
   6.100 +    |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
   6.101      |> note_local kind local_facts
   6.102    end;
   6.103  
   6.104 @@ -313,7 +296,7 @@
   6.105            (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
   6.106        | NONE =>
   6.107            if is_none (Class_Target.instantiation_param lthy c)
   6.108 -          then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
   6.109 +          then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
   6.110            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
   6.111      val (global_def, lthy3) = lthy2
   6.112        |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
   6.113 @@ -335,13 +318,13 @@
   6.114  fun init_target _ NONE = global_target
   6.115    | init_target thy (SOME target) =
   6.116        make_target target (Locale.defined thy (Locale.intern thy target))
   6.117 -      true (Class_Target.is_class thy target) ([], [], []) [];
   6.118 +      (Class_Target.is_class thy target) ([], [], []) [];
   6.119  
   6.120 -fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
   6.121 +fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
   6.122    if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
   6.123    else if not (null overloading) then Overloading.init overloading
   6.124    else if not is_locale then ProofContext.init
   6.125 -  else if not is_class then locale_init new_locale target
   6.126 +  else if not is_class then Locale.init target
   6.127    else Class_Target.init target;
   6.128  
   6.129  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   6.130 @@ -375,7 +358,7 @@
   6.131      val ctxt = ProofContext.init thy;
   6.132      val ops = raw_ops |> map (fn (name, const, checked) =>
   6.133        (name, Term.dest_Const (prep_const ctxt const), checked));
   6.134 -  in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end;
   6.135 +  in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
   6.136  
   6.137  in
   6.138  
   6.139 @@ -383,10 +366,9 @@
   6.140  fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
   6.141  
   6.142  fun context "-" thy = init NONE thy
   6.143 -  | context target thy = init (SOME (locale_intern
   6.144 -      (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
   6.145 +  | context target thy = init (SOME (Locale.intern thy target)) thy;
   6.146  
   6.147 -fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
   6.148 +fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
   6.149  fun instantiation_cmd raw_arities thy =
   6.150    instantiation (read_multi_arity thy raw_arities) thy;
   6.151  
     7.1 --- a/src/Pure/Tools/ROOT.ML	Wed Jan 21 16:47:02 2009 +0100
     7.2 +++ b/src/Pure/Tools/ROOT.ML	Wed Jan 21 16:47:03 2009 +0100
     7.3 @@ -9,8 +9,5 @@
     7.4  (*basic XML support*)
     7.5  use "xml_syntax.ML";
     7.6  
     7.7 -(*derived theory and proof elements*)
     7.8 -use "invoke.ML";
     7.9 -
    7.10  (*quickcheck needed here because of pg preferences*)
    7.11  use "../../Tools/quickcheck.ML"
     8.1 --- a/src/Pure/Tools/invoke.ML	Wed Jan 21 16:47:02 2009 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,127 +0,0 @@
     8.4 -(*  Title:      Pure/Tools/invoke.ML
     8.5 -    Author:     Makarius
     8.6 -
     8.7 -Schematic invocation of locale expression in proof context.
     8.8 -*)
     8.9 -
    8.10 -signature INVOKE =
    8.11 -sig
    8.12 -  val invoke: string * Attrib.src list -> Old_Locale.expr -> string option list ->
    8.13 -    (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    8.14 -  val invoke_i: string * attribute list -> Old_Locale.expr -> term option list ->
    8.15 -    (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    8.16 -end;
    8.17 -
    8.18 -structure Invoke: INVOKE =
    8.19 -struct
    8.20 -
    8.21 -
    8.22 -(* invoke *)
    8.23 -
    8.24 -local
    8.25 -
    8.26 -fun gen_invoke prep_att prep_expr parse_term add_fixes
    8.27 -    (prfx, raw_atts) raw_expr raw_insts fixes int state =
    8.28 -  let
    8.29 -    val thy = Proof.theory_of state;
    8.30 -    val _ = Proof.assert_forward_or_chain state;
    8.31 -    val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    8.32 -
    8.33 -    val more_atts = map (prep_att thy) raw_atts;
    8.34 -    val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy);
    8.35 -
    8.36 -    val prems = maps Element.prems_of elems;
    8.37 -    val params = maps Element.params_of elems;
    8.38 -    val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params []));
    8.39 -
    8.40 -    val prems' = map Logic.varify prems;
    8.41 -    val params' = map (Logic.varify o Free) params;
    8.42 -    val types' = map (Logic.varifyT o TFree) types;
    8.43 -
    8.44 -    val state' = state
    8.45 -      |> Proof.enter_forward
    8.46 -      |> Proof.begin_block
    8.47 -      |> Proof.map_context (snd o add_fixes fixes);
    8.48 -    val ctxt' = Proof.context_of state';
    8.49 -
    8.50 -    val raw_insts' = zip_options params' raw_insts
    8.51 -      handle Library.UnequalLengths => error "Too many instantiations";
    8.52 -
    8.53 -    fun prep_inst (t, u) =
    8.54 -      TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u);
    8.55 -    val insts = map #1 raw_insts' ~~
    8.56 -      Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts'));
    8.57 -    val inst_rules =
    8.58 -      replicate (length types') Drule.termI @
    8.59 -      map (fn t =>
    8.60 -        (case AList.lookup (op =) insts t of
    8.61 -          SOME u => Drule.mk_term (Thm.cterm_of thy u)
    8.62 -        | NONE => Drule.termI)) params';
    8.63 -
    8.64 -    val propp =
    8.65 -      [((Binding.empty, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
    8.66 -       ((Binding.empty, []), map (rpair [] o Logic.mk_term) params'),
    8.67 -       ((Binding.empty, []), map (rpair [] o Element.mark_witness) prems')];
    8.68 -    fun after_qed results =
    8.69 -      Proof.end_block #>
    8.70 -      Proof.map_context (fn ctxt =>
    8.71 -        let
    8.72 -          val ([res_types, res_params, res_prems], ctxt'') =
    8.73 -            fold_burrow (apfst snd oo Variable.import_thms false) results ctxt';
    8.74 -
    8.75 -          val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
    8.76 -          val params'' = map (Thm.term_of o Drule.dest_term) res_params;
    8.77 -          val inst = Element.morph_ctxt (Element.inst_morphism thy
    8.78 -            (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
    8.79 -          val elems' = map inst elems;
    8.80 -          val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
    8.81 -          val notes =
    8.82 -            maps (Element.facts_of thy) elems'
    8.83 -            |> Element.satisfy_facts prems''
    8.84 -            |> Element.generalize_facts ctxt'' ctxt
    8.85 -            |> Attrib.map_facts (Attrib.attribute_i thy)
    8.86 -            |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
    8.87 -        in
    8.88 -          ctxt
    8.89 -          |> ProofContext.sticky_prefix prfx
    8.90 -          |> ProofContext.qualified_names
    8.91 -          |> (snd o ProofContext.note_thmss_i "" notes)
    8.92 -          |> ProofContext.restore_naming ctxt
    8.93 -        end) #>
    8.94 -      Proof.put_facts NONE;
    8.95 -  in
    8.96 -    state'
    8.97 -    |> Proof.chain_facts chain_facts
    8.98 -    |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
    8.99 -      "invoke" NONE after_qed propp
   8.100 -    |> Element.refine_witness
   8.101 -    |> Seq.hd
   8.102 -    |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))),
   8.103 -      Position.none))
   8.104 -    |> Seq.hd
   8.105 -  end;
   8.106 -
   8.107 -in
   8.108 -
   8.109 -fun invoke x =
   8.110 -  gen_invoke Attrib.attribute Old_Locale.read_expr Syntax.parse_term ProofContext.add_fixes x;
   8.111 -fun invoke_i x = gen_invoke (K I) Old_Locale.cert_expr (K I) ProofContext.add_fixes_i x;
   8.112 -
   8.113 -end;
   8.114 -
   8.115 -
   8.116 -(* concrete syntax *)
   8.117 -
   8.118 -local structure P = OuterParse and K = OuterKeyword in
   8.119 -
   8.120 -val _ =
   8.121 -  OuterSyntax.command "invoke"
   8.122 -    "schematic invocation of locale expression in proof context"
   8.123 -    (K.tag_proof K.prf_goal)
   8.124 -    (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
   8.125 -      >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
   8.126 -          Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
   8.127 -
   8.128 -end;
   8.129 -
   8.130 -end;