equal
deleted
inserted
replaced
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 map_sels = [], |
87 rel_injects = @{thms rel_sum_simps(1,4)}, |
87 rel_injects = @{thms rel_sum_simps(1,4)}, |
88 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]]}, |
|
89 rel_sels = []}, |
89 fp_co_induct_sugar = |
90 fp_co_induct_sugar = |
90 {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), |
91 {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), |
91 common_co_inducts = @{thms sum.induct}, |
92 common_co_inducts = @{thms sum.induct}, |
92 co_inducts = @{thms sum.induct}, |
93 co_inducts = @{thms sum.induct}, |
93 co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]}, |
94 co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]}, |
129 fp_bnf_sugar = |
130 fp_bnf_sugar = |
130 {map_thms = @{thms map_prod_simp}, |
131 {map_thms = @{thms map_prod_simp}, |
131 map_disc_iffs = [], |
132 map_disc_iffs = [], |
132 map_sels = [], |
133 map_sels = [], |
133 rel_injects = @{thms rel_prod_apply}, |
134 rel_injects = @{thms rel_prod_apply}, |
134 rel_distincts = []}, |
135 rel_distincts = [], |
|
136 rel_sels = []}, |
135 fp_co_induct_sugar = |
137 fp_co_induct_sugar = |
136 {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
138 {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
137 common_co_inducts = @{thms prod.induct}, |
139 common_co_inducts = @{thms prod.induct}, |
138 co_inducts = @{thms prod.induct}, |
140 co_inducts = @{thms prod.induct}, |
139 co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, |
141 co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, |