equal
deleted
inserted
replaced
65 fun mk_cong_intro_ctr_or_friend_tac ctxt ctr_or_friend_def extra_simps cong_alg_intro = |
65 fun mk_cong_intro_ctr_or_friend_tac ctxt ctr_or_friend_def extra_simps cong_alg_intro = |
66 HEADGOAL (REPEAT_DETERM_N 2 o subst_tac ctxt NONE [ctr_or_friend_def] THEN' |
66 HEADGOAL (REPEAT_DETERM_N 2 o subst_tac ctxt NONE [ctr_or_friend_def] THEN' |
67 rtac ctxt cong_alg_intro) THEN |
67 rtac ctxt cong_alg_intro) THEN |
68 unfold_thms_tac ctxt (extra_simps @ sumprod_thms_rel @ |
68 unfold_thms_tac ctxt (extra_simps @ sumprod_thms_rel @ |
69 @{thms vimage2p_def prod.rel_eq sum.rel_eq}) THEN |
69 @{thms vimage2p_def prod.rel_eq sum.rel_eq}) THEN |
70 REPEAT_DETERM (HEADGOAL (etac ctxt subst ORELSE' rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE' |
70 REPEAT_DETERM (HEADGOAL (rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE' rtac ctxt refl ORELSE' |
71 rtac ctxt refl)); |
71 etac ctxt subst)); |
72 |
72 |
73 val shared_simps = |
73 val shared_simps = |
74 @{thms map_prod_simp map_sum.simps sum.case prod.case_eq_if split_beta' prod.sel |
74 @{thms map_prod_simp map_sum.simps sum.case prod.case_eq_if split_beta' prod.sel |
75 sum.disc(1)[THEN eq_True[THEN iffD2]] sum.disc(2)[THEN eq_False[THEN iffD2]] sum.sel |
75 sum.disc(1)[THEN eq_True[THEN iffD2]] sum.disc(2)[THEN eq_False[THEN iffD2]] sum.sel |
76 isl_map_sum map_sum_sel if_True if_False if_True_False Let_def[abs_def] o_def[abs_def] id_def |
76 isl_map_sum map_sum_sel if_True if_False if_True_False Let_def[abs_def] o_def[abs_def] id_def |