--- a/src/HOL/List.thy Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/List.thy Mon Sep 21 23:03:11 1998 +0200
@@ -17,7 +17,9 @@
foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
hd, last :: 'a list => 'a
set :: 'a list => 'a set
+ list_all :: ('a => bool) => ('a list => bool)
map :: ('a=>'b) => ('a list => 'b list)
+ mem :: ['a, 'a list] => bool (infixl 55)
nth :: ['a list, nat] => 'a (infixl "!" 100)
list_update :: 'a list => nat => 'a => 'a list
take, drop :: [nat, 'a list] => 'a list
@@ -35,9 +37,6 @@
lupdbinds lupdbind
syntax
- mem :: ['a, 'a list] => bool (infixl 55)
- list_all :: ('a => bool) => ('a list => bool)
-
(* list Enumeration *)
"@list" :: args => 'a list ("[(_)]")
@@ -53,9 +52,6 @@
upto :: nat => nat => nat list ("(1[_../_])")
translations
- "x mem xs" == "x:set xs"
- "list_all P xs" == "Ball (set xs) P"
-
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
"[x:xs . P]" == "filter (%x. P) xs"
@@ -97,9 +93,15 @@
"butlast [] = []"
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
primrec
+ "x mem [] = False"
+ "x mem (y#ys) = (if y=x then True else x mem ys)"
+primrec
"set [] = {}"
"set (x#xs) = insert x (set xs)"
primrec
+ list_all_Nil "list_all P [] = True"
+ list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
+primrec
"map f [] = []"
"map f (x#xs) = f(x)#map f xs"
primrec