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

Information

namenatural-mult-thm
version1.53
descriptionProperties of natural number multiplication
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2014-11-17
checksum4d3440b0e8f76cf3b33f9d671b0f9bc56d782b74
requiresbool
natural-add
natural-def
natural-mult-def
natural-numeral
natural-order
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

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

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

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)
    c. m n. p m n c * (m + n)

External Type Operators

External Constants

Assumptions

¬

¬

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. p

t. t ¬t

m. ¬(m < 0)

n. ¬(n < n)

n. 0 < suc n

(¬) = λp. p

t. (x. t) t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t

t. t t t

n. ¬(suc n = 0)

n. 0 * n = 0

n. 0 + n = n

m. m + 0 = m

t. ( t) ¬t

t. t ¬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 )

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 - m = n

m n. ¬(m n) n < m

m n. m < suc n m n

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

() = λ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