817 |
817 |
818 (** Interpretation in theories and proof contexts **) |
818 (** Interpretation in theories and proof contexts **) |
819 |
819 |
820 local |
820 local |
821 |
821 |
822 fun note_eqns_register deps witss attrss eqns export export' = |
822 fun note_eqns_register deps witss attrss eqns export export' context = |
823 Attrib.generic_notes Thm.lemmaK |
823 let |
824 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns) |
824 val facts = |
825 #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts))) |
825 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns); |
826 #-> (fn eqns => fold (fn ((dep, morph), wits) => |
826 val (eqns', context') = context |
827 fn context => |
827 |> Attrib.generic_notes Thm.lemmaK facts |
|
828 |-> (fn facts' => `(fn context'' => meta_rewrite (Context.proof_of context'') (maps snd facts'))); |
|
829 in |
|
830 context' |
|
831 |> fold2 (fn (dep, morph) => fn wits => fn context'' => |
828 Locale.add_registration |
832 Locale.add_registration |
829 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
833 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
830 (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true)) |
834 (Element.eq_morphism (Context.theory_of context'') eqns' |> Option.map (rpair true)) |
831 export context) (deps ~~ witss)); |
835 export context'') deps witss |
|
836 end; |
832 |
837 |
833 fun gen_interpretation prep_expr parse_prop prep_attr |
838 fun gen_interpretation prep_expr parse_prop prep_attr |
834 expression equations thy = |
839 expression equations thy = |
835 let |
840 let |
836 val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global thy |
841 val initial_ctxt = Proof_Context.init_global thy; |
837 |> prep_expr expression; |
842 |
|
843 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
838 val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations; |
844 val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations; |
839 |
845 |
840 val attrss = map (apsnd (map (prep_attr thy)) o fst) equations; |
846 val attrss = map (apsnd (map (prep_attr thy)) o fst) equations; |
841 val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; |
847 val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; |
842 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
848 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
889 |
895 |
890 fun note_eqns_dependency target deps witss attrss eqns export export' ctxt = |
896 fun note_eqns_dependency target deps witss attrss eqns export export' ctxt = |
891 let |
897 let |
892 val facts = |
898 val facts = |
893 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns); |
899 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns); |
894 val eqns' = ctxt |
900 val (eqns', _) = ctxt (* FIXME duplication to add_thmss *) |
895 |> Attrib.local_notes Thm.lemmaK facts |
901 |> Attrib.local_notes Thm.lemmaK facts |
896 |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts))) |
902 |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts'))); |
897 |> fst; (* FIXME duplication to add_thmss *) |
|
898 in |
903 in |
899 ctxt |
904 ctxt |
900 |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts) |
905 |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts) |
901 |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) => |
906 |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits => |
902 fn thy => |
907 fn thy => |
903 Locale.add_dependency target |
908 Locale.add_dependency target |
904 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
909 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
905 (Element.eq_morphism thy eqns' |> Option.map (rpair true)) |
910 (Element.eq_morphism thy eqns' |> Option.map (rpair true)) |
906 export thy) (deps ~~ witss)) |
911 export thy) deps witss) |
907 end; |
912 end; |
908 |
913 |
909 fun gen_sublocale prep_expr prep_loc parse_prop prep_attr |
914 fun gen_sublocale prep_expr prep_loc parse_prop prep_attr |
910 before_exit raw_target expression equations thy = |
915 before_exit raw_target expression equations thy = |
911 let |
916 let |
912 val target = prep_loc thy raw_target; |
917 val target = prep_loc thy raw_target; |
913 val target_ctxt = Named_Target.init before_exit target thy; |
918 val initial_ctxt = Named_Target.init before_exit target thy; |
914 val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt; |
919 |
|
920 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
915 val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations; |
921 val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations; |
916 |
922 |
917 val attrss = map (apsnd (map (prep_attr thy)) o fst) equations; |
923 val attrss = map (apsnd (map (prep_attr thy)) o fst) equations; |
918 val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; |
924 val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; |
919 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
925 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |