Package set-fold-def: Definition of a fold operation on finite sets

Information

name	set-fold-def
version	1.25
description	Definition of a fold operation on finite sets
author	Joe Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2011-11-27
requires	bool natural set-thm set-finite
show	Data.Bool Number.Natural Set

Files

Package tarball set-fold-def-1.25.tgz
Theory file set-fold-def.thy (included in the package tarball)

Defined Constant

Set
- fold

Theorem

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

Input Type Operators

→
bool
Number
- Natural
  - natural
Set
- set

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - F
  - T
Number
- Natural
  - suc
  - zero
Set
- ∅
- delete
- finite
- insert
- ∈

Assumptions

⊦ T

⊦ finite ∅

⊦ ¬F ⇔ T

⊦ ∀t. t ⇒ t

⊦ F ⇔ ∀p. p

⊦ ∀x. ¬(x ∈ ∅)

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ F

⊦ (∃) = λP. P ((select) P)

⊦ ∀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. T ∨ t ⇔ T

⊦ ∀t. t ∨ F ⇔ t

⊦ ∀n. ¬(suc n = 0)

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

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

⊦ ∀t. t ⇒ F ⇔ ¬t

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

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

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

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1

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

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

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

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

⊦ ∀t1 t2. ¬(t1 ∧ t2) ⇔ ¬t1 ∨ ¬t2

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

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

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

⊦ ∀x y s. delete (delete s x) y = delete (delete s y) x

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

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

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

⊦ (∃!) = λP. (∃) P ∧ ∀x y. P x ∧ P y ⇒ x = y

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

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

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

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