Package function-def: Definition of function operators and combinators
Information
| name | function-def |
| version | 1.6 |
| description | Definition of function operators and combinators |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| requires | bool |
| show | Data.Bool Function |
Files
- Package tarball function-def-1.6.tgz
- Theory file function-def.thy (included in the package tarball)
Defined Constants
- Function
- id
- injective
- ∘
- surjective
Theorems
⊦ id = λx. x
⊦ ∀f g. (f ∘ g) = λx. f (g x)
⊦ ∀f. surjective f ⇔ ∀y. ∃x. y = f x
⊦ ∀f. injective f ⇔ ∀x1 x2. f x1 = f x2 ⇒ x1 = x2
Input Type Operators
- →
- bool
Input Constants
- =
- Data
- Bool
- ∀
- ⇒
- ∃
- T
- Bool
Assumptions
⊦ T
⊦ (∀) = λp. p = λx. T