Package list-set-thm: Properties of list to set conversions
Information
| name | list-set-thm |
| version | 1.27 |
| description | Properties of list to set conversions |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2011-12-18 |
| requires | bool natural set list-def list-thm list-length list-set-def |
| show | Data.Bool Data.List Number.Natural Set |
Files
- Package tarball list-set-thm-1.27.tgz
- Theory file list-set-thm.thy (included in the package tarball)
Theorems
⊦ ∀l. finite (toSet l)
⊦ ∀l. size (toSet l) ≤ length l
⊦ ∀l. toSet l = ∅ ⇔ l = []
⊦ ∀s. finite s ⇒ toSet (fromSet s) = s
⊦ ∀s. finite s ⇒ length (fromSet s) = size s
Input Type Operators
- →
- bool
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
- Set
- set
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- cond
- F
- T
- List
- ::
- []
- fromSet
- length
- toSet
- Bool
- Number
- Natural
- ≤
- suc
- zero
- Natural
- Set
- ∅
- finite
- insert
- ∈
- size
Assumptions
⊦ T
⊦ finite ∅
⊦ ¬F ⇔ T
⊦ size ∅ = 0
⊦ toSet [] = ∅
⊦ ∀n. 0 ≤ n
⊦ ∀n. n ≤ n
⊦ F ⇔ ∀p. p
⊦ ∀n. n ≤ suc n
⊦ (¬) = λp. p ⇒ F
⊦ (∀) = λp. p = λx. T
⊦ ∀t. (T ⇔ t) ⇔ t
⊦ ∀t. t ∧ T ⇔ t
⊦ ∀t. T ⇒ t ⇔ t
⊦ ∀t. (F ⇔ t) ⇔ ¬t
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀h t. ¬(h :: t = [])
⊦ ∀x s. ¬(insert x s = ∅)
⊦ ∀s x. finite (insert x s) ⇔ finite s
⊦ ∀h t. length (h :: t) = suc (length t)
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀h t. toSet (h :: t) = insert h (toSet t)
⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀s. finite s ⇒ toSet (fromSet s) = s ∧ length (fromSet s) = size s
⊦ ∀P. P [] ∧ (∀a0 a1. P a1 ⇒ P (a0 :: a1)) ⇒ ∀x. P x
⊦ ∀x s.
finite s ⇒ size (insert x s) = if x ∈ s then size s else suc (size s)
⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)