Package function-thm: Properties of function operators and combinators

Information

namefunction-thm
version1.29
descriptionProperties of function operators and combinators
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-03-24
requiresbool
function-def
showData.Bool

Files

Theorems

x. Function.id x = x

x. Function.S Function.K x = Function.id

f. Function.∘ f Function.id = f

f. Function.∘ Function.id f = f

f. Function.C (Function.C f) = f

x y. Function.K x y = x

f x. Function.W f x = f x x

f g x. Function.∘ f g x = f (g x)

f x y. Function.C f x y = f y x

f g x. Function.S f g x = f x (g x)

f g h. Function.∘ f (Function.∘ g h) = Function.∘ (Function.∘ f g) h

f g. (x. y. g y = f x) h. f = Function.∘ g h

f. (y. x. f x = y) P. (x. P (f x)) y. P y

f. (y. x. f x = y) P. (x. P (f x)) y. P y

f g. (x y. g x = g y f x = f y) h. f = Function.∘ h g

p f g. (x. p x y. g y = f x) h. x. p x f x = g (h x)

p f g.
    (x y. p x p y g x = g y f x = f y) h. x. p x f x = h (g x)

Input Type Operators

Input Constants

Assumptions

Function.id = λx. x

Function.K = λx y. x

¬

¬

t. t t

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

Function.W = λf x. f x x

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t t

t. t t

Function.∘ = λf g x. f (g x)

Function.C = λf x y. f y x

t. ( t) ¬t

t. (t ) ¬t

Function.S = λf g x. f x (g x)

() = λp q. p q p

t. (t ) (t )

f y. (let x y in f x) = f y

x y. x = y y = x

x y. x = y y = x

() = λp q. (λf. f p q) = λf. f

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

p q. p (x. q x) x. p q x

p. (x. y. p x y) y. x. p x (y x)