784 |
784 |
785 (** Interpretation in theories **) |
785 (** Interpretation in theories **) |
786 |
786 |
787 local |
787 local |
788 |
788 |
789 fun gen_interpretation prep_expr prep_thms |
789 datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list; |
|
790 |
|
791 fun gen_interpretation prep_expr parse_prop prep_attr |
790 expression equations thy = |
792 expression equations thy = |
791 let |
793 let |
792 val ctxt = ProofContext.init thy; |
794 val ctxt = ProofContext.init thy; |
793 |
795 |
794 val eqns = equations |> prep_thms ctxt |> |
796 val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt; |
795 map (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt); |
797 |
796 val eq_morph = |
798 val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt; |
797 Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> |
799 val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations; |
798 Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns); |
800 val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; |
799 |
801 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
800 val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; |
802 |
801 |
803 fun store (Reg (name, morph), thms) (regs, thy) = |
802 fun store_reg ((name, morph), thms) = |
804 let |
803 let |
805 val thms' = map (Element.morph_witness export') thms; |
804 val morph' = morph $> Element.satisfy_morphism thms; |
806 val morph' = morph $> Element.satisfy_morphism thms'; |
805 in |
807 val add = NewLocale.add_global_registration (name, (morph', export)); |
806 NewLocale.add_global_registration (name, (morph', export)) #> |
808 in ((name, morph') :: regs, add thy) end |
807 NewLocale.amend_global_registration (name, morph') eq_morph #> |
809 | store (Eqns [], []) (regs, thy) = |
808 NewLocale.activate_global_facts (name, morph' $> eq_morph $> export) |
810 let val add = fold_rev (fn (name, morph) => |
809 end; |
811 NewLocale.activate_global_facts (name, morph $> export)) regs; |
|
812 in (regs, add thy) end |
|
813 | store (Eqns attns, thms) (regs, thy) = |
|
814 let |
|
815 val thms' = thms |> map (Element.conclude_witness #> |
|
816 Morphism.thm (export' $> export) #> |
|
817 LocalDefs.meta_rewrite_rule (ProofContext.init thy) #> |
|
818 Drule.abs_def); |
|
819 val eq_morph = |
|
820 Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $> |
|
821 Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms'); |
|
822 val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns; |
|
823 val add = |
|
824 fold_rev (fn (name, morph) => |
|
825 NewLocale.amend_global_registration eq_morph (name, morph) #> |
|
826 NewLocale.activate_global_facts (name, morph $> eq_morph $> export)) regs #> |
|
827 PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #> |
|
828 snd |
|
829 in (regs, add thy) end; |
810 |
830 |
811 fun after_qed results = |
831 fun after_qed results = |
812 ProofContext.theory (fold store_reg (regs ~~ prep_result propss results)); |
832 ProofContext.theory (fn thy => |
|
833 fold store (map Reg regs @ [Eqns eq_attns] ~~ |
|
834 prep_result (propss @ [eqns]) results) ([], thy) |> snd); |
813 in |
835 in |
814 goal_ctxt |> |
836 goal_ctxt |> |
815 Proof.theorem_i NONE after_qed (prep_propp propss) |> |
837 Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |> |
816 Element.refine_witness |> Seq.hd |
838 Element.refine_witness |> Seq.hd |
817 end; |
839 end; |
818 |
840 |
819 in |
841 in |
820 |
842 |
821 fun interpretation_cmd x = gen_interpretation read_goal_expression |
843 fun interpretation_cmd x = gen_interpretation read_goal_expression |
822 (fn ctxt => map (ProofContext.get_fact ctxt) #> flat) x; |
844 Syntax.parse_prop Attrib.intern_src x; |
823 fun interpretation x = gen_interpretation cert_goal_expression (K I) x; |
845 fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x; |
824 |
846 |
825 end; |
847 end; |
826 |
848 |
827 |
849 |
828 (** Interpretation in proof contexts **) |
850 (** Interpretation in proof contexts **) |