1 (* Title: Pure/Isar/locale.ML |
|
2 Author: Clemens Ballarin, TU Muenchen |
|
3 Author: Markus Wenzel, LMU/TU Muenchen |
|
4 |
|
5 Locales -- Isar proof contexts as meta-level predicates, with local |
|
6 syntax and implicit structures. |
|
7 |
|
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. |
|
13 |
|
14 Interpretation enables the reuse of theorems of locales in other |
|
15 contexts, namely those defined by theories, structured proofs and |
|
16 locales themselves. |
|
17 |
|
18 See also: |
|
19 |
|
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, |
|
28 pages 31-43, 2006. |
|
29 *) |
|
30 |
|
31 (* TODO: |
|
32 - beta-eta normalisation of interpretation parameters |
|
33 - dangling type frees in locales |
|
34 - test subsumption of interpretations when merging theories |
|
35 *) |
|
36 |
|
37 signature OLD_LOCALE = |
|
38 sig |
|
39 datatype expr = |
|
40 Locale of string | |
|
41 Rename of expr * (string * mixfix option) option list | |
|
42 Merge of expr list |
|
43 val empty: expr |
|
44 |
|
45 val intern: theory -> xstring -> string |
|
46 val intern_expr: theory -> expr -> expr |
|
47 val extern: theory -> string -> xstring |
|
48 val init: string -> theory -> Proof.context |
|
49 |
|
50 (* The specification of a locale *) |
|
51 val parameters_of: theory -> string -> ((string * typ) * mixfix) list |
|
52 val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list |
|
53 val local_asms_of: theory -> string -> (Attrib.binding * term list) list |
|
54 val global_asms_of: theory -> string -> (Attrib.binding * term list) list |
|
55 |
|
56 (* Theorems *) |
|
57 val intros: theory -> string -> thm list * thm list |
|
58 val dests: theory -> string -> thm list |
|
59 (* Not part of the official interface. DO NOT USE *) |
|
60 val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list |
|
61 |
|
62 (* Not part of the official interface. DO NOT USE *) |
|
63 val declarations_of: theory -> string -> declaration list * declaration list; |
|
64 |
|
65 (* Processing of locale statements *) |
|
66 val read_context_statement: string option -> Element.context list -> |
|
67 (string * string list) list list -> Proof.context -> |
|
68 string option * Proof.context * Proof.context * (term * term list) list list |
|
69 val read_context_statement_cmd: xstring option -> Element.context list -> |
|
70 (string * string list) list list -> Proof.context -> |
|
71 string option * Proof.context * Proof.context * (term * term list) list list |
|
72 val cert_context_statement: string option -> Element.context_i list -> |
|
73 (term * term list) list list -> Proof.context -> |
|
74 string option * Proof.context * Proof.context * (term * term list) list list |
|
75 val read_expr: expr -> Element.context list -> Proof.context -> |
|
76 Element.context_i list * Proof.context |
|
77 val cert_expr: expr -> Element.context_i list -> Proof.context -> |
|
78 Element.context_i list * Proof.context |
|
79 |
|
80 (* Diagnostic functions *) |
|
81 val print_locales: theory -> unit |
|
82 val print_locale: theory -> bool -> expr -> Element.context list -> unit |
|
83 val print_registrations: bool -> string -> Proof.context -> unit |
|
84 |
|
85 val add_locale: string -> bstring -> expr -> Element.context_i list -> theory |
|
86 -> string * Proof.context |
|
87 val add_locale_cmd: bstring -> expr -> Element.context list -> theory |
|
88 -> string * Proof.context |
|
89 |
|
90 (* Tactics *) |
|
91 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic |
|
92 |
|
93 (* Storing results *) |
|
94 val global_note_qualified: string -> |
|
95 ((Binding.T * attribute list) * (thm list * attribute list) list) list -> |
|
96 theory -> (string * thm list) list * theory |
|
97 val local_note_qualified: string -> |
|
98 ((Binding.T * attribute list) * (thm list * attribute list) list) list -> |
|
99 Proof.context -> (string * thm list) list * Proof.context |
|
100 val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
|
101 Proof.context -> Proof.context |
|
102 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context |
|
103 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context |
|
104 val add_declaration: string -> declaration -> Proof.context -> Proof.context |
|
105 |
|
106 (* Interpretation *) |
|
107 val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string -> |
|
108 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
|
109 string -> term list -> Morphism.morphism |
|
110 val interpretation: (Proof.context -> Proof.context) -> |
|
111 (Binding.T -> Binding.T) -> expr -> |
|
112 term option list * (Attrib.binding * term) list -> |
|
113 theory -> |
|
114 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
|
115 val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list -> |
|
116 theory -> Proof.state |
|
117 val interpretation_in_locale: (Proof.context -> Proof.context) -> |
|
118 xstring * expr -> theory -> Proof.state |
|
119 val interpret: (Proof.state -> Proof.state) -> |
|
120 (Binding.T -> Binding.T) -> expr -> |
|
121 term option list * (Attrib.binding * term) list -> |
|
122 bool -> Proof.state -> |
|
123 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
|
124 val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list -> |
|
125 bool -> Proof.state -> Proof.state |
|
126 end; |
|
127 |
|
128 structure Old_Locale: OLD_LOCALE = |
|
129 struct |
|
130 |
|
131 (* legacy operations *) |
|
132 |
|
133 fun merge_lists _ xs [] = xs |
|
134 | merge_lists _ [] ys = ys |
|
135 | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys; |
|
136 |
|
137 fun merge_alists eq xs = merge_lists (eq_fst eq) xs; |
|
138 |
|
139 |
|
140 (* auxiliary: noting name bindings with qualified base names *) |
|
141 |
|
142 fun global_note_qualified kind facts thy = |
|
143 thy |
|
144 |> Sign.qualified_names |
|
145 |> PureThy.note_thmss kind facts |
|
146 ||> Sign.restore_naming thy; |
|
147 |
|
148 fun local_note_qualified kind facts ctxt = |
|
149 ctxt |
|
150 |> ProofContext.qualified_names |
|
151 |> ProofContext.note_thmss_i kind facts |
|
152 ||> ProofContext.restore_naming ctxt; |
|
153 |
|
154 |
|
155 (** locale elements and expressions **) |
|
156 |
|
157 datatype ctxt = datatype Element.ctxt; |
|
158 |
|
159 datatype expr = |
|
160 Locale of string | |
|
161 Rename of expr * (string * mixfix option) option list | |
|
162 Merge of expr list; |
|
163 |
|
164 val empty = Merge []; |
|
165 |
|
166 datatype 'a element = |
|
167 Elem of 'a | Expr of expr; |
|
168 |
|
169 fun map_elem f (Elem e) = Elem (f e) |
|
170 | map_elem _ (Expr e) = Expr e; |
|
171 |
|
172 type decl = declaration * stamp; |
|
173 |
|
174 type locale = |
|
175 {axiom: Element.witness list, |
|
176 (* For locales that define predicates this is [A [A]], where A is the locale |
|
177 specification. Otherwise []. |
|
178 Only required to generate the right witnesses for locales with predicates. *) |
|
179 elems: (Element.context_i * stamp) list, |
|
180 (* Static content, neither Fixes nor Constrains elements *) |
|
181 params: ((string * typ) * mixfix) list, (*all term params*) |
|
182 decls: decl list * decl list, (*type/term_syntax declarations*) |
|
183 regs: ((string * string list) * Element.witness list) list, |
|
184 (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *) |
|
185 intros: thm list * thm list, |
|
186 (* Introduction rules: of delta predicate and locale predicate. *) |
|
187 dests: thm list} |
|
188 (* Destruction rules: projections from locale predicate to predicates of fragments. *) |
|
189 |
|
190 (* CB: an internal (Int) locale element was either imported or included, |
|
191 an external (Ext) element appears directly in the locale text. *) |
|
192 |
|
193 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; |
|
194 |
|
195 |
|
196 |
|
197 (** substitutions on Vars -- clone from element.ML **) |
|
198 |
|
199 (* instantiate types *) |
|
200 |
|
201 fun var_instT_type env = |
|
202 if Vartab.is_empty env then I |
|
203 else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x)); |
|
204 |
|
205 fun var_instT_term env = |
|
206 if Vartab.is_empty env then I |
|
207 else Term.map_types (var_instT_type env); |
|
208 |
|
209 fun var_inst_term (envT, env) = |
|
210 if Vartab.is_empty env then var_instT_term envT |
|
211 else |
|
212 let |
|
213 val instT = var_instT_type envT; |
|
214 fun inst (Const (x, T)) = Const (x, instT T) |
|
215 | inst (Free (x, T)) = Free(x, instT T) |
|
216 | inst (Var (xi, T)) = |
|
217 (case Vartab.lookup env xi of |
|
218 NONE => Var (xi, instT T) |
|
219 | SOME t => t) |
|
220 | inst (b as Bound _) = b |
|
221 | inst (Abs (x, T, t)) = Abs (x, instT T, inst t) |
|
222 | inst (t $ u) = inst t $ inst u; |
|
223 in Envir.beta_norm o inst end; |
|
224 |
|
225 |
|
226 (** management of registrations in theories and proof contexts **) |
|
227 |
|
228 type registration = |
|
229 {prfx: (Binding.T -> Binding.T) * (string * string), |
|
230 (* first component: interpretation name morphism; |
|
231 second component: parameter prefix *) |
|
232 exp: Morphism.morphism, |
|
233 (* maps content to its originating context *) |
|
234 imp: (typ Vartab.table * typ list) * (term Vartab.table * term list), |
|
235 (* inverse of exp *) |
|
236 wits: Element.witness list, |
|
237 (* witnesses of the registration *) |
|
238 eqns: thm Termtab.table, |
|
239 (* theorems (equations) interpreting derived concepts and indexed by lhs *) |
|
240 morph: unit |
|
241 (* interpreting morphism *) |
|
242 } |
|
243 |
|
244 structure Registrations : |
|
245 sig |
|
246 type T |
|
247 val empty: T |
|
248 val join: T * T -> T |
|
249 val dest: theory -> T -> |
|
250 (term list * |
|
251 (((Binding.T -> Binding.T) * (string * string)) * |
|
252 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * |
|
253 Element.witness list * |
|
254 thm Termtab.table)) list |
|
255 val test: theory -> T * term list -> bool |
|
256 val lookup: theory -> |
|
257 T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
|
258 (((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option |
|
259 val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) -> |
|
260 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
|
261 T -> |
|
262 T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list |
|
263 val add_witness: term list -> Element.witness -> T -> T |
|
264 val add_equation: term list -> thm -> T -> T |
|
265 (* |
|
266 val update_morph: term list -> Morphism.morphism -> T -> T |
|
267 val get_morph: theory -> T -> |
|
268 term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) -> |
|
269 Morphism.morphism |
|
270 *) |
|
271 end = |
|
272 struct |
|
273 (* A registration is indexed by parameter instantiation. |
|
274 NB: index is exported whereas content is internalised. *) |
|
275 type T = registration Termtab.table; |
|
276 |
|
277 fun mk_reg prfx exp imp wits eqns morph = |
|
278 {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph}; |
|
279 |
|
280 fun map_reg f reg = |
|
281 let |
|
282 val {prfx, exp, imp, wits, eqns, morph} = reg; |
|
283 val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph); |
|
284 in mk_reg prfx' exp' imp' wits' eqns' morph' end; |
|
285 |
|
286 val empty = Termtab.empty; |
|
287 |
|
288 (* term list represented as single term, for simultaneous matching *) |
|
289 fun termify ts = |
|
290 Term.list_comb (Const ("", map fastype_of ts ---> propT), ts); |
|
291 fun untermify t = |
|
292 let fun ut (Const _) ts = ts |
|
293 | ut (s $ t) ts = ut s (t::ts) |
|
294 in ut t [] end; |
|
295 |
|
296 (* joining of registrations: |
|
297 - prefix and morphisms of right theory; |
|
298 - witnesses are equal, no attempt to subsumption testing; |
|
299 - union of equalities, if conflicting (i.e. two eqns with equal lhs) |
|
300 eqn of right theory takes precedence *) |
|
301 fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) => |
|
302 mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2); |
|
303 |
|
304 fun dest_transfer thy regs = |
|
305 Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) => |
|
306 (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m)))); |
|
307 |
|
308 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |> |
|
309 map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns))); |
|
310 |
|
311 (* registrations that subsume t *) |
|
312 fun subsumers thy t regs = |
|
313 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); |
|
314 |
|
315 (* test if registration that subsumes the query is present *) |
|
316 fun test thy (regs, ts) = |
|
317 not (null (subsumers thy (termify ts) regs)); |
|
318 |
|
319 (* look up registration, pick one that subsumes the query *) |
|
320 fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) = |
|
321 let |
|
322 val t = termify ts; |
|
323 val subs = subsumers thy t regs; |
|
324 in |
|
325 (case subs of |
|
326 [] => NONE |
|
327 | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) => |
|
328 let |
|
329 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); |
|
330 val tinst' = domT' |> map (fn (T as TFree (x, _)) => |
|
331 (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst |
|
332 |> var_instT_type impT)) |> Symtab.make; |
|
333 val inst' = dom' |> map (fn (t as Free (x, _)) => |
|
334 (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst) |
|
335 |> var_inst_term (impT, imp))) |> Symtab.make; |
|
336 val inst'_morph = Element.inst_morphism thy (tinst', inst'); |
|
337 in SOME (prfx, |
|
338 map (Element.morph_witness inst'_morph) wits, |
|
339 Termtab.map (Morphism.thm inst'_morph) eqns) |
|
340 end) |
|
341 end; |
|
342 |
|
343 (* add registration if not subsumed by ones already present, |
|
344 additionally returns registrations that are strictly subsumed *) |
|
345 fun insert thy ts prfx (exp, imp) regs = |
|
346 let |
|
347 val t = termify ts; |
|
348 val subs = subsumers thy t regs ; |
|
349 in (case subs of |
|
350 [] => let |
|
351 val sups = |
|
352 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); |
|
353 val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits))) |
|
354 in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end |
|
355 | _ => (regs, [])) |
|
356 end; |
|
357 |
|
358 fun gen_add f ts regs = |
|
359 let |
|
360 val t = termify ts; |
|
361 in |
|
362 Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs |
|
363 end; |
|
364 |
|
365 (* add witness theorem to registration, |
|
366 only if instantiation is exact, otherwise exception Option raised *) |
|
367 fun add_witness ts wit regs = |
|
368 gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m)) |
|
369 ts regs; |
|
370 |
|
371 (* add equation to registration, replaces previous equation with same lhs; |
|
372 only if instantiation is exact, otherwise exception Option raised; |
|
373 exception TERM raised if not a meta equality *) |
|
374 fun add_equation ts thm regs = |
|
375 gen_add (fn (x, e, i, thms, eqns, m) => |
|
376 (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m)) |
|
377 ts regs; |
|
378 |
|
379 end; |
|
380 |
|
381 |
|
382 (** theory data : locales **) |
|
383 |
|
384 structure LocalesData = TheoryDataFun |
|
385 ( |
|
386 type T = NameSpace.T * locale Symtab.table; |
|
387 (* 1st entry: locale namespace, |
|
388 2nd entry: locales of the theory *) |
|
389 |
|
390 val empty = NameSpace.empty_table; |
|
391 val copy = I; |
|
392 val extend = I; |
|
393 |
|
394 fun join_locales _ |
|
395 ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale, |
|
396 {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) = |
|
397 {axiom = axiom, |
|
398 elems = merge_lists (eq_snd (op =)) elems elems', |
|
399 params = params, |
|
400 decls = |
|
401 (Library.merge (eq_snd (op =)) (decls1, decls1'), |
|
402 Library.merge (eq_snd (op =)) (decls2, decls2')), |
|
403 regs = merge_alists (op =) regs regs', |
|
404 intros = intros, |
|
405 dests = dests}; |
|
406 fun merge _ = NameSpace.join_tables join_locales; |
|
407 ); |
|
408 |
|
409 |
|
410 |
|
411 (** context data : registrations **) |
|
412 |
|
413 structure RegistrationsData = GenericDataFun |
|
414 ( |
|
415 type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*) |
|
416 val empty = Symtab.empty; |
|
417 val extend = I; |
|
418 fun merge _ = Symtab.join (K Registrations.join); |
|
419 ); |
|
420 |
|
421 |
|
422 (** access locales **) |
|
423 |
|
424 val intern = NameSpace.intern o #1 o LocalesData.get; |
|
425 val extern = NameSpace.extern o #1 o LocalesData.get; |
|
426 |
|
427 fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name; |
|
428 |
|
429 fun the_locale thy name = case get_locale thy name |
|
430 of SOME loc => loc |
|
431 | NONE => error ("Unknown locale " ^ quote name); |
|
432 |
|
433 fun register_locale bname loc thy = |
|
434 thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) |
|
435 (Binding.name bname, loc) #> snd); |
|
436 |
|
437 fun change_locale name f thy = |
|
438 let |
|
439 val {axiom, elems, params, decls, regs, intros, dests} = |
|
440 the_locale thy name; |
|
441 val (axiom', elems', params', decls', regs', intros', dests') = |
|
442 f (axiom, elems, params, decls, regs, intros, dests); |
|
443 in |
|
444 thy |
|
445 |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom', |
|
446 elems = elems', params = params', |
|
447 decls = decls', regs = regs', intros = intros', dests = dests'})) |
|
448 end; |
|
449 |
|
450 fun print_locales thy = |
|
451 let val (space, locs) = LocalesData.get thy in |
|
452 Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) |
|
453 |> Pretty.writeln |
|
454 end; |
|
455 |
|
456 |
|
457 (* access registrations *) |
|
458 |
|
459 (* retrieve registration from theory or context *) |
|
460 |
|
461 fun get_registrations ctxt name = |
|
462 case Symtab.lookup (RegistrationsData.get ctxt) name of |
|
463 NONE => [] |
|
464 | SOME reg => Registrations.dest (Context.theory_of ctxt) reg; |
|
465 |
|
466 fun get_global_registrations thy = get_registrations (Context.Theory thy); |
|
467 fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt); |
|
468 |
|
469 |
|
470 fun get_registration ctxt imprt (name, ps) = |
|
471 case Symtab.lookup (RegistrationsData.get ctxt) name of |
|
472 NONE => NONE |
|
473 | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt)); |
|
474 |
|
475 fun get_global_registration thy = get_registration (Context.Theory thy); |
|
476 fun get_local_registration ctxt = get_registration (Context.Proof ctxt); |
|
477 |
|
478 |
|
479 fun test_registration ctxt (name, ps) = |
|
480 case Symtab.lookup (RegistrationsData.get ctxt) name of |
|
481 NONE => false |
|
482 | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps); |
|
483 |
|
484 fun test_global_registration thy = test_registration (Context.Theory thy); |
|
485 fun test_local_registration ctxt = test_registration (Context.Proof ctxt); |
|
486 |
|
487 |
|
488 (* add registration to theory or context, ignored if subsumed *) |
|
489 |
|
490 fun put_registration (name, ps) prfx morphs ctxt = |
|
491 RegistrationsData.map (fn regs => |
|
492 let |
|
493 val thy = Context.theory_of ctxt; |
|
494 val reg = the_default Registrations.empty (Symtab.lookup regs name); |
|
495 val (reg', sups) = Registrations.insert thy ps prfx morphs reg; |
|
496 val _ = if not (null sups) then warning |
|
497 ("Subsumed interpretation(s) of locale " ^ |
|
498 quote (extern thy name) ^ |
|
499 "\nwith the following prefix(es):" ^ |
|
500 commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups)) |
|
501 else (); |
|
502 in Symtab.update (name, reg') regs end) ctxt; |
|
503 |
|
504 fun put_global_registration id prfx morphs = |
|
505 Context.theory_map (put_registration id prfx morphs); |
|
506 fun put_local_registration id prfx morphs = |
|
507 Context.proof_map (put_registration id prfx morphs); |
|
508 |
|
509 fun put_registration_in_locale name id = |
|
510 change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => |
|
511 (axiom, elems, params, decls, regs @ [(id, [])], intros, dests)); |
|
512 |
|
513 |
|
514 (* add witness theorem to registration, ignored if registration not present *) |
|
515 |
|
516 fun add_witness (name, ps) thm = |
|
517 RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm)); |
|
518 |
|
519 fun add_global_witness id thm = Context.theory_map (add_witness id thm); |
|
520 fun add_local_witness id thm = Context.proof_map (add_witness id thm); |
|
521 |
|
522 |
|
523 fun add_witness_in_locale name id thm = |
|
524 change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => |
|
525 let |
|
526 fun add (id', thms) = |
|
527 if id = id' then (id', thm :: thms) else (id', thms); |
|
528 in (axiom, elems, params, decls, map add regs, intros, dests) end); |
|
529 |
|
530 |
|
531 (* add equation to registration, ignored if registration not present *) |
|
532 |
|
533 fun add_equation (name, ps) thm = |
|
534 RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm)); |
|
535 |
|
536 fun add_global_equation id thm = Context.theory_map (add_equation id thm); |
|
537 fun add_local_equation id thm = Context.proof_map (add_equation id thm); |
|
538 |
|
539 (* |
|
540 (* update morphism of registration, ignored if registration not present *) |
|
541 |
|
542 fun update_morph (name, ps) morph = |
|
543 RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph)); |
|
544 |
|
545 fun update_global_morph id morph = Context.theory_map (update_morph id morph); |
|
546 fun update_local_morph id morph = Context.proof_map (update_morph id morph); |
|
547 *) |
|
548 |
|
549 |
|
550 (* printing of registrations *) |
|
551 |
|
552 fun print_registrations show_wits loc ctxt = |
|
553 let |
|
554 val thy = ProofContext.theory_of ctxt; |
|
555 val prt_term = Pretty.quote o Syntax.pretty_term ctxt; |
|
556 fun prt_term' t = if !show_types |
|
557 then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", |
|
558 Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] |
|
559 else prt_term t; |
|
560 val prt_thm = prt_term o prop_of; |
|
561 fun prt_inst ts = |
|
562 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts)); |
|
563 fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx] |
|
564 | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx]; |
|
565 fun prt_eqns [] = Pretty.str "no equations." |
|
566 | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 :: |
|
567 Pretty.breaks (map prt_thm eqns)); |
|
568 fun prt_core ts eqns = |
|
569 [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)]; |
|
570 fun prt_witns [] = Pretty.str "no witnesses." |
|
571 | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 :: |
|
572 Pretty.breaks (map (Element.pretty_witness ctxt) witns)) |
|
573 fun prt_reg (ts, (_, _, witns, eqns)) = |
|
574 if show_wits |
|
575 then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]) |
|
576 else Pretty.block (prt_core ts eqns) |
|
577 |
|
578 val loc_int = intern thy loc; |
|
579 val regs = RegistrationsData.get (Context.Proof ctxt); |
|
580 val loc_regs = Symtab.lookup regs loc_int; |
|
581 in |
|
582 (case loc_regs of |
|
583 NONE => Pretty.str ("no interpretations") |
|
584 | SOME r => let |
|
585 val r' = Registrations.dest thy r; |
|
586 val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r'; |
|
587 in Pretty.big_list ("interpretations:") (map prt_reg r'') end) |
|
588 |> Pretty.writeln |
|
589 end; |
|
590 |
|
591 |
|
592 (* diagnostics *) |
|
593 |
|
594 fun err_in_locale ctxt msg ids = |
|
595 let |
|
596 val thy = ProofContext.theory_of ctxt; |
|
597 fun prt_id (name, parms) = |
|
598 [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))]; |
|
599 val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); |
|
600 val err_msg = |
|
601 if forall (fn (s, _) => s = "") ids then msg |
|
602 else msg ^ "\n" ^ Pretty.string_of (Pretty.block |
|
603 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); |
|
604 in error err_msg end; |
|
605 |
|
606 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); |
|
607 |
|
608 |
|
609 fun pretty_ren NONE = Pretty.str "_" |
|
610 | pretty_ren (SOME (x, NONE)) = Pretty.str x |
|
611 | pretty_ren (SOME (x, SOME syn)) = |
|
612 Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn]; |
|
613 |
|
614 fun pretty_expr thy (Locale name) = Pretty.str (extern thy name) |
|
615 | pretty_expr thy (Rename (expr, xs)) = |
|
616 Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)] |
|
617 | pretty_expr thy (Merge es) = |
|
618 Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block; |
|
619 |
|
620 fun err_in_expr _ msg (Merge []) = error msg |
|
621 | err_in_expr ctxt msg expr = |
|
622 error (msg ^ "\n" ^ Pretty.string_of (Pretty.block |
|
623 [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1, |
|
624 pretty_expr (ProofContext.theory_of ctxt) expr])); |
|
625 |
|
626 |
|
627 (** structured contexts: rename + merge + implicit type instantiation **) |
|
628 |
|
629 (* parameter types *) |
|
630 |
|
631 fun frozen_tvars ctxt Ts = |
|
632 #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt) |
|
633 |> map (fn ((xi, S), T) => (xi, (S, T))); |
|
634 |
|
635 fun unify_frozen ctxt maxidx Ts Us = |
|
636 let |
|
637 fun paramify NONE i = (NONE, i) |
|
638 | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i); |
|
639 |
|
640 val (Ts', maxidx') = fold_map paramify Ts maxidx; |
|
641 val (Us', maxidx'') = fold_map paramify Us maxidx'; |
|
642 val thy = ProofContext.theory_of ctxt; |
|
643 |
|
644 fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env |
|
645 handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) |
|
646 | unify _ env = env; |
|
647 val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx''); |
|
648 val Vs = map (Option.map (Envir.norm_type unifier)) Us'; |
|
649 val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier; |
|
650 in map (Option.map (Envir.norm_type unifier')) Vs end; |
|
651 |
|
652 fun params_of elemss = |
|
653 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss); |
|
654 |
|
655 fun params_of' elemss = |
|
656 distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss); |
|
657 |
|
658 fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params); |
|
659 |
|
660 |
|
661 (* CB: param_types has the following type: |
|
662 ('a * 'b option) list -> ('a * 'b) list *) |
|
663 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; |
|
664 |
|
665 |
|
666 fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss |
|
667 handle Symtab.DUP x => err_in_locale ctxt |
|
668 ("Conflicting syntax for parameter: " ^ quote x) (map fst ids); |
|
669 |
|
670 |
|
671 (* Distinction of assumed vs. derived identifiers. |
|
672 The former may have axioms relating assumptions of the context to |
|
673 assumptions of the specification fragment (for locales with |
|
674 predicates). The latter have witnesses relating assumptions of the |
|
675 specification fragment to assumptions of other (assumed) specification |
|
676 fragments. *) |
|
677 |
|
678 datatype 'a mode = Assumed of 'a | Derived of 'a; |
|
679 |
|
680 fun map_mode f (Assumed x) = Assumed (f x) |
|
681 | map_mode f (Derived x) = Derived (f x); |
|
682 |
|
683 |
|
684 (* flatten expressions *) |
|
685 |
|
686 local |
|
687 |
|
688 fun unify_parms ctxt fixed_parms raw_parmss = |
|
689 let |
|
690 val thy = ProofContext.theory_of ctxt; |
|
691 val maxidx = length raw_parmss; |
|
692 val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss; |
|
693 |
|
694 fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S)); |
|
695 fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); |
|
696 val parms = fixed_parms @ maps varify_parms idx_parmss; |
|
697 |
|
698 fun unify T U envir = Sign.typ_unify thy (U, T) envir |
|
699 handle Type.TUNIFY => |
|
700 let |
|
701 val T' = Envir.norm_type (fst envir) T; |
|
702 val U' = Envir.norm_type (fst envir) U; |
|
703 val prt = Syntax.string_of_typ ctxt; |
|
704 in |
|
705 raise TYPE ("unify_parms: failed to unify types " ^ |
|
706 prt U' ^ " and " ^ prt T', [U', T'], []) |
|
707 end; |
|
708 fun unify_list (T :: Us) = fold (unify T) Us |
|
709 | unify_list [] = I; |
|
710 val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms))) |
|
711 (Vartab.empty, maxidx); |
|
712 |
|
713 val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms); |
|
714 val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier; |
|
715 |
|
716 fun inst_parms (i, ps) = |
|
717 List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps) |
|
718 |> map_filter (fn (a, S) => |
|
719 let val T = Envir.norm_type unifier' (TVar ((a, i), S)) |
|
720 in if T = TFree (a, S) then NONE else SOME (a, T) end) |
|
721 |> Symtab.make; |
|
722 in map inst_parms idx_parmss end; |
|
723 |
|
724 in |
|
725 |
|
726 fun unify_elemss _ _ [] = [] |
|
727 | unify_elemss _ [] [elems] = [elems] |
|
728 | unify_elemss ctxt fixed_parms elemss = |
|
729 let |
|
730 val thy = ProofContext.theory_of ctxt; |
|
731 val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss) |
|
732 |> map (Element.instT_morphism thy); |
|
733 fun inst ((((name, ps), mode), elems), phi) = |
|
734 (((name, map (apsnd (Option.map (Morphism.typ phi))) ps), |
|
735 map_mode (map (Element.morph_witness phi)) mode), |
|
736 map (Element.morph_ctxt phi) elems); |
|
737 in map inst (elemss ~~ phis) end; |
|
738 |
|
739 |
|
740 fun renaming xs parms = zip_options parms xs |
|
741 handle Library.UnequalLengths => |
|
742 error ("Too many arguments in renaming: " ^ |
|
743 commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs)); |
|
744 |
|
745 |
|
746 (* params_of_expr: |
|
747 Compute parameters (with types and syntax) of locale expression. |
|
748 *) |
|
749 |
|
750 fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) = |
|
751 let |
|
752 val thy = ProofContext.theory_of ctxt; |
|
753 |
|
754 fun merge_tenvs fixed tenv1 tenv2 = |
|
755 let |
|
756 val [env1, env2] = unify_parms ctxt fixed |
|
757 [tenv1 |> Symtab.dest |> map (apsnd SOME), |
|
758 tenv2 |> Symtab.dest |> map (apsnd SOME)] |
|
759 in |
|
760 Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1, |
|
761 Symtab.map (Element.instT_type env2) tenv2) |
|
762 end; |
|
763 |
|
764 fun merge_syn expr syn1 syn2 = |
|
765 Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2) |
|
766 handle Symtab.DUP x => err_in_expr ctxt |
|
767 ("Conflicting syntax for parameter: " ^ quote x) expr; |
|
768 |
|
769 fun params_of (expr as Locale name) = |
|
770 let |
|
771 val {params, ...} = the_locale thy name; |
|
772 in (map (fst o fst) params, params |> map fst |> Symtab.make, |
|
773 params |> map (apfst fst) |> Symtab.make) end |
|
774 | params_of (expr as Rename (e, xs)) = |
|
775 let |
|
776 val (parms', types', syn') = params_of e; |
|
777 val ren = renaming xs parms'; |
|
778 (* renaming may reduce number of parameters *) |
|
779 val new_parms = map (Element.rename ren) parms' |> distinct (op =); |
|
780 val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren); |
|
781 val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty |
|
782 handle Symtab.DUP x => |
|
783 err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr; |
|
784 val syn_types = map (apsnd (fn mx => |
|
785 SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0))))) |
|
786 (Symtab.dest new_syn); |
|
787 val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren)); |
|
788 val (env :: _) = unify_parms ctxt [] |
|
789 ((ren_types |> map (apsnd SOME)) :: map single syn_types); |
|
790 val new_types = fold (Symtab.insert (op =)) |
|
791 (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty; |
|
792 in (new_parms, new_types, new_syn) end |
|
793 | params_of (Merge es) = |
|
794 fold (fn e => fn (parms, types, syn) => |
|
795 let |
|
796 val (parms', types', syn') = params_of e |
|
797 in |
|
798 (merge_lists (op =) parms parms', merge_tenvs [] types types', |
|
799 merge_syn e syn syn') |
|
800 end) |
|
801 es ([], Symtab.empty, Symtab.empty) |
|
802 |
|
803 val (parms, types, syn) = params_of expr; |
|
804 in |
|
805 (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types, |
|
806 merge_syn expr prev_syn syn) |
|
807 end; |
|
808 |
|
809 fun make_params_ids params = [(("", params), ([], Assumed []))]; |
|
810 fun make_raw_params_elemss (params, tenv, syn) = |
|
811 [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []), |
|
812 Int [Fixes (map (fn p => |
|
813 (Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])]; |
|
814 |
|
815 |
|
816 (* flatten_expr: |
|
817 Extend list of identifiers by those new in locale expression expr. |
|
818 Compute corresponding list of lists of locale elements (one entry per |
|
819 identifier). |
|
820 |
|
821 Identifiers represent locale fragments and are in an extended form: |
|
822 ((name, ps), (ax_ps, axs)) |
|
823 (name, ps) is the locale name with all its parameters. |
|
824 (ax_ps, axs) is the locale axioms with its parameters; |
|
825 axs are always taken from the top level of the locale hierarchy, |
|
826 hence axioms may contain additional parameters from later fragments: |
|
827 ps subset of ax_ps. axs is either singleton or empty. |
|
828 |
|
829 Elements are enriched by identifier-like information: |
|
830 (((name, ax_ps), axs), elems) |
|
831 The parameters in ax_ps are the axiom parameters, but enriched by type |
|
832 info: now each entry is a pair of string and typ option. Axioms are |
|
833 type-instantiated. |
|
834 |
|
835 *) |
|
836 |
|
837 fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = |
|
838 let |
|
839 val thy = ProofContext.theory_of ctxt; |
|
840 |
|
841 fun rename_parms top ren ((name, ps), (parms, mode)) = |
|
842 ((name, map (Element.rename ren) ps), |
|
843 if top |
|
844 then (map (Element.rename ren) parms, |
|
845 map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode) |
|
846 else (parms, mode)); |
|
847 |
|
848 (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *) |
|
849 |
|
850 fun add_with_regs ((name, pTs), mode) (wits, ids, visited) = |
|
851 if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs) |
|
852 then (wits, ids, visited) |
|
853 else |
|
854 let |
|
855 val {params, regs, ...} = the_locale thy name; |
|
856 val pTs' = map #1 params; |
|
857 val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs; |
|
858 (* dummy syntax, since required by rename *) |
|
859 val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs'); |
|
860 val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs'']; |
|
861 (* propagate parameter types, to keep them consistent *) |
|
862 val regs' = map (fn ((name, ps), wits) => |
|
863 ((name, map (Element.rename ren) ps), |
|
864 map (Element.transfer_witness thy) wits)) regs; |
|
865 val new_regs = regs'; |
|
866 val new_ids = map fst new_regs; |
|
867 val new_idTs = |
|
868 map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids; |
|
869 |
|
870 val new_wits = new_regs |> map (#2 #> map |
|
871 (Element.morph_witness |
|
872 (Element.instT_morphism thy env $> |
|
873 Element.rename_morphism ren $> |
|
874 Element.satisfy_morphism wits) |
|
875 #> Element.close_witness)); |
|
876 val new_ids' = map (fn (id, wits) => |
|
877 (id, ([], Derived wits))) (new_ids ~~ new_wits); |
|
878 val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) => |
|
879 ((n, pTs), mode)) (new_idTs ~~ new_ids'); |
|
880 val new_id = ((name, map #1 pTs), ([], mode)); |
|
881 val (wits', ids', visited') = fold add_with_regs new_idTs' |
|
882 (wits @ flat new_wits, ids, visited @ [new_id]); |
|
883 in |
|
884 (wits', ids' @ [new_id], visited') |
|
885 end; |
|
886 |
|
887 (* distribute top-level axioms over assumed ids *) |
|
888 |
|
889 fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms = |
|
890 let |
|
891 val {elems, ...} = the_locale thy name; |
|
892 val ts = maps |
|
893 (fn (Assumes asms, _) => maps (map #1 o #2) asms |
|
894 | _ => []) |
|
895 elems; |
|
896 val (axs1, axs2) = chop (length ts) axioms; |
|
897 in (((name, parms), (all_ps, Assumed axs1)), axs2) end |
|
898 | axiomify all_ps (id, (_, Derived ths)) axioms = |
|
899 ((id, (all_ps, Derived ths)), axioms); |
|
900 |
|
901 (* identifiers of an expression *) |
|
902 |
|
903 fun identify top (Locale name) = |
|
904 (* CB: ids_ax is a list of tuples of the form ((name, ps), axs), |
|
905 where name is a locale name, ps a list of parameter names and axs |
|
906 a list of axioms relating to the identifier, axs is empty unless |
|
907 identify at top level (top = true); |
|
908 parms is accumulated list of parameters *) |
|
909 let |
|
910 val {axiom, params, ...} = the_locale thy name; |
|
911 val ps = map (#1 o #1) params; |
|
912 val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []); |
|
913 val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids''; |
|
914 in (ids_ax, ps) end |
|
915 | identify top (Rename (e, xs)) = |
|
916 let |
|
917 val (ids', parms') = identify top e; |
|
918 val ren = renaming xs parms' |
|
919 handle ERROR msg => err_in_locale' ctxt msg ids'; |
|
920 |
|
921 val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids'); |
|
922 val parms'' = distinct (op =) (maps (#2 o #1) ids''); |
|
923 in (ids'', parms'') end |
|
924 | identify top (Merge es) = |
|
925 fold (fn e => fn (ids, parms) => |
|
926 let |
|
927 val (ids', parms') = identify top e |
|
928 in |
|
929 (merge_alists (op =) ids ids', merge_lists (op =) parms parms') |
|
930 end) |
|
931 es ([], []); |
|
932 |
|
933 fun inst_wit all_params (t, th) = let |
|
934 val {hyps, prop, ...} = Thm.rep_thm th; |
|
935 val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []); |
|
936 val [env] = unify_parms ctxt all_params [ps]; |
|
937 val t' = Element.instT_term env t; |
|
938 val th' = Element.instT_thm thy env th; |
|
939 in (t', th') end; |
|
940 |
|
941 fun eval all_params tenv syn ((name, params), (locale_params, mode)) = |
|
942 let |
|
943 val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name; |
|
944 val elems = map fst elems_stamped; |
|
945 val ps = map fst ps_mx; |
|
946 fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt); |
|
947 val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params; |
|
948 val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode; |
|
949 val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params; |
|
950 val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps]; |
|
951 val (lprfx, pprfx) = param_prefix name params; |
|
952 val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx |
|
953 #> Binding.add_prefix false lprfx; |
|
954 val elem_morphism = |
|
955 Element.rename_morphism ren $> |
|
956 Morphism.binding_morphism add_prefices $> |
|
957 Element.instT_morphism thy env; |
|
958 val elems' = map (Element.morph_ctxt elem_morphism) elems; |
|
959 in (((name, map (apsnd SOME) locale_params'), mode'), elems') end; |
|
960 |
|
961 (* parameters, their types and syntax *) |
|
962 val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty); |
|
963 val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params'; |
|
964 (* compute identifiers and syntax, merge with previous ones *) |
|
965 val (ids, _) = identify true expr; |
|
966 val idents = subtract (eq_fst (op =)) prev_idents ids; |
|
967 val syntax = merge_syntax ctxt ids (syn, prev_syntax); |
|
968 (* type-instantiate elements *) |
|
969 val final_elemss = map (eval all_params tenv syntax) idents; |
|
970 in ((prev_idents @ idents, syntax), final_elemss) end; |
|
971 |
|
972 end; |
|
973 |
|
974 |
|
975 (* activate elements *) |
|
976 |
|
977 local |
|
978 |
|
979 fun axioms_export axs _ As = |
|
980 (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t); |
|
981 |
|
982 |
|
983 (* NB: derived ids contain only facts at this stage *) |
|
984 |
|
985 fun activate_elem _ _ (Fixes fixes) (ctxt, mode) = |
|
986 ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode)) |
|
987 | activate_elem _ _ (Constrains _) (ctxt, mode) = |
|
988 ([], (ctxt, mode)) |
|
989 | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) = |
|
990 let |
|
991 val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; |
|
992 val ts = maps (map #1 o #2) asms'; |
|
993 val (ps, qs) = chop (length ts) axs; |
|
994 val (_, ctxt') = |
|
995 ctxt |> fold Variable.auto_fixes ts |
|
996 |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms'; |
|
997 in ([], (ctxt', Assumed qs)) end |
|
998 | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) = |
|
999 ([], (ctxt, Derived ths)) |
|
1000 | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) = |
|
1001 let |
|
1002 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; |
|
1003 val asms = defs' |> map (fn ((name, atts), (t, ps)) => |
|
1004 let val ((c, _), t') = LocalDefs.cert_def ctxt t |
|
1005 in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end); |
|
1006 val (_, ctxt') = |
|
1007 ctxt |> fold (Variable.auto_fixes o #1) asms |
|
1008 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); |
|
1009 in ([], (ctxt', Assumed axs)) end |
|
1010 | activate_elem _ _ (Defines defs) (ctxt, Derived ths) = |
|
1011 ([], (ctxt, Derived ths)) |
|
1012 | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) = |
|
1013 let |
|
1014 val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; |
|
1015 val (res, ctxt') = ctxt |> local_note_qualified kind facts'; |
|
1016 in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end; |
|
1017 |
|
1018 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt = |
|
1019 let |
|
1020 val thy = ProofContext.theory_of ctxt; |
|
1021 val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = "")) |
|
1022 elems (ProofContext.qualified_names ctxt, mode) |
|
1023 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]; |
|
1024 val ctxt'' = if name = "" then ctxt' |
|
1025 else let |
|
1026 val ps' = map (fn (n, SOME T) => Free (n, T)) ps; |
|
1027 in if test_local_registration ctxt' (name, ps') then ctxt' |
|
1028 else let |
|
1029 val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, "")) |
|
1030 (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt' |
|
1031 in case mode of |
|
1032 Assumed axs => |
|
1033 fold (add_local_witness (name, ps') o |
|
1034 Element.assume_witness thy o Element.witness_prop) axs ctxt'' |
|
1035 | Derived ths => |
|
1036 fold (add_local_witness (name, ps')) ths ctxt'' |
|
1037 end |
|
1038 end |
|
1039 in (ProofContext.restore_naming ctxt ctxt'', res) end; |
|
1040 |
|
1041 fun activate_elemss ax_in_ctxt prep_facts = |
|
1042 fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt => |
|
1043 let |
|
1044 val elems = map (prep_facts ctxt) raw_elems; |
|
1045 val (ctxt', res) = apsnd flat |
|
1046 (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt); |
|
1047 val elems' = elems |> map (Element.map_ctxt_attrib Args.closure); |
|
1048 in (((((name, ps), mode), elems'), res), ctxt') end); |
|
1049 |
|
1050 in |
|
1051 |
|
1052 (* CB: activate_facts prep_facts elemss ctxt, |
|
1053 where elemss is a list of pairs consisting of identifiers and |
|
1054 context elements, extends ctxt by the context elements yielding |
|
1055 ctxt' and returns ((elemss', facts), ctxt'). |
|
1056 Identifiers in the argument are of the form ((name, ps), axs) and |
|
1057 assumptions use the axioms in the identifiers to set up exporters |
|
1058 in ctxt'. elemss' does not contain identifiers and is obtained |
|
1059 from elemss and the intermediate context with prep_facts. |
|
1060 If read_facts or cert_facts is used for prep_facts, these also remove |
|
1061 the internal/external markers from elemss. *) |
|
1062 |
|
1063 fun activate_facts ax_in_ctxt prep_facts args = |
|
1064 activate_elemss ax_in_ctxt prep_facts args |
|
1065 #>> (apsnd flat o split_list); |
|
1066 |
|
1067 end; |
|
1068 |
|
1069 |
|
1070 |
|
1071 (** prepare locale elements **) |
|
1072 |
|
1073 (* expressions *) |
|
1074 |
|
1075 fun intern_expr thy (Locale xname) = Locale (intern thy xname) |
|
1076 | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) |
|
1077 | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs); |
|
1078 |
|
1079 |
|
1080 (* propositions and bindings *) |
|
1081 |
|
1082 (* flatten (ctxt, prep_expr) ((ids, syn), expr) |
|
1083 normalises expr (which is either a locale |
|
1084 expression or a single context element) wrt. |
|
1085 to the list ids of already accumulated identifiers. |
|
1086 It returns ((ids', syn'), elemss) where ids' is an extension of ids |
|
1087 with identifiers generated for expr, and elemss is the list of |
|
1088 context elements generated from expr. |
|
1089 syn and syn' are symtabs mapping parameter names to their syntax. syn' |
|
1090 is an extension of syn. |
|
1091 For details, see flatten_expr. |
|
1092 |
|
1093 Additionally, for a locale expression, the elems are grouped into a single |
|
1094 Int; individual context elements are marked Ext. In this case, the |
|
1095 identifier-like information of the element is as follows: |
|
1096 - for Fixes: (("", ps), []) where the ps have type info NONE |
|
1097 - for other elements: (("", []), []). |
|
1098 The implementation of activate_facts relies on identifier names being |
|
1099 empty strings for external elements. |
|
1100 *) |
|
1101 |
|
1102 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let |
|
1103 val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))] |
|
1104 in |
|
1105 ((ids', |
|
1106 merge_syntax ctxt ids' |
|
1107 (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes)) |
|
1108 handle Symtab.DUP x => err_in_locale ctxt |
|
1109 ("Conflicting syntax for parameter: " ^ quote x) |
|
1110 (map #1 ids')), |
|
1111 [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))]) |
|
1112 end |
|
1113 | flatten _ ((ids, syn), Elem elem) = |
|
1114 ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)]) |
|
1115 | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) = |
|
1116 apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr)); |
|
1117 |
|
1118 local |
|
1119 |
|
1120 local |
|
1121 |
|
1122 fun declare_int_elem (Fixes fixes) ctxt = |
|
1123 ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) => |
|
1124 (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd) |
|
1125 | declare_int_elem _ ctxt = ([], ctxt); |
|
1126 |
|
1127 fun declare_ext_elem prep_vars (Fixes fixes) ctxt = |
|
1128 let val (vars, _) = prep_vars fixes ctxt |
|
1129 in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end |
|
1130 | declare_ext_elem prep_vars (Constrains csts) ctxt = |
|
1131 let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt |
|
1132 in ([], ctxt') end |
|
1133 | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt) |
|
1134 | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt) |
|
1135 | declare_ext_elem _ (Notes _) ctxt = ([], ctxt); |
|
1136 |
|
1137 fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems |
|
1138 of Int es => fold_map declare_int_elem es ctxt |
|
1139 | Ext e => declare_ext_elem prep_vars e ctxt |>> single) |
|
1140 handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]) |
|
1141 | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt); |
|
1142 |
|
1143 in |
|
1144 |
|
1145 fun declare_elemss prep_vars fixed_params raw_elemss ctxt = |
|
1146 let |
|
1147 (* CB: fix of type bug of goal in target with context elements. |
|
1148 Parameters new in context elements must receive types that are |
|
1149 distinct from types of parameters in target (fixed_params). *) |
|
1150 val ctxt_with_fixed = |
|
1151 fold Variable.declare_term (map Free fixed_params) ctxt; |
|
1152 val int_elemss = |
|
1153 raw_elemss |
|
1154 |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE) |
|
1155 |> unify_elemss ctxt_with_fixed fixed_params; |
|
1156 val (raw_elemss', _) = |
|
1157 fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x)) |
|
1158 raw_elemss int_elemss; |
|
1159 in fold_map (declare_elems prep_vars) raw_elemss' ctxt end; |
|
1160 |
|
1161 end; |
|
1162 |
|
1163 local |
|
1164 |
|
1165 val norm_term = Envir.beta_norm oo Term.subst_atomic; |
|
1166 |
|
1167 fun abstract_thm thy eq = |
|
1168 Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def; |
|
1169 |
|
1170 fun bind_def ctxt (name, ps) eq (xs, env, ths) = |
|
1171 let |
|
1172 val ((y, T), b) = LocalDefs.abs_def eq; |
|
1173 val b' = norm_term env b; |
|
1174 val th = abstract_thm (ProofContext.theory_of ctxt) eq; |
|
1175 fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; |
|
1176 in |
|
1177 exists (fn (x, _) => x = y) xs andalso |
|
1178 err "Attempt to define previously specified variable"; |
|
1179 exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso |
|
1180 err "Attempt to redefine variable"; |
|
1181 (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) |
|
1182 end; |
|
1183 |
|
1184 |
|
1185 (* CB: for finish_elems (Int and Ext), |
|
1186 extracts specification, only of assumed elements *) |
|
1187 |
|
1188 fun eval_text _ _ _ (Fixes _) text = text |
|
1189 | eval_text _ _ _ (Constrains _) text = text |
|
1190 | eval_text _ (_, Assumed _) is_ext (Assumes asms) |
|
1191 (((exts, exts'), (ints, ints')), (xs, env, defs)) = |
|
1192 let |
|
1193 val ts = maps (map #1 o #2) asms; |
|
1194 val ts' = map (norm_term env) ts; |
|
1195 val spec' = |
|
1196 if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) |
|
1197 else ((exts, exts'), (ints @ ts, ints' @ ts')); |
|
1198 in (spec', (fold Term.add_frees ts' xs, env, defs)) end |
|
1199 | eval_text _ (_, Derived _) _ (Assumes _) text = text |
|
1200 | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) = |
|
1201 (spec, fold (bind_def ctxt id o #1 o #2) defs binds) |
|
1202 | eval_text _ (_, Derived _) _ (Defines _) text = text |
|
1203 | eval_text _ _ _ (Notes _) text = text; |
|
1204 |
|
1205 |
|
1206 (* for finish_elems (Int), |
|
1207 remove redundant elements of derived identifiers, |
|
1208 turn assumptions and definitions into facts, |
|
1209 satisfy hypotheses of facts *) |
|
1210 |
|
1211 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes) |
|
1212 | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts) |
|
1213 | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms) |
|
1214 | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs) |
|
1215 |
|
1216 | finish_derived _ _ (Derived _) (Fixes _) = NONE |
|
1217 | finish_derived _ _ (Derived _) (Constrains _) = NONE |
|
1218 | finish_derived sign satisfy (Derived _) (Assumes asms) = asms |
|
1219 |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) |
|
1220 |> pair Thm.assumptionK |> Notes |
|
1221 |> Element.morph_ctxt satisfy |> SOME |
|
1222 | finish_derived sign satisfy (Derived _) (Defines defs) = defs |
|
1223 |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) |
|
1224 |> pair Thm.definitionK |> Notes |
|
1225 |> Element.morph_ctxt satisfy |> SOME |
|
1226 |
|
1227 | finish_derived _ satisfy _ (Notes facts) = Notes facts |
|
1228 |> Element.morph_ctxt satisfy |> SOME; |
|
1229 |
|
1230 (* CB: for finish_elems (Ext) *) |
|
1231 |
|
1232 fun closeup _ false elem = elem |
|
1233 | closeup ctxt true elem = |
|
1234 let |
|
1235 fun close_frees t = |
|
1236 let |
|
1237 val rev_frees = |
|
1238 Term.fold_aterms (fn Free (x, T) => |
|
1239 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t []; |
|
1240 in Term.list_all_free (rev rev_frees, t) end; |
|
1241 |
|
1242 fun no_binds [] = [] |
|
1243 | no_binds _ = error "Illegal term bindings in locale element"; |
|
1244 in |
|
1245 (case elem of |
|
1246 Assumes asms => Assumes (asms |> map (fn (a, propps) => |
|
1247 (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) |
|
1248 | Defines defs => Defines (defs |> map (fn (a, (t, ps)) => |
|
1249 (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) |
|
1250 | e => e) |
|
1251 end; |
|
1252 |
|
1253 |
|
1254 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) => |
|
1255 let val x = Binding.base_name b |
|
1256 in (b, AList.lookup (op =) parms x, mx) end) fixes) |
|
1257 | finish_ext_elem parms _ (Constrains _, _) = Constrains [] |
|
1258 | finish_ext_elem _ close (Assumes asms, propp) = |
|
1259 close (Assumes (map #1 asms ~~ propp)) |
|
1260 | finish_ext_elem _ close (Defines defs, propp) = |
|
1261 close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp)) |
|
1262 | finish_ext_elem _ _ (Notes facts, _) = Notes facts; |
|
1263 |
|
1264 |
|
1265 (* CB: finish_parms introduces type info from parms to identifiers *) |
|
1266 (* CB: only needed for types that have been NONE so far??? |
|
1267 If so, which are these??? *) |
|
1268 |
|
1269 fun finish_parms parms (((name, ps), mode), elems) = |
|
1270 (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems); |
|
1271 |
|
1272 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) = |
|
1273 let |
|
1274 val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; |
|
1275 val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths; |
|
1276 val text' = fold (eval_text ctxt id' false) es text; |
|
1277 val es' = map_filter |
|
1278 (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es; |
|
1279 in ((text', wits'), (id', map Int es')) end |
|
1280 | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) = |
|
1281 let |
|
1282 val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); |
|
1283 val text' = eval_text ctxt id true e' text; |
|
1284 in ((text', wits), (id, [Ext e'])) end |
|
1285 |
|
1286 in |
|
1287 |
|
1288 (* CB: only called by prep_elemss *) |
|
1289 |
|
1290 fun finish_elemss ctxt parms do_close = |
|
1291 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); |
|
1292 |
|
1293 end; |
|
1294 |
|
1295 |
|
1296 (* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *) |
|
1297 |
|
1298 fun defs_ord (defs1, defs2) = |
|
1299 list_ord (fn ((_, (d1, _)), (_, (d2, _))) => |
|
1300 TermOrd.fast_term_ord (d1, d2)) (defs1, defs2); |
|
1301 structure Defstab = |
|
1302 TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord); |
|
1303 |
|
1304 fun rem_dup_defs es ds = |
|
1305 fold_map (fn e as (Defines defs) => (fn ds => |
|
1306 if Defstab.defined ds defs |
|
1307 then (Defines [], ds) |
|
1308 else (e, Defstab.update (defs, ()) ds)) |
|
1309 | e => (fn ds => (e, ds))) es ds; |
|
1310 fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds) |
|
1311 | rem_dup_elemss (Ext e) ds = (Ext e, ds); |
|
1312 fun rem_dup_defines raw_elemss = |
|
1313 fold_map (fn (id as (_, (Assumed _)), es) => (fn ds => |
|
1314 apfst (pair id) (rem_dup_elemss es ds)) |
|
1315 | (id as (_, (Derived _)), es) => (fn ds => |
|
1316 ((id, es), ds))) raw_elemss Defstab.empty |> #1; |
|
1317 |
|
1318 (* CB: type inference and consistency checks for locales. |
|
1319 |
|
1320 Works by building a context (through declare_elemss), extracting the |
|
1321 required information and adjusting the context elements (finish_elemss). |
|
1322 Can also universally close free vars in assms and defs. This is only |
|
1323 needed for Ext elements and controlled by parameter do_close. |
|
1324 |
|
1325 Only elements of assumed identifiers are considered. |
|
1326 *) |
|
1327 |
|
1328 fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl = |
|
1329 let |
|
1330 (* CB: contexts computed in the course of this function are discarded. |
|
1331 They are used for type inference and consistency checks only. *) |
|
1332 (* CB: fixed_params are the parameters (with types) of the target locale, |
|
1333 empty list if there is no target. *) |
|
1334 (* CB: raw_elemss are list of pairs consisting of identifiers and |
|
1335 context elements, the latter marked as internal or external. *) |
|
1336 val raw_elemss = rem_dup_defines raw_elemss; |
|
1337 val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context; |
|
1338 (* CB: raw_ctxt is context with additional fixed variables derived from |
|
1339 the fixes elements in raw_elemss, |
|
1340 raw_proppss contains assumptions and definitions from the |
|
1341 external elements in raw_elemss. *) |
|
1342 fun prep_prop raw_propp (raw_ctxt, raw_concl) = |
|
1343 let |
|
1344 (* CB: add type information from fixed_params to context (declare_term) *) |
|
1345 (* CB: process patterns (conclusion and external elements only) *) |
|
1346 val (ctxt, all_propp) = |
|
1347 prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); |
|
1348 (* CB: add type information from conclusion and external elements to context *) |
|
1349 val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt; |
|
1350 (* CB: resolve schematic variables (patterns) in conclusion and external elements. *) |
|
1351 val all_propp' = map2 (curry (op ~~)) |
|
1352 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); |
|
1353 val (concl, propp) = chop (length raw_concl) all_propp'; |
|
1354 in (propp, (ctxt, concl)) end |
|
1355 |
|
1356 val (proppss, (ctxt, concl)) = |
|
1357 (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl); |
|
1358 |
|
1359 (* CB: obtain all parameters from identifier part of raw_elemss *) |
|
1360 val xs = map #1 (params_of' raw_elemss); |
|
1361 val typing = unify_frozen ctxt 0 |
|
1362 (map (Variable.default_type raw_ctxt) xs) |
|
1363 (map (Variable.default_type ctxt) xs); |
|
1364 val parms = param_types (xs ~~ typing); |
|
1365 (* CB: parms are the parameters from raw_elemss, with correct typing. *) |
|
1366 |
|
1367 (* CB: extract information from assumes and defines elements |
|
1368 (fixes, constrains and notes in raw_elemss don't have an effect on |
|
1369 text and elemss), compute final form of context elements. *) |
|
1370 val ((text, _), elemss) = finish_elemss ctxt parms do_close |
|
1371 ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss); |
|
1372 (* CB: text has the following structure: |
|
1373 (((exts, exts'), (ints, ints')), (xs, env, defs)) |
|
1374 where |
|
1375 exts: external assumptions (terms in external assumes elements) |
|
1376 exts': dito, normalised wrt. env |
|
1377 ints: internal assumptions (terms in internal assumes elements) |
|
1378 ints': dito, normalised wrt. env |
|
1379 xs: the free variables in exts' and ints' and rhss of definitions, |
|
1380 this includes parameters except defined parameters |
|
1381 env: list of term pairs encoding substitutions, where the first term |
|
1382 is a free variable; substitutions represent defines elements and |
|
1383 the rhs is normalised wrt. the previous env |
|
1384 defs: theorems representing the substitutions from defines elements |
|
1385 (thms are normalised wrt. env). |
|
1386 elemss is an updated version of raw_elemss: |
|
1387 - type info added to Fixes and modified in Constrains |
|
1388 - axiom and definition statement replaced by corresponding one |
|
1389 from proppss in Assumes and Defines |
|
1390 - Facts unchanged |
|
1391 *) |
|
1392 in ((parms, elemss, concl), text) end; |
|
1393 |
|
1394 in |
|
1395 |
|
1396 fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x; |
|
1397 fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x; |
|
1398 |
|
1399 end; |
|
1400 |
|
1401 |
|
1402 (* facts and attributes *) |
|
1403 |
|
1404 local |
|
1405 |
|
1406 fun check_name name = |
|
1407 if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) |
|
1408 else name; |
|
1409 |
|
1410 fun prep_facts _ _ _ ctxt (Int elem) = elem |
|
1411 |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt))) |
|
1412 | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt |
|
1413 {var = I, typ = I, term = I, |
|
1414 binding = Binding.map_base prep_name, |
|
1415 fact = get ctxt, |
|
1416 attrib = Args.assignable o intern (ProofContext.theory_of ctxt)}; |
|
1417 |
|
1418 in |
|
1419 |
|
1420 fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x; |
|
1421 fun cert_facts x = prep_facts I (K I) (K I) x; |
|
1422 |
|
1423 end; |
|
1424 |
|
1425 |
|
1426 (* Get the specification of a locale *) |
|
1427 |
|
1428 (*The global specification is made from the parameters and global |
|
1429 assumptions, the local specification from the parameters and the |
|
1430 local assumptions.*) |
|
1431 |
|
1432 local |
|
1433 |
|
1434 fun gen_asms_of get thy name = |
|
1435 let |
|
1436 val ctxt = ProofContext.init thy; |
|
1437 val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name)); |
|
1438 val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss []; |
|
1439 in |
|
1440 elemss |> get |
|
1441 |> maps (fn (_, es) => map (fn Int e => e) es) |
|
1442 |> maps (fn Assumes asms => asms | _ => []) |
|
1443 |> map (apsnd (map fst)) |
|
1444 end; |
|
1445 |
|
1446 in |
|
1447 |
|
1448 fun parameters_of thy = #params o the_locale thy; |
|
1449 |
|
1450 fun intros thy = #intros o the_locale thy; |
|
1451 (*returns introduction rule for delta predicate and locale predicate |
|
1452 as a pair of singleton lists*) |
|
1453 |
|
1454 fun dests thy = #dests o the_locale thy; |
|
1455 |
|
1456 fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts |
|
1457 | _ => NONE) o #elems o the_locale thy; |
|
1458 |
|
1459 fun parameters_of_expr thy expr = |
|
1460 let |
|
1461 val ctxt = ProofContext.init thy; |
|
1462 val pts = params_of_expr ctxt [] (intern_expr thy expr) |
|
1463 ([], Symtab.empty, Symtab.empty); |
|
1464 val raw_params_elemss = make_raw_params_elemss pts; |
|
1465 val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy) |
|
1466 (([], Symtab.empty), Expr expr); |
|
1467 val ((parms, _, _), _) = |
|
1468 read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) []; |
|
1469 in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end; |
|
1470 |
|
1471 fun local_asms_of thy name = |
|
1472 gen_asms_of (single o Library.last_elem) thy name; |
|
1473 |
|
1474 fun global_asms_of thy name = |
|
1475 gen_asms_of I thy name; |
|
1476 |
|
1477 end; |
|
1478 |
|
1479 |
|
1480 (* full context statements: imports + elements + conclusion *) |
|
1481 |
|
1482 local |
|
1483 |
|
1484 fun prep_context_statement prep_expr prep_elemss prep_facts |
|
1485 do_close fixed_params imports elements raw_concl context = |
|
1486 let |
|
1487 val thy = ProofContext.theory_of context; |
|
1488 |
|
1489 val (import_params, import_tenv, import_syn) = |
|
1490 params_of_expr context fixed_params (prep_expr thy imports) |
|
1491 ([], Symtab.empty, Symtab.empty); |
|
1492 val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements; |
|
1493 val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params) |
|
1494 (map (prep_expr thy) includes) (import_params, import_tenv, import_syn); |
|
1495 |
|
1496 val ((import_ids, _), raw_import_elemss) = |
|
1497 flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports); |
|
1498 (* CB: normalise "includes" among elements *) |
|
1499 val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy)) |
|
1500 ((import_ids, incl_syn), elements); |
|
1501 |
|
1502 val raw_elemss = flat raw_elemsss; |
|
1503 (* CB: raw_import_elemss @ raw_elemss is the normalised list of |
|
1504 context elements obtained from import and elements. *) |
|
1505 (* Now additional elements for parameters are inserted. *) |
|
1506 val import_params_ids = make_params_ids import_params; |
|
1507 val incl_params_ids = |
|
1508 make_params_ids (incl_params \\ import_params); |
|
1509 val raw_import_params_elemss = |
|
1510 make_raw_params_elemss (import_params, incl_tenv, incl_syn); |
|
1511 val raw_incl_params_elemss = |
|
1512 make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn); |
|
1513 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close |
|
1514 context fixed_params |
|
1515 (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl; |
|
1516 |
|
1517 (* replace extended ids (for axioms) by ids *) |
|
1518 val (import_ids', incl_ids) = chop (length import_ids) ids; |
|
1519 val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids; |
|
1520 val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) => |
|
1521 (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems)) |
|
1522 (all_ids ~~ all_elemss); |
|
1523 (* CB: all_elemss and parms contain the correct parameter types *) |
|
1524 |
|
1525 val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss'; |
|
1526 val ((import_elemss, _), import_ctxt) = |
|
1527 activate_facts false prep_facts ps context; |
|
1528 |
|
1529 val ((elemss, _), ctxt) = |
|
1530 activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt); |
|
1531 in |
|
1532 ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), |
|
1533 (parms, spec, defs)), concl) |
|
1534 end; |
|
1535 |
|
1536 fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt = |
|
1537 let |
|
1538 val thy = ProofContext.theory_of ctxt; |
|
1539 val locale = Option.map (prep_locale thy) raw_locale; |
|
1540 val (fixed_params, imports) = |
|
1541 (case locale of |
|
1542 NONE => ([], empty) |
|
1543 | SOME name => |
|
1544 let val {params = ps, ...} = the_locale thy name |
|
1545 in (map fst ps, Locale name) end); |
|
1546 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') = |
|
1547 prep_ctxt false fixed_params imports (map Elem elems) concl ctxt; |
|
1548 in (locale, locale_ctxt, elems_ctxt, concl') end; |
|
1549 |
|
1550 fun prep_expr prep imports body ctxt = |
|
1551 let |
|
1552 val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt; |
|
1553 val all_elems = maps snd (import_elemss @ elemss); |
|
1554 in (all_elems, ctxt') end; |
|
1555 |
|
1556 in |
|
1557 |
|
1558 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts; |
|
1559 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts; |
|
1560 |
|
1561 fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt); |
|
1562 fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt); |
|
1563 |
|
1564 val read_expr = prep_expr read_context; |
|
1565 val cert_expr = prep_expr cert_context; |
|
1566 |
|
1567 fun read_context_statement loc = prep_statement (K I) read_ctxt loc; |
|
1568 fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc; |
|
1569 fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc; |
|
1570 |
|
1571 end; |
|
1572 |
|
1573 |
|
1574 (* init *) |
|
1575 |
|
1576 fun init loc = |
|
1577 ProofContext.init |
|
1578 #> #2 o cert_context_statement (SOME loc) [] []; |
|
1579 |
|
1580 |
|
1581 (* print locale *) |
|
1582 |
|
1583 fun print_locale thy show_facts imports body = |
|
1584 let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in |
|
1585 Pretty.big_list "locale elements:" (all_elems |
|
1586 |> (if show_facts then I else filter (fn Notes _ => false | _ => true)) |
|
1587 |> map (Element.pretty_ctxt ctxt) |> filter_out null |
|
1588 |> map Pretty.chunks) |
|
1589 |> Pretty.writeln |
|
1590 end; |
|
1591 |
|
1592 |
|
1593 |
|
1594 (** store results **) |
|
1595 |
|
1596 (* join equations of an id with already accumulated ones *) |
|
1597 |
|
1598 fun join_eqns get_reg id eqns = |
|
1599 let |
|
1600 val eqns' = case get_reg id |
|
1601 of NONE => eqns |
|
1602 | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns') |
|
1603 (* prefer equations from eqns' *) |
|
1604 in ((id, eqns'), eqns') end; |
|
1605 |
|
1606 |
|
1607 (* collect witnesses and equations up to a particular target for a |
|
1608 registration; requires parameters and flattened list of identifiers |
|
1609 instead of recomputing it from the target *) |
|
1610 |
|
1611 fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let |
|
1612 |
|
1613 val thy = ProofContext.theory_of ctxt; |
|
1614 |
|
1615 val ts = map (var_inst_term (impT, imp)) ext_ts; |
|
1616 val (parms, parmTs) = split_list parms; |
|
1617 val parmvTs = map Logic.varifyT parmTs; |
|
1618 val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty; |
|
1619 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T)) |
|
1620 |> Symtab.make; |
|
1621 val inst = Symtab.make (parms ~~ ts); |
|
1622 |
|
1623 (* instantiate parameter names in ids *) |
|
1624 val ext_inst = Symtab.make (parms ~~ ext_ts); |
|
1625 fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps; |
|
1626 val inst_ids = map (apfst (apsnd ext_inst_names)) ids; |
|
1627 val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids; |
|
1628 val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids; |
|
1629 val eqns = |
|
1630 fold_map (join_eqns (get_local_registration ctxt imprt)) |
|
1631 (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd; |
|
1632 in ((tinst, inst), wits, eqns) end; |
|
1633 |
|
1634 |
|
1635 (* compute and apply morphism *) |
|
1636 |
|
1637 fun name_morph phi_name (lprfx, pprfx) b = |
|
1638 b |
|
1639 |> (if not (Binding.is_empty b) andalso pprfx <> "" |
|
1640 then Binding.add_prefix false pprfx else I) |
|
1641 |> (if not (Binding.is_empty b) |
|
1642 then Binding.add_prefix false lprfx else I) |
|
1643 |> phi_name; |
|
1644 |
|
1645 fun inst_morph thy phi_name param_prfx insts prems eqns export = |
|
1646 let |
|
1647 (* standardise export morphism *) |
|
1648 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
|
1649 val exp_term = TermSubst.zero_var_indexes o Morphism.term export; |
|
1650 (* FIXME sync with exp_fact *) |
|
1651 val exp_typ = Logic.type_map exp_term; |
|
1652 val export' = |
|
1653 Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
|
1654 in |
|
1655 Morphism.binding_morphism (name_morph phi_name param_prfx) $> |
|
1656 Element.inst_morphism thy insts $> |
|
1657 Element.satisfy_morphism prems $> |
|
1658 Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> |
|
1659 Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $> |
|
1660 export' |
|
1661 end; |
|
1662 |
|
1663 fun activate_note thy phi_name param_prfx attrib insts prems eqns exp = |
|
1664 (Element.facts_map o Element.morph_ctxt) |
|
1665 (inst_morph thy phi_name param_prfx insts prems eqns exp) |
|
1666 #> Attrib.map_facts attrib; |
|
1667 |
|
1668 |
|
1669 (* public interface to interpretation morphism *) |
|
1670 |
|
1671 fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts = |
|
1672 let |
|
1673 val parms = the_locale thy target |> #params |> map fst; |
|
1674 val ids = flatten (ProofContext.init thy, intern_expr thy) |
|
1675 (([], Symtab.empty), Expr (Locale target)) |> fst |> fst; |
|
1676 val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; |
|
1677 in |
|
1678 inst_morph thy phi_name param_prfx insts prems eqns exp |
|
1679 end; |
|
1680 |
|
1681 (* store instantiations of args for all registered interpretations |
|
1682 of the theory *) |
|
1683 |
|
1684 fun note_thmss_registrations target (kind, args) thy = |
|
1685 let |
|
1686 val parms = the_locale thy target |> #params |> map fst; |
|
1687 val ids = flatten (ProofContext.init thy, intern_expr thy) |
|
1688 (([], Symtab.empty), Expr (Locale target)) |> fst |> fst; |
|
1689 |
|
1690 val regs = get_global_registrations thy target; |
|
1691 (* add args to thy for all registrations *) |
|
1692 |
|
1693 fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy = |
|
1694 let |
|
1695 val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; |
|
1696 val args' = args |
|
1697 |> activate_note thy phi_name param_prfx |
|
1698 (Attrib.attribute_i thy) insts prems eqns exp; |
|
1699 in |
|
1700 thy |
|
1701 |> global_note_qualified kind args' |
|
1702 |> snd |
|
1703 end; |
|
1704 in fold activate regs thy end; |
|
1705 |
|
1706 |
|
1707 (* locale results *) |
|
1708 |
|
1709 fun add_thmss loc kind args ctxt = |
|
1710 let |
|
1711 val (([(_, [Notes args'])], _), ctxt') = |
|
1712 activate_facts true cert_facts |
|
1713 [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt; |
|
1714 val ctxt'' = ctxt' |> ProofContext.theory |
|
1715 (change_locale loc |
|
1716 (fn (axiom, elems, params, decls, regs, intros, dests) => |
|
1717 (axiom, elems @ [(Notes args', stamp ())], |
|
1718 params, decls, regs, intros, dests)) |
|
1719 #> note_thmss_registrations loc args'); |
|
1720 in ctxt'' end; |
|
1721 |
|
1722 |
|
1723 (* declarations *) |
|
1724 |
|
1725 local |
|
1726 |
|
1727 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi)); |
|
1728 |
|
1729 fun add_decls add loc decl = |
|
1730 ProofContext.theory (change_locale loc |
|
1731 (fn (axiom, elems, params, decls, regs, intros, dests) => |
|
1732 (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #> |
|
1733 add_thmss loc Thm.internalK |
|
1734 [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])]; |
|
1735 |
|
1736 in |
|
1737 |
|
1738 val add_type_syntax = add_decls (apfst o cons); |
|
1739 val add_term_syntax = add_decls (apsnd o cons); |
|
1740 val add_declaration = add_decls (K I); |
|
1741 |
|
1742 fun declarations_of thy loc = |
|
1743 the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst); |
|
1744 |
|
1745 end; |
|
1746 |
|
1747 |
|
1748 |
|
1749 (** define locales **) |
|
1750 |
|
1751 (* predicate text *) |
|
1752 (* CB: generate locale predicates and delta predicates *) |
|
1753 |
|
1754 local |
|
1755 |
|
1756 (* introN: name of theorems for introduction rules of locale and |
|
1757 delta predicates; |
|
1758 axiomsN: name of theorem set with destruct rules for locale predicates, |
|
1759 also name suffix of delta predicates. *) |
|
1760 |
|
1761 val introN = "intro"; |
|
1762 val axiomsN = "axioms"; |
|
1763 |
|
1764 fun atomize_spec thy ts = |
|
1765 let |
|
1766 val t = Logic.mk_conjunction_balanced ts; |
|
1767 val body = ObjectLogic.atomize_term thy t; |
|
1768 val bodyT = Term.fastype_of body; |
|
1769 in |
|
1770 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) |
|
1771 else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t)) |
|
1772 end; |
|
1773 |
|
1774 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => |
|
1775 if length args = n then |
|
1776 Syntax.const "_aprop" $ |
|
1777 Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) |
|
1778 else raise Match); |
|
1779 |
|
1780 (* CB: define one predicate including its intro rule and axioms |
|
1781 - bname: predicate name |
|
1782 - parms: locale parameters |
|
1783 - defs: thms representing substitutions from defines elements |
|
1784 - ts: terms representing locale assumptions (not normalised wrt. defs) |
|
1785 - norm_ts: terms representing locale assumptions (normalised wrt. defs) |
|
1786 - thy: the theory |
|
1787 *) |
|
1788 |
|
1789 fun def_pred bname parms defs ts norm_ts thy = |
|
1790 let |
|
1791 val name = Sign.full_bname thy bname; |
|
1792 |
|
1793 val (body, bodyT, body_eq) = atomize_spec thy norm_ts; |
|
1794 val env = Term.add_free_names body []; |
|
1795 val xs = filter (member (op =) env o #1) parms; |
|
1796 val Ts = map #2 xs; |
|
1797 val extraTs = |
|
1798 (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts []) |
|
1799 |> Library.sort_wrt #1 |> map TFree; |
|
1800 val predT = map Term.itselfT extraTs ---> Ts ---> bodyT; |
|
1801 |
|
1802 val args = map Logic.mk_type extraTs @ map Free xs; |
|
1803 val head = Term.list_comb (Const (name, predT), args); |
|
1804 val statement = ObjectLogic.ensure_propT thy head; |
|
1805 |
|
1806 val ([pred_def], defs_thy) = |
|
1807 thy |
|
1808 |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |
|
1809 |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd |
|
1810 |> PureThy.add_defs false |
|
1811 [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; |
|
1812 val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; |
|
1813 |
|
1814 val cert = Thm.cterm_of defs_thy; |
|
1815 |
|
1816 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => |
|
1817 MetaSimplifier.rewrite_goals_tac [pred_def] THEN |
|
1818 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
|
1819 Tactic.compose_tac (false, |
|
1820 Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); |
|
1821 |
|
1822 val conjuncts = |
|
1823 (Drule.equal_elim_rule2 OF [body_eq, |
|
1824 MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
|
1825 |> Conjunction.elim_balanced (length ts); |
|
1826 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
|
1827 Element.prove_witness defs_ctxt t |
|
1828 (MetaSimplifier.rewrite_goals_tac defs THEN |
|
1829 Tactic.compose_tac (false, ax, 0) 1)); |
|
1830 in ((statement, intro, axioms), defs_thy) end; |
|
1831 |
|
1832 fun assumes_to_notes (Assumes asms) axms = |
|
1833 fold_map (fn (a, spec) => fn axs => |
|
1834 let val (ps, qs) = chop (length spec) axs |
|
1835 in ((a, [(ps, [])]), qs) end) asms axms |
|
1836 |> apfst (curry Notes Thm.assumptionK) |
|
1837 | assumes_to_notes e axms = (e, axms); |
|
1838 |
|
1839 (* CB: the following two change only "new" elems, these have identifier ("", _). *) |
|
1840 |
|
1841 (* turn Assumes into Notes elements *) |
|
1842 |
|
1843 fun change_assumes_elemss axioms elemss = |
|
1844 let |
|
1845 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms); |
|
1846 fun change (id as ("", _), es) = |
|
1847 fold_map assumes_to_notes (map satisfy es) |
|
1848 #-> (fn es' => pair (id, es')) |
|
1849 | change e = pair e; |
|
1850 in |
|
1851 fst (fold_map change elemss (map Element.conclude_witness axioms)) |
|
1852 end; |
|
1853 |
|
1854 (* adjust hyps of Notes elements *) |
|
1855 |
|
1856 fun change_elemss_hyps axioms elemss = |
|
1857 let |
|
1858 val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms); |
|
1859 fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es) |
|
1860 | change e = e; |
|
1861 in map change elemss end; |
|
1862 |
|
1863 in |
|
1864 |
|
1865 (* CB: main predicate definition function *) |
|
1866 |
|
1867 fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy = |
|
1868 let |
|
1869 val ((elemss', more_ts), a_elem, a_intro, thy'') = |
|
1870 if null exts then ((elemss, []), [], [], thy) |
|
1871 else |
|
1872 let |
|
1873 val aname = if null ints then pname else pname ^ "_" ^ axiomsN; |
|
1874 val ((statement, intro, axioms), thy') = |
|
1875 thy |
|
1876 |> def_pred aname parms defs exts exts'; |
|
1877 val elemss' = change_assumes_elemss axioms elemss; |
|
1878 val a_elem = [(("", []), |
|
1879 [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])]; |
|
1880 val (_, thy'') = |
|
1881 thy' |
|
1882 |> Sign.add_path aname |
|
1883 |> Sign.no_base_names |
|
1884 |> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])] |
|
1885 ||> Sign.restore_naming thy'; |
|
1886 in ((elemss', [statement]), a_elem, [intro], thy'') end; |
|
1887 val (predicate, stmt', elemss'', b_intro, thy'''') = |
|
1888 if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'') |
|
1889 else |
|
1890 let |
|
1891 val ((statement, intro, axioms), thy''') = |
|
1892 thy'' |
|
1893 |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts); |
|
1894 val cstatement = Thm.cterm_of thy''' statement; |
|
1895 val elemss'' = change_elemss_hyps axioms elemss'; |
|
1896 val b_elem = [(("", []), |
|
1897 [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])]; |
|
1898 val (_, thy'''') = |
|
1899 thy''' |
|
1900 |> Sign.add_path pname |
|
1901 |> Sign.no_base_names |
|
1902 |> PureThy.note_thmss Thm.internalK |
|
1903 [((Binding.name introN, []), [([intro], [])]), |
|
1904 ((Binding.name axiomsN, []), |
|
1905 [(map (Drule.standard o Element.conclude_witness) axioms, [])])] |
|
1906 ||> Sign.restore_naming thy'''; |
|
1907 in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end; |
|
1908 in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end; |
|
1909 |
|
1910 end; |
|
1911 |
|
1912 |
|
1913 (* add_locale(_i) *) |
|
1914 |
|
1915 local |
|
1916 |
|
1917 (* turn Defines into Notes elements, accumulate definition terms *) |
|
1918 |
|
1919 fun defines_to_notes is_ext thy (Defines defs) defns = |
|
1920 let |
|
1921 val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs |
|
1922 val notes = map (fn (a, (def, _)) => |
|
1923 (a, [([assume (cterm_of thy def)], [])])) defs |
|
1924 in |
|
1925 (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs']) |
|
1926 end |
|
1927 | defines_to_notes _ _ e defns = (SOME e, defns); |
|
1928 |
|
1929 fun change_defines_elemss thy elemss defns = |
|
1930 let |
|
1931 fun change (id as (n, _), es) defns = |
|
1932 let |
|
1933 val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns |
|
1934 in ((id, map_filter I es'), defns') end |
|
1935 in fold_map change elemss defns end; |
|
1936 |
|
1937 fun gen_add_locale prep_ctxt prep_expr |
|
1938 predicate_name bname raw_imports raw_body thy = |
|
1939 (* predicate_name: "" - locale with predicate named as locale |
|
1940 "name" - locale with predicate named "name" *) |
|
1941 let |
|
1942 val thy_ctxt = ProofContext.init thy; |
|
1943 val name = Sign.full_bname thy bname; |
|
1944 val _ = is_some (get_locale thy name) andalso |
|
1945 error ("Duplicate definition of locale " ^ quote name); |
|
1946 |
|
1947 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), |
|
1948 text as (parms, ((_, exts'), _), defs)) = |
|
1949 prep_ctxt raw_imports raw_body thy_ctxt; |
|
1950 val elemss = import_elemss @ body_elemss |> |
|
1951 map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE); |
|
1952 |
|
1953 val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\ |
|
1954 List.foldr OldTerm.add_typ_tfrees [] (map snd parms); |
|
1955 val _ = if null extraTs then () |
|
1956 else warning ("Additional type variable(s) in locale specification " ^ quote bname); |
|
1957 |
|
1958 val predicate_name' = case predicate_name of "" => bname | _ => predicate_name; |
|
1959 val (elemss', defns) = change_defines_elemss thy elemss []; |
|
1960 val elemss'' = elemss' @ [(("", []), defns)]; |
|
1961 val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') = |
|
1962 define_preds predicate_name' text elemss'' thy; |
|
1963 val regs = pred_axioms |
|
1964 |> fold_map (fn (id, elems) => fn wts => let |
|
1965 val ts = flat (map_filter (fn (Assumes asms) => |
|
1966 SOME (maps (map #1 o #2) asms) | _ => NONE) elems); |
|
1967 val (wts1, wts2) = chop (length ts) wts; |
|
1968 in ((apsnd (map fst) id, wts1), wts2) end) elemss''' |
|
1969 |> fst |
|
1970 |> map_filter (fn (("", _), _) => NONE | e => SOME e); |
|
1971 fun axiomify axioms elemss = |
|
1972 (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let |
|
1973 val ts = flat (map_filter (fn (Assumes asms) => |
|
1974 SOME (maps (map #1 o #2) asms) | _ => NONE) elems); |
|
1975 val (axs1, axs2) = chop (length ts) axs; |
|
1976 in (axs2, ((id, Assumed axs1), elems)) end) |
|
1977 |> snd; |
|
1978 val ((_, facts), ctxt) = activate_facts true (K I) |
|
1979 (axiomify pred_axioms elemss''') (ProofContext.init thy'); |
|
1980 val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt; |
|
1981 val export = Thm.close_derivation o Goal.norm_result o |
|
1982 singleton (ProofContext.export view_ctxt thy_ctxt); |
|
1983 val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); |
|
1984 val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss'''); |
|
1985 val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems'; |
|
1986 val axs' = map (Element.assume_witness thy') stmt'; |
|
1987 val loc_ctxt = thy' |
|
1988 |> Sign.add_path bname |
|
1989 |> Sign.no_base_names |
|
1990 |> PureThy.note_thmss Thm.assumptionK facts' |> snd |
|
1991 |> Sign.restore_naming thy' |
|
1992 |> register_locale bname {axiom = axs', |
|
1993 elems = map (fn e => (e, stamp ())) elems'', |
|
1994 params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), |
|
1995 decls = ([], []), |
|
1996 regs = regs, |
|
1997 intros = intros, |
|
1998 dests = map Element.conclude_witness pred_axioms} |
|
1999 |> init name; |
|
2000 in (name, loc_ctxt) end; |
|
2001 |
|
2002 in |
|
2003 |
|
2004 val add_locale = gen_add_locale cert_context (K I); |
|
2005 val add_locale_cmd = gen_add_locale read_context intern_expr ""; |
|
2006 |
|
2007 end; |
|
2008 |
|
2009 val _ = Context.>> (Context.map_theory |
|
2010 (add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #> |
|
2011 snd #> ProofContext.theory_of #> |
|
2012 add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #> |
|
2013 snd #> ProofContext.theory_of)); |
|
2014 |
|
2015 |
|
2016 |
|
2017 |
|
2018 (** Normalisation of locale statements --- |
|
2019 discharges goals implied by interpretations **) |
|
2020 |
|
2021 local |
|
2022 |
|
2023 fun locale_assm_intros thy = |
|
2024 Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros)) |
|
2025 (#2 (LocalesData.get thy)) []; |
|
2026 fun locale_base_intros thy = |
|
2027 Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros)) |
|
2028 (#2 (LocalesData.get thy)) []; |
|
2029 |
|
2030 fun all_witnesses ctxt = |
|
2031 let |
|
2032 val thy = ProofContext.theory_of ctxt; |
|
2033 fun get registrations = Symtab.fold (fn (_, regs) => fn thms => |
|
2034 (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) => |
|
2035 map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms) |
|
2036 registrations []; |
|
2037 in get (RegistrationsData.get (Context.Proof ctxt)) end; |
|
2038 |
|
2039 in |
|
2040 |
|
2041 fun intro_locales_tac eager ctxt facts st = |
|
2042 let |
|
2043 val wits = all_witnesses ctxt; |
|
2044 val thy = ProofContext.theory_of ctxt; |
|
2045 val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []); |
|
2046 in |
|
2047 Method.intros_tac (wits @ intros) facts st |
|
2048 end; |
|
2049 |
|
2050 end; |
|
2051 |
|
2052 |
|
2053 (** Interpretation commands **) |
|
2054 |
|
2055 local |
|
2056 |
|
2057 (* extract proof obligations (assms and defs) from elements *) |
|
2058 |
|
2059 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems) |
|
2060 | extract_asms_elems ((id, Derived _), _) = (id, []); |
|
2061 |
|
2062 |
|
2063 (* activate instantiated facts in theory or context *) |
|
2064 |
|
2065 fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn |
|
2066 phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt = |
|
2067 let |
|
2068 val ctxt = mk_ctxt thy_ctxt; |
|
2069 fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt); |
|
2070 fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt); |
|
2071 |
|
2072 val (all_propss, eq_props) = chop (length all_elemss) propss; |
|
2073 val (all_thmss, eq_thms) = chop (length all_elemss) thmss; |
|
2074 |
|
2075 (* Filter out fragments already registered. *) |
|
2076 |
|
2077 val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) => |
|
2078 test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss)))); |
|
2079 val (new_pss, ys) = split_list xs; |
|
2080 val (new_propss, new_thmss) = split_list ys; |
|
2081 |
|
2082 val thy_ctxt' = thy_ctxt |
|
2083 (* add registrations *) |
|
2084 |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp)) |
|
2085 new_elemss new_pss |
|
2086 (* add witnesses of Assumed elements (only those generate proof obligations) *) |
|
2087 |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss |
|
2088 (* add equations *) |
|
2089 |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props |
|
2090 ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o |
|
2091 Element.conclude_witness) eq_thms); |
|
2092 |
|
2093 val prems = flat (map_filter |
|
2094 (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) |
|
2095 | ((_, Derived _), _) => NONE) all_elemss); |
|
2096 |
|
2097 val thy_ctxt'' = thy_ctxt' |
|
2098 (* add witnesses of Derived elements *) |
|
2099 |> fold (fn (id, thms) => fold |
|
2100 (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms) |
|
2101 (map_filter (fn ((_, Assumed _), _) => NONE |
|
2102 | ((id, Derived thms), _) => SOME (id, thms)) new_elemss) |
|
2103 |
|
2104 fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt = |
|
2105 let |
|
2106 val ctxt = mk_ctxt thy_ctxt; |
|
2107 val thy = ProofContext.theory_of ctxt; |
|
2108 val facts' = facts |
|
2109 |> activate_note thy phi_name param_prfx |
|
2110 (attrib thy_ctxt) insts prems eqns exp; |
|
2111 in |
|
2112 thy_ctxt |
|
2113 |> note kind facts' |
|
2114 |> snd |
|
2115 end |
|
2116 | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt; |
|
2117 |
|
2118 fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt = |
|
2119 let |
|
2120 val ctxt = mk_ctxt thy_ctxt; |
|
2121 val thy = ProofContext.theory_of ctxt; |
|
2122 val {params, elems, ...} = the_locale thy loc; |
|
2123 val parms = map fst params; |
|
2124 val param_prfx = param_prefix loc ps; |
|
2125 val ids = flatten (ProofContext.init thy, intern_expr thy) |
|
2126 (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst; |
|
2127 val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts; |
|
2128 in |
|
2129 thy_ctxt |
|
2130 |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems |
|
2131 end; |
|
2132 |
|
2133 in |
|
2134 thy_ctxt'' |
|
2135 (* add equations as lemmas to context *) |
|
2136 |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK) |
|
2137 ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])])) |
|
2138 (unflat eq_thms eq_attns) eq_thms |
|
2139 (* add interpreted facts *) |
|
2140 |> fold2 activate_elems new_elemss new_pss |
|
2141 end; |
|
2142 |
|
2143 fun global_activate_facts_elemss x = gen_activate_facts_elemss |
|
2144 ProofContext.init |
|
2145 global_note_qualified |
|
2146 Attrib.attribute_i |
|
2147 put_global_registration |
|
2148 add_global_witness |
|
2149 add_global_equation |
|
2150 x; |
|
2151 |
|
2152 fun local_activate_facts_elemss x = gen_activate_facts_elemss |
|
2153 I |
|
2154 local_note_qualified |
|
2155 (Attrib.attribute_i o ProofContext.theory_of) |
|
2156 put_local_registration |
|
2157 add_local_witness |
|
2158 add_local_equation |
|
2159 x; |
|
2160 |
|
2161 fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) = |
|
2162 let |
|
2163 (* parameters *) |
|
2164 val (parm_names, parm_types) = parms |> split_list |
|
2165 ||> map (TypeInfer.paramify_vars o Logic.varifyT); |
|
2166 val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar); |
|
2167 val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst; |
|
2168 |
|
2169 (* parameter instantiations *) |
|
2170 val d = length parms - length insts; |
|
2171 val insts = |
|
2172 if d < 0 then error "More arguments than parameters in instantiation." |
|
2173 else insts @ replicate d NONE; |
|
2174 val (given_ps, given_insts) = |
|
2175 ((parm_names ~~ parm_types) ~~ insts) |> map_filter |
|
2176 (fn (_, NONE) => NONE |
|
2177 | ((n, T), SOME inst) => SOME ((n, T), inst)) |
|
2178 |> split_list; |
|
2179 val (given_parm_names, given_parm_types) = given_ps |> split_list; |
|
2180 |
|
2181 (* parse insts / eqns *) |
|
2182 val given_insts' = map (parse_term ctxt) given_insts; |
|
2183 val eqns' = map (parse_prop ctxt) eqns; |
|
2184 |
|
2185 (* type inference and contexts *) |
|
2186 val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns'; |
|
2187 val res = Syntax.check_terms ctxt arg; |
|
2188 val ctxt' = ctxt |> fold Variable.auto_fixes res; |
|
2189 |
|
2190 (* instantiation *) |
|
2191 val (type_parms'', res') = chop (length type_parms) res; |
|
2192 val (given_insts'', eqns'') = chop (length given_insts) res'; |
|
2193 val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); |
|
2194 val inst = Symtab.make (given_parm_names ~~ given_insts''); |
|
2195 |
|
2196 (* export from eigencontext *) |
|
2197 val export = Variable.export_morphism ctxt' ctxt; |
|
2198 |
|
2199 (* import, its inverse *) |
|
2200 val domT = fold Term.add_tfrees res [] |> map TFree; |
|
2201 val importT = domT |> map (fn x => (Morphism.typ export x, x)) |
|
2202 |> map_filter (fn (TFree _, _) => NONE (* fixed point of export *) |
|
2203 | (TVar y, x) => SOME (fst y, x) |
|
2204 | _ => error "internal: illegal export in interpretation") |
|
2205 |> Vartab.make; |
|
2206 val dom = fold Term.add_frees res [] |> map Free; |
|
2207 val imprt = dom |> map (fn x => (Morphism.term export x, x)) |
|
2208 |> map_filter (fn (Free _, _) => NONE (* fixed point of export *) |
|
2209 | (Var y, x) => SOME (fst y, x) |
|
2210 | _ => error "internal: illegal export in interpretation") |
|
2211 |> Vartab.make; |
|
2212 in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end; |
|
2213 |
|
2214 val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop; |
|
2215 val check_instantiations = prep_instantiations (K I) (K I); |
|
2216 |
|
2217 fun gen_prep_registration mk_ctxt test_reg activate |
|
2218 prep_attr prep_expr prep_insts |
|
2219 thy_ctxt phi_name raw_expr raw_insts = |
|
2220 let |
|
2221 val ctxt = mk_ctxt thy_ctxt; |
|
2222 val thy = ProofContext.theory_of ctxt; |
|
2223 val ctxt' = ProofContext.init thy; |
|
2224 fun prep_attn attn = (apsnd o map) |
|
2225 (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn; |
|
2226 |
|
2227 val expr = prep_expr thy raw_expr; |
|
2228 |
|
2229 val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty); |
|
2230 val params_ids = make_params_ids (#1 pts); |
|
2231 val raw_params_elemss = make_raw_params_elemss pts; |
|
2232 val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr); |
|
2233 val ((parms, all_elemss, _), (_, (_, defs, _))) = |
|
2234 read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) []; |
|
2235 |
|
2236 (** compute instantiation **) |
|
2237 |
|
2238 (* consistency check: equations need to be stored in a particular locale, |
|
2239 therefore if equations are present locale expression must be a name *) |
|
2240 |
|
2241 val _ = case (expr, snd raw_insts) of |
|
2242 (Locale _, _) => () | (_, []) => () |
|
2243 | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name."; |
|
2244 |
|
2245 (* read or certify instantiation *) |
|
2246 val (raw_insts', raw_eqns) = raw_insts; |
|
2247 val (raw_eq_attns, raw_eqns') = split_list raw_eqns; |
|
2248 val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns'); |
|
2249 val eq_attns = map prep_attn raw_eq_attns; |
|
2250 |
|
2251 (* defined params without given instantiation *) |
|
2252 val not_given = filter_out (Symtab.defined inst1 o fst) parms; |
|
2253 fun add_def (p, pT) inst = |
|
2254 let |
|
2255 val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of |
|
2256 NONE => error ("Instance missing for parameter " ^ quote p) |
|
2257 | SOME (Free (_, T), t) => (t, T); |
|
2258 val d = Element.inst_term (instT, inst) t; |
|
2259 in Symtab.update_new (p, d) inst end; |
|
2260 val inst2 = fold add_def not_given inst1; |
|
2261 val inst_morphism = Element.inst_morphism thy (instT, inst2); |
|
2262 (* Note: insts contain no vars. *) |
|
2263 |
|
2264 (** compute proof obligations **) |
|
2265 |
|
2266 (* restore "small" ids *) |
|
2267 val ids' = map (fn ((n, ps), (_, mode)) => |
|
2268 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) |
|
2269 ids; |
|
2270 val (_, all_elemss') = chop (length raw_params_elemss) all_elemss |
|
2271 (* instantiate ids and elements *) |
|
2272 val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) => |
|
2273 ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps), |
|
2274 map (fn Int e => Element.morph_ctxt inst_morphism e) elems) |
|
2275 |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode))); |
|
2276 |
|
2277 (* equations *) |
|
2278 val eqn_elems = if null eqns then [] |
|
2279 else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; |
|
2280 |
|
2281 val propss = map extract_asms_elems inst_elemss @ eqn_elems; |
|
2282 |
|
2283 in |
|
2284 (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs) |
|
2285 end; |
|
2286 |
|
2287 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init |
|
2288 test_global_registration |
|
2289 global_activate_facts_elemss mk_ctxt; |
|
2290 |
|
2291 fun gen_prep_local_registration mk_ctxt = gen_prep_registration I |
|
2292 test_local_registration |
|
2293 local_activate_facts_elemss mk_ctxt; |
|
2294 |
|
2295 val prep_global_registration = gen_prep_global_registration |
|
2296 (K I) (K I) check_instantiations; |
|
2297 val prep_global_registration_cmd = gen_prep_global_registration |
|
2298 Attrib.intern_src intern_expr read_instantiations; |
|
2299 |
|
2300 val prep_local_registration = gen_prep_local_registration |
|
2301 (K I) (K I) check_instantiations; |
|
2302 val prep_local_registration_cmd = gen_prep_local_registration |
|
2303 Attrib.intern_src intern_expr read_instantiations; |
|
2304 |
|
2305 fun prep_registration_in_locale target expr thy = |
|
2306 (* target already in internal form *) |
|
2307 let |
|
2308 val ctxt = ProofContext.init thy; |
|
2309 val ((raw_target_ids, target_syn), _) = flatten (ctxt, I) |
|
2310 (([], Symtab.empty), Expr (Locale target)); |
|
2311 val fixed = the_locale thy target |> #params |> map #1; |
|
2312 val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy) |
|
2313 ((raw_target_ids, target_syn), Expr expr); |
|
2314 val (target_ids, ids) = chop (length raw_target_ids) all_ids; |
|
2315 val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss []; |
|
2316 |
|
2317 (** compute proof obligations **) |
|
2318 |
|
2319 (* restore "small" ids, with mode *) |
|
2320 val ids' = map (apsnd snd) ids; |
|
2321 (* remove Int markers *) |
|
2322 val elemss' = map (fn (_, es) => |
|
2323 map (fn Int e => e) es) elemss |
|
2324 (* extract assumptions and defs *) |
|
2325 val ids_elemss = ids' ~~ elemss'; |
|
2326 val propss = map extract_asms_elems ids_elemss; |
|
2327 |
|
2328 (** activation function: |
|
2329 - add registrations to the target locale |
|
2330 - add induced registrations for all global registrations of |
|
2331 the target, unless already present |
|
2332 - add facts of induced registrations to theory **) |
|
2333 |
|
2334 fun activate thmss thy = |
|
2335 let |
|
2336 val satisfy = Element.satisfy_thm (flat thmss); |
|
2337 val ids_elemss_thmss = ids_elemss ~~ thmss; |
|
2338 val regs = get_global_registrations thy target; |
|
2339 |
|
2340 fun activate_id (((id, Assumed _), _), thms) thy = |
|
2341 thy |> put_registration_in_locale target id |
|
2342 |> fold (add_witness_in_locale target id) thms |
|
2343 | activate_id _ thy = thy; |
|
2344 |
|
2345 fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy = |
|
2346 let |
|
2347 val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts; |
|
2348 val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts)); |
|
2349 val disch = Element.satisfy_thm wits; |
|
2350 val new_elemss = filter (fn (((name, ps), _), _) => |
|
2351 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); |
|
2352 fun activate_assumed_id (((_, Derived _), _), _) thy = thy |
|
2353 | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let |
|
2354 val ps' = inst_parms ps; |
|
2355 in |
|
2356 if test_global_registration thy (name, ps') |
|
2357 then thy |
|
2358 else thy |
|
2359 |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp) |
|
2360 |> fold (fn witn => fn thy => add_global_witness (name, ps') |
|
2361 (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms |
|
2362 end; |
|
2363 |
|
2364 fun activate_derived_id ((_, Assumed _), _) thy = thy |
|
2365 | activate_derived_id (((name, ps), Derived ths), _) thy = let |
|
2366 val ps' = inst_parms ps; |
|
2367 in |
|
2368 if test_global_registration thy (name, ps') |
|
2369 then thy |
|
2370 else thy |
|
2371 |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp) |
|
2372 |> fold (fn witn => fn thy => add_global_witness (name, ps') |
|
2373 (witn |> Element.map_witness (fn (t, th) => (* FIXME *) |
|
2374 (Element.inst_term insts t, |
|
2375 disch (Element.inst_thm thy insts (satisfy th))))) thy) ths |
|
2376 end; |
|
2377 |
|
2378 fun activate_elem (loc, ps) (Notes (kind, facts)) thy = |
|
2379 let |
|
2380 val att_morphism = |
|
2381 Morphism.binding_morphism (name_morph phi_name param_prfx) $> |
|
2382 Morphism.thm_morphism satisfy $> |
|
2383 Element.inst_morphism thy insts $> |
|
2384 Morphism.thm_morphism disch; |
|
2385 val facts' = facts |
|
2386 |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) |
|
2387 |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy) |
|
2388 |> (map o apfst o apfst) (name_morph phi_name param_prfx); |
|
2389 in |
|
2390 thy |
|
2391 |> global_note_qualified kind facts' |
|
2392 |> snd |
|
2393 end |
|
2394 | activate_elem _ _ thy = thy; |
|
2395 |
|
2396 fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy; |
|
2397 |
|
2398 in thy |> fold activate_assumed_id ids_elemss_thmss |
|
2399 |> fold activate_derived_id ids_elemss |
|
2400 |> fold activate_elems new_elemss end; |
|
2401 in |
|
2402 thy |> fold activate_id ids_elemss_thmss |
|
2403 |> fold activate_reg regs |
|
2404 end; |
|
2405 |
|
2406 in (propss, activate) end; |
|
2407 |
|
2408 fun prep_propp propss = propss |> map (fn (_, props) => |
|
2409 map (rpair [] o Element.mark_witness) props); |
|
2410 |
|
2411 fun prep_result propps thmss = |
|
2412 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss); |
|
2413 |
|
2414 fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy = |
|
2415 let |
|
2416 val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts; |
|
2417 fun after_qed' results = |
|
2418 ProofContext.theory (activate (prep_result propss results)) |
|
2419 #> after_qed; |
|
2420 in |
|
2421 thy |
|
2422 |> ProofContext.init |
|
2423 |> Proof.theorem_i NONE after_qed' (prep_propp propss) |
|
2424 |> Element.refine_witness |
|
2425 |> Seq.hd |
|
2426 |> pair morphs |
|
2427 end; |
|
2428 |
|
2429 fun gen_interpret prep_registration after_qed name_morph expr insts int state = |
|
2430 let |
|
2431 val _ = Proof.assert_forward_or_chain state; |
|
2432 val ctxt = Proof.context_of state; |
|
2433 val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts; |
|
2434 fun after_qed' results = |
|
2435 Proof.map_context (K (ctxt |> activate (prep_result propss results))) |
|
2436 #> Proof.put_facts NONE |
|
2437 #> after_qed; |
|
2438 in |
|
2439 state |
|
2440 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i |
|
2441 "interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss)) |
|
2442 |> Element.refine_witness |> Seq.hd |
|
2443 |> pair morphs |
|
2444 end; |
|
2445 |
|
2446 fun standard_name_morph interp_prfx b = |
|
2447 if Binding.is_empty b then b |
|
2448 else Binding.map_prefix (fn ((lprfx, _) :: pprfx) => |
|
2449 fold (Binding.add_prefix false o fst) pprfx |
|
2450 #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx |
|
2451 #> Binding.add_prefix false lprfx |
|
2452 ) b; |
|
2453 |
|
2454 in |
|
2455 |
|
2456 val interpretation = gen_interpretation prep_global_registration; |
|
2457 fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd |
|
2458 I (standard_name_morph interp_prfx); |
|
2459 |
|
2460 fun interpretation_in_locale after_qed (raw_target, expr) thy = |
|
2461 let |
|
2462 val target = intern thy raw_target; |
|
2463 val (propss, activate) = prep_registration_in_locale target expr thy; |
|
2464 val raw_propp = prep_propp propss; |
|
2465 |
|
2466 val (_, _, goal_ctxt, propp) = thy |
|
2467 |> ProofContext.init |
|
2468 |> cert_context_statement (SOME target) [] raw_propp; |
|
2469 |
|
2470 fun after_qed' results = |
|
2471 ProofContext.theory (activate (prep_result propss results)) |
|
2472 #> after_qed; |
|
2473 in |
|
2474 goal_ctxt |
|
2475 |> Proof.theorem_i NONE after_qed' propp |
|
2476 |> Element.refine_witness |> Seq.hd |
|
2477 end; |
|
2478 |
|
2479 val interpret = gen_interpret prep_local_registration; |
|
2480 fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd |
|
2481 I (standard_name_morph interp_prfx); |
|
2482 |
|
2483 end; |
|
2484 |
|
2485 end; |
|