Package natural-sub-thm: Properties of natural number subtraction

Information

name	natural-sub-thm
version	1.13
description	Properties of natural number subtraction
author	Joe Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2011-11-27
requires	bool natural-def natural-dest natural-order natural-add natural-mult natural-sub-def
show	Data.Bool Number.Natural

Files

Package tarball natural-sub-thm-1.13.tgz
Theory file natural-sub-thm.thy (included in the package tarball)

Theorems

⊦ ∀m. m - 0 = m

⊦ ∀n. n - n = 0

⊦ ∀n. suc n - 1 = n

⊦ ∀m n. m + n - m = n

⊦ ∀n. ¬(n = 0) ⇒ pre n = n - 1

⊦ ∀m n. n ≤ m ⇒ n + (m - n) = m

⊦ ∀m n. n ≤ m ⇒ m - n + n = m

⊦ ∀m n. n < m ⇒ m - suc n = pre (m - n)

⊦ ∀m n. n < m ⇒ suc (m - suc n) = m - n

⊦ ∀m n. n ≤ m ⇒ suc (m - n) = suc m - n

⊦ ∀m n. n ≤ m ⇒ (m - n = 0 ⇔ m = n)

⊦ ∀m n. n ≤ m ⇒ pre (suc m - n) = m - n

⊦ ∀m n. n ≤ m ⇒ suc m - suc n = m - n

⊦ ∀m n p. n ≤ m ⇒ m + p - (n + p) = m - n

⊦ ∀m n p. p ≤ n ⇒ m + n - (m + p) = n - p

⊦ ∀m n p. n ≤ m ⇒ (m - n) * p = m * p - n * p

⊦ ∀m n p. p ≤ n ⇒ m * (n - p) = m * n - m * p

Input Type Operators

→
bool
Number
- Natural
  - natural

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ¬
  - F
  - T
Number
- Natural
  - *
  - +
  - -
  - <
  - ≤
  - bit1
  - pre
  - suc
  - zero

Assumptions

⊦ T

⊦ ¬F ⇔ T

⊦ ¬T ⇔ F

⊦ ∀t. t ⇒ t

⊦ F ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ F

⊦ ∀t. (∀x. t) ⇔ t

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

⊦ ∀t. F ⇒ t ⇔ T

⊦ ∀t. T ⇒ t ⇔ t

⊦ ∀t. t ⇒ T ⇔ T

⊦ ∀n. ¬(suc n = 0)

⊦ ∀m. m < 0 ⇔ F

⊦ ∀n. pre (suc n) = n

⊦ ∀m. m + 0 = m

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀m. suc m = m + 1

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀m n. m * n = n * m

⊦ ∀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

⊦ ∀m n. suc m ≤ n ⇔ m < n

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

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

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

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀m n. m + n = m ⇔ n = 0

⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d

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

⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n

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