223 T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
238 T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
224 (((bool * string) * Attrib.src list) * |
239 (((bool * string) * Attrib.src list) * |
225 Element.witness list * |
240 Element.witness list * |
226 thm Termtab.table) option |
241 thm Termtab.table) option |
227 val insert: theory -> term list -> ((bool * string) * Attrib.src list) -> |
242 val insert: theory -> term list -> ((bool * string) * Attrib.src list) -> |
228 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> T -> |
243 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
|
244 T -> |
229 T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list |
245 T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list |
230 val add_witness: term list -> Element.witness -> T -> T |
246 val add_witness: term list -> Element.witness -> T -> T |
231 val add_equation: term list -> thm -> T -> T |
247 val add_equation: term list -> thm -> T -> T |
232 end = |
248 end = |
233 struct |
249 struct |
234 (* A registration is indexed by parameter instantiation. Its components are: |
250 (* A registration is indexed by parameter instantiation. |
235 - parameters and prefix |
251 NB: index is exported whereas content is internalised. *) |
236 (if the Boolean flag is set, only accesses containing the prefix are generated, |
252 type T = registration Termtab.table; |
237 otherwise the prefix may be omitted when accessing theorems etc.) |
253 |
238 - pair of export and import morphisms, export maps content to its originating |
254 fun mk_reg attn exp imp wits eqns = |
239 context, import is its inverse |
255 {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns}; |
240 - theorems (actually witnesses) instantiating locale assumptions |
256 |
241 - theorems (equations) interpreting derived concepts and indexed by lhs. |
257 fun map_reg f reg = |
242 NB: index is exported whereas content is internalised. |
258 let |
243 *) |
259 val {attn, exp, imp, wits, eqns} = reg; |
244 type T = (((bool * string) * Attrib.src list) * |
260 val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns); |
245 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * |
261 in mk_reg attn' exp' imp' wits' eqns' end; |
246 Element.witness list * |
|
247 thm Termtab.table) Termtab.table; |
|
248 |
262 |
249 val empty = Termtab.empty; |
263 val empty = Termtab.empty; |
250 |
264 |
251 (* term list represented as single term, for simultaneous matching *) |
265 (* term list represented as single term, for simultaneous matching *) |
252 fun termify ts = |
266 fun termify ts = |
259 (* joining of registrations: |
273 (* joining of registrations: |
260 - prefix, attributes and morphisms of right theory; |
274 - prefix, attributes and morphisms of right theory; |
261 - witnesses are equal, no attempt to subsumption testing; |
275 - witnesses are equal, no attempt to subsumption testing; |
262 - union of equalities, if conflicting (i.e. two eqns with equal lhs) |
276 - union of equalities, if conflicting (i.e. two eqns with equal lhs) |
263 eqn of right theory takes precedence *) |
277 eqn of right theory takes precedence *) |
264 fun join (r1, r2) = Termtab.join (fn _ => fn ((_, _, _, e1), (n, m, w, e2)) => |
278 fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) => |
265 (n, m, w, Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2); |
279 mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2); |
266 |
280 |
267 fun dest_transfer thy regs = |
281 fun dest_transfer thy regs = |
268 Termtab.dest regs |> map (apsnd (fn (n, m, ws, es) => |
282 Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es) => |
269 (n, m, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))); |
283 (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es)))); |
270 |
284 |
271 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify); |
285 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |> |
|
286 map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns))); |
272 |
287 |
273 (* registrations that subsume t *) |
288 (* registrations that subsume t *) |
274 fun subsumers thy t regs = |
289 fun subsumers thy t regs = |
275 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); |
290 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); |
276 |
291 |
284 val t = termify ts; |
299 val t = termify ts; |
285 val subs = subsumers thy t regs; |
300 val subs = subsumers thy t regs; |
286 in |
301 in |
287 (case subs of |
302 (case subs of |
288 [] => NONE |
303 [] => NONE |
289 | ((t', ((prfx, atts), (exp', ((impT', domT'), (imp', dom'))), thms, eqns)) :: _) => |
304 | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) => |
290 let |
305 let |
291 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); |
306 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); |
292 val tinst' = domT' |> map (fn (T as TFree (x, _)) => |
307 val tinst' = domT' |> map (fn (T as TFree (x, _)) => |
293 (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst |
308 (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst |
294 |> var_instT_type impT)) |> Symtab.make; |
309 |> var_instT_type impT)) |> Symtab.make; |
295 val inst' = dom' |> map (fn (t as Free (x, _)) => |
310 val inst' = dom' |> map (fn (t as Free (x, _)) => |
296 (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst) |
311 (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst) |
297 |> var_inst_term (impT, imp))) |> Symtab.make; |
312 |> var_inst_term (impT, imp))) |> Symtab.make; |
298 val inst'_morph = Element.inst_morphism thy (tinst', inst'); |
313 val inst'_morph = Element.inst_morphism thy (tinst', inst'); |
299 in SOME ((prfx, map (Args.morph_values inst'_morph) atts), |
314 in SOME ((prfx, map (Args.morph_values inst'_morph) atts), |
300 map (Element.morph_witness inst'_morph) thms, |
315 map (Element.morph_witness inst'_morph) wits, |
301 Termtab.map (Morphism.thm inst'_morph) eqns) |
316 Termtab.map (Morphism.thm inst'_morph) eqns) |
302 end) |
317 end) |
303 end; |
318 end; |
304 |
319 |
305 (* add registration if not subsumed by ones already present, |
320 (* add registration if not subsumed by ones already present, |
306 additionally returns registrations that are strictly subsumed *) |
321 additionally returns registrations that are strictly subsumed *) |
307 fun insert thy ts attn m regs = |
322 fun insert thy ts attn (exp, imp) regs = |
308 let |
323 let |
309 val t = termify ts; |
324 val t = termify ts; |
310 val subs = subsumers thy t regs ; |
325 val subs = subsumers thy t regs ; |
311 in (case subs of |
326 in (case subs of |
312 [] => let |
327 [] => let |
313 val sups = |
328 val sups = |
314 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); |
329 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); |
315 val sups' = map (apfst untermify) sups |> map (fn (ts, (n, _, w, _)) => (ts, (n, w))) |
330 val sups' = map (apfst untermify) sups |> map (fn (ts, {attn, wits, ...}) => (ts, (attn, wits))) |
316 in (Termtab.update (t, (attn, m, [], Termtab.empty)) regs, sups') end |
331 in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end |
317 | _ => (regs, [])) |
332 | _ => (regs, [])) |
318 end; |
333 end; |
319 |
334 |
320 fun gen_add f ts regs = |
335 fun gen_add f ts regs = |
321 let |
336 let |
322 val t = termify ts; |
337 val t = termify ts; |
323 in |
338 in |
324 Termtab.update (t, f (the (Termtab.lookup regs t))) regs |
339 Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs |
325 end; |
340 end; |
326 |
341 |
327 (* add witness theorem to registration, |
342 (* add witness theorem to registration, |
328 only if instantiation is exact, otherwise exception Option raised *) |
343 only if instantiation is exact, otherwise exception Option raised *) |
329 fun add_witness ts wit regs = |
344 fun add_witness ts wit regs = |
330 gen_add (fn (x, m, wits, eqns) => (x, m, Element.close_witness wit :: wits, eqns)) |
345 gen_add (fn (x, e, i, wits, eqns) => (x, e, i, Element.close_witness wit :: wits, eqns)) |
331 ts regs; |
346 ts regs; |
332 |
347 |
333 (* add equation to registration, replaces previous equation with same lhs; |
348 (* add equation to registration, replaces previous equation with same lhs; |
334 only if instantiation is exact, otherwise exception Option raised; |
349 only if instantiation is exact, otherwise exception Option raised; |
335 exception TERM raised if not a meta equality *) |
350 exception TERM raised if not a meta equality *) |
336 fun add_equation ts thm regs = |
351 fun add_equation ts thm regs = |
337 gen_add (fn (x, m, thms, eqns) => |
352 gen_add (fn (x, e, i, thms, eqns) => |
338 (x, m, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns)) |
353 (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns)) |
339 ts regs; |
354 ts regs; |
340 end; |
355 end; |
341 |
356 |
342 |
357 |
343 (** theory data : locales **) |
358 (** theory data : locales **) |
447 fun test_local_registration ctxt = test_registration (Context.Proof ctxt); |
462 fun test_local_registration ctxt = test_registration (Context.Proof ctxt); |
448 |
463 |
449 |
464 |
450 (* add registration to theory or context, ignored if subsumed *) |
465 (* add registration to theory or context, ignored if subsumed *) |
451 |
466 |
452 fun put_registration (name, ps) attn morphs ctxt = |
467 fun put_registration (name, ps) attn morphs (* wits *) ctxt = |
453 RegistrationsData.map (fn regs => |
468 RegistrationsData.map (fn regs => |
454 let |
469 let |
455 val thy = Context.theory_of ctxt; |
470 val thy = Context.theory_of ctxt; |
456 val reg = the_default Registrations.empty (Symtab.lookup regs name); |
471 val reg = the_default Registrations.empty (Symtab.lookup regs name); |
457 val (reg', sups) = Registrations.insert thy ps attn morphs reg; |
472 val (reg', sups) = Registrations.insert thy ps attn morphs (* wits *) reg; |
458 val _ = if not (null sups) then warning |
473 val _ = if not (null sups) then warning |
459 ("Subsumed interpretation(s) of locale " ^ |
474 ("Subsumed interpretation(s) of locale " ^ |
460 quote (extern thy name) ^ |
475 quote (extern thy name) ^ |
461 "\nwith the following prefix(es):" ^ |
476 "\nwith the following prefix(es):" ^ |
462 commas_quote (map (fn (_, (((_, s), _), _)) => s) sups)) |
477 commas_quote (map (fn (_, (((_, s), _), _)) => s) sups)) |
2042 |
2057 |
2043 fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn |
2058 fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn |
2044 attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt = |
2059 attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt = |
2045 let |
2060 let |
2046 val ctxt = mk_ctxt thy_ctxt; |
2061 val ctxt = mk_ctxt thy_ctxt; |
2047 val (propss, eq_props) = chop (length all_elemss) propss; |
2062 val (all_propss, eq_props) = chop (length all_elemss) propss; |
2048 val (thmss, eq_thms) = chop (length all_elemss) thmss; |
2063 val (all_thmss, eq_thms) = chop (length all_elemss) thmss; |
2049 |
2064 |
2050 (* Filter out fragments already registered. *) |
2065 (* Filter out fragments already registered. *) |
2051 |
2066 |
2052 val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) => |
2067 val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) => |
2053 test_reg thy_ctxt id) (all_elemss ~~ (propss ~~ thmss))); |
2068 test_reg thy_ctxt id) (all_elemss ~~ (all_propss ~~ all_thmss))); |
2054 val (propss, thmss) = split_list xs; |
2069 val (new_propss, new_thmss) = split_list xs; |
2055 |
2070 |
2056 fun activate_elem prems eqns exp loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt = |
2071 val thy_ctxt' = thy_ctxt |
|
2072 (* add registrations *) |
|
2073 (* |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *) |
|
2074 |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss |
|
2075 (* add witnesses of Assumed elements (only those generate proof obligations) *) |
|
2076 |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss) |
|
2077 (* add equations *) |
|
2078 |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~ |
|
2079 (map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o |
|
2080 Element.conclude_witness) eq_thms); |
|
2081 |
|
2082 val prems = flat (map_filter |
|
2083 (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) |
|
2084 | ((_, Derived _), _) => NONE) all_elemss); |
|
2085 |
|
2086 fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt = |
2057 let |
2087 let |
2058 val ctxt = mk_ctxt thy_ctxt; |
2088 val ctxt = mk_ctxt thy_ctxt; |
2059 val facts' = interpret_args (ProofContext.theory_of ctxt) prfx |
2089 val facts' = interpret_args (ProofContext.theory_of ctxt) prfx |
2060 (Symtab.empty, Symtab.empty) prems eqns atts |
2090 (Symtab.empty, Symtab.empty) prems eqns atts |
2061 exp (attrib thy_ctxt) facts; |
2091 exp (attrib thy_ctxt) facts; |
2062 in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end |
2092 in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end |
2063 | activate_elem _ _ _ _ _ _ thy_ctxt = thy_ctxt; |
2093 | activate_elem _ _ _ _ thy_ctxt = thy_ctxt; |
2064 |
2094 |
2065 fun activate_elems prems eqns exp ((id, _), elems) thy_ctxt = |
2095 fun activate_elems all_eqns ((id, _), elems) thy_ctxt = |
2066 let |
2096 let |
2067 val (prfx_atts, _, _) = case get_reg thy_ctxt imp id |
2097 val (prfx_atts, _, _) = case get_reg thy_ctxt imp id |
2068 of SOME x => x |
2098 of SOME x => x |
2069 | NONE => sys_error ("Unknown registration of " ^ quote (fst id) |
2099 | NONE => sys_error ("Unknown registration of " ^ quote (fst id) |
2070 ^ " while activating facts."); |
2100 ^ " while activating facts."); |
2071 in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp (fst id) prfx_atts) elems thy_ctxt end; |
2101 in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end; |
2072 |
|
2073 val thy_ctxt' = thy_ctxt |
|
2074 (* add registrations *) |
|
2075 |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss |
|
2076 (* add witnesses of Assumed elements (only those generate proof obligations) *) |
|
2077 |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss) |
|
2078 (* add equations *) |
|
2079 |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~ |
|
2080 (map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o |
|
2081 Element.conclude_witness) eq_thms); |
|
2082 |
|
2083 val prems = flat (map_filter |
|
2084 (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) |
|
2085 | ((_, Derived _), _) => NONE) all_elemss); |
|
2086 |
2102 |
2087 val thy_ctxt'' = thy_ctxt' |
2103 val thy_ctxt'' = thy_ctxt' |
2088 (* add witnesses of Derived elements *) |
2104 (* add witnesses of Derived elements *) |
2089 |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms) |
2105 |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms) |
2090 (map_filter (fn ((_, Assumed _), _) => NONE |
2106 (map_filter (fn ((_, Assumed _), _) => NONE |
2091 | ((id, Derived thms), _) => SOME (id, thms)) new_elemss) |
2107 | ((id, Derived thms), _) => SOME (id, thms)) new_elemss) |
2092 |
2108 |
2093 (* Accumulate equations *) |
2109 (* Accumulate equations *) |
2094 val all_eqns = |
2110 val all_eqns = |
2095 fold_map (join_eqns (get_reg thy_ctxt'' imp) (fst o fst) ctxt) all_elemss Termtab.empty |
2111 fold_map (join_eqns (get_reg thy_ctxt'' imp) fst ctxt) all_propss Termtab.empty |
2096 |> fst |
2112 |> fst |
2097 |> map (apsnd (map snd o Termtab.dest)) |
2113 |> map (apsnd (map snd o Termtab.dest)) |
2098 |> (fn xs => fold Idtab.update xs Idtab.empty) |
2114 |> (fn xs => fold Idtab.update xs Idtab.empty) |
2099 (* Idtab.make wouldn't work here: can have conflicting duplicates, |
2115 (* Idtab.make wouldn't work here: can have conflicting duplicates, |
2100 because instantiation may equate ids and equations are accumulated! *) |
2116 because instantiation may equate ids and equations are accumulated! *) |