Package natural-add-sub: Natural number subtraction

Information

Files

• Package tarball natural-add-sub-1.10.tgz
• Theory source file natural-add-sub.thy (included in the package tarball)

Defined Constant

• Number
  • Natural
    • -

Theorems

⊦ ∀m. m - 0 = m

⊦ ∀n. n - n = 0

⊦ ∀n. suc n - 1 = n

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

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

⊦ ∀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 + p ≤ m ⇒ m - (n + p) = m - n - p

External Type Operators

• →
• bool
• Number
  • Natural
    • natural

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∃!
    • ¬
    • ⊥
    • ⊤
• Number
  • Natural
    • +
    • <
    • ≤
    • bit1
    • pre
    • suc
    • zero

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀t. t ⇒ t

⊦ ⊥ ⇔ ∀p. p

⊦ ∀m. ¬(m < 0)

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) 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 < 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. m + suc n = suc (m + n)

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

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

OpenTheory package document generated by opentheory 1.3 (release 20141119)