src/Pure/Isar/locale.ML
author wenzelm
Fri Sep 15 22:56:13 2006 +0200 (2006-09-15)
changeset 20548 8ef25fe585a8
parent 20366 867696dc64fc
child 20664 ffbc5a57191a
permissions -rw-r--r--
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
     1 (*  Title:      Pure/Isar/locale.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
     4 
     5 Locales -- Isar proof contexts as meta-level predicates, with local
     6 syntax and implicit structures.
     7 
     8 Draws basic ideas from Florian Kammueller's original version of
     9 locales, but uses the richer infrastructure of Isar instead of the raw
    10 meta-logic.  Furthermore, structured import of contexts (with merge
    11 and rename operations) are provided, as well as type-inference of the
    12 signature parts, and predicate definitions of the specification text.
    13 
    14 Interpretation enables the reuse of theorems of locales in other
    15 contexts, namely those defined by theories, structured proofs and
    16 locales themselves.
    17 
    18 See also:
    19 
    20 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    21     In Stefano Berardi et al., Types for Proofs and Programs: International
    22     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    23 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    24     Dependencies between Locales. Technical Report TUM-I0607, Technische
    25     Universitaet Muenchen, 2006.
    26 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    27     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    28     pages 31-43, 2006.
    29 *)
    30 
    31 (* TODO:
    32 - beta-eta normalisation of interpretation parameters
    33 - dangling type frees in locales
    34 - test subsumption of interpretations when merging theories
    35 *)
    36 
    37 signature LOCALE =
    38 sig
    39   datatype expr =
    40     Locale of string |
    41     Rename of expr * (string * mixfix option) option list |
    42     Merge of expr list
    43   val empty: expr
    44   datatype 'a element = Elem of 'a | Expr of expr
    45 
    46   val intern: theory -> xstring -> string
    47   val extern: theory -> string -> xstring
    48   val init: string -> theory -> Proof.context
    49 
    50   (* The specification of a locale *)
    51 
    52   val parameters_of: theory -> string ->
    53     ((string * typ) * mixfix) list
    54   val parameters_of_expr: theory -> expr ->
    55     ((string * typ) * mixfix) list
    56   val local_asms_of: theory -> string ->
    57     ((string * Attrib.src list) * term list) list
    58   val global_asms_of: theory -> string ->
    59     ((string * Attrib.src list) * term list) list
    60 
    61   (* Processing of locale statements *)
    62   val read_context_statement: xstring option -> Element.context element list ->
    63     (string * string list) list list -> Proof.context ->
    64     string option * Proof.context * Proof.context * (term * term list) list list
    65   val cert_context_statement: string option -> Element.context_i element list ->
    66     (term * term list) list list -> Proof.context ->
    67     string option * Proof.context * Proof.context * (term * term list) list list
    68   val read_expr: expr -> Element.context list -> Proof.context ->
    69     Element.context_i list * Proof.context
    70   val cert_expr: expr -> Element.context_i list -> Proof.context ->
    71     Element.context_i list * Proof.context
    72 
    73   (* Diagnostic functions *)
    74   val print_locales: theory -> unit
    75   val print_locale: theory -> bool -> expr -> Element.context list -> unit
    76   val print_global_registrations: bool -> string -> theory -> unit
    77   val print_local_registrations': bool -> string -> Proof.context -> unit
    78   val print_local_registrations: bool -> string -> Proof.context -> unit
    79 
    80   val add_locale: bool -> bstring -> expr -> Element.context list -> theory
    81     -> (string * Proof.context (*body context!*)) * theory
    82   val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory
    83     -> (string * Proof.context (*body context!*)) * theory
    84 
    85   (* Storing results *)
    86   val note_thmss: string -> xstring ->
    87     ((string * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    88     theory -> ((string * thm list) list * (string * thm list) list) * Proof.context
    89   val note_thmss_i: string -> string ->
    90     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    91     theory -> ((string * thm list) list * (string * thm list) list) * Proof.context
    92   val add_thmss: string -> string ->
    93     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    94     Proof.context ->
    95     ((string * thm list) list * (string * thm list) list) * Proof.context
    96   val add_term_syntax: string -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context
    97 
    98   val theorem: string -> Method.text option ->
    99     (thm list list -> Proof.context -> Proof.context) ->
   100     string * Attrib.src list -> Element.context element list -> Element.statement ->
   101     theory -> Proof.state
   102   val theorem_i: string -> Method.text option ->
   103     (thm list list -> Proof.context -> Proof.context) ->
   104     string * Attrib.src list -> Element.context_i element list -> Element.statement_i ->
   105     theory -> Proof.state
   106   val theorem_in_locale: string -> Method.text option ->
   107     (thm list list -> thm list list -> Proof.context -> Proof.context) ->
   108     xstring -> string * Attrib.src list -> Element.context element list -> Element.statement ->
   109     theory -> Proof.state
   110   val theorem_in_locale_i: string -> Method.text option ->
   111     (thm list list -> thm list list -> Proof.context -> Proof.context) ->
   112     string -> string * Attrib.src list -> Element.context_i element list ->
   113     Element.statement_i -> theory -> Proof.state
   114   val smart_theorem: string -> xstring option ->
   115     string * Attrib.src list -> Element.context element list -> Element.statement ->
   116     theory -> Proof.state
   117   val interpretation: (Proof.context -> Proof.context) ->
   118     string * Attrib.src list -> expr -> string option list ->
   119     theory -> Proof.state
   120   val interpretation_in_locale: (Proof.context -> Proof.context) ->
   121     xstring * expr -> theory -> Proof.state
   122   val interpret: (Proof.state -> Proof.state Seq.seq) ->
   123     string * Attrib.src list -> expr -> string option list ->
   124     bool -> Proof.state -> Proof.state
   125 end;
   126 
   127 structure Locale: LOCALE =
   128 struct
   129 
   130 fun legacy_unvarifyT thm =
   131   let
   132     val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
   133     val tvars = rev (Drule.fold_terms Term.add_tvars thm []);
   134     val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
   135   in Drule.instantiate' tfrees [] thm end;
   136 
   137 fun legacy_unvarify raw_thm =
   138   let
   139     val thm = legacy_unvarifyT raw_thm;
   140     val ct = Thm.cterm_of (Thm.theory_of_thm thm);
   141     val vars = rev (Drule.fold_terms Term.add_vars thm []);
   142     val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
   143   in Drule.instantiate' [] frees thm end;
   144 
   145 
   146 (** locale elements and expressions **)
   147 
   148 datatype ctxt = datatype Element.ctxt;
   149 
   150 datatype expr =
   151   Locale of string |
   152   Rename of expr * (string * mixfix option) option list |
   153   Merge of expr list;
   154 
   155 val empty = Merge [];
   156 
   157 datatype 'a element =
   158   Elem of 'a | Expr of expr;
   159 
   160 fun map_elem f (Elem e) = Elem (f e)
   161   | map_elem _ (Expr e) = Expr e;
   162 
   163 type locale =
   164  {axiom: Element.witness list,
   165     (* For locales that define predicates this is [A [A]], where A is the locale
   166        specification.  Otherwise [].
   167        Only required to generate the right witnesses for locales with predicates. *)
   168   import: expr,                                                     (*dynamic import*)
   169   elems: (Element.context_i * stamp) list,
   170     (* Static content, neither Fixes nor Constrains elements *)
   171   params: ((string * typ) * mixfix) list,                           (*all params*)
   172   lparams: string list,                                             (*local params*)
   173   term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *)
   174   regs: ((string * string list) * Element.witness list) list,
   175     (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
   176   intros: thm list * thm list}
   177     (* Introduction rules: of delta predicate and locale predicate. *)
   178 
   179 (* CB: an internal (Int) locale element was either imported or included,
   180    an external (Ext) element appears directly in the locale text. *)
   181 
   182 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   183 
   184 
   185 
   186 (** management of registrations in theories and proof contexts **)
   187 
   188 structure Registrations :
   189   sig
   190     type T
   191     val empty: T
   192     val join: T * T -> T
   193     val dest: theory -> T ->
   194       (term list * ((string * Attrib.src list) * Element.witness list)) list
   195     val lookup: theory -> T * term list ->
   196       ((string * Attrib.src list) * Element.witness list) option
   197     val insert: theory -> term list * (string * Attrib.src list) -> T ->
   198       T * (term list * ((string * Attrib.src list) * Element.witness list)) list
   199     val add_witness: term list -> Element.witness -> T -> T
   200   end =
   201 struct
   202   (* a registration consists of theorems (actually, witnesses) instantiating locale
   203      assumptions and prefix and attributes, indexed by parameter instantiation *)
   204   type T = ((string * Attrib.src list) * Element.witness list) Termtab.table;
   205 
   206   val empty = Termtab.empty;
   207 
   208   (* term list represented as single term, for simultaneous matching *)
   209   fun termify ts =
   210     Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
   211   fun untermify t =
   212     let fun ut (Const _) ts = ts
   213           | ut (s $ t) ts = ut s (t::ts)
   214     in ut t [] end;
   215 
   216   (* joining of registrations: prefix and attributes of left theory,
   217      thms are equal, no attempt to subsumption testing *)
   218   fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);
   219 
   220   fun dest_transfer thy regs =
   221     Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy))));
   222 
   223   fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
   224 
   225   (* registrations that subsume t *)
   226   fun subsumers thy t regs =
   227     filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
   228 
   229   (* look up registration, pick one that subsumes the query *)
   230   fun lookup thy (regs, ts) =
   231     let
   232       val t = termify ts;
   233       val subs = subsumers thy t regs;
   234     in (case subs of
   235         [] => NONE
   236       | ((t', (attn, thms)) :: _) => let
   237             val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   238             (* thms contain Frees, not Vars *)
   239             val tinst' = tinst |> Vartab.dest
   240                  |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
   241                  |> Symtab.make;
   242             val inst' = inst |> Vartab.dest
   243                  |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
   244                  |> Symtab.make;
   245           in
   246             SOME (attn, map (Element.inst_witness thy (tinst', inst')) thms)
   247           end)
   248     end;
   249 
   250   (* add registration if not subsumed by ones already present,
   251      additionally returns registrations that are strictly subsumed *)
   252   fun insert thy (ts, attn) regs =
   253     let
   254       val t = termify ts;
   255       val subs = subsumers thy t regs ;
   256     in (case subs of
   257         [] => let
   258                 val sups =
   259                   filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   260                 val sups' = map (apfst untermify) sups
   261               in (Termtab.update (t, (attn, [])) regs, sups') end
   262       | _ => (regs, []))
   263     end;
   264 
   265   (* add witness theorem to registration,
   266      only if instantiation is exact, otherwise exception Option raised *)
   267   fun add_witness ts thm regs =
   268     let
   269       val t = termify ts;
   270       val (x, thms) = the (Termtab.lookup regs t);
   271     in
   272       Termtab.update (t, (x, thm::thms)) regs
   273     end;
   274 end;
   275 
   276 
   277 (** theory data **)
   278 
   279 structure GlobalLocalesData = TheoryDataFun
   280 (struct
   281   val name = "Isar/locales";
   282   type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
   283     (* 1st entry: locale namespace,
   284        2nd entry: locales of the theory,
   285        3rd entry: registrations, indexed by locale name *)
   286 
   287   val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
   288   val copy = I;
   289   val extend = I;
   290 
   291   fun join_locs _ ({axiom, import, elems, params, lparams, term_syntax, regs, intros}: locale,
   292       {elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) =
   293      {axiom = axiom,
   294       import = import,
   295       elems = gen_merge_lists (eq_snd (op =)) elems elems',
   296       params = params,
   297       lparams = lparams,
   298       term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'),
   299       regs = merge_alists regs regs',
   300       intros = intros};
   301   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
   302     (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
   303      Symtab.join (K Registrations.join) (regs1, regs2));
   304 
   305   fun print _ (space, locs, _) =
   306     Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   307     |> Pretty.writeln;
   308 end);
   309 
   310 val _ = Context.add_setup GlobalLocalesData.init;
   311 
   312 
   313 
   314 (** context data **)
   315 
   316 structure LocalLocalesData = ProofDataFun
   317 (struct
   318   val name = "Isar/locales";
   319   type T = Registrations.T Symtab.table;
   320     (* registrations, indexed by locale name *)
   321   fun init _ = Symtab.empty;
   322   fun print _ _ = ();
   323 end);
   324 
   325 val _ = Context.add_setup LocalLocalesData.init;
   326 
   327 
   328 (* access locales *)
   329 
   330 val print_locales = GlobalLocalesData.print;
   331 
   332 val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
   333 val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
   334 
   335 fun declare_locale name thy =
   336   thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
   337     (Sign.declare_name thy name space, locs, regs));
   338 
   339 fun put_locale name loc =
   340   GlobalLocalesData.map (fn (space, locs, regs) =>
   341     (space, Symtab.update (name, loc) locs, regs));
   342 
   343 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;
   344 
   345 fun the_locale thy name =
   346   (case get_locale thy name of
   347     SOME loc => loc
   348   | NONE => error ("Unknown locale " ^ quote name));
   349 
   350 fun change_locale name f thy =
   351   let
   352     val {axiom, import, elems, params, lparams, term_syntax, regs, intros} =
   353         the_locale thy name;
   354     val (axiom', import', elems', params', lparams', term_syntax', regs', intros') =
   355       f (axiom, import, elems, params, lparams, term_syntax, regs, intros);
   356   in
   357     put_locale name {axiom = axiom', import = import', elems = elems',
   358       params = params', lparams = lparams', term_syntax = term_syntax', regs = regs',
   359       intros = intros'} thy
   360   end;
   361 
   362 
   363 (* access registrations *)
   364 
   365 (* Ids of global registrations are varified,
   366    Ids of local registrations are not.
   367    Thms of registrations are never varified. *)
   368 
   369 (* retrieve registration from theory or context *)
   370 
   371 fun gen_get_registrations get thy_of thy_ctxt name =
   372   case Symtab.lookup (get thy_ctxt) name of
   373       NONE => []
   374     | SOME reg => Registrations.dest (thy_of thy_ctxt) reg;
   375 
   376 val get_global_registrations =
   377      gen_get_registrations (#3 o GlobalLocalesData.get) I;
   378 val get_local_registrations =
   379      gen_get_registrations LocalLocalesData.get ProofContext.theory_of;
   380 
   381 fun gen_get_registration get thy_of thy_ctxt (name, ps) =
   382   case Symtab.lookup (get thy_ctxt) name of
   383       NONE => NONE
   384     | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
   385 
   386 val get_global_registration =
   387      gen_get_registration (#3 o GlobalLocalesData.get) I;
   388 val get_local_registration =
   389      gen_get_registration LocalLocalesData.get ProofContext.theory_of;
   390 
   391 val test_global_registration = is_some oo get_global_registration;
   392 val test_local_registration = is_some oo get_local_registration;
   393 fun smart_test_registration ctxt id =
   394   let
   395     val thy = ProofContext.theory_of ctxt;
   396   in
   397     test_global_registration thy id orelse test_local_registration ctxt id
   398   end;
   399 
   400 
   401 (* add registration to theory or context, ignored if subsumed *)
   402 
   403 fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
   404   map_data (fn regs =>
   405     let
   406       val thy = thy_of thy_ctxt;
   407       val reg = the_default Registrations.empty (Symtab.lookup regs name);
   408       val (reg', sups) = Registrations.insert thy (ps, attn) reg;
   409       val _ = if not (null sups) then warning
   410                 ("Subsumed interpretation(s) of locale " ^
   411                  quote (extern thy name) ^
   412                  "\nby interpretation(s) with the following prefix(es):\n" ^
   413                   commas_quote (map (fn (_, ((s, _), _)) => s) sups))
   414               else ();
   415     in Symtab.update (name, reg') regs end) thy_ctxt;
   416 
   417 val put_global_registration =
   418      gen_put_registration (fn f =>
   419        GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
   420 val put_local_registration =
   421      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
   422 
   423 fun put_registration_in_locale name id =
   424   change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
   425     (axiom, import, elems, params, lparams, term_syntax, regs @ [(id, [])], intros));
   426 
   427 
   428 (* add witness theorem to registration in theory or context,
   429    ignored if registration not present *)
   430 
   431 fun add_witness (name, ps) thm =
   432   Symtab.map_entry name (Registrations.add_witness ps thm);
   433 
   434 fun add_global_witness id thm =
   435   GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
   436 
   437 val add_local_witness = LocalLocalesData.map oo add_witness;
   438 
   439 fun add_witness_in_locale name id thm =
   440   change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
   441     let
   442       fun add (id', thms) =
   443         if id = id' then (id', thm :: thms) else (id', thms);
   444     in (axiom, import, elems, params, lparams, term_syntax, map add regs, intros) end);
   445 
   446 
   447 (* printing of registrations *)
   448 
   449 fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
   450   let
   451     val ctxt = mk_ctxt thy_ctxt;
   452     val thy = ProofContext.theory_of ctxt;
   453 
   454     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   455     fun prt_inst ts =
   456         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
   457     fun prt_attn (prfx, atts) =
   458         Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
   459     fun prt_witns witns = Pretty.enclose "[" "]"
   460       (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
   461     fun prt_reg (ts, (("", []), witns)) =
   462         if show_wits
   463           then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
   464           else prt_inst ts
   465       | prt_reg (ts, (attn, witns)) =
   466         if show_wits
   467           then Pretty.block ((prt_attn attn @
   468             [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
   469               prt_witns witns]))
   470           else Pretty.block ((prt_attn attn @
   471             [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
   472 
   473     val loc_int = intern thy loc;
   474     val regs = get_regs thy_ctxt;
   475     val loc_regs = Symtab.lookup regs loc_int;
   476   in
   477     (case loc_regs of
   478         NONE => Pretty.str ("no interpretations in " ^ msg)
   479       | SOME r => let
   480             val r' = Registrations.dest thy r;
   481             val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
   482           in Pretty.big_list ("interpretations in " ^ msg ^ ":")
   483             (map prt_reg r'')
   484           end)
   485     |> Pretty.writeln
   486   end;
   487 
   488 val print_global_registrations =
   489      gen_print_registrations (#3 o GlobalLocalesData.get)
   490        ProofContext.init "theory";
   491 val print_local_registrations' =
   492      gen_print_registrations LocalLocalesData.get
   493        I "context";
   494 fun print_local_registrations show_wits loc ctxt =
   495   (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
   496    print_local_registrations' show_wits loc ctxt);
   497 
   498 
   499 (* diagnostics *)
   500 
   501 fun err_in_locale ctxt msg ids =
   502   let
   503     val thy = ProofContext.theory_of ctxt;
   504     fun prt_id (name, parms) =
   505       [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   506     val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   507     val err_msg =
   508       if forall (equal "" o #1) ids then msg
   509       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   510         (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   511   in error err_msg end;
   512 
   513 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   514 
   515 
   516 fun pretty_ren NONE = Pretty.str "_"
   517   | pretty_ren (SOME (x, NONE)) = Pretty.str x
   518   | pretty_ren (SOME (x, SOME syn)) =
   519       Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
   520 
   521 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
   522   | pretty_expr thy (Rename (expr, xs)) =
   523       Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
   524   | pretty_expr thy (Merge es) =
   525       Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
   526 
   527 fun err_in_expr _ msg (Merge []) = error msg
   528   | err_in_expr ctxt msg expr =
   529     error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
   530       [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
   531        pretty_expr (ProofContext.theory_of ctxt) expr]));
   532 
   533 
   534 (** structured contexts: rename + merge + implicit type instantiation **)
   535 
   536 (* parameter types *)
   537 
   538 fun frozen_tvars ctxt Ts =
   539   #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   540   |> map (fn ((xi, S), T) => (xi, (S, T)));
   541 
   542 fun unify_frozen ctxt maxidx Ts Us =
   543   let
   544     fun paramify NONE i = (NONE, i)
   545       | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   546 
   547     val (Ts', maxidx') = fold_map paramify Ts maxidx;
   548     val (Us', maxidx'') = fold_map paramify Us maxidx';
   549     val thy = ProofContext.theory_of ctxt;
   550 
   551     fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   552           handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   553       | unify _ env = env;
   554     val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   555     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   556     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   557   in map (Option.map (Envir.norm_type unifier')) Vs end;
   558 
   559 fun params_of elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
   560 fun params_of' elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   561 
   562 
   563 (* CB: param_types has the following type:
   564   ('a * 'b option) list -> ('a * 'b) list *)
   565 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   566 
   567 
   568 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
   569   handle Symtab.DUPS xs => err_in_locale ctxt
   570     ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
   571 
   572 
   573 (* Distinction of assumed vs. derived identifiers.
   574    The former may have axioms relating assumptions of the context to
   575    assumptions of the specification fragment (for locales with
   576    predicates).  The latter have witnesses relating assumptions of the
   577    specification fragment to assumptions of other (assumed) specification
   578    fragments. *)
   579 
   580 datatype 'a mode = Assumed of 'a | Derived of 'a;
   581 
   582 fun map_mode f (Assumed x) = Assumed (f x)
   583   | map_mode f (Derived x) = Derived (f x);
   584 
   585 
   586 (* flatten expressions *)
   587 
   588 local
   589 
   590 fun unify_parms ctxt fixed_parms raw_parmss =
   591   let
   592     val thy = ProofContext.theory_of ctxt;
   593     val maxidx = length raw_parmss;
   594     val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   595 
   596     fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   597     fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   598     val parms = fixed_parms @ maps varify_parms idx_parmss;
   599 
   600     fun unify T U envir = Sign.typ_unify thy (U, T) envir
   601       handle Type.TUNIFY =>
   602         let val prt = Sign.string_of_typ thy in
   603           raise TYPE ("unify_parms: failed to unify types " ^
   604             prt U ^ " and " ^ prt T, [U, T], [])
   605         end;
   606     fun unify_list (T :: Us) = fold (unify T) Us
   607       | unify_list [] = I;
   608     val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
   609       (Vartab.empty, maxidx);
   610 
   611     val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
   612     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   613 
   614     fun inst_parms (i, ps) =
   615       foldr Term.add_typ_tfrees [] (map_filter snd ps)
   616       |> map_filter (fn (a, S) =>
   617           let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   618           in if T = TFree (a, S) then NONE else SOME (a, T) end)
   619       |> Symtab.make;
   620   in map inst_parms idx_parmss end;
   621 
   622 in
   623 
   624 fun unify_elemss _ _ [] = []
   625   | unify_elemss _ [] [elems] = [elems]
   626   | unify_elemss ctxt fixed_parms elemss =
   627       let
   628         val thy = ProofContext.theory_of ctxt;
   629         val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
   630         fun inst ((((name, ps), mode), elems), env) =
   631           (((name, map (apsnd (Option.map (Element.instT_type env))) ps),
   632               map_mode (map (Element.instT_witness thy env)) mode),
   633             map (Element.instT_ctxt thy env) elems);
   634       in map inst (elemss ~~ envs) end;
   635 
   636 
   637 fun renaming xs parms = zip_options parms xs
   638   handle Library.UnequalLengths =>
   639     error ("Too many arguments in renaming: " ^
   640       commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
   641 
   642 
   643 (* params_of_expr:
   644    Compute parameters (with types and syntax) of locale expression.
   645 *)
   646 
   647 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
   648   let
   649     val thy = ProofContext.theory_of ctxt;
   650 
   651     fun merge_tenvs fixed tenv1 tenv2 =
   652         let
   653           val [env1, env2] = unify_parms ctxt fixed
   654                 [tenv1 |> Symtab.dest |> map (apsnd SOME),
   655                  tenv2 |> Symtab.dest |> map (apsnd SOME)]
   656         in
   657           Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
   658             Symtab.map (Element.instT_type env2) tenv2)
   659         end;
   660 
   661     fun merge_syn expr syn1 syn2 =
   662         Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
   663         handle Symtab.DUPS xs => err_in_expr ctxt
   664           ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
   665 
   666     fun params_of (expr as Locale name) =
   667           let
   668             val {import, params, ...} = the_locale thy name;
   669             val parms = map (fst o fst) params;
   670             val (parms', types', syn') = params_of import;
   671             val all_parms = merge_lists parms' parms;
   672             val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
   673             val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
   674           in (all_parms, all_types, all_syn) end
   675       | params_of (expr as Rename (e, xs)) =
   676           let
   677             val (parms', types', syn') = params_of e;
   678             val ren = renaming xs parms';
   679             (* renaming may reduce number of parameters *)
   680             val new_parms = map (Element.rename ren) parms' |> distinct (op =);
   681             val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
   682             val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
   683                 handle Symtab.DUP x =>
   684                   err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
   685             val syn_types = map (apsnd (fn mx => SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))))) (Symtab.dest new_syn);
   686             val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
   687             val (env :: _) = unify_parms ctxt []
   688                 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
   689             val new_types = fold (Symtab.insert (op =))
   690                 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
   691           in (new_parms, new_types, new_syn) end
   692       | params_of (Merge es) =
   693           fold (fn e => fn (parms, types, syn) =>
   694                    let
   695                      val (parms', types', syn') = params_of e
   696                    in
   697                      (merge_lists parms parms', merge_tenvs [] types types',
   698                       merge_syn e syn syn')
   699                    end)
   700             es ([], Symtab.empty, Symtab.empty)
   701 
   702       val (parms, types, syn) = params_of expr;
   703     in
   704       (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
   705        merge_syn expr prev_syn syn)
   706     end;
   707 
   708 fun make_params_ids params = [(("", params), ([], Assumed []))];
   709 fun make_raw_params_elemss (params, tenv, syn) =
   710     [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   711       Int [Fixes (map (fn p =>
   712         (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   713 
   714 
   715 (* flatten_expr:
   716    Extend list of identifiers by those new in locale expression expr.
   717    Compute corresponding list of lists of locale elements (one entry per
   718    identifier).
   719 
   720    Identifiers represent locale fragments and are in an extended form:
   721      ((name, ps), (ax_ps, axs))
   722    (name, ps) is the locale name with all its parameters.
   723    (ax_ps, axs) is the locale axioms with its parameters;
   724      axs are always taken from the top level of the locale hierarchy,
   725      hence axioms may contain additional parameters from later fragments:
   726      ps subset of ax_ps.  axs is either singleton or empty.
   727 
   728    Elements are enriched by identifier-like information:
   729      (((name, ax_ps), axs), elems)
   730    The parameters in ax_ps are the axiom parameters, but enriched by type
   731    info: now each entry is a pair of string and typ option.  Axioms are
   732    type-instantiated.
   733 
   734 *)
   735 
   736 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
   737   let
   738     val thy = ProofContext.theory_of ctxt;
   739 
   740     fun rename_parms top ren ((name, ps), (parms, mode)) =
   741         ((name, map (Element.rename ren) ps),
   742          if top
   743          then (map (Element.rename ren) parms,
   744                map_mode (map (Element.rename_witness ren)) mode)
   745          else (parms, mode));
   746 
   747     (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
   748 
   749     fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
   750         if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
   751         then (wits, ids, visited)
   752         else
   753           let
   754             val {params, regs, ...} = the_locale thy name;
   755             val pTs' = map #1 params;
   756             val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
   757               (* dummy syntax, since required by rename *)
   758             val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
   759             val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
   760               (* propagate parameter types, to keep them consistent *)
   761             val regs' = map (fn ((name, ps), wits) =>
   762                 ((name, map (Element.rename ren) ps),
   763                  map (Element.transfer_witness thy) wits)) regs;
   764             val new_regs = regs';
   765             val new_ids = map fst new_regs;
   766             val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
   767 
   768             val new_wits = new_regs |> map (#2 #> map
   769               (Element.instT_witness thy env #> Element.rename_witness ren #>
   770                 Element.satisfy_witness wits));
   771             val new_ids' = map (fn (id, wits) =>
   772                 (id, ([], Derived wits))) (new_ids ~~ new_wits);
   773             val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
   774                 ((n, pTs), mode)) (new_idTs ~~ new_ids');
   775             val new_id = ((name, map #1 pTs), ([], mode));
   776             val (wits', ids', visited') = fold add_with_regs new_idTs'
   777               (wits @ flat new_wits, ids, visited @ [new_id]);
   778           in
   779             (wits', ids' @ [new_id], visited')
   780           end;
   781 
   782     (* distribute top-level axioms over assumed ids *)
   783 
   784     fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
   785         let
   786           val {elems, ...} = the_locale thy name;
   787           val ts = maps
   788             (fn (Assumes asms, _) => maps (map #1 o #2) asms
   789               | _ => [])
   790             elems;
   791           val (axs1, axs2) = chop (length ts) axioms;
   792         in (((name, parms), (all_ps, Assumed axs1)), axs2) end
   793       | axiomify all_ps (id, (_, Derived ths)) axioms =
   794           ((id, (all_ps, Derived ths)), axioms);
   795 
   796     (* identifiers of an expression *)
   797 
   798     fun identify top (Locale name) =
   799     (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
   800        where name is a locale name, ps a list of parameter names and axs
   801        a list of axioms relating to the identifier, axs is empty unless
   802        identify at top level (top = true);
   803        parms is accumulated list of parameters *)
   804           let
   805             val {axiom, import, params, ...} = the_locale thy name;
   806             val ps = map (#1 o #1) params;
   807             val (ids', parms') = identify false import;
   808                 (* acyclic import dependencies *)
   809 
   810             val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
   811             val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
   812             in (ids_ax, merge_lists parms' ps) end
   813       | identify top (Rename (e, xs)) =
   814           let
   815             val (ids', parms') = identify top e;
   816             val ren = renaming xs parms'
   817               handle ERROR msg => err_in_locale' ctxt msg ids';
   818 
   819             val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   820             val parms'' = distinct (op =) (maps (#2 o #1) ids'');
   821           in (ids'', parms'') end
   822       | identify top (Merge es) =
   823           fold (fn e => fn (ids, parms) =>
   824                    let
   825                      val (ids', parms') = identify top e
   826                    in
   827                      (merge_alists ids ids', merge_lists parms parms')
   828                    end)
   829             es ([], []);
   830 
   831     fun inst_wit all_params (t, th) = let
   832          val {hyps, prop, ...} = Thm.rep_thm th;
   833          val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
   834          val [env] = unify_parms ctxt all_params [ps];
   835          val t' = Element.instT_term env t;
   836          val th' = Element.instT_thm thy env th;
   837        in (t', th') end;
   838 
   839     fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
   840       let
   841         val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
   842         val elems = map fst elems_stamped;
   843         val ps = map fst ps_mx;
   844         fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
   845         val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
   846         val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
   847         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
   848         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
   849         val elems' = elems
   850               |> map (Element.rename_ctxt ren)
   851               |> map (Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I,
   852                    name = NameSpace.qualified (space_implode "_" params)})
   853               |> map (Element.instT_ctxt thy env)
   854       in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   855 
   856     (* parameters, their types and syntax *)
   857     val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
   858     val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
   859     (* compute identifiers and syntax, merge with previous ones *)
   860     val (ids, _) = identify true expr;
   861     val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
   862     val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   863     (* type-instantiate elements *)
   864     val final_elemss = map (eval all_params tenv syntax) idents;
   865   in ((prev_idents @ idents, syntax), final_elemss) end;
   866 
   867 end;
   868 
   869 
   870 (* activate elements *)
   871 
   872 local
   873 
   874 fun axioms_export axs _ hyps =
   875   Element.satisfy_thm axs
   876   #> Drule.implies_intr_list (Library.drop (length axs, hyps));
   877 
   878 
   879 (* NB: derived ids contain only facts at this stage *)
   880 
   881 fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
   882       ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
   883   | activate_elem _ _ ((ctxt, mode), Constrains _) =
   884       ((ctxt, mode), [])
   885   | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
   886       let
   887         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   888         val ts = maps (map #1 o #2) asms';
   889         val (ps, qs) = chop (length ts) axs;
   890         val (_, ctxt') =
   891           ctxt |> fold Variable.fix_frees ts
   892           |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
   893       in ((ctxt', Assumed qs), []) end
   894   | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
   895       ((ctxt, Derived ths), [])
   896   | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
   897       let
   898         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   899         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
   900             let val ((c, _), t') = LocalDefs.cert_def ctxt t
   901             in (t', ((if name = "" then Thm.def_name c else name, atts), [(t', ps)])) end);
   902         val (_, ctxt') =
   903           ctxt |> fold (Variable.fix_frees o #1) asms
   904           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
   905       in ((ctxt', Assumed axs), []) end
   906   | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
   907       ((ctxt, Derived ths), [])
   908   | activate_elem _ is_ext ((ctxt, mode), Notes facts) =
   909       let
   910         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
   911         val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
   912       in ((ctxt', mode), if is_ext then res else []) end;
   913 
   914 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
   915   let
   916     val thy = ProofContext.theory_of ctxt;
   917     val ((ctxt', _), res) =
   918         foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
   919       handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
   920     val ctxt'' = if name = "" then ctxt'
   921           else let
   922               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   923               val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
   924             in case mode of
   925                 Assumed axs =>
   926                   fold (add_local_witness (name, ps') o
   927                     Element.assume_witness thy o Element.witness_prop) axs ctxt''
   928               | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
   929             end
   930   in (ProofContext.restore_naming ctxt ctxt'', res) end;
   931 
   932 fun activate_elemss ax_in_ctxt prep_facts =
   933     fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
   934       let
   935         val elems = map (prep_facts ctxt) raw_elems;
   936         val (ctxt', res) = apsnd flat
   937             (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
   938         val elems' = elems |> map (Element.map_ctxt
   939           {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure});
   940       in (((((name, ps), mode), elems'), res), ctxt') end);
   941 
   942 in
   943 
   944 (* CB: activate_facts prep_facts (ctxt, elemss),
   945    where elemss is a list of pairs consisting of identifiers and
   946    context elements, extends ctxt by the context elements yielding
   947    ctxt' and returns (ctxt', (elemss', facts)).
   948    Identifiers in the argument are of the form ((name, ps), axs) and
   949    assumptions use the axioms in the identifiers to set up exporters
   950    in ctxt'.  elemss' does not contain identifiers and is obtained
   951    from elemss and the intermediate context with prep_facts.
   952    If read_facts or cert_facts is used for prep_facts, these also remove
   953    the internal/external markers from elemss. *)
   954 
   955 fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
   956   let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
   957   in (ctxt', (elemss, flat factss)) end;
   958 
   959 end;
   960 
   961 
   962 
   963 (** prepare locale elements **)
   964 
   965 (* expressions *)
   966 
   967 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
   968   | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
   969   | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
   970 
   971 
   972 (* propositions and bindings *)
   973 
   974 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
   975    normalises expr (which is either a locale
   976    expression or a single context element) wrt.
   977    to the list ids of already accumulated identifiers.
   978    It returns ((ids', syn'), elemss) where ids' is an extension of ids
   979    with identifiers generated for expr, and elemss is the list of
   980    context elements generated from expr.
   981    syn and syn' are symtabs mapping parameter names to their syntax.  syn'
   982    is an extension of syn.
   983    For details, see flatten_expr.
   984 
   985    Additionally, for a locale expression, the elems are grouped into a single
   986    Int; individual context elements are marked Ext.  In this case, the
   987    identifier-like information of the element is as follows:
   988    - for Fixes: (("", ps), []) where the ps have type info NONE
   989    - for other elements: (("", []), []).
   990    The implementation of activate_facts relies on identifier names being
   991    empty strings for external elements.
   992 *)
   993 
   994 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
   995         val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
   996       in
   997         ((ids',
   998          merge_syntax ctxt ids'
   999            (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
  1000            handle Symtab.DUPS xs => err_in_locale ctxt
  1001              ("Conflicting syntax for parameters: " ^ commas_quote xs)
  1002              (map #1 ids')),
  1003          [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
  1004       end
  1005   | flatten _ ((ids, syn), Elem elem) =
  1006       ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
  1007   | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
  1008       apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
  1009 
  1010 local
  1011 
  1012 local
  1013 
  1014 fun declare_int_elem (ctxt, Fixes fixes) =
  1015       (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  1016         (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
  1017   | declare_int_elem (ctxt, _) = (ctxt, []);
  1018 
  1019 fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
  1020       let val (vars, _) = prep_vars fixes ctxt
  1021       in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
  1022   | declare_ext_elem prep_vars (ctxt, Constrains csts) =
  1023       let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
  1024       in (ctxt', []) end
  1025   | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
  1026   | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
  1027   | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
  1028 
  1029 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
  1030     let val (ctxt', propps) =
  1031       (case elems of
  1032         Int es => foldl_map declare_int_elem (ctxt, es)
  1033       | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
  1034       handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
  1035     in (ctxt', propps) end
  1036   | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
  1037 
  1038 in
  1039 
  1040 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
  1041   let
  1042     (* CB: fix of type bug of goal in target with context elements.
  1043        Parameters new in context elements must receive types that are
  1044        distinct from types of parameters in target (fixed_params).  *)
  1045     val ctxt_with_fixed =
  1046       fold Variable.declare_term (map Free fixed_params) ctxt;
  1047     val int_elemss =
  1048       raw_elemss
  1049       |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  1050       |> unify_elemss ctxt_with_fixed fixed_params;
  1051     val (_, raw_elemss') =
  1052       foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
  1053         (int_elemss, raw_elemss);
  1054   in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
  1055 
  1056 end;
  1057 
  1058 local
  1059 
  1060 val norm_term = Envir.beta_norm oo Term.subst_atomic;
  1061 
  1062 fun abstract_thm thy eq =
  1063   Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
  1064 
  1065 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
  1066   let
  1067     val ((y, T), b) = LocalDefs.abs_def eq;
  1068     val b' = norm_term env b;
  1069     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
  1070     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
  1071   in
  1072     conditional (exists (equal y o #1) xs) (fn () =>
  1073       err "Attempt to define previously specified variable");
  1074     conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
  1075       err "Attempt to redefine variable");
  1076     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
  1077   end;
  1078 
  1079 
  1080 (* CB: for finish_elems (Int and Ext),
  1081    extracts specification, only of assumed elements *)
  1082 
  1083 fun eval_text _ _ _ (Fixes _) text = text
  1084   | eval_text _ _ _ (Constrains _) text = text
  1085   | eval_text _ (_, Assumed _) is_ext (Assumes asms)
  1086         (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  1087       let
  1088         val ts = maps (map #1 o #2) asms;
  1089         val ts' = map (norm_term env) ts;
  1090         val spec' =
  1091           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  1092           else ((exts, exts'), (ints @ ts, ints' @ ts'));
  1093       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  1094   | eval_text _ (_, Derived _) _ (Assumes _) text = text
  1095   | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
  1096       (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
  1097   | eval_text _ (_, Derived _) _ (Defines _) text = text
  1098   | eval_text _ _ _ (Notes _) text = text;
  1099 
  1100 
  1101 (* for finish_elems (Int),
  1102    remove redundant elements of derived identifiers,
  1103    turn assumptions and definitions into facts,
  1104    adjust hypotheses of facts using witnesses *)
  1105 
  1106 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
  1107   | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
  1108   | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
  1109   | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
  1110 
  1111   | finish_derived _ _ (Derived _) (Fixes _) = NONE
  1112   | finish_derived _ _ (Derived _) (Constrains _) = NONE
  1113   | finish_derived sign wits (Derived _) (Assumes asms) = asms
  1114       |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
  1115       |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
  1116   | finish_derived sign wits (Derived _) (Defines defs) = defs
  1117       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
  1118       |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
  1119 
  1120   | finish_derived _ wits _ (Notes facts) = (Notes facts)
  1121       |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;
  1122 
  1123 (* CB: for finish_elems (Ext) *)
  1124 
  1125 fun closeup _ false elem = elem
  1126   | closeup ctxt true elem =
  1127       let
  1128         fun close_frees t =
  1129           let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
  1130           in Term.list_all_free (frees, t) end;
  1131 
  1132         fun no_binds [] = []
  1133           | no_binds _ = error "Illegal term bindings in locale element";
  1134       in
  1135         (case elem of
  1136           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
  1137             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
  1138         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
  1139             (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
  1140         | e => e)
  1141       end;
  1142 
  1143 
  1144 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
  1145       (x, AList.lookup (op =) parms x, mx)) fixes)
  1146   | finish_ext_elem parms _ (Constrains _, _) = Constrains []
  1147   | finish_ext_elem _ close (Assumes asms, propp) =
  1148       close (Assumes (map #1 asms ~~ propp))
  1149   | finish_ext_elem _ close (Defines defs, propp) =
  1150       close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
  1151   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
  1152 
  1153 
  1154 (* CB: finish_parms introduces type info from parms to identifiers *)
  1155 (* CB: only needed for types that have been NONE so far???
  1156    If so, which are these??? *)
  1157 
  1158 fun finish_parms parms (((name, ps), mode), elems) =
  1159   (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
  1160 
  1161 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
  1162       let
  1163         val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
  1164         val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
  1165         val text' = fold (eval_text ctxt id' false) es text;
  1166         val es' = map_filter
  1167               (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
  1168       in ((text', wits'), (id', map Int es')) end
  1169   | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
  1170       let
  1171         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
  1172         val text' = eval_text ctxt id true e' text;
  1173       in ((text', wits), (id, [Ext e'])) end
  1174 
  1175 in
  1176 
  1177 (* CB: only called by prep_elemss *)
  1178 
  1179 fun finish_elemss ctxt parms do_close =
  1180   foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
  1181 
  1182 end;
  1183 
  1184 
  1185 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
  1186 
  1187 fun defs_ord (defs1, defs2) =
  1188     list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
  1189       Term.fast_term_ord (d1, d2)) (defs1, defs2);
  1190 structure Defstab =
  1191     TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
  1192         val ord = defs_ord);
  1193 
  1194 fun rem_dup_defs es ds =
  1195     fold_map (fn e as (Defines defs) => (fn ds =>
  1196                  if Defstab.defined ds defs
  1197                  then (Defines [], ds)
  1198                  else (e, Defstab.update (defs, ()) ds))
  1199                | e => (fn ds => (e, ds))) es ds;
  1200 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
  1201   | rem_dup_elemss (Ext e) ds = (Ext e, ds);
  1202 fun rem_dup_defines raw_elemss =
  1203     fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
  1204                      apfst (pair id) (rem_dup_elemss es ds))
  1205                | (id as (_, (Derived _)), es) => (fn ds =>
  1206                      ((id, es), ds))) raw_elemss Defstab.empty |> #1;
  1207 
  1208 (* CB: type inference and consistency checks for locales.
  1209 
  1210    Works by building a context (through declare_elemss), extracting the
  1211    required information and adjusting the context elements (finish_elemss).
  1212    Can also universally close free vars in assms and defs.  This is only
  1213    needed for Ext elements and controlled by parameter do_close.
  1214 
  1215    Only elements of assumed identifiers are considered.
  1216 *)
  1217 
  1218 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
  1219   let
  1220     (* CB: contexts computed in the course of this function are discarded.
  1221        They are used for type inference and consistency checks only. *)
  1222     (* CB: fixed_params are the parameters (with types) of the target locale,
  1223        empty list if there is no target. *)
  1224     (* CB: raw_elemss are list of pairs consisting of identifiers and
  1225        context elements, the latter marked as internal or external. *)
  1226     val raw_elemss = rem_dup_defines raw_elemss;
  1227     val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
  1228     (* CB: raw_ctxt is context with additional fixed variables derived from
  1229        the fixes elements in raw_elemss,
  1230        raw_proppss contains assumptions and definitions from the
  1231        external elements in raw_elemss. *)
  1232     fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
  1233       let
  1234         (* CB: add type information from fixed_params to context (declare_term) *)
  1235         (* CB: process patterns (conclusion and external elements only) *)
  1236         val (ctxt, all_propp) =
  1237           prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  1238         (* CB: add type information from conclusion and external elements to context *)
  1239         val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
  1240         (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
  1241         val all_propp' = map2 (curry (op ~~))
  1242           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
  1243         val (concl, propp) = chop (length raw_concl) all_propp';
  1244       in (propp, (ctxt, concl)) end
  1245 
  1246     val (proppss, (ctxt, concl)) =
  1247       (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
  1248 
  1249     (* CB: obtain all parameters from identifier part of raw_elemss *)
  1250     val xs = map #1 (params_of' raw_elemss);
  1251     val typing = unify_frozen ctxt 0
  1252       (map (Variable.default_type raw_ctxt) xs)
  1253       (map (Variable.default_type ctxt) xs);
  1254     val parms = param_types (xs ~~ typing);
  1255     (* CB: parms are the parameters from raw_elemss, with correct typing. *)
  1256 
  1257     (* CB: extract information from assumes and defines elements
  1258        (fixes, constrains and notes in raw_elemss don't have an effect on
  1259        text and elemss), compute final form of context elements. *)
  1260     val ((text, _), elemss) = finish_elemss ctxt parms do_close
  1261       ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
  1262     (* CB: text has the following structure:
  1263            (((exts, exts'), (ints, ints')), (xs, env, defs))
  1264        where
  1265          exts: external assumptions (terms in external assumes elements)
  1266          exts': dito, normalised wrt. env
  1267          ints: internal assumptions (terms in internal assumes elements)
  1268          ints': dito, normalised wrt. env
  1269          xs: the free variables in exts' and ints' and rhss of definitions,
  1270            this includes parameters except defined parameters
  1271          env: list of term pairs encoding substitutions, where the first term
  1272            is a free variable; substitutions represent defines elements and
  1273            the rhs is normalised wrt. the previous env
  1274          defs: theorems representing the substitutions from defines elements
  1275            (thms are normalised wrt. env).
  1276        elemss is an updated version of raw_elemss:
  1277          - type info added to Fixes and modified in Constrains
  1278          - axiom and definition statement replaced by corresponding one
  1279            from proppss in Assumes and Defines
  1280          - Facts unchanged
  1281        *)
  1282   in ((parms, elemss, concl), text) end;
  1283 
  1284 in
  1285 
  1286 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
  1287 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
  1288 
  1289 end;
  1290 
  1291 
  1292 (* facts and attributes *)
  1293 
  1294 local
  1295 
  1296 fun prep_name name =
  1297   if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
  1298   else name;
  1299 
  1300 fun prep_facts _ _ ctxt (Int elem) =
  1301       Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
  1302   | prep_facts get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  1303      {var = I, typ = I, term = I,
  1304       name = prep_name,
  1305       fact = get ctxt,
  1306       attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  1307 
  1308 in
  1309 
  1310 fun read_facts x = prep_facts ProofContext.get_thms Attrib.intern_src x;
  1311 fun cert_facts x = prep_facts (K I) (K I) x;
  1312 
  1313 end;
  1314 
  1315 
  1316 (* Get the specification of a locale *)
  1317 
  1318 (*The global specification is made from the parameters and global
  1319   assumptions, the local specification from the parameters and the
  1320   local assumptions.*)
  1321 
  1322 local
  1323 
  1324 fun gen_asms_of get thy name =
  1325   let
  1326     val ctxt = ProofContext.init thy;
  1327     val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
  1328     val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
  1329   in
  1330     elemss |> get
  1331       |> maps (fn (_, es) => map (fn Int e => e) es)
  1332       |> maps (fn Assumes asms => asms | _ => [])
  1333       |> map (apsnd (map fst))
  1334   end;
  1335 
  1336 in
  1337 
  1338 fun parameters_of thy name =
  1339   the_locale thy name |> #params;
  1340 
  1341 fun parameters_of_expr thy expr =
  1342   let
  1343     val ctxt = ProofContext.init thy;
  1344     val pts = params_of_expr ctxt [] (intern_expr thy expr)
  1345         ([], Symtab.empty, Symtab.empty);
  1346     val raw_params_elemss = make_raw_params_elemss pts;
  1347     val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  1348         (([], Symtab.empty), Expr expr);
  1349     val ((parms, _, _), _) =
  1350         read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
  1351   in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
  1352 
  1353 fun local_asms_of thy name =
  1354   gen_asms_of (single o Library.last_elem) thy name;
  1355 
  1356 fun global_asms_of thy name =
  1357   gen_asms_of I thy name;
  1358 
  1359 end;
  1360 
  1361 
  1362 (* full context statements: import + elements + conclusion *)
  1363 
  1364 local
  1365 
  1366 fun prep_context_statement prep_expr prep_elemss prep_facts
  1367     do_close fixed_params import elements raw_concl context =
  1368   let
  1369     val thy = ProofContext.theory_of context;
  1370 
  1371     val (import_params, import_tenv, import_syn) =
  1372       params_of_expr context fixed_params (prep_expr thy import)
  1373         ([], Symtab.empty, Symtab.empty);
  1374     val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
  1375     val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
  1376       (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
  1377 
  1378     val ((import_ids, _), raw_import_elemss) =
  1379       flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
  1380     (* CB: normalise "includes" among elements *)
  1381     val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
  1382       ((import_ids, incl_syn), elements);
  1383 
  1384     val raw_elemss = flat raw_elemsss;
  1385     (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  1386        context elements obtained from import and elements. *)
  1387     (* Now additional elements for parameters are inserted. *)
  1388     val import_params_ids = make_params_ids import_params;
  1389     val incl_params_ids =
  1390         make_params_ids (incl_params \\ import_params);
  1391     val raw_import_params_elemss =
  1392         make_raw_params_elemss (import_params, incl_tenv, incl_syn);
  1393     val raw_incl_params_elemss =
  1394         make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
  1395     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  1396       context fixed_params
  1397       (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
  1398 
  1399     (* replace extended ids (for axioms) by ids *)
  1400     val (import_ids', incl_ids) = chop (length import_ids) ids;
  1401     val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
  1402     val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
  1403         (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
  1404       (all_ids ~~ all_elemss);
  1405     (* CB: all_elemss and parms contain the correct parameter types *)
  1406 
  1407     val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  1408     val (import_ctxt, (import_elemss, _)) =
  1409       activate_facts false prep_facts (context, ps);
  1410 
  1411     val (ctxt, (elemss, _)) =
  1412       activate_facts false prep_facts (import_ctxt, qs);
  1413   in
  1414     ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  1415       (parms, spec, defs)), concl)
  1416   end;
  1417 
  1418 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  1419   let
  1420     val thy = ProofContext.theory_of ctxt;
  1421     val locale = Option.map (prep_locale thy) raw_locale;
  1422     val (fixed_params, import) =
  1423       (case locale of
  1424         NONE => ([], empty)
  1425       | SOME name =>
  1426           let val {params = ps, ...} = the_locale thy name
  1427           in (map fst ps, Locale name) end);
  1428     val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
  1429       prep_ctxt false fixed_params import elems concl ctxt;
  1430   in (locale, locale_ctxt, elems_ctxt, concl') end;
  1431 
  1432 fun prep_expr prep import body ctxt =
  1433   let
  1434     val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt;
  1435     val all_elems = maps snd (import_elemss @ elemss);
  1436   in (all_elems, ctxt') end;
  1437 
  1438 in
  1439 
  1440 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
  1441 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
  1442 
  1443 fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt);
  1444 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
  1445 
  1446 val read_expr = prep_expr read_context;
  1447 val cert_expr = prep_expr cert_context;
  1448 
  1449 fun read_context_statement raw_locale = prep_statement intern read_ctxt raw_locale ;
  1450 fun cert_context_statement raw_locale = prep_statement (K I) cert_ctxt raw_locale ;
  1451 
  1452 end;
  1453 
  1454 
  1455 (* print locale *)
  1456 
  1457 fun print_locale thy show_facts import body =
  1458   let
  1459     val (all_elems, ctxt) = read_expr import body (ProofContext.init thy);
  1460     val prt_elem = Element.pretty_ctxt ctxt;
  1461   in
  1462     Pretty.big_list "locale elements:" (all_elems
  1463       |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
  1464       |> map (Pretty.chunks o prt_elem))
  1465     |> Pretty.writeln
  1466   end;
  1467 
  1468 
  1469 
  1470 (** store results **)
  1471 
  1472 (* naming of interpreted theorems *)
  1473 
  1474 fun global_note_prefix_i kind prfx args thy =
  1475   thy
  1476   |> Theory.qualified_names
  1477   |> Theory.sticky_prefix prfx
  1478   |> PureThy.note_thmss_i kind args
  1479   ||> Theory.restore_naming thy;
  1480 
  1481 fun local_note_prefix_i prfx args ctxt =
  1482   ctxt
  1483   |> ProofContext.qualified_names
  1484   |> ProofContext.sticky_prefix prfx
  1485   |> ProofContext.note_thmss_i args
  1486   ||> ProofContext.restore_naming ctxt;
  1487 
  1488 
  1489 (* collect witnesses for global registration;
  1490    requires parameters and flattened list of (assumed!) identifiers
  1491    instead of recomputing it from the target *)
  1492 
  1493 fun collect_global_witnesses thy parms ids vts = let
  1494     val ts = map Logic.unvarify vts;
  1495     val (parms, parmTs) = split_list parms;
  1496     val parmvTs = map Logic.varifyT parmTs;
  1497     val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
  1498     val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
  1499         |> Symtab.make;
  1500     (* replace parameter names in ids by instantiations *)
  1501     val vinst = Symtab.make (parms ~~ vts);
  1502     fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
  1503     val inst = Symtab.make (parms ~~ ts);
  1504     val ids' = map (apsnd vinst_names) ids;
  1505     val wits = maps (snd o the o get_global_registration thy) ids';
  1506   in ((tinst, inst), wits) end;
  1507 
  1508 
  1509 (* store instantiations of args for all registered interpretations
  1510    of the theory *)
  1511 
  1512 fun note_thmss_registrations kind target args thy =
  1513   let
  1514     val parms = the_locale thy target |> #params |> map fst;
  1515     val ids = flatten (ProofContext.init thy, intern_expr thy)
  1516       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
  1517       |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
  1518 
  1519     val regs = get_global_registrations thy target;
  1520 
  1521     (* add args to thy for all registrations *)
  1522 
  1523     fun activate (vts, ((prfx, atts2), _)) thy =
  1524       let
  1525         val (insts, prems) = collect_global_witnesses thy parms ids vts;
  1526         val inst_atts =
  1527           Args.map_values I (Element.instT_type (#1 insts))
  1528             (Element.inst_term insts) (Element.inst_thm thy insts);
  1529         val args' = args |> map (fn ((n, atts), [(ths, [])]) =>
  1530             ((n, map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)),
  1531              [(map (Drule.standard o Element.satisfy_thm prems o
  1532             Element.inst_thm thy insts) ths, [])]));
  1533       in global_note_prefix_i kind prfx args' thy |> snd end;
  1534   in fold activate regs thy end;
  1535 
  1536 
  1537 (* term syntax *)
  1538 
  1539 fun add_term_syntax loc syn =
  1540   syn #> ProofContext.theory (change_locale loc
  1541     (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
  1542       (axiom, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs, intros)));
  1543 
  1544 fun init_term_syntax loc ctxt =
  1545   fold_rev (fn (f, _) => fn ctxt' => f ctxt')
  1546     (#term_syntax (the_locale (ProofContext.theory_of ctxt) loc)) ctxt;
  1547 
  1548 fun init loc =
  1549   ProofContext.init
  1550   #> init_term_syntax loc
  1551   #> (#2 o cert_context_statement (SOME loc) [] []);
  1552 
  1553 
  1554 (* theory/locale results *)
  1555 
  1556 fun theory_results kind prefix results ctxt thy =
  1557   let
  1558     val thy_ctxt = ProofContext.init thy;
  1559     val export = singleton (ProofContext.export_standard ctxt thy_ctxt);
  1560     val facts = map (fn (name, ths) => ((name, []), [(map export ths, [])])) results;
  1561   in thy |> PureThy.note_thmss_qualified kind prefix facts end;
  1562 
  1563 local
  1564 
  1565 (* FIXME tune *)
  1566 
  1567 fun gen_thmss prep_facts global_results kind loc args ctxt =
  1568   let
  1569     val (ctxt', ([(_, [Notes args'])], facts)) =
  1570       activate_facts true prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
  1571     val (facts', ctxt'') =
  1572       ctxt' |> ProofContext.theory_result
  1573         (change_locale loc
  1574           (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
  1575             (axiom, import, elems @ [(Notes args', stamp ())],
  1576               params, lparams, term_syntax, regs, intros))
  1577         #> note_thmss_registrations kind loc args'
  1578         #> global_results (map (#1 o #1) args' ~~ map #2 facts) ctxt);
  1579   in ((facts, facts'), ctxt'') end;
  1580 
  1581 fun gen_note prep_locale prep_facts kind raw_loc args thy =
  1582   let
  1583     val loc = prep_locale thy raw_loc;
  1584     val prefix = Sign.base_name loc;
  1585     val ctxt = init loc thy;
  1586   in gen_thmss prep_facts (theory_results kind prefix) kind loc args ctxt end;
  1587 
  1588 in
  1589 
  1590 val note_thmss = gen_note intern read_facts;
  1591 val note_thmss_i = gen_note (K I) cert_facts;
  1592 
  1593 fun add_thmss kind = gen_thmss cert_facts (theory_results kind "") kind;
  1594 
  1595 fun locale_results kind loc args ctxt =
  1596   gen_thmss cert_facts (K (K (pair []))) kind loc (map (apsnd Thm.simple_fact) args) ctxt
  1597   |>> #1;
  1598 
  1599 end;
  1600 
  1601 
  1602 
  1603 (** define locales **)
  1604 
  1605 (* predicate text *)
  1606 (* CB: generate locale predicates and delta predicates *)
  1607 
  1608 local
  1609 
  1610 (* introN: name of theorems for introduction rules of locale and
  1611      delta predicates;
  1612    axiomsN: name of theorem set with destruct rules for locale predicates,
  1613      also name suffix of delta predicates. *)
  1614 
  1615 val introN = "intro";
  1616 val axiomsN = "axioms";
  1617 
  1618 fun atomize_spec thy ts =
  1619   let
  1620     val t = Logic.mk_conjunction_list ts;
  1621     val body = ObjectLogic.atomize_term thy t;
  1622     val bodyT = Term.fastype_of body;
  1623   in
  1624     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
  1625     else (body, bodyT, ObjectLogic.atomize_cterm (Thm.cterm_of thy t))
  1626   end;
  1627 
  1628 fun aprop_tr' n c = (c, fn args =>
  1629   if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
  1630   else raise Match);
  1631 
  1632 (* CB: define one predicate including its intro rule and axioms
  1633    - bname: predicate name
  1634    - parms: locale parameters
  1635    - defs: thms representing substitutions from defines elements
  1636    - ts: terms representing locale assumptions (not normalised wrt. defs)
  1637    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
  1638    - thy: the theory
  1639 *)
  1640 
  1641 fun def_pred bname parms defs ts norm_ts thy =
  1642   let
  1643     val name = Sign.full_name thy bname;
  1644 
  1645     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  1646     val env = Term.add_term_free_names (body, []);
  1647     val xs = filter (fn (x, _) => x mem_string env) parms;
  1648     val Ts = map #2 xs;
  1649     val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
  1650       |> Library.sort_wrt #1 |> map TFree;
  1651     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
  1652 
  1653     val args = map Logic.mk_type extraTs @ map Free xs;
  1654     val head = Term.list_comb (Const (name, predT), args);
  1655     val statement = ObjectLogic.ensure_propT thy head;
  1656 
  1657     val ([pred_def], defs_thy) =
  1658       thy
  1659       |> (if bodyT <> propT then I else
  1660         Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
  1661       |> Theory.add_consts_i [(bname, predT, NoSyn)]
  1662       |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
  1663     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  1664 
  1665     val cert = Thm.cterm_of defs_thy;
  1666 
  1667     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
  1668       Tactic.rewrite_goals_tac [pred_def] THEN
  1669       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
  1670       Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
  1671 
  1672     val conjuncts =
  1673       (Drule.equal_elim_rule2 OF [body_eq,
  1674         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
  1675       |> Conjunction.elim_precise [length ts] |> hd;
  1676     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
  1677       Element.prove_witness defs_ctxt t
  1678        (Tactic.rewrite_goals_tac defs THEN
  1679         Tactic.compose_tac (false, ax, 0) 1));
  1680   in ((statement, intro, axioms), defs_thy) end;
  1681 
  1682 fun assumes_to_notes (Assumes asms) axms =
  1683     fold_map (fn (a, spec) => fn axs =>
  1684        let val (ps, qs) = chop (length spec) axs
  1685        in ((a, [(ps, [])]), qs) end) asms axms
  1686     |> apfst Notes
  1687   | assumes_to_notes e axms = (e, axms);
  1688 
  1689 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
  1690 
  1691 (* turn Assumes into Notes elements *)
  1692 
  1693 fun change_assumes_elemss axioms elemss =
  1694   let
  1695     fun change (id as ("", _), es) =
  1696           fold_map assumes_to_notes
  1697             (map (Element.map_ctxt_values I I (Element.satisfy_thm axioms)) es)
  1698           #-> (fn es' => pair (id, es'))
  1699       | change e = pair e;
  1700   in
  1701     fst (fold_map change elemss (map Element.conclude_witness axioms))
  1702   end;
  1703 
  1704 (* adjust hyps of Notes elements *)
  1705 
  1706 fun change_elemss_hyps axioms elemss =
  1707   let
  1708     fun change (id as ("", _), es) =
  1709         (id, map (fn e as (Notes _) => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
  1710                    | e => e) es)
  1711       | change e = e;
  1712   in map change elemss end;
  1713 
  1714 in
  1715 
  1716 (* CB: main predicate definition function *)
  1717 
  1718 fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  1719   let
  1720     val ((elemss', more_ts), a_elem, a_intro, thy') =
  1721       if null exts then ((elemss, []), [], [], thy)
  1722       else
  1723         let
  1724           val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
  1725           val ((statement, intro, axioms), def_thy) =
  1726             thy |> def_pred aname parms defs exts exts';
  1727           val elemss' = change_assumes_elemss axioms elemss;
  1728           val def_thy' = def_thy
  1729             |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
  1730             |> snd;
  1731           val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  1732         in ((elemss', [statement]), a_elem, [intro], def_thy') end;
  1733     val (predicate, stmt', elemss'', b_intro, thy'') =
  1734       if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy')
  1735       else
  1736         let
  1737           val ((statement, intro, axioms), def_thy) =
  1738             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
  1739           val cstatement = Thm.cterm_of def_thy statement;
  1740           val elemss'' = change_elemss_hyps axioms elemss';
  1741           val def_thy' =
  1742           def_thy
  1743           |> PureThy.note_thmss_qualified "" bname
  1744                [((introN, []), [([intro], [])]),
  1745                 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  1746           |> snd;
  1747           val b_elem = [(("", []),
  1748                [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  1749         in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], def_thy') end;
  1750   in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'') end;
  1751 
  1752 end;
  1753 
  1754 
  1755 (* add_locale(_i) *)
  1756 
  1757 local
  1758 
  1759 (* turn Defines into Notes elements, accumulate definition terms *)
  1760 
  1761 fun defines_to_notes is_ext thy (Defines defs) defns =
  1762     let
  1763       val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
  1764       val notes = map (fn (a, (def, _)) =>
  1765         (a, [([assume (cterm_of thy def)], [])])) defs
  1766     in (if is_ext then SOME (Notes notes) else NONE, defns @ [Defines defs']) end
  1767   | defines_to_notes _ _ e defns = (SOME e, defns);
  1768 
  1769 fun change_defines_elemss thy elemss defns =
  1770   let
  1771     fun change (id as (n, _), es) defns =
  1772         let
  1773           val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
  1774         in ((id, map_filter I es'), defns') end
  1775   in fold_map change elemss defns end;
  1776 
  1777 fun gen_add_locale prep_ctxt prep_expr
  1778     do_predicate bname raw_import raw_body thy =
  1779   let
  1780     val name = Sign.full_name thy bname;
  1781     val _ = conditional (is_some (get_locale thy name)) (fn () =>
  1782       error ("Duplicate definition of locale " ^ quote name));
  1783 
  1784     val thy_ctxt = ProofContext.init thy;
  1785     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  1786       text as (parms, ((_, exts'), _), defs)) =
  1787       prep_ctxt raw_import raw_body thy_ctxt;
  1788     val elemss = import_elemss @ body_elemss |>
  1789         map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  1790     val import = prep_expr thy raw_import;
  1791 
  1792     val extraTs = foldr Term.add_term_tfrees [] exts' \\
  1793       foldr Term.add_typ_tfrees [] (map snd parms);
  1794     val _ = if null extraTs then ()
  1795       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  1796 
  1797     val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
  1798           pred_thy), (import, regs)) =
  1799       if do_predicate then
  1800         let
  1801           val (elemss', defns) = change_defines_elemss thy elemss [];
  1802           val elemss'' = elemss' @ [(("", []), defns)];
  1803           val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
  1804             define_preds bname text elemss'' thy;
  1805           fun mk_regs elemss wits =
  1806             fold_map (fn (id, elems) => fn wts => let
  1807                 val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
  1808                   SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
  1809                 val (wts1, wts2) = chop (length ts) wts
  1810               in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
  1811           val regs = mk_regs elemss''' axioms |>
  1812                 map_filter (fn (("", _), _) => NONE | e => SOME e);
  1813         in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
  1814       else ((((elemss, ([], []), []), ([], [])), thy), (import, []));
  1815 
  1816     fun axiomify axioms elemss =
  1817       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  1818                    val ts = flat (map_filter (fn (Assumes asms) =>
  1819                      SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  1820                    val (axs1, axs2) = chop (length ts) axs;
  1821                  in (axs2, ((id, Assumed axs1), elems)) end)
  1822         |> snd;
  1823     val pred_ctxt = ProofContext.init pred_thy;
  1824     val (ctxt, (_, facts)) = activate_facts true (K I)
  1825       (pred_ctxt, axiomify predicate_axioms elemss');
  1826     val export = singleton (ProofContext.export_standard
  1827         (Assumption.add_view thy_ctxt predicate_statement ctxt) thy_ctxt);
  1828     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  1829     val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
  1830     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  1831     val axs' = map (Element.assume_witness pred_thy) stmt';
  1832     val thy' = pred_thy
  1833       |> PureThy.note_thmss_qualified "" bname facts' |> snd
  1834       |> declare_locale name
  1835       |> put_locale name
  1836        {axiom = axs',
  1837         import = import,
  1838         elems = map (fn e => (e, stamp ())) elems'',
  1839         params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  1840         lparams = map #1 (params_of' body_elemss),
  1841         term_syntax = [],
  1842         regs = regs,
  1843         intros = intros};
  1844   in ((name, ProofContext.transfer thy' body_ctxt), thy') end;
  1845 
  1846 in
  1847 
  1848 val add_locale = gen_add_locale read_context intern_expr;
  1849 val add_locale_i = gen_add_locale cert_context (K I);
  1850 
  1851 end;
  1852 
  1853 val _ = Context.add_setup
  1854  (add_locale_i true "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #> snd #>
  1855   add_locale_i true "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #> snd);
  1856 
  1857 
  1858 
  1859 (** locale goals **)
  1860 
  1861 local
  1862 
  1863 fun intern_attrib thy = map_elem (Element.map_ctxt
  1864   {name = I, var = I, typ = I, term = I, fact = I, attrib = Attrib.intern_src thy});
  1865 
  1866 val global_goal = Proof.global_goal ProofDisplay.present_results
  1867   Attrib.attribute_i ProofContext.bind_propp_schematic_i;
  1868 
  1869 fun mk_shows prep_att stmt ctxt =
  1870   ((Attrib.map_specs prep_att stmt, []), fold (fold (Variable.fix_frees o fst) o snd) stmt ctxt);
  1871 
  1872 fun conclusion prep_att (Element.Shows concl) = (([], concl), mk_shows prep_att)
  1873   | conclusion _ (Element.Obtains cases) = apfst (apfst (map Elem)) (Obtain.statement cases);
  1874 
  1875 fun gen_theorem prep_src prep_elem prep_stmt
  1876     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl thy =
  1877   let
  1878     val atts = map (prep_src thy) raw_atts;
  1879     val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl;
  1880 
  1881     val thy_ctxt = ProofContext.init thy;
  1882     val elems = map (prep_elem thy) (raw_elems @ concl_elems);
  1883     val (_, _, elems_ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt;
  1884     val ((stmt, facts), goal_ctxt) = mk_stmt (map fst concl ~~ propp) elems_ctxt;
  1885 
  1886     fun after_qed' results goal_ctxt' =
  1887       thy_ctxt
  1888       |> ProofContext.transfer (ProofContext.theory_of goal_ctxt')
  1889       |> after_qed results;
  1890   in
  1891     global_goal kind before_qed after_qed' (SOME "") (name, atts) stmt goal_ctxt
  1892     |> Proof.refine_insert facts
  1893   end;
  1894 
  1895 fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt no_target
  1896     kind before_qed after_qed raw_loc (name, atts) raw_elems raw_concl thy =
  1897   let
  1898     val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl;
  1899     val loc = prep_locale thy raw_loc;
  1900     val loc_atts = map (prep_src thy) atts;
  1901     val loc_attss = map (map (prep_src thy) o snd o fst) concl;
  1902     val target = if no_target then NONE else SOME (extern thy loc);
  1903     val elems = map (prep_elem thy) (raw_elems @ concl_elems);
  1904     val names = map (fst o fst) concl;
  1905 
  1906     val thy_ctxt = init_term_syntax loc (ProofContext.init thy);
  1907     val (_, loc_ctxt, elems_ctxt, propp) =
  1908       prep_stmt (SOME raw_loc) elems (map snd concl) thy_ctxt;
  1909     val ((stmt, facts), goal_ctxt) = mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt;
  1910 
  1911     fun after_qed' results goal_ctxt' =
  1912       let
  1913         val loc_ctxt' = loc_ctxt |> ProofContext.transfer (ProofContext.theory_of goal_ctxt');
  1914         val loc_results = results |> burrow (ProofContext.export_standard goal_ctxt' loc_ctxt');
  1915       in
  1916         loc_ctxt'
  1917         |> locale_results kind loc ((names ~~ loc_attss) ~~ loc_results)
  1918         |-> (fn res =>
  1919           if name = "" andalso null loc_atts then I
  1920           else #2 o locale_results kind loc [((name, loc_atts), maps #2 res)])
  1921         |> after_qed loc_results results
  1922       end;
  1923   in
  1924     global_goal kind before_qed after_qed' target (name, []) stmt goal_ctxt
  1925     |> Proof.refine_insert facts
  1926   end;
  1927 
  1928 in
  1929 
  1930 val theorem = gen_theorem Attrib.intern_src intern_attrib read_context_statement;
  1931 val theorem_i = gen_theorem (K I) (K I) cert_context_statement;
  1932 
  1933 val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src intern_attrib
  1934   read_context_statement false;
  1935 
  1936 val theorem_in_locale_i = gen_theorem_in_locale (K I) (K I) (K I)
  1937   cert_context_statement false;
  1938 
  1939 val theorem_in_locale_no_target = gen_theorem_in_locale (K I) (K I) (K I)
  1940   cert_context_statement true;
  1941 
  1942 fun smart_theorem kind NONE a [] (Element.Shows concl) =
  1943       Proof.theorem kind NONE (K I) (SOME "") a concl o ProofContext.init
  1944   | smart_theorem kind NONE a elems concl =
  1945       theorem kind NONE (K I) a elems concl
  1946   | smart_theorem kind (SOME loc) a elems concl =
  1947       theorem_in_locale kind NONE (K (K I)) loc a elems concl;
  1948 
  1949 end;
  1950 
  1951 
  1952 (** Normalisation of locale statements ---
  1953     discharges goals implied by interpretations **)
  1954 
  1955 local
  1956 
  1957 fun locale_assm_intros thy =
  1958   Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
  1959     (#2 (GlobalLocalesData.get thy)) [];
  1960 fun locale_base_intros thy =
  1961   Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
  1962     (#2 (GlobalLocalesData.get thy)) [];
  1963 
  1964 fun all_witnesses ctxt =
  1965   let
  1966     val thy = ProofContext.theory_of ctxt;
  1967     fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
  1968         (Registrations.dest thy regs |> map (fn (_, (_, wits)) =>
  1969           map Element.conclude_witness wits) |> flat) @ thms)
  1970       registrations [];
  1971     val globals = get (#3 (GlobalLocalesData.get thy));
  1972     val locals = get (LocalLocalesData.get ctxt);
  1973   in globals @ locals end;
  1974 (* FIXME: proper varification *)
  1975 
  1976 in
  1977 
  1978 fun intro_locales_tac eager ctxt facts st =
  1979   let
  1980     val wits = all_witnesses ctxt |> map Thm.varifyT;
  1981     val thy = ProofContext.theory_of ctxt;
  1982     val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
  1983   in
  1984     (ALLGOALS (Method.insert_tac facts THEN'
  1985         REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
  1986       THEN Tactic.distinct_subgoals_tac) st
  1987   end;
  1988 
  1989 val _ = Context.add_setup (Method.add_methods
  1990   [("intro_locales",
  1991     Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
  1992     "back-chain introduction rules of locales without unfolding predicates"),
  1993    ("unfold_locales",
  1994     Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
  1995     "back-chain all introduction rules of locales")]);
  1996 
  1997 end;
  1998 
  1999 
  2000 (** Interpretation commands **)
  2001 
  2002 local
  2003 
  2004 (* extract proof obligations (assms and defs) from elements *)
  2005 
  2006 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
  2007   | extract_asms_elems ((id, Derived _), _) = (id, []);
  2008 
  2009 
  2010 (* activate instantiated facts in theory or context *)
  2011 
  2012 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
  2013         attn all_elemss new_elemss propss thmss thy_ctxt =
  2014     let
  2015       fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
  2016           let
  2017             val facts' = facts
  2018               (* discharge hyps in attributes *)
  2019               |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch)
  2020               (* insert interpretation attributes *)
  2021               |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
  2022               (* discharge hyps *)
  2023               |> map (apsnd (map (apfst (map disch))));
  2024           in snd (note prfx facts' thy_ctxt) end
  2025         | activate_elem _ _ _ thy_ctxt = thy_ctxt;
  2026 
  2027       fun activate_elems disch ((id, _), elems) thy_ctxt =
  2028           let
  2029             val ((prfx, atts2), _) = the (get_reg thy_ctxt id)
  2030                 handle Option => sys_error ("Unknown registration of " ^
  2031                   quote (fst id) ^ " while activating facts.");
  2032           in
  2033             fold (activate_elem disch (prfx, atts2)) elems thy_ctxt
  2034           end;
  2035 
  2036       val thy_ctxt' = thy_ctxt
  2037         (* add registrations *)
  2038         |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
  2039         (* add witnesses of Assumed elements *)
  2040         |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
  2041 
  2042       val prems = flat (map_filter
  2043             (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
  2044               | ((_, Derived _), _) => NONE) all_elemss);
  2045       val thy_ctxt'' = thy_ctxt'
  2046         (* add witnesses of Derived elements *)
  2047         |> fold (fn (id, thms) => fold (add_wit id o Element.satisfy_witness prems) thms)
  2048            (map_filter (fn ((_, Assumed _), _) => NONE
  2049               | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
  2050 
  2051       val disch' = std o Element.satisfy_thm prems;  (* FIXME *)
  2052     in
  2053       thy_ctxt''
  2054         (* add facts to theory or context *)
  2055         |> fold (activate_elems disch') new_elemss
  2056     end;
  2057 
  2058 fun global_activate_facts_elemss x = gen_activate_facts_elemss
  2059       (fn thy => fn (name, ps) =>
  2060         get_global_registration thy (name, map Logic.varify ps))
  2061       (global_note_prefix_i "")
  2062       Attrib.attribute_i Drule.standard
  2063       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
  2064       (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
  2065         Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
  2066         (* FIXME *)) x;
  2067 
  2068 fun local_activate_facts_elemss x = gen_activate_facts_elemss
  2069       get_local_registration
  2070       local_note_prefix_i
  2071       (Attrib.attribute_i o ProofContext.theory_of) I
  2072       put_local_registration
  2073       add_local_witness x;
  2074 
  2075 fun gen_prep_registration mk_ctxt is_local read_terms test_reg activate
  2076     attn expr insts thy_ctxt =
  2077   let
  2078     val ctxt = mk_ctxt thy_ctxt;
  2079     val thy = ProofContext.theory_of ctxt;
  2080 
  2081     val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
  2082     val pts = params_of_expr ctxt' [] (intern_expr thy expr)
  2083           ([], Symtab.empty, Symtab.empty);
  2084     val params_ids = make_params_ids (#1 pts);
  2085     val raw_params_elemss = make_raw_params_elemss pts;
  2086     val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
  2087           (([], Symtab.empty), Expr expr);
  2088     val ((parms, all_elemss, _), (_, (_, defs, _))) =
  2089           read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
  2090 
  2091     (** compute instantiation **)
  2092 
  2093     (* user input *)
  2094     val insts = if length parms < length insts
  2095          then error "More arguments than parameters in instantiation."
  2096          else insts @ replicate (length parms - length insts) NONE;
  2097     val (ps, pTs) = split_list parms;
  2098     val pvTs = map Logic.legacy_varifyT pTs;
  2099 
  2100     (* instantiations given by user *)
  2101     val given = map_filter (fn (_, (NONE, _)) => NONE
  2102          | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
  2103     val (given_ps, given_insts) = split_list given;
  2104     val tvars = foldr Term.add_typ_tvars [] pvTs;
  2105     val used = foldr Term.add_typ_varnames [] pvTs;
  2106     fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
  2107     val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
  2108     val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
  2109     val vars' = fold Term.add_varnames vs vars;
  2110     val _ = if null vars' then ()
  2111          else error ("Illegal schematic variable(s) in instantiation: " ^
  2112            commas_quote (map Syntax.string_of_vname vars'));
  2113     (* replace new types (which are TFrees) by ones with new names *)
  2114     val new_Tnames = foldr Term.add_term_tfree_names [] vs;
  2115     val new_Tnames' = Name.invent_list used "'a" (length new_Tnames);
  2116     val renameT =
  2117           if is_local then I
  2118           else Logic.legacy_unvarifyT o Term.map_type_tfree (fn (a, s) =>
  2119             TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
  2120     val rename =
  2121           if is_local then I
  2122           else Term.map_types renameT;
  2123 
  2124     val tinst = Symtab.make (map
  2125                 (fn ((x, 0), T) => (x, T |> renameT)
  2126                   | ((_, n), _) => sys_error "Internal error var in prep_registration") vinst);
  2127     val inst = Symtab.make (given_ps ~~ map rename vs);
  2128 
  2129     (* defined params without user input *)
  2130     val not_given = map_filter (fn (x, (NONE, T)) => SOME (x, T)
  2131          | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
  2132     fun add_def (p, pT) inst =
  2133       let
  2134         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  2135                NONE => error ("Instance missing for parameter " ^ quote p)
  2136              | SOME (Free (_, T), t) => (t, T);
  2137         val d = Element.inst_term (tinst, inst) t;
  2138       in Symtab.update_new (p, d) inst end;
  2139     val inst = fold add_def not_given inst;
  2140     val insts = (tinst, inst);
  2141     (* Note: insts contain no vars. *)
  2142 
  2143 
  2144     (** compute proof obligations **)
  2145 
  2146     (* restore "small" ids *)
  2147     val ids' = map (fn ((n, ps), (_, mode)) =>
  2148           ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
  2149         ids;
  2150     val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
  2151     (* instantiate ids and elements *)
  2152     val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  2153       ((n, map (Element.inst_term insts) ps),
  2154         map (fn Int e => Element.inst_ctxt thy insts e) elems)
  2155       |> apfst (fn id => (id, map_mode (map (Element.inst_witness thy insts)) mode)));
  2156 
  2157     (* remove fragments already registered with theory or context *)
  2158     val new_inst_elemss = filter (fn ((id, _), _) =>
  2159           not (test_reg thy_ctxt id)) inst_elemss;
  2160     val new_ids = map #1 new_inst_elemss;
  2161 
  2162     val propss = map extract_asms_elems new_inst_elemss;
  2163 
  2164     val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
  2165     val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
  2166 
  2167   in (propss, activate attn' inst_elemss new_inst_elemss propss) end;
  2168 
  2169 val prep_global_registration = gen_prep_registration
  2170      ProofContext.init false
  2171      (fn thy => fn sorts => fn used =>
  2172        Sign.read_def_terms (thy, K NONE, sorts) used true)
  2173      (fn thy => fn (name, ps) =>
  2174        test_global_registration thy (name, map Logic.varify ps))
  2175      global_activate_facts_elemss;
  2176 
  2177 val prep_local_registration = gen_prep_registration
  2178      I true
  2179      (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
  2180      smart_test_registration
  2181      local_activate_facts_elemss;
  2182 
  2183 fun prep_registration_in_locale target expr thy =
  2184   (* target already in internal form *)
  2185   let
  2186     val ctxt = ProofContext.init thy;
  2187     val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
  2188         (([], Symtab.empty), Expr (Locale target));
  2189     val fixed = the_locale thy target |> #params |> map #1;
  2190     val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
  2191         ((raw_target_ids, target_syn), Expr expr);
  2192     val (target_ids, ids) = chop (length raw_target_ids) all_ids;
  2193     val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
  2194 
  2195     (** compute proof obligations **)
  2196 
  2197     (* restore "small" ids, with mode *)
  2198     val ids' = map (apsnd snd) ids;
  2199     (* remove Int markers *)
  2200     val elemss' = map (fn (_, es) =>
  2201         map (fn Int e => e) es) elemss
  2202     (* extract assumptions and defs *)
  2203     val ids_elemss = ids' ~~ elemss';
  2204     val propss = map extract_asms_elems ids_elemss;
  2205 
  2206     (** activation function:
  2207         - add registrations to the target locale
  2208         - add induced registrations for all global registrations of
  2209           the target, unless already present
  2210         - add facts of induced registrations to theory **)
  2211 
  2212     val t_ids = map_filter
  2213         (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
  2214 
  2215     fun activate thmss thy = let
  2216         val satisfy = Element.satisfy_thm (flat thmss);
  2217         val ids_elemss_thmss = ids_elemss ~~ thmss;
  2218         val regs = get_global_registrations thy target;
  2219 
  2220         fun activate_id (((id, Assumed _), _), thms) thy =
  2221             thy |> put_registration_in_locale target id
  2222                 |> fold (add_witness_in_locale target id) thms
  2223           | activate_id _ thy = thy;
  2224 
  2225         fun activate_reg (vts, ((prfx, atts2), _)) thy = let
  2226             val (insts, wits) = collect_global_witnesses thy fixed t_ids vts;
  2227             fun inst_parms ps = map
  2228                   (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
  2229             val disch = Element.satisfy_thm wits;
  2230             val new_elemss = filter (fn (((name, ps), _), _) =>
  2231                 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
  2232             fun activate_assumed_id (((_, Derived _), _), _) thy = thy
  2233               | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
  2234                 val ps' = inst_parms ps;
  2235               in
  2236                 if test_global_registration thy (name, ps')
  2237                 then thy
  2238                 else thy
  2239                   |> put_global_registration (name, ps') (prfx, atts2)
  2240                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2241                      (Element.inst_witness thy insts witn) thy) thms
  2242               end;
  2243 
  2244             fun activate_derived_id ((_, Assumed _), _) thy = thy
  2245               | activate_derived_id (((name, ps), Derived ths), _) thy = let
  2246                 val ps' = inst_parms ps;
  2247               in
  2248                 if test_global_registration thy (name, ps')
  2249                 then thy
  2250                 else thy
  2251                   |> put_global_registration (name, ps') (prfx, atts2)
  2252                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
  2253                        (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
  2254                        (Element.inst_term insts t,
  2255                         disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
  2256               end;
  2257 
  2258             fun activate_elem (Notes facts) thy =
  2259                 let
  2260                   val facts' = facts
  2261                       |> Attrib.map_facts (Attrib.attribute_i thy o
  2262                          Args.map_values I (Element.instT_type (#1 insts))
  2263                            (Element.inst_term insts)
  2264                            (disch o Element.inst_thm thy insts o satisfy))
  2265                       |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
  2266                       |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
  2267                 in
  2268                   thy
  2269                   |> global_note_prefix_i "" prfx facts'
  2270                   |> snd
  2271                 end
  2272               | activate_elem _ thy = thy;
  2273 
  2274             fun activate_elems (_, elems) thy = fold activate_elem elems thy;
  2275 
  2276           in thy |> fold activate_assumed_id ids_elemss_thmss
  2277                  |> fold activate_derived_id ids_elemss
  2278                  |> fold activate_elems new_elemss end;
  2279       in
  2280         thy |> fold activate_id ids_elemss_thmss
  2281             |> fold activate_reg regs
  2282       end;
  2283 
  2284   in (propss, activate) end;
  2285 
  2286 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
  2287   (("", []), map (rpair [] o Element.mark_witness) props));
  2288 
  2289 fun prep_result propps thmss =
  2290   ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
  2291 
  2292 fun goal_name thy kind target propss =
  2293     kind ^ Proof.goal_names (Option.map (extern thy) target) ""
  2294       (propss |> map (fn ((name, _), _) => extern thy name));
  2295 
  2296 in
  2297 
  2298 fun interpretation after_qed (prfx, atts) expr insts thy =
  2299   let
  2300     val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
  2301     val kind = goal_name thy "interpretation" NONE propss;
  2302     fun after_qed' results =
  2303       ProofContext.theory (activate (prep_result propss results))
  2304       #> after_qed;
  2305   in
  2306     ProofContext.init thy
  2307     |> Proof.theorem_i kind NONE after_qed' NONE ("", []) (prep_propp propss)
  2308     |> Element.refine_witness |> Seq.hd
  2309   end;
  2310 
  2311 fun interpretation_in_locale after_qed (raw_target, expr) thy =
  2312   let
  2313     val target = intern thy raw_target;
  2314     val (propss, activate) = prep_registration_in_locale target expr thy;
  2315     val kind = goal_name thy "interpretation" (SOME target) propss;
  2316     fun after_qed' locale_results results =
  2317       ProofContext.theory (activate (prep_result propss results))
  2318       #> after_qed;
  2319   in
  2320     thy
  2321     |> theorem_in_locale_no_target kind NONE after_qed' target ("", []) []
  2322       (Element.Shows (prep_propp propss))
  2323     |> Element.refine_witness |> Seq.hd
  2324   end;
  2325 
  2326 fun interpret after_qed (prfx, atts) expr insts int state =
  2327   let
  2328     val _ = Proof.assert_forward_or_chain state;
  2329     val ctxt = Proof.context_of state;
  2330     val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;
  2331     val kind = goal_name (Proof.theory_of state) "interpret" NONE propss;
  2332     fun after_qed' results =
  2333       Proof.map_context (K (ctxt |> activate (prep_result propss results)))
  2334       #> Proof.put_facts NONE
  2335       #> after_qed;
  2336   in
  2337     state
  2338     |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  2339       kind NONE after_qed' (prep_propp propss)
  2340     |> Element.refine_witness |> Seq.hd
  2341   end;
  2342 
  2343 end;
  2344 
  2345 end;