--- a/List.thy Fri Jan 14 12:35:27 1994 +0100
+++ b/List.thy Mon Jan 24 15:59:02 1994 +0100
@@ -37,22 +37,29 @@
null :: "'a list => bool"
hd :: "'a list => 'a"
tl :: "'a list => 'a list"
+ mem :: "['a, 'a list] => bool" (infixl 55)
list_all :: "('a => bool) => ('a list => bool)"
map :: "('a=>'b) => ('a list => 'b list)"
"@" :: "['a list, 'a list] => 'a list" (infixr 65)
list_case :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
+ filter :: "['a => bool, 'a list] => 'a list"
(* List Enumeration *)
"[]" :: "'a list" ("[]")
"@List" :: "args => 'a list" ("[(_)]")
+ (* Special syntax for list_all and filter *)
+ "@Alls" :: "[id, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
+ "@filter" :: "[id, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
translations
"[x, xs]" == "Cons(x, [xs])"
"[x]" == "Cons(x, [])"
"[]" == "Nil"
+ "[x:xs . P]" == "filter(%x.P,xs)"
+ "Alls x:xs.P" == "list_all(%x.P,xs)"
rules
@@ -97,9 +104,13 @@
null_def "null(xs) == list_rec(xs, True, %x xs r.False)"
hd_def "hd(xs) == list_rec(xs, @x.True, %x xs r.x)"
tl_def "tl(xs) == list_rec(xs, @xs.True, %x xs r.xs)"
+ mem_def "x mem xs == \
+\ list_rec(xs, False, %y ys r. if(y=x, True, r))"
list_all_def "list_all(P, xs) == list_rec(xs, True, %x l r. P(x) & r)"
- map_def "map(f, xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r))"
+ map_def "map(f, xs) == list_rec(xs, [], %x l r. Cons(f(x),r))"
append_def "xs@ys == list_rec(xs, ys, %x l r. Cons(x,r))"
+ filter_def "filter(P,xs) == \
+\ list_rec(xs, [], %x xs r. if(P(x), Cons(x,r), r))"
list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
end