94 Proof.context -> Proof.context |
94 Proof.context -> Proof.context |
95 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context |
95 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context |
96 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context |
96 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context |
97 val add_declaration: string -> declaration -> Proof.context -> Proof.context |
97 val add_declaration: string -> declaration -> Proof.context -> Proof.context |
98 |
98 |
|
99 (* Interpretation *) |
|
100 val get_interpret_morph: theory -> string -> string -> |
|
101 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
|
102 string -> term list -> Morphism.morphism |
99 val interpretation_i: (Proof.context -> Proof.context) -> |
103 val interpretation_i: (Proof.context -> Proof.context) -> |
100 bool * string -> expr -> |
104 bool * string -> expr -> |
101 term option list * (Attrib.binding * term) list -> |
105 term option list * (Attrib.binding * term) list -> |
102 theory -> Proof.state |
106 theory -> |
|
107 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
103 val interpretation: (Proof.context -> Proof.context) -> |
108 val interpretation: (Proof.context -> Proof.context) -> |
104 bool * string -> expr -> |
109 bool * string -> expr -> |
105 string option list * (Attrib.binding * string) list -> |
110 string option list * (Attrib.binding * string) list -> |
106 theory -> Proof.state |
111 theory -> |
|
112 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
107 val interpretation_in_locale: (Proof.context -> Proof.context) -> |
113 val interpretation_in_locale: (Proof.context -> Proof.context) -> |
108 xstring * expr -> theory -> Proof.state |
114 xstring * expr -> theory -> Proof.state |
109 val interpret_i: (Proof.state -> Proof.state Seq.seq) -> |
115 val interpret_i: (Proof.state -> Proof.state Seq.seq) -> |
110 bool * string -> expr -> |
116 bool * string -> expr -> |
111 term option list * (Attrib.binding * term) list -> |
117 term option list * (Attrib.binding * term) list -> |
112 bool -> Proof.state -> Proof.state |
118 bool -> Proof.state -> |
|
119 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
113 val interpret: (Proof.state -> Proof.state Seq.seq) -> |
120 val interpret: (Proof.state -> Proof.state Seq.seq) -> |
114 bool * string -> expr -> |
121 bool * string -> expr -> |
115 string option list * (Attrib.binding * string) list -> |
122 string option list * (Attrib.binding * string) list -> |
116 bool -> Proof.state -> Proof.state |
123 bool -> Proof.state -> |
|
124 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
117 end; |
125 end; |
118 |
126 |
119 structure Locale: LOCALE = |
127 structure Locale: LOCALE = |
120 struct |
128 struct |
121 |
129 |
238 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
246 (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
239 T -> |
247 T -> |
240 T * (term list * (((bool * string) * string) * Element.witness list)) list |
248 T * (term list * (((bool * string) * string) * Element.witness list)) list |
241 val add_witness: term list -> Element.witness -> T -> T |
249 val add_witness: term list -> Element.witness -> T -> T |
242 val add_equation: term list -> thm -> T -> T |
250 val add_equation: term list -> thm -> T -> T |
243 (* val update_morph: term list -> Element.witness list * thm list -> T -> T *) |
251 (* |
244 (* val get_morph: theory -> T -> term list -> string list -> Morphism.morphism *) |
252 val update_morph: term list -> Morphism.morphism -> T -> T |
|
253 val get_morph: theory -> T -> |
|
254 term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) -> |
|
255 Morphism.morphism |
|
256 *) |
245 end = |
257 end = |
246 struct |
258 struct |
247 (* A registration is indexed by parameter instantiation. |
259 (* A registration is indexed by parameter instantiation. |
248 NB: index is exported whereas content is internalised. *) |
260 NB: index is exported whereas content is internalised. *) |
249 type T = registration Termtab.table; |
261 type T = registration Termtab.table; |
347 exception TERM raised if not a meta equality *) |
359 exception TERM raised if not a meta equality *) |
348 fun add_equation ts thm regs = |
360 fun add_equation ts thm regs = |
349 gen_add (fn (x, e, i, thms, eqns, m) => |
361 gen_add (fn (x, e, i, thms, eqns, m) => |
350 (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m)) |
362 (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m)) |
351 ts regs; |
363 ts regs; |
352 |
|
353 (* update morphism of registration; |
|
354 only if instantiation is exact, otherwise exception Option raised *) |
|
355 (* |
|
356 fun update_morph ts (wits, eqns') regs = |
|
357 gen_add (fn (x, e, i, thms, eqns, _) => |
|
358 (x, e, i, thms, eqns, (wits, eqns'))) |
|
359 ts regs; |
|
360 *) |
|
361 |
364 |
362 end; |
365 end; |
363 |
366 |
364 |
367 |
365 (** theory data : locales **) |
368 (** theory data : locales **) |
1644 fold_map (join_eqns (get_local_registration ctxt imprt)) |
1647 fold_map (join_eqns (get_local_registration ctxt imprt)) |
1645 (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd; |
1648 (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd; |
1646 in ((tinst, inst), wits, eqns) end; |
1649 in ((tinst, inst), wits, eqns) end; |
1647 |
1650 |
1648 |
1651 |
1649 (* standardise export morphism *) |
1652 (* compute morphism and apply to args *) |
1650 |
1653 |
1651 (* clone from Element.generalize_facts *) |
1654 fun inst_morph thy prfx param_prfx insts prems eqns export = |
1652 fun standardize thy export facts = |
1655 let |
1653 let |
1656 (* standardise export morphism *) |
1654 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
1657 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
1655 val exp_term = TermSubst.zero_var_indexes o Morphism.term export; |
1658 val exp_term = TermSubst.zero_var_indexes o Morphism.term export; |
1656 (* FIXME sync with exp_fact *) |
1659 (* FIXME sync with exp_fact *) |
1657 val exp_typ = Logic.type_map exp_term; |
1660 val exp_typ = Logic.type_map exp_term; |
1658 val morphism = |
1661 val export' = |
1659 Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
1662 Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
1660 in Element.facts_map (Element.morph_ctxt morphism) facts end; |
1663 in |
1661 |
1664 Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $> |
|
1665 Element.inst_morphism thy insts $> Element.satisfy_morphism prems $> |
|
1666 Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> |
|
1667 Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $> |
|
1668 export' |
|
1669 end; |
1662 |
1670 |
1663 fun morph_ctxt' phi = Element.map_ctxt |
1671 fun morph_ctxt' phi = Element.map_ctxt |
1664 {name = I, |
1672 {name = I, |
1665 var = Morphism.var phi, |
1673 var = Morphism.var phi, |
1666 typ = Morphism.typ phi, |
1674 typ = Morphism.typ phi, |
1667 term = Morphism.term phi, |
1675 term = Morphism.term phi, |
1668 fact = Morphism.fact phi, |
1676 fact = Morphism.fact phi, |
1669 attrib = Args.morph_values phi}; |
1677 attrib = Args.morph_values phi}; |
1670 |
1678 |
1671 |
1679 fun interpret_args thy inst attrib args = |
1672 (* compute morphism and apply to args *) |
1680 args |> Element.facts_map (morph_ctxt' inst) |> Attrib.map_facts attrib; |
1673 |
1681 (* morph_ctxt' suppresses application of name morphism. FIXME *) |
1674 fun inst_morph thy prfx param_prfx insts prems eqns = |
1682 |
1675 Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $> |
1683 (* public interface to interpretation morphism *) |
1676 Element.inst_morphism thy insts $> Element.satisfy_morphism prems $> |
1684 |
1677 Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> |
1685 fun get_interpret_morph thy prfx param_prfx (exp, imp) target ext_ts = |
1678 Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns); |
1686 let |
1679 |
1687 val parms = the_locale thy target |> #params |> map fst; |
1680 fun interpret_args thy inst exp attrib args = |
1688 val ids = flatten (ProofContext.init thy, intern_expr thy) |
1681 args |> Element.facts_map (morph_ctxt' inst) |> |
1689 (([], Symtab.empty), Expr (Locale target)) |> fst |> fst; |
1682 (* morph_ctxt' suppresses application of name morphism. FIXME *) |
1690 val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; |
1683 standardize thy exp |> Attrib.map_facts attrib; |
1691 in |
1684 |
1692 inst_morph thy prfx param_prfx insts prems eqns exp |
|
1693 end; |
1685 |
1694 |
1686 (* store instantiations of args for all registered interpretations |
1695 (* store instantiations of args for all registered interpretations |
1687 of the theory *) |
1696 of the theory *) |
1688 |
1697 |
1689 fun note_thmss_registrations target (kind, args) thy = |
1698 fun note_thmss_registrations target (kind, args) thy = |
1698 fun activate (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy = |
1707 fun activate (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy = |
1699 let |
1708 let |
1700 val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; |
1709 val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; |
1701 val attrib = Attrib.attribute_i thy; |
1710 val attrib = Attrib.attribute_i thy; |
1702 val args' = args |
1711 val args' = args |
1703 |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns) exp attrib |
1712 |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns exp) attrib |
1704 |> add_param_prefixss pprfx; |
1713 |> add_param_prefixss pprfx; |
1705 in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end; |
1714 in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end; |
1706 in fold activate regs thy end; |
1715 in fold activate regs thy end; |
1707 |
1716 |
1708 |
1717 |
2108 |
2117 |
2109 fun activate_elem inst loc prfx pprfx (Notes (kind, facts)) thy_ctxt = |
2118 fun activate_elem inst loc prfx pprfx (Notes (kind, facts)) thy_ctxt = |
2110 let |
2119 let |
2111 val ctxt = mk_ctxt thy_ctxt; |
2120 val ctxt = mk_ctxt thy_ctxt; |
2112 val facts' = facts |> |
2121 val facts' = facts |> |
2113 interpret_args (ProofContext.theory_of ctxt) inst exp (attrib thy_ctxt) |> |
2122 interpret_args (ProofContext.theory_of ctxt) inst (attrib thy_ctxt) |> |
2114 add_param_prefixss pprfx; |
2123 add_param_prefixss pprfx; |
2115 in snd (note_interp kind loc prfx facts' thy_ctxt) end |
2124 in snd (note_interp kind loc prfx facts' thy_ctxt) end |
2116 | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt; |
2125 | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt; |
2117 |
2126 |
2118 fun activate_elems ((((loc, ext_ts), _), _), ps) thy_ctxt = |
2127 fun activate_elems ((((loc, ext_ts), _), _), ps) thy_ctxt = |
2123 val parms = map fst params; |
2132 val parms = map fst params; |
2124 val pprfx = param_prefix ps; |
2133 val pprfx = param_prefix ps; |
2125 val ids = flatten (ProofContext.init thy, intern_expr thy) |
2134 val ids = flatten (ProofContext.init thy, intern_expr thy) |
2126 (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst; |
2135 (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst; |
2127 val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts; |
2136 val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts; |
2128 val inst = inst_morph thy (snd prfx) pprfx insts prems eqns; |
2137 val inst = inst_morph thy (snd prfx) pprfx insts prems eqns exp; |
2129 in |
2138 in |
2130 fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt |
2139 fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt |
2131 end; |
2140 end; |
2132 |
2141 |
2133 in |
2142 in |
2282 val eqn_elems = if null eqns then [] |
2291 val eqn_elems = if null eqns then [] |
2283 else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; |
2292 else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; |
2284 |
2293 |
2285 val propss = map extract_asms_elems inst_elemss @ eqn_elems; |
2294 val propss = map extract_asms_elems inst_elemss @ eqn_elems; |
2286 |
2295 |
2287 in (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs) end; |
2296 in |
|
2297 (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs) |
|
2298 end; |
2288 |
2299 |
2289 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init |
2300 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init |
2290 test_global_registration |
2301 test_global_registration |
2291 global_activate_facts_elemss mk_ctxt; |
2302 global_activate_facts_elemss mk_ctxt; |
2292 |
2303 |
2414 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss); |
2425 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss); |
2415 |
2426 |
2416 fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy = |
2427 fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy = |
2417 (* prfx = (flag indicating full qualification, name prefix) *) |
2428 (* prfx = (flag indicating full qualification, name prefix) *) |
2418 let |
2429 let |
2419 val (propss, activate) = prep_registration thy prfx raw_expr raw_insts; |
2430 val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts; |
2420 fun after_qed' results = |
2431 fun after_qed' results = |
2421 ProofContext.theory (activate (prep_result propss results)) |
2432 ProofContext.theory (activate (prep_result propss results)) |
2422 #> after_qed; |
2433 #> after_qed; |
2423 in |
2434 in |
2424 thy |
2435 thy |
2425 |> ProofContext.init |
2436 |> ProofContext.init |
2426 |> Proof.theorem_i NONE after_qed' (prep_propp propss) |
2437 |> Proof.theorem_i NONE after_qed' (prep_propp propss) |
2427 |> Element.refine_witness |
2438 |> Element.refine_witness |
2428 |> Seq.hd |
2439 |> Seq.hd |
|
2440 |> pair morphs |
2429 end; |
2441 end; |
2430 |
2442 |
2431 fun gen_interpret prep_registration after_qed prfx expr insts int state = |
2443 fun gen_interpret prep_registration after_qed prfx expr insts int state = |
2432 (* prfx = (flag indicating full qualification, name prefix) *) |
2444 (* prfx = (flag indicating full qualification, name prefix) *) |
2433 let |
2445 let |
2434 val _ = Proof.assert_forward_or_chain state; |
2446 val _ = Proof.assert_forward_or_chain state; |
2435 val ctxt = Proof.context_of state; |
2447 val ctxt = Proof.context_of state; |
2436 val (propss, activate) = prep_registration ctxt prfx expr insts; |
2448 val (propss, activate, morphs) = prep_registration ctxt prfx expr insts; |
2437 fun after_qed' results = |
2449 fun after_qed' results = |
2438 Proof.map_context (K (ctxt |> activate (prep_result propss results))) |
2450 Proof.map_context (K (ctxt |> activate (prep_result propss results))) |
2439 #> Proof.put_facts NONE |
2451 #> Proof.put_facts NONE |
2440 #> after_qed; |
2452 #> after_qed; |
2441 in |
2453 in |
2442 state |
2454 state |
2443 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i |
2455 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i |
2444 "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss)) |
2456 "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss)) |
2445 |> Element.refine_witness |> Seq.hd |
2457 |> Element.refine_witness |> Seq.hd |
|
2458 |> pair morphs |
2446 end; |
2459 end; |
2447 |
2460 |
2448 in |
2461 in |
2449 |
2462 |
2450 val interpretation_i = gen_interpretation prep_global_registration_i; |
2463 val interpretation_i = gen_interpretation prep_global_registration_i; |