Package natural-divides-thm: Properties of the divides relation on natural numbers

Information

namenatural-divides-thm
version1.11
descriptionProperties of the divides relation on natural numbers
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2011-11-28
requiresbool
natural
natural-divides-def
showData.Bool
Number.Natural

Files

Theorems

a. divides a 0

a. divides a a

a. divides 1 a

a. divides 0 a a = 0

a. divides 2 a even a

a b. a = b divides a b

a. divides a 1 a = 1

a b c. divides a b divides a (b * c)

a b c. divides a c divides a (b * c)

a b c. divides (a * b) c divides a c

a b c. divides (a * b) c divides b c

a b. divides a b divides b a a = b

a b. ¬(b = 0) divides a b a b

a b c. divides a b divides b c divides a c

a b. (c. divides b c divides a c) divides a b

a b. (c. divides c a divides c b) divides a b

a b. (c. divides b c divides a c) divides a b

a b. (c. divides c a divides c b) divides a b

a b. ¬(b = 0) b a divides b (factorial a)

a b. ¬(a = 0) (divides a b b mod a = 0)

a b c. divides a b divides a c divides a (b + c)

a. divides a 2 a = 1 a = 2

a. divides a 3 a = 1 a = 3

a b. divides a b if a = 0 then b = 0 else b mod a = 0

a b. ¬(a = 0) (divides a b b div a * a = b)

a b c. divides (a * b) (a * c) a = 0 divides b c

a b c. divides (b * a) (c * a) a = 0 divides b c

a b c d. divides a c divides b d divides (a * b) (c * d)

a b c. c b divides a b divides a c divides a (b - c)

a b.
    g.
      divides g a divides g b
      c. divides c a divides c b divides c g

p.
    (n. p 0 n) (m n. n < m p n m p m n)
    (m n. p m n p m (n + m)) m n. p m n

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

bit0 0 = 0

t. t t

n. 0 n

F p. p

t. t ¬t

(¬) = λp. p F

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx. T

t. ¬¬t t

t. (T t) t

t. (t T) t

t. F t F

t. T t t

t. t F F

t. t T t

t. F t T

t. T t t

t. t T T

t. F t t

t. T t T

t. t F t

n. ¬(suc n = 0)

n. 0 * n = 0

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

n. n - n = 0

t. (F t) ¬t

t. (t F) ¬t

t. t F ¬t

n. bit1 n = suc (bit0 n)

m. m * 1 = m

m. 1 * m = m

m n. n m + n

() = λp q. p q p

t. (t T) (t F)

n. even (suc n) ¬even n

m. m 0 m = 0

t1 t2. (if F then t1 else t2) = t2

t1 t2. (if T then t1 else t2) = t1

n. 0 < n ¬(n = 0)

n. bit0 (suc n) = suc (suc (bit0 n))

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

m n. m * n = n * m

m n. m + n = n + m

m n. m + n - n = m

n. factorial (suc n) = suc n * factorial n

n. 2 * n = n + n

m n. ¬(m n) n < m

m n. suc m n m < n

P. (b. P b) P T P F

() = λp q. (λf. f p q) = λf. f T T

n. even n n mod 2 = 0

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

t1 t2. ¬(t1 t2) t1 ¬t2

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. n < m + n 0 < m

m n. suc m = suc n m = n

m n. m + n = m n = 0

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. even (m * n) even m even n

m n. even (m + n) even m even n

m n. m n d. n = m + d

a b. divides a b c. c * a = b

P a. (x. x = a P x) P a

() = λp q. r. (p r) (q r) r

m n. m n m < n m = n

m n. m n n m m = n

P Q. P (x. Q x) x. P Q x

P Q. P (x. Q x) x. P Q x

P Q. P (x. Q x) x. P Q x

m n. ¬(m = 0) m * n div m = n

P Q. (x. P x) Q x. P x Q

P Q. (x. P x) Q x. P x Q

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

m n p. m + n < m + p n < p

m n p. n + m < p + m n < p

m n. m suc n m = suc n m n

m n. m * n = 0 m = 0 n = 0

P. P 0 (n. P n P (suc n)) n. P n

m n. n * m = m m = 0 n = 1

m n p. (m + n) * p = m * p + n * p

P. (n. (m. m < n P m) P n) n. P n

P Q. (x. P x) (x. Q x) x. P x Q x

m n. ¬(n = 0) m div n * n + m mod n = m

m n. m * n = 1 m = 1 n = 1

m n p. m * n = m * p m = 0 n = p

m n p. m * p = n * p m = n p = 0

m n p. m * n m * p m = 0 n p

m n p. m * p n * p m n p = 0

m n p. m * n < m * p ¬(m = 0) n < p

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