equal
deleted
inserted
replaced
24 val add_codetypes_hook_bootstrap: hook -> theory -> theory |
24 val add_codetypes_hook_bootstrap: hook -> theory -> theory |
25 val the_codetypes_mut_specs: theory -> (string * bool) list |
25 val the_codetypes_mut_specs: theory -> (string * bool) list |
26 -> ((string * sort) list * (string * (bool * (string * typ list) list)) list) |
26 -> ((string * sort) list * (string * (bool * (string * typ list) list)) list) |
27 val get_codetypes_arities: theory -> (string * bool) list -> sort |
27 val get_codetypes_arities: theory -> (string * bool) list -> sort |
28 -> (string * (((string * sort list) * sort) * term list)) list option |
28 -> (string * (((string * sort list) * sort) * term list)) list option |
29 val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort |
29 val prove_codetypes_arities: tactic -> (string * bool) list -> sort |
30 -> (((string * sort list) * sort) list -> (string * term list) list -> theory |
30 -> (((string * sort list) * sort) list -> (string * term list) list -> theory |
31 -> ((bstring * attribute list) * term) list * theory) |
31 -> ((bstring * attribute list) * term) list * theory) |
32 -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory) |
32 -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory) |
33 -> theory -> theory |
33 -> theory -> theory |
34 |
34 |
610 in |
610 in |
611 thy |
611 thy |
612 |> not (null arities) ? ( |
612 |> not (null arities) ? ( |
613 f arities css |
613 f arities css |
614 #-> (fn defs => |
614 #-> (fn defs => |
615 ClassPackage.prove_instance_arity tac arities ("", []) defs |
615 ClassPackage.prove_instance_arity tac arities defs |
616 #> after_qed arities css)) |
616 #> after_qed arities css)) |
617 end; |
617 end; |
618 |
618 |
619 |
619 |
620 (* operational equality *) |
620 (* operational equality *) |
629 val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev); |
629 val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev); |
630 in |
630 in |
631 CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy |
631 CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy |
632 end; |
632 end; |
633 in |
633 in |
634 prove_codetypes_arities (K (ClassPackage.intro_classes_tac [])) |
634 prove_codetypes_arities (ClassPackage.intro_classes_tac []) |
635 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
635 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
636 [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs)) |
636 [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs)) |
637 end; |
637 end; |
638 |
638 |
639 |
639 |