Package list-zipwith-thm: list-zipwith-thm

Information

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

Files

Theorems

f. Data.List.zipWith f Data.List.[] Data.List.[] = Data.List.[]

f l1 l2 n.
    Data.List.length l1 = n Data.List.length l2 = n
    Data.List.length (Data.List.zipWith f l1 l2) = n

f h1 h2 t1 t2.
    Data.List.length t1 = Data.List.length t2
    Data.List.zipWith f (Data.List.:: h1 t1) (Data.List.:: h2 t2) =
    Data.List.:: (f h1 h2) (Data.List.zipWith f t1 t2)

Input Type Operators

Input Constants

Assumptions

T

F p. p

(~) = λp. p F

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

x. x = x T

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

() = λp q. p q p

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

m n. Number.Natural.suc m = Number.Natural.suc n 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

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)

(f. Data.List.zipWith f Data.List.[] Data.List.[] = Data.List.[])
  f h1 h2 t1 t2.
    Data.List.length t1 = Data.List.length t2
    Data.List.zipWith f (Data.List.:: h1 t1) (Data.List.:: h2 t2) =
    Data.List.:: (f h1 h2) (Data.List.zipWith f t1 t2)