The Theory list

Parents

Children

char

Constants

IsListRep	( 'a) BOOL
Cons	'a 'a LIST '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)

V