src/HOL/List.thy
changeset 5518 654ead0ba4f7
parent 5443 e2459d18ff47
child 6141 a6922171b396
     1.1 --- a/src/HOL/List.thy	Mon Sep 21 22:58:43 1998 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Sep 21 23:03:11 1998 +0200
     1.3 @@ -17,7 +17,9 @@
     1.4    foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
     1.5    hd, last    :: 'a list => 'a
     1.6    set         :: 'a list => 'a set
     1.7 +  list_all    :: ('a => bool) => ('a list => bool)
     1.8    map         :: ('a=>'b) => ('a list => 'b list)
     1.9 +  mem         :: ['a, 'a list] => bool                    (infixl 55)
    1.10    nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
    1.11    list_update :: 'a list => nat => 'a => 'a list
    1.12    take, drop  :: [nat, 'a list] => 'a list
    1.13 @@ -35,9 +37,6 @@
    1.14    lupdbinds  lupdbind
    1.15  
    1.16  syntax
    1.17 -  mem         :: ['a, 'a list] => bool                    (infixl 55)
    1.18 -  list_all    :: ('a => bool) => ('a list => bool)
    1.19 -
    1.20    (* list Enumeration *)
    1.21    "@list"     :: args => 'a list                          ("[(_)]")
    1.22  
    1.23 @@ -53,9 +52,6 @@
    1.24    upto        :: nat => nat => nat list                   ("(1[_../_])")
    1.25  
    1.26  translations
    1.27 -  "x mem xs"      == "x:set xs"
    1.28 -  "list_all P xs" == "Ball (set xs) P"
    1.29 -  
    1.30    "[x, xs]"     == "x#[xs]"
    1.31    "[x]"         == "x#[]"
    1.32    "[x:xs . P]"  == "filter (%x. P) xs"
    1.33 @@ -97,9 +93,15 @@
    1.34    "butlast [] = []"
    1.35    "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
    1.36  primrec
    1.37 +  "x mem [] = False"
    1.38 +  "x mem (y#ys) = (if y=x then True else x mem ys)"
    1.39 +primrec
    1.40    "set [] = {}"
    1.41    "set (x#xs) = insert x (set xs)"
    1.42  primrec
    1.43 +  list_all_Nil  "list_all P [] = True"
    1.44 +  list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
    1.45 +primrec
    1.46    "map f [] = []"
    1.47    "map f (x#xs) = f(x)#map f xs"
    1.48  primrec