summaryrefslogtreecommitdiff
path: root/files/practicum/BewijsMeppenEnTippen.icl
blob: 720ff4d87ddc8feb05ad095ef73b1f2d6d329236 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
Zij gegeven:

:: BTree a              = Tip a | Bin (BTree a) (BTree a)

map                     :: (a -> b) [a] -> [b]
map f []                = []                                    (1.)
map f [x:xs]            = [f x : map f xs]                      (2.)

mapbtree                :: (a -> b) (BTree a) -> BTree b
mapbtree f (Tip a)      = Tip (f a)                             (3.)
mapbtree f (Bin t1 t2)  = Bin (mapbtree f t1) (mapbtree f t2)   (4.)

foldbtree               :: (a a -> a) (BTree a) -> a
foldbtree f (Tip x)     = x                                     (5.)
foldbtree f (Bin t1 t2) = f (foldbtree f t1) (foldbtree f t2)   (6.)

tips                    :: (BTree a) -> [a]
tips t                  = foldbtree (++) (mapbtree unit t)      (7.)

unit                    :: a -> [a]
unit x                  = [x]                                   (8.)


Te bewijzen:
    voor alle functies f, voor alle eindige bomen t:
    
        map f (tips t) = tips (mapbtree f t)

Bewijs: