src/HOL/List.thy

     Copyright   1994 TU Muenchen
 
 Definition of type 'a list as a datatype. This allows primrec to work.
 
 TODO: delete list_all from this theory and from ex/Sorting, etc.
-      use setOfList instead
+      use set_of_list instead
 *)
 
 List = Arith +
 
 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
 
 consts
 
-  "@"       :: ['a list, 'a list] => 'a list            (infixr 65)
-  drop      :: [nat, 'a list] => 'a list
-  filter    :: ['a => bool, 'a list] => 'a list
-  flat      :: 'a list list => 'a list
-  foldl     :: [['b,'a] => 'b, 'b, 'a list] => 'b
-  hd        :: 'a list => 'a
-  length    :: 'a list => nat
-  setOfList :: ('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       :: [nat, 'a list] => 'a
-  take      :: [nat, 'a list] => 'a list
-  tl,ttl    :: 'a list => 'a list
-  rev       :: 'a list => 'a list
+  "@"         :: ['a list, 'a list] => 'a list            (infixr 65)
+  drop        :: [nat, 'a list] => 'a list
+  filter      :: ['a => bool, 'a list] => 'a list
+  flat        :: 'a list list => 'a list
+  foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
+  hd          :: 'a list => 'a
+  length      :: 'a list => nat
+  set_of_list :: ('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         :: [nat, 'a list] => 'a
+  take        :: [nat, 'a list] => 'a list
+  tl,ttl      :: 'a list => 'a list
+  rev         :: 'a list => 'a list
 
 syntax
   (* list Enumeration *)
-  "@list"   :: args => 'a list                        ("[(_)]")
+  "@list"     :: args => 'a list                        ("[(_)]")
 
   (* Special syntax for list_all and filter *)
-  "@Alls"       :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
-  "@filter"     :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
+  "@Alls"     :: [idt, 'a list, bool] => bool         ("(2Alls _:_./ _)" 10)
+  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
 
 translations
   "[x, xs]"     == "x#[xs]"
   "[x]"         == "x#[]"
 

   "ttl([]) = []"
   "ttl(x#xs) = xs"
 primrec "op mem" list
   "x mem [] = False"
   "x mem (y#ys) = (if y=x then True else x mem ys)"
-primrec setOfList list
-  "setOfList [] = {}"
-  "setOfList (x#xs) = insert x (setOfList xs)"
+primrec set_of_list list
+  "set_of_list [] = {}"
+  "set_of_list (x#xs) = insert x (set_of_list xs)"
 primrec list_all list
   list_all_Nil  "list_all P [] = True"
   list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
 primrec map list
   "map f [] = []"