Package set-finite: Finite set theory

Information

Files

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

Defined Constants

• Set
  • finite
  • infinite

Theorems

⊦ finite ∅

⊦ finite universe

⊦ infinite universe

⊦ ∀a. finite (insert a ∅)

⊦ ∀s. infinite s ⇔ ¬finite s

⊦ ∀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 | Number.Natural.< m n }

⊦ ∀n. finite { m. m | Number.Natural.≤ 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)

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

⊦ ∀s. finite s ⇔ ∃a. ∀x. x ∈ s ⇒ Number.Natural.≤ 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

⊦ ∀a. finite a ⇔ a = ∅ ∨ ∃x s. a = insert x s ∧ finite s

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

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

⊦ ∀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. Data.Pair., 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
    • Data.Pair.*
• Number
  • Natural
    • Number.Natural.natural
• Set
  • set

Input Constants

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

Assumptions

⊦ T

⊦ bigUnion ∅ = ∅

⊦ ∀x. x ∈ universe

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

⊦ ∀x. x = x ⇔ T

⊦ universe = insert T (insert F ∅)

⊦ ∀x s. 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. s - t ⊆ s

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

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

⊦ ∀s. s ⊆ ∅ ⇔ s = ∅

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

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

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

⊦ ∀p x. x ∈ 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. 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 | Number.Natural.< m 0 } = ∅

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

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

⊦ ∀P. (∃p. P p) ⇔ ∃p1 p2. P (Data.Pair., 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 (Data.Pair., 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

⊦ ∀x s t. s ⊆ insert x t ⇔ 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. 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. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

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

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

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

⊦ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ 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

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

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

⊦ ∀A B C D. (A ⇒ B) ∧ (C ⇒ D) ⇒ A ∧ C ⇒ B ∧ D

⊦ ∀A B C D. (A ⇒ B) ∧ (C ⇒ D) ⇒ A ∨ C ⇒ B ∨ D

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

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

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

⊦ ∀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. Data.Pair., x y | x ∈ s ∧ y ∈ t }

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

⊦ ∀P a b. 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. x ∈ ∅ ⇒ f x ∈ t) ∧ ∀x. ¬(x ∈ ∅) ⇒ f x = d } =
    insert (λx. d) ∅

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

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