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