Package list-nub: The list nub function

Information

name	list-nub
version	1.50
description	The list nub function
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool list-def list-length list-reverse list-set natural set
show	Data.Bool Data.List Number.Natural Set

Files

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

Defined Constants

Data
- List
  - nub
  - nubReverse

Theorems

⊦ nubReverse [] = []

⊦ ∀l. nub (nub l) = nub l

⊦ ∀l. nubReverse (nubReverse l) = nubReverse l

⊦ ∀l. toSet (nub l) = toSet l

⊦ ∀l. toSet (nubReverse l) = toSet l

⊦ ∀l. length (nub l) ≤ length l

⊦ ∀l. length (nubReverse l) ≤ length l

⊦ ∀l. nub l = reverse (nubReverse (reverse l))

⊦ ∀l x. member x (nub l) ⇔ member x l

⊦ ∀l x. member x (nubReverse l) ⇔ member x l

⊦ ∀h t.
nubReverse (h :: t) =
if member h t then nubReverse t else h :: nubReverse t

External Type Operators

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

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - length
  - member
  - reverse
  - toSet
Number
- Natural
  - ≤
  - suc
  - zero
Set
- ∈

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ length [] = 0

⊦ ∀n. n ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ ∀x. ¬member x []

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

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

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

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. (t ⇔ ⊤) ⇔ t

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀l. reverse (reverse l) = l

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

⊦ ∀l. length (reverse l) = length l

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

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

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

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

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

⊦ ∀l x. member x l ⇔ x ∈ toSet l

⊦ ∀l x. member x (reverse l) ⇔ member x l

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

⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n

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

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

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

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

⊦ ∀x h t. member x (h :: t) ⇔ x = h ∨ member x t

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

⊦ ∀b f. ∃fn. fn [] = b ∧ ∀h t. fn (h :: t) = f h t (fn t)