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