Package list-nth: The list nth function

Information

name	list-nth
version	1.55
description	The list nth function
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool list-append list-def list-dest list-last list-length list-map list-set list-thm natural set
show	Data.Bool Data.List Number.Natural Set

Files

Package tarball list-nth-1.55.tgz
Theory source file list-nth.thy (included in the package tarball)

Defined Constant

Data
- List
  - nth

Theorems

⊦ ∀h t. nth (h :: t) 0 = h

⊦ ∀l. ¬null l ⇒ nth l (length l - 1) = last l

⊦ ∀p l. all p l ⇔ ∀i. i < length l ⇒ p (nth l i)

⊦ ∀p l. any p l ⇔ ∃i. i < length l ∧ p (nth l i)

⊦ ∀l x. member x l ⇔ ∃i. i < length l ∧ x = nth l i

⊦ ∀l. toSet l = image (nth l) { i. i | i < length l }

⊦ ∀h t n. n < length t ⇒ nth (h :: t) (suc n) = nth t n

⊦ ∀f l i. i < length l ⇒ nth (map f l) i = f (nth l i)

⊦ ∀l₁ l₂.
length l₁ = length l₂ ∧ (∀i. i < length l₁ ⇒ nth l₁ i = nth l₂ i) ⇒
l₁ = l₂

⊦ ∀l₁ l₂ k.
    k < length l₁ + length l₂ ⇒
    nth (l₁ @ l₂) k =
    if k < length l₁ then nth l₁ k else nth l₂ (k - length l₁)

External Type Operators

→
bool
Data
- List
  - list
Number
- Natural
  - natural
Set
- set

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - all
  - any
  - head
  - last
  - length
  - map
  - member
  - null
  - tail
  - toSet
Number
- Natural
  - +
  - -
  - <
  - ≤
  - bit1
  - suc
  - zero
Set
- ∅
- fromPredicate
- image
- insert
- ∈

Assumptions

⊦ ⊤

⊦ null []

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ length [] = 0

⊦ toSet [] = ∅

⊦ ∀t. t ⇒ t

⊦ ⊥ ⇔ ∀p. p

⊦ fromPredicate (λx. ⊥) = ∅

⊦ ∀m. ¬(m < 0)

⊦ ∀n. ¬(n < n)

⊦ ∀n. 0 < suc n

⊦ ∀n. n < suc n

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) p)

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀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

⊦ ∀n. ¬(suc n = 0)

⊦ ∀m. m - 0 = m

⊦ ∀l. [] @ l = l

⊦ ∀f. image f ∅ = ∅

⊦ ∀l. null l ⇔ l = []

⊦ ∀h t. ¬null (h :: t)

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀n. suc n - 1 = n

⊦ ∀l. length l = 0 ⇔ null l

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀h t. head (h :: t) = h

⊦ ∀h t. tail (h :: t) = t

⊦ ∀l. length l = 0 ⇔ l = []

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀t₁ t₂. t₁ ∧ t₂ ⇔ t₂ ∧ t₁

⊦ ∀f l. length (map f l) = length l

⊦ ∀p x. x ∈ fromPredicate p ⇔ p x

⊦ ∀h t. length (h :: t) = suc (length t)

⊦ ∀m n. ¬(m < n) ⇔ n ≤ m

⊦ ∀m. m = 0 ∨ ∃n. m = suc n

⊦ ∀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)

⊦ ∀m n. suc m + n = suc (m + n)

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀l₁ l₂. length (l₁ @ l₂) = length l₁ + length l₂

⊦ ∀h t. last (h :: t) = if null t then h else last t

⊦ ∀p. (∀x y. p x y) ⇔ ∀y x. p x y

⊦ ∀l h t. (h :: t) @ l = h :: t @ l

⊦ ∀s t. (∀x. x ∈ s ⇔ x ∈ t) ⇔ s = t

⊦ ∀p l. all p l ⇔ ∀x. x ∈ toSet l ⇒ p x

⊦ ∀p l. any p l ⇔ ∃x. x ∈ toSet l ∧ p x

⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)

⊦ ∀m n. n ≤ m ⇒ suc m - suc n = m - n

⊦ ∀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. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀p x. x ∈ { y. y | p y } ⇔ p x

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

⊦ ∀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

⊦ ∀h₁ h₂ t₁ t₂. h₁ :: t₁ = h₂ :: t₂ ⇔ h₁ = h₂ ∧ t₁ = t₂

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀p f s. (∀y. y ∈ image f s ⇒ p y) ⇔ ∀x. x ∈ s ⇒ p (f x)

⊦ ∀p f s. (∃y. y ∈ image f s ∧ p y) ⇔ ∃x. x ∈ s ∧ p (f x)

⊦ ∀n. { m. m | m < suc n } = insert 0 { m. suc m | m < n }