466 fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts rel_eqs = |
466 fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts rel_eqs = |
467 HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW |
467 HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW |
468 rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW |
468 rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW |
469 hyp_subst_tac ctxt) THEN |
469 hyp_subst_tac ctxt) THEN |
470 unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @ |
470 unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @ |
471 ((discs @ distincts) RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ |
471 ((discs @ distincts) RL [eqTrueI, eqFalseI]) @ |
472 (rel_injects RL @{thms iffD2[OF eq_True]}) @ |
472 (rel_injects RL [eqTrueI]) @ |
473 (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN |
473 (rel_distincts RL [eqFalseI])) THEN |
474 TRYALL (resolve_tac [TrueI, refl]); |
474 TRYALL (resolve_tac [TrueI, refl]); |
475 |
475 |
476 fun mk_sel_transfer_tac ctxt n sel_defs case_transfer = |
476 fun mk_sel_transfer_tac ctxt n sel_defs case_transfer = |
477 TRYALL Goal.conjunction_tac THEN |
477 TRYALL Goal.conjunction_tac THEN |
478 unfold_thms_tac ctxt (map (Drule.abs_def o Local_Defs.meta_rewrite_rule ctxt) sel_defs) THEN |
478 unfold_thms_tac ctxt (map (Drule.abs_def o Local_Defs.meta_rewrite_rule ctxt) sel_defs) THEN |