src/Pure/Isar/locale.ML
author ballarin
Thu Feb 11 21:00:36 2010 +0100 (2010-02-11)
changeset 36091 055934ed89b0
parent 36090 87e950efb359
child 36093 0880493627ca
permissions -rw-r--r--
A rough implementation of full mixin inheritance; additional unit tests.
     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 * 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   val declarations_of: theory -> string -> declaration list * declaration list
    48 
    49   (* Storing results *)
    50   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    51     Proof.context -> Proof.context
    52   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    53   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    54   val add_declaration: string -> declaration -> Proof.context -> Proof.context
    55 
    56   (* Activation *)
    57   val activate_declarations: string * morphism -> Proof.context -> Proof.context
    58   val activate_facts: string * morphism -> Context.generic -> Context.generic
    59   val init: string -> theory -> Proof.context
    60 
    61   (* Reasoning about locales *)
    62   val get_witnesses: Proof.context -> thm list
    63   val get_intros: Proof.context -> thm list
    64   val get_unfolds: Proof.context -> thm list
    65   val witness_add: attribute
    66   val intro_add: attribute
    67   val unfold_add: attribute
    68   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    69 
    70   (* Registrations and dependencies *)
    71   val add_registration: string * morphism -> (morphism * bool) option ->
    72     morphism -> theory -> theory
    73   val amend_registration: string * morphism -> morphism * bool ->
    74     morphism -> theory -> theory
    75   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
    76 
    77   (* Diagnostic *)
    78   val print_locales: theory -> unit
    79   val print_locale: theory -> bool -> xstring -> unit
    80   val print_registrations: theory -> string -> unit
    81 end;
    82 
    83 structure Locale: LOCALE =
    84 struct
    85 
    86 datatype ctxt = datatype Element.ctxt;
    87 
    88 
    89 (*** Theory data ***)
    90 
    91 datatype locale = Loc of {
    92   (** static part **)
    93   parameters: (string * sort) list * ((string * typ) * mixfix) list,
    94     (* type and term parameters *)
    95   spec: term option * term list,
    96     (* assumptions (as a single predicate expression) and defines *)
    97   intros: thm option * thm option,
    98   axioms: thm list,
    99   (** dynamic part **)
   100   decls: (declaration * serial) list * (declaration * serial) list,
   101     (* type and term syntax declarations *)
   102   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
   103     (* theorem declarations *)
   104   dependencies: ((string * morphism) * serial) list
   105     (* locale dependencies (sublocale relation) *)
   106 };
   107 
   108 fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
   109   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
   110     decls = decls, notes = notes, dependencies = dependencies};
   111 
   112 fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
   113   mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
   114 
   115 fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
   116   notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
   117     dependencies = dependencies', ...}) = mk_locale
   118       ((parameters, spec, intros, axioms),
   119         (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
   120           merge (eq_snd op =) (notes, notes')),
   121             merge (eq_snd op =) (dependencies, dependencies')));
   122 
   123 structure Locales = Theory_Data
   124 (
   125   type T = locale Name_Space.table;
   126   val empty : T = Name_Space.empty_table "locale";
   127   val extend = I;
   128   val merge = Name_Space.join_tables (K merge_locale);
   129 );
   130 
   131 val intern = Name_Space.intern o #1 o Locales.get;
   132 val extern = Name_Space.extern o #1 o Locales.get;
   133 
   134 val get_locale = Symtab.lookup o #2 o Locales.get;
   135 val defined = Symtab.defined o #2 o Locales.get;
   136 
   137 fun the_locale thy name =
   138   (case get_locale thy name of
   139     SOME (Loc loc) => loc
   140   | NONE => error ("Unknown locale " ^ quote name));
   141 
   142 fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
   143   thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
   144     (binding,
   145       mk_locale ((parameters, spec, intros, axioms),
   146         ((pairself (map (fn decl => (decl, serial ()))) decls, map (fn n => (n, serial ())) notes),
   147           map (fn d => (d, serial ())) dependencies))) #> snd);
   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 declarations_of thy name = the_locale thy name |>
   171   #decls |> pairself (map fst);
   172 
   173 fun dependencies_of thy name = the_locale thy name |>
   174   #dependencies |> map fst;
   175 
   176 
   177 (*** Activate context elements of locale ***)
   178 
   179 (** Identifiers: activated locales in theory or proof context **)
   180 
   181 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   182 (* FIXME: this is ident_le, smaller term is more general *)
   183 
   184 local
   185 
   186 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
   187 
   188 structure Identifiers = Generic_Data
   189 (
   190   type T = (string * term list) list delayed;
   191   val empty = Ready [];
   192   val extend = I;
   193   val merge = ToDo;
   194 );
   195 
   196 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   197   | finish _ (Ready ids) = ids;
   198 
   199 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   200   (case Identifiers.get (Context.Theory thy) of
   201     Ready _ => NONE
   202   | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
   203 
   204 in
   205 
   206 val get_idents = (fn Ready ids => ids) o Identifiers.get;
   207 val put_idents = Identifiers.put o Ready;
   208 
   209 end;
   210 
   211 
   212 (** Resolve locale dependencies in a depth-first fashion **)
   213 
   214 local
   215 
   216 val roundup_bound = 120;
   217 
   218 fun add thy depth export (name, morph) (deps, marked) =
   219   if depth > roundup_bound
   220   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   221   else
   222     let
   223       val dependencies = dependencies_of thy name;
   224       val instance = instance_of thy name (morph $> export);
   225     in
   226       if member (ident_eq thy) marked (name, instance)
   227       then (deps, marked)
   228       else
   229         let
   230           val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
   231           val marked' = (name, instance) :: marked;
   232           val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
   233         in
   234           ((name, morph) :: deps' @ deps, marked'')
   235         end
   236     end;
   237 
   238 in
   239 
   240 (* Note that while identifiers always have the external (exported) view, activate_dep
   241   is presented with the internal view. *)
   242 
   243 fun roundup thy activate_dep export (name, morph) (marked, input) =
   244   let
   245     (* Find all dependencies incuding new ones (which are dependencies enriching
   246       existing registrations). *)
   247     val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
   248     (* Filter out fragments from marked; these won't be activated. *)
   249     val dependencies' = filter_out (fn (name, morph) =>
   250       member (ident_eq thy) marked (name, instance_of thy name (morph $> export))) dependencies;
   251   in
   252     (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
   253   end;
   254 
   255 end;
   256 
   257 
   258 (* Declarations, facts and entire locale content *)
   259 
   260 fun activate_decls (name, morph) context =
   261   let
   262     val thy = Context.theory_of context;
   263     val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   264   in
   265     context
   266     |> fold_rev (fn (decl, _) => decl morph) typ_decls
   267     |> fold_rev (fn (decl, _) => decl morph) term_decls
   268   end;
   269 
   270 fun activate_notes activ_elem transfer thy (name, morph) input =
   271   let
   272     val {notes, ...} = the_locale thy name;
   273     fun activate ((kind, facts), _) input =
   274       let
   275         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   276       in activ_elem (Notes (kind, facts')) input end;
   277   in
   278     fold_rev activate notes input
   279   end;
   280 
   281 fun activate_all name thy activ_elem transfer (marked, input) =
   282   let
   283     val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
   284     val input' = input |>
   285       (not (null params) ?
   286         activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
   287       (* FIXME type parameters *)
   288       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
   289       (if not (null defs)
   290         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   291         else I);
   292     val activate = activate_notes activ_elem transfer thy;
   293   in
   294     roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   295   end;
   296 
   297 
   298 (** Public activation functions **)
   299 
   300 fun activate_declarations dep = Context.proof_map (fn context =>
   301   let
   302     val thy = Context.theory_of context;
   303   in roundup thy activate_decls Morphism.identity dep (get_idents context, context) |-> put_idents end);
   304 
   305 fun activate_facts dep context =
   306   let
   307     val thy = Context.theory_of context;
   308     val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
   309   in roundup thy activate Morphism.identity dep (get_idents context, context) |-> put_idents end;
   310 
   311 fun init name thy =
   312   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
   313     ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
   314 
   315 fun print_locale thy show_facts raw_name =
   316   let
   317     val name = intern thy raw_name;
   318     val ctxt = init name thy;
   319     fun cons_elem (elem as Notes _) = show_facts ? cons elem
   320       | cons_elem elem = cons elem;
   321     val elems =
   322       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   323       |> snd |> rev;
   324   in
   325     Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   326     |> Pretty.writeln
   327   end;
   328 
   329 
   330 (*** Registrations: interpretations in theories ***)
   331 
   332 structure Registrations = Theory_Data
   333 (
   334   type T = ((string * (morphism * morphism)) * serial) list *
   335     (* registrations, in reverse order of declaration;
   336        serial points to mixin list *)
   337     (serial * ((morphism * bool) * serial) list) list;
   338     (* alist of mixin lists, per list mixins in reverse order of declaration;
   339        lists indexed by registration serial,
   340        entries for empty lists may be omitted *)
   341   val empty = ([], []);
   342   val extend = I;
   343   fun merge ((r1, m1), (r2, m2)) : T =
   344     (Library.merge (eq_snd op =) (r1, r2),
   345       AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
   346     (* FIXME consolidate with dependencies, consider one data slot only *)
   347 );
   348 
   349 
   350 (* Primitive operations *)
   351 
   352 fun get_mixins thy (name, morph) =
   353   let
   354     val (regs, mixins) = Registrations.get thy;
   355   in
   356     case find_first (fn ((name', (morph', export')), _) => ident_eq thy
   357       ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
   358       NONE => []
   359     | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
   360   end;
   361 
   362 fun collect_mixins thy (name, morph) =
   363   roundup thy (fn dep => fn mixins =>
   364     merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
   365   |> snd |> filter (snd o fst);  (* only inheritable mixins *)
   366 
   367 fun compose_mixins mixins =
   368   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
   369 
   370 fun reg_morph mixins ((name, (base, export)), serial) =
   371   let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
   372   in (name, base $> mix $> export) end;
   373 
   374 fun these_registrations thy name = Registrations.get thy
   375   |>> filter (curry (op =) name o fst o fst)
   376 (*  |-> (fn regs => fn mixins => map (reg_morph mixins) regs); *)
   377   |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
   378     (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
   379 
   380 fun all_registrations thy = Registrations.get thy
   381   |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
   382 
   383 fun activate_notes' activ_elem transfer thy export (name, morph) input =
   384   let
   385     val {notes, ...} = the_locale thy name;
   386     fun activate ((kind, facts), _) input =
   387       let
   388         val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
   389         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
   390       in activ_elem (Notes (kind, facts')) input end;
   391   in
   392     fold_rev activate notes input
   393   end;
   394 
   395 fun activate_facts' export dep context =
   396   let
   397     val thy = Context.theory_of context;
   398     val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
   399   in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
   400 
   401 
   402 (* Diagnostic *)
   403 
   404 fun print_registrations thy raw_name =
   405   let
   406     val name = intern thy raw_name;
   407     val name' = extern thy name;
   408     val ctxt = ProofContext.init thy;
   409     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   410     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   411     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   412     fun prt_term' t = if !show_types
   413       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   414         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   415       else prt_term t;
   416     fun prt_inst ts =
   417       Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   418     fun prt_reg (name, morph) =
   419       let
   420         val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   421         val ts = instance_of thy name morph;
   422       in
   423         case qs of
   424            [] => prt_inst ts
   425          | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
   426              Pretty.brk 1, prt_inst ts]
   427       end;
   428   in
   429     (case these_registrations thy name of
   430         [] => Pretty.str ("no interpretations")
   431       | regs => Pretty.big_list "interpretations:" (map prt_reg (rev regs)))
   432     |> Pretty.writeln
   433   end;
   434 
   435 
   436 (* Add and extend registrations *)
   437 
   438 fun amend_registration (name, morph) mixin export thy =
   439   let
   440     val regs = Registrations.get thy |> fst;
   441     val base = instance_of thy name (morph $> export);
   442     fun match ((name', (morph', export')), _) =
   443       name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export'));
   444   in
   445     case find_first match (rev regs) of
   446         NONE => error ("No interpretation of locale " ^
   447           quote (extern thy name) ^ " and\nparameter instantiation " ^
   448           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   449           " available")
   450       | SOME (_, serial') => Registrations.map 
   451           (apsnd (AList.map_default (op =) (serial', []) (cons (mixin, serial ())))) thy
   452     (* FIXME deal with inheritance: propagate to existing children *)
   453   end;
   454 
   455 (* Note that a registration that would be subsumed by an existing one will not be
   456    generated, and it will not be possible to amend it. *)
   457 
   458 fun add_registration (name, base_morph) mixin export thy =
   459   let
   460     val base = instance_of thy name base_morph;
   461   in
   462     if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
   463     then thy
   464     else
   465       let
   466         fun add_reg (dep', morph') =
   467           let
   468 (*            val mixins = collect_mixins thy (dep', morph' $> export); *)
   469             val mixins = [];  (* FIXME *)
   470             val serial = serial ();
   471           in
   472             Registrations.map (apfst (cons ((dep', (morph', export)), serial))
   473               #> not (null mixins) ? apsnd (cons (serial, mixins)))
   474           end
   475       in
   476         (get_idents (Context.Theory thy), thy)
   477         (* add new registrations with inherited mixins *)
   478         |> roundup thy add_reg export (name, base_morph)
   479         |> snd
   480         (* add mixin *)
   481         |> (case mixin of NONE => I
   482              | SOME mixin => amend_registration (name, base_morph) mixin export)
   483         (* activate import hierarchy as far as not already active *)
   484         |> Context.theory_map (activate_facts' export (name, base_morph))
   485       end
   486   end;
   487 
   488 
   489 (*** Dependencies ***)
   490 
   491 fun add_dependency loc (dep, morph) export thy =
   492   thy
   493   |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
   494   |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
   495       (all_registrations thy) thy);
   496   (* FIXME deal with inheritance: propagate mixins to new children *)
   497 
   498 
   499 (*** Storing results ***)
   500 
   501 (* Theorems *)
   502 
   503 fun add_thmss loc kind args ctxt =
   504   let
   505     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   506     val ctxt'' = ctxt' |> ProofContext.theory (
   507       (change_locale loc o apfst o apsnd) (cons (args', serial ()))
   508         #>
   509       (* Registrations *)
   510       (fn thy => fold_rev (fn (_, morph) =>
   511             let
   512               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   513                 Attrib.map_facts (Attrib.attribute_i thy)
   514             in PureThy.note_thmss kind args'' #> snd end)
   515         (these_registrations thy loc) thy))
   516 (* FIXME apply mixins *)
   517   in ctxt'' end;
   518 
   519 
   520 (* Declarations *)
   521 
   522 local
   523 
   524 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   525 
   526 fun add_decls add loc decl =
   527   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #>
   528   add_thmss loc ""
   529     [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
   530       [([Drule.dummy_thm], [])])];
   531 
   532 in
   533 
   534 val add_type_syntax = add_decls (apfst o cons);
   535 val add_term_syntax = add_decls (apsnd o cons);
   536 val add_declaration = add_decls (K I);
   537 
   538 end;
   539 
   540 
   541 (*** Reasoning about locales ***)
   542 
   543 (* Storage for witnesses, intro and unfold rules *)
   544 
   545 structure Thms = Generic_Data
   546 (
   547   type T = thm list * thm list * thm list;
   548   val empty = ([], [], []);
   549   val extend = I;
   550   fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   551    (Thm.merge_thms (witnesses1, witnesses2),
   552     Thm.merge_thms (intros1, intros2),
   553     Thm.merge_thms (unfolds1, unfolds2));
   554 );
   555 
   556 val get_witnesses = #1 o Thms.get o Context.Proof;
   557 val get_intros = #2 o Thms.get o Context.Proof;
   558 val get_unfolds = #3 o Thms.get o Context.Proof;
   559 
   560 val witness_add =
   561   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   562 val intro_add =
   563   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   564 val unfold_add =
   565   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   566 
   567 
   568 (* Tactic *)
   569 
   570 fun intro_locales_tac eager ctxt =
   571   Method.intros_tac
   572     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   573 
   574 val _ = Context.>> (Context.map_theory
   575  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
   576     "back-chain introduction rules of locales without unfolding predicates" #>
   577   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
   578     "back-chain all introduction rules of locales"));
   579 
   580 end;
   581