src/Pure/Isar/locale.ML
author ballarin
Tue Apr 20 22:34:17 2010 +0200 (2010-04-20)
changeset 36240 95a3fac5dcae
parent 36239 1385c4172d47
child 36610 bafd82950e24
child 36651 97c3bbe63389
permissions -rw-r--r--
Remove garbage.
     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) * 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, serial ())) dependencies))) #> snd);
   147 
   148 fun change_locale name =
   149   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   150 
   151 fun print_locales thy =
   152   Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   153   |> Pretty.writeln;
   154 
   155 
   156 (*** Primitive operations ***)
   157 
   158 fun params_of thy = snd o #parameters o the_locale thy;
   159 
   160 fun intros_of thy = #intros o the_locale thy;
   161 
   162 fun axioms_of thy = #axioms o the_locale thy;
   163 
   164 fun instance_of thy name morph = params_of thy name |>
   165   map (Morphism.term morph o Free o #1);
   166 
   167 fun specification_of thy = #spec o the_locale thy;
   168 
   169 fun dependencies_of thy name = the_locale thy name |>
   170   #dependencies |> map fst;
   171 
   172 
   173 (*** Activate context elements of locale ***)
   174 
   175 (** Identifiers: activated locales in theory or proof context **)
   176 
   177 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   178 (* FIXME: this is ident_le, smaller term is more general *)
   179 
   180 local
   181 
   182 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
   183 
   184 structure Identifiers = Generic_Data
   185 (
   186   type T = (string * term list) list delayed;
   187   val empty = Ready [];
   188   val extend = I;
   189   val merge = ToDo;
   190 );
   191 
   192 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   193   | finish _ (Ready ids) = ids;
   194 
   195 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   196   (case Identifiers.get (Context.Theory thy) of
   197     Ready _ => NONE
   198   | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
   199 
   200 in
   201 
   202 val get_idents = (fn Ready ids => ids) o Identifiers.get;
   203 val put_idents = Identifiers.put o Ready;
   204 
   205 end;
   206 
   207 
   208 (** Resolve locale dependencies in a depth-first fashion **)
   209 
   210 local
   211 
   212 val roundup_bound = 120;
   213 
   214 fun add thy depth export (name, morph) (deps, marked) =
   215   if depth > roundup_bound
   216   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   217   else
   218     let
   219       val dependencies = dependencies_of thy name;
   220       val instance = instance_of thy name (morph $> export);
   221     in
   222       if member (ident_eq thy) marked (name, instance)
   223       then (deps, marked)
   224       else
   225         let
   226           val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
   227           val marked' = (name, instance) :: marked;
   228           val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
   229         in
   230           ((name, morph) :: deps' @ deps, marked'')
   231         end
   232     end;
   233 
   234 in
   235 
   236 (* Note that while identifiers always have the external (exported) view, activate_dep
   237   is presented with the internal view. *)
   238 
   239 fun roundup thy activate_dep export (name, morph) (marked, input) =
   240   let
   241     (* Find all dependencies incuding new ones (which are dependencies enriching
   242       existing registrations). *)
   243     val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
   244     (* Filter out fragments from marked; these won't be activated. *)
   245     val dependencies' = filter_out (fn (name, morph) =>
   246       member (ident_eq thy) marked (name, instance_of thy name (morph $> export))) dependencies;
   247   in
   248     (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
   249   end;
   250 
   251 end;
   252 
   253 
   254 (* Declarations, facts and entire locale content *)
   255 
   256 fun activate_syntax_decls (name, morph) context =
   257   let
   258     val thy = Context.theory_of context;
   259     val {syntax_decls, ...} = the_locale thy name;
   260   in
   261     context
   262     |> fold_rev (fn (decl, _) => decl morph) syntax_decls
   263   end;
   264 
   265 fun activate_notes activ_elem transfer thy (name, morph) input =
   266   let
   267     val {notes, ...} = the_locale thy name;
   268     fun activate ((kind, facts), _) input =
   269       let
   270         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   271       in activ_elem (Notes (kind, facts')) input end;
   272   in
   273     fold_rev activate notes input
   274   end;
   275 
   276 fun activate_all name thy activ_elem transfer (marked, input) =
   277   let
   278     val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
   279     val input' = input |>
   280       (not (null params) ?
   281         activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
   282       (* FIXME type parameters *)
   283       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
   284       (if not (null defs)
   285         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   286         else I);
   287     val activate = activate_notes activ_elem transfer thy;
   288   in
   289     roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   290   end;
   291 
   292 
   293 (** Public activation functions **)
   294 
   295 fun activate_declarations dep = Context.proof_map (fn context =>
   296   let
   297     val thy = Context.theory_of context;
   298   in
   299     roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
   300     |-> put_idents
   301   end);
   302 
   303 fun activate_facts dep context =
   304   let
   305     val thy = Context.theory_of context;
   306     val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
   307   in roundup thy activate Morphism.identity dep (get_idents context, context) |-> put_idents end;
   308 
   309 fun init name thy =
   310   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
   311     ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
   312 
   313 fun print_locale thy show_facts raw_name =
   314   let
   315     val name = intern thy raw_name;
   316     val ctxt = init name thy;
   317     fun cons_elem (elem as Notes _) = show_facts ? cons elem
   318       | cons_elem elem = cons elem;
   319     val elems =
   320       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   321       |> snd |> rev;
   322   in
   323     Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   324     |> Pretty.writeln
   325   end;
   326 
   327 
   328 (*** Registrations: interpretations in theories ***)
   329 
   330 structure Registrations = Theory_Data
   331 (
   332   type T = ((string * (morphism * morphism)) * serial) list *
   333     (* registrations, in reverse order of declaration;
   334        serial points to mixin list *)
   335     (serial * ((morphism * bool) * serial) list) list;
   336     (* alist of mixin lists, per list mixins in reverse order of declaration;
   337        lists indexed by registration serial,
   338        entries for empty lists may be omitted *)
   339   val empty = ([], []);
   340   val extend = I;
   341   fun merge ((r1, m1), (r2, m2)) : T =
   342     (Library.merge (eq_snd op =) (r1, r2),
   343       AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
   344     (* FIXME consolidate with dependencies, consider one data slot only *)
   345 );
   346 
   347 
   348 (* Primitive operations *)
   349 
   350 fun add_reg export (dep, morph) =
   351   Registrations.map (apfst (cons ((dep, (morph, export)), serial ())));
   352 
   353 fun add_mixin serial' mixin =
   354   (* registration to be amended identified by its serial id *)
   355   Registrations.map (apsnd (AList.map_default (op =) (serial', []) (cons (mixin, serial ()))));
   356 
   357 fun get_mixins thy (name, morph) =
   358   let
   359     val (regs, mixins) = Registrations.get thy;
   360   in
   361     case find_first (fn ((name', (morph', export')), _) => ident_eq thy
   362       ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
   363       NONE => []
   364     | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
   365   end;
   366 
   367 fun collect_mixins thy (name, morph) =
   368   roundup thy (fn dep => fn mixins =>
   369     merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
   370   |> snd |> filter (snd o fst);  (* only inheritable mixins *)
   371   (* FIXME refactor usage *)
   372 
   373 fun compose_mixins mixins =
   374   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
   375 
   376 fun reg_morph mixins ((name, (base, export)), serial) =
   377   let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
   378   in (name, base $> mix $> export) end;
   379 
   380 fun these_registrations thy name = Registrations.get thy
   381   |>> filter (curry (op =) name o fst o fst)
   382   (* with inherited mixins *)
   383   |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
   384     (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
   385 
   386 fun all_registrations thy = Registrations.get thy
   387   |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
   388   (* without inherited mixins *)
   389 
   390 fun activate_notes' activ_elem transfer thy export (name, morph) input =
   391   let
   392     val {notes, ...} = the_locale thy name;
   393     fun activate ((kind, facts), _) input =
   394       let
   395         val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
   396         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
   397       in activ_elem (Notes (kind, facts')) input end;
   398   in
   399     fold_rev activate notes input
   400   end;
   401 
   402 fun activate_facts' export dep context =
   403   let
   404     val thy = Context.theory_of context;
   405     val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
   406   in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
   407 
   408 
   409 (* Diagnostic *)
   410 
   411 fun print_registrations thy raw_name =
   412   let
   413     val name = intern thy raw_name;
   414     val name' = extern thy name;
   415     val ctxt = ProofContext.init thy;
   416     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   417     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   418     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   419     fun prt_term' t = if !show_types
   420       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   421         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   422       else prt_term t;
   423     fun prt_inst ts =
   424       Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   425     fun prt_reg (name, morph) =
   426       let
   427         val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   428         val ts = instance_of thy name morph;
   429       in
   430         case qs of
   431            [] => prt_inst ts
   432          | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
   433              Pretty.brk 1, prt_inst ts]
   434       end;
   435   in
   436     (case these_registrations thy name of
   437         [] => Pretty.str ("no interpretations")
   438       | regs => Pretty.big_list "interpretations:" (map prt_reg (rev regs)))
   439     |> Pretty.writeln
   440   end;
   441 
   442 
   443 (* Add and extend registrations *)
   444 
   445 fun amend_registration (name, morph) mixin export thy =
   446   let
   447     val regs = Registrations.get thy |> fst;
   448     val base = instance_of thy name (morph $> export);
   449     fun match ((name', (morph', export')), _) =
   450       name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export'));
   451   in
   452     case find_first match (rev regs) of
   453         NONE => error ("No interpretation of locale " ^
   454           quote (extern thy name) ^ " and\nparameter instantiation " ^
   455           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   456           " available")
   457       | SOME (_, serial') => add_mixin serial' mixin thy
   458   end;
   459 
   460 (* Note that a registration that would be subsumed by an existing one will not be
   461    generated, and it will not be possible to amend it. *)
   462 
   463 fun add_registration (name, base_morph) mixin export thy =
   464   let
   465     val base = instance_of thy name base_morph;
   466   in
   467     if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
   468     then thy
   469     else
   470       (get_idents (Context.Theory thy), thy)
   471       (* add new registrations with inherited mixins *)
   472       |> roundup thy (add_reg export) export (name, base_morph)
   473       |> snd
   474       (* add mixin *)
   475       |> (case mixin of NONE => I
   476            | SOME mixin => amend_registration (name, base_morph) mixin export)
   477       (* activate import hierarchy as far as not already active *)
   478       |> Context.theory_map (activate_facts' export (name, base_morph))
   479   end;
   480 
   481 
   482 (*** Dependencies ***)
   483 
   484 fun add_reg_activate_facts export (dep, morph) thy =
   485   (get_idents (Context.Theory thy), thy)
   486   |> roundup thy (add_reg export) export (dep, morph)
   487   |> snd
   488   |> Context.theory_map (activate_facts' export (dep, morph));
   489 
   490 fun add_dependency loc (dep, morph) export thy =
   491   thy
   492   |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
   493   |> (fn thy => fold_rev (add_reg_activate_facts export)
   494       (all_registrations thy) thy);
   495 
   496 
   497 (*** Storing results ***)
   498 
   499 (* Theorems *)
   500 
   501 fun add_thmss loc kind args ctxt =
   502   let
   503     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   504     val ctxt'' = ctxt' |> ProofContext.theory (
   505       (change_locale loc o apfst o apsnd) (cons (args', serial ()))
   506         #>
   507       (* Registrations *)
   508       (fn thy => fold_rev (fn (_, morph) =>
   509             let
   510               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   511                 Attrib.map_facts (Attrib.attribute_i thy)
   512             in PureThy.note_thmss kind args'' #> snd end)
   513         (these_registrations thy loc) thy))
   514   in ctxt'' end;
   515 
   516 
   517 (* Declarations *)
   518 
   519 fun add_declaration loc decl =
   520   add_thmss loc ""
   521     [((Binding.conceal Binding.empty,
   522         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
   523       [([Drule.dummy_thm], [])])];
   524 
   525 fun add_syntax_declaration loc decl =
   526   ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   527   #> add_declaration loc decl;
   528 
   529 
   530 (*** Reasoning about locales ***)
   531 
   532 (* Storage for witnesses, intro and unfold rules *)
   533 
   534 structure Thms = Generic_Data
   535 (
   536   type T = thm list * thm list * thm list;
   537   val empty = ([], [], []);
   538   val extend = I;
   539   fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   540    (Thm.merge_thms (witnesses1, witnesses2),
   541     Thm.merge_thms (intros1, intros2),
   542     Thm.merge_thms (unfolds1, unfolds2));
   543 );
   544 
   545 val get_witnesses = #1 o Thms.get o Context.Proof;
   546 val get_intros = #2 o Thms.get o Context.Proof;
   547 val get_unfolds = #3 o Thms.get o Context.Proof;
   548 
   549 val witness_add =
   550   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   551 val intro_add =
   552   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   553 val unfold_add =
   554   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   555 
   556 
   557 (* Tactic *)
   558 
   559 fun gen_intro_locales_tac intros_tac eager ctxt =
   560   intros_tac
   561     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   562 
   563 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
   564 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
   565 
   566 val _ = Context.>> (Context.map_theory
   567  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
   568     "back-chain introduction rules of locales without unfolding predicates" #>
   569   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
   570     "back-chain all introduction rules of locales"));
   571 
   572 end;