7 Codatatype construction. |
7 Codatatype construction. |
8 *) |
8 *) |
9 |
9 |
10 signature BNF_GFP = |
10 signature BNF_GFP = |
11 sig |
11 sig |
12 val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> |
12 val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list -> |
13 binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory -> |
13 binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory -> |
14 BNF_FP.fp_result * local_theory |
14 BNF_FP.fp_result * local_theory |
15 end; |
15 end; |
16 |
16 |
17 structure BNF_GFP : BNF_GFP = |
17 structure BNF_GFP : BNF_GFP = |
53 fun tree_to_coind_wits _ (Wit_Leaf _) = [] |
53 fun tree_to_coind_wits _ (Wit_Leaf _) = [] |
54 | tree_to_coind_wits lwitss (Wit_Node ((i, nwit, I), subtrees)) = |
54 | tree_to_coind_wits lwitss (Wit_Node ((i, nwit, I), subtrees)) = |
55 ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; |
55 ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; |
56 |
56 |
57 (*all BNFs have the same lives*) |
57 (*all BNFs have the same lives*) |
58 fun construct_gfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy = |
58 fun construct_gfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy = |
59 let |
59 let |
60 val timer = time (Timer.startRealTimer ()); |
60 val timer = time (Timer.startRealTimer ()); |
61 |
61 |
62 val note_all = Config.get lthy bnf_note_all; |
62 val note_all = Config.get lthy bnf_note_all; |
63 |
63 |
2893 |> map (apsnd (map snd o minimize_wits)); |
2893 |> map (apsnd (map snd o minimize_wits)); |
2894 |
2894 |
2895 val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs); |
2895 val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs); |
2896 |
2896 |
2897 val (Jbnfs, lthy) = |
2897 val (Jbnfs, lthy) = |
2898 fold_map7 (fn tacs => fn b => fn set_bs => fn mapx => fn sets => fn T => |
2898 fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T => |
2899 fn (thms, wits) => fn lthy => |
2899 fn (thms, wits) => fn lthy => |
2900 bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) set_bs |
2900 bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b |
2901 (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy |
2901 set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) |
|
2902 lthy |
2902 |> register_bnf (Local_Theory.full_name lthy b)) |
2903 |> register_bnf (Local_Theory.full_name lthy b)) |
2903 tacss bs set_bss fs_maps setss_by_bnf Ts all_witss lthy; |
2904 tacss bs map_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy; |
2904 |
2905 |
2905 val fold_maps = fold_thms lthy (map (fn bnf => |
2906 val fold_maps = fold_thms lthy (map (fn bnf => |
2906 mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs); |
2907 mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs); |
2907 |
2908 |
2908 val fold_sets = fold_thms lthy (maps (fn bnf => |
2909 val fold_sets = fold_thms lthy (maps (fn bnf => |