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