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