39 val fold_union: term list -> term |
39 val fold_union: term list -> term |
40 val mk_conj: term * term -> term |
40 val mk_conj: term * term -> term |
41 val fold_conj: term list -> term |
41 val fold_conj: term list -> term |
42 |
42 |
43 (* datatype operations *) |
43 (* datatype operations *) |
|
44 type cns_info = (term * typ * typ list * bool list) list |
|
45 |
44 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
46 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
45 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
47 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
46 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
48 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
47 (term * typ * typ list * bool list) list list |
49 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info |
48 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> |
|
49 (term * typ * typ list * bool list) list |
|
50 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
50 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
51 |
51 |
52 (* tactics for function package *) |
52 (* tactics for function package *) |
53 val pat_completeness_auto: Proof.context -> tactic |
53 val pat_completeness_auto: Proof.context -> tactic |
54 val pat_completeness_simp: thm list -> Proof.context -> tactic |
54 val pat_completeness_simp: thm list -> Proof.context -> tactic |
128 |
128 |
129 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
129 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
130 |
130 |
131 (** datatypes **) |
131 (** datatypes **) |
132 |
132 |
|
133 (* constructor infos *) |
|
134 type cns_info = (term * typ * typ list * bool list) list |
133 |
135 |
134 (* returns the type of the nth datatype *) |
136 (* returns the type of the nth datatype *) |
135 fun all_dtyps descr sorts = |
137 fun all_dtyps descr sorts = |
136 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
138 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
137 |
139 |