67 fun mk_xtor_un_fold_unique_tac fp xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps |
67 fun mk_xtor_un_fold_unique_tac fp xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps |
68 Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs {context = ctxt, prems} = |
68 Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs {context = ctxt, prems} = |
69 unfold_thms_tac ctxt xtor_un_fold_defs THEN |
69 unfold_thms_tac ctxt xtor_un_fold_defs THEN |
70 HEADGOAL (REPEAT_DETERM o FIRST' [hyp_subst_tac_thin true ctxt, rtac ctxt refl, |
70 HEADGOAL (REPEAT_DETERM o FIRST' [hyp_subst_tac_thin true ctxt, rtac ctxt refl, |
71 rtac ctxt conjI, |
71 rtac ctxt conjI, |
72 rtac ctxt @{thm arg_cong2[of _ _ _ _ "op o", OF refl]}, |
72 rtac ctxt @{thm arg_cong2[of _ _ _ _ "op \<circ>", OF refl]}, |
73 rtac ctxt @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}, |
73 rtac ctxt @{thm arg_cong2[of _ _ _ _ "op \<circ>", OF _ refl]}, |
74 resolve_tac ctxt map_arg_congs, |
74 resolve_tac ctxt map_arg_congs, |
75 resolve_tac ctxt fp_un_fold_uniques THEN_ALL_NEW case_fp fp (K all_tac) (rtac ctxt sym), |
75 resolve_tac ctxt fp_un_fold_uniques THEN_ALL_NEW case_fp fp (K all_tac) (rtac ctxt sym), |
76 SELECT_GOAL (CHANGED (unfold_thms_tac ctxt (flat [simp_thms, map_thms, map_defs, |
76 SELECT_GOAL (CHANGED (unfold_thms_tac ctxt (flat [simp_thms, map_thms, map_defs, |
77 xtor_un_fold_defs, xtor_un_fold_o_maps, Rep_o_Abss, prems]))), |
77 xtor_un_fold_defs, xtor_un_fold_o_maps, Rep_o_Abss, prems]))), |
78 unfold_once_tac ctxt cache_defs]); |
78 unfold_once_tac ctxt cache_defs]); |