1569 |
1569 |
1570 (** store results **) |
1570 (** store results **) |
1571 |
1571 |
1572 (* naming of interpreted theorems *) |
1572 (* naming of interpreted theorems *) |
1573 |
1573 |
1574 fun global_note_prefix_i kind loc (fully_qualified, prfx) params args thy = |
1574 fun add_param_prefixss s = |
|
1575 (map o apfst o apfst) (NameSpace.qualified s); |
|
1576 fun drop_param_prefixss args = (map o apfst o apfst) |
|
1577 (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args; |
|
1578 |
|
1579 fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy = |
1575 thy |
1580 thy |
1576 |> Sign.qualified_names |
1581 |> Sign.qualified_names |
1577 |> Sign.add_path (NameSpace.base loc ^ "_locale") |
1582 |> Sign.add_path (NameSpace.base loc ^ "_locale") |
1578 |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx) |
1583 |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx) |
1579 |> (if fully_qualified then Sign.add_path (space_implode "_" params) else I) |
1584 |> PureThy.note_thmss kind (if fully_qualified then args else drop_param_prefixss args) |
1580 |> PureThy.note_thmss kind args |
|
1581 ||> Sign.restore_naming thy; |
1585 ||> Sign.restore_naming thy; |
1582 |
1586 |
1583 fun local_note_prefix_i kind loc (fully_qualified, prfx) params args ctxt = |
1587 fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt = |
1584 ctxt |
1588 ctxt |
1585 |> ProofContext.qualified_names |
1589 |> ProofContext.qualified_names |
1586 |> ProofContext.add_path (NameSpace.base loc ^ "_locale") |
1590 |> ProofContext.add_path (NameSpace.base loc ^ "_locale") |
1587 |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx) |
1591 |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx) |
1588 |> (if fully_qualified then ProofContext.add_path (space_implode "_" params) else I) |
1592 |> ProofContext.note_thmss_i kind (if fully_qualified then args else drop_param_prefixss args) |
1589 |> ProofContext.note_thmss_i kind args |
|
1590 ||> ProofContext.restore_naming ctxt; |
1593 ||> ProofContext.restore_naming ctxt; |
1591 |
1594 |
1592 |
1595 |
1593 (* join equations of an id with already accumulated ones *) |
1596 (* join equations of an id with already accumulated ones *) |
1594 |
1597 |
1685 |
1688 |
1686 fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy = |
1689 fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy = |
1687 let |
1690 let |
1688 val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts; |
1691 val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts; |
1689 val attrib = Attrib.attribute_i thy; |
1692 val attrib = Attrib.attribute_i thy; |
1690 val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args; |
1693 val args' = args |
1691 in global_note_prefix_i kind target (fully_qualified, prfx) (map fst parms) args' thy |> snd end; |
1694 |> interpret_args thy prfx insts prems eqns atts2 exp attrib |
|
1695 |> add_param_prefixss (space_implode "_" (map fst parms)); |
|
1696 in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end; |
1692 in fold activate regs thy end; |
1697 in fold activate regs thy end; |
1693 |
1698 |
1694 |
1699 |
1695 (* locale results *) |
1700 (* locale results *) |
1696 |
1701 |
2089 let |
2094 let |
2090 val ctxt = mk_ctxt thy_ctxt; |
2095 val ctxt = mk_ctxt thy_ctxt; |
2091 val facts' = interpret_args (ProofContext.theory_of ctxt) prfx |
2096 val facts' = interpret_args (ProofContext.theory_of ctxt) prfx |
2092 (Symtab.empty, Symtab.empty) prems eqns atts |
2097 (Symtab.empty, Symtab.empty) prems eqns atts |
2093 exp (attrib thy_ctxt) facts; |
2098 exp (attrib thy_ctxt) facts; |
2094 in snd (note_interp kind loc (fully_qualified, prfx) [] facts' thy_ctxt) end |
2099 in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end |
2095 | activate_elem _ _ _ _ thy_ctxt = thy_ctxt; |
2100 | activate_elem _ _ _ _ thy_ctxt = thy_ctxt; |
2096 |
2101 |
2097 fun activate_elems all_eqns ((id, _), elems) thy_ctxt = |
2102 fun activate_elems all_eqns ((id, _), elems) thy_ctxt = |
2098 let |
2103 let |
2099 val (prfx_atts, _, _) = case get_reg thy_ctxt imp id |
2104 val (prfx_atts, _, _) = case get_reg thy_ctxt imp id |
2264 (* instantiate ids and elements *) |
2269 (* instantiate ids and elements *) |
2265 val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) => |
2270 val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) => |
2266 ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps), |
2271 ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps), |
2267 map (fn Int e => Element.morph_ctxt inst_morphism e) elems) |
2272 map (fn Int e => Element.morph_ctxt inst_morphism e) elems) |
2268 |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode))); |
2273 |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode))); |
|
2274 |
2269 (* equations *) |
2275 (* equations *) |
2270 val eqn_elems = if null eqns then [] |
2276 val eqn_elems = if null eqns then [] |
2271 else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; |
2277 else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; |
2272 |
2278 |
2273 val propss = map extract_asms_elems inst_elemss @ eqn_elems; |
2279 val propss = map extract_asms_elems inst_elemss @ eqn_elems; |
2376 |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) |
2382 |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) |
2377 |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2))) |
2383 |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2))) |
2378 |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy))))) |
2384 |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy))))) |
2379 in |
2385 in |
2380 thy |
2386 thy |
2381 |> global_note_prefix_i kind loc (fully_qualified, prfx) [] facts' |
2387 |> global_note_prefix_i kind loc (fully_qualified, prfx) facts' |
2382 |> snd |
2388 |> snd |
2383 end |
2389 end |
2384 | activate_elem _ _ thy = thy; |
2390 | activate_elem _ _ thy = thy; |
2385 |
2391 |
2386 fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy; |
2392 fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy; |