Package list-fold-thm: Properties of the list fold operations

Information

namelist-fold-thm
version1.23
descriptionProperties of the list fold operations
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-12-02
requiresbool
function
list-append
list-def
list-fold-def
list-length
list-reverse
natural
showData.Bool
Data.List
Function
Number.Natural

Files

Theorems

l. foldr (::) [] l = l

f b. foldl f b [] = b

l. foldl (C (::)) [] l = reverse l

l1 l2. foldr (::) l2 l1 = l1 @ l2

l1 l2. foldl (C (::)) l2 l1 = reverse l1 @ l2

l k. foldl (λn x. suc n) k l = length l + k

l k. foldr (λx n. suc n) k l = length l + k

f b l. foldr f b (reverse l) = foldl (C f) b l

f b l. foldl f b (reverse l) = foldr (C f) b l

f b h t. foldl f b (h :: t) = foldl f (f b h) t

f b l1 l2. foldr f b (l1 @ l2) = foldr f (foldr f b l2) l1

f b l1 l2. foldl f b (l1 @ l2) = foldl f (foldl f b l1) l2

g f b l1 l2.
    (s. g b s = s) (x s1 s2. g (f x s1) s2 = f x (g s1 s2))
    foldr f b (l1 @ l2) = g (foldr f b l1) (foldr f b l2)

g f b l1 l2.
    (s. g s b = s) (s1 s2 x. g s1 (f s2 x) = f (g s1 s2) x)
    foldl f b (l1 @ l2) = g (foldl f b l1) (foldl f b l2)

External Type Operators

External Constants

Assumptions

length [] = 0

reverse [] = []

t. (x. t) t

() = λp. p = λx.

t. t t

n. 0 + n = n

l. reverse (reverse l) = l

l. [] @ l = l

l. l @ [] = l

f. C (C f) = f

C = λf x y. f y x

l. length (reverse l) = length l

() = λp q. p q p

f b. foldr f b [] = b

f y. (let x y in f x) = f y

h t. length (h :: t) = suc (length t)

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

m n. suc m + n = suc (m + n)

f x y. C f x y = f y x

l1 l2. reverse (l1 @ l2) = reverse l2 @ reverse l1

h t. reverse (h :: t) = reverse t @ h :: []

l h t. (h :: t) @ l = h :: t @ l

f b l. foldl f b l = foldr (C f) b (reverse l)

p. p [] (h t. p t p (h :: t)) l. p l

f b h t. foldr f b (h :: t) = f h (foldr f b t)