fp1/week7/camil/BewijsMeppenEnTippen.icl

   1 // Mart Lubbers, s4109503
   2 // Camil Staps, s4498062
   3
   4 Zij gegeven:
   5
   6 :: BTree a              = Tip a | Bin (BTree a) (BTree a)
   7
   8 map                     :: (a -> b) [a] -> [b]
   9 map f []                = []                                    (1.)
  10 map f [x:xs]            = [f x : map f xs]                      (2.)
  11
  12 mapbtree                :: (a -> b) (BTree a) -> BTree b
  13 mapbtree f (Tip a)      = Tip (f a)                             (3.)
  14 mapbtree f (Bin t1 t2)  = Bin (mapbtree f t1) (mapbtree f t2)   (4.)
  15
  16 foldbtree               :: (a a -> a) (BTree a) -> a
  17 foldbtree f (Tip x)     = x                                     (5.)
  18 foldbtree f (Bin t1 t2) = f (foldbtree f t1) (foldbtree f t2)   (6.)
  19
  20 tips                    :: (BTree a) -> [a]
  21 tips t                  = foldbtree (++) (mapbtree unit t)      (7.)
  22
  23 unit                    :: a -> [a]
  24 unit x                  = [x]                                   (8.)
  25
  26
  27 Te bewijzen:
  28     voor alle functies f, voor alle eindige bomen t:
  29
  30         map f (tips t) = tips (mapbtree f t)
  31
  32 Bewijs:
  33     Met inductie over t.
  34
  35     Inductiebasis: stel t = Tip a.
  36     Dan hebben we:
  37
  38         map f (tips t)                                          // definitie tips (7)
  39         = map f (foldbtree (++) (mapbtree unit t))              // aanname t = Tip a
  40         = map f (foldbtree (++) (mapbtree unit (Tip a)))        // definitie mapbtree (3)
  41         = map f (foldbtree (++) (Tip unit a))                   // definitie foldbtree (5)
  42         = map f (unit a)                                        // definitie unit (8)
  43         = map f [a]                                             // herschrijven lijst
  44         = map f [a:[]]                                          // definitie map (2)
  45         = [f a : map f []]                                      // definitie map (1)
  46         = [f a : []]                                            // herschrijven lijst
  47         = [f a]                                                 // definitie unit (8)
  48         = unit (f a)                                            // definitie foldbtree (5)
  49         = foldbtree (++) (Tip (unit (f a)))                     // definitie mapbtree (3)
  50         = foldbtree (++) (mapbtree unit (Tip (f a)))            // definitie tips (7)
  51         = tips (Tip (f a))                                      // definitie mapbtree (3)
  52         = tips (mapbtree f (Tip a))                             // aanname t = Tip a
  53         = tips (mapbtree f t)
  54
  55     Dus de stelling geldt voor t = Tip a.
  56
  57     Inductiestap: laten we aannemen dat
  58         map f (tips t) = tips (mapbtree f t)
  59     voor alle f en zekere t=t1,t=t2 (inductiehypothese).
  60     Dan hebben we:
  61
  62         map f (tips (Bin t1 t2))                                                                    // definitie tips (7)
  63         = map f (foldbtree (++) (mapbtree unit (Bin t1 t2)))                                        // definitie mapbtree (4)
  64         = map f (foldbtree (++) (Bin (mapbtree unit t1) (mapbtree unit t2)))                        // definitie foldbtree (6)
  65         = map f ((++) (foldbtree (++) (mapbtree unit t1)) (foldbtree (++) (mapbtree unit t2)))      // definitie tips (7)
  66         = map f ((++) (tips t1) (tips t2))                                                          // 9.4.1
  67         = (map f (tips t1)) ++ (map f (tips t2))                                                    // inductiehypothese
  68         = (tips (mapbtree f t1)) ++ (tips (mapbtree f t2))                                          // definitie tips (7)
  69         = (foldbtree (++) (mapbtree unit (f t1))) ++ (foldbtree (++) (mapbtree unit (f t2)))        // herschrijven infixnotatie
  70         = (++) (foldbtree (++) (mapbtree unit (f t1))) (foldbtree (++) (mapbtree unit (f t2)))      // definitie foldbtree (6)
  71         = foldbtree (++) (Bin (mapbtree unit (f t1)) (mapbtree unit (f t2)))                        // definitie mapbtree (4)
  72         = foldbtree (++) (mapbtree unit (Bin (mapbtree f t1) (mapbtree f t2)))                      // definitie tips (7)
  73         = tips (Bin (mapbtree f t1) (mapbtree f t2))                                                // definitie mapbtree (4)
  74         = tips (mapbtree f (Bin t1 t2))
  75
  76     Conclusie:
  77     We hebben laten zien dat de stelling geldt voor elke f met t = Tip a. Vervolgens hebben we laten zien dat als de stelling geldt voor elke f met t=t1 of t=t2, de stelling óók geldt voor elke f met t = Bin t1 t2.
  78     Met het principe van inductie volgt nu
  79
  80         map f (tips t) = tips (mapbtree f t)
  81
  82     voor alle functies f en alle eindige bomen t.