equal
deleted
inserted
replaced
666 let |
666 let |
667 val rhs = list_comb (un_fold, @{map 2} (absT_info_encode thy fp) absT_info_opts xtors); |
667 val rhs = list_comb (un_fold, @{map 2} (absT_info_encode thy fp) absT_info_opts xtors); |
668 val T = range_type (fastype_of rhs); |
668 val T = range_type (fastype_of rhs); |
669 in |
669 in |
670 HOLogic.mk_eq (HOLogic.id_const T, rhs) |
670 HOLogic.mk_eq (HOLogic.id_const T, rhs) |
671 end; |
671 end; |
672 val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map mk_goal un_folds)); |
672 val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map mk_goal un_folds)); |
673 fun mk_inverses NONE = [] |
673 fun mk_inverses NONE = [] |
674 | mk_inverses (SOME (src, dst)) = |
674 | mk_inverses (SOME (src, dst)) = |
675 [#type_definition dst RS @{thm type_definition.Abs_inverse[OF _ UNIV_I]}, |
675 [#type_definition dst RS @{thm type_definition.Abs_inverse[OF _ UNIV_I]}, |
676 #type_definition src RS @{thm type_definition.Rep_inverse}]; |
676 #type_definition src RS @{thm type_definition.Rep_inverse}]; |
881 val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop |
881 val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop |
882 #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb) |
882 #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb) |
883 #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of |
883 #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of |
884 #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T')) |
884 #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T')) |
885 Ts Us xtor_un_fold_transfers; |
885 Ts Us xtor_un_fold_transfers; |
886 |
886 |
887 fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs |
887 fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs |
888 xtor_un_fold_transfers map_transfers xtor_rels; |
888 xtor_un_fold_transfers map_transfers xtor_rels; |
889 |
889 |
890 val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum; |
890 val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum; |
891 val rec_phis = |
891 val rec_phis = |
892 map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis; |
892 map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis; |
893 in |
893 in |
894 mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis |
894 mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis |