equal
deleted
inserted
replaced
69 fun mk_inject_tac ctxt ctr_def ctor_inject = |
69 fun mk_inject_tac ctxt ctr_def ctor_inject = |
70 unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN |
70 unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN |
71 unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; |
71 unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; |
72 |
72 |
73 val rec_like_unfold_thms = |
73 val rec_like_unfold_thms = |
74 @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps |
74 @{thms comp_def convol_def id_apply map_pair_def prod_case_Pair_iden sum.simps(5,6) sum_map.simps |
75 split_conv}; |
75 split_conv unit_case_Unity}; |
76 |
76 |
77 fun mk_rec_like_tac pre_map_defs map_ids rec_like_defs ctor_rec_like ctr_def ctxt = |
77 fun mk_rec_like_tac pre_map_defs map_ids rec_like_defs ctor_rec_like ctr_def ctxt = |
78 unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_ids @ |
78 unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_ids @ |
79 rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1; |
79 rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1; |
80 |
80 |