fp1/week7/mart/BewijsMeppenEnTippen.icl

   1 Zij gegeven:
   2
   3 :: BTree a              = Tip a | Bin (BTree a) (BTree a)
   4
   5 map                     :: (a -> b) [a] -> [b]
   6 map f []                = []                                    (1.)
   7 map f [x:xs]            = [f x : map f xs]                      (2.)
   8
   9 mapbtree                :: (a -> b) (BTree a) -> BTree b
  10 mapbtree f (Tip a)      = Tip (f a)                             (3.)
  11 mapbtree f (Bin t1 t2)  = Bin (mapbtree f t1) (mapbtree f t2)   (4.)
  12
  13 foldbtree               :: (a a -> a) (BTree a) -> a
  14 foldbtree f (Tip x)     = x                                     (5.)
  15 foldbtree f (Bin t1 t2) = f (foldbtree f t1) (foldbtree f t2)   (6.)
  16
  17 tips                    :: (BTree a) -> [a]
  18 tips t                  = foldbtree (++) (mapbtree unit t)      (7.)
  19
  20 unit                    :: a -> [a]
  21 unit x                  = [x]                                   (8.)
  22
  23
  24 Te bewijzen:
  25     voor alle functies f, voor alle eindige bomen t:
  26
  27         map f (tips t) = tips (mapbtree f t)
  28
  29 Bewijs: