Package list-take-drop-def: list-take-drop-def

Information

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

Files

Defined Constants

Theorems

(l. Data.List.drop 0 l = l)
  n h t.
    Number.Natural.≤ n (Data.List.length t)
    Data.List.drop (Number.Natural.suc n) (Data.List.:: h t) =
    Data.List.drop n t

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

Input Type Operators

Input Constants

Assumptions

T

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

t. (x. t) t

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

x. x = x T

() = λp q. p q p

h t. Data.List.head (Data.List.:: h t) = h

h t. Data.List.tail (Data.List.:: h t) = t

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

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

e f. fn. fn 0 = e n. fn (Number.Natural.suc n) = f (fn n) n

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)