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