equal
deleted
inserted
replaced
80 {ctrXs_Tss = ctr_Tss, |
80 {ctrXs_Tss = ctr_Tss, |
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 rel_injects = @{thms rel_sum_simps(1,4)}, |
86 rel_injects = @{thms rel_sum_simps(1,4)}, |
86 rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}, |
87 rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}, |
87 fp_co_induct_sugar = |
88 fp_co_induct_sugar = |
88 {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), |
89 {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), |
89 common_co_inducts = @{thms sum.induct}, |
90 common_co_inducts = @{thms sum.induct}, |
124 {ctrXs_Tss = [ctr_Ts], |
125 {ctrXs_Tss = [ctr_Ts], |
125 ctr_defs = @{thms Pair_def_alt}, |
126 ctr_defs = @{thms Pair_def_alt}, |
126 ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, |
127 ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, |
127 fp_bnf_sugar = |
128 fp_bnf_sugar = |
128 {map_thms = @{thms map_prod_simp}, |
129 {map_thms = @{thms map_prod_simp}, |
|
130 map_disc_iffs = [], |
129 rel_injects = @{thms rel_prod_apply}, |
131 rel_injects = @{thms rel_prod_apply}, |
130 rel_distincts = []}, |
132 rel_distincts = []}, |
131 fp_co_induct_sugar = |
133 fp_co_induct_sugar = |
132 {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
134 {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
133 common_co_inducts = @{thms prod.induct}, |
135 common_co_inducts = @{thms prod.induct}, |