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

Information

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

Files

Package tarball set-finite-thm-1.10.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 (Set.fromPredicate (λv. ∃m. v = m ∧ Number.Natural.< m n))

⊦ ∀n. Set.finite (Set.fromPredicate (λv. ∃m. v = 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 (Set.fromPredicate (λv. ∃t. v = 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 (Set.fromPredicate (λv. ∃x. v = 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
      (Set.fromPredicate (λv. ∃y. v = 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
      (Set.fromPredicate
         (λv. ∃x y. v = 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 (Set.fromPredicate (λv. ∃x. v = x ∧ Set.∈ (f x) A))

⊦ ∀f t.
    Set.finite t ∧
    (∀y.
       Set.∈ y t ⇒
       Set.finite (Set.fromPredicate (λv. ∃x. v = x ∧ f x = y))) ⇒
    Set.finite (Set.fromPredicate (λv. ∃x. v = x ∧ Set.∈ (f x) t))

⊦ ∀f s t.
    Set.finite s ∧ (∀x. Set.∈ x s ⇒ Set.finite (t x)) ⇒
    Set.finite
      (Set.fromPredicate (λv. ∃x y. v = f x y ∧ Set.∈ x s ∧ Set.∈ y (t x)))

⊦ ∀d s t.
    Set.finite s ∧ Set.finite t ⇒
    Set.finite
      (Set.fromPredicate
         (λv.
            ∃f.
              v = 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
      (Set.fromPredicate (λv. ∃x. v = x ∧ Set.∈ x s ∧ Set.∈ (f x) A))

⊦ ∀f s t.
    Set.finite t ∧
    (∀y.
       Set.∈ y t ⇒
       Set.finite
         (Set.fromPredicate (λv. ∃x. v = x ∧ Set.∈ x s ∧ f x = y))) ⇒
    Set.finite
      (Set.fromPredicate (λv. ∃x. v = 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

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ~
  - cond
  - select
  - F
  - T
- Pair
  - Data.Pair.,
Function
- Function.o
Number
- Natural
  - Number.Natural.<
  - Number.Natural.≤
  - Number.Natural.max
  - Number.Natural.suc
- Numeral
  - Number.Numeral.zero
Set
- Set.-
- Set.∅
- Set.bigUnion
- Set.cross
- Set.delete
- Set.finite
- Set.fromPredicate
- Set.image
- Set.∈
- Set.infinite
- Set.insert
- 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)

⊦ Set.fromPredicate
(λv. ∃m. v = m ∧ Number.Natural.< m Number.Numeral.zero) = Set.∅

⊦ ∀f g x. Function.o 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.o f g) s = Set.image f (Set.image g s)

⊦ ∀P.
P Number.Numeral.zero ∧ (∀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 (Set.fromPredicate (λv. ∃y. v = 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.
    Set.fromPredicate
      (λv. ∃x y. v = 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 Number.Numeral.zero ⇔ F) ∧
  ∀m n.
    Number.Natural.< m (Number.Natural.suc n) ⇔
    m = n ∨ Number.Natural.< m n

⊦ ∀f s.
Set.image f s =
Set.fromPredicate (λv. ∃y. v = 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 =
    Set.fromPredicate
      (λv. ∃x y. v = Data.Pair., x y ∧ Set.∈ x s ∧ Set.∈ y t)

⊦ ∀n.
    Set.fromPredicate
      (λv. ∃m. v = m ∧ Number.Natural.< m (Number.Natural.suc n)) =
    Set.insert n (Set.fromPredicate (λv. ∃m. v = m ∧ Number.Natural.< m n))

⊦ ∀P a b.
Set.∈ (Data.Pair., a b)
(Set.fromPredicate (λv. ∃x y. v = 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.
    Set.fromPredicate
      (λv.
         ∃f.
           v = f ∧ (∀x. Set.∈ x Set.∅ ⇒ Set.∈ (f x) t) ∧
           ∀x. ¬Set.∈ x Set.∅ ⇒ f x = d) = Set.insert (λx. d) Set.∅

⊦ ∀s t a.
    Set.fromPredicate
      (λv.
         ∃x y.
           v = Data.Pair., x y ∧ Set.∈ x (Set.insert a s) ∧
           Set.∈ y (t x)) =
    Set.∪ (Set.image (Data.Pair., a) (t a))
      (Set.fromPredicate
         (λv. ∃x y. v = Data.Pair., x y ∧ Set.∈ x s ∧ Set.∈ y (t x)))

⊦ ∀s.
    Set.fromPredicate (λv. ∃t. v = t ∧ Set.⊆ t s) =
    Set.image (λp. Set.fromPredicate (λv. ∃x. v = x ∧ p x))
      (Set.fromPredicate
         (λv.
            ∃p.
              v = p ∧ (∀x. Set.∈ x s ⇒ Set.∈ (p x) Set.universe) ∧
              ∀x. ¬Set.∈ x s ⇒ (p x ⇔ F)))

⊦ ∀d a s t.
    Set.fromPredicate
      (λv.
         ∃f.
           v = 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
         (Set.fromPredicate
            (λv.
               ∃f.
                 v = f ∧ (∀x. Set.∈ x s ⇒ Set.∈ (f x) t) ∧
                 ∀x. ¬Set.∈ x s ⇒ f x = d)))

⊦ (∀P f Q.
     (∀z. Set.∈ z (Set.fromPredicate (λv. ∃x. v = f x ∧ P x)) ⇒ Q z) ⇔
     ∀x. P x ⇒ Q (f x)) ∧
  (∀P f Q.
     (∀z.
        Set.∈ z (Set.fromPredicate (λv. ∃x y. v = f x y ∧ P x y)) ⇒ Q z) ⇔
     ∀x y. P x y ⇒ Q (f x y)) ∧
  ∀P f Q.
    (∀z.
       Set.∈ z (Set.fromPredicate (λv. ∃w x y. v = f w x y ∧ P w x y)) ⇒
       Q z) ⇔ ∀w x y. P w x y ⇒ Q (f w x y)