Package list-append-thm: list-append-thm

Information

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

Files

Theorems

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

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

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

l1 l2.
    Data.List.toSet (Data.List.@ l1 l2) =
    Set.∪ (Data.List.toSet l1) (Data.List.toSet l2)

l m n. Data.List.@ l (Data.List.@ m n) = Data.List.@ (Data.List.@ l m) n

l m.
    Data.List.head (Data.List.@ l m) =
    if l = Data.List.[] then Data.List.head m else Data.List.head l

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

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

l. Data.List.null l l = Data.List.[]

() = λp q. p q p

h t. ¬(Data.List.:: h t = Data.List.[])

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

(¬T F) (¬F T)

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

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

(s. Set.∪ Set.∅ s = s) s. Set.∪ s Set.∅ = s

P. (x y. P x y) y x. P x y

s t u. Set.∪ (Set.∪ s t) u = Set.∪ s (Set.∪ t u)

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)

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

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

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

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

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

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