src/Pure/Isar/locale.ML
author ballarin
Mon Feb 01 21:55:00 2010 +0100 (2010-02-01)
changeset 36088 a4369989bc45
parent 33643 b275f26a638b
child 36090 87e950efb359
permissions -rw-r--r--
Use serial to be more debug friendly.
     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 * ((morphism * bool) * serial) list) list;
   337     (* alist of mixin lists, per list mixins in reverse order of declaration *)
   338   val empty = ([], []);
   339   val extend = I;
   340   fun merge ((r1, m1), (r2, m2)) : T =
   341     (Library.merge (eq_snd op =) (r1, r2),
   342       AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
   343     (* FIXME consolidate with dependencies, consider one data slot only *)
   344 );
   345 
   346 
   347 (* Primitive operations *)
   348 
   349 fun compose_mixins mixins =
   350   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
   351 
   352 fun reg_morph mixins ((name, (base, export)), serial) =
   353   let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
   354   in (name, base $> mix $> export) end;
   355 
   356 fun these_registrations thy name = Registrations.get thy
   357   |>> filter (curry (op =) name o fst o fst)
   358   |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
   359 
   360 fun all_registrations thy = Registrations.get thy
   361   |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
   362 
   363 fun get_mixins thy (name, morph) =
   364   let
   365     val (regs, mixins) = Registrations.get thy;
   366   in
   367     case find_first (fn ((name', (morph', export')), _) => ident_eq thy
   368       ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
   369       NONE => []
   370     | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
   371   end;
   372 
   373 fun collect_mixins thy (name, morph) =
   374   roundup thy (fn dep => fn mixins =>
   375     merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
   376   |> snd |> filter (snd o fst);  (* only inheritable mixins *)
   377 
   378 fun activate_notes' activ_elem transfer thy export (name, morph) input =
   379   let
   380     val {notes, ...} = the_locale thy name;
   381     fun activate ((kind, facts), _) input =
   382       let
   383         val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
   384         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
   385       in activ_elem (Notes (kind, facts')) input end;
   386   in
   387     fold_rev activate notes input
   388   end;
   389 
   390 fun activate_facts' export dep context =
   391   let
   392     val thy = Context.theory_of context;
   393     val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
   394   in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
   395 
   396 
   397 (* Diagnostic *)
   398 
   399 fun print_registrations thy raw_name =
   400   let
   401     val name = intern thy raw_name;
   402     val name' = extern thy name;
   403     val ctxt = ProofContext.init thy;
   404     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   405     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   406     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   407     fun prt_term' t = if !show_types
   408       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   409         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   410       else prt_term t;
   411     fun prt_inst ts =
   412       Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   413     fun prt_reg (name, morph) =
   414       let
   415         val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   416         val ts = instance_of thy name morph;
   417       in
   418         case qs of
   419            [] => prt_inst ts
   420          | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
   421              Pretty.brk 1, prt_inst ts]
   422       end;
   423   in
   424     (case these_registrations thy name of
   425         [] => Pretty.str ("no interpretations")
   426       | regs => Pretty.big_list "interpretations:" (map prt_reg (rev regs)))
   427     |> Pretty.writeln
   428   end;
   429 
   430 
   431 (* Add and extend registrations *)
   432 
   433 fun amend_registration (name, morph) mixin export thy =
   434   let
   435     val regs = Registrations.get thy |> fst;
   436     val base = instance_of thy name (morph $> export);
   437     fun match ((name', (morph', export')), _) =
   438       name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export'));
   439   in
   440     case find_first match (rev regs) of
   441         NONE => error ("No interpretation of locale " ^
   442           quote (extern thy name) ^ " and\nparameter instantiation " ^
   443           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   444           " available")
   445       | SOME (_, serial') => Registrations.map 
   446           (apsnd (AList.map_default (op =) (serial', []) (cons (mixin, serial ())))) thy
   447     (* FIXME deal with inheritance: propagate to existing children *)
   448   end;
   449 
   450 (* Note that a registration that would be subsumed by an existing one will not be
   451    generated, and it will not be possible to amend it. *)
   452 
   453 fun add_registration (name, base_morph) mixin export thy =
   454   let
   455     val base = instance_of thy name base_morph;
   456   in
   457     if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
   458     then thy
   459     else
   460       let
   461         fun add_reg (dep', morph') =
   462           let
   463             val mixins = collect_mixins thy (dep', morph' $> export);
   464             (* FIXME empty list *)
   465             val serial = serial ();
   466           in
   467             Registrations.map (apfst (cons ((dep', (morph', export)), serial))
   468               #> apsnd (cons (serial, mixins)))
   469           end
   470       in
   471         (get_idents (Context.Theory thy), thy)
   472         (* add new registrations with inherited mixins *)
   473         |> roundup thy add_reg export (name, base_morph)
   474         |> snd
   475         (* add mixin *)
   476         |> (case mixin of NONE => I
   477              | SOME mixin => amend_registration (name, base_morph) mixin export)
   478         (* activate import hierarchy as far as not already active *)
   479         |> Context.theory_map (activate_facts' export (name, base_morph))
   480       end
   481   end;
   482 
   483 
   484 (*** Dependencies ***)
   485 
   486 fun add_dependency loc (dep, morph) export thy =
   487   thy
   488   |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
   489   |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
   490       (all_registrations thy) thy);
   491   (* FIXME deal with inheritance: propagate mixins to new children *)
   492 
   493 
   494 (*** Storing results ***)
   495 
   496 (* Theorems *)
   497 
   498 fun add_thmss loc kind args ctxt =
   499   let
   500     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   501     val ctxt'' = ctxt' |> ProofContext.theory (
   502       (change_locale loc o apfst o apsnd) (cons (args', serial ()))
   503         #>
   504       (* Registrations *)
   505       (fn thy => fold_rev (fn (_, morph) =>
   506             let
   507               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   508                 Attrib.map_facts (Attrib.attribute_i thy)
   509             in PureThy.note_thmss kind args'' #> snd end)
   510         (these_registrations thy loc) thy))
   511   in ctxt'' end;
   512 
   513 
   514 (* Declarations *)
   515 
   516 local
   517 
   518 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   519 
   520 fun add_decls add loc decl =
   521   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #>
   522   add_thmss loc ""
   523     [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
   524       [([Drule.dummy_thm], [])])];
   525 
   526 in
   527 
   528 val add_type_syntax = add_decls (apfst o cons);
   529 val add_term_syntax = add_decls (apsnd o cons);
   530 val add_declaration = add_decls (K I);
   531 
   532 end;
   533 
   534 
   535 (*** Reasoning about locales ***)
   536 
   537 (* Storage for witnesses, intro and unfold rules *)
   538 
   539 structure Thms = Generic_Data
   540 (
   541   type T = thm list * thm list * thm list;
   542   val empty = ([], [], []);
   543   val extend = I;
   544   fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   545    (Thm.merge_thms (witnesses1, witnesses2),
   546     Thm.merge_thms (intros1, intros2),
   547     Thm.merge_thms (unfolds1, unfolds2));
   548 );
   549 
   550 val get_witnesses = #1 o Thms.get o Context.Proof;
   551 val get_intros = #2 o Thms.get o Context.Proof;
   552 val get_unfolds = #3 o Thms.get o Context.Proof;
   553 
   554 val witness_add =
   555   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   556 val intro_add =
   557   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   558 val unfold_add =
   559   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   560 
   561 
   562 (* Tactic *)
   563 
   564 fun intro_locales_tac eager ctxt =
   565   Method.intros_tac
   566     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   567 
   568 val _ = Context.>> (Context.map_theory
   569  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
   570     "back-chain introduction rules of locales without unfolding predicates" #>
   571   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
   572     "back-chain all introduction rules of locales"));
   573 
   574 end;
   575