6 Composition of bounded natural functors. |
6 Composition of bounded natural functors. |
7 *) |
7 *) |
8 |
8 |
9 signature BNF_COMP = |
9 signature BNF_COMP = |
10 sig |
10 sig |
11 val ID_bnf: BNF_Def.BNF |
11 val ID_bnf: BNF_Def.bnf |
12 val DEADID_bnf: BNF_Def.BNF |
12 val DEADID_bnf: BNF_Def.bnf |
13 |
13 |
14 type unfold_set |
14 type unfold_set |
15 val empty_unfolds: unfold_set |
15 val empty_unfolds: unfold_set |
16 |
16 |
17 val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> |
17 val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> |
18 ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context -> |
18 ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context -> |
19 (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context) |
19 (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context) |
20 val default_comp_sort: (string * sort) list list -> (string * sort) list |
20 val default_comp_sort: (string * sort) list list -> (string * sort) list |
21 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> |
21 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> |
22 (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context -> |
22 (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context -> |
23 (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context)) |
23 (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context)) |
24 val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> |
24 val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.bnf -> Proof.context -> |
25 (BNF_Def.BNF * typ list) * local_theory |
25 (BNF_Def.bnf * typ list) * local_theory |
26 end; |
26 end; |
27 |
27 |
28 structure BNF_Comp : BNF_COMP = |
28 structure BNF_Comp : BNF_COMP = |
29 struct |
29 struct |
30 |
30 |