Package natural-order-min-max-def: Definition of natural number min and max functions
Information
| name | natural-order-min-max-def |
| version | 1.29 |
| description | Definition of natural number min and max functions |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2014-11-01 |
| checksum | 756975b4923e6b7b8bca33930309ae17e5864a39 |
| requires | bool natural-order-thm |
| show | Data.Bool Number.Natural |
Files
- Package tarball natural-order-min-max-def-1.29.tgz
- Theory source file natural-order-min-max-def.thy (included in the package tarball)
Defined Constants
- Number
- Natural
- max
- min
- minimal
- Natural
Theorems
⊦ ∀m n. max m n = if m ≤ n then n else m
⊦ ∀m n. min m n = if m ≤ n then m else n
⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- cond
- ⊤
- Bool
- Number
- Natural
- <
- ≤
- Natural
Assumptions
⊦ ⊤
⊦ (∃) = λp. p ((select) p)
⊦ (∀) = λp. p = λx. ⊤
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀p. (∃n. p n) ⇔ ∃n. p n ∧ ∀m. m < n ⇒ ¬p m