Package natural-distance-thm: Properties of natural number distance

Information

namenatural-distance-thm
version1.59
descriptionProperties of natural number distance
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2014-11-01
checksum58ae1e3461ae7358e92803981f68dbb713388cba
requiresbool
natural-add
natural-distance-def
natural-mult
natural-numeral
natural-order
natural-thm
showData.Bool
Number.Natural

Files

Theorems

n. distance 0 n = n

n. distance n 0 = n

n. distance n n = 0

m n. distance m n = distance n m

m n. distance m n m + n

m n. distance m (m + n) = n

m n. distance (m + n) m = n

m n. distance m n = 0 m = n

m n. distance (suc m) (suc n) = distance m n

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

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

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

m n. distance (distance m n) (distance m (n + 1)) = 1

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

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

m n p q. distance m p distance (m + n) (p + q) + distance n q

m n p q. distance (m + n) (p + q) distance m p + distance n q

m n p q. distance m n + distance n p q distance m p q

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

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

p x y. p (distance x y) d. (x = y + d p d) (y = x + d p d)

m n p q r s.
    distance m n r distance p q s
    distance m p distance n q + (r + s)

External Type Operators

External Constants

Assumptions

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. p

t. t ¬t

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

n. 0 * n = 0

n. 0 + n = n

m. m - 0 = m

n. n - n = 0

n. bit1 n = suc (bit0 n)

m n. m m + n

m n. n m + n

() = λp q. p q p

m. suc m = m + 1

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

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

x y. x = y y = x

m n. m * n = n * m

m n. m + n = n + m

m n. m n n m

m n. m + n - m = n

m. m = 0 n. m = suc n

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

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

m n. m + n = m n = 0

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

p a. (x. x = a p x) p a

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

m n. m n n m 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. n + m p + m n p

m n p. m n n p m p

m n. n m (m - n = 0 m = n)

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

m n. distance m n = if m n then n - m else m - n

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

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

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

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

p c x y. p (if c then x else y) (c p x) (¬c p y)