Package list-set-def: list-set-def

Information

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

Files

Defined Constants

Theorems

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)

Input Type Operators

Input Constants

Assumptions

T

F p. p

(~) = λp. p F

() = λP. P ((select) P)

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

x. x = x T

() = λp q. p q p

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

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

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)

NIL' CONS'.
    fn.
      fn Data.List.[] = NIL'
      a0 a1. fn (Data.List.:: 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)

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)