Package list-take-drop-thm: Properties of the list take and drop functions
Information
| name | list-take-drop-thm |
| version | 1.49 |
| description | Properties of the list take and drop functions |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-08-06 |
| requires | bool list-append list-def list-length list-nth list-take-drop-def list-thm natural |
| show | Data.Bool Data.List Number.Natural |
Files
- Package tarball list-take-drop-thm-1.49.tgz
- Theory file list-take-drop-thm.thy (included in the package tarball)
Theorems
⊦ ∀l. drop (length l) l = []
⊦ ∀l. take (length l) l = l
⊦ ∀n l. n ≤ length l ⇒ length (take n l) = n
⊦ ∀n l. n ≤ length l ⇒ length (drop n l) = length l - n
⊦ ∀n l. n ≤ length l ⇒ n + length (drop n l) = length l
⊦ ∀n l. n ≤ length l ⇒ take n l @ drop n l = l
⊦ ∀n l i. n + i < length l ⇒ nth (drop n l) i = nth l (n + i)
⊦ ∀n l i. n ≤ length l ∧ i < n ⇒ nth (take n l) i = nth l i
⊦ ∀n l i.
n ≤ length l ∧ i < length l ⇒
nth l i = if i < n then nth (take n l) i else nth (drop n l) (i - n)
Input Type Operators
- →
- bool
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- drop
- length
- nth
- take
- Bool
- Number
- Natural
- +
- -
- <
- ≤
- bit1
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ length [] = 0
⊦ ∀n. n ≤ n
⊦ ⊥ ⇔ ∀p. p
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. ⊥ ⇒ t ⇔ ⊤
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ ∀n. ¬(suc n = 0)
⊦ ∀n. n - n = 0
⊦ ∀l. [] @ l = l
⊦ ∀l. l @ [] = l
⊦ ∀l. drop 0 l = l
⊦ ∀l. take 0 l = []
⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t
⊦ ∀m n. m ≤ m + n
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀m. suc m = m + 1
⊦ ∀m. m ≤ 0 ⇔ m = 0
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀l. length l = 0 ⇔ l = []
⊦ ∀x y. x = y ⇒ y = x
⊦ ∀m n. m + n - m = n
⊦ ∀h t. length (h :: t) = suc (length t)
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. suc m ≤ n ⇔ m < n
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n
⊦ ∀l1 l2. length (l1 @ l2) = length l1 + length l2
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀l h t. (h :: t) @ l = h :: t @ l
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l
⊦ ∀n h t. n ≤ length t ⇒ drop (suc n) (h :: t) = drop n t
⊦ ∀h1 h2 t1 t2. h1 :: t1 = h2 :: t2 ⇔ h1 = h2 ∧ t1 = t2
⊦ ∀n h t. n ≤ length t ⇒ take (suc n) (h :: t) = h :: take n t
⊦ ∀l1 l2 k.
k < length l1 + length l2 ⇒
nth (l1 @ l2) k =
if k < length l1 then nth l1 k else nth l2 (k - length l1)