Package relation-natural-def: Definition of relations over natural numbers
Information
| name | relation-natural-def |
| version | 1.20 |
| description | Definition of relations over natural numbers |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2012-08-06 |
| requires | bool |
| show | Data.Bool Number.Natural Relation |
Files
- Package tarball relation-natural-def-1.20.tgz
- Theory 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
Input Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
Input Constants
- =
- Data
- Bool
- ∀
- ⊤
- Bool
- Number
- Natural
- <
- suc
- Natural
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤