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

Infix 300:@
Definitions
IsListRep
is_list_rep_def
mk_var("nil", (( 'a) ))
mk_var("cons", ('a
(( 'a) )
( 'a)
))
IsListRep mk_var("nil", (( 'a) ))
( x
IsListRep x
( h
mk_var("cons", ('a
(( 'a) )
( 'a)
))
h
x
= mk_var("nil", ( 'a) )))
( x y
IsListRep x IsListRep y
( a b
mk_var("cons", ('a
(( 'a) )
( 'a)
))
a
x
= mk_var("cons", ('a
(( 'a) )
( 'a)
))
b
y
a = b x = y))
( x
IsListRep x
( h
IsListRep
(mk_var("cons", ('a
(( 'a) )
( 'a)
))
h
x)))
( p
p mk_var("nil", (( 'a) ))
( m
p m
( h
p
(mk_var("cons", ('a
(( 'a) )
( 'a)
))
h
m)))
( n IsListRep n p n))
LIST
list_def
f TypeDefn IsListRep f
Nil
Cons
nil_cons_def
( x mk_var("list", 'a LIST)
Cons x mk_var("list", 'a LIST) = [])
( x1 x2 list1 list2
Cons x1 list1 = Cons x2 list2
x1 = x2 list1 = list2)
( p
p []
( mk_var("list", 'a LIST)
p mk_var("list", 'a LIST)
( x
p
(Cons
x
mk_var("list", 'a LIST))))
( mk_var("list", 'a LIST)
p mk_var("list", 'a LIST)))
Length
length_def
Length [] = 0
( h mk_var("list", 'a LIST)
Length (Cons h mk_var("list", 'a LIST))
= Length mk_var("list", 'a LIST) + 1)
Hd
hd_def
h mk_var("list", 'a LIST)
Hd (Cons h mk_var("list", 'a LIST)) = h
Tl
tl_def
h mk_var("list", 'a LIST)
Tl (Cons h mk_var("list", 'a LIST))
= mk_var("list", 'a LIST)
Append
append_def
( mk_var("list", 'a LIST)
[] @ mk_var("list", 'a LIST)
= mk_var("list", 'a LIST))
( h mk_var("list", 'a LIST) list'
Cons h mk_var("list", 'a LIST) @ list'
= Cons h (mk_var("list", 'a LIST) @ list'))
Rev
rev_def
Rev [] = []
( h mk_var("list", 'a LIST)
Rev (Cons h mk_var("list", 'a LIST))
= Rev mk_var("list", 'a LIST) @ [h])
Split
split_def
Split [] = ([], [])
( mk_var("list", ('a 'b) LIST) h1 h2
Split
(Cons
(h1, h2)
mk_var("list", ('a 'b) LIST))
= (Cons
h1
(Fst
(Split
mk_var("list", ('a 'b)
LIST))),
Cons
h2
(Snd
(Split
mk_var("list", ('a 'b)
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 mk_var("list", 'a LIST)
Map g (Cons h mk_var("list", 'a LIST))
= Cons
(g h)
(Map g mk_var("list", 'a LIST)))
Fold
fold_def
( g x Fold g [] x = x)
( h g x mk_var("list", 'a LIST)
Fold g (Cons h mk_var("list", 'a LIST)) x
= g h (Fold g mk_var("list", 'a LIST) x))
Theorems
list_induction_thm
p
p []
( mk_var("list", 'a LIST)
p mk_var("list", 'a LIST)
( x
p (Cons x mk_var("list", 'a LIST))))
( mk_var("list", 'a LIST)
p mk_var("list", 'a LIST))
list_prim_rec_thm
n c
1 f
f [] = n
( mk_var("list", 'a LIST) a
f (Cons a mk_var("list", 'a LIST))
= c
a
(f mk_var("list", 'a LIST))
mk_var("list", 'a LIST))
list_clauses
x1 x2 list1 list2
Cons x1 list1 = []
[] = Cons x1 list1
(Cons x1 list1 = Cons x2 list2
x1 = x2 list1 = list2)
Hd (Cons x1 list1) = x1
Tl (Cons x1 list1) = list1
list_cases_thm
list1
list1 = [] ( x list2 list1 = Cons x list2)

up quick index © RBJ