Package list-concat-thm: list-concat-thm

Information

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

Files

Theorem

l. Data.List.null (Data.List.concat l) Data.List.all Data.List.null l

Input Type Operators

Input Constants

Assumptions

T

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

x. x = x T

() = λp q. p q p

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

l m.
    Data.List.null (Data.List.@ l m) Data.List.null l Data.List.null m

(Data.List.null Data.List.[] T)
  h t. Data.List.null (Data.List.:: h t) F

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

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

(P. Data.List.all P Data.List.[] T)
  P h t. Data.List.all P (Data.List.:: h t) P h Data.List.all P t

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