Package option-dest-thm: Properties of option type destructors

Information

nameoption-dest-thm
version1.8
descriptionProperties of option type destructors
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2011-12-18
requiresbool
option-thm
option-dest-def
showData.Bool
Data.Option

Files

Theorem

x. case none some x = x

Input Type Operators

Input Constants

Assumptions

T

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

() = λp q. p q p

b f. case b f none = b

x. x = none a. x = some a

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

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

b f a. case b f (some a) = f a

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