Package natural-add-sub-thm: Properties of natural number subtraction
Information
| name | natural-add-sub-thm |
| version | 1.5 |
| description | Properties of natural number subtraction |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2014-06-12 |
| requires | bool natural-add-def natural-add-sub-def natural-add-thm natural-def natural-dest natural-order |
| show | Data.Bool Number.Natural |
Files
- Package tarball natural-add-sub-thm-1.5.tgz
- Theory source file natural-add-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
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- ⊥
- ⊤
- Bool
- Number
- Natural
- +
- -
- <
- ≤
- bit1
- pre
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ ∀t. t ⇒ t
⊦ ⊥ ⇔ ∀p. p
⊦ ∀m. ¬(m < 0)
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊥ ⇒ t ⇔ ⊤
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ ∀n. ¬(suc n = 0)
⊦ ∀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 ⇒ 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 ⊤ ⊤
⊦ (∃) = λ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