Package set-finite-thm: set-finite-thm

Information

name	set-finite-thm
version	1.15
description	set-finite-thm
author	Joe Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2011-09-21
show	Data.Bool

Files

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

Theorems

⊦ Set.finite Set.∅

⊦ Set.finite Set.universe

⊦ Set.infinite Set.universe

⊦ ∀a. Set.finite (Set.insert a Set.∅)

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

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

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

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

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

⊦ ∀s. Set.finite s ⇒ ∃a. ¬Set.∈ a s

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

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

⊦ ∀n. Set.finite { m. m | Number.Natural.< m n }

⊦ ∀n. Set.finite { m. m | Number.Natural.≤ m n }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Input Type Operators

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

Input Constants

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

Assumptions

⊦ T

⊦ Set.bigUnion Set.∅ = Set.∅

⊦ ∀x. Set.∈ x Set.universe

⊦ ∀s. Set.⊆ s s

⊦ F ⇔ ∀p. p

⊦ Set.fromPredicate (λx. F) = Set.∅

⊦ ∀x. ¬Set.∈ x Set.∅

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ F

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀t. (λx. t x) = t

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

⊦ ∀x. x = x ⇔ T

⊦ Set.universe = Set.insert T (Set.insert F Set.∅)

⊦ ∀s. Set.infinite s ⇔ ¬Set.finite s

⊦ ∀x s. Set.⊆ (Set.delete s x) s

⊦ ∀m n. Number.Natural.≤ m (Number.Natural.max m n)

⊦ ∀m n. Number.Natural.≤ n (Number.Natural.max m n)

⊦ ∀s t. Set.⊆ (Set.\ s t) s

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

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

⊦ ∀s. Set.⊆ s Set.∅ ⇔ s = Set.∅

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

⊦ (¬T ⇔ F) ∧ (¬F ⇔ T)

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

⊦ ∀p x. Set.∈ x (Set.fromPredicate p) ⇔ p x

⊦ ∀m n. ¬Number.Natural.≤ m n ⇔ Number.Natural.< n m

⊦ ∀m n. Number.Natural.< m (Number.Natural.suc n) ⇔ Number.Natural.≤ m n

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

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

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

⊦ ∀x s. Set.∪ (Set.insert x Set.∅) s = Set.insert x s

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

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

⊦ { m. m | Number.Natural.< m 0 } = Set.∅

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

⊦ ∀x s. Set.delete s x = s ⇔ ¬Set.∈ x s

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

⊦ Set.finite Set.∅ ∧ ∀x s. Set.finite s ⇒ Set.finite (Set.insert x s)

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

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

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

⊦ (∀s. Set.∪ Set.∅ s = s) ∧ ∀s. Set.∪ s Set.∅ = s

⊦ ∀f s x. Set.∈ x s ⇒ Set.∈ (f x) (Set.image f s)

⊦ ∀P. (∀x y. P x y) ⇔ ∀y x. P x y

⊦ ∀P Q. (∀x. P ⇒ Q x) ⇔ P ⇒ ∀x. Q x

⊦ ∀x s t. Set.⊆ s (Set.insert x t) ⇔ Set.⊆ (Set.delete s x) t

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

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

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

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

⊦ ∀s t u. Set.⊆ s (Set.∪ t u) ⇔ Set.⊆ (Set.\ s t) u

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

⊦ ∀s t. s = t ⇔ ∀x. Set.∈ x s ⇔ Set.∈ x t

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

⊦ ∀f s t. Set.⊆ s t ⇒ Set.⊆ (Set.image f s) (Set.image f t)

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

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

⊦ ∀s x. Set.∈ x (Set.bigUnion s) ⇔ ∃t. Set.∈ t s ∧ Set.∈ x t

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

⊦ ∀p x. Set.∈ x { y. y | p y } ⇔ p x

⊦ (∀s t. Set.⊆ s (Set.∪ s t)) ∧ ∀s t. Set.⊆ s (Set.∪ t s)

⊦ (∀s t. Set.⊆ (Set.∩ s t) s) ∧ ∀s t. Set.⊆ (Set.∩ t s) s

⊦ ∀x y s. Set.∈ x (Set.insert y s) ⇔ x = y ∨ Set.∈ x s

⊦ ∀s t x. Set.∈ x (Set.∪ s t) ⇔ Set.∈ x s ∨ Set.∈ x t

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

⊦ ∀P c x y. P (if c then x else y) ⇔ (c ⇒ P x) ∧ (¬c ⇒ P y)

⊦ ∀t. { x y. Data.Pair., x y | Set.∈ x Set.∅ ∧ Set.∈ y (t x) } = Set.∅

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

⊦ (∀m. Number.Natural.< m 0 ⇔ F) ∧
  ∀m n.
    Number.Natural.< m (Number.Natural.suc n) ⇔
    m = n ∨ Number.Natural.< m n

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

⊦ ∀P f s. (∀y. Set.∈ y (Set.image f s) ⇒ P y) ⇔ ∀x. Set.∈ x s ⇒ P (f x)

⊦ ∀P f s. (∃y. Set.∈ y (Set.image f s) ∧ P y) ⇔ ∃x. Set.∈ x s ∧ P (f x)

⊦ ∀s t. Set.cross s t = { x y. Data.Pair., x y | Set.∈ x s ∧ Set.∈ y t }

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

⊦ ∀P a b. Set.∈ (Data.Pair., a b) { x y. Data.Pair., x y | P x y } ⇔ P a b

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

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

⊦ ∀s t a.
    { x y. Data.Pair., x y | Set.∈ x (Set.insert a s) ∧ Set.∈ y (t x) } =
    Set.∪ (Set.image (Data.Pair., a) (t a))
      { x y. Data.Pair., x y | Set.∈ x s ∧ Set.∈ y (t x) }

⊦ ∀s.
    { t. t | Set.⊆ t s } =
    Set.image (λp. { x. x | p x })
      { p. p |
        (∀x. Set.∈ x s ⇒ Set.∈ (p x) Set.universe) ∧
        ∀x. ¬Set.∈ x s ⇒ (p x ⇔ F) }

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

⊦ (∀P f Q. (∀z. Set.∈ z { x. f x | P x } ⇒ Q z) ⇔ ∀x. P x ⇒ Q (f x)) ∧
  (∀P f Q.
     (∀z. Set.∈ z { x y. f x y | P x y } ⇒ Q z) ⇔
     ∀x y. P x y ⇒ Q (f x y)) ∧
  ∀P f Q.
    (∀z. Set.∈ 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)