(* ------------------------------------------------------------------------- *)
(* 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