Package natural-min-max-def: natural-min-max-def

Information

Files

• Package tarball natural-min-max-def-1.3.tgz
• Theory file natural-min-max-def.thy (included in the package tarball)

Defined Constants

• Number
  • Natural
    • Number.Natural.max
    • Number.Natural.min
    • Number.Natural.minimal

Theorems

⊦ ∀m n. Number.Natural.max m n = if Number.Natural.≤ m n then n else m

⊦ ∀m n. Number.Natural.min m n = if Number.Natural.≤ m n then m else n

⊦ ∀P.
    (∃n. P n) ⇔
    P (Number.Natural.minimal P) ∧
    ∀m. Number.Natural.< m (Number.Natural.minimal P) ⇒ ¬P m

Input Type Operators

• →
• bool
• Number
  • Natural
    • Number.Natural.natural

Input Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ~
    • cond
    • T
• Number
  • Natural
    • Number.Natural.<
    • Number.Natural.≤

Assumptions

⊦ T

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

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

⊦ ∀x. x = x ⇔ T

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

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

⊦ ∀P. (∃n. P n) ⇔ ∃n. P n ∧ ∀m. Number.Natural.< m n ⇒ ¬P m