Package set-size-def: set-size-def

Information

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

Files

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

Defined Constants

Set
- Set.hasSize
- Set.size

Theorems

⊦ ∀s.
Set.size s =
Set.fold (λx n. Number.Natural.suc n) s Number.Numeral.zero

⊦ ∀s n. Set.hasSize s n ⇔ Set.finite s ∧ Set.size s = n

Input Type Operators

→
bool
Number
- Natural
  - Number.Natural.natural
Set
- Set.set

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - T
Number
- Natural
  - Number.Natural.suc
- Numeral
  - Number.Numeral.zero
Set
- Set.finite
- Set.fold

Assumptions

⊦ T

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