Theory: arithmetic

Parents

• prim_rec

Types

Constants

• *  :num -> num -> num
• +  :num -> num -> num
• -  :num -> num -> num
• >  :num -> num -> bool
• EVEN  :num -> bool
• FUNPOW  :('a -> 'a) -> num -> 'a -> 'a
• <=  :num -> num -> bool
• >=  :num -> num -> bool
• NUMERAL  :num -> num
• ALT_ZERO  :num
• NUMERAL_BIT1  :num -> num
• NUMERAL_BIT2  :num -> num
• num_case  :'a -> (num -> 'a) -> num -> 'a
• DIV  :num -> num -> num
• EXP  :num -> num -> num
• ODD  :num -> bool
• MOD  :num -> num -> num
• nat_elim__magic  :num -> num
• FACT  :num -> num

Definitions

ADD

|- (!n. 0 + n = n) /\ !m n. SUC m + n = SUC (m + n)

ALT_ZERO

|- ALT_ZERO = 0

DIVISION

|- !n. 0 < n ==> !k. (k = k DIV n * n + k MOD n) /\ k MOD n < n

EVEN

|- (EVEN 0 = T) /\ !n. EVEN (SUC n) = ~EVEN n

EXP

|- (!m. m ** 0 = 1) /\ !m n. m ** SUC n = m * m ** n

FACT

|- (FACT 0 = 1) /\ !n. FACT (SUC n) = SUC n * FACT n

FUNPOW

|- (!f x. FUNPOW f 0 x = x) /\ !f n x. FUNPOW f (SUC n) x = FUNPOW f n (f x)

GREATER_DEF

|- !m n. m > n = n < m

GREATER_OR_EQ

|- !m n. m >= n = m > n \/ (m = n)

LESS_OR_EQ

|- !m n. m <= n = m < n \/ (m = n)

MULT

|- (!n. 0 * n = 0) /\ !m n. SUC m * n = m * n + n

nat_elim__magic

|- !n. & n = n

num_case_def

|- (!b f. num_case b f 0 = b) /\ !b f n. num_case b f (SUC n) = f n

NUMERAL_BIT1

|- !n. NUMERAL_BIT1 n = n + (n + SUC 0)

NUMERAL_BIT2

|- !n. NUMERAL_BIT2 n = n + (n + SUC (SUC 0))

NUMERAL_DEF

|- !x. NUMERAL x = x

ODD

|- (ODD 0 = F) /\ !n. ODD (SUC n) = ~ODD n

SUB

|- (!m. 0 - m = 0) /\ !m n. SUC m - n = (if m < n then 0 else SUC (m - n))

Theorems

ADD1

|- !m. SUC m = m + 1

ADD_0

|- !m. m + 0 = m

ADD_ASSOC

|- !m n p. m + (n + p) = m + n + p

ADD_CLAUSES

|- (0 + m = m) /\ (m + 0 = m) /\ (SUC m + n = SUC (m + n)) /\
   (m + SUC n = SUC (m + n))

ADD_COMM

|- !m n. m + n = n + m

ADD_DIV_ADD_DIV

|- !n. 0 < n ==> !x r. (x * n + r) DIV n = x + r DIV n

ADD_EQ_0

|- !m n. (m + n = 0) = (m = 0) /\ (n = 0)

ADD_EQ_1

|- !m n. (m + n = 1) = (m = 1) /\ (n = 0) \/ (m = 0) /\ (n = 1)

ADD_EQ_SUB

|- !m n p. n <= p ==> ((m + n = p) = (m = p - n))

ADD_INV_0

|- !m n. (m + n = m) ==> (n = 0)

ADD_INV_0_EQ

|- !m n. (m + n = m) = (n = 0)

ADD_MONO_LESS_EQ

|- !m n p. m + n <= m + p = n <= p

ADD_SUB

|- !a c. a + c - c = a

ADD_SUC

|- !m n. SUC (m + n) = m + SUC n

ADD_SYM

|- !m n. m + n = n + m

CANCEL_SUB

|- !p n m. p <= n /\ p <= m ==> ((n - p = m - p) = (n = m))

COMPLETE_INDUCTION

|- !P. (!n. (!m. m < n ==> P m) ==> P n) ==> !n. P n

DA

|- !k n. 0 < n ==> ?r q. (k = q * n + r) /\ r < n

DIV_DIV_DIV_MULT

|- !m n. 0 < m /\ 0 < n ==> !x. x DIV m DIV n = x DIV (m * n)

DIV_LESS

|- !n d. 0 < n /\ 1 < d ==> n DIV d < n

DIV_LESS_EQ

|- !n. 0 < n ==> !k. k DIV n <= k

DIV_MULT

|- !n r. r < n ==> !q. (q * n + r) DIV n = q

DIV_ONE

|- !q. q DIV SUC 0 = q

DIV_UNIQUE

|- !n k q. (?r. (k = q * n + r) /\ r < n) ==> (k DIV n = q)

DIVMOD_ID

|- !n. 0 < n ==> (n DIV n = 1) /\ (n MOD n = 0)

EQ_ADD_LCANCEL

|- !m n p. (m + n = m + p) = (n = p)

EQ_ADD_RCANCEL

|- !m n p. (m + p = n + p) = (m = n)

EQ_LESS_EQ

|- !m n. (m = n) = m <= n /\ n <= m

EQ_MONO_ADD_EQ

|- !m n p. (m + p = n + p) = (m = n)

EQ_MULT_LCANCEL

|- !m n p. (m * n = m * p) = (m = 0) \/ (n = p)

EVEN_ADD

|- !m n. EVEN (m + n) = (EVEN m = EVEN n)

EVEN_AND_ODD

|- !n. ~(EVEN n /\ ODD n)

EVEN_DOUBLE

|- !n. EVEN (2 * n)

EVEN_EXISTS

|- !n. EVEN n = ?m. n = 2 * m

EVEN_MULT

|- !m n. EVEN (m * n) = EVEN m \/ EVEN n

EVEN_ODD

|- !n. EVEN n = ~ODD n

EVEN_ODD_EXISTS

|- !n. (EVEN n ==> ?m. n = 2 * m) /\ (ODD n ==> ?m. n = SUC (2 * m))

EVEN_OR_ODD

|- !n. EVEN n \/ ODD n

EXISTS_GREATEST

|- !P. (?x. P x) /\ (?x. !y. y > x ==> ~P y) = ?x. P x /\ !y. y > x ==> ~P y

EXP_1

|- !n. (1 ** n = 1) /\ (n ** 1 = n)

EXP_ADD

|- !p q n. n ** (p + q) = n ** p * n ** q

EXP_ALWAYS_BIG_ENOUGH

|- !b. 1 < b ==> !n. ?m. n <= b ** m

EXP_EQ_0

|- !n m. (n ** m = 0) = (n = 0) /\ 0 < m

EXP_EQ_1

|- !n m. (n ** m = 1) = (n = 1) \/ (m = 0)

EXP_INJECTIVE

|- !b. 1 < b ==> !n m. (b ** n = b ** m) = (n = m)

FACT_LESS

|- !n. 0 < FACT n

FUN_EQ_LEMMA

|- !f x1 x2. f x1 /\ ~f x2 ==> ~(x1 = x2)

GREATER_EQ

|- !n m. n >= m = m <= n

INV_PRE_EQ

|- !m n. 0 < m /\ 0 < n ==> ((PRE m = PRE n) = (m = n))

INV_PRE_LESS

|- !m. 0 < m ==> !n. PRE m < PRE n = m < n

INV_PRE_LESS_EQ

|- !n. 0 < n ==> !m. PRE m <= PRE n = m <= n

LE

|- (!n. n <= 0 = (n = 0)) /\ !m n. m <= SUC n = (m = SUC n) \/ m <= n

LEFT_ADD_DISTRIB

|- !m n p. p * (m + n) = p * m + p * n

LEFT_SUB_DISTRIB

|- !m n p. p * (m - n) = p * m - p * n

LESS_0_CASES

|- !m. (0 = m) \/ 0 < m

LESS_ADD

|- !m n. n < m ==> ?p. p + n = m

LESS_ADD_1

|- !m n. n < m ==> ?p. m = n + (p + 1)

LESS_ADD_NONZERO

|- !m n. ~(n = 0) ==> m < m + n

LESS_ADD_SUC

|- !m n. m < m + SUC n

LESS_ANTISYM

|- !m n. ~(m < n /\ n < m)

LESS_CASES

|- !m n. m < n \/ n <= m

LESS_CASES_IMP

|- !m n. ~(m < n) /\ ~(m = n) ==> n < m

LESS_DIV_EQ_ZERO

|- !r n. r < n ==> (r DIV n = 0)

LESS_EQ

|- !m n. m < n = SUC m <= n

LESS_EQ_0

|- !n. n <= 0 = (n = 0)

LESS_EQ_ADD

|- !m n. m <= m + n

LESS_EQ_ADD_SUB

|- !c b. c <= b ==> !a. a + b - c = a + (b - c)

LESS_EQ_ANTISYM

|- !m n. ~(m < n /\ n <= m)

LESS_EQ_CASES

|- !m n. m <= n \/ n <= m

LESS_EQ_EXISTS

|- !m n. m <= n = ?p. n = m + p

LESS_EQ_IMP_LESS_SUC

|- !n m. n <= m ==> n < SUC m

LESS_EQ_LESS_EQ_MONO

|- !m n p q. m <= p /\ n <= q ==> m + n <= p + q

LESS_EQ_LESS_TRANS

|- !m n p. m <= n /\ n < p ==> m < p

LESS_EQ_MONO

|- !n m. SUC n <= SUC m = n <= m

LESS_EQ_MONO_ADD_EQ

|- !m n p. m + p <= n + p = m <= n

LESS_EQ_REFL

|- !m. m <= m

LESS_EQ_SUB_LESS

|- !a b. b <= a ==> !c. a - b < c = a < b + c

LESS_EQ_SUC_REFL

|- !m. m <= SUC m

LESS_EQ_TRANS

|- !m n p. m <= n /\ n <= p ==> m <= p

LESS_EQUAL_ADD

|- !m n. m <= n ==> ?p. n = m + p

LESS_EQUAL_ANTISYM

|- !n m. n <= m /\ m <= n ==> (n = m)

LESS_EXP_SUC_MONO

|- !n m. SUC (SUC m) ** n < SUC (SUC m) ** SUC n

LESS_IMP_LESS_ADD

|- !n m. n < m ==> !p. n < m + p

LESS_IMP_LESS_OR_EQ

|- !m n. m < n ==> m <= n

LESS_LESS_CASES

|- !m n. (m = n) \/ m < n \/ n < m

LESS_LESS_EQ_TRANS

|- !m n p. m < n /\ n <= p ==> m < p

LESS_LESS_SUC

|- !m n. ~(m < n /\ n < SUC m)

LESS_MOD

|- !n k. k < n ==> (k MOD n = k)

LESS_MONO_ADD

|- !m n p. m < n ==> m + p < n + p

LESS_MONO_ADD_EQ

|- !m n p. m + p < n + p = m < n

LESS_MONO_ADD_INV

|- !m n p. m + p < n + p ==> m < n

LESS_MONO_EQ

|- !m n. SUC m < SUC n = m < n

LESS_MONO_MULT

|- !m n p. m <= n ==> m * p <= n * p

LESS_MONO_REV

|- !m n. SUC m < SUC n ==> m < n

LESS_MULT2

|- !m n. 0 < m /\ 0 < n ==> 0 < m * n

LESS_MULT_MONO

|- !m i n. SUC n * m < SUC n * i = m < i

LESS_NOT_SUC

|- !m n. m < n /\ ~(n = SUC m) ==> SUC m < n

LESS_OR

|- !m n. m < n ==> SUC m <= n

LESS_OR_EQ_ADD

|- !n m. n < m \/ ?p. n = p + m

LESS_SUB_ADD_LESS

|- !n m i. i < n - m ==> i + m < n

LESS_SUC_EQ_COR

|- !m n. m < n /\ ~(SUC m = n) ==> SUC m < n

LESS_SUC_NOT

|- !m n. m < n ==> ~(n < SUC m)

LESS_TRANS

|- !m n p. m < n /\ n < p ==> m < p

MOD_EQ_0

|- !n. 0 < n ==> !k. (k * n) MOD n = 0

MOD_MOD

|- !n. 0 < n ==> !k. k MOD n MOD n = k MOD n

MOD_MULT

|- !n r. r < n ==> !q. (q * n + r) MOD n = r

MOD_MULT_MOD

|- !m n. 0 < n /\ 0 < m ==> !x. x MOD (n * m) MOD n = x MOD n

MOD_ONE

|- !k. k MOD SUC 0 = 0

MOD_PLUS

|- !n. 0 < n ==> !j k. (j MOD n + k MOD n) MOD n = (j + k) MOD n

MOD_TIMES

|- !n. 0 < n ==> !q r. (q * n + r) MOD n = r MOD n

MOD_UNIQUE

|- !n k r. (?q. (k = q * n + r) /\ r < n) ==> (k MOD n = r)

MULT_0

|- !m. m * 0 = 0

MULT_ASSOC

|- !m n p. m * (n * p) = m * n * p

MULT_CLAUSES

|- !m n.
     (0 * m = 0) /\ (m * 0 = 0) /\ (1 * m = m) /\ (m * 1 = m) /\
     (SUC m * n = m * n + n) /\ (m * SUC n = m + m * n)

MULT_COMM

|- !m n. m * n = n * m

MULT_DIV

|- !n q. 0 < n ==> (q * n DIV n = q)

MULT_EQ_0

|- !m n. (m * n = 0) = (m = 0) \/ (n = 0)

MULT_EQ_1

|- !x y. (x * y = 1) = (x = 1) /\ (y = 1)

MULT_EXP_MONO

|- !p q n m. (n * SUC q ** p = m * SUC q ** p) = (n = m)

MULT_INCREASES

|- !m n. 1 < m /\ 0 < n ==> SUC n <= m * n

MULT_LEFT_1

|- !m. 1 * m = m

MULT_LESS_EQ_SUC

|- !m n p. m <= n = SUC p * m <= SUC p * n

MULT_MONO_EQ

|- !m i n. (SUC n * m = SUC n * i) = (m = i)

MULT_RIGHT_1

|- !m. m * 1 = m

MULT_SUC

|- !m n. m * SUC n = m + m * n

MULT_SUC_EQ

|- !p m n. (n * SUC p = m * SUC p) = (n = m)

MULT_SYM

|- !m n. m * n = n * m

NOT_EXP_0

|- !m n. ~(SUC n ** m = 0)

NOT_GREATER

|- !m n. ~(m > n) = m <= n

NOT_GREATER_EQ

|- !m n. ~(m >= n) = SUC m <= n

NOT_LEQ

|- !m n. ~(m <= n) = SUC n <= m

NOT_LESS

|- !m n. ~(m < n) = n <= m

NOT_LESS_EQUAL

|- !m n. ~(m <= n) = n < m

NOT_NUM_EQ

|- !m n. ~(m = n) = SUC m <= n \/ SUC n <= m

NOT_ODD_EQ_EVEN

|- !n m. ~(SUC (n + n) = m + m)

NOT_SUC_ADD_LESS_EQ

|- !m n. ~(SUC (m + n) <= m)

NOT_SUC_LESS_EQ

|- !n m. ~(SUC n <= m) = m <= n

NOT_SUC_LESS_EQ_0

|- !n. ~(SUC n <= 0)

NOT_ZERO_LT_ZERO

|- !n. ~(n = 0) = 0 < n

num_case_compute

|- !n. num_case f g n = (if n = 0 then f else g (PRE n))

num_case_cong

|- !f' f b' b M' M.
     (M = M') /\ ((M' = 0) ==> (b = b')) /\
     (!n. (M' = SUC n) ==> (f n = f' n)) ==>
     (num_case b f M = num_case b' f' M')

num_CASES

|- !m. (m = 0) \/ ?n. m = SUC n

ODD_ADD

|- !m n. ODD (m + n) = ~(ODD m = ODD n)

ODD_DOUBLE

|- !n. ODD (SUC (2 * n))

ODD_EVEN

|- !n. ODD n = ~EVEN n

ODD_EXISTS

|- !n. ODD n = ?m. n = SUC (2 * m)

ODD_MULT

|- !m n. ODD (m * n) = ODD m /\ ODD n

ODD_OR_EVEN

|- !n. ?m. (n = SUC (SUC 0) * m) \/ (n = SUC (SUC 0) * m + 1)

ONE

|- 1 = SUC 0

OR_LESS

|- !m n. SUC m <= n ==> m < n

PRE_ELIM_THM

|- P (PRE n) = !m. ((n = 0) ==> P 0) /\ ((n = SUC m) ==> P m)

PRE_SUB

|- !m n. PRE (m - n) = PRE m - n

PRE_SUB1

|- !m. PRE m = m - 1

PRE_SUC_EQ

|- !m n. 0 < n ==> ((m = PRE n) = (SUC m = n))

RIGHT_ADD_DISTRIB

|- !m n p. (m + n) * p = m * p + n * p

RIGHT_SUB_DISTRIB

|- !m n p. (m - n) * p = m * p - n * p

SUB_0

|- !m. (0 - m = 0) /\ (m - 0 = m)

SUB_ADD

|- !m n. n <= m ==> (m - n + n = m)

SUB_CANCEL

|- !p n m. n <= p /\ m <= p ==> ((p - n = p - m) = (n = m))

SUB_ELIM_THM

|- P (a - b) = !d. ((b = a + d) ==> P 0) /\ ((a = b + d) ==> P d)

SUB_EQ_0

|- !m n. (m - n = 0) = m <= n

SUB_EQ_EQ_0

|- !m n. (m - n = m) = (m = 0) \/ (n = 0)

SUB_EQUAL_0

|- !c. c - c = 0

SUB_LEFT_ADD

|- !m n p. m + (n - p) = (if n <= p then m else m + n - p)

SUB_LEFT_EQ

|- !m n p. (m = n - p) = (m + p = n) \/ m <= 0 /\ n <= p

SUB_LEFT_GREATER

|- !m n p. m > n - p = m + p > n /\ m > 0

SUB_LEFT_GREATER_EQ

|- !m n p. m >= n - p = m + p >= n

SUB_LEFT_LESS

|- !m n p. m < n - p = m + p < n

SUB_LEFT_LESS_EQ

|- !m n p. m <= n - p = m + p <= n \/ m <= 0

SUB_LEFT_SUB

|- !m n p. m - (n - p) = (if n <= p then m else m + p - n)

SUB_LEFT_SUC

|- !m n. SUC (m - n) = (if m <= n then SUC 0 else SUC m - n)

SUB_LESS_0

|- !n m. m < n = 0 < n - m

SUB_LESS_EQ

|- !n m. n - m <= n

SUB_LESS_EQ_ADD

|- !m p. m <= p ==> !n. p - m <= n = p <= m + n

SUB_LESS_OR

|- !m n. n < m ==> n <= m - 1

SUB_MONO_EQ

|- !n m. SUC n - SUC m = n - m

SUB_PLUS

|- !a b c. a - (b + c) = a - b - c

SUB_RIGHT_ADD

|- !m n p. m - n + p = (if m <= n then p else m + p - n)

SUB_RIGHT_EQ

|- !m n p. (m - n = p) = (m = n + p) \/ m <= n /\ p <= 0

SUB_RIGHT_GREATER

|- !m n p. m - n > p = m > n + p

SUB_RIGHT_GREATER_EQ

|- !m n p. m - n >= p = m >= n + p \/ 0 >= p

SUB_RIGHT_LESS

|- !m n p. m - n < p = m < n + p /\ 0 < p

SUB_RIGHT_LESS_EQ

|- !m n p. m - n <= p = m <= n + p

SUB_RIGHT_SUB

|- !m n p. m - n - p = m - (n + p)

SUB_SUB

|- !b c. c <= b ==> !a. a - (b - c) = a + c - b

SUC_ADD_SYM

|- !m n. SUC (m + n) = SUC n + m

SUC_ELIM_THM

|- !P. (!n. P (SUC n) n) = !n. 0 < n ==> P n (n - 1)

SUC_NOT

|- !n. ~(0 = SUC n)

SUC_ONE_ADD

|- !n. SUC n = 1 + n

SUC_SUB1

|- !m. SUC m - 1 = m

TIMES2

|- !n. 2 * n = n + n

TWO

|- 2 = SUC 1

WOP

|- !P. (?n. P n) ==> ?n. P n /\ !m. m < n ==> ~P m

ZERO_DIV

|- !n. 0 < n ==> (0 DIV n = 0)

ZERO_LESS_EQ

|- !n. 0 <= n

ZERO_LESS_EXP

|- !m n. 0 < SUC n ** m

ZERO_MOD

|- !n. 0 < n ==> (0 MOD n = 0)