Package list-take-drop-thm: list-take-drop-thm

Information

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

Files

Theorems

l. Data.List.drop 0 l = l

l. Data.List.take 0 l = Data.List.[]

l. Data.List.drop (Data.List.length l) l = Data.List.[]

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

n l.
    Number.Natural.≤ n (Data.List.length l)
    Data.List.length (Data.List.take n l) = n

n l.
    Number.Natural.≤ n (Data.List.length l)
    Data.List.length (Data.List.drop n l) =
    Number.Natural.- (Data.List.length l) n

n l.
    Number.Natural.≤ n (Data.List.length l)
    Data.List.@ (Data.List.take n l) (Data.List.drop n 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

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)

n l i.
    Number.Natural.≤ n (Data.List.length l) Number.Natural.< i n
    Data.List.nth i (Data.List.take n l) = Data.List.nth i l

n l i.
    Number.Natural.≤ n (Data.List.length l)
    Number.Natural.< i (Number.Natural.- (Data.List.length l) n)
    Data.List.nth i (Data.List.drop n l) =
    Data.List.nth (Number.Natural.+ n i) l

Input Type Operators

Input Constants

Assumptions

T

n. Number.Natural.≤ n n

F p. p

(~) = λp. p F

t. (x. t) t

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

x. x = x T

n. ¬(Number.Natural.suc n = 0)

n. Number.Natural.- n n = 0

l. Data.List.@ l Data.List.[] = l

() = λp q. p q p

l. Data.List.length l = 0 l = Data.List.[]

h t. Data.List.nth 0 (Data.List.:: h t) = h

m n. Number.Natural.- (Number.Natural.+ m n) m = n

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

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

m n. Number.Natural.suc m = Number.Natural.suc n m = n

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

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

l m.
    Data.List.length (Data.List.@ l m) =
    Number.Natural.+ (Data.List.length l) (Data.List.length m)

m n. Number.Natural.≤ m n d. n = Number.Natural.+ m d

m n p.
    Number.Natural.< (Number.Natural.+ m n) (Number.Natural.+ m p)
    Number.Natural.< n p

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

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

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

P. P 0 (n. P n P (Number.Natural.suc n)) n. P n

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

h t n.
    Number.Natural.< n (Data.List.length t)
    Data.List.nth (Number.Natural.suc n) (Data.List.:: h t) =
    Data.List.nth n t

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

h1 h2 t1 t2. Data.List.:: h1 t1 = Data.List.:: h2 t2 h1 = h2 t1 = t2

(m. Number.Natural.< m 0 F)
  m n.
    Number.Natural.< m (Number.Natural.suc n)
    m = n Number.Natural.< m n

(l. Data.List.@ Data.List.[] l = l)
  l h t.
    Data.List.@ (Data.List.:: h t) l = Data.List.:: h (Data.List.@ t l)

(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

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

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)