79 val mk_full_horn: (string * typ) list -> term list -> term -> term |
79 val mk_full_horn: (string * typ) list -> term list -> term -> term |
80 |
80 |
81 (* datatype operations *) |
81 (* datatype operations *) |
82 type cns_info = (term * typ * typ list * bool list) list |
82 type cns_info = (term * typ * typ list * bool list) list |
83 |
83 |
84 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
84 val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list |
85 |
85 |
86 (* tactics for function package *) |
86 (* tactics for function package *) |
87 val size_simpset: simpset |
87 val size_simpset: simpset |
88 val pat_completeness_simp: thm list -> Proof.context -> tactic |
88 val pat_completeness_simp: thm list -> Proof.context -> tactic |
89 val prove_termination_ind: Proof.context -> int -> tactic |
89 val prove_termination_ind: Proof.context -> int -> tactic |
317 fun all_dtyp_constrs_info descr = |
317 fun all_dtyp_constrs_info descr = |
318 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
318 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
319 |
319 |
320 (* returns the constants of the constructors plus the |
320 (* returns the constants of the constructors plus the |
321 corresponding type and types of arguments *) |
321 corresponding type and types of arguments *) |
322 fun all_dtyp_constrs_types descr sorts = |
322 fun all_dtyp_constrs_types descr = |
323 let |
323 let |
324 fun aux ((ty_name, vs), (cname, args)) = |
324 fun aux ((ty_name, vs), (cname, args)) = |
325 let |
325 let |
326 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs |
326 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr) vs |
327 val ty = Type (ty_name, vs_tys) |
327 val ty = Type (ty_name, vs_tys) |
328 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args |
328 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr) args |
329 val is_rec = map Datatype_Aux.is_rec_type args |
329 val is_rec = map Datatype_Aux.is_rec_type args |
330 in |
330 in |
331 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
331 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
332 end |
332 end |
333 in |
333 in |