equal
deleted
inserted
replaced
98 unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN |
98 unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN |
99 unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; |
99 unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; |
100 |
100 |
101 (*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*) |
101 (*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*) |
102 val rec_like_unfold_thms = |
102 val rec_like_unfold_thms = |
103 @{thms comp_def convol_def fst_conv id_def map_pair_def prod_case_Pair_iden snd_conv split_conv |
103 @{thms comp_def convol_def fst_conv id_def map_pair_simp prod_case_Pair_iden snd_conv split_conv |
104 sum.simps(5,6) sum_map.simps unit_case_Unity}; |
104 sum.simps(5,6) sum_map.simps unit_case_Unity}; |
105 |
105 |
106 fun mk_rec_like_tac pre_map_defs map_comp's map_ids'' rec_like_defs ctor_rec_like ctr_def ctxt = |
106 fun mk_rec_like_tac pre_map_defs map_comp's map_ids'' rec_like_defs ctor_rec_like ctr_def ctxt = |
107 unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_comp's @ |
107 unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_comp's @ |
108 map_ids'' @ rec_like_unfold_thms) THEN rtac refl 1; |
108 map_ids'' @ rec_like_unfold_thms) THEN rtac refl 1; |