Package list-nub-thm: list-nub-thm

Information

namelist-nub-thm
version1.15
descriptionlist-nub-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-09-21
showData.Bool

Files

Theorems

l. Data.List.nub (Data.List.nub l) = Data.List.nub l

l.
    Data.List.nubReverse (Data.List.nubReverse l) = Data.List.nubReverse l

l. Data.List.toSet (Data.List.nub l) = Data.List.toSet l

l. Data.List.toSet (Data.List.nubReverse l) = Data.List.toSet l

l.
    Number.Natural.≤ (Data.List.length (Data.List.nub l))
      (Data.List.length l)

l.
    Number.Natural.≤ (Data.List.length (Data.List.nubReverse l))
      (Data.List.length l)

l x. Data.List.member x (Data.List.nub l) Data.List.member x l

l x. Data.List.member x (Data.List.nubReverse l) Data.List.member x l

Input Type Operators

Input Constants

Assumptions

T

n. Number.Natural.≤ n n

F p. p

t. t ¬t

(¬) = λp. p F

t. (x. t) t

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

x. x = x T

l. Data.List.reverse (Data.List.reverse l) = l

l. Data.List.length (Data.List.reverse l) = Data.List.length l

() = λp q. p q p

t. (t T) (t F)

l.
    Data.List.nub l =
    Data.List.reverse (Data.List.nubReverse (Data.List.reverse l))

(¬T F) (¬F T)

x l. Data.List.member x l Set.∈ x (Data.List.toSet l)

l x. Data.List.member x (Data.List.reverse l) Data.List.member x l

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

m n.
    Number.Natural.≤ (Number.Natural.suc m) (Number.Natural.suc n)
    Number.Natural.≤ m n

() = λp q. r. (p r) (q r) r

s t. s = t x. Set.∈ x s Set.∈ x t

t1 t2. (if T then t1 else t2) = t1 (if F then t1 else t2) = t2

Data.List.length Data.List.[] = 0
  h t.
    Data.List.length (Data.List.:: h t) =
    Number.Natural.suc (Data.List.length t)

P. P Data.List.[] (a0 a1. P a1 P (Data.List.:: a0 a1)) x. P x

Data.List.nubReverse Data.List.[] = Data.List.[]
  h t.
    Data.List.nubReverse (Data.List.:: h t) =
    if Data.List.member h t then Data.List.nubReverse t
    else Data.List.:: h (Data.List.nubReverse t)

(x. Data.List.member x Data.List.[] F)
  x h t.
    Data.List.member x (Data.List.:: h t) x = h Data.List.member x t

(m. Number.Natural.≤ m 0 m = 0)
  m n.
    Number.Natural.≤ m (Number.Natural.suc n)
    m = Number.Natural.suc n Number.Natural.≤ m n

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t T) (t T T) (F t t) (t F t) (t t t)