Package function-def: Definition of function operators and combinators
Information
| name | function-def |
| version | 1.16 |
| description | Definition of function operators and combinators |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | HOLLight |
| requires | bool |
| show | Data.Bool Function |
Files
- Package tarball function-def-1.16.tgz
- Theory file function-def.thy (included in the package tarball)
Defined Constants
- Function
- id
- injective
- ∘
- surjective
- C
- K
- S
- W
Theorems
⊦ id = λx. x
⊦ K = λx y. x
⊦ W = λf x. f x x
⊦ (∘) = λf g x. f (g x)
⊦ C = λf x y. f y x
⊦ S = λf g x. f x (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
- ∀
- ⇒
- ∃
- ⊤
- Bool
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤