45 |
45 |
46 "[x:xs . P]" == "filter (%x.P) xs" |
46 "[x:xs . P]" == "filter (%x.P) xs" |
47 "Alls x:xs.P" == "list_all (%x.P) xs" |
47 "Alls x:xs.P" == "list_all (%x.P) xs" |
48 |
48 |
49 primrec hd list |
49 primrec hd list |
50 hd_Nil "hd([]) = (@x.False)" |
50 "hd([]) = (@x.False)" |
51 hd_Cons "hd(x#xs) = x" |
51 "hd(x#xs) = x" |
52 primrec tl list |
52 primrec tl list |
53 tl_Nil "tl([]) = (@x.False)" |
53 "tl([]) = (@x.False)" |
54 tl_Cons "tl(x#xs) = xs" |
54 "tl(x#xs) = xs" |
55 primrec ttl list |
55 primrec ttl list |
56 (* a "total" version of tl: *) |
56 (* a "total" version of tl: *) |
57 ttl_Nil "ttl([]) = []" |
57 "ttl([]) = []" |
58 ttl_Cons "ttl(x#xs) = xs" |
58 "ttl(x#xs) = xs" |
59 primrec "op mem" list |
59 primrec "op mem" list |
60 mem_Nil "x mem [] = False" |
60 "x mem [] = False" |
61 mem_Cons "x mem (y#ys) = (if y=x then True else x mem ys)" |
61 "x mem (y#ys) = (if y=x then True else x mem ys)" |
62 primrec setOfList list |
62 primrec setOfList list |
63 setOfList_Nil "setOfList [] = {}" |
63 "setOfList [] = {}" |
64 setOfList_Cons "setOfList (x#xs) = insert x (setOfList xs)" |
64 "setOfList (x#xs) = insert x (setOfList xs)" |
65 primrec list_all list |
65 primrec list_all list |
66 list_all_Nil "list_all P [] = True" |
66 list_all_Nil "list_all P [] = True" |
67 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)" |
67 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)" |
68 primrec map list |
68 primrec map list |
69 map_Nil "map f [] = []" |
69 "map f [] = []" |
70 map_Cons "map f (x#xs) = f(x)#map f xs" |
70 "map f (x#xs) = f(x)#map f xs" |
71 primrec "op @" list |
71 primrec "op @" list |
72 append_Nil "[] @ ys = ys" |
72 "[] @ ys = ys" |
73 append_Cons "(x#xs)@ys = x#(xs@ys)" |
73 "(x#xs)@ys = x#(xs@ys)" |
74 primrec rev list |
74 primrec rev list |
75 rev_Nil "rev([]) = []" |
75 "rev([]) = []" |
76 rev_Cons "rev(x#xs) = rev(xs) @ [x]" |
76 "rev(x#xs) = rev(xs) @ [x]" |
77 primrec filter list |
77 primrec filter list |
78 filter_Nil "filter P [] = []" |
78 "filter P [] = []" |
79 filter_Cons "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" |
79 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" |
80 primrec foldl list |
80 primrec foldl list |
81 foldl_Nil "foldl f a [] = a" |
81 "foldl f a [] = a" |
82 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs" |
82 "foldl f a (x#xs) = foldl f (f a x) xs" |
83 primrec length list |
83 primrec length list |
84 length_Nil "length([]) = 0" |
84 "length([]) = 0" |
85 length_Cons "length(x#xs) = Suc(length(xs))" |
85 "length(x#xs) = Suc(length(xs))" |
86 primrec flat list |
86 primrec flat list |
87 flat_Nil "flat([]) = []" |
87 "flat([]) = []" |
88 flat_Cons "flat(x#xs) = x @ flat(xs)" |
88 "flat(x#xs) = x @ flat(xs)" |
89 primrec drop list |
89 primrec drop list |
90 drop_Nil "drop n [] = []" |
90 drop_Nil "drop n [] = []" |
91 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
91 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
92 primrec take list |
92 primrec take list |
93 take_Nil "take n [] = []" |
93 take_Nil "take n [] = []" |
94 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
94 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
95 defs |
95 defs |
96 nth_def "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n" |
96 nth_def "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n" |
97 end |
97 end |
|
98 |