Package set-finite-thm: Properties of finite sets

Information

name	set-finite-thm
version	1.28
description	Properties of finite sets
author	Joe Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2011-11-27
requires	bool function pair natural set-def set-thm set-finite-def
show	Data.Bool Data.Pair Function Number.Natural Set

Files

Package tarball set-finite-thm-1.28.tgz
Theory file set-finite-thm.thy (included in the package tarball)

Theorems

⊦ finite universe

⊦ infinite universe

⊦ ∀a. finite (insert a ∅)

⊦ ∀s. infinite s ⇒ ¬(s = ∅)

⊦ ∀s x. finite s ⇒ finite (delete s x)

⊦ ∀s x. finite (delete s x) ⇔ finite s

⊦ ∀s x. finite (insert x s) ⇔ finite s

⊦ ∀s t. finite s ⇒ finite (s \ t)

⊦ ∀s. finite s ⇒ ∃a. ¬(a ∈ s)

⊦ ∀f s. finite s ⇒ finite (image f s)

⊦ ∀s t. finite t ∧ s ⊆ t ⇒ finite s

⊦ ∀n. finite { m. m | m < n }

⊦ ∀n. finite { m. m | m ≤ n }

⊦ ∀s t. finite (s ∪ t) ⇔ finite s ∧ finite t

⊦ ∀s t. finite s ∧ finite t ⇒ finite (s ∪ t)

⊦ ∀s t. infinite s ∧ finite t ⇒ infinite (s \ t)

⊦ ∀s t. finite s ∨ finite t ⇒ finite (s ∩ t)

⊦ ∀s t. finite s ∧ finite t ⇒ finite (cross s t)

⊦ ∀s. finite s ⇔ ∃a. ∀x. x ∈ s ⇒ x ≤ a

⊦ ∀s. finite s ⇒ finite { t. t | t ⊆ s }

⊦ ∀s. finite s ⇒ (finite (bigUnion s) ⇔ ∀t. t ∈ s ⇒ finite t)

⊦ ∀s. finite (bigUnion s) ⇔ finite s ∧ ∀t. t ∈ s ⇒ finite t

⊦ ∀s P. finite s ⇒ finite { x. x | x ∈ s ∧ P x }

⊦ ∀f s. (∀x y. f x = f y ⇒ x = y) ∧ infinite s ⇒ infinite (image f s)

⊦ ∀f. (∀x y. f x = f y ⇒ x = y) ⇒ ∀s. infinite (image f s) ⇔ infinite s

⊦ ∀f s. finite s ⇒ finite { y. y | ∃x. x ∈ s ∧ y = f x }

⊦ ∀f s t.
finite t ∧ t ⊆ image f s ⇔ ∃s'. finite s' ∧ s' ⊆ s ∧ t = image f s'

⊦ ∀f s t.
finite t ∧ t ⊆ image f s ⇒ ∃s'. finite s' ∧ s' ⊆ s ∧ t ⊆ image f s'

⊦ ∀s t. finite s ∧ finite t ⇒ finite { x y. x, y | x ∈ s ∧ y ∈ t }

⊦ ∀P.
P ∅ ∧ (∀x s. P s ∧ ¬(x ∈ s) ∧ finite s ⇒ P (insert x s)) ⇒
∀s. finite s ⇒ P s

⊦ ∀P f s.
(∃t. finite t ∧ t ⊆ image f s ∧ P t) ⇔
∃t. finite t ∧ t ⊆ s ∧ P (image f t)

⊦ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
(finite (image f s) ⇔ finite s)

⊦ ∀f A. (∀x y. f x = f y ⇒ x = y) ∧ finite A ⇒ finite { x. x | f x ∈ A }

⊦ ∀f t.
finite t ∧ (∀y. y ∈ t ⇒ finite { x. x | f x = y }) ⇒
finite { x. x | f x ∈ t }

⊦ ∀f s t.
finite s ∧ (∀x. x ∈ s ⇒ finite (t x)) ⇒
finite { x y. f x y | x ∈ s ∧ y ∈ t x }

⊦ ∀d s t.
finite s ∧ finite t ⇒
finite { f. f | (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. ¬(x ∈ s) ⇒ f x = d }

⊦ ∀f A s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧ finite A ⇒
finite { x. x | x ∈ s ∧ f x ∈ A }

⊦ ∀f s t.
finite t ∧ (∀y. y ∈ t ⇒ finite { x. x | x ∈ s ∧ f x = y }) ⇒
finite { x. x | x ∈ s ∧ f x ∈ t }

Input Type Operators

→
bool
Data
- Pair
  - ×
Number
- Natural
  - natural
Set
- set

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - F
  - T
- Pair
  - ,
Function
- ∘
Number
- Natural
  - <
  - ≤
  - max
  - suc
  - zero
Set
- ∅
- bigUnion
- cross
- delete
- \
- finite
- fromPredicate
- image
- infinite
- insert
- ∩
- ∈
- ⊆
- ∪
- universe

Assumptions

⊦ T

⊦ finite ∅

⊦ ¬F ⇔ T

⊦ ¬T ⇔ F

⊦ bigUnion ∅ = ∅

⊦ ∀x. x ∈ universe

⊦ ∀t. t ⇒ t

⊦ ∀s. s ⊆ s

⊦ F ⇔ ∀p. p

⊦ fromPredicate (λx. F) = ∅

⊦ ∀x. ¬(x ∈ ∅)

⊦ ∀t. t ∨ ¬t

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

⊦ universe = insert T (insert F ∅)

⊦ ∀t. (t ⇔ F) ⇔ ¬t

⊦ ∀t. t ⇒ F ⇔ ¬t

⊦ ∀s. infinite s ⇔ ¬finite s

⊦ ∀x s. delete s x ⊆ s

⊦ ∀m n. m ≤ max m n

⊦ ∀m n. n ≤ max m n

⊦ ∀s t. s \ t ⊆ s

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀s. s ⊆ ∅ ⇔ s = ∅

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x s. finite s ⇒ finite (insert x s)

⊦ ∀a b. (a ⇔ b) ⇒ a ⇒ b

⊦ ∀p x. x ∈ fromPredicate p ⇔ p x

⊦ ∀m n. ¬(m ≤ n) ⇔ n < m

⊦ ∀m n. m < suc n ⇔ m ≤ n

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

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ ∀x s. x ∈ s ⇔ insert x s = s

⊦ ∀x s. insert x ∅ ∪ s = insert x s

⊦ ∀t1 t2. ¬t1 ⇒ ¬t2 ⇔ t2 ⇒ t1

⊦ ∀s u. bigUnion (insert s u) = s ∪ bigUnion u

⊦ { m. m | m < 0 } = ∅

⊦ ∀f g x. (f ∘ g) x = f (g x)

⊦ ∀x s. delete s x = s ⇔ ¬(x ∈ s)

⊦ ∀P. (∃p. P p) ⇔ ∃p1 p2. P (p1, p2)

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀x s. x ∈ s ⇒ insert x (delete s x) = s

⊦ ∀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

⊦ ∀m n. m < suc n ⇔ m = n ∨ m < n

⊦ ∀x s t. s ⊆ insert x t ⇔ delete s x ⊆ t

⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r

⊦ ∀t1 t2 t3. (t1 ∧ t2) ∧ t3 ⇔ t1 ∧ t2 ∧ t3

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀s t u. s ⊆ t ∪ u ⇔ s \ t ⊆ u

⊦ ∀s t u. s ∪ t ∪ u = s ∪ (t ∪ u)

⊦ ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

⊦ ∀s t. (∀x. x ∈ s ⇔ x ∈ t) ⇔ s = t

⊦ ∀f s t. s ⊆ t ⇒ image f s ⊆ image f t

⊦ ∀f g s. image (f ∘ g) s = image f (image g s)

⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n

⊦ ∀s x. x ∈ bigUnion s ⇔ ∃t. t ∈ s ∧ x ∈ t

⊦ ∀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

⊦ ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t

⊦ ∀y s f. y ∈ image f s ⇔ ∃x. y = f x ∧ x ∈ s

⊦ ∀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 } = ∅

⊦ ∀FINITE'.
FINITE' ∅ ∧ (∀x s. FINITE' s ⇒ FINITE' (insert x s)) ⇒
∀a. finite a ⇒ FINITE' a

⊦ ∀f s. image f s = { y. y | ∃x. x ∈ s ∧ y = f x }

⊦ ∀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)

⊦ ∀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

⊦ ∀d t.
{ f. f | (∀x. x ∈ ∅ ⇒ f x ∈ t) ∧ ∀x. ¬(x ∈ ∅) ⇒ f x = d } =
insert (λx. d) ∅

⊦ ∀p f q. (∀z. z ∈ { x y. f x y | p x y } ⇒ q z) ⇔ ∀x y. p x y ⇒ q (f x 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) }

⊦ ∀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 })