1signature FinalThm =
2sig
3  type thm
4  type tag
5  type term
6  type hol_type
7  type 'a set   = 'a HOLset.set
8  type depdisk  = (string * int) * ((string * int list) list)
9
10  val kernelid : string
11
12  (* Simple operations on the type of theorems *)
13
14  val tag           : thm -> tag
15  val hyp           : thm -> term list
16  val hypset        : thm -> term set
17  val concl         : thm -> term
18  val dest_thm      : thm -> term list * term
19  val thm_frees     : thm -> term list
20  val hyp_frees     : thm -> term set
21  val hyp_tyvars    : thm -> hol_type set
22
23
24  (* The primitive rules of inference *)
25
26  val ASSUME        : term -> thm
27  val REFL          : term -> thm
28  val BETA_CONV     : term -> thm
29  val ABS           : term -> thm -> thm
30  val DISCH         : term -> thm -> thm
31  val MP            : thm -> thm -> thm
32  val SUBST         : (term,thm)Lib.subst -> term -> thm -> thm
33  val INST_TYPE     : (hol_type,hol_type)Lib.subst -> thm -> thm
34
35
36  (* Now some derivable-but-primitive rules of inference *)
37
38
39  (* Lambda calculus rules *)
40
41  val ALPHA         : term -> term -> thm
42  val MK_COMB       : thm * thm -> thm
43  val AP_TERM       : term -> thm -> thm
44  val AP_THM        : thm -> term -> thm
45
46
47  (* Equality *)
48
49  val SYM           : thm -> thm
50  val TRANS         : thm -> thm -> thm
51  val EQ_MP         : thm -> thm -> thm
52  val EQ_IMP_RULE   : thm -> thm * thm
53
54
55  (* Free variable instantiation *)
56
57  val INST          : (term,term)Lib.subst -> thm -> thm
58
59
60  (* Universal quantification *)
61
62  val SPEC          : term -> thm -> thm
63  val GEN           : term -> thm -> thm
64  val GENL          : term list -> thm -> thm
65
66
67  (* Existential quantification *)
68
69  val EXISTS        : term * term -> thm -> thm
70  val CHOOSE        : term * thm -> thm -> thm
71
72
73  (* Conjunction *)
74
75  val CONJ          : thm -> thm -> thm
76  val CONJUNCT1     : thm -> thm
77  val CONJUNCT2     : thm -> thm
78
79
80  (* Disjunction *)
81
82  val DISJ1         : thm -> term -> thm
83  val DISJ2         : term -> thm -> thm
84  val DISJ_CASES    : thm -> thm -> thm -> thm
85
86
87  (* Negation *)
88
89  val NOT_INTRO     : thm -> thm
90  val NOT_ELIM      : thm -> thm
91  val CCONTR        : term -> thm -> thm
92
93
94  (* Computing with explicit substitutions *)
95
96  val Beta          : thm -> thm
97  val Mk_comb       : thm -> thm * thm * (thm -> thm -> thm)
98  val Mk_abs        : thm -> term * thm * (thm -> thm)
99  val Specialize    : term -> thm -> thm
100
101  (* Multiple binders *)
102
103  val GEN_ABS       : term option -> term list -> thm -> thm
104
105  (* Oracle invocation *)
106
107  val mk_thm        : term list * term -> thm
108  val mk_oracle_thm : string -> term list * term -> thm
109  val mk_axiom_thm  : (string Nonce.t * term) -> thm
110  val add_tag       : tag * thm -> thm
111
112  (* definitional rules of inference *)
113  val prim_type_definition : {Thy : string, Tyop : string} * thm -> thm
114  val prim_specification : string -> string list -> thm -> thm
115  val gen_prim_specification : string -> thm -> string list * thm
116
117  (* Fetching theorems from disk *)
118
119  val disk_thm : (depdisk * string list) * term list -> thm
120
121  (* Saving proof dependencies *)
122
123  val save_dep : string -> thm -> thm
124
125end;
126