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