Package list-set-thm: list-set-thm

Information

namelist-set-thm
version1.9
descriptionlist-set-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-25
showData.Bool

Files

Theorems

l. Set.finite (Data.List.toSet l)

l. Number.Natural.≤ (Set.size (Data.List.toSet l)) (Data.List.length l)

l. Data.List.toSet l = Set.∅ l = Data.List.[]

s. Set.finite s Data.List.toSet (Data.List.fromSet s) = s

s. Set.finite s Data.List.length (Data.List.fromSet s) = Set.size s

Input Type Operators

Input Constants

Assumptions

T

Set.finite Set.∅

Set.size Set.∅ = 0

n. Number.Natural.≤ 0 n

n. Number.Natural.≤ n n

F p. p

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

(~) = λp. p F

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

x. x = x T

() = λp q. p q p

h t. ¬(Data.List.:: h t = Data.List.[])

x s. ¬(Set.insert x s = Set.∅)

(¬T F) (¬F T)

s x. Set.finite (Set.insert x s) Set.finite s

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

() = λP. q. (x. P x q) q

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

m n p.
    Number.Natural.≤ m n Number.Natural.≤ n p Number.Natural.≤ m p

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

s.
    Set.finite s
    Data.List.toSet (Data.List.fromSet s) = s
    Data.List.length (Data.List.fromSet s) = Set.size s

Data.List.toSet Data.List.[] = Set.∅
  h t.
    Data.List.toSet (Data.List.:: h t) = Set.insert h (Data.List.toSet t)

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

P c x y. P (if c then x else y) (c P x) (¬c P y)

Set.size Set.∅ = 0
  x s.
    Set.finite s
    Set.size (Set.insert x s) =
    if Set.∈ x s then Set.size s else Number.Natural.suc (Set.size s)

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

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

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