Package list-set: Viewing lists as finite sets

Information

namelist-set
version1.12
descriptionViewing lists as finite sets
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.List

Files

Defined Constants

Theorems

l. Set.finite (toSet l)

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

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

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

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

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

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

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 ((select) P)

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

x. x = x T

() = λp q. p q p

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

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

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

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

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

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

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)

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)

P.
    P Set.∅
    (x s. P s ¬Set.∈ x s Set.finite s P (Set.insert x s))
    s. Set.finite s P s

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)