Package sum-thm: Properties of sum types

Information

namesum-thm
version1.1
descriptionProperties of sum types
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-09
checksum01fd163ede0704e34ff00760c9bb8182f4e51762
requiresbool
sum-def
showData.Bool
Data.Sum

Files

Theorems

x. case left right x = x

x. (a. x = left a) b. x = right b

f g x. isLeft x case f g x = f (destLeft x)

f g x. isRight x case f g x = g (destRight x)

External Type Operators

External Constants

Assumptions

a. isLeft (left a)

b. isRight (right b)

p. p

a. ¬isRight (left a)

b. ¬isLeft (right b)

(¬) = λp. p

() = λp. p = λx.

a. destLeft (left a) = a

b. destRight (right b) = b

t. t

t. t t

() = λp q. p q p

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

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

f g a. case f g (left a) = f a

f g b. case f g (right b) = g b

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

p. (a. p (left a)) (b. p (right b)) x. p x