Package set-thm: set-thm

Information

nameset-thm
version1.12
descriptionset-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-25
showData.Bool
Set

Files

Theorems

¬( = universe)

¬(universe = )

bigIntersect = universe

bigUnion =

x. x universe

s. s

s. s universe

s. s s

fromPredicate (λx. F) =

x. ¬(x )

s. ¬(universe s)

s. ¬(s )

s. ¬(s s)

x. delete x =

x. insert x universe = universe

s. - s =

s. s - = s

s. s - universe =

s. s - s =

s. image Function.id s = s

s. s s = s

s. s s = s

s. image (λx. x) s = s

universe = insert T (insert F )

s. bigIntersect (insert s ) = s

s. bigUnion (insert s ) = s

x s. x insert x s

x s. delete s x s

s t. disjoint s (t - s)

s t. disjoint (t - s) s

s t. s - t s

s. s = disjoint s s

s. universe s s = universe

s. s s =

s. disjoint s disjoint s

x s. ¬( = insert x s)

x s. ¬(insert x s = )

s t. disjoint s t disjoint t s

s t. s t = t s

s t. s t = t s

s. (x. x s) s = universe

s. s universe x. ¬(x s)

s. (x. x s) ¬(s = )

x y. x insert y x = y

x s. x s insert x s = s

x s. s - insert x = delete s x

x s. insert x (insert x s) = insert x s

x s. delete (delete s x) x = delete s x

x s. insert x s = insert x s

s x. insert x s x s

s t. s t s t = s

s t. s t s t = t

s t. s - t = s t

s t. s - t = s disjoint s t

s t. t (s - t) = t s

s t. s - t - t = s - t

s t. s - t t = s t

s u. bigIntersect (insert s u) = s bigIntersect u

s u. bigUnion (insert s u) = s bigUnion u

f s. image f s = s =

f g. f g bigIntersect g bigIntersect f

f g. f g bigUnion f bigUnion g

{ m. m | Number.Natural.< m 0 } =

x s. disjoint s (insert x ) ¬(x s)

x s. delete s x = s ¬(x s)

x s. disjoint (insert x ) s ¬(x s)

s t. bigIntersect (insert s (insert t )) = s t

s t. bigUnion (insert s (insert t )) = s t

f x. image f (insert x ) = insert (f x)

f s. image f (bigUnion s) = bigUnion (image (image f) s)

s t. bigIntersect (s t) = bigIntersect s bigIntersect t

s t. bigUnion (s t) = bigUnion s bigUnion t

s t x. s t s insert x t

x s. x s insert x (delete s x) = s

s t. s t t s s = t

s t. s (t - s) = t s t

s t. t - s s = t s t

s t. s t t s s = t

(s. s = ) s. s =

(s. universe s = s) s. s universe = s

(s. s = s) s. s = s

(s. universe s = universe) s. s universe = universe

f s x. x s f x image f s

x s. delete (insert x s) x = s ¬(x s)

s t. s t s t ¬(t s)

s. bigIntersect s = universe t. t s t = universe

s. bigUnion s = t. t s t =

x y s. insert x (insert y s) = insert y (insert x s)

x y s. delete (delete s x) y = delete (delete s y) x

x s t. s insert x t delete s x t

x s t. insert x s t = insert x (s t)

s c. image (λx. c) s = if s = then else insert c

s t x. disjoint (delete s x) t disjoint (delete t x) s

s t x. s - insert x t = delete s x - t

s t x. delete s x t = delete (s t) x

s t u. s t u s - t u

s t u. s t u s - u t

t u s. s - t - u = s - (t u)

t u s. s - t - u = s - u - t

s t u. s t u = s (t u)

s t u. s t u = s (t u)

s t u. s t t u s u

s t u. s t t u s u

s t u. s t t u s u

s t u. s t t u s u

f s t. s t image f s image f t

f g s. image (Function.o f g) s = image f (image g s)

s t. s t = s = t =

s t. cross s t = s = t =

s t. disjoint s t ¬x. x s x t

s t. disjoint s (bigUnion t) x. x t disjoint s x

t f. t bigIntersect f s. s f t s

s x. x bigIntersect s t. t s x t

s x. x bigUnion s t. t s x t

f t. bigUnion f t s. s f s t

x s. x rest s x s ¬(x = choice s)

p x. x { y. y | p y } p x

(s t. s s t) s t. s t s

(s t. s t s) s t. t s s

x y s. x insert y s x = y x s

x s t. insert x s t x t s t

s t x. x s t x s x t

s t x. x s t x s x t

s t u. s t - u s t disjoint s u

s t u. s t u s t s u

s t u. disjoint (s t) u disjoint s u disjoint t u

s t u. s t u s u t u

s t u. s (t u) = s t s u

s t u. s t u = (s t) (s u)

s t u. (s t) u = s u t u

s t u. s t u = (s u) (t u)

s t. ¬(s = t) x. x t ¬(x s)

f s t. image f (s t) = image f s image f t

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

f. (t. s. image f s = t) y. x. f x = y

s P. { x. x | x s P x } s

f s. { x. f x | x s } = image f s

x s t. s delete t x s t ¬(x s)

x s t. disjoint (insert x s) t ¬(x t) disjoint s t

x s. ¬(x s) t. s insert x t s t

s x y. x delete s y x s ¬(x = y)

s x. x s t. s = insert x t ¬(x t)

s t x. x s - t x s ¬(x t)

s t. s t x. ¬(x s) insert x s t

s. s = x t. s = insert x t ¬(x t)

y s f. y image f s x. y = f x x s

s t. s t s t a. a t ¬(a s)

x y s t. Data.Pair., x y cross s t x s y t

f s t. s image f t u. u t s = image f u

s t. t bigUnion s = bigUnion { x. t x | x s }

s t. t bigIntersect s = bigIntersect { x. t x | x s }

s t. bigUnion s t = bigUnion { x. x t | x s }

s t. bigIntersect s t = bigIntersect { x. x t | x s }

P. P (a s. ¬(a s) P (insert a s)) s. P s

t. { x y. Data.Pair., x y | x y t x } =

x y s.
    delete (insert x s) y =
    if x = y then delete s y else insert x (delete s y)

x s t. insert x s t = if x t then insert x (s t) else s t

x s t. insert x s t = if x t then s t else insert x (s t)

s t x. insert x s - t = if x t then s - t else insert x (s - t)

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

s x x'. (x s x' s) (x delete s x' x' delete s x)

s x x'. (x delete s x' x' delete s x) x s x' s

P f s. (y. y image f s P y) x. x s P (f x)

P f s. (y. y image f s P y) x. x s P (f x)

(f. image f = )
  f x s. image f (insert x s) = insert (f x) (image f s)

P f s. (t. t image f s P t) t. t s P (image f t)

f s. bigIntersect (image f s) = { y. y | x. x s y f x }

f s. bigUnion (image f s) = { y. y | x. x s y f x }

P f. { x. f x | P x } = image f { x. x | P x }

x y s.
    insert x (insert y s) = insert y (insert x s)
    insert x (insert x s) = insert x s

n.
    { m. m | Number.Natural.< m (Number.Natural.suc n) } =
    insert n { m. m | Number.Natural.< m n }

P a s. (x. x insert a s P x) P a x. x s P x

P a s. (x. x insert a s P x) P a x. x s P x

P s. (x. x bigUnion s P x) t x. t s x t P x

P s. (x. x bigUnion s P x) t x. t s x t P x

P a b. Data.Pair., a b { x y. Data.Pair., x y | P x y } P a b

P. { p. p | P p } = { a b. Data.Pair., a b | P (Data.Pair., a b) }

f s a.
    (x. f x = f a x = a)
    image f (delete s a) = delete (image f s) (f a)

f. (s t. image f s = image f t s = t) x y. f x = f y x = y

f s t.
    (x y. f x = f y x = y) image f (s - t) = image f s - image f t

f s t.
    (x y. f x = f y x = y) image f (s t) = image f s image f t

f s t. (y. y t x. f x = y) (x. f x t x s) image f s = t

(a. { x. x | x = a } = insert a ) a. { x. x | a = x } = insert a

f. (y. x. f x = y) P. image f { x. x | P (f x) } = { x. x | P x }

d t.
    { f. f | (x. x f x t) x. ¬(x ) f x = d } =
    insert (λx. d)

f s.
    (x y. x s y s f x = f y x = y) g. x. x s g (f x) = x

f u v.
    (t. t v s. s u image f s = t)
    y. y v x. x u f x = y

f s t.
    (y. y t x. x s f x = y)
    g. y. y t g y s f (g y) = y

(P. (x. x P x) T)
  P a s. (x. x insert a s P x) P a x. x s P x

(P. (x. x P x) F)
  P a s. (x. x insert a s P x) P a x. x s P x

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

f u.
    (s t. s u t u image f s = image f t s = t)
    x y. x u y u f x = f y x = y

s t a.
    { x y. Data.Pair., x y | x insert a s y t x } =
    image (Data.Pair., a) (t a)
    { x y. Data.Pair., x y | x s y t x }

s.
    { t. t | t s } =
    image (λp. { x. x | p x })
      { p. p | (x. x s p x universe) x. ¬(x s) (p x F) }

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

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

f s t.
    (x. x s f x t)
    ((x y. x s y s f x = f y x = y)
     (y. y t x. x s f x = y)
     g.
       (y. y t g y s) (y. y t f (g y) = y)
       x. x s g (f x) = x)

d a s t.
    { f. f |
      (x. x insert a s f x t) x. ¬(x insert a s) f x = d } =
    image (λ(Data.Pair., b g) x. if x = a then b else g x)
      (cross t { f. f | (x. x s f x t) x. ¬(x s) f x = d })

(P f Q. (z. z { x. f x | P x } Q z) x. P x Q (f x))
  (P f Q.
     (z. z { x y. f x y | P x y } Q z) x y. P x y Q (f x y))
  P f Q.
    (z. z { w x y. f w x y | P w x y } Q z)
    w x y. P w x y Q (f w x y)

(P f Q. (z. z { x. f x | P x } Q z) x. P x Q (f x))
  (P f Q.
     (z. z { x y. f x y | P x y } Q z) x y. P x y Q (f x y))
  P f Q.
    (z. z { w x y. f w x y | P w x y } Q z)
    w x y. P w x y Q (f w x y)

(P f. bigIntersect { x. f x | P x } = { a. a | x. P x a f x })
  (P f.
     bigIntersect { x y. f x y | P x y } =
     { a. a | x y. P x y a f x y })
  P f.
    bigIntersect { x y z. f x y z | P x y z } =
    { a. a | x y z. P x y z a f x y z }

(P f. bigUnion { x. f x | P x } = { a. a | x. P x a f x })
  (P f.
     bigUnion { x y. f x y | P x y } =
     { a. a | x y. P x y a f x y })
  P f.
    bigUnion { x y z. f x y z | P x y z } =
    { a. a | x y z. P x y z a f x y z }

Input Type Operators

Input Constants

Assumptions

T

Function.id = λx. x

F p. p

t. t ¬t

(~) = λp. p F

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

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

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

x. x = x T

() = λp q. p q p

t. (t T) (t F)

s. rest s = delete s (choice s)

p x. p x p ((select) p)

(¬T F) (¬F T)

p. x y. p = Data.Pair., x y

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

p x. x fromPredicate p p x

= { x. x | F }

universe = { x. x | T }

() = λ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

t1 t2. ¬(t1 t2) t1 ¬t2

t1 t2. ¬t1 ¬t2 t2 t1

s t. disjoint s t s t =

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

P. (p. P p) p1 p2. P (Data.Pair., p1 p2)

P. (p. P p) p1 p2. P (Data.Pair., p1 p2)

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

P a. (x. a = x P x) P a

P a. (x. x = a P x) P a

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

PAIR'. fn. a0 a1. fn (Data.Pair., a0 a1) = PAIR' a0 a1

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

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

P Q. (x. P Q x) P x. Q x

P Q. P (x. Q x) x. P Q x

P Q. P (x. Q x) x. P Q x

P Q. P (x. Q x) x. P Q x

s t. s t s t ¬(s = t)

P Q. (x. P x Q) (x. P x) Q

P Q. (x. P x) Q x. P x Q

P Q. (x. P x) Q x. P x Q

x y z. x = y y = z x = z

t1 t2 t3. t1 t2 t3 (t1 t2) t3

t1 t2 t3. t1 t2 t3 (t1 t2) t3

s t. s = t x. x s x t

s t. s t x. x s x t

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

t1 t2. (if T then t1 else t2) = t1 (if F then t1 else t2) = t2

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

p q r. p (q r) p q p r

p q r. p q r (p q) (p r)

p q r. (p q) r p r q r

P Q. (x. P x Q x) (x. P x) x. Q x

P Q. (x. P x Q x) (x. P x) x. Q x

s. bigIntersect s = { x. x | u. u s x u }

s. bigUnion s = { x. x | u. u s x u }

x y a b. Data.Pair., x y = Data.Pair., a b x = a y = b

x s. insert x s = { y. y | y = x y s }

s t. s t = { x. x | x s x t }

s t. s t = { x. x | x s x t }

s x. delete s x = { y. y | y s ¬(y = x) }

s t. s - t = { x. x | x s ¬(x t) }

P c x y. P (if c then x else y) (c P x) (¬c P y)

(m. Number.Natural.< m 0 F)
  m n.
    Number.Natural.< m (Number.Natural.suc n)
    m = n Number.Natural.< m n

f s. image f s = { y. y | x. x s y = f x }

t1 t2. (¬(t1 t2) ¬t1 ¬t2) (¬(t1 t2) ¬t1 ¬t2)

s t. cross s t = { x y. Data.Pair., x y | x s y t }

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

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

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

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

p q r.
    (p q q p) ((p q) r p q r) (p q r q p r)
    (p p p) (p p q p q)

p q r.
    (p q q p) ((p q) r p q r) (p q r q p r)
    (p p p) (p p q p q)