Package list-fold-thm: Properties of the list fold operations
Information
| name | list-fold-thm |
| version | 1.11 |
| description | Properties of the list fold operations |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-06-08 |
| requires | bool function list-append list-def list-fold-def list-length list-reverse natural |
| show | Data.Bool Data.List Function Number.Natural |
Files
- Package tarball list-fold-thm-1.11.tgz
- Theory file list-fold-thm.thy (included in the package tarball)
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)
Input Type Operators
- →
- bool
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ⊤
- List
- ::
- @
- []
- foldl
- foldr
- length
- reverse
- Bool
- Function
- C
- Number
- Natural
- +
- suc
- zero
- Natural
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)