30 tl, butlast :: 'a list => 'a list |
30 tl, butlast :: 'a list => 'a list |
31 rev :: 'a list => 'a list |
31 rev :: 'a list => 'a list |
32 zip :: "'a list => 'b list => ('a * 'b) list" |
32 zip :: "'a list => 'b list => ('a * 'b) list" |
33 upt :: nat => nat => nat list ("(1[_../_'(])") |
33 upt :: nat => nat => nat list ("(1[_../_'(])") |
34 remdups :: 'a list => 'a list |
34 remdups :: 'a list => 'a list |
35 nodups :: "'a list => bool" |
35 null, nodups :: "'a list => bool" |
36 replicate :: nat => 'a => 'a list |
36 replicate :: nat => 'a => 'a list |
37 |
37 |
38 nonterminals |
38 nonterminals |
39 lupdbinds lupdbind |
39 lupdbinds lupdbind |
40 |
40 |
83 translations "length" => "size:: _ list => nat" |
83 translations "length" => "size:: _ list => nat" |
84 |
84 |
85 primrec |
85 primrec |
86 "hd(x#xs) = x" |
86 "hd(x#xs) = x" |
87 primrec |
87 primrec |
88 "tl([]) = []" |
88 "tl([]) = []" |
89 "tl(x#xs) = xs" |
89 "tl(x#xs) = xs" |
90 primrec |
90 primrec |
|
91 "null([]) = True" |
|
92 "null(x#xs) = False" |
|
93 primrec |
91 "last(x#xs) = (if xs=[] then x else last xs)" |
94 "last(x#xs) = (if xs=[] then x else last xs)" |
92 primrec |
95 primrec |
93 "butlast [] = []" |
96 "butlast [] = []" |
94 "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" |
97 "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" |
95 primrec |
98 primrec |
96 "x mem [] = False" |
99 "x mem [] = False" |
97 "x mem (y#ys) = (if y=x then True else x mem ys)" |
100 "x mem (y#ys) = (if y=x then True else x mem ys)" |
98 primrec |
101 primrec |
99 "set [] = {}" |
102 "set [] = {}" |
100 "set (x#xs) = insert x (set xs)" |
103 "set (x#xs) = insert x (set xs)" |
101 primrec |
104 primrec |
102 list_all_Nil "list_all P [] = True" |
105 list_all_Nil "list_all P [] = True" |
103 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)" |
106 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)" |
104 primrec |
107 primrec |
105 "map f [] = []" |
108 "map f [] = []" |
106 "map f (x#xs) = f(x)#map f xs" |
109 "map f (x#xs) = f(x)#map f xs" |
107 primrec |
110 primrec |
108 append_Nil "[] @ys = ys" |
111 append_Nil "[] @ys = ys" |
109 append_Cons "(x#xs)@ys = x#(xs@ys)" |
112 append_Cons "(x#xs)@ys = x#(xs@ys)" |
110 primrec |
113 primrec |
111 "rev([]) = []" |
114 "rev([]) = []" |
112 "rev(x#xs) = rev(xs) @ [x]" |
115 "rev(x#xs) = rev(xs) @ [x]" |
113 primrec |
116 primrec |
114 "filter P [] = []" |
117 "filter P [] = []" |
115 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" |
118 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" |
116 primrec |
119 primrec |
117 foldl_Nil "foldl f a [] = a" |
120 foldl_Nil "foldl f a [] = a" |
118 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs" |
121 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs" |
119 primrec |
122 primrec |
120 "foldr f [] a = a" |
123 "foldr f [] a = a" |
121 "foldr f (x#xs) a = f x (foldr f xs a)" |
124 "foldr f (x#xs) a = f x (foldr f xs a)" |
122 primrec |
125 primrec |
123 "concat([]) = []" |
126 "concat([]) = []" |
124 "concat(x#xs) = x @ concat(xs)" |
127 "concat(x#xs) = x @ concat(xs)" |
125 primrec |
128 primrec |
126 drop_Nil "drop n [] = []" |
129 drop_Nil "drop n [] = []" |
127 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
130 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
128 (* Warning: simpset does not contain this definition but separate theorems |
131 (* Warning: simpset does not contain this definition but separate theorems |
139 primrec |
142 primrec |
140 " [][i:=v] = []" |
143 " [][i:=v] = []" |
141 "(x#xs)[i:=v] = (case i of 0 => v # xs |
144 "(x#xs)[i:=v] = (case i of 0 => v # xs |
142 | Suc j => x # xs[j:=v])" |
145 | Suc j => x # xs[j:=v])" |
143 primrec |
146 primrec |
144 "takeWhile P [] = []" |
147 "takeWhile P [] = []" |
145 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" |
148 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" |
146 primrec |
149 primrec |
147 "dropWhile P [] = []" |
150 "dropWhile P [] = []" |
148 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" |
151 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" |
149 primrec |
152 primrec |
150 "zip xs [] = []" |
153 "zip xs [] = []" |
151 "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)" |
154 "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)" |
152 (* Warning: simpset does not contain this definition but separate theorems |
155 (* Warning: simpset does not contain this definition but separate theorems |