217 val bd_Cnotzeros = map bd_Cnotzero_of_bnf bnfs; |
217 val bd_Cnotzeros = map bd_Cnotzero_of_bnf bnfs; |
218 val bd_Cnotzero = hd bd_Cnotzeros; |
218 val bd_Cnotzero = hd bd_Cnotzeros; |
219 val in_bds = map in_bd_of_bnf bnfs; |
219 val in_bds = map in_bd_of_bnf bnfs; |
220 val in_monos = map in_mono_of_bnf bnfs; |
220 val in_monos = map in_mono_of_bnf bnfs; |
221 val map_comps = map map_comp_of_bnf bnfs; |
221 val map_comps = map map_comp_of_bnf bnfs; |
|
222 val sym_map_comps = map (fn thm => thm RS sym) map_comps; |
222 val map_comp's = map map_comp'_of_bnf bnfs; |
223 val map_comp's = map map_comp'_of_bnf bnfs; |
223 val map_congs = map map_cong_of_bnf bnfs; |
224 val map_congs = map map_cong_of_bnf bnfs; |
|
225 val map_ids = map map_id_of_bnf bnfs; |
224 val map_id's = map map_id'_of_bnf bnfs; |
226 val map_id's = map map_id'_of_bnf bnfs; |
225 val map_wpulls = map map_wpull_of_bnf bnfs; |
227 val map_wpulls = map map_wpull_of_bnf bnfs; |
226 val set_bdss = map set_bd_of_bnf bnfs; |
228 val set_bdss = map set_bd_of_bnf bnfs; |
227 val set_natural'ss = map set_natural'_of_bnf bnfs; |
229 val set_natural'ss = map set_natural'_of_bnf bnfs; |
228 val srel_congs = map srel_cong_of_bnf bnfs; |
230 val srel_congs = map srel_cong_of_bnf bnfs; |
1859 val unfold_fTs = map2 (curry op -->) activeAs Ts; |
1861 val unfold_fTs = map2 (curry op -->) activeAs Ts; |
1860 val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs; |
1862 val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs; |
1861 val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls; |
1863 val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls; |
1862 val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev; |
1864 val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev; |
1863 val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls; |
1865 val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls; |
|
1866 val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs; |
1864 |
1867 |
1865 val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs), |
1868 val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs), |
1866 FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy |
1869 FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy |
1867 |> mk_Frees' "z" Ts |
1870 |> mk_Frees' "z" Ts |
1868 ||>> mk_Frees' "z" Ts' |
1871 ||>> mk_Frees' "z" Ts' |
2124 |
2127 |
2125 fun corec_bind i = Binding.suffix_name ("_" ^ dtor_corecN) (nth bs (i - 1)); |
2128 fun corec_bind i = Binding.suffix_name ("_" ^ dtor_corecN) (nth bs (i - 1)); |
2126 val corec_name = Binding.name_of o corec_bind; |
2129 val corec_name = Binding.name_of o corec_bind; |
2127 val corec_def_bind = rpair [] o Thm.def_binding o corec_bind; |
2130 val corec_def_bind = rpair [] o Thm.def_binding o corec_bind; |
2128 |
2131 |
|
2132 val corec_strs = |
|
2133 map3 (fn dtor => fn sum_s => fn mapx => |
|
2134 mk_sum_case |
|
2135 (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) |
|
2136 dtors corec_ss corec_maps; |
|
2137 |
2129 fun corec_spec i T AT = |
2138 fun corec_spec i T AT = |
2130 let |
2139 let |
2131 val corecT = Library.foldr (op -->) (corec_sTs, AT --> T); |
2140 val corecT = Library.foldr (op -->) (corec_sTs, AT --> T); |
2132 val maps = map3 (fn dtor => fn sum_s => fn mapx => mk_sum_case |
|
2133 (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) |
|
2134 dtors corec_ss corec_maps; |
|
2135 |
2141 |
2136 val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss); |
2142 val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss); |
2137 val rhs = HOLogic.mk_comp (mk_unfold Ts maps i, Inr_const T AT); |
2143 val rhs = HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT); |
2138 in |
2144 in |
2139 mk_Trueprop_eq (lhs, rhs) |
2145 mk_Trueprop_eq (lhs, rhs) |
2140 end; |
2146 end; |
2141 |
2147 |
2142 val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) = |
2148 val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) = |
2172 Goal.prove_sorry lthy [] [] goal |
2178 Goal.prove_sorry lthy [] [] goal |
2173 (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms) |
2179 (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms) |
2174 |> Thm.close_derivation) |
2180 |> Thm.close_derivation) |
2175 goals dtor_unfold_thms map_congs |
2181 goals dtor_unfold_thms map_congs |
2176 end; |
2182 end; |
|
2183 |
|
2184 val corec_unique_mor_thm = |
|
2185 let |
|
2186 val id_fs = map2 (fn T => fn f => mk_sum_case (HOLogic.id_const T, f)) Ts unfold_fs; |
|
2187 val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs corec_strs UNIVs dtors id_fs); |
|
2188 fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i); |
|
2189 val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
2190 (map2 mk_fun_eq unfold_fs ks)); |
|
2191 in |
|
2192 Goal.prove_sorry lthy [] [] |
|
2193 (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique))) |
|
2194 (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm) |
|
2195 |> Thm.close_derivation |
|
2196 end; |
|
2197 |
|
2198 val dtor_corec_unique_thms = |
|
2199 split_conj_thm (split_conj_prems n |
|
2200 (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS corec_unique_mor_thm) |
|
2201 |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_comp_Inl} @ |
|
2202 map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); |
2177 |
2203 |
2178 val ctor_dtor_corec_thms = |
2204 val ctor_dtor_corec_thms = |
2179 map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms; |
2205 map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms; |
2180 |
2206 |
2181 val timer = time (timer "corec definitions & thms"); |
2207 val timer = time (timer "corec definitions & thms"); |
2988 (dtor_corecN, dtor_corec_thms), |
3014 (dtor_corecN, dtor_corec_thms), |
2989 (dtor_ctorN, dtor_ctor_thms), |
3015 (dtor_ctorN, dtor_ctor_thms), |
2990 (dtor_exhaustN, dtor_exhaust_thms), |
3016 (dtor_exhaustN, dtor_exhaust_thms), |
2991 (dtor_injectN, dtor_inject_thms), |
3017 (dtor_injectN, dtor_inject_thms), |
2992 (dtor_unfoldN, dtor_unfold_thms), |
3018 (dtor_unfoldN, dtor_unfold_thms), |
2993 (dtor_unfold_uniqueN, dtor_unfold_unique_thms)] |
3019 (dtor_unfold_uniqueN, dtor_unfold_unique_thms), |
|
3020 (dtor_corec_uniqueN, dtor_corec_unique_thms)] |
2994 |> map (apsnd (map single)) |
3021 |> map (apsnd (map single)) |
2995 |> maps (fn (thmN, thmss) => |
3022 |> maps (fn (thmN, thmss) => |
2996 map2 (fn b => fn thms => |
3023 map2 (fn b => fn thms => |
2997 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
3024 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
2998 bs thmss) |
3025 bs thmss) |