Package list-replicate-thm: list-replicate-thm

Information

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

Files

Theorems

n x. Data.List.length (Data.List.replicate n x) = n

n x i.
    Number.Natural.< i n Data.List.nth i (Data.List.replicate n x) = x

n x.
    Data.List.toSet (Data.List.replicate n x) =
    if n = 0 then Set.∅ else Set.insert x Set.∅

Input Type Operators

Input Constants

Assumptions

T

F p. p

(~) = λp. p F

t. (x. t) t

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

x. x = x T

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

() = λp q. p q p

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

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

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

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

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

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

() = λp q. r. (p r) (q r) r

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)

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

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

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

(x. Data.List.replicate 0 x = Data.List.[])
  x n.
    Data.List.replicate (Number.Natural.suc n) x =
    Data.List.:: x (Data.List.replicate n x)

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

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

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