Package list-set-thm: Properties of list to set conversions
Information
| name | list-set-thm |
| version | 1.29 |
| description | Properties of list to set conversions |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2012-02-07 |
| 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.29.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
- ⊥
- ⊤
- List
- ::
- []
- fromSet
- length
- toSet
- Bool
- Number
- Natural
- ≤
- suc
- zero
- Natural
- Set
- ∅
- finite
- insert
- ∈
- size
Assumptions
⊦ ⊤
⊦ finite ∅
⊦ ¬⊥ ⇔ ⊤
⊦ size ∅ = 0
⊦ toSet [] = ∅
⊦ ∀n. 0 ≤ n
⊦ ∀n. n ≤ n
⊦ ⊥ ⇔ ∀p. p
⊦ ∀n. n ≤ suc n
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. (⊥ ⇔ 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 ⊤ ⊤
⊦ (∃) = λ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)