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