The Theory list

The Theory list

Parents

ℕ

Children

char

Constants

IsListRep	(ℕ → 'a) × ℕ → BOOL
[]	'a LIST
Cons	'a → 'a LIST → 'a LIST
Length	'a LIST → ℕ
Hd	'a LIST → 'a
Tl	'a LIST → 'a LIST
Append	'a LIST → 'a LIST → 'a LIST
Rev	'a LIST → 'a LIST
Split	('a × 'b) LIST → 'a LIST × 'b LIST
Combine	'a LIST → 'b LIST → ('a × 'b) LIST
Map	('a → 'b) → 'a LIST → 'b LIST
Fold	('a → 'b → 'b) → 'a LIST → 'b → 'b

Aliases

@	Append : 'a LIST → 'a LIST → 'a LIST

Types

'1 LIST

Fixity

Right Infix 300:

@

Definitions

IsListRep is_list_rep_def	⊢ ∃ nil cons • IsListRep nil ∧ (∀ x• IsListRep x ⇒ (∀ h• ¬ cons h x = nil)) ∧ (∀ x y • IsListRep x ∧ IsListRep y ⇒ (∀ a b • cons a x = cons b y ⇔ a = b ∧ x = y)) ∧ (∀ x • IsListRep x ⇒ (∀ h• IsListRep (cons h x))) ∧ (∀ p • p nil ∧ (∀ m• p m ⇒ (∀ h• p (cons h m))) ⇒ (∀ n• IsListRep n ⇒ p n))
LIST list_def	⊢ ∃ f• TypeDefn IsListRep f
Nil Cons nil_cons_def	⊢ (∀ x list• ¬ Cons x list = []) ∧ (∀ x1 x2 list1 list2 • Cons x1 list1 = Cons x2 list2 ⇔ x1 = x2 ∧ list1 = list2) ∧ (∀ p • p [] ∧ (∀ list• p list ⇒ (∀ x• p (Cons x list))) ⇒ (∀ list• p list))
Length length_def	⊢ # [] = 0 ∧ (∀ h list• # (Cons h list) = # list + 1)
Hd hd_def	⊢ ∀ h list• Head (Cons h list) = h
Tl tl_def	⊢ ∀ h list• Tail (Cons h list) = list
Append append_def	⊢ (∀ list• [] @ list = list) ∧ (∀ h list list' • Cons h list @ list' = Cons h (list @ list'))
Rev rev_def	⊢ Rev [] = [] ∧ (∀ h list• Rev (Cons h list) = Rev list @ [h])
Split split_def	⊢ Split [] = ([], []) ∧ (∀ list h1 h2 • Split (Cons (h1, h2) list) = (Cons h1 (Fst (Split list)), Cons h2 (Snd (Split list))))
Combine combine_def	⊢ Combine [] [] = [] ∧ (∀ h1 h2 list1 list2 • Combine (Cons h1 list1) (Cons h2 list2) = Cons (h1, h2) (Combine list1 list2))
Map map_def	⊢ (∀ g• Map g [] = []) ∧ (∀ h g list • Map g (Cons h list) = Cons (g h) (Map g list))
Fold fold_def	⊢ (∀ g x• Fold g [] x = x) ∧ (∀ h g x list • Fold g (Cons h list) x = g h (Fold g list x))

Theorems

list_induction_thm	⊢ ∀ p • p [] ∧ (∀ list• p list ⇒ (∀ x• p (Cons x list))) ⇒ (∀ list• p list)
list_prim_rec_thm	⊢ ∀ n c • ∃₁ f • f [] = n ∧ (∀ list a • f (Cons a list) = c a (f list) list)
list_clauses	⊢ ∀ x1 x2 list1 list2 • ¬ Cons x1 list1 = [] ∧ ¬ [] = Cons x1 list1 ∧ (Cons x1 list1 = Cons x2 list2 ⇔ x1 = x2 ∧ list1 = list2) ∧ Head (Cons x1 list1) = x1 ∧ Tail (Cons x1 list1) = list1
list_cases_thm	⊢ ∀ list1 • list1 = [] ∨ (∃ x list2• list1 = Cons x list2)

privacy policy

Created:

V