1signature Prim_rec = 2sig 3 4 include Abbrev 5 6 (*------------------------------------------------------------------------ 7 Returns the types defined by an axiom. Does not return type 8 operators that are applied to other types that are defined in 9 the axiom. This is a test for detecting nested recursion, where 10 the operator must already have an axiom elsewhere. 11 -------------------------------------------------------------------------*) 12 13 val doms_of_tyaxiom : thm -> hol_type list 14 15 (*------------------------------------------------------------------------ 16 Given a type axiom and the type name, returns the constructors 17 associated with that type in the axiom. 18 -------------------------------------------------------------------------*) 19 20 val type_constructors : thm -> string -> term list 21 val type_constructors_with_args : thm -> string -> term list 22 23 val new_recursive_definition : {name:string, rec_axiom:thm, def:term} -> thm 24 25 (*------------------------------------------------------------------------ 26 Because a type axiom can be for multiple (mutually recursive) types at 27 once, this function returns the definitions of the case constants for 28 each type introduced by an axiom. 29 -------------------------------------------------------------------------*) 30 31 val define_case_constant : thm -> thm list 32 val case_constant_name : {type_name:string} -> string 33 val case_constant_defn_name : {type_name:string} -> string 34 35 val INDUCT_THEN : thm -> thm_tactic -> tactic 36 val prove_rec_fn_exists : thm -> term -> thm 37 val prove_induction_thm : thm -> thm 38 39 (*------------------------------------------------------------------------- 40 Similarly, this function returns a list of theorems where each theorem 41 in the list is the cases theorem for a type characterised in the axiom. 42 -------------------------------------------------------------------------*) 43 44 val prove_cases_thm : thm -> thm list 45 val case_cong_thm : thm -> thm -> thm 46 val prove_constructors_distinct : thm -> thm option list 47 val prove_constructors_one_one : thm -> thm option list 48 val prove_case_rand_thm : {case_def : thm, nchotomy : thm} -> thm 49 val prove_case_elim_thm : {case_def : thm, nchotomy : thm} -> thm 50 val prove_case_eq_thm : {case_def : thm, nchotomy : thm} -> thm 51 52 (* A utility function *) 53 val EXISTS_EQUATION : term -> thm -> thm 54 55end 56