Package natural-mult-thm: Properties of natural number multiplication

Information

namenatural-mult-thm
version1.22
descriptionProperties of natural number multiplication
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-27
requiresbool
natural-def
natural-numeral
natural-order
natural-add
natural-mult-def
showData.Bool
Number.Natural

Files

Theorems

n. n n * n

m. m * 0 = 0

m. m * 1 = m

m. 1 * m = m

m n. m * n = n * m

n. 2 * n = n + n

m n. m * suc n = m + m * n

A B. (n. A * n B) A = 0

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

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

m n. 0 < m * n 0 < m 0 < n

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

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

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

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

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

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

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

A B C. (n. A * n B * n + C) A B

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. m * p < n * p m < n ¬(p = 0)

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

m n p q. m < n p < q m * p < n * q

m n p q. m n p q m * p n * q

P. (B. n. P n B) A B. n. n * P n A * n + B

P A B.
    P 0 0 = 0 (m n. P m n A * (m + n) + B)
    B. m n. P m n B * (m + n)

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

bit0 0 = 0

n. 0 n

n. n n

F p. p

t. t ¬t

n. ¬(n < n)

n. 0 < suc n

(¬) = λp. p F

t. (x. t) 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. 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 T T

t. t t t

n. ¬(suc n = 0)

m. m < 0 F

n. 0 * n = 0

n. 0 + n = n

m. m + 0 = m

t. (F t) ¬t

t. t F ¬t

n. bit1 n = suc (bit0 n)

m n. m m + n

m n. n m + n

() = λp q. p q p

t. (t T) (t F)

m. m 0 m = 0

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

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

m n. m + n = n + m

m n. m < n m n

m n. ¬(m n) n < m

m n. m < suc n m n

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

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

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

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

m n. suc m = suc n m = n

m n. suc m < suc n m < n

m n. suc m suc n m n

m n. suc m * n = m * n + n

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

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

m n. m < n d. n = m + suc d

m n. m < n m n ¬(m = n)

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

m n p. m + n = m + p n = p

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

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

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

m n p. m n n p m p

m n. m + n = 0 m = 0 n = 0

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