src/Pure/Isar/locale.ML
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 37133 1d048c6940c8
child 37471 907e13072675
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
     1 (*  Title:      Pure/Isar/locale.ML
     2     Author:     Clemens Ballarin, TU Muenchen
     3 
     4 Locales -- managed Isar proof contexts, based on Pure predicates.
     5 
     6 Draws basic ideas from Florian Kammueller's original version of
     7 locales, but uses the richer infrastructure of Isar instead of the raw
     8 meta-logic.  Furthermore, structured import of contexts (with merge
     9 and rename operations) are provided, as well as type-inference of the
    10 signature parts, and predicate definitions of the specification text.
    11 
    12 Interpretation enables the reuse of theorems of locales in other
    13 contexts, namely those defined by theories, structured proofs and
    14 locales themselves.
    15 
    16 See also:
    17 
    18 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    19     In Stefano Berardi et al., Types for Proofs and Programs: International
    20     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    21 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    22     Dependencies between Locales. Technical Report TUM-I0607, Technische
    23     Universitaet Muenchen, 2006.
    24 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    25     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    26     pages 31-43, 2006.
    27 *)
    28 
    29 signature LOCALE =
    30 sig
    31   (* Locale specification *)
    32   val register_locale: binding ->
    33     (string * sort) list * ((string * typ) * mixfix) list ->
    34     term option * term list ->
    35     thm option * thm option -> thm list ->
    36     declaration list ->
    37     (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
    38     (string * morphism) list -> theory -> theory
    39   val intern: theory -> xstring -> string
    40   val extern: theory -> string -> xstring
    41   val defined: theory -> string -> bool
    42   val params_of: theory -> string -> ((string * typ) * mixfix) list
    43   val intros_of: theory -> string -> thm option * thm option
    44   val axioms_of: theory -> string -> thm list
    45   val instance_of: theory -> string -> morphism -> term list
    46   val specification_of: theory -> string -> term option * term list
    47 
    48   (* Storing results *)
    49   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    50     Proof.context -> Proof.context
    51   val add_declaration: string -> declaration -> Proof.context -> Proof.context
    52   val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
    53 
    54   (* Activation *)
    55   val activate_declarations: string * morphism -> Proof.context -> Proof.context
    56   val activate_facts: string * morphism -> Context.generic -> Context.generic
    57   val init: string -> theory -> Proof.context
    58 
    59   (* Reasoning about locales *)
    60   val get_witnesses: Proof.context -> thm list
    61   val get_intros: Proof.context -> thm list
    62   val get_unfolds: Proof.context -> thm list
    63   val witness_add: attribute
    64   val intro_add: attribute
    65   val unfold_add: attribute
    66   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    67 
    68   (* Registrations and dependencies *)
    69   val add_registration: string * morphism -> (morphism * bool) option ->
    70     morphism -> theory -> theory
    71   val amend_registration: string * morphism -> morphism * bool ->
    72     morphism -> theory -> theory
    73   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
    74 
    75   (* Diagnostic *)
    76   val print_locales: theory -> unit
    77   val print_locale: theory -> bool -> xstring -> unit
    78   val print_registrations: theory -> string -> unit
    79 end;
    80 
    81 structure Locale: LOCALE =
    82 struct
    83 
    84 datatype ctxt = datatype Element.ctxt;
    85 
    86 
    87 (*** Theory data ***)
    88 
    89 datatype locale = Loc of {
    90   (** static part **)
    91   parameters: (string * sort) list * ((string * typ) * mixfix) list,
    92     (* type and term parameters *)
    93   spec: term option * term list,
    94     (* assumptions (as a single predicate expression) and defines *)
    95   intros: thm option * thm option,
    96   axioms: thm list,
    97   (** dynamic part **)
    98   syntax_decls: (declaration * serial) list,
    99     (* syntax declarations *)
   100   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
   101     (* theorem declarations *)
   102   dependencies: ((string * (morphism * morphism)) * serial) list
   103     (* locale dependencies (sublocale relation) *)
   104 };
   105 
   106 fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
   107   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
   108     syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
   109 
   110 fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
   111   mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
   112 
   113 fun merge_locale
   114  (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
   115   Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
   116     mk_locale
   117       ((parameters, spec, intros, axioms),
   118         ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
   119           merge (eq_snd op =) (notes, notes')),
   120             merge (eq_snd op =) (dependencies, dependencies')));
   121 
   122 structure Locales = Theory_Data
   123 (
   124   type T = locale Name_Space.table;
   125   val empty : T = Name_Space.empty_table "locale";
   126   val extend = I;
   127   val merge = Name_Space.join_tables (K merge_locale);
   128 );
   129 
   130 val intern = Name_Space.intern o #1 o Locales.get;
   131 val extern = Name_Space.extern o #1 o Locales.get;
   132 
   133 val get_locale = Symtab.lookup o #2 o Locales.get;
   134 val defined = Symtab.defined o #2 o Locales.get;
   135 
   136 fun the_locale thy name =
   137   (case get_locale thy name of
   138     SOME (Loc loc) => loc
   139   | NONE => error ("Unknown locale " ^ quote name));
   140 
   141 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
   142   thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
   143     (binding,
   144       mk_locale ((parameters, spec, intros, axioms),
   145         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
   146           map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
   147           (* FIXME *)
   148 
   149 fun change_locale name =
   150   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   151 
   152 fun print_locales thy =
   153   Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   154   |> Pretty.writeln;
   155 
   156 
   157 (*** Primitive operations ***)
   158 
   159 fun params_of thy = snd o #parameters o the_locale thy;
   160 
   161 fun intros_of thy = #intros o the_locale thy;
   162 
   163 fun axioms_of thy = #axioms o the_locale thy;
   164 
   165 fun instance_of thy name morph = params_of thy name |>
   166   map (Morphism.term morph o Free o #1);
   167 
   168 fun specification_of thy = #spec o the_locale thy;
   169 
   170 fun dependencies_of thy name = the_locale thy name |>
   171   #dependencies |> map fst;
   172 
   173 (* Print instance and qualifiers *)
   174 
   175 fun pretty_reg thy (name, morph) =
   176   let
   177     val name' = extern thy name;
   178     val ctxt = ProofContext.init_global thy;
   179     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   180     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   181     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   182     fun prt_term' t = if !show_types
   183       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   184         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   185       else prt_term t;
   186     fun prt_inst ts =
   187       Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   188 
   189     val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   190     val ts = instance_of thy name morph;
   191   in
   192     case qs of
   193        [] => prt_inst ts
   194      | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
   195          Pretty.brk 1, prt_inst ts]
   196   end;
   197 
   198 
   199 (*** Activate context elements of locale ***)
   200 
   201 (** Identifiers: activated locales in theory or proof context **)
   202 
   203 (* subsumption *)
   204 fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   205   (* smaller term is more general *)
   206 
   207 (* total order *)
   208 fun ident_ord ((n: string, ts), (m, ss)) =
   209   case fast_string_ord (m, n) of
   210       EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
   211     | ord => ord;
   212 
   213 local
   214 
   215 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
   216 
   217 structure Identifiers = Generic_Data
   218 (
   219   type T = (string * term list) list delayed;
   220   val empty = Ready [];
   221   val extend = I;
   222   val merge = ToDo;
   223 );
   224 
   225 fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2)
   226   | finish _ (Ready ids) = ids;
   227 
   228 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   229   (case Identifiers.get (Context.Theory thy) of
   230     Ready _ => NONE
   231   | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
   232 
   233 in
   234 
   235 val get_idents = (fn Ready ids => ids) o Identifiers.get;
   236 val put_idents = Identifiers.put o Ready;
   237 
   238 end;
   239 
   240 
   241 (** Resolve locale dependencies in a depth-first fashion **)
   242 
   243 local
   244 
   245 val roundup_bound = 120;
   246 
   247 fun add thy depth export (name, morph) (deps, marked) =
   248   if depth > roundup_bound
   249   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   250   else
   251     let
   252       val dependencies = dependencies_of thy name;
   253       val instance = instance_of thy name (morph $> export);
   254     in
   255       if member (ident_le thy) marked (name, instance)
   256       then (deps, marked)
   257       else
   258         let
   259           val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
   260           val marked' = (name, instance) :: marked;
   261           val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
   262         in
   263           ((name, morph) :: deps' @ deps, marked'')
   264         end
   265     end;
   266 
   267 in
   268 
   269 (* Note that while identifiers always have the external (exported) view, activate_dep
   270   is presented with the internal view. *)
   271 
   272 fun roundup thy activate_dep export (name, morph) (marked, input) =
   273   let
   274     (* Find all dependencies incuding new ones (which are dependencies enriching
   275       existing registrations). *)
   276     val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
   277     (* Filter out fragments from marked; these won't be activated. *)
   278     val dependencies' = filter_out (fn (name, morph) =>
   279       member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
   280   in
   281     (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
   282   end;
   283 
   284 end;
   285 
   286 
   287 (* Declarations, facts and entire locale content *)
   288 
   289 fun activate_syntax_decls (name, morph) context =
   290   let
   291     val thy = Context.theory_of context;
   292     val {syntax_decls, ...} = the_locale thy name;
   293   in
   294     context
   295     |> fold_rev (fn (decl, _) => decl morph) syntax_decls
   296   end;
   297 
   298 fun activate_notes activ_elem transfer thy (name, morph) input =
   299   let
   300     val {notes, ...} = the_locale thy name;
   301     fun activate ((kind, facts), _) input =
   302       let
   303         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   304       in activ_elem (Notes (kind, facts')) input end;
   305   in
   306     fold_rev activate notes input
   307   end;
   308 
   309 fun activate_all name thy activ_elem transfer (marked, input) =
   310   let
   311     val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
   312     val input' = input |>
   313       (not (null params) ?
   314         activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
   315       (* FIXME type parameters *)
   316       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
   317       (if not (null defs)
   318         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   319         else I);
   320     val activate = activate_notes activ_elem transfer thy;
   321   in
   322     roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   323   end;
   324 
   325 
   326 (** Public activation functions **)
   327 
   328 fun activate_declarations dep = Context.proof_map (fn context =>
   329   let
   330     val thy = Context.theory_of context;
   331   in
   332     roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
   333     |-> put_idents
   334   end);
   335 
   336 fun activate_facts dep context =
   337   let
   338     val thy = Context.theory_of context;
   339     val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
   340   in roundup thy activate Morphism.identity dep (get_idents context, context) |-> put_idents end;
   341 
   342 fun init name thy =
   343   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
   344     ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
   345 
   346 fun print_locale thy show_facts raw_name =
   347   let
   348     val name = intern thy raw_name;
   349     val ctxt = init name thy;
   350     fun cons_elem (elem as Notes _) = show_facts ? cons elem
   351       | cons_elem elem = cons elem;
   352     val elems =
   353       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   354       |> snd |> rev;
   355   in
   356     Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   357     |> Pretty.writeln
   358   end;
   359 
   360 
   361 (*** Registrations: interpretations in theories ***)
   362 
   363 structure Idtab = Table(type key = string * term list val ord = ident_ord);
   364 
   365 structure Registrations = Theory_Data
   366 (
   367   type T = ((morphism * morphism) * serial) Idtab.table *
   368     (* registrations, indexed by locale name and instance;
   369        serial points to mixin list *)
   370     (((morphism * bool) * serial) list) Inttab.table;
   371     (* table of mixin lists, per list mixins in reverse order of declaration;
   372        lists indexed by registration serial,
   373        entries for empty lists may be omitted *)
   374   val empty = (Idtab.empty, Inttab.empty);
   375   val extend = I;
   376   fun merge ((reg1, mix1), (reg2, mix2)) : T =
   377     (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
   378         if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
   379       Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2))
   380     handle Idtab.DUP id =>
   381       (* distinct interpretations with same base: merge their mixins *)
   382       let
   383         val (_, s1) = Idtab.lookup reg1 id |> the;
   384         val (morph2, s2) = Idtab.lookup reg2 id |> the;
   385         val reg2' = Idtab.update (id, (morph2, s1)) reg2;
   386         val mix2' = case Inttab.lookup mix2 s2 of
   387               NONE => mix2 |
   388               SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
   389         val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
   390         (* FIXME print interpretations,
   391            which is not straightforward without theory context *)
   392       in merge ((reg1, mix1), (reg2', mix2')) end;
   393     (* FIXME consolidate with dependencies, consider one data slot only *)
   394 );
   395 
   396 
   397 (* Primitive operations *)
   398 
   399 fun add_reg thy export (name, morph) =
   400   Registrations.map (apfst (Idtab.insert (K false)
   401     ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
   402 
   403 fun add_mixin serial' mixin =
   404   (* registration to be amended identified by its serial id *)
   405   Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
   406 
   407 fun get_mixins thy (name, morph) =
   408   let
   409     val (regs, mixins) = Registrations.get thy;
   410   in
   411     case Idtab.lookup regs (name, instance_of thy name morph) of
   412       NONE => []
   413     | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
   414   end;
   415 
   416 fun collect_mixins thy (name, morph) =
   417   roundup thy (fn dep => fn mixins =>
   418     merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
   419   |> snd |> filter (snd o fst);  (* only inheritable mixins *) (* FIXME *)
   420   (* FIXME refactor usage *)
   421 
   422 fun compose_mixins mixins =
   423   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
   424 
   425 fun reg_morph mixins ((name, (base, export)), serial) =
   426   let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
   427   in (name, base $> mix $> export) end;
   428 
   429 fun these_registrations thy name = Registrations.get thy
   430   |>> Idtab.dest
   431   |>> filter (curry (op =) name o fst o fst)
   432   (* with inherited mixins *)
   433   |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
   434     (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
   435 
   436 fun all_registrations thy = Registrations.get thy (* FIXME clone *)
   437   |>> Idtab.dest
   438   (* with inherited mixins *)
   439   |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
   440     (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
   441 
   442 fun activate_notes' activ_elem transfer thy export (name, morph) input =
   443   let
   444     val {notes, ...} = the_locale thy name;
   445     fun activate ((kind, facts), _) input =
   446       let
   447         val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
   448         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
   449       in activ_elem (Notes (kind, facts')) input end;
   450   in
   451     fold_rev activate notes input
   452   end;
   453 
   454 fun activate_facts' export dep context =
   455   let
   456     val thy = Context.theory_of context;
   457     val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
   458   in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
   459 
   460 
   461 (* Diagnostic *)
   462 
   463 fun print_registrations thy raw_name =
   464   (case these_registrations thy (intern thy raw_name) of
   465       [] => Pretty.str ("no interpretations")
   466     | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   467   |> Pretty.writeln;
   468 
   469 
   470 (* Add and extend registrations *)
   471 
   472 fun amend_registration (name, morph) mixin export thy =
   473   let
   474     val regs = Registrations.get thy |> fst;
   475     val base = instance_of thy name (morph $> export);
   476   in
   477     case Idtab.lookup regs (name, base) of
   478         NONE => error ("No interpretation of locale " ^
   479           quote (extern thy name) ^ " and\nparameter instantiation " ^
   480           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   481           " available")
   482       | SOME (_, serial') => add_mixin serial' mixin thy
   483   end;
   484 
   485 (* Note that a registration that would be subsumed by an existing one will not be
   486    generated, and it will not be possible to amend it. *)
   487 
   488 fun add_registration (name, base_morph) mixin export thy =
   489   let
   490     val mix = case mixin of NONE => Morphism.identity
   491           | SOME (mix, _) => mix;
   492     val morph = base_morph $> mix;
   493     val inst = instance_of thy name morph;
   494   in
   495     if member (ident_le thy) (get_idents (Context.Theory thy)) (name, inst)
   496     then thy
   497     else
   498       (get_idents (Context.Theory thy), thy)
   499       (* add new registrations with inherited mixins *)
   500       |> roundup thy (add_reg thy export) export (name, morph)
   501       |> snd
   502       (* add mixin *)
   503       |> (case mixin of NONE => I
   504            | SOME mixin => amend_registration (name, morph) mixin export)
   505       (* activate import hierarchy as far as not already active *)
   506       |> Context.theory_map (activate_facts' export (name, morph))
   507   end;
   508 
   509 
   510 (*** Dependencies ***)
   511 
   512 fun add_dependency loc (name, morph) export thy =
   513   let
   514     val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
   515     val (_, regs) = fold_rev (roundup thy' cons export)
   516       (all_registrations thy') (get_idents (Context.Theory thy'), []);
   517   in
   518     thy'
   519     |> fold_rev (fn dep => add_registration dep NONE export) regs
   520   end;
   521 
   522 
   523 (*** Storing results ***)
   524 
   525 (* Theorems *)
   526 
   527 fun add_thmss loc kind args ctxt =
   528   let
   529     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   530     val ctxt'' = ctxt' |> ProofContext.theory (
   531       (change_locale loc o apfst o apsnd) (cons (args', serial ()))
   532         #>
   533       (* Registrations *)
   534       (fn thy => fold_rev (fn (_, morph) =>
   535             let
   536               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   537                 Attrib.map_facts (Attrib.attribute_i thy)
   538             in PureThy.note_thmss kind args'' #> snd end)
   539         (these_registrations thy loc) thy))
   540   in ctxt'' end;
   541 
   542 
   543 (* Declarations *)
   544 
   545 fun add_declaration loc decl =
   546   add_thmss loc ""
   547     [((Binding.conceal Binding.empty,
   548         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
   549       [([Drule.dummy_thm], [])])];
   550 
   551 fun add_syntax_declaration loc decl =
   552   ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   553   #> add_declaration loc decl;
   554 
   555 
   556 (*** Reasoning about locales ***)
   557 
   558 (* Storage for witnesses, intro and unfold rules *)
   559 
   560 structure Thms = Generic_Data
   561 (
   562   type T = thm list * thm list * thm list;
   563   val empty = ([], [], []);
   564   val extend = I;
   565   fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   566    (Thm.merge_thms (witnesses1, witnesses2),
   567     Thm.merge_thms (intros1, intros2),
   568     Thm.merge_thms (unfolds1, unfolds2));
   569 );
   570 
   571 val get_witnesses = #1 o Thms.get o Context.Proof;
   572 val get_intros = #2 o Thms.get o Context.Proof;
   573 val get_unfolds = #3 o Thms.get o Context.Proof;
   574 
   575 val witness_add =
   576   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   577 val intro_add =
   578   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   579 val unfold_add =
   580   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   581 
   582 
   583 (* Tactic *)
   584 
   585 fun gen_intro_locales_tac intros_tac eager ctxt =
   586   intros_tac
   587     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   588 
   589 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
   590 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
   591 
   592 val _ = Context.>> (Context.map_theory
   593  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
   594     "back-chain introduction rules of locales without unfolding predicates" #>
   595   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
   596     "back-chain all introduction rules of locales"));
   597 
   598 end;