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