removed obsolete theorem statements (cf. specification.ML);
1 (* Title: Pure/Isar/locale.ML
3 Author: Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
5 Locales -- Isar proof contexts as meta-level predicates, with local
6 syntax and implicit structures.
8 Draws basic ideas from Florian Kammueller's original version of
9 locales, but uses the richer infrastructure of Isar instead of the raw
10 meta-logic. Furthermore, structured import of contexts (with merge
11 and rename operations) are provided, as well as type-inference of the
12 signature parts, and predicate definitions of the specification text.
14 Interpretation enables the reuse of theorems of locales in other
15 contexts, namely those defined by theories, structured proofs and
20 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
21 In Stefano Berardi et al., Types for Proofs and Programs: International
22 Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
23 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
24 Dependencies between Locales. Technical Report TUM-I0607, Technische
25 Universitaet Muenchen, 2006.
26 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
27 Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
32 - beta-eta normalisation of interpretation parameters
33 - dangling type frees in locales
34 - test subsumption of interpretations when merging theories
41 Rename of expr * (string * mixfix option) option list |
44 datatype 'a element = Elem of 'a | Expr of expr
45 val map_elem: ('a -> 'b) -> 'a element -> 'b element
47 val intern: theory -> xstring -> string
48 val extern: theory -> string -> xstring
49 val init: string -> theory -> Proof.context
51 (* The specification of a locale *)
53 val parameters_of: theory -> string ->
54 ((string * typ) * mixfix) list
55 val parameters_of_expr: theory -> expr ->
56 ((string * typ) * mixfix) list
57 val local_asms_of: theory -> string ->
58 ((string * Attrib.src list) * term list) list
59 val global_asms_of: theory -> string ->
60 ((string * Attrib.src list) * term list) list
62 (* Processing of locale statements *)
63 val read_context_statement: xstring option -> Element.context element list ->
64 (string * string list) list list -> Proof.context ->
65 string option * Proof.context * Proof.context * (term * term list) list list
66 val read_context_statement_i: string option -> Element.context element list ->
67 (string * string list) list list -> Proof.context ->
68 string option * Proof.context * Proof.context * (term * term list) list list
69 val cert_context_statement: string option -> Element.context_i element list ->
70 (term * term list) list list -> Proof.context ->
71 string option * Proof.context * Proof.context * (term * term list) list list
72 val read_expr: expr -> Element.context list -> Proof.context ->
73 Element.context_i list * Proof.context
74 val cert_expr: expr -> Element.context_i list -> Proof.context ->
75 Element.context_i list * Proof.context
77 (* Diagnostic functions *)
78 val print_locales: theory -> unit
79 val print_locale: theory -> bool -> expr -> Element.context list -> unit
80 val print_global_registrations: bool -> string -> theory -> unit
81 val print_local_registrations': bool -> string -> Proof.context -> unit
82 val print_local_registrations: bool -> string -> Proof.context -> unit
84 val add_locale: bool -> bstring -> expr -> Element.context list -> theory
85 -> string * Proof.context
86 val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory
87 -> string * Proof.context
90 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
93 val add_thmss: string -> string ->
94 ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
95 Proof.context -> (string * thm list) list * Proof.context
96 val add_term_syntax: string -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context
98 val interpretation: (Proof.context -> Proof.context) ->
99 string * Attrib.src list -> expr -> string option list ->
100 theory -> Proof.state
101 val interpretation_in_locale: (Proof.context -> Proof.context) ->
102 xstring * expr -> theory -> Proof.state
103 val interpret: (Proof.state -> Proof.state Seq.seq) ->
104 string * Attrib.src list -> expr -> string option list ->
105 bool -> Proof.state -> Proof.state
108 structure Locale: LOCALE =
111 fun legacy_unvarifyT thm =
113 val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
114 val tvars = rev (Drule.fold_terms Term.add_tvars thm []);
115 val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
116 in Drule.instantiate' tfrees [] thm end;
118 fun legacy_unvarify raw_thm =
120 val thm = legacy_unvarifyT raw_thm;
121 val ct = Thm.cterm_of (Thm.theory_of_thm thm);
122 val vars = rev (Drule.fold_terms Term.add_vars thm []);
123 val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
124 in Drule.instantiate' [] frees thm end;
127 (** locale elements and expressions **)
129 datatype ctxt = datatype Element.ctxt;
133 Rename of expr * (string * mixfix option) option list |
136 val empty = Merge [];
138 datatype 'a element =
139 Elem of 'a | Expr of expr;
141 fun map_elem f (Elem e) = Elem (f e)
142 | map_elem _ (Expr e) = Expr e;
145 {axiom: Element.witness list,
146 (* For locales that define predicates this is [A [A]], where A is the locale
147 specification. Otherwise [].
148 Only required to generate the right witnesses for locales with predicates. *)
149 import: expr, (*dynamic import*)
150 elems: (Element.context_i * stamp) list,
151 (* Static content, neither Fixes nor Constrains elements *)
152 params: ((string * typ) * mixfix) list, (*all params*)
153 lparams: string list, (*local params*)
154 term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *)
155 regs: ((string * string list) * Element.witness list) list,
156 (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
157 intros: thm list * thm list}
158 (* Introduction rules: of delta predicate and locale predicate. *)
160 (* CB: an internal (Int) locale element was either imported or included,
161 an external (Ext) element appears directly in the locale text. *)
163 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
167 (** management of registrations in theories and proof contexts **)
169 structure Registrations :
174 val dest: theory -> T ->
175 (term list * ((string * Attrib.src list) * Element.witness list)) list
176 val lookup: theory -> T * term list ->
177 ((string * Attrib.src list) * Element.witness list) option
178 val insert: theory -> term list * (string * Attrib.src list) -> T ->
179 T * (term list * ((string * Attrib.src list) * Element.witness list)) list
180 val add_witness: term list -> Element.witness -> T -> T
183 (* a registration consists of theorems (actually, witnesses) instantiating locale
184 assumptions and prefix and attributes, indexed by parameter instantiation *)
185 type T = ((string * Attrib.src list) * Element.witness list) Termtab.table;
187 val empty = Termtab.empty;
189 (* term list represented as single term, for simultaneous matching *)
191 Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
193 let fun ut (Const _) ts = ts
194 | ut (s $ t) ts = ut s (t::ts)
197 (* joining of registrations: prefix and attributes of left theory,
198 thms are equal, no attempt to subsumption testing *)
199 fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);
201 fun dest_transfer thy regs =
202 Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy))));
204 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
206 (* registrations that subsume t *)
207 fun subsumers thy t regs =
208 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
210 (* look up registration, pick one that subsumes the query *)
211 fun lookup thy (regs, ts) =
214 val subs = subsumers thy t regs;
217 | ((t', (attn, thms)) :: _) => let
218 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
219 (* thms contain Frees, not Vars *)
220 val tinst' = tinst |> Vartab.dest
221 |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
223 val inst' = inst |> Vartab.dest
224 |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
227 SOME (attn, map (Element.inst_witness thy (tinst', inst')) thms)
231 (* add registration if not subsumed by ones already present,
232 additionally returns registrations that are strictly subsumed *)
233 fun insert thy (ts, attn) regs =
236 val subs = subsumers thy t regs ;
240 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
241 val sups' = map (apfst untermify) sups
242 in (Termtab.update (t, (attn, [])) regs, sups') end
246 (* add witness theorem to registration,
247 only if instantiation is exact, otherwise exception Option raised *)
248 fun add_witness ts thm regs =
251 val (x, thms) = the (Termtab.lookup regs t);
253 Termtab.update (t, (x, thm::thms)) regs
260 structure GlobalLocalesData = TheoryDataFun
262 val name = "Isar/locales";
263 type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
264 (* 1st entry: locale namespace,
265 2nd entry: locales of the theory,
266 3rd entry: registrations, indexed by locale name *)
268 val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
272 fun join_locs _ ({axiom, import, elems, params, lparams, term_syntax, regs, intros}: locale,
273 {elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) =
276 elems = gen_merge_lists (eq_snd (op =)) elems elems',
279 term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'),
280 regs = merge_alists regs regs',
282 fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
283 (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
284 Symtab.join (K Registrations.join) (regs1, regs2));
286 fun print _ (space, locs, _) =
287 Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
291 val _ = Context.add_setup GlobalLocalesData.init;
297 structure LocalLocalesData = ProofDataFun
299 val name = "Isar/locales";
300 type T = Registrations.T Symtab.table;
301 (* registrations, indexed by locale name *)
302 fun init _ = Symtab.empty;
306 val _ = Context.add_setup LocalLocalesData.init;
311 val print_locales = GlobalLocalesData.print;
313 val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
314 val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
316 fun declare_locale name thy =
317 thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
318 (Sign.declare_name thy name space, locs, regs));
320 fun put_locale name loc =
321 GlobalLocalesData.map (fn (space, locs, regs) =>
322 (space, Symtab.update (name, loc) locs, regs));
324 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;
326 fun the_locale thy name =
327 (case get_locale thy name of
329 | NONE => error ("Unknown locale " ^ quote name));
331 fun change_locale name f thy =
333 val {axiom, import, elems, params, lparams, term_syntax, regs, intros} =
335 val (axiom', import', elems', params', lparams', term_syntax', regs', intros') =
336 f (axiom, import, elems, params, lparams, term_syntax, regs, intros);
338 put_locale name {axiom = axiom', import = import', elems = elems',
339 params = params', lparams = lparams', term_syntax = term_syntax', regs = regs',
340 intros = intros'} thy
344 (* access registrations *)
346 (* Ids of global registrations are varified,
347 Ids of local registrations are not.
348 Thms of registrations are never varified. *)
350 (* retrieve registration from theory or context *)
352 fun gen_get_registrations get thy_of thy_ctxt name =
353 case Symtab.lookup (get thy_ctxt) name of
355 | SOME reg => Registrations.dest (thy_of thy_ctxt) reg;
357 val get_global_registrations =
358 gen_get_registrations (#3 o GlobalLocalesData.get) I;
359 val get_local_registrations =
360 gen_get_registrations LocalLocalesData.get ProofContext.theory_of;
362 fun gen_get_registration get thy_of thy_ctxt (name, ps) =
363 case Symtab.lookup (get thy_ctxt) name of
365 | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
367 val get_global_registration =
368 gen_get_registration (#3 o GlobalLocalesData.get) I;
369 val get_local_registration =
370 gen_get_registration LocalLocalesData.get ProofContext.theory_of;
372 val test_global_registration = is_some oo get_global_registration;
373 val test_local_registration = is_some oo get_local_registration;
374 fun smart_test_registration ctxt id =
376 val thy = ProofContext.theory_of ctxt;
378 test_global_registration thy id orelse test_local_registration ctxt id
382 (* add registration to theory or context, ignored if subsumed *)
384 fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
387 val thy = thy_of thy_ctxt;
388 val reg = the_default Registrations.empty (Symtab.lookup regs name);
389 val (reg', sups) = Registrations.insert thy (ps, attn) reg;
390 val _ = if not (null sups) then warning
391 ("Subsumed interpretation(s) of locale " ^
392 quote (extern thy name) ^
393 "\nby interpretation(s) with the following prefix(es):\n" ^
394 commas_quote (map (fn (_, ((s, _), _)) => s) sups))
396 in Symtab.update (name, reg') regs end) thy_ctxt;
398 val put_global_registration =
399 gen_put_registration (fn f =>
400 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
401 val put_local_registration =
402 gen_put_registration LocalLocalesData.map ProofContext.theory_of;
404 fun put_registration_in_locale name id =
405 change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
406 (axiom, import, elems, params, lparams, term_syntax, regs @ [(id, [])], intros));
409 (* add witness theorem to registration in theory or context,
410 ignored if registration not present *)
412 fun add_witness (name, ps) thm =
413 Symtab.map_entry name (Registrations.add_witness ps thm);
415 fun add_global_witness id thm =
416 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
418 val add_local_witness = LocalLocalesData.map oo add_witness;
420 fun add_witness_in_locale name id thm =
421 change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
423 fun add (id', thms) =
424 if id = id' then (id', thm :: thms) else (id', thms);
425 in (axiom, import, elems, params, lparams, term_syntax, map add regs, intros) end);
428 (* printing of registrations *)
430 fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
432 val ctxt = mk_ctxt thy_ctxt;
433 val thy = ProofContext.theory_of ctxt;
435 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
437 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
438 fun prt_attn (prfx, atts) =
439 Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
440 fun prt_witns witns = Pretty.enclose "[" "]"
441 (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
442 fun prt_reg (ts, (("", []), witns)) =
444 then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
446 | prt_reg (ts, (attn, witns)) =
448 then Pretty.block ((prt_attn attn @
449 [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
451 else Pretty.block ((prt_attn attn @
452 [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
454 val loc_int = intern thy loc;
455 val regs = get_regs thy_ctxt;
456 val loc_regs = Symtab.lookup regs loc_int;
459 NONE => Pretty.str ("no interpretations in " ^ msg)
461 val r' = Registrations.dest thy r;
462 val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
463 in Pretty.big_list ("interpretations in " ^ msg ^ ":")
469 val print_global_registrations =
470 gen_print_registrations (#3 o GlobalLocalesData.get)
471 ProofContext.init "theory";
472 val print_local_registrations' =
473 gen_print_registrations LocalLocalesData.get
475 fun print_local_registrations show_wits loc ctxt =
476 (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
477 print_local_registrations' show_wits loc ctxt);
482 fun err_in_locale ctxt msg ids =
484 val thy = ProofContext.theory_of ctxt;
485 fun prt_id (name, parms) =
486 [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
487 val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
489 if forall (equal "" o #1) ids then msg
490 else msg ^ "\n" ^ Pretty.string_of (Pretty.block
491 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
492 in error err_msg end;
494 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
497 fun pretty_ren NONE = Pretty.str "_"
498 | pretty_ren (SOME (x, NONE)) = Pretty.str x
499 | pretty_ren (SOME (x, SOME syn)) =
500 Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
502 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
503 | pretty_expr thy (Rename (expr, xs)) =
504 Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
505 | pretty_expr thy (Merge es) =
506 Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
508 fun err_in_expr _ msg (Merge []) = error msg
509 | err_in_expr ctxt msg expr =
510 error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
511 [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
512 pretty_expr (ProofContext.theory_of ctxt) expr]));
515 (** structured contexts: rename + merge + implicit type instantiation **)
517 (* parameter types *)
519 fun frozen_tvars ctxt Ts =
520 #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
521 |> map (fn ((xi, S), T) => (xi, (S, T)));
523 fun unify_frozen ctxt maxidx Ts Us =
525 fun paramify NONE i = (NONE, i)
526 | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
528 val (Ts', maxidx') = fold_map paramify Ts maxidx;
529 val (Us', maxidx'') = fold_map paramify Us maxidx';
530 val thy = ProofContext.theory_of ctxt;
532 fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
533 handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
535 val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
536 val Vs = map (Option.map (Envir.norm_type unifier)) Us';
537 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
538 in map (Option.map (Envir.norm_type unifier')) Vs end;
540 fun params_of elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
541 fun params_of' elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
544 (* CB: param_types has the following type:
545 ('a * 'b option) list -> ('a * 'b) list *)
546 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
549 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
550 handle Symtab.DUPS xs => err_in_locale ctxt
551 ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
554 (* Distinction of assumed vs. derived identifiers.
555 The former may have axioms relating assumptions of the context to
556 assumptions of the specification fragment (for locales with
557 predicates). The latter have witnesses relating assumptions of the
558 specification fragment to assumptions of other (assumed) specification
561 datatype 'a mode = Assumed of 'a | Derived of 'a;
563 fun map_mode f (Assumed x) = Assumed (f x)
564 | map_mode f (Derived x) = Derived (f x);
567 (* flatten expressions *)
571 fun unify_parms ctxt fixed_parms raw_parmss =
573 val thy = ProofContext.theory_of ctxt;
574 val maxidx = length raw_parmss;
575 val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
577 fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
578 fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
579 val parms = fixed_parms @ maps varify_parms idx_parmss;
581 fun unify T U envir = Sign.typ_unify thy (U, T) envir
582 handle Type.TUNIFY =>
583 let val prt = Sign.string_of_typ thy in
584 raise TYPE ("unify_parms: failed to unify types " ^
585 prt U ^ " and " ^ prt T, [U, T], [])
587 fun unify_list (T :: Us) = fold (unify T) Us
589 val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
590 (Vartab.empty, maxidx);
592 val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
593 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
595 fun inst_parms (i, ps) =
596 foldr Term.add_typ_tfrees [] (map_filter snd ps)
597 |> map_filter (fn (a, S) =>
598 let val T = Envir.norm_type unifier' (TVar ((a, i), S))
599 in if T = TFree (a, S) then NONE else SOME (a, T) end)
601 in map inst_parms idx_parmss end;
605 fun unify_elemss _ _ [] = []
606 | unify_elemss _ [] [elems] = [elems]
607 | unify_elemss ctxt fixed_parms elemss =
609 val thy = ProofContext.theory_of ctxt;
610 val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
611 fun inst ((((name, ps), mode), elems), env) =
612 (((name, map (apsnd (Option.map (Element.instT_type env))) ps),
613 map_mode (map (Element.instT_witness thy env)) mode),
614 map (Element.instT_ctxt thy env) elems);
615 in map inst (elemss ~~ envs) end;
618 fun renaming xs parms = zip_options parms xs
619 handle Library.UnequalLengths =>
620 error ("Too many arguments in renaming: " ^
621 commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
625 Compute parameters (with types and syntax) of locale expression.
628 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
630 val thy = ProofContext.theory_of ctxt;
632 fun merge_tenvs fixed tenv1 tenv2 =
634 val [env1, env2] = unify_parms ctxt fixed
635 [tenv1 |> Symtab.dest |> map (apsnd SOME),
636 tenv2 |> Symtab.dest |> map (apsnd SOME)]
638 Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
639 Symtab.map (Element.instT_type env2) tenv2)
642 fun merge_syn expr syn1 syn2 =
643 Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
644 handle Symtab.DUPS xs => err_in_expr ctxt
645 ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
647 fun params_of (expr as Locale name) =
649 val {import, params, ...} = the_locale thy name;
650 val parms = map (fst o fst) params;
651 val (parms', types', syn') = params_of import;
652 val all_parms = merge_lists parms' parms;
653 val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
654 val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
655 in (all_parms, all_types, all_syn) end
656 | params_of (expr as Rename (e, xs)) =
658 val (parms', types', syn') = params_of e;
659 val ren = renaming xs parms';
660 (* renaming may reduce number of parameters *)
661 val new_parms = map (Element.rename ren) parms' |> distinct (op =);
662 val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
663 val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
664 handle Symtab.DUP x =>
665 err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
666 val syn_types = map (apsnd (fn mx => SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))))) (Symtab.dest new_syn);
667 val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
668 val (env :: _) = unify_parms ctxt []
669 ((ren_types |> map (apsnd SOME)) :: map single syn_types);
670 val new_types = fold (Symtab.insert (op =))
671 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
672 in (new_parms, new_types, new_syn) end
673 | params_of (Merge es) =
674 fold (fn e => fn (parms, types, syn) =>
676 val (parms', types', syn') = params_of e
678 (merge_lists parms parms', merge_tenvs [] types types',
679 merge_syn e syn syn')
681 es ([], Symtab.empty, Symtab.empty)
683 val (parms, types, syn) = params_of expr;
685 (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
686 merge_syn expr prev_syn syn)
689 fun make_params_ids params = [(("", params), ([], Assumed []))];
690 fun make_raw_params_elemss (params, tenv, syn) =
691 [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
692 Int [Fixes (map (fn p =>
693 (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
697 Extend list of identifiers by those new in locale expression expr.
698 Compute corresponding list of lists of locale elements (one entry per
701 Identifiers represent locale fragments and are in an extended form:
702 ((name, ps), (ax_ps, axs))
703 (name, ps) is the locale name with all its parameters.
704 (ax_ps, axs) is the locale axioms with its parameters;
705 axs are always taken from the top level of the locale hierarchy,
706 hence axioms may contain additional parameters from later fragments:
707 ps subset of ax_ps. axs is either singleton or empty.
709 Elements are enriched by identifier-like information:
710 (((name, ax_ps), axs), elems)
711 The parameters in ax_ps are the axiom parameters, but enriched by type
712 info: now each entry is a pair of string and typ option. Axioms are
717 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
719 val thy = ProofContext.theory_of ctxt;
721 fun rename_parms top ren ((name, ps), (parms, mode)) =
722 ((name, map (Element.rename ren) ps),
724 then (map (Element.rename ren) parms,
725 map_mode (map (Element.rename_witness ren)) mode)
728 (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
730 fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
731 if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
732 then (wits, ids, visited)
735 val {params, regs, ...} = the_locale thy name;
736 val pTs' = map #1 params;
737 val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
738 (* dummy syntax, since required by rename *)
739 val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
740 val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
741 (* propagate parameter types, to keep them consistent *)
742 val regs' = map (fn ((name, ps), wits) =>
743 ((name, map (Element.rename ren) ps),
744 map (Element.transfer_witness thy) wits)) regs;
745 val new_regs = regs';
746 val new_ids = map fst new_regs;
747 val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
749 val new_wits = new_regs |> map (#2 #> map
750 (Element.instT_witness thy env #> Element.rename_witness ren #>
751 Element.satisfy_witness wits));
752 val new_ids' = map (fn (id, wits) =>
753 (id, ([], Derived wits))) (new_ids ~~ new_wits);
754 val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
755 ((n, pTs), mode)) (new_idTs ~~ new_ids');
756 val new_id = ((name, map #1 pTs), ([], mode));
757 val (wits', ids', visited') = fold add_with_regs new_idTs'
758 (wits @ flat new_wits, ids, visited @ [new_id]);
760 (wits', ids' @ [new_id], visited')
763 (* distribute top-level axioms over assumed ids *)
765 fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
767 val {elems, ...} = the_locale thy name;
769 (fn (Assumes asms, _) => maps (map #1 o #2) asms
772 val (axs1, axs2) = chop (length ts) axioms;
773 in (((name, parms), (all_ps, Assumed axs1)), axs2) end
774 | axiomify all_ps (id, (_, Derived ths)) axioms =
775 ((id, (all_ps, Derived ths)), axioms);
777 (* identifiers of an expression *)
779 fun identify top (Locale name) =
780 (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
781 where name is a locale name, ps a list of parameter names and axs
782 a list of axioms relating to the identifier, axs is empty unless
783 identify at top level (top = true);
784 parms is accumulated list of parameters *)
786 val {axiom, import, params, ...} = the_locale thy name;
787 val ps = map (#1 o #1) params;
788 val (ids', parms') = identify false import;
789 (* acyclic import dependencies *)
791 val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
792 val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
793 in (ids_ax, merge_lists parms' ps) end
794 | identify top (Rename (e, xs)) =
796 val (ids', parms') = identify top e;
797 val ren = renaming xs parms'
798 handle ERROR msg => err_in_locale' ctxt msg ids';
800 val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
801 val parms'' = distinct (op =) (maps (#2 o #1) ids'');
802 in (ids'', parms'') end
803 | identify top (Merge es) =
804 fold (fn e => fn (ids, parms) =>
806 val (ids', parms') = identify top e
808 (merge_alists ids ids', merge_lists parms parms')
812 fun inst_wit all_params (t, th) = let
813 val {hyps, prop, ...} = Thm.rep_thm th;
814 val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
815 val [env] = unify_parms ctxt all_params [ps];
816 val t' = Element.instT_term env t;
817 val th' = Element.instT_thm thy env th;
820 fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
822 val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
823 val elems = map fst elems_stamped;
824 val ps = map fst ps_mx;
825 fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
826 val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
827 val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
828 val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
829 val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
831 |> map (Element.rename_ctxt ren)
832 |> map (Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I,
833 name = NameSpace.qualified (space_implode "_" params)})
834 |> map (Element.instT_ctxt thy env)
835 in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
837 (* parameters, their types and syntax *)
838 val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
839 val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
840 (* compute identifiers and syntax, merge with previous ones *)
841 val (ids, _) = identify true expr;
842 val idents = subtract (eq_fst (op =)) prev_idents ids;
843 val syntax = merge_syntax ctxt ids (syn, prev_syntax);
844 (* type-instantiate elements *)
845 val final_elemss = map (eval all_params tenv syntax) idents;
846 in ((prev_idents @ idents, syntax), final_elemss) end;
851 (* activate elements *)
855 fun axioms_export axs _ hyps =
856 Element.satisfy_thm axs
857 #> Drule.implies_intr_list (Library.drop (length axs, hyps));
860 (* NB: derived ids contain only facts at this stage *)
862 fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
863 ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
864 | activate_elem _ _ ((ctxt, mode), Constrains _) =
866 | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
868 val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
869 val ts = maps (map #1 o #2) asms';
870 val (ps, qs) = chop (length ts) axs;
872 ctxt |> fold Variable.fix_frees ts
873 |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
874 in ((ctxt', Assumed qs), []) end
875 | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
876 ((ctxt, Derived ths), [])
877 | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
879 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
880 val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
881 let val ((c, _), t') = LocalDefs.cert_def ctxt t
882 in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
884 ctxt |> fold (Variable.fix_frees o #1) asms
885 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
886 in ((ctxt', Assumed axs), []) end
887 | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
888 ((ctxt, Derived ths), [])
889 | activate_elem _ is_ext ((ctxt, mode), Notes facts) =
891 val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
892 val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
893 in ((ctxt', mode), if is_ext then res else []) end;
895 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
897 val thy = ProofContext.theory_of ctxt;
898 val ((ctxt', _), res) =
899 foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
900 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
901 val ctxt'' = if name = "" then ctxt'
903 val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
904 val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
907 fold (add_local_witness (name, ps') o
908 Element.assume_witness thy o Element.witness_prop) axs ctxt''
909 | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
911 in (ProofContext.restore_naming ctxt ctxt'', res) end;
913 fun activate_elemss ax_in_ctxt prep_facts =
914 fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
916 val elems = map (prep_facts ctxt) raw_elems;
917 val (ctxt', res) = apsnd flat
918 (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
919 val elems' = elems |> map (Element.map_ctxt
920 {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure});
921 in (((((name, ps), mode), elems'), res), ctxt') end);
925 (* CB: activate_facts prep_facts (ctxt, elemss),
926 where elemss is a list of pairs consisting of identifiers and
927 context elements, extends ctxt by the context elements yielding
928 ctxt' and returns (ctxt', (elemss', facts)).
929 Identifiers in the argument are of the form ((name, ps), axs) and
930 assumptions use the axioms in the identifiers to set up exporters
931 in ctxt'. elemss' does not contain identifiers and is obtained
932 from elemss and the intermediate context with prep_facts.
933 If read_facts or cert_facts is used for prep_facts, these also remove
934 the internal/external markers from elemss. *)
936 fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
937 let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
938 in (ctxt', (elemss, flat factss)) end;
944 (** prepare locale elements **)
948 fun intern_expr thy (Locale xname) = Locale (intern thy xname)
949 | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
950 | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
953 (* propositions and bindings *)
955 (* flatten (ctxt, prep_expr) ((ids, syn), expr)
956 normalises expr (which is either a locale
957 expression or a single context element) wrt.
958 to the list ids of already accumulated identifiers.
959 It returns ((ids', syn'), elemss) where ids' is an extension of ids
960 with identifiers generated for expr, and elemss is the list of
961 context elements generated from expr.
962 syn and syn' are symtabs mapping parameter names to their syntax. syn'
963 is an extension of syn.
964 For details, see flatten_expr.
966 Additionally, for a locale expression, the elems are grouped into a single
967 Int; individual context elements are marked Ext. In this case, the
968 identifier-like information of the element is as follows:
969 - for Fixes: (("", ps), []) where the ps have type info NONE
970 - for other elements: (("", []), []).
971 The implementation of activate_facts relies on identifier names being
972 empty strings for external elements.
975 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
976 val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
979 merge_syntax ctxt ids'
980 (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
981 handle Symtab.DUPS xs => err_in_locale ctxt
982 ("Conflicting syntax for parameters: " ^ commas_quote xs)
984 [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
986 | flatten _ ((ids, syn), Elem elem) =
987 ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
988 | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
989 apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
995 fun declare_int_elem (ctxt, Fixes fixes) =
996 (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
997 (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
998 | declare_int_elem (ctxt, _) = (ctxt, []);
1000 fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
1001 let val (vars, _) = prep_vars fixes ctxt
1002 in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
1003 | declare_ext_elem prep_vars (ctxt, Constrains csts) =
1004 let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
1006 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
1007 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
1008 | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
1010 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
1011 let val (ctxt', propps) =
1013 Int es => foldl_map declare_int_elem (ctxt, es)
1014 | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
1015 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
1016 in (ctxt', propps) end
1017 | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
1021 fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
1023 (* CB: fix of type bug of goal in target with context elements.
1024 Parameters new in context elements must receive types that are
1025 distinct from types of parameters in target (fixed_params). *)
1026 val ctxt_with_fixed =
1027 fold Variable.declare_term (map Free fixed_params) ctxt;
1030 |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
1031 |> unify_elemss ctxt_with_fixed fixed_params;
1032 val (_, raw_elemss') =
1033 foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
1034 (int_elemss, raw_elemss);
1035 in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
1041 val norm_term = Envir.beta_norm oo Term.subst_atomic;
1043 fun abstract_thm thy eq =
1044 Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
1046 fun bind_def ctxt (name, ps) eq (xs, env, ths) =
1048 val ((y, T), b) = LocalDefs.abs_def eq;
1049 val b' = norm_term env b;
1050 val th = abstract_thm (ProofContext.theory_of ctxt) eq;
1051 fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
1053 conditional (exists (equal y o #1) xs) (fn () =>
1054 err "Attempt to define previously specified variable");
1055 conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
1056 err "Attempt to redefine variable");
1057 (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
1061 (* CB: for finish_elems (Int and Ext),
1062 extracts specification, only of assumed elements *)
1064 fun eval_text _ _ _ (Fixes _) text = text
1065 | eval_text _ _ _ (Constrains _) text = text
1066 | eval_text _ (_, Assumed _) is_ext (Assumes asms)
1067 (((exts, exts'), (ints, ints')), (xs, env, defs)) =
1069 val ts = maps (map #1 o #2) asms;
1070 val ts' = map (norm_term env) ts;
1072 if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
1073 else ((exts, exts'), (ints @ ts, ints' @ ts'));
1074 in (spec', (fold Term.add_frees ts' xs, env, defs)) end
1075 | eval_text _ (_, Derived _) _ (Assumes _) text = text
1076 | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
1077 (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
1078 | eval_text _ (_, Derived _) _ (Defines _) text = text
1079 | eval_text _ _ _ (Notes _) text = text;
1082 (* for finish_elems (Int),
1083 remove redundant elements of derived identifiers,
1084 turn assumptions and definitions into facts,
1085 adjust hypotheses of facts using witnesses *)
1087 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
1088 | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
1089 | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
1090 | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
1092 | finish_derived _ _ (Derived _) (Fixes _) = NONE
1093 | finish_derived _ _ (Derived _) (Constrains _) = NONE
1094 | finish_derived sign wits (Derived _) (Assumes asms) = asms
1095 |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
1096 |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
1097 | finish_derived sign wits (Derived _) (Defines defs) = defs
1098 |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
1099 |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
1101 | finish_derived _ wits _ (Notes facts) = (Notes facts)
1102 |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;
1104 (* CB: for finish_elems (Ext) *)
1106 fun closeup _ false elem = elem
1107 | closeup ctxt true elem =
1110 let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
1111 in Term.list_all_free (frees, t) end;
1113 fun no_binds [] = []
1114 | no_binds _ = error "Illegal term bindings in locale element";
1117 Assumes asms => Assumes (asms |> map (fn (a, propps) =>
1118 (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
1119 | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
1120 (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
1125 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
1126 (x, AList.lookup (op =) parms x, mx)) fixes)
1127 | finish_ext_elem parms _ (Constrains _, _) = Constrains []
1128 | finish_ext_elem _ close (Assumes asms, propp) =
1129 close (Assumes (map #1 asms ~~ propp))
1130 | finish_ext_elem _ close (Defines defs, propp) =
1131 close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
1132 | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
1135 (* CB: finish_parms introduces type info from parms to identifiers *)
1136 (* CB: only needed for types that have been NONE so far???
1137 If so, which are these??? *)
1139 fun finish_parms parms (((name, ps), mode), elems) =
1140 (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
1142 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
1144 val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
1145 val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
1146 val text' = fold (eval_text ctxt id' false) es text;
1147 val es' = map_filter
1148 (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
1149 in ((text', wits'), (id', map Int es')) end
1150 | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
1152 val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
1153 val text' = eval_text ctxt id true e' text;
1154 in ((text', wits), (id, [Ext e'])) end
1158 (* CB: only called by prep_elemss *)
1160 fun finish_elemss ctxt parms do_close =
1161 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
1166 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
1168 fun defs_ord (defs1, defs2) =
1169 list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
1170 Term.fast_term_ord (d1, d2)) (defs1, defs2);
1172 TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
1173 val ord = defs_ord);
1175 fun rem_dup_defs es ds =
1176 fold_map (fn e as (Defines defs) => (fn ds =>
1177 if Defstab.defined ds defs
1178 then (Defines [], ds)
1179 else (e, Defstab.update (defs, ()) ds))
1180 | e => (fn ds => (e, ds))) es ds;
1181 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
1182 | rem_dup_elemss (Ext e) ds = (Ext e, ds);
1183 fun rem_dup_defines raw_elemss =
1184 fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
1185 apfst (pair id) (rem_dup_elemss es ds))
1186 | (id as (_, (Derived _)), es) => (fn ds =>
1187 ((id, es), ds))) raw_elemss Defstab.empty |> #1;
1189 (* CB: type inference and consistency checks for locales.
1191 Works by building a context (through declare_elemss), extracting the
1192 required information and adjusting the context elements (finish_elemss).
1193 Can also universally close free vars in assms and defs. This is only
1194 needed for Ext elements and controlled by parameter do_close.
1196 Only elements of assumed identifiers are considered.
1199 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
1201 (* CB: contexts computed in the course of this function are discarded.
1202 They are used for type inference and consistency checks only. *)
1203 (* CB: fixed_params are the parameters (with types) of the target locale,
1204 empty list if there is no target. *)
1205 (* CB: raw_elemss are list of pairs consisting of identifiers and
1206 context elements, the latter marked as internal or external. *)
1207 val raw_elemss = rem_dup_defines raw_elemss;
1208 val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
1209 (* CB: raw_ctxt is context with additional fixed variables derived from
1210 the fixes elements in raw_elemss,
1211 raw_proppss contains assumptions and definitions from the
1212 external elements in raw_elemss. *)
1213 fun prep_prop raw_propp (raw_ctxt, raw_concl) =
1215 (* CB: add type information from fixed_params to context (declare_term) *)
1216 (* CB: process patterns (conclusion and external elements only) *)
1217 val (ctxt, all_propp) =
1218 prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
1219 (* CB: add type information from conclusion and external elements to context *)
1220 val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
1221 (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
1222 val all_propp' = map2 (curry (op ~~))
1223 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
1224 val (concl, propp) = chop (length raw_concl) all_propp';
1225 in (propp, (ctxt, concl)) end
1227 val (proppss, (ctxt, concl)) =
1228 (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
1230 (* CB: obtain all parameters from identifier part of raw_elemss *)
1231 val xs = map #1 (params_of' raw_elemss);
1232 val typing = unify_frozen ctxt 0
1233 (map (Variable.default_type raw_ctxt) xs)
1234 (map (Variable.default_type ctxt) xs);
1235 val parms = param_types (xs ~~ typing);
1236 (* CB: parms are the parameters from raw_elemss, with correct typing. *)
1238 (* CB: extract information from assumes and defines elements
1239 (fixes, constrains and notes in raw_elemss don't have an effect on
1240 text and elemss), compute final form of context elements. *)
1241 val ((text, _), elemss) = finish_elemss ctxt parms do_close
1242 ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
1243 (* CB: text has the following structure:
1244 (((exts, exts'), (ints, ints')), (xs, env, defs))
1246 exts: external assumptions (terms in external assumes elements)
1247 exts': dito, normalised wrt. env
1248 ints: internal assumptions (terms in internal assumes elements)
1249 ints': dito, normalised wrt. env
1250 xs: the free variables in exts' and ints' and rhss of definitions,
1251 this includes parameters except defined parameters
1252 env: list of term pairs encoding substitutions, where the first term
1253 is a free variable; substitutions represent defines elements and
1254 the rhs is normalised wrt. the previous env
1255 defs: theorems representing the substitutions from defines elements
1256 (thms are normalised wrt. env).
1257 elemss is an updated version of raw_elemss:
1258 - type info added to Fixes and modified in Constrains
1259 - axiom and definition statement replaced by corresponding one
1260 from proppss in Assumes and Defines
1263 in ((parms, elemss, concl), text) end;
1267 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
1268 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
1273 (* facts and attributes *)
1277 fun check_name name =
1278 if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
1281 fun prep_facts _ _ _ ctxt (Int elem) =
1282 Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
1283 | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
1284 {var = I, typ = I, term = I,
1287 attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
1291 fun read_facts x = prep_facts check_name ProofContext.get_thms Attrib.intern_src x;
1292 fun cert_facts x = prep_facts I (K I) (K I) x;
1297 (* Get the specification of a locale *)
1299 (*The global specification is made from the parameters and global
1300 assumptions, the local specification from the parameters and the
1301 local assumptions.*)
1305 fun gen_asms_of get thy name =
1307 val ctxt = ProofContext.init thy;
1308 val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
1309 val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
1312 |> maps (fn (_, es) => map (fn Int e => e) es)
1313 |> maps (fn Assumes asms => asms | _ => [])
1314 |> map (apsnd (map fst))
1319 fun parameters_of thy name =
1320 the_locale thy name |> #params;
1322 fun parameters_of_expr thy expr =
1324 val ctxt = ProofContext.init thy;
1325 val pts = params_of_expr ctxt [] (intern_expr thy expr)
1326 ([], Symtab.empty, Symtab.empty);
1327 val raw_params_elemss = make_raw_params_elemss pts;
1328 val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
1329 (([], Symtab.empty), Expr expr);
1330 val ((parms, _, _), _) =
1331 read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
1332 in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
1334 fun local_asms_of thy name =
1335 gen_asms_of (single o Library.last_elem) thy name;
1337 fun global_asms_of thy name =
1338 gen_asms_of I thy name;
1343 (* full context statements: import + elements + conclusion *)
1347 fun prep_context_statement prep_expr prep_elemss prep_facts
1348 do_close fixed_params import elements raw_concl context =
1350 val thy = ProofContext.theory_of context;
1352 val (import_params, import_tenv, import_syn) =
1353 params_of_expr context fixed_params (prep_expr thy import)
1354 ([], Symtab.empty, Symtab.empty);
1355 val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
1356 val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
1357 (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
1359 val ((import_ids, _), raw_import_elemss) =
1360 flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
1361 (* CB: normalise "includes" among elements *)
1362 val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
1363 ((import_ids, incl_syn), elements);
1365 val raw_elemss = flat raw_elemsss;
1366 (* CB: raw_import_elemss @ raw_elemss is the normalised list of
1367 context elements obtained from import and elements. *)
1368 (* Now additional elements for parameters are inserted. *)
1369 val import_params_ids = make_params_ids import_params;
1370 val incl_params_ids =
1371 make_params_ids (incl_params \\ import_params);
1372 val raw_import_params_elemss =
1373 make_raw_params_elemss (import_params, incl_tenv, incl_syn);
1374 val raw_incl_params_elemss =
1375 make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
1376 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
1377 context fixed_params
1378 (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
1380 (* replace extended ids (for axioms) by ids *)
1381 val (import_ids', incl_ids) = chop (length import_ids) ids;
1382 val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
1383 val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
1384 (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
1385 (all_ids ~~ all_elemss);
1386 (* CB: all_elemss and parms contain the correct parameter types *)
1388 val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
1389 val (import_ctxt, (import_elemss, _)) =
1390 activate_facts false prep_facts (context, ps);
1392 val (ctxt, (elemss, _)) =
1393 activate_facts false prep_facts (import_ctxt, qs);
1395 ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
1396 (parms, spec, defs)), concl)
1399 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
1401 val thy = ProofContext.theory_of ctxt;
1402 val locale = Option.map (prep_locale thy) raw_locale;
1403 val (fixed_params, import) =
1407 let val {params = ps, ...} = the_locale thy name
1408 in (map fst ps, Locale name) end);
1409 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
1410 prep_ctxt false fixed_params import elems concl ctxt;
1411 in (locale, locale_ctxt, elems_ctxt, concl') end;
1413 fun prep_expr prep import body ctxt =
1415 val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt;
1416 val all_elems = maps snd (import_elemss @ elemss);
1417 in (all_elems, ctxt') end;
1421 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
1422 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
1424 fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt);
1425 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
1427 val read_expr = prep_expr read_context;
1428 val cert_expr = prep_expr cert_context;
1430 fun read_context_statement loc = prep_statement intern read_ctxt loc;
1431 fun read_context_statement_i loc = prep_statement (K I) read_ctxt loc;
1432 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
1439 fun print_locale thy show_facts import body =
1440 let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in
1441 Pretty.big_list "locale elements:" (all_elems
1442 |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
1443 |> map (Pretty.chunks o Element.pretty_ctxt ctxt))
1449 (** store results **)
1451 (* naming of interpreted theorems *)
1453 fun global_note_prefix_i kind prfx args thy =
1455 |> Theory.qualified_names
1456 |> Theory.sticky_prefix prfx
1457 |> PureThy.note_thmss_i kind args
1458 ||> Theory.restore_naming thy;
1460 fun local_note_prefix_i prfx args ctxt =
1462 |> ProofContext.qualified_names
1463 |> ProofContext.sticky_prefix prfx
1464 |> ProofContext.note_thmss_i args
1465 ||> ProofContext.restore_naming ctxt;
1468 (* collect witnesses for global registration;
1469 requires parameters and flattened list of (assumed!) identifiers
1470 instead of recomputing it from the target *)
1472 fun collect_global_witnesses thy parms ids vts = let
1473 val ts = map Logic.unvarify vts;
1474 val (parms, parmTs) = split_list parms;
1475 val parmvTs = map Logic.varifyT parmTs;
1476 val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
1477 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
1479 (* replace parameter names in ids by instantiations *)
1480 val vinst = Symtab.make (parms ~~ vts);
1481 fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
1482 val inst = Symtab.make (parms ~~ ts);
1483 val ids' = map (apsnd vinst_names) ids;
1484 val wits = maps (snd o the o get_global_registration thy) ids';
1485 in ((tinst, inst), wits) end;
1488 (* store instantiations of args for all registered interpretations
1491 fun note_thmss_registrations kind target args thy =
1493 val parms = the_locale thy target |> #params |> map fst;
1494 val ids = flatten (ProofContext.init thy, intern_expr thy)
1495 (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
1496 |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
1498 val regs = get_global_registrations thy target;
1500 (* add args to thy for all registrations *)
1502 fun activate (vts, ((prfx, atts2), _)) thy =
1504 val (insts, prems) = collect_global_witnesses thy parms ids vts;
1505 val attrib = Attrib.attribute_i thy;
1507 Args.map_values I (Element.instT_type (#1 insts))
1508 (Element.inst_term insts) (Element.inst_thm thy insts);
1510 Drule.standard o Element.satisfy_thm prems o Element.inst_thm thy insts;
1511 val args' = args |> map (fn ((name, atts), bs) =>
1512 ((name, map (attrib o inst_atts) atts),
1513 bs |> map (fn (ths, more_atts) =>
1514 (map inst_thm ths, map attrib (map inst_atts more_atts @ atts2)))));
1515 in global_note_prefix_i kind prfx args' thy |> snd end;
1516 in fold activate regs thy end;
1521 fun add_term_syntax loc syn =
1522 syn #> ProofContext.theory (change_locale loc
1523 (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
1524 (axiom, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs, intros)));
1526 fun init_term_syntax loc ctxt =
1527 fold_rev (fn (f, _) => fn ctxt' => f ctxt')
1528 (#term_syntax (the_locale (ProofContext.theory_of ctxt) loc)) ctxt;
1532 #> init_term_syntax loc
1533 #> (#2 o cert_context_statement (SOME loc) [] []);
1536 (* locale results *)
1538 fun add_thmss kind loc args ctxt =
1540 val (ctxt', ([(_, [Notes args'])], facts)) =
1541 activate_facts true cert_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
1542 val ctxt'' = ctxt' |> ProofContext.theory
1544 (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
1545 (axiom, import, elems @ [(Notes args', stamp ())],
1546 params, lparams, term_syntax, regs, intros))
1547 #> note_thmss_registrations kind loc args');
1548 in (facts, ctxt'') end;
1550 fun locale_results kind loc args = add_thmss kind loc (map (apsnd Thm.simple_fact) args);
1554 (** define locales **)
1556 (* predicate text *)
1557 (* CB: generate locale predicates and delta predicates *)
1561 (* introN: name of theorems for introduction rules of locale and
1563 axiomsN: name of theorem set with destruct rules for locale predicates,
1564 also name suffix of delta predicates. *)
1566 val introN = "intro";
1567 val axiomsN = "axioms";
1569 fun atomize_spec thy ts =
1571 val t = Logic.mk_conjunction_list ts;
1572 val body = ObjectLogic.atomize_term thy t;
1573 val bodyT = Term.fastype_of body;
1575 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
1576 else (body, bodyT, ObjectLogic.atomize_cterm (Thm.cterm_of thy t))
1579 fun aprop_tr' n c = (c, fn args =>
1580 if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
1583 (* CB: define one predicate including its intro rule and axioms
1584 - bname: predicate name
1585 - parms: locale parameters
1586 - defs: thms representing substitutions from defines elements
1587 - ts: terms representing locale assumptions (not normalised wrt. defs)
1588 - norm_ts: terms representing locale assumptions (normalised wrt. defs)
1592 fun def_pred bname parms defs ts norm_ts thy =
1594 val name = Sign.full_name thy bname;
1596 val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
1597 val env = Term.add_term_free_names (body, []);
1598 val xs = filter (member (op =) env o #1) parms;
1600 val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
1601 |> Library.sort_wrt #1 |> map TFree;
1602 val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
1604 val args = map Logic.mk_type extraTs @ map Free xs;
1605 val head = Term.list_comb (Const (name, predT), args);
1606 val statement = ObjectLogic.ensure_propT thy head;
1608 val ([pred_def], defs_thy) =
1610 |> (if bodyT <> propT then I else
1611 Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
1612 |> Theory.add_consts_i [(bname, predT, NoSyn)]
1613 |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
1614 val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
1616 val cert = Thm.cterm_of defs_thy;
1618 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
1619 Tactic.rewrite_goals_tac [pred_def] THEN
1620 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
1621 Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
1624 (Drule.equal_elim_rule2 OF [body_eq,
1625 Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
1626 |> Conjunction.elim_precise [length ts] |> hd;
1627 val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
1628 Element.prove_witness defs_ctxt t
1629 (Tactic.rewrite_goals_tac defs THEN
1630 Tactic.compose_tac (false, ax, 0) 1));
1631 in ((statement, intro, axioms), defs_thy) end;
1633 fun assumes_to_notes (Assumes asms) axms =
1634 fold_map (fn (a, spec) => fn axs =>
1635 let val (ps, qs) = chop (length spec) axs
1636 in ((a, [(ps, [])]), qs) end) asms axms
1638 | assumes_to_notes e axms = (e, axms);
1640 (* CB: the following two change only "new" elems, these have identifier ("", _). *)
1642 (* turn Assumes into Notes elements *)
1644 fun change_assumes_elemss axioms elemss =
1646 fun change (id as ("", _), es) =
1647 fold_map assumes_to_notes
1648 (map (Element.map_ctxt_values I I (Element.satisfy_thm axioms)) es)
1649 #-> (fn es' => pair (id, es'))
1650 | change e = pair e;
1652 fst (fold_map change elemss (map Element.conclude_witness axioms))
1655 (* adjust hyps of Notes elements *)
1657 fun change_elemss_hyps axioms elemss =
1659 fun change (id as ("", _), es) =
1660 (id, map (fn e as (Notes _) => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
1663 in map change elemss end;
1667 (* CB: main predicate definition function *)
1669 fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
1671 val ((elemss', more_ts), a_elem, a_intro, thy') =
1672 if null exts then ((elemss, []), [], [], thy)
1675 val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
1676 val ((statement, intro, axioms), def_thy) =
1677 thy |> def_pred aname parms defs exts exts';
1678 val elemss' = change_assumes_elemss axioms elemss;
1679 val def_thy' = def_thy
1680 |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
1682 val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1683 in ((elemss', [statement]), a_elem, [intro], def_thy') end;
1684 val (predicate, stmt', elemss'', b_intro, thy'') =
1685 if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy')
1688 val ((statement, intro, axioms), def_thy) =
1689 thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
1690 val cstatement = Thm.cterm_of def_thy statement;
1691 val elemss'' = change_elemss_hyps axioms elemss';
1694 |> PureThy.note_thmss_qualified "" bname
1695 [((introN, []), [([intro], [])]),
1696 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
1698 val b_elem = [(("", []),
1699 [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
1700 in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], def_thy') end;
1701 in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'') end;
1706 (* add_locale(_i) *)
1710 (* turn Defines into Notes elements, accumulate definition terms *)
1712 fun defines_to_notes is_ext thy (Defines defs) defns =
1714 val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
1715 val notes = map (fn (a, (def, _)) =>
1716 (a, [([assume (cterm_of thy def)], [])])) defs
1717 in (if is_ext then SOME (Notes notes) else NONE, defns @ [Defines defs']) end
1718 | defines_to_notes _ _ e defns = (SOME e, defns);
1720 fun change_defines_elemss thy elemss defns =
1722 fun change (id as (n, _), es) defns =
1724 val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
1725 in ((id, map_filter I es'), defns') end
1726 in fold_map change elemss defns end;
1728 fun gen_add_locale prep_ctxt prep_expr
1729 do_predicate bname raw_import raw_body thy =
1731 val name = Sign.full_name thy bname;
1732 val _ = conditional (is_some (get_locale thy name)) (fn () =>
1733 error ("Duplicate definition of locale " ^ quote name));
1735 val thy_ctxt = ProofContext.init thy;
1736 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
1737 text as (parms, ((_, exts'), _), defs)) =
1738 prep_ctxt raw_import raw_body thy_ctxt;
1739 val elemss = import_elemss @ body_elemss |>
1740 map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
1741 val import = prep_expr thy raw_import;
1743 val extraTs = foldr Term.add_term_tfrees [] exts' \\
1744 foldr Term.add_typ_tfrees [] (map snd parms);
1745 val _ = if null extraTs then ()
1746 else warning ("Additional type variable(s) in locale specification " ^ quote bname);
1748 val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
1749 pred_thy), (import, regs)) =
1750 if do_predicate then
1752 val (elemss', defns) = change_defines_elemss thy elemss [];
1753 val elemss'' = elemss' @ [(("", []), defns)];
1754 val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
1755 define_preds bname text elemss'' thy;
1756 fun mk_regs elemss wits =
1757 fold_map (fn (id, elems) => fn wts => let
1758 val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
1759 SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
1760 val (wts1, wts2) = chop (length ts) wts
1761 in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
1762 val regs = mk_regs elemss''' axioms |>
1763 map_filter (fn (("", _), _) => NONE | e => SOME e);
1764 in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
1765 else ((((elemss, ([], []), []), ([], [])), thy), (import, []));
1767 fun axiomify axioms elemss =
1768 (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
1769 val ts = flat (map_filter (fn (Assumes asms) =>
1770 SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
1771 val (axs1, axs2) = chop (length ts) axs;
1772 in (axs2, ((id, Assumed axs1), elems)) end)
1774 val (ctxt, (_, facts)) = activate_facts true (K I)
1775 (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
1776 val export = singleton (ProofContext.export_standard
1777 (Assumption.add_view thy_ctxt predicate_statement ctxt) thy_ctxt);
1778 val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
1779 val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
1780 val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
1781 val axs' = map (Element.assume_witness pred_thy) stmt';
1782 val ctxt' = ctxt |> ProofContext.theory (fn pred_thy => pred_thy
1783 |> PureThy.note_thmss_qualified "" bname facts' |> snd
1784 |> declare_locale name
1788 elems = map (fn e => (e, stamp ())) elems'',
1789 params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
1790 lparams = map #1 (params_of' body_elemss),
1794 in (name, ctxt') end;
1798 val add_locale = gen_add_locale read_context intern_expr;
1799 val add_locale_i = gen_add_locale cert_context (K I);
1803 val _ = Context.add_setup
1804 (add_locale_i true "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
1805 snd #> ProofContext.theory_of #>
1806 add_locale_i true "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
1807 snd #> ProofContext.theory_of);
1812 (** Normalisation of locale statements ---
1813 discharges goals implied by interpretations **)
1817 fun locale_assm_intros thy =
1818 Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
1819 (#2 (GlobalLocalesData.get thy)) [];
1820 fun locale_base_intros thy =
1821 Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
1822 (#2 (GlobalLocalesData.get thy)) [];
1824 fun all_witnesses ctxt =
1826 val thy = ProofContext.theory_of ctxt;
1827 fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
1828 (Registrations.dest thy regs |> map (fn (_, (_, wits)) =>
1829 map Element.conclude_witness wits) |> flat) @ thms)
1831 val globals = get (#3 (GlobalLocalesData.get thy));
1832 val locals = get (LocalLocalesData.get ctxt);
1833 in globals @ locals end;
1834 (* FIXME: proper varification *)
1838 fun intro_locales_tac eager ctxt facts st =
1840 val wits = all_witnesses ctxt |> map Thm.varifyT;
1841 val thy = ProofContext.theory_of ctxt;
1842 val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
1844 (ALLGOALS (Method.insert_tac facts THEN'
1845 REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
1846 THEN Tactic.distinct_subgoals_tac) st
1849 val _ = Context.add_setup (Method.add_methods
1851 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
1852 "back-chain introduction rules of locales without unfolding predicates"),
1854 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
1855 "back-chain all introduction rules of locales")]);
1860 (** Interpretation commands **)
1864 (* extract proof obligations (assms and defs) from elements *)
1866 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
1867 | extract_asms_elems ((id, Derived _), _) = (id, []);
1870 (* activate instantiated facts in theory or context *)
1872 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
1873 attn all_elemss new_elemss propss thmss thy_ctxt =
1875 fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
1878 (* discharge hyps in attributes *)
1879 |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch)
1880 (* insert interpretation attributes *)
1881 |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
1882 (* discharge hyps *)
1883 |> map (apsnd (map (apfst (map disch))));
1884 in snd (note prfx facts' thy_ctxt) end
1885 | activate_elem _ _ _ thy_ctxt = thy_ctxt;
1887 fun activate_elems disch ((id, _), elems) thy_ctxt =
1889 val ((prfx, atts2), _) = the (get_reg thy_ctxt id)
1890 handle Option => sys_error ("Unknown registration of " ^
1891 quote (fst id) ^ " while activating facts.");
1893 fold (activate_elem disch (prfx, atts2)) elems thy_ctxt
1896 val thy_ctxt' = thy_ctxt
1897 (* add registrations *)
1898 |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
1899 (* add witnesses of Assumed elements *)
1900 |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
1902 val prems = flat (map_filter
1903 (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
1904 | ((_, Derived _), _) => NONE) all_elemss);
1905 val thy_ctxt'' = thy_ctxt'
1906 (* add witnesses of Derived elements *)
1907 |> fold (fn (id, thms) => fold (add_wit id o Element.satisfy_witness prems) thms)
1908 (map_filter (fn ((_, Assumed _), _) => NONE
1909 | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
1911 val disch' = std o Element.satisfy_thm prems; (* FIXME *)
1914 (* add facts to theory or context *)
1915 |> fold (activate_elems disch') new_elemss
1918 fun global_activate_facts_elemss x = gen_activate_facts_elemss
1919 (fn thy => fn (name, ps) =>
1920 get_global_registration thy (name, map Logic.varify ps))
1921 (global_note_prefix_i "")
1922 Attrib.attribute_i Drule.standard
1923 (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
1924 (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
1925 Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
1928 fun local_activate_facts_elemss x = gen_activate_facts_elemss
1929 get_local_registration
1931 (Attrib.attribute_i o ProofContext.theory_of) I
1932 put_local_registration
1933 add_local_witness x;
1935 fun gen_prep_registration mk_ctxt is_local read_terms test_reg activate
1936 attn expr insts thy_ctxt =
1938 val ctxt = mk_ctxt thy_ctxt;
1939 val thy = ProofContext.theory_of ctxt;
1941 val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
1942 val pts = params_of_expr ctxt' [] (intern_expr thy expr)
1943 ([], Symtab.empty, Symtab.empty);
1944 val params_ids = make_params_ids (#1 pts);
1945 val raw_params_elemss = make_raw_params_elemss pts;
1946 val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
1947 (([], Symtab.empty), Expr expr);
1948 val ((parms, all_elemss, _), (_, (_, defs, _))) =
1949 read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
1951 (** compute instantiation **)
1954 val insts = if length parms < length insts
1955 then error "More arguments than parameters in instantiation."
1956 else insts @ replicate (length parms - length insts) NONE;
1957 val (ps, pTs) = split_list parms;
1958 val pvTs = map Logic.legacy_varifyT pTs;
1960 (* instantiations given by user *)
1961 val given = map_filter (fn (_, (NONE, _)) => NONE
1962 | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
1963 val (given_ps, given_insts) = split_list given;
1964 val tvars = foldr Term.add_typ_tvars [] pvTs;
1965 val used = foldr Term.add_typ_varnames [] pvTs;
1966 fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
1967 val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
1968 val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
1969 val vars' = fold Term.add_varnames vs vars;
1970 val _ = if null vars' then ()
1971 else error ("Illegal schematic variable(s) in instantiation: " ^
1972 commas_quote (map Syntax.string_of_vname vars'));
1973 (* replace new types (which are TFrees) by ones with new names *)
1974 val new_Tnames = foldr Term.add_term_tfree_names [] vs;
1975 val new_Tnames' = Name.invent_list used "'a" (length new_Tnames);
1978 else Logic.legacy_unvarifyT o Term.map_type_tfree (fn (a, s) =>
1979 TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
1982 else Term.map_types renameT;
1984 val tinst = Symtab.make (map
1985 (fn ((x, 0), T) => (x, T |> renameT)
1986 | ((_, n), _) => sys_error "Internal error var in prep_registration") vinst);
1987 val inst = Symtab.make (given_ps ~~ map rename vs);
1989 (* defined params without user input *)
1990 val not_given = map_filter (fn (x, (NONE, T)) => SOME (x, T)
1991 | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
1992 fun add_def (p, pT) inst =
1994 val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
1995 NONE => error ("Instance missing for parameter " ^ quote p)
1996 | SOME (Free (_, T), t) => (t, T);
1997 val d = Element.inst_term (tinst, inst) t;
1998 in Symtab.update_new (p, d) inst end;
1999 val inst = fold add_def not_given inst;
2000 val insts = (tinst, inst);
2001 (* Note: insts contain no vars. *)
2004 (** compute proof obligations **)
2006 (* restore "small" ids *)
2007 val ids' = map (fn ((n, ps), (_, mode)) =>
2008 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
2010 val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
2011 (* instantiate ids and elements *)
2012 val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
2013 ((n, map (Element.inst_term insts) ps),
2014 map (fn Int e => Element.inst_ctxt thy insts e) elems)
2015 |> apfst (fn id => (id, map_mode (map (Element.inst_witness thy insts)) mode)));
2017 (* remove fragments already registered with theory or context *)
2018 val new_inst_elemss = filter (fn ((id, _), _) =>
2019 not (test_reg thy_ctxt id)) inst_elemss;
2020 val new_ids = map #1 new_inst_elemss;
2022 val propss = map extract_asms_elems new_inst_elemss;
2024 val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
2025 val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
2027 in (propss, activate attn' inst_elemss new_inst_elemss propss) end;
2029 val prep_global_registration = gen_prep_registration
2030 ProofContext.init false
2031 (fn thy => fn sorts => fn used =>
2032 Sign.read_def_terms (thy, K NONE, sorts) used true)
2033 (fn thy => fn (name, ps) =>
2034 test_global_registration thy (name, map Logic.varify ps))
2035 global_activate_facts_elemss;
2037 val prep_local_registration = gen_prep_registration
2039 (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
2040 smart_test_registration
2041 local_activate_facts_elemss;
2043 fun prep_registration_in_locale target expr thy =
2044 (* target already in internal form *)
2046 val ctxt = ProofContext.init thy;
2047 val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
2048 (([], Symtab.empty), Expr (Locale target));
2049 val fixed = the_locale thy target |> #params |> map #1;
2050 val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
2051 ((raw_target_ids, target_syn), Expr expr);
2052 val (target_ids, ids) = chop (length raw_target_ids) all_ids;
2053 val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
2055 (** compute proof obligations **)
2057 (* restore "small" ids, with mode *)
2058 val ids' = map (apsnd snd) ids;
2059 (* remove Int markers *)
2060 val elemss' = map (fn (_, es) =>
2061 map (fn Int e => e) es) elemss
2062 (* extract assumptions and defs *)
2063 val ids_elemss = ids' ~~ elemss';
2064 val propss = map extract_asms_elems ids_elemss;
2066 (** activation function:
2067 - add registrations to the target locale
2068 - add induced registrations for all global registrations of
2069 the target, unless already present
2070 - add facts of induced registrations to theory **)
2072 val t_ids = map_filter
2073 (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
2075 fun activate thmss thy = let
2076 val satisfy = Element.satisfy_thm (flat thmss);
2077 val ids_elemss_thmss = ids_elemss ~~ thmss;
2078 val regs = get_global_registrations thy target;
2080 fun activate_id (((id, Assumed _), _), thms) thy =
2081 thy |> put_registration_in_locale target id
2082 |> fold (add_witness_in_locale target id) thms
2083 | activate_id _ thy = thy;
2085 fun activate_reg (vts, ((prfx, atts2), _)) thy = let
2086 val (insts, wits) = collect_global_witnesses thy fixed t_ids vts;
2087 fun inst_parms ps = map
2088 (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
2089 val disch = Element.satisfy_thm wits;
2090 val new_elemss = filter (fn (((name, ps), _), _) =>
2091 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
2092 fun activate_assumed_id (((_, Derived _), _), _) thy = thy
2093 | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
2094 val ps' = inst_parms ps;
2096 if test_global_registration thy (name, ps')
2099 |> put_global_registration (name, ps') (prfx, atts2)
2100 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2101 (Element.inst_witness thy insts witn) thy) thms
2104 fun activate_derived_id ((_, Assumed _), _) thy = thy
2105 | activate_derived_id (((name, ps), Derived ths), _) thy = let
2106 val ps' = inst_parms ps;
2108 if test_global_registration thy (name, ps')
2111 |> put_global_registration (name, ps') (prfx, atts2)
2112 |> fold (fn witn => fn thy => add_global_witness (name, ps')
2113 (witn |> Element.map_witness (fn (t, th) => (* FIXME *)
2114 (Element.inst_term insts t,
2115 disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
2118 fun activate_elem (Notes facts) thy =
2121 |> Attrib.map_facts (Attrib.attribute_i thy o
2122 Args.map_values I (Element.instT_type (#1 insts))
2123 (Element.inst_term insts)
2124 (disch o Element.inst_thm thy insts o satisfy))
2125 |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
2126 |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
2129 |> global_note_prefix_i "" prfx facts'
2132 | activate_elem _ thy = thy;
2134 fun activate_elems (_, elems) thy = fold activate_elem elems thy;
2136 in thy |> fold activate_assumed_id ids_elemss_thmss
2137 |> fold activate_derived_id ids_elemss
2138 |> fold activate_elems new_elemss end;
2140 thy |> fold activate_id ids_elemss_thmss
2141 |> fold activate_reg regs
2144 in (propss, activate) end;
2146 fun prep_propp propss = propss |> map (fn (_, props) =>
2147 (("", []), map (rpair [] o Element.mark_witness) props));
2149 fun prep_result propps thmss =
2150 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
2152 fun goal_name thy kind target propss =
2153 kind ^ Proof.goal_names (Option.map (extern thy) target) ""
2154 (propss |> map (fn ((name, _), _) => extern thy name));
2156 val global_goal = Proof.global_goal ProofDisplay.present_results
2157 Attrib.attribute_i ProofContext.bind_propp_schematic_i;
2161 fun interpretation after_qed (prfx, atts) expr insts thy =
2163 val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
2164 val kind = goal_name thy "interpretation" NONE propss;
2165 fun after_qed' results =
2166 ProofContext.theory (activate (prep_result propss results))
2169 ProofContext.init thy
2170 |> Proof.theorem_i kind NONE after_qed' NONE ("", []) (prep_propp propss)
2171 |> Element.refine_witness |> Seq.hd
2174 fun interpretation_in_locale after_qed (raw_target, expr) thy =
2176 val target = intern thy raw_target;
2177 val (propss, activate) = prep_registration_in_locale target expr thy;
2178 val kind = goal_name thy "interpretation" (SOME target) propss;
2179 val raw_stmt = prep_propp propss;
2181 val (_, _, goal_ctxt, propp) = thy
2182 |> ProofContext.init |> init_term_syntax target
2183 |> cert_context_statement (SOME target) [] (map snd raw_stmt)
2185 fun after_qed' results =
2186 ProofContext.theory (activate (prep_result propss results))
2190 |> global_goal kind NONE after_qed' NONE ("", []) (map fst raw_stmt ~~ propp)
2191 |> Element.refine_witness |> Seq.hd
2194 fun interpret after_qed (prfx, atts) expr insts int state =
2196 val _ = Proof.assert_forward_or_chain state;
2197 val ctxt = Proof.context_of state;
2198 val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;
2199 val kind = goal_name (Proof.theory_of state) "interpret" NONE propss;
2200 fun after_qed' results =
2201 Proof.map_context (K (ctxt |> activate (prep_result propss results)))
2202 #> Proof.put_facts NONE
2206 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
2207 kind NONE after_qed' (prep_propp propss)
2208 |> Element.refine_witness |> Seq.hd