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