Package list-fold: List fold operations

Information

name	list-fold
version	1.5
description	List fold operations
author	Joe Hurd <joe@gilith.com>
license	MIT
requires	bool function natural list-def list-length list-append list-reverse
show	Data.Bool Data.List Function Number.Natural

Files

Package tarball list-fold-1.5.tgz
Theory file list-fold.thy (included in the package tarball)

Defined Constants

Data
- List
  - foldl
  - foldr

Theorems

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

⊦ ∀f b. foldr f b [] = b

⊦ ∀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 l = foldr (C f) b (reverse l)

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

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

⊦ ∀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)

Input Type Operators

→
bool
Data
- List
  - list
Number
- Natural
  - natural

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ⊤
- List
  - ::
  - @
  - []
  - length
  - reverse
Function
- C
Number
- Natural
  - +
  - suc
  - zero

Assumptions

⊦ ⊤

⊦ length [] = 0

⊦ reverse [] = []

⊦ (∃) = λp. p ((select) p)

⊦ ∀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 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 ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

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

⊦ ∀f x y. C f x y = f y x

⊦ ∀l m. reverse (l @ m) = reverse m @ reverse l

⊦ ∀x l. reverse (x :: l) = reverse l @ x :: []

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

⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)

⊦ ∀P. P [] ∧ (∀a0 a1. P a1 ⇒ P (a0 :: a1)) ⇒ ∀x. P x

⊦ ∀NIL' CONS'.
∃fn. fn [] = NIL' ∧ ∀a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)