equal
deleted
inserted
replaced
71 SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' |
71 SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' |
72 rtac refl)) 1; |
72 rtac refl)) 1; |
73 |
73 |
74 fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = |
74 fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = |
75 (rtac exhaust' THEN' |
75 (rtac exhaust' THEN' |
76 EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ |
76 EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => |
77 hyp_subst_tac THEN' |
77 EVERY' [hyp_subst_tac THEN' |
78 SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' |
78 SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' rtac case_thm]) |
79 rtac case_thm]) case_thms |
79 case_thms (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) |
80 (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1; |
80 sel_thmss)) 1; |
81 |
81 |
82 fun mk_case_cong_tac exhaust' case_thms = |
82 fun mk_case_cong_tac exhaust' case_thms = |
83 (rtac exhaust' THEN' |
83 (rtac exhaust' THEN' |
84 EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; |
84 EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; |
85 |
85 |