Theory: arithmetic

Parents

• prim_rec

Type constants

Term constants

• +:num -> num -> num {fixity = Infix 500}
• -:num -> num -> num {fixity = Infix 500}
• *:num -> num -> num {fixity = Infix 600}
• EXP:num -> num -> num {fixity = Infix 700}
• >:num -> num -> bool {fixity = Infix 450}
• <=:num -> num -> bool {fixity = Infix 450}
• >=:num -> num -> bool {fixity = Infix 450}
• FACT:num -> num {fixity = Prefix}
• EVEN:num -> bool {fixity = Prefix}
• ODD:num -> bool {fixity = Prefix}
• MOD:num -> num -> num {fixity = Infix 650}
• DIV:num -> num -> num {fixity = Infix 600}

Axioms

Definitions

ADD

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

SUB

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

MULT

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

EXP

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

GREATER

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

LESS_OR_EQ

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

GREATER_OR_EQ

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

FACT

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

EVEN

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

ODD

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

DIVISION

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

Theorems

SUC_NOT

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

ADD_0

|- !m. m + 0 = m

ADD_SUC

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

ADD_CLAUSES

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

ADD_SYM

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

num_CASES

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

LESS_MONO_REV

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

LESS_MONO_EQ

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

SUC_SUB1

|- !m. SUC m - 1 = m

PRE_SUB1

|- !m. PRE m = m - 1

LESS_ADD

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

SUB_0

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

LESS_TRANS

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

ADD1

|- !m. SUC m = m + 1

LESS_ANTISYM

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

LESS_LESS_SUC

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

FUN_EQ_LEMMA

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

LESS_OR

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

OR_LESS

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

LESS_EQ

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

LESS_SUC_EQ_COR

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

LESS_NOT_SUC

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

LESS_0_CASES

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

LESS_CASES_IMP

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

LESS_CASES

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

ADD_INV_0

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

LESS_EQ_ADD

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

LESS_EQ_SUC_REFL

|- !m. m <= SUC m

LESS_ADD_NONZERO

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

LESS_EQ_ANTISYM

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

NOT_LESS

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

SUB_EQ_0

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

ADD_ASSOC

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

MULT_0

|- !m. m * 0 = 0

MULT_SUC

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

MULT_LEFT_1

|- !m. 1 * m = m

MULT_RIGHT_1

|- !m. m * 1 = m

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_SYM

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

RIGHT_ADD_DISTRIB

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

LEFT_ADD_DISTRIB

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

MULT_ASSOC

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

SUB_ADD

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

PRE_SUB

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

ADD_EQ_0

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

ADD_INV_0_EQ

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

PRE_SUC_EQ

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

INV_PRE_EQ

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

LESS_SUC_NOT

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

ADD_EQ_SUB

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

LESS_MONO_ADD

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

LESS_MONO_ADD_INV

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

LESS_MONO_ADD_EQ

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

EQ_MONO_ADD_EQ

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

LESS_EQ_MONO_ADD_EQ

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

LESS_EQ_TRANS

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

LESS_EQ_LESS_EQ_MONO

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

LESS_EQ_REFL

|- !m. m <= m

LESS_IMP_LESS_OR_EQ

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

LESS_MONO_MULT

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

RIGHT_SUB_DISTRIB

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

LEFT_SUB_DISTRIB

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

LESS_ADD_1

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

EXP_ADD

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

NOT_ODD_EQ_EVEN

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

MULT_SUC_EQ

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

MULT_EXP_MONO

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

LESS_EQUAL_ANTISYM

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

LESS_ADD_SUC

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

ZERO_LESS_EQ

|- !n. 0 <= n

LESS_EQ_MONO

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

LESS_OR_EQ_ADD

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

WOP

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

GEN_INDUCTION

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

DA

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

MOD_ONE

|- !k. k MOD SUC 0 = 0

DIV_LESS_EQ

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

DIV_UNIQUE

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

MOD_UNIQUE

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

DIV_MULT

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

LESS_MOD

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

MOD_EQ_0

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

ZERO_MOD

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

ZERO_DIV

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

MOD_MULT

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

MOD_TIMES

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

MOD_PLUS

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

MOD_MOD

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

SUB_MONO_EQ

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

SUB_PLUS

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

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)

SUB_LESS_EQ

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

SUB_EQ_EQ_0

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

SUB_LESS_0

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

SUB_LESS_OR

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

LESS_SUB_ADD_LESS

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

TIMES2

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

LESS_MULT_MONO

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

MULT_MONO_EQ

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

ADD_SUB

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

LESS_EQ_ADD_SUB

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

SUB_EQUAL_0

|- !c. c - c = 0

LESS_EQ_SUB_LESS

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

NOT_SUC_LESS_EQ

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

SUB_SUB

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

LESS_IMP_LESS_ADD

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

LESS_EQ_IMP_LESS_SUC

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

SUB_LESS_EQ_ADD

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

SUB_CANCEL

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

CANCEL_SUB

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

NOT_EXP_0

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

ZERO_LESS_EXP

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

ODD_OR_EVEN

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

LESS_EXP_SUC_MONO

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

LESS_LESS_CASES

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

GREATER_EQ

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

LESS_EQ_CASES

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

LESS_EQUAL_ADD

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

LESS_EQ_EXISTS

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

NOT_LESS_EQUAL

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

LESS_EQ_0

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

MULT_EQ_0

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

LESS_MULT2

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

LESS_EQ_LESS_TRANS

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

LESS_LESS_EQ_TRANS

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

FACT_LESS

|- !n. 0 < FACT n

EVEN_ODD

|- !n. EVEN n = ~(ODD n)

ODD_EVEN

|- !n. ODD n = ~(EVEN n)

EVEN_OR_ODD

|- !n. EVEN n \/ ODD n

EVEN_AND_ODD

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

EVEN_ADD

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

EVEN_MULT

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

ODD_ADD

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

ODD_MULT

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

EVEN_DOUBLE

|- !n. EVEN (2 * n)

ODD_DOUBLE

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

EVEN_ODD_EXISTS

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

EVEN_EXISTS

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

ODD_EXISTS

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

EQ_LESS_EQ

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

ADD_MONO_LESS_EQ

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

NOT_SUC_LESS_EQ_0

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

NOT_LEQ

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

NOT_NUM_EQ

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

NOT_GREATER

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

NOT_GREATER_EQ

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

SUC_ONE_ADD

|- !n. SUC n = 1 + n

SUC_ADD_SYM

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

NOT_SUC_ADD_LESS_EQ

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

MULT_LESS_EQ_SUC

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

SUB_LEFT_ADD

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

SUB_RIGHT_ADD

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

SUB_LEFT_SUB

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

SUB_RIGHT_SUB

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

SUB_LEFT_SUC

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

SUB_LEFT_LESS_EQ

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

SUB_RIGHT_LESS_EQ

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

SUB_LEFT_LESS

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

SUB_RIGHT_LESS

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

SUB_LEFT_GREATER_EQ

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

SUB_RIGHT_GREATER_EQ

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

SUB_LEFT_GREATER

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

SUB_RIGHT_GREATER

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

SUB_LEFT_EQ

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

SUB_RIGHT_EQ

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