forked from jrh13/hol-light
-
Notifications
You must be signed in to change notification settings - Fork 0
/
VERYQUICK_REFERENCE.txt
325 lines (310 loc) · 19.3 KB
/
VERYQUICK_REFERENCE.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
(* ------------------------------------------------------------------------- *)
(* Theorems (type thm) *)
(* ------------------------------------------------------------------------- *)
ADD1 |- SUC m = m + 1
ADD_AC |- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
ADD_ASSOC |- m + n + p = (m + n) + p
ADD_CLAUSES |- (!n. 0 + n = n) /\ (!m. m + 0 = m) /\ (!m n. SUC m + n = SUC (m + n)) /\ (!m n. m + SUC n = SUC (m + n))
ADD_SUB |- (m + n) - n = m
ADD_SYM |- m + n = n + m
ALL |- (ALL P [] <=> T) /\ (ALL P (CONS h t) <=> P h /\ ALL P t)
ALL2 |- (ALL2 P [] [] <=> T) /\ ... /\ (ALL2 P (CONS h1 t1) (CONS h2 t2) <=> P h1 h2 /\ ALL2 P t1 t2)
APPEND |- (!l. APPEND [] l = l) /\ (!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))
ARITH |- (NUMERAL 0 = 0 /\ BIT0 _0 = _0) /\ ((!n. SUC (NUMERAL n) = NUMERAL (SUC n)) /\ ...
ARITH_EQ |- (!m n. NUMERAL m = NUMERAL n <=> m = n) /\ (_0 = _0 <=> T) /\ ...
CARD_CLAUSES |- CARD {} = 0 /\ (!x s. FINITE s ==> CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD s)))
CART_EQ |- x = y <=> (!i. 1 <= i /\ i <= dimindex UNIV ==> x $ i = y $ i)
CONJ_ASSOC |- t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3
DE_MORGAN_THM |- (~(t1 /\ t2) <=> ~t1 \/ ~t2) /\ (~(t1 \/ t2) <=> ~t1 /\ ~t2)
DIVISION |- ~(n = 0) ==> m = m DIV n * n + m MOD n /\ m MOD n < n
ETA_AX |- (\x. t x) = t
EVEN |- (EVEN 0 <=> T) /\ (!n. EVEN (SUC n) <=> ~EVEN n)
EXISTS_REFL |- ?x. x = a
EXP |- (!m. m EXP 0 = 1) /\ (!m n. m EXP SUC n = m * m EXP n)
EXTENSION |- s = t <=> (!x. x IN s <=> x IN t)
FACT |- FACT 0 = 1 /\ (!n. FACT (SUC n) = SUC n * FACT n)
FINITE_INDUCT_STRONG |- P {} /\ (!x s. P s /\ ~(x IN s) /\ FINITE s ==> P (x INSERT s)) ==> (!s. FINITE s ==> P s)
FINITE_NUMSEG |- FINITE (m .. n)
FINITE_RULES |- FINITE {} /\ (!x s. FINITE s ==> FINITE (x INSERT s))
FINITE_SUBSET |- FINITE t /\ s SUBSET t ==> FINITE s
FORALL_PAIR_THM |- (!p. P p) <=> (!p1 p2. P (p1,p2))
FUN_EQ_THM |- f = g <=> (!x. f x = g x)
GE |- m >= n <=> n <= m
HAS_SIZE |- s HAS_SIZE n <=> FINITE s /\ CARD s = n
HD |- HD (CONS h t) = h
IMP_IMP |- p ==> q ==> r <=> p /\ q ==> r
IN |- x IN P <=> P x
IN_DELETE |- x IN s DELETE y <=> x IN s /\ ~(x = y)
IN_ELIM_THM |- (!P x. x IN GSPEC (\v. P (SETSPEC v)) <=> P (\p t. p /\ x = t)) /\ ...
IN_IMAGE |- y IN IMAGE f s <=> (?x. y = f x /\ x IN s)
IN_INSERT |- x IN y INSERT s <=> x = y \/ x IN s
IN_INTER |- x IN s INTER t <=> x IN s /\ x IN t
IN_NUMSEG |- p IN m .. n <=> m <= p /\ p <= n
IN_SING |- x IN {y} <=> x = y
IN_UNION |- x IN s UNION t <=> x IN s \/ x IN t
IN_UNIV |- x IN UNIV
LAMBDA_BETA |- 1 <= i /\ i <= dimindex UNIV ==> (lambda) g $ i = g i
LAST |- LAST (CONS h t) = (if t = [] then h else LAST t)
LE |- (!m. m <= 0 <=> m = 0) /\ (!m n. m <= SUC n <=> m = SUC n \/ m <= n)
LEFT_ADD_DISTRIB |- m * (n + p) = m * n + m * p
LEFT_IMP_EXISTS_THM |- (?x. P x) ==> Q <=> (!x. P x ==> Q)
LENGTH |- LENGTH [] = 0 /\ (!h t. LENGTH (CONS h t) = SUC (LENGTH t))
LENGTH_APPEND |- LENGTH (APPEND l m) = LENGTH l + LENGTH m
LE_0 |- 0 <= n
LE_ADD |- m <= m + n
LE_EXISTS |- m <= n <=> (?d. n = m + d)
LE_MULT_LCANCEL |- m * n <= m * p <=> m = 0 \/ n <= p
LE_REFL |- n <= n
LE_TRANS |- m <= n /\ n <= p ==> m <= p
LT |- (!m. m < 0 <=> F) /\ (!m n. m < SUC n <=> m = n \/ m < n)
LT_0 |- 0 < SUC n
LT_REFL |- ~(n < n)
MEM |- (MEM x [] <=> F) /\ (MEM x (CONS h t) <=> x = h \/ MEM x t)
MEMBER_NOT_EMPTY |- (?x. x IN s) <=> ~(s = {})
MONO_EXISTS |- (!x. P x ==> Q x) ==> (?x. P x) ==> (?x. Q x)
MONO_FORALL |- (!x. P x ==> Q x) ==> (!x. P x) ==> (!x. Q x)
MULT_AC |- m * n = n * m /\ (m * n) * p = m * n * p /\ m * n * p = n * m * p
MULT_ASSOC |- m * n * p = (m * n) * p
MULT_CLAUSES |- (!n. 0 * n = 0) /\ ... /\ (!m n. m * SUC n = m + m * n)
MULT_SYM |- m * n = n * m
NOT_CONS_NIL |- ~(CONS h t = [])
NOT_EXISTS_THM |- ~(?x. P x) <=> (!x. ~P x)
NOT_FORALL_THM |- ~(!x. P x) <=> (?x. ~P x)
NOT_IMP |- ~(t1 ==> t2) <=> t1 /\ ~t2
NOT_IN_EMPTY |- ~(x IN {})
NOT_LE |- ~(m <= n) <=> n < m
NOT_LT |- ~(m < n) <=> n <= m
NOT_SUC |- ~(SUC n = 0)
PAIR_EQ |- x,y = a,b <=> x = a /\ y = b
PRE |- PRE 0 = 0 /\ (!n. PRE (SUC n) = n)
REAL_ABS_MUL |- abs (x * y) = abs x * abs y
REAL_ABS_NEG |- abs (--x) = abs x
REAL_ABS_NUM |- abs (&n) = &n
REAL_ABS_POS |- &0 <= abs x
REAL_ABS_POW |- abs (x pow n) = abs x pow n
REAL_ADD_ASSOC |- x + y + z = (x + y) + z
REAL_ADD_LID |- &0 + x = x
REAL_ADD_LINV |- --x + x = &0
REAL_ADD_RID |- x + &0 = x
REAL_ADD_SYM |- x + y = y + x
REAL_ENTIRE |- x * y = &0 <=> x = &0 \/ y = &0
REAL_EQ_IMP_LE |- x = y ==> x <= y
REAL_INV_MUL |- inv (x * y) = inv x * inv y
REAL_LET_TRANS |- x <= y /\ y < z ==> x < z
REAL_LE_LMUL |- &0 <= x /\ y <= z ==> x * y <= x * z
REAL_LE_LT |- x <= y <=> x < y \/ x = y
REAL_LE_REFL |- x <= x
REAL_LE_SQUARE |- &0 <= x * x
REAL_LE_TOTAL |- x <= y \/ y <= x
REAL_LTE_TRANS |- x < y /\ y <= z ==> x < z
REAL_LT_01 |- &0 < &1
REAL_LT_DIV |- &0 < x /\ &0 < y ==> &0 < x / y
REAL_LT_IMP_LE |- x < y ==> x <= y
REAL_LT_IMP_NZ |- &0 < x ==> ~(x = &0)
REAL_LT_LE |- x < y <=> x <= y /\ ~(x = y)
REAL_LT_MUL |- &0 < x /\ &0 < y ==> &0 < x * y
REAL_LT_REFL |- ~(x < x)
REAL_LT_TRANS |- x < y /\ y < z ==> x < z
REAL_MUL_AC |- m * n = n * m /\ (m * n) * p = m * n * p /\ m * n * p = n * m * p
REAL_MUL_ASSOC |- x * y * z = (x * y) * z
REAL_MUL_LID |- &1 * x = x
REAL_MUL_LINV |- ~(x = &0) ==> inv x * x = &1
REAL_MUL_LZERO |- &0 * x = &0
REAL_MUL_RID |- x * &1 = x
REAL_MUL_RINV |- ~(x = &0) ==> x * inv x = &1
REAL_MUL_RZERO |- x * &0 = &0
REAL_MUL_SYM |- x * y = y * x
REAL_NEGNEG |- -- --x = x
REAL_NEG_NEG |- -- --x = x
REAL_NOT_LE |- ~(x <= y) <=> y < x
REAL_NOT_LT |- ~(x < y) <=> y <= x
REAL_OF_NUM_ADD |- &m + &n = &(m + n)
REAL_OF_NUM_EQ |- &m = &n <=> m = n
REAL_OF_NUM_LE |- &m <= &n <=> m <= n
REAL_OF_NUM_LT |- &m < &n <=> m < n
REAL_OF_NUM_MUL |- &m * &n = &(m * n)
REAL_OF_NUM_POW |- &x pow n = &(x EXP n)
REAL_POS |- &0 <= &n
REAL_POW_2 |- x pow 2 = x * x
REAL_POW_ADD |- x pow (m + n) = x pow m * x pow n
REAL_SUB_0 |- x - y = &0 <=> x = y
REAL_SUB_LDISTRIB |- x * (y - z) = x * y - x * z
REAL_SUB_LE |- &0 <= x - y <=> y <= x
REAL_SUB_LT |- &0 < x - y <=> y < x
REAL_SUB_REFL |- x - x = &0
REAL_SUB_RZERO |- x - &0 = x
RIGHT_ADD_DISTRIB |- (m + n) * p = m * p + n * p
RIGHT_FORALL_IMP_THM |- (!x. P ==> Q x) <=> P ==> (!x. Q x)
SKOLEM_THM |- (!x. ?y. P x y) <=> (?y. !x. P x (y x))
SUBSET |- s SUBSET t <=> (!x. x IN s ==> x IN t)
SUC_INJ |- SUC m = SUC n <=> m = n
TL |- TL (CONS h t) = t
TRUTH |- T
(* ------------------------------------------------------------------------- *)
(* Inference rules (result type "thm") *)
(* ------------------------------------------------------------------------- *)
AC th tm Prove equivalence by associativity and commutativity
AP_TERM tm th From |- s = t to |- f s = f t
AP_THM th tm From |- f = g to |- f x = g x
ARITH_RULE tm Linear arithmetic prover over N
ASSUME tm Generate trivial theorem p |- p
BETA_RULE th Reduce all beta-redexes in theorem
CONJ th th From |- p and |- q to |- p /\ q
CONJUNCT1 th From |- p /\ q to |- p
CONJUNCT2 th From |- p /\ q to |- q
CONV_RULE conv th Apply conversion to conclusion of theorem
DISCH tm th From p |- q to |- p ==> q
DISCH_ALL th From p1, ..., pn |- q to |- p1 ==> ... ==> pn ==> q
EQT_ELIM th From |- p <=> T to |- p
EQT_INTRO th From |- p to |- p <=> T
EQ_MP th th From |- p <=> q and |- p to |- q
GEN tm th From |- p[x] to |- !x. p[x]
GENL tml th From |- p[x1,...,xn] to |- !x1 .. xn. p[x1,...,xn]
GEN_ALL th From |- p[x1,...,xn] to |- !x1 .. xn. p[x1,...,xn], all variables
GEN_REWRITE_RULE convfn thl th Rewrite conclusion of theorem using precise depth conversion
GSYM th Switch topmost equations, e.g. from |- !x. s[x] = t[x] to !x. t[x] = s[x]
INST tmtml th Instantiate |- p[x1,...xn] to |- p[t1,...,tn]
INT_ARITH tm Linear arithmetic prover over Z
INT_OF_REAL_THM th Map universal theorem from R to analog over Z
ISPEC tm th From |- !x. p[x] to |- p[t] with type instantiation
ISPECL tml th From |- !x1 .. xn. p[x1,...,xn] to |- p[t1,...,tn] with type instantiation
MATCH_MP th th From |- p ==> q and |- p' to |- q', instantiating first theorem to match
MK_COMB thth From |- f = g and |- x = y to |- f(x) = g(y)
MP th th From |- p ==> q and |- p to |- q, no matching
ONCE_REWRITE_RULE thl th Rewrite conclusion of theorem once at topmost subterms
PART_MATCH tmfn th tm Instantiate theorem by matching part of it to a term
PROVE_HYP th th From |- p and p |- q to |- q
REAL_ARITH tm Linear arithmetic prover over R
REFL tm Produce trivial theorem |- t = t
REWRITE_RULE thl th Rewrite conclusion of theorem with equational theorems
SPEC tm th From |- !x. p[x] to |- p[t]
SPECL tml th From |- !x1 .. xn. p[x1,...,xn] to |- p[t1,...,tn]
SPEC_ALL th From |- !x1 .. xn. p[x1,...,xn] to |- p[x1,...,xn]
SYM th From |- s = t to |- t = s
TAUT tm Prove propositional tautology like `p /\ q ==> p`
TRANS th th From |- s = t and |- t = u and |- s = u
UNDISCH th From |- p ==> q to p |- q
(* ------------------------------------------------------------------------- *)
(* Inference rule with return type "thm list" *)
(* ------------------------------------------------------------------------- *)
CONJUNCTS th From |- p1 /\ ... /\ pn to [|- p1; ...; |- pn]
(* ------------------------------------------------------------------------- *)
(* Conversions (type "conv = term -> thm") *)
(* ------------------------------------------------------------------------- *)
BETA_CONV tm Reduce toplevel beta-redex |- (\x. s[x]) t = s[t]
CONTRAPOS_CONV From `p ==> q` give |- (p ==> q) <=> (~q ==> ~p)
GEN_BETA_CONV Reduce general beta-redex like |- (\(x,y). p[x,y]) (a,b) = p[a,b]
GEN_REWRITE_CONV convfn thl Rewriting conversion using precise depth conversion
NUM_REDUCE_CONV Evaluate numerical expressions over N like `2 + 7 DIV (FACT 3)`
conv ORELSEC conv Try to apply one conversion and if it fails, apply the other
REAL_RAT_REDUCE_CONV Evaluate numerical expressions over R like `&22 / &7 - &3 * &1`
REWRITE_CONV thl Conversion to rewrite a term t to t' giving |- t = t'
REWR_CONV th Conversion to rewrite a term t once at top level giving |- t = t'
SYM_CONV Conversion to switch equations once |- P[s = t] <=> P[t = s]
conv THENC conv Apply one conversion then the other
TOP_DEPTH_CONV conv Apply conversion once to top-level terms
(* ------------------------------------------------------------------------- *)
(* Conversionals (type "conv -> conv") *)
(* ------------------------------------------------------------------------- *)
BINDER_CONV Apply conversion to body of quantifier etc.
LAND_CONV Apply conversion to LHS of binary operator, e.g. `s` in `s + t`
ONCE_DEPTH_CONV Apply conversion to first possible subterms top-down
RAND_CONV Apply conversion to rand of combination, e.g. x in f(x)
RATOR_CONV Apply conversion to rator of combination, e.g. f in f(x)
(* ------------------------------------------------------------------------- *)
(* Tactics (return type "tactic") *)
(* ------------------------------------------------------------------------- *)
ABBREV_TAC tm Introduce abbreviation for t, from ?- p[t] to t = x ?- p[x]
ABS_TAC From ?- (\x. s[x]) = (\x. t[x]) to ?- s[x] = t[x]
ALL_TAC Tactic with no effect
ANTS_TAC From ?- (p ==> q) ==> r to ?- p and ?- q ==> r
AP_TERM_TAC From ?- f s = f t to ?- s = t
AP_THM_TAC From ?- f x = g x to ?- f = g
ARITH_TAC Tactic to solve linear arithmetic over N
ASM_CASES_TAC tm Split ?- q into p ?- q and ~p ?- q
ASM_MESON_TAC thl Tactic for first-order logic including assumptions
ASM_REWRITE_TAC thl Rewrite goal by theorems including assumptions
ASM_SIMP_TAC thl Simplify goal by theorems including assumptions
BETA_TAC Reduce all beta-redexes in conclusion of goal
COND_CASES_TAC From ?- P[if p then x else y] to p ?- p[x] and ~p ?- p[y]
CONJ_TAC Split ?- p /\ q into ?- p and ?- q
CONV_TAC conv Apply conversion to conclusion of goal
DISCH_TAC From ?- p ==> q to p ?- q
DISCH_THEN ttac From ?- p ==> q to ?- q after using |- p
DISJ1_TAC From ?- p \/ q to ?- p
DISJ2_TAC From ?- p \/ q to ?- q
EQ_TAC Split ?- p <=> q into ?- p ==> q and ?- q ==> p
EVERY_ASSUM ttac Apply function to each assumption of goal
EXISTS_TAC tm From ?- ?x. p[x] to ?- p[t]
EXPAND_TAC s Expand an abbreviation in a goal
FIRST_ASSUM ttac Apply function to first possible assumption of goal
FIRST_X_ASSUM ttac Apply function to and remove first possible assumption of goal
GEN_REWRITE_TAC convfn thl Rewrite conclusion of goal using precise depth conversion
GEN_TAC From ?- !x. p[x] to ?- p[x]
INDUCT_TAC Apply ordinary mathematical induction to goal
LIST_INDUCT_TAC Apply list induction to goal
MAP_EVERY atac al Map tactic-producing function over a list of arguments, apply in sequence
MESON_TAC thl Solve goal using first-order automation, ignoring assumptions
ONCE_REWRITE_TAC thl Rewrite conclusion of goal once at topmost subterms
tac ORELSE tac Try to apply one tactic and if it fails, apply the other
POP_ASSUM ttac Remove first assumption of goal and apply function to it
POP_ASSUM_LIST tltac Remove assumptions of goal and apply function to it
REAL_ARITH_TAC Tactic to solve linear arithmetic over R
REFL_TAC Solve trivial goal ?- t = t
REPEAT tac Apply a tactic repeatedly until it fails
REWRITE_TAC thl Rewrite conclusion of goal with equational theorems
RULE_ASSUM_TAC thfn Apply inference rule to all hypotheses of goal
SET_TAC thl Solve trivial set-theoretic goal like `x IN (x INSERT s)`
SIMP_TAC thl Simplify goal by theorems ignoring assumptions
SPEC_TAC tmtm From ?- p[t] to ?- !x. p[x]
STRIP_TAC Break down goal, ?- p /\ q to ?- p and ?- q etc. etc.
SUBGOAL_THEN tm ttac Split off a separate subgoal
TRY tac Try a tactic but do nothing if it fails
tac THEN tac Apply one tactic then the other to all resulting subgoals
tac THENL tacl Apply one tactic then second list to corresponding subgoals
UNDISCH_TAC tm From p ?- q to ?- p ==> q
USE_THEN s ttac Apply function to assumption with particular label
X_GEN_TAC tm From ?- !x. p[x] to ?- p[y] with specified `y`
(* ------------------------------------------------------------------------- *)
(* thm_tactic = thm -> tactic *)
(* ------------------------------------------------------------------------- *)
ACCEPT_TAC Solve goal ?- p by theorem |- p
ANTE_RES_THEN ttac Using |- p ==> q in goal p ?- r apply theorem-tactic to |- q
ASSUME_TAC Given |- p, from ?- q to p ?- q, no label on new assumption
CHOOSE_THEN ttac Using |- ?x. p[x] apply theorem-tactic to |- p[x]
CONJUNCTS_THEN ttac Using |- p /\ q apply theorem-tactic to |- p and |- q
CONJUNCTS_THEN2 ttac ttac Using |- p /\ q apply respective theorem-tactics to |- p and |- q
DISJ_CASES_TAC Use |- p \/ q, from ?- r to p ?- r and q ?- r
DISJ_CASES_THEN ttac Use |- p \/ q, apply theorem-tactic to |- p and |- q separately
LABEL_TAC s Given |- p, from ?- q to p ?- q, labelling new assumption "s"
MATCH_ACCEPT_TAC From |- p[x1,...,xn] solve goal ?- p[t1,...,tn] that's an instance
MATCH_MP_TAC Use |- p ==> q to go from ?- q' to ?- p', instantiation theorem to match
MP_TAC Use |- p to go from ?- q to ?- p ==> q
REPEAT_TCL ttacfn ttac Apply theorem-tactical repeatedly until it fails
STRIP_ASSUME_TAC Break theorem down into pieces and add them as assumptions
SUBST1_TAC Substitute equation in conclusion of goal, no matching
SUBST_ALL_TAC Substitute equation in hypotheses and conclusion of goal, no matching
X_CHOOSE_TAC tm From |- ?x. p[x] and ?- q to p[y] ?- q, specified y
X_CHOOSE_THEN tm ttac From |- ?x. p[x] apply theorem-tactic to |- p[y], specified y
(* ------------------------------------------------------------------------- *)
(* *)
(* ------------------------------------------------------------------------- *)
tm : term
tml : term list
tmtm : term * term
tmtml : (term * term) list
tmfn : term -> term
th : thm
thl : thm list
thth : thm * thm
thfn : thm -> thm
conv : conv
convfn : conv -> conv
tac : tactic
tacl : tactic list
ttac : thm_tactic = thm -> tactic
tltac : thm list -> tactic
ttacfn : thm_tactical = thm_tactic -> thm_tactic
atac : 'a -> tactic
al : 'a list
s : string