Package list-map-thm: Properties of the list map function
Information
| name | list-map-thm |
| version | 1.41 |
| description | Properties of the list map function |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2012-06-08 |
| requires | bool function list-append list-def list-dest list-length list-map-def list-set list-thm set |
| show | Data.Bool Data.List Function Number.Natural Set |
Files
- Package tarball list-map-thm-1.41.tgz
- Theory file list-map-thm.thy (included in the package tarball)
Theorems
⊦ map id = id
⊦ ∀l. map (λx. x) l = l
⊦ ∀f l. null (map f l) ⇔ null l
⊦ ∀f l. length (map f l) = length l
⊦ ∀f l. toSet (map f l) = image f (toSet l)
⊦ ∀f l. map f l = [] ⇔ l = []
⊦ ∀f g l. map (f ∘ g) l = map f (map g l)
⊦ ∀p f l. all p (map f l) ⇔ all (p ∘ f) l
⊦ ∀p f l. exists p (map f l) ⇔ exists (p ∘ f) l
⊦ ∀f l1 l2. map f (l1 @ l2) = map f l1 @ map f l2
⊦ ∀f. (∀ys. ∃xs. map f xs = ys) ⇔ ∀y. ∃x. f x = y
⊦ ∀f l y. member y (map f l) ⇔ ∃x. y = f x ∧ member x l
⊦ ∀f g l. all (λx. f x = g x) l ⇒ map f l = map g l
⊦ ∀f. (∀l1 l2. map f l1 = map f l2 ⇒ l1 = l2) ⇔ ∀x y. f x = f y ⇒ x = y
Input Type Operators
- →
- bool
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
- Set
- set
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- exists
- length
- map
- member
- null
- toSet
- Bool
- Function
- id
- ∘
- Number
- Natural
- suc
- zero
- Natural
- Set
- ∅
- image
- insert
- ∈
Assumptions
⊦ ⊤
⊦ id = λx. x
⊦ ¬⊥ ⇔ ⊤
⊦ length [] = 0
⊦ toSet [] = ∅
⊦ ∀t. t ⇒ t
⊦ ⊥ ⇔ ∀p. p
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊥ ∧ t ⇔ ⊥
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. ⊥ ⇒ t ⇔ ⊤
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀t. ⊤ ∨ t ⇔ ⊤
⊦ ∀l. [] @ l = l
⊦ ∀f. map f [] = []
⊦ ∀f. image f ∅ = ∅
⊦ (∘) = λf g x. f (g x)
⊦ ∀t. t ⇒ ⊥ ⇔ ¬t
⊦ ∀l. null l ⇔ l = []
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀l. length l = 0 ⇔ null l
⊦ ∀h t. ¬(h :: t = [])
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀h t. length (h :: t) = suc (length t)
⊦ ∀l x. member x l ⇔ x ∈ toSet l
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀h t. toSet (h :: t) = insert h (toSet t)
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀l. l = [] ∨ ∃h t. l = h :: t
⊦ ∀f g. (∀x. f x = g x) ⇔ f = g
⊦ ∀p l. ¬all (λx. ¬p x) l ⇔ exists p l
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀l h t. (h :: t) @ l = h :: t @ l
⊦ ∀p l. all p l ⇔ ∀x. x ∈ toSet l ⇒ p x
⊦ ∀f h t. map f (h :: t) = f h :: map f t
⊦ ∀f x s. image f (insert x s) = insert (f x) (image f s)
⊦ ∀p h t. all p (h :: t) ⇔ p h ∧ all p t
⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l
⊦ ∀y s f. y ∈ image f s ⇔ ∃x. y = f x ∧ x ∈ s
⊦ ∀h1 h2 t1 t2. h1 :: t1 = h2 :: t2 ⇔ h1 = h2 ∧ t1 = t2
⊦ ∀p f s. (∀y. y ∈ image f s ⇒ p y) ⇔ ∀x. x ∈ s ⇒ p (f x)