Package list-nub: The list nub function

Information

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

Files

Package tarball list-nub-1.32.tgz
Theory 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

Input Type Operators

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

Input Constants

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

Assumptions

⊦ T

⊦ ¬F ⇔ T

⊦ length [] = 0

⊦ ∀n. n ≤ n

⊦ F ⇔ ∀p. p

⊦ ∀x. ¬member x []

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ F

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

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

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

⊦ ∀t. (t ⇔ T) ⇔ t

⊦ ∀t. F ∨ t ⇔ t

⊦ ∀t. T ∨ t ⇔ T

⊦ ∀t. t ∨ T ⇔ T

⊦ ∀l. reverse (reverse l) = l

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

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

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

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀t1 t2. (if F then t1 else t2) = t2

⊦ ∀t1 t2. (if T then t1 else t2) = t1

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

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

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

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

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

⊦ ∀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 [] ∧ (∀a0 a1. P a1 ⇒ P (a0 :: a1)) ⇒ ∀x. P x

⊦ ∀NIL' CONS'.
∃fn. fn [] = NIL' ∧ ∀a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)