Package list-last: The last list function

Information

name	list-last
version	1.31
description	The last list function
author	Joe Hurd <joe@gilith.com>
license	MIT
requires	bool set list-def list-thm list-set list-append
show	Data.Bool Data.List Set

Files

Package tarball list-last-1.31.tgz
Theory file list-last.thy (included in the package tarball)

Defined Constant

Data
- List
  - last

Theorems

⊦ ∀h. last (h :: []) = h

⊦ ∀l. ¬(l = []) ⇒ last l ∈ toSet l

⊦ ∀h t. last (h :: t) = if t = [] then h else last t

⊦ ∀h k t. last (h :: k :: t) = last (k :: t)

⊦ ∀p q. last (p @ q) = if q = [] then last p else last q

Input Type Operators

→
bool
Data
- List
  - list
Set
- set

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - toSet
Set
- insert
- ∈

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀t. t ⇒ t

⊦ ⊥ ⇔ ∀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. t ∧ ⊤ ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀l. [] @ l = l

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

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

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

⊦ ∀h t. ¬(h :: 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)

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

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

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

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

⊦ ∀x y s. x ∈ insert y s ⇔ x = y ∨ x ∈ s

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

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

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