week 6 done

diff --git a/week6/mart/BewijsMapFlatten.icl b/week6/mart/BewijsMapFlatten.icl
new file mode 100644 (file)
index 0000000..59fa5bc
--- /dev/null
+++ b/week6/mart/BewijsMapFlatten.icl
@@ -0,0 +1,97 @@
+Zij gegeven:\r
+\r
+(++) :: [a] [a] -> [a]\r
+(++) []     xs = xs                (1)\r
+(++) [y:ys] xs = [y : ys ++ xs]    (2)\r
+\r
+map :: (a -> b) [a] -> [b]\r
+map f []       = []                (3)\r
+map f [x:xs]   = [f x : map f xs]  (4)\r
+\r
+flatten :: [[a]] -> [a]\r
+flatten []     = []                (5)\r
+flatten [x:xs] = x ++ (flatten xs) (6)\r
+\r
+1. \r
+Te bewijzen: \r
+       voor iedere functie f, eindige lijst as en bs:\r
+               \r
+               map f (as ++ bs) = (map f as) ++ (map f bs)\r
+\r
+Bewijs:\r
+       met inductie naar de lengte van as.\r
+\r
+       Basis:\r
+       aanname: as = [].\r
+\r
+            map f ([] ++ bs) = (map f []) ++ (map f bs)                  basis\r
+                  ********\r
+         => map f (bs) = (map f []) ++ (map f bs)                        (1)\r
+                          ********\r
+         => map f (bs) = [] ++ (map f bs)                                (3)\r
+                         ****************\r
+         => map f bs = map f bs                                          (1)\r
+\r
+       Inductiestap:\r
+       aanname: stelling geldt voor zekere as, ofwel:\r
+               map f (as ++ bs) = (map f as) ++ (map f bs) (IH)\r
+\r
+       Te bewijzen: stelling geldt ook voor as, ofwel:\r
+               map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs)\r
+\r
+            map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs)          basis\r
+                ************\r
+         => map f [a:as ++ bs] = (map f [a:as]) ++ (map f bs)            (2)\r
+           ******************\r
+         => [f a : map f (as ++ bs)] = (map f [a:as]) ++ (map f bs)      (4)\r
+                                       ************\r
+         => [f a : map f (as ++ bs)] = [f a : map f as] ++ (map f bs)    (4)\r
+                                       ****************************\r
+         => [f a : map f (as ++ bs)] = [f a : (map f as) ++ (map f bs)]  (4)\r
+                  ****************           ************************\r
+         => map f (as ++ bs) = (map f as) ++ (map f bs)                  (IH)\r
+\r
+       Dus: basis + inductiestap => stelling bewezen.\r
+\r
+2. \r
+Te bewijzen:\r
+       voor iedere functie f, voor iedere eindige lijst xs:\r
+       \r
+               flatten (map (map f) xs) = map f (flatten xs)\r
+\r
+Bewijs:\r
+       met inductio van de lengte van xs\r
+       \r
+       Basis:\r
+       aanname: xs = [].\r
+\r
+           flatten (map (map f) []) = map f (flatten [])                                basis\r
+                    **************\r
+         = flatten [] = map f (flatten [])                                              (3)\r
+                               **********\r
+         = flatten [] = map f []                                                        (5)\r
+           **********\r
+         = [] = map f []                                                                (5)\r
+                *****\r
+         = [] = []                                                                      (3)\r
+\r
+       Inductiestap:\r
+       aanname: stelling geldt voor zekere xs, ofwel:\r
+               flatten (map (map f) xs) = map f (flatten xs)\r
+\r
+       Te bewijzen: stelling geldt ook voor xs, ofwel:\r
+               flatten (map (map f) [x:xs]) = map f (flatten [x:xs])\r
+\r
+            flatten (map (map f) [x:xs]) = map f (flatten [x:xs])                       basis\r
+                     ******************\r
+         => flatten [map f x: map (map f) xs] = map f (flatten [x:xs])                  (4)\r
+            *********************************\r
+         => (map f x) ++ (flatten (map (map f) xs)) = map f (flatten [x:xs])            (6)\r
+                                                           **************\r
+         => (map f x) ++ (flatten (map (map f) xs)) = map f (x ++ (flatten xs))         (6)\r
+                                                      *************************\r
+         => (map f x) ++ (flatten (map (map f) xs)) = (map f x) ++ (map f (flatten xs)) (9.4.1)\r
+                          ************************                  ****************\r
+         => flatten (map (map f) xs) = map f (flatten xs)                               (IH)\r
+\r
+       Dus: basis + inductiestap => stelling  bewezen.\r