Package list-length-thm: Properties of the list length function

Information

name	list-length-thm
version	1.42
description	Properties of the list length function
author	Joe Leslie-Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2015-02-01
checksum	6b359afbb6802bb767175a11385027ce26f42dc5
requires	bool list-def list-dest list-length-def list-thm natural
show	Data.Bool Data.List Number.Natural

Files

Package tarball list-length-thm-1.42.tgz
Theory source file list-length-thm.thy (included in the package tarball)

Theorems

⊦ ∀l. length l = 0 ⇔ null l

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

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

⊦ length [] = 0 ∧ ∀h t. length (h :: t) = length t + 1

⊦ ∀l n. length l = suc n ⇔ ∃h t. l = h :: t ∧ length t = n

External Type Operators

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

External Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - ⊥
  - ⊤
- List
  - ::
  - []
  - length
  - null
  - tail
Number
- Natural
  - +
  - -
  - bit1
  - suc
  - zero

Assumptions

⊦ ⊤

⊦ null []

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ length [] = 0

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. 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

⊦ ∀n. ¬(suc n = 0)

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀l. null l ⇔ l = []

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

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

⊦ ∀m. suc m = m + 1

⊦ ∀n. suc n - 1 = n

⊦ ∀h t. ¬(h :: t = [])

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

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

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

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

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l

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