2176 val ctor_dtor_corec_thms = |
2176 val ctor_dtor_corec_thms = |
2177 map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms; |
2177 map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms; |
2178 |
2178 |
2179 val timer = time (timer "corec definitions & thms"); |
2179 val timer = time (timer "corec definitions & thms"); |
2180 |
2180 |
2181 val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, pred_coinduct_thm, |
2181 val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, rel_coinduct_thm, |
2182 dtor_strong_coinduct_thm, srel_strong_coinduct_thm, pred_strong_coinduct_thm) = |
2182 dtor_strong_coinduct_thm, srel_strong_coinduct_thm, rel_strong_coinduct_thm) = |
2183 let |
2183 let |
2184 val zs = Jzs1 @ Jzs2; |
2184 val zs = Jzs1 @ Jzs2; |
2185 val frees = phis @ zs; |
2185 val frees = phis @ zs; |
2186 |
2186 |
2187 fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_diag passive_UNIVs; |
2187 fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_diag passive_UNIVs; |
2267 (fold_rev Logic.all zs (Logic.list_implies (dtor_upto_prems, concl))) |
2267 (fold_rev Logic.all zs (Logic.list_implies (dtor_upto_prems, concl))) |
2268 (K (mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def |
2268 (K (mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def |
2269 (tcoalg_thm RS bis_diag_thm)))) |
2269 (tcoalg_thm RS bis_diag_thm)))) |
2270 |> Thm.close_derivation; |
2270 |> Thm.close_derivation; |
2271 |
2271 |
2272 val pred_of_srel_thms = |
2272 val rel_of_srel_thms = |
2273 srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv}; |
2273 srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv}; |
2274 |
2274 |
2275 val pred_coinduct = unfold_thms lthy pred_of_srel_thms srel_coinduct; |
2275 val rel_coinduct = unfold_thms lthy rel_of_srel_thms srel_coinduct; |
2276 val pred_strong_coinduct = unfold_thms lthy pred_of_srel_thms srel_strong_coinduct; |
2276 val rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms srel_strong_coinduct; |
2277 in |
2277 in |
2278 (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), srel_coinduct, pred_coinduct, |
2278 (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), srel_coinduct, rel_coinduct, |
2279 dtor_strong_coinduct, srel_strong_coinduct, pred_strong_coinduct) |
2279 dtor_strong_coinduct, srel_strong_coinduct, rel_strong_coinduct) |
2280 end; |
2280 end; |
2281 |
2281 |
2282 val timer = time (timer "coinduction"); |
2282 val timer = time (timer "coinduction"); |
2283 |
2283 |
2284 (*register new codatatypes as BNFs*) |
2284 (*register new codatatypes as BNFs*) |
2880 val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss; |
2880 val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss; |
2881 val set_induct_thms = map fold_sets hset_induct_thms; |
2881 val set_induct_thms = map fold_sets hset_induct_thms; |
2882 |
2882 |
2883 val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2883 val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2884 val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs; |
2884 val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs; |
2885 val preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2885 val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
2886 val Jpreds = map (mk_pred_of_bnf deads passiveAs passiveBs) Jbnfs; |
2886 val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; |
2887 |
2887 |
2888 val JrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels; |
2888 val JrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels; |
2889 val relRs = map (fn srel => Term.list_comb (srel, JRs @ JrelRs)) srels; |
2889 val relRs = map (fn srel => Term.list_comb (srel, JRs @ JrelRs)) srels; |
2890 val Jpredphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jpreds; |
2890 val Jpredphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jrels; |
2891 val predphis = map (fn srel => Term.list_comb (srel, Jphis @ Jpredphis)) preds; |
2891 val predphis = map (fn srel => Term.list_comb (srel, Jphis @ Jpredphis)) rels; |
2892 |
2892 |
2893 val in_srels = map in_srel_of_bnf bnfs; |
2893 val in_srels = map in_srel_of_bnf bnfs; |
2894 val in_Jsrels = map in_srel_of_bnf Jbnfs; |
2894 val in_Jsrels = map in_srel_of_bnf Jbnfs; |
2895 val Jsrel_defs = map srel_def_of_bnf Jbnfs; |
2895 val Jsrel_defs = map srel_def_of_bnf Jbnfs; |
2896 val Jpred_defs = map pred_def_of_bnf Jbnfs; |
2896 val Jrel_defs = map rel_def_of_bnf Jbnfs; |
2897 |
2897 |
2898 val folded_map_simp_thms = map fold_maps map_simp_thms; |
2898 val folded_map_simp_thms = map fold_maps map_simp_thms; |
2899 val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; |
2899 val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; |
2900 val folded_set_simp_thmss' = transpose folded_set_simp_thmss; |
2900 val folded_set_simp_thmss' = transpose folded_set_simp_thmss; |
2901 |
2901 |
2915 |> Thm.close_derivation) |
2915 |> Thm.close_derivation) |
2916 ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' |
2916 ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' |
2917 dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss |
2917 dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss |
2918 end; |
2918 end; |
2919 |
2919 |
2920 val Jpred_simp_thms = |
2920 val Jrel_simp_thms = |
2921 let |
2921 let |
2922 fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) |
2922 fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) |
2923 (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz'))); |
2923 (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz'))); |
2924 val goals = map6 mk_goal Jzs Jz's dtors dtor's Jpredphis predphis; |
2924 val goals = map6 mk_goal Jzs Jz's dtors dtor's Jpredphis predphis; |
2925 in |
2925 in |
2926 map3 (fn goal => fn srel_def => fn Jsrel_simp => |
2926 map3 (fn goal => fn srel_def => fn Jsrel_simp => |
2927 Skip_Proof.prove lthy [] [] goal |
2927 Skip_Proof.prove lthy [] [] goal |
2928 (mk_pred_simp_tac srel_def Jpred_defs Jsrel_defs Jsrel_simp) |
2928 (mk_rel_simp_tac srel_def Jrel_defs Jsrel_defs Jsrel_simp) |
2929 |> Thm.close_derivation) |
2929 |> Thm.close_derivation) |
2930 goals srel_defs Jsrel_simp_thms |
2930 goals srel_defs Jsrel_simp_thms |
2931 end; |
2931 end; |
2932 |
2932 |
2933 val timer = time (timer "additional properties"); |
2933 val timer = time (timer "additional properties"); |
2940 |> map (fn (thmN, thms) => |
2940 |> map (fn (thmN, thms) => |
2941 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2941 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2942 |
2942 |
2943 val Jbnf_notes = |
2943 val Jbnf_notes = |
2944 [(map_simpsN, map single folded_map_simp_thms), |
2944 [(map_simpsN, map single folded_map_simp_thms), |
2945 (pred_simpN, map single Jpred_simp_thms), |
2945 (rel_simpN, map single Jrel_simp_thms), |
2946 (set_inclN, set_incl_thmss), |
2946 (set_inclN, set_incl_thmss), |
2947 (set_set_inclN, map flat set_set_incl_thmsss), |
2947 (set_set_inclN, map flat set_set_incl_thmsss), |
2948 (srel_simpN, map single Jsrel_simp_thms)] @ |
2948 (srel_simpN, map single Jsrel_simp_thms)] @ |
2949 map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss |
2949 map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss |
2950 |> maps (fn (thmN, thmss) => |
2950 |> maps (fn (thmN, thmss) => |
2956 end; |
2956 end; |
2957 |
2957 |
2958 val common_notes = |
2958 val common_notes = |
2959 [(dtor_coinductN, [dtor_coinduct_thm]), |
2959 [(dtor_coinductN, [dtor_coinduct_thm]), |
2960 (dtor_strong_coinductN, [dtor_strong_coinduct_thm]), |
2960 (dtor_strong_coinductN, [dtor_strong_coinduct_thm]), |
2961 (pred_coinductN, [pred_coinduct_thm]), |
2961 (rel_coinductN, [rel_coinduct_thm]), |
2962 (pred_strong_coinductN, [pred_strong_coinduct_thm]), |
2962 (rel_strong_coinductN, [rel_strong_coinduct_thm]), |
2963 (srel_coinductN, [srel_coinduct_thm]), |
2963 (srel_coinductN, [srel_coinduct_thm]), |
2964 (srel_strong_coinductN, [srel_strong_coinduct_thm])] |
2964 (srel_strong_coinductN, [srel_strong_coinduct_thm])] |
2965 |> map (fn (thmN, thms) => |
2965 |> map (fn (thmN, thms) => |
2966 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2966 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2967 |
2967 |