Package function-thm: Properties of function operators and combinators

Information

namefunction-thm
version1.10
descriptionProperties of function operators and combinators
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-09-21
requiresbool
function-def
showData.Bool

Files

Theorems

x. Function.id x = x

f. Function.∘ Function.id f = f Function.∘ f Function.id = f

f g x. Function.∘ f g x = f (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

Input Type Operators

Input Constants

Assumptions

T

Function.id = λx. x

() = λP. P ((select) P)

t. (x. t) t

() = λp. p = λx. T

x. x = x T

() = λp q. p q p

t. (t T) (t F)

(¬T F) (¬F T)

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

x y. x = y y = x

x y. x = y y = x

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

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

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

f g. f = g x. f x = g x

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

P. (x. y. P x y) y. x. P x (y x)

(t. ¬¬t t) (¬T F) (¬F T)

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)