Package natural-sub: Definitions and theorems about natural number subtraction

Information

Files

• Package tarball natural-sub-1.5.tgz
• Theory file natural-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. n ≤ m ⇒ (even (m - n) ⇔ even m ⇔ even n)

⊦ ∀m n. n ≤ m ⇒ (odd (m - n) ⇔ ¬(odd m ⇔ odd 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

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ~
    • F
    • T
• Number
  • Natural
    • *
    • +
    • <
    • ≤
    • bit1
    • even
    • odd
    • pre
    • suc
    • zero

Assumptions

⊦ T

⊦ F ⇔ ∀p. p

⊦ (~) = λp. p ⇒ F

⊦ (∃) = λP. P ((select) P)

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

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

⊦ ∀x. x = x ⇔ T

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. pre (suc n) = n

⊦ ∀m. m + 0 = m

⊦ ∀n. ¬even n ⇔ odd n

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

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀m. suc m = m + 1

⊦ (¬T ⇔ F) ∧ (¬F ⇔ T)

⊦ ∀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 < 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 < suc n ⇔ m < n

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

⊦ ∀m n. even (m + n) ⇔ even m ⇔ even n

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

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

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

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

⊦ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)

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

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

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

⊦ (∀m. m < 0 ⇔ F) ∧ ∀m n. m < suc n ⇔ m = n ∨ m < n

⊦ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)

⊦ ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)

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