Package list-member-thm: Properties of the list member function
Information
| name | list-member-thm |
| version | 1.30 |
| description | Properties of the list member function |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2011-11-27 |
| requires | bool function natural set list-def list-length list-set list-append list-map list-quant list-filter list-reverse list-nth list-member-def |
| show | Data.Bool Data.List Function Number.Natural Set |
Files
- Package tarball list-member-thm-1.30.tgz
- Theory file list-member-thm.thy (included in the package tarball)
Theorems
⊦ ∀x l. member x l ⇔ x ∈ toSet l
⊦ ∀l x. member x (reverse l) ⇔ member x l
⊦ ∀l n. n < length l ⇒ member (nth n l) l
⊦ ∀s. finite s ⇒ ∀x. member x (fromSet s) ⇔ x ∈ s
⊦ ∀P l. (∀x. member x l ⇒ P x) ⇔ all P l
⊦ ∀P l. (∃x. P x ∧ member x l) ⇔ exists P l
⊦ ∀P l x. member x (filter P l) ⇔ P x ∧ member x l
⊦ ∀x l1 l2. member x (l1 @ l2) ⇔ member x l1 ∨ member x l2
⊦ ∀l x. member x l ⇔ ∃i. i < length l ∧ x = nth i l
⊦ ∀f y l. member y (map f l) ⇔ ∃x. member x l ∧ y = f x
⊦ ∀P Q l. (∀x. member x l ∧ P x ⇒ Q x) ∧ all P l ⇒ all Q l
⊦ ∀P Q l. (∀x. member x l ∧ P x ⇒ Q x) ∧ exists P l ⇒ exists Q l
Input Type Operators
- →
- bool
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
- Set
- set
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- F
- T
- List
- ::
- @
- []
- all
- exists
- filter
- fromSet
- length
- map
- member
- nth
- reverse
- toSet
- Bool
- Function
- id
- Number
- Natural
- <
- suc
- zero
- Natural
- Set
- ∅
- finite
- insert
- ∈
Assumptions
⊦ T
⊦ ¬F ⇔ T
⊦ ¬T ⇔ F
⊦ length [] = 0
⊦ reverse [] = []
⊦ toSet [] = ∅
⊦ ∀p. all p []
⊦ F ⇔ ∀p. p
⊦ ∀x. ¬member x []
⊦ ∀x. ¬(x ∈ ∅)
⊦ ∀x. id x = x
⊦ ∀n. 0 < suc n
⊦ ∀p. ¬exists p []
⊦ (¬) = λp. p ⇒ F
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (∃x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. T
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀t. (T ⇔ t) ⇔ t
⊦ ∀t. F ∧ t ⇔ F
⊦ ∀t. T ∧ t ⇔ t
⊦ ∀t. t ∧ F ⇔ F
⊦ ∀t. F ⇒ t ⇔ T
⊦ ∀t. T ⇒ t ⇔ t
⊦ ∀t. t ⇒ T ⇔ T
⊦ ∀t. F ∨ t ⇔ t
⊦ ∀t. T ∨ t ⇔ T
⊦ ∀t. t ∨ F ⇔ t
⊦ ∀t. t ∨ T ⇔ T
⊦ ∀m. m < 0 ⇔ F
⊦ ∀l. [] @ l = l
⊦ ∀f. map f [] = []
⊦ ∀P. filter P [] = []
⊦ ∀t. (F ⇔ t) ⇔ ¬t
⊦ ∀t. t ⇒ F ⇔ ¬t
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)
⊦ ∀s. finite s ⇒ toSet (fromSet s) = s
⊦ ∀x y. x = y ⇒ y = x
⊦ ∀h t. nth 0 (h :: t) = h
⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1
⊦ ∀h t. length (h :: t) = suc (length t)
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x
⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀h t. toSet (h :: t) = insert h (toSet t)
⊦ ∀m n. suc m < suc n ⇔ m < n
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀x l. reverse (x :: l) = reverse l @ x :: []
⊦ ∀P Q. P ∧ (∃x. Q x) ⇔ ∃x. P ∧ Q x
⊦ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃x. P ∨ Q x
⊦ ∀P Q. (∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q
⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q
⊦ ∀t1 t2 t3. (t1 ∨ t2) ∨ t3 ⇔ t1 ∨ t2 ∨ t3
⊦ ∀l h t. (h :: t) @ l = h :: t @ l
⊦ ∀f h t. map f (h :: t) = f h :: map f t
⊦ ∀p h t. all p (h :: t) ⇔ p h ∧ all p t
⊦ ∀p h t. exists p (h :: t) ⇔ p h ∨ exists p t
⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n
⊦ ∀x h t. member x (h :: t) ⇔ x = h ∨ member x t
⊦ ∀x y s. x ∈ insert y s ⇔ x = y ∨ x ∈ s
⊦ ∀P Q. (∃x. P x) ∨ (∃x. Q x) ⇔ ∃x. P x ∨ Q x
⊦ ∀P. P [] ∧ (∀a0 a1. P a1 ⇒ P (a0 :: a1)) ⇒ ∀x. P x
⊦ ∀h t n. n < length t ⇒ nth (suc n) (h :: t) = nth n t
⊦ ∀P h t. filter P (h :: t) = if P h then h :: filter P t else filter P t
⊦ ∀P c x y. P (if c then x else y) ⇔ (c ⇒ P x) ∧ (¬c ⇒ P y)