equal
deleted
inserted
replaced
81 ctr_defs = @{thms Inl_def_alt Inr_def_alt}, |
81 ctr_defs = @{thms Inl_def_alt Inr_def_alt}, |
82 ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, |
82 ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, |
83 fp_bnf_sugar = |
83 fp_bnf_sugar = |
84 {map_thms = @{thms map_sum.simps}, |
84 {map_thms = @{thms map_sum.simps}, |
85 map_disc_iffs = [], |
85 map_disc_iffs = [], |
|
86 map_sels = [], |
86 rel_injects = @{thms rel_sum_simps(1,4)}, |
87 rel_injects = @{thms rel_sum_simps(1,4)}, |
87 rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}, |
88 rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}, |
88 fp_co_induct_sugar = |
89 fp_co_induct_sugar = |
89 {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), |
90 {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), |
90 common_co_inducts = @{thms sum.induct}, |
91 common_co_inducts = @{thms sum.induct}, |
126 ctr_defs = @{thms Pair_def_alt}, |
127 ctr_defs = @{thms Pair_def_alt}, |
127 ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, |
128 ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, |
128 fp_bnf_sugar = |
129 fp_bnf_sugar = |
129 {map_thms = @{thms map_prod_simp}, |
130 {map_thms = @{thms map_prod_simp}, |
130 map_disc_iffs = [], |
131 map_disc_iffs = [], |
|
132 map_sels = [], |
131 rel_injects = @{thms rel_prod_apply}, |
133 rel_injects = @{thms rel_prod_apply}, |
132 rel_distincts = []}, |
134 rel_distincts = []}, |
133 fp_co_induct_sugar = |
135 fp_co_induct_sugar = |
134 {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
136 {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
135 common_co_inducts = @{thms prod.induct}, |
137 common_co_inducts = @{thms prod.induct}, |