Package relation-natural-def: Definition of relations over natural numbers
Information
| name | relation-natural-def |
| version | 1.26 |
| description | Definition of relations over natural numbers |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2014-10-30 |
| checksum | bb6564664b7136f9979da87aed52df68a786e00f |
| requires | bool natural |
| show | Data.Bool Number.Natural Relation |
Files
- Package tarball relation-natural-def-1.26.tgz
- Theory source file relation-natural-def.thy (included in the package tarball)
Defined Constants
- Number
- Natural
- isSuc
- Natural
- Relation
- measure
Theorems
⊦ ∀m n. isSuc m n ⇔ suc m = n
⊦ ∀m x y. measure m x y ⇔ m x < m y
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ⊤
- Bool
- Number
- Natural
- <
- suc
- Natural
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤