renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
1 (* Title: Pure/Isar/locale.ML
2 Author: Clemens Ballarin, TU Muenchen
4 Locales -- managed Isar proof contexts, based on Pure predicates.
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.
12 Interpretation enables the reuse of theorems of locales in other
13 contexts, namely those defined by theories, structured proofs and
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,
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 ->
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
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
55 val activate_declarations: string * morphism -> Proof.context -> Proof.context
56 val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
57 val init: string -> theory -> Proof.context
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
68 (* Registrations and dependencies *)
69 val add_registration: string * morphism -> (morphism * bool) option ->
70 morphism -> Context.generic -> Context.generic
71 val amend_registration: string * morphism -> morphism * bool ->
72 morphism -> Context.generic -> Context.generic
73 val registrations_of: Context.generic -> string -> (string * morphism) list
74 val add_dependency: string -> string * morphism -> morphism -> theory -> theory
77 val all_locales: theory -> string list
78 val print_locales: theory -> unit
79 val print_locale: theory -> bool -> xstring -> unit
80 val print_registrations: Proof.context -> string -> unit
81 val locale_deps: theory ->
82 { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
83 * term list list Symtab.table Symtab.table
86 structure Locale: LOCALE =
89 datatype ctxt = datatype Element.ctxt;
94 datatype locale = Loc of {
96 parameters: (string * sort) list * ((string * typ) * mixfix) list,
97 (* type and term parameters *)
98 spec: term option * term list,
99 (* assumptions (as a single predicate expression) and defines *)
100 intros: thm option * thm option,
103 syntax_decls: (declaration * serial) list,
104 (* syntax declarations *)
105 notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
106 (* theorem declarations *)
107 dependencies: ((string * (morphism * morphism)) * serial) list
108 (* locale dependencies (sublocale relation) *)
111 fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
112 Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
113 syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
115 fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
116 mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
119 (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
120 Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
122 ((parameters, spec, intros, axioms),
123 ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
124 merge (eq_snd op =) (notes, notes')),
125 merge (eq_snd op =) (dependencies, dependencies')));
127 structure Locales = Theory_Data
129 type T = locale Name_Space.table;
130 val empty : T = Name_Space.empty_table "locale";
132 val merge = Name_Space.join_tables (K merge_locale);
135 val intern = Name_Space.intern o #1 o Locales.get;
136 val extern = Name_Space.extern o #1 o Locales.get;
138 val get_locale = Symtab.lookup o #2 o Locales.get;
139 val defined = Symtab.defined o #2 o Locales.get;
141 fun the_locale thy name =
142 (case get_locale thy name of
143 SOME (Loc loc) => loc
144 | NONE => error ("Unknown locale " ^ quote name));
146 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
147 thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
149 mk_locale ((parameters, spec, intros, axioms),
150 ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
151 map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
154 fun change_locale name =
155 Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
158 (** Primitive operations **)
160 fun params_of thy = snd o #parameters o the_locale thy;
162 fun intros_of thy = #intros o the_locale thy;
164 fun axioms_of thy = #axioms o the_locale thy;
166 fun instance_of thy name morph = params_of thy name |>
167 map (Morphism.term morph o Free o #1);
169 fun specification_of thy = #spec o the_locale thy;
171 fun dependencies_of thy name = the_locale thy name |>
172 #dependencies |> map fst;
174 (* Print instance and qualifiers *)
176 fun pretty_reg thy (name, morph) =
178 val name' = extern thy name;
179 val ctxt = ProofContext.init_global thy;
180 fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
181 fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
182 val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
183 fun prt_term' t = if !show_types
184 then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
185 Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
188 Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
190 val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
191 val ts = instance_of thy name morph;
195 | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
196 Pretty.brk 1, prt_inst ts]
200 (*** Identifiers: activated locales in theory or proof context ***)
203 fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
204 (* smaller term is more general *)
207 fun ident_ord ((n: string, ts), (m, ss)) =
208 case fast_string_ord (m, n) of
209 EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
214 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
216 structure Identifiers = Generic_Data
218 type T = (string * term list) list delayed;
219 val empty = Ready [];
224 fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2)
225 | finish _ (Ready ids) = ids;
227 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
228 (case Identifiers.get (Context.Theory thy) of
230 | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
234 val get_idents = (fn Ready ids => ids) o Identifiers.get;
235 val put_idents = Identifiers.put o Ready;
240 (** Resolve locale dependencies in a depth-first fashion **)
244 val roundup_bound = 120;
246 fun add thy depth export (name, morph) (deps, marked) =
247 if depth > roundup_bound
248 then error "Roundup bound exceeded (sublocale relation probably not terminating)."
251 val dependencies = dependencies_of thy name;
252 val instance = instance_of thy name (morph $> export);
254 if member (ident_le thy) marked (name, instance)
258 val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
259 val marked' = (name, instance) :: marked;
260 val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
262 ((name, morph) :: deps' @ deps, marked'')
268 (* Note that while identifiers always have the external (exported) view, activate_dep
269 is presented with the internal view. *)
271 fun roundup thy activate_dep export (name, morph) (marked, input) =
273 (* Find all dependencies incuding new ones (which are dependencies enriching
274 existing registrations). *)
275 val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
276 (* Filter out fragments from marked; these won't be activated. *)
277 val dependencies' = filter_out (fn (name, morph) =>
278 member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
280 (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
286 (*** Registrations: interpretations in theories or proof contexts ***)
288 structure Idtab = Table(type key = string * term list val ord = ident_ord);
290 structure Registrations = Generic_Data
292 type T = ((morphism * morphism) * serial) Idtab.table *
293 (* registrations, indexed by locale name and instance;
294 serial points to mixin list *)
295 (((morphism * bool) * serial) list) Inttab.table;
296 (* table of mixin lists, per list mixins in reverse order of declaration;
297 lists indexed by registration serial,
298 entries for empty lists may be omitted *)
299 val empty = (Idtab.empty, Inttab.empty);
301 fun merge ((reg1, mix1), (reg2, mix2)) : T =
302 (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
303 if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
304 Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2))
305 handle Idtab.DUP id =>
306 (* distinct interpretations with same base: merge their mixins *)
308 val (_, s1) = Idtab.lookup reg1 id |> the;
309 val (morph2, s2) = Idtab.lookup reg2 id |> the;
310 val reg2' = Idtab.update (id, (morph2, s1)) reg2;
311 val mix2' = case Inttab.lookup mix2 s2 of
313 SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
314 val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
315 (* FIXME print interpretations,
316 which is not straightforward without theory context *)
317 in merge ((reg1, mix1), (reg2', mix2')) end;
318 (* FIXME consolidate with dependencies, consider one data slot only *)
322 (* Primitive operations *)
324 fun add_reg thy export (name, morph) =
325 Registrations.map (apfst (Idtab.insert (K false)
326 ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
328 fun add_mixin serial' mixin =
329 (* registration to be amended identified by its serial id *)
330 Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
332 fun get_mixins context (name, morph) =
334 val thy = Context.theory_of context;
335 val (regs, mixins) = Registrations.get context;
337 case Idtab.lookup regs (name, instance_of thy name morph) of
339 | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
342 fun compose_mixins mixins =
343 fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
345 fun collect_mixins context (name, morph) =
347 val thy = Context.theory_of context;
349 roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
350 Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
351 |> snd |> filter (snd o fst) (* only inheritable mixins *)
352 |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
356 fun get_registrations context select = Registrations.get context
357 |>> Idtab.dest |>> select
358 (* with inherited mixins *)
359 |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
360 (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
362 fun registrations_of context name =
363 get_registrations context (filter (curry (op =) name o fst o fst));
365 fun all_registrations context = get_registrations context I;
368 (*** Activate context elements of locale ***)
370 (* Declarations, facts and entire locale content *)
372 fun activate_syntax_decls (name, morph) context =
374 val thy = Context.theory_of context;
375 val {syntax_decls, ...} = the_locale thy name;
378 |> fold_rev (fn (decl, _) => decl morph) syntax_decls
381 fun activate_notes activ_elem transfer context export' (name, morph) input =
383 val thy = Context.theory_of context;
384 val {notes, ...} = the_locale thy name;
385 fun activate ((kind, facts), _) input =
387 val mixin = case export' of NONE => Morphism.identity
388 | SOME export => collect_mixins context (name, morph $> export) $> export;
389 val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin))
390 in activ_elem (Notes (kind, facts')) input end;
392 fold_rev activate notes input
395 fun activate_all name thy activ_elem transfer (marked, input) =
397 val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
398 val input' = input |>
400 activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
401 (* FIXME type parameters *)
402 (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
404 then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
406 val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
408 roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
412 (** Public activation functions **)
414 fun activate_declarations dep = Context.proof_map (fn context =>
416 val thy = Context.theory_of context;
418 roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
422 fun activate_facts export dep context =
424 val thy = Context.theory_of context;
425 val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
427 roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
428 dep (get_idents context, context)
433 activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
434 ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
437 (*** Add and extend registrations ***)
439 fun amend_registration (name, morph) mixin export context =
441 val thy = Context.theory_of context;
442 val regs = Registrations.get context |> fst;
443 val base = instance_of thy name (morph $> export);
445 case Idtab.lookup regs (name, base) of
446 NONE => error ("No interpretation of locale " ^
447 quote (extern thy name) ^ " and\nparameter instantiation " ^
448 space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
450 | SOME (_, serial') => add_mixin serial' mixin context
453 (* Note that a registration that would be subsumed by an existing one will not be
454 generated, and it will not be possible to amend it. *)
456 fun add_registration (name, base_morph) mixin export context =
458 val thy = Context.theory_of context;
459 val mix = case mixin of NONE => Morphism.identity
460 | SOME (mix, _) => mix;
461 val morph = base_morph $> mix;
462 val inst = instance_of thy name morph;
464 if member (ident_le thy) (get_idents context) (name, inst)
467 (get_idents context, context)
468 (* add new registrations with inherited mixins *)
469 |> roundup thy (add_reg thy export) export (name, morph)
472 |> (case mixin of NONE => I
473 | SOME mixin => amend_registration (name, morph) mixin export)
474 (* activate import hierarchy as far as not already active *)
475 |> activate_facts (SOME export) (name, morph)
479 (*** Dependencies ***)
481 fun add_dependency loc (name, morph) export thy =
483 val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
484 val context' = Context.Theory thy';
485 val (_, regs) = fold_rev (roundup thy' cons export)
486 (all_registrations context') (get_idents (context'), []);
489 |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
493 (*** Storing results ***)
497 fun add_thmss loc kind args ctxt =
499 val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
500 val ctxt'' = ctxt' |> ProofContext.background_theory
501 ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
504 (fn thy => fold_rev (fn (_, morph) =>
506 val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
507 Attrib.map_facts (Attrib.attribute_i thy)
508 in PureThy.note_thmss kind args'' #> snd end)
509 (registrations_of (Context.Theory thy) loc) thy))
515 fun add_declaration loc decl =
517 [((Binding.conceal Binding.empty,
518 [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
519 [([Drule.dummy_thm], [])])];
521 fun add_syntax_declaration loc decl =
522 ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
523 #> add_declaration loc decl;
526 (*** Reasoning about locales ***)
528 (* Storage for witnesses, intro and unfold rules *)
530 structure Thms = Generic_Data
532 type T = thm list * thm list * thm list;
533 val empty = ([], [], []);
535 fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
536 (Thm.merge_thms (witnesses1, witnesses2),
537 Thm.merge_thms (intros1, intros2),
538 Thm.merge_thms (unfolds1, unfolds2));
541 val get_witnesses = #1 o Thms.get o Context.Proof;
542 val get_intros = #2 o Thms.get o Context.Proof;
543 val get_unfolds = #3 o Thms.get o Context.Proof;
546 Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
548 Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
550 Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
555 fun gen_intro_locales_tac intros_tac eager ctxt =
557 (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
559 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
560 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
562 val _ = Context.>> (Context.map_theory
563 (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
564 "back-chain introduction rules of locales without unfolding predicates" #>
565 Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
566 "back-chain all introduction rules of locales"));
569 (*** diagnostic commands and interfaces ***)
571 val all_locales = Symtab.keys o snd o Locales.get;
573 fun print_locales thy =
574 Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
577 fun print_locale thy show_facts raw_name =
579 val name = intern thy raw_name;
580 val ctxt = init name thy;
581 fun cons_elem (elem as Notes _) = show_facts ? cons elem
582 | cons_elem elem = cons elem;
584 activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
587 Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
591 fun print_registrations ctxt raw_name =
593 val thy = ProofContext.theory_of ctxt;
595 (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
596 [] => Pretty.str ("no interpretations")
597 | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
601 fun locale_deps thy =
603 val names = all_locales thy
604 fun add_locale_node name =
606 val params = params_of thy name;
607 val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
608 val registrations = map (instance_of thy name o snd)
609 (registrations_of (Context.Theory thy) name);
611 Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
613 fun add_locale_deps name =
615 val dependencies = (map o apsnd) (instance_of thy name o op $>)
616 (dependencies_of thy name);
618 fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
619 deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
624 |> fold add_locale_node names
625 |> rpair Symtab.empty
626 |> fold add_locale_deps names