49 fun mk_inject_tac ctxt ctr_def fld_inject = |
49 fun mk_inject_tac ctxt ctr_def fld_inject = |
50 Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN |
50 Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN |
51 Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; |
51 Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; |
52 |
52 |
53 val iter_like_thms = |
53 val iter_like_thms = |
54 @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps |
54 @{thms case_unit comp_def convol_def map_pair_def sum.simps(5,6) sum_map.simps split_conv}; |
55 split_conv}; |
|
56 |
55 |
57 fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt = |
56 fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt = |
58 Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ |
57 Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ |
59 iter_like_thms) THEN rtac refl 1; |
58 iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1; |
60 |
59 |
61 val coiter_like_ss = ss_only @{thms if_True if_False}; |
60 val coiter_like_ss = ss_only @{thms if_True if_False}; |
62 val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases}; |
61 val coiter_like_thms = @{thms map_pair_def sum_map.simps prod.cases}; |
63 |
62 |
64 fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt = |
63 fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt = |
65 Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN |
64 Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN |
66 subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN |
65 subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN |
67 Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN rtac refl 1; |
66 Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN |
|
67 Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1; |
68 |
68 |
69 end; |
69 end; |