2009 (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique))) |
2009 (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique))) |
2010 (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm) |
2010 (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm) |
2011 |> Thm.close_derivation |
2011 |> Thm.close_derivation |
2012 end; |
2012 end; |
2013 |
2013 |
|
2014 val map_id0s_o_id = |
|
2015 map (fn thm => |
|
2016 mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_o}) |
|
2017 map_id0s; |
|
2018 |
2014 val (dtor_corec_unique_thms, dtor_corec_unique_thm) = |
2019 val (dtor_corec_unique_thms, dtor_corec_unique_thm) = |
2015 `split_conj_thm (split_conj_prems n |
2020 `split_conj_thm (split_conj_prems n |
2016 (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) |
2021 (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) |
2017 |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o id_apply o_assoc sum_case_o_inj(1)} @ |
2022 |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ |
2018 map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); |
2023 map_id0s_o_id @ sym_map_comps) |
|
2024 OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); |
2019 |
2025 |
2020 val timer = time (timer "corec definitions & thms"); |
2026 val timer = time (timer "corec definitions & thms"); |
2021 |
2027 |
2022 val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) = |
2028 val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) = |
2023 let |
2029 let |