equal
deleted
inserted
replaced
79 |
79 |
80 (* datatype operations *) |
80 (* datatype operations *) |
81 type cns_info = (term * typ * typ list * bool list) list |
81 type cns_info = (term * typ * typ list * bool list) list |
82 |
82 |
83 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
83 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
84 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
|
85 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
84 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
86 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info |
|
87 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
|
88 |
85 |
89 (* tactics for function package *) |
86 (* tactics for function package *) |
90 val size_simpset: simpset |
87 val size_simpset: simpset |
91 val pat_completeness_simp: thm list -> Proof.context -> tactic |
88 val pat_completeness_simp: thm list -> Proof.context -> tactic |
92 val prove_termination_ind: Proof.context -> int -> tactic |
89 val prove_termination_ind: Proof.context -> int -> tactic |
315 |
312 |
316 (* returns the type of the nth datatype *) |
313 (* returns the type of the nth datatype *) |
317 fun all_dtyps descr sorts = |
314 fun all_dtyps descr sorts = |
318 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
315 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
319 |
316 |
320 fun nth_dtyp descr sorts n = |
|
321 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); |
|
322 |
|
323 (* returns info about constructors in a datatype *) |
317 (* returns info about constructors in a datatype *) |
324 fun all_dtyp_constrs_info descr = |
318 fun all_dtyp_constrs_info descr = |
325 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
319 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
326 |
320 |
327 (* returns the constants of the constructors plus the |
321 (* returns the constants of the constructors plus the |
338 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
332 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
339 end |
333 end |
340 in |
334 in |
341 map (map aux) (all_dtyp_constrs_info descr) |
335 map (map aux) (all_dtyp_constrs_info descr) |
342 end |
336 end |
343 |
|
344 fun nth_dtyp_constrs_types descr sorts n = |
|
345 nth (all_dtyp_constrs_types descr sorts) n |
|
346 |
|
347 |
|
348 (* generates for every datatype a name str ^ dt_name |
|
349 plus and index for multiple occurences of a string *) |
|
350 fun prefix_dt_names descr sorts str = |
|
351 let |
|
352 fun get_nth_name (i, _) = |
|
353 Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) |
|
354 in |
|
355 Datatype_Prop.indexify_names |
|
356 (map (prefix str o get_nth_name) descr) |
|
357 end |
|
358 |
|
359 |
|
360 |
337 |
361 (** function package tactics **) |
338 (** function package tactics **) |
362 |
339 |
363 fun pat_completeness_simp simps lthy = |
340 fun pat_completeness_simp simps lthy = |
364 let |
341 let |