equal
deleted
inserted
replaced
2394 split_conj_thm (Skip_Proof.prove lthy [] [] goal |
2394 split_conj_thm (Skip_Proof.prove lthy [] [] goal |
2395 (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm)) |
2395 (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm)) |
2396 |> Thm.close_derivation) |
2396 |> Thm.close_derivation) |
2397 end; |
2397 end; |
2398 |
2398 |
2399 val map_unique_thm = |
2399 val dtor_map_unique_thm = |
2400 let |
2400 let |
2401 fun mk_prem u map dtor dtor' = |
2401 fun mk_prem u map dtor dtor' = |
2402 mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), |
2402 mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), |
2403 HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); |
2403 HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); |
2404 val prems = map4 mk_prem us map_FTFT's dtors dtor's; |
2404 val prems = map4 mk_prem us map_FTFT's dtors dtor's; |
2406 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2406 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
2407 (map2 (curry HOLogic.mk_eq) us fs_maps)); |
2407 (map2 (curry HOLogic.mk_eq) us fs_maps)); |
2408 in |
2408 in |
2409 Skip_Proof.prove lthy [] [] |
2409 Skip_Proof.prove lthy [] [] |
2410 (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) |
2410 (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) |
2411 (mk_map_unique_tac dtor_unfold_unique_thm map_comps) |
2411 (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps) |
2412 |> Thm.close_derivation |
2412 |> Thm.close_derivation |
2413 end; |
2413 end; |
2414 |
2414 |
2415 val timer = time (timer "map functions for the new codatatypes"); |
2415 val timer = time (timer "map functions for the new codatatypes"); |
2416 |
2416 |
2931 val timer = time (timer "additional properties"); |
2931 val timer = time (timer "additional properties"); |
2932 |
2932 |
2933 val ls' = if m = 1 then [0] else ls; |
2933 val ls' = if m = 1 then [0] else ls; |
2934 |
2934 |
2935 val Jbnf_common_notes = |
2935 val Jbnf_common_notes = |
2936 [(map_uniqueN, [fold_maps map_unique_thm])] @ |
2936 [(dtor_map_uniqueN, [fold_maps dtor_map_unique_thm])] @ |
2937 map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms |
2937 map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms |
2938 |> map (fn (thmN, thms) => |
2938 |> map (fn (thmN, thms) => |
2939 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2939 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2940 |
2940 |
2941 val Jbnf_notes = |
2941 val Jbnf_notes = |