Package set-size-thm: Properties of finite set cardinality

Information

nameset-size-thm
version1.28
descriptionProperties of finite set cardinality
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-27
requiresbool
pair
natural
set-def
set-thm
set-finite
set-fold
set-size-def
showData.Bool
Data.Pair
Number.Natural
Set

Files

Theorems

size = 0

hasSize universe 2

x. hasSize (insert x ) 1

x. size (insert x ) = 1

s. finite s hasSize s (size s)

s. hasSize s 0 s =

s n. hasSize s n size s = n

s. finite s (size s = 0 s = )

f s. finite s size (image f s) size s

n. hasSize { m. m | m < n } n

n. size { m. m | m < n } = n

a b. a b finite b size a < size b

a b. a b finite b size a size b

n. hasSize { m. m | m n } (n + 1)

n. size { m. m | m n } = n + 1

f s t. finite t s image f t size s size t

s t. finite s finite t size (s t) size s + size t

s t. finite t s t (size s = size t s = t)

a b. finite b a b size a = size b a = b

a b. finite b a b size b size a a = b

s t. finite s finite t size (cross s t) = size s * size t

s n. finite s n size s t. t s hasSize t n

s n. (finite s n size s) t. t s hasSize t n

x s.
    finite s size (insert x s) = if x s then size s else suc (size s)

s t. finite s t s size (s \ t) = size s - size t

s t. finite s finite t size (s t) = size s + size (t \ s)

s t m n. hasSize s m hasSize t n hasSize (cross s t) (m * n)

x s. finite s size (delete s x) = if x s then size s - 1 else size s

s. finite s size { t. t | t s } = exp 2 (size s)

s n. hasSize s n hasSize { t. t | t s } (exp 2 n)

s t.
    finite s finite t (size (s t) = size s + size t disjoint s t)

s t. finite s finite t disjoint s t size (s t) = size s + size t

s n. hasSize s (suc n) ¬(s = ) a. a s hasSize (delete s a) n

s t. finite s finite t size (s t) = size s + size t - size (s t)

s t. finite s finite t size (s t) + size (s t) = size s + size t

s t.
    finite s finite t size (s t) < size s + size t ¬disjoint s t

s n. hasSize s (suc n) a t. hasSize t n ¬(a t) s = insert a t

s t m n.
    hasSize s m hasSize t n disjoint s t hasSize (s t) (m + n)

s t m n. hasSize s m hasSize t n t s hasSize (s \ t) (m - n)

s t u. finite u disjoint s t s t = u size s + size t = size u

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

s t.
    finite s finite t
    size { x y. x, y | x s y t } = size s * size t

s n.
    hasSize s n
    f. (m. m < n f m s) x. x s ∃!m. m < n f m = x

f s.
    (x y. x s y s f x = f y x = y) finite s
    size (image f s) = size s

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

f s n.
    (x y. x s y s f x = f y x = y)
    (hasSize (image f s) n hasSize s n)

f s n.
    (x y. x s y s f x = f y x = y) hasSize s n
    hasSize (image f s) n

s t m n.
    hasSize s m hasSize t n
    hasSize { x y. x, y | x s y t } (m * n)

f s t.
    finite s (x. x s f x t) (y. y t ∃!x. x s f x = y)
    size t = size s

s t f.
    finite s size s = size t image f s = t
    x y. x s y s f x = f y x = y

s t.
    finite s finite t size s size t
    f. image f s t x y. x s y s f x = f y x = y

s t m n.
    hasSize s m (x. x s finite (t x) size (t x) n)
    size (bigUnion { x. t x | x s }) m * n

s t m n.
    hasSize s m (x. x s hasSize (t x) n)
    hasSize { x y. x, y | x s y t x } (m * n)

d s t.
    finite s finite t
    size { f. f | (x. x s f x t) x. ¬(x s) f x = d } =
    exp (size t) (size s)

d s t m n.
    hasSize s m hasSize t n
    hasSize { f. f | (x. x s f x t) x. ¬(x s) f x = d }
      (exp n m)

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

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

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

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

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

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

s t m n.
    hasSize s m (x. x s hasSize (t x) n)
    (x y. x s y s ¬(x = y) disjoint (t x) (t y))
    hasSize (bigUnion { x. t x | x s }) (m * n)

s t.
    finite s finite t size s = size t
    f.
      (x. x s f x t) (y. y t x. x s f x = y)
      x y. x s y s f x = f y x = y

Input Type Operators

Input Constants

Assumptions

T

finite

¬F T

¬T F

bit0 0 = 0

bigUnion =

t. t t

n. 0 n

n. n n

s. s

s. s s

F p. p

x. ¬(x )

a. finite (insert a )

t. t ¬t

n. ¬(n < n)

n. n < suc n

(¬) = λp. p F

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

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

t. ¬¬t t

t. (T t) t

t. (t T) t

t. F t F

t. T t t

t. t F F

t. t T t

t. t t t

t. F t T

t. T t t

t. t T T

t. F t t

t. T t T

t. t F t

t. t T T

n. ¬(suc n = 0)

m. m < 0 F

n. 0 * n = 0

n. 0 + n = n

m. m - 0 = m

n. n - n = 0

f. image f =

universe = insert T (insert F )

size = fold (λx n. suc n) 0

t. (F t) ¬t

t. (t F) ¬t

t. t F ¬t

n. bit1 n = suc (bit0 n)

m. exp m 0 = 1

s t. disjoint s (t \ s)

() = λp q. p q p

t. (t T) (t F)

m. suc m = m + 1

m. m 0 m = 0

n. suc n - 1 = n

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

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

x s. ¬(insert x s = )

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

n. bit0 (suc n) = suc (suc (bit0 n))

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

p. x y. p = (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

m n. m * n = n * m

m n. m + n = n + m

m n. m = n m n

m n. m < n m n

m n. m + n - n = m

s x. finite (delete s x) finite s

s x. finite (insert x s) finite s

s t. finite s finite (s \ t)

s t. s t = t s

f s. finite s finite (image f s)

p x. x fromPredicate p p x

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

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

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

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m = suc n m = n

m n. suc m suc n m n

m n. m + n = m n = 0

s t. disjoint s t s t =

s t. s t s t = t

s t. s \ t = s t

s t. s \ t = s disjoint s t

s t. s \ t \ t = s \ t

s t. s \ t t = s t

s t. finite t s t finite s

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

{ m. m | m < 0 } =

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

m n. m * suc n = m + m * n

m n. exp m (suc n) = m * exp m n

m n. suc m * n = m * n + n

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

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

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

m n. m n d. n = m + d

s t x. s t s insert x t

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

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

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

m n. m n n m m = n

s n. hasSize s n finite s size s = n

s t. s (t \ s) = t s t

s t. s t t s s = t

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

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

f s x. x s f x image f s

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

m n. m < n m n ¬(m = n)

m n. m < suc n m = n m < n

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

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

s. bigUnion s = t. t s t =

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

p q r. p q r p q r

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

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

m n p. m + (n + p) = m + n + p

m n p. m + n = m + p n = p

m n p. m < n n < p m < p

m n p. m n n < p m < p

m n p. m n n p m p

s t. s t x. x s x t

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

m n. n < m suc (m - suc n) = m - n

s. finite s (finite (bigUnion s) t. t s finite t)

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

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

P. P 0 (n. P n P (suc n)) n. P n

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

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

(∃!) = λP. () P x y. P x P y x = y

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

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

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

s t x. x s \ t x s ¬(x t)

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

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

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

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

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

x y a b. (x, y) = (a, b) x = a y = b

x y s t. (x, y) cross s t x s y t

m n p q. m p n q m + n p + q

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

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

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

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

n. { m. m | m < suc n } = insert n { m. m | m < n }

P a b. (a, b) { x y. x, y | P x y } P a b

P.
    P (x s. P s ¬(x s) finite s P (insert x s))
    s. finite s P s

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

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

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

s t a.
    { x y. x, y | x insert a s y t x } =
    image ((,) a) (t a) { x y. 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) }

f b.
    (x y s. ¬(x = y) f x (f y s) = f y (f x s))
    fold f b = b
    x s.
      finite s
      fold f b (insert x s) =
      if x s then fold f b s else f x (fold f b s)

d a s t.
    { f. f |
      (x. x insert a s f x t) x. ¬(x insert a s) f x = d } =
    image (λ(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 })