added foldr
authorpaulson
Fri Nov 05 12:47:15 1999 +0100 (1999-11-05)
changeset 8000acafa0f15131
parent 7999 7acf6eb8eec1
child 8001 14c8843cd35b
added foldr
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri Nov 05 12:45:37 1999 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Nov 05 12:47:15 1999 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    filter      :: ['a => bool, 'a list] => 'a list
     1.5    concat      :: 'a list list => 'a list
     1.6    foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
     1.7 +  foldr       :: [['a,'b] => 'b, 'a list, 'b] => 'b
     1.8    hd, last    :: 'a list => 'a
     1.9    set         :: 'a list => 'a set
    1.10    list_all    :: ('a => bool) => ('a list => bool)
    1.11 @@ -117,6 +118,9 @@
    1.12    foldl_Nil  "foldl f a [] = a"
    1.13    foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
    1.14  primrec
    1.15 +  "foldr f [] a = a"
    1.16 +  "foldr f (x#xs) a = f x (foldr f xs a)"
    1.17 +primrec
    1.18    "concat([]) = []"
    1.19    "concat(x#xs) = x @ concat(xs)"
    1.20  primrec