Package list-append: The list append function

Information

name	list-append
version	1.30
description	The list append function
author	Joe Hurd <joe@gilith.com>
license	MIT
requires	bool natural set list-def list-thm list-dest list-length list-set
show	Data.Bool Data.List Number.Natural Set

Files

Package tarball list-append-1.30.tgz
Theory file list-append.thy (included in the package tarball)

Defined Constant

Data
- List
  - @

Theorems

⊦ ∀l. [] @ l = l

⊦ ∀l. l @ [] = l

⊦ ∀l m. null (l @ m) ⇔ null l ∧ null m

⊦ ∀l m. length (l @ m) = length l + length m

⊦ ∀l1 l2. toSet (l1 @ l2) = toSet l1 ∪ toSet l2

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

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

⊦ ∀l m. head (l @ m) = if l = [] then head m else head l

⊦ ∀l m. l @ m = [] ⇔ l = [] ∧ m = []

Input Type Operators

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

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - head
  - length
  - null
  - toSet
Number
- Natural
  - +
  - suc
  - zero
Set
- ∅
- insert
- ∪

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ length [] = 0

⊦ toSet [] = ∅

⊦ ⊥ ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ ⊥

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

⊦ ∀t. (∀x. t) ⇔ t

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ t ⇔ t

⊦ ∀n. 0 + n = n

⊦ ∀s. ∅ ∪ s = s

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀l. null l ⇔ l = []

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2

⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1

⊦ ∀h t. ¬(h :: t = [])

⊦ ∀h t. head (h :: t) = h

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

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

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

⊦ ∀h t. toSet (h :: t) = insert h (toSet t)

⊦ ∀x s. insert x ∅ ∪ s = insert x s

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

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

⊦ ∀s t u. s ∪ t ∪ u = s ∪ (t ∪ u)

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