162 set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]], |
162 set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]], |
163 [[[], @{thms snds.intros[of "(a, b)" for a b, unfolded snd_conv]}]]], |
163 [[[], @{thms snds.intros[of "(a, b)" for a b, unfolded snd_conv]}]]], |
164 set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos] |
164 set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos] |
165 snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}}, |
165 snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}}, |
166 fp_co_induct_sugar = |
166 fp_co_induct_sugar = |
167 {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
167 {co_rec = Const (@{const_name uncurry}, (ctr_Ts ---> C) --> fpT --> C), |
168 common_co_inducts = @{thms prod.induct}, |
168 common_co_inducts = @{thms prod.induct}, |
169 co_inducts = @{thms prod.induct}, |
169 co_inducts = @{thms prod.induct}, |
170 co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, |
170 co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, |
171 co_rec_thms = @{thms prod.case}, |
171 co_rec_thms = @{thms prod.case}, |
172 co_rec_discs = [], |
172 co_rec_discs = [], |