Put w6 in format

diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1
deleted file mode 100644 (file)
index d9b2608..0000000
--- a/week6/camil/9.4.1
+++ /dev/null
@@ -1,23 +0,0 @@
-9.4.1 - proof by induction over as
-
-Induction base:
-    Suppose as = []. Then we have:
-
-    map f (as ++ bs)                        // assumption as = []
-    = map f ([] ++ bs)                      // definition of ++, rule 1
-    = map f bs                              // definition of ++, rule 1
-    = [] ++ (map f bs)                      // definition of map, rule 3
-    = (map f []) ++ (map f bs)              // assumption as = []
-    = (map f as) ++ (map f bs).
-
-Induction step:
-    Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs (induction hypothesis). Then we have:
-    
-    map f ([a:as] ++ bs)                    // definition of ++, rule 2
-    = map f [a:as ++ bs]                    // definition of map, rule 4
-    = [f a : map f (as ++ bs)]              // induction hypothesis: assumption map f (as ++ bs) = (map f as) ++ (map f bs)
-    = [f a : (map f as) ++ (map f bs)]      // rewriting list
-    = [f a : map f as] ++ (map f bs)        // definition of map, rule 4
-    = (map f [a:as]) ++ (map f bs).
-
-By the principle of induction we have now proven that map f (as ++ bs) = (map f as) ++ (map f bs) for any finite lists as, bs.
\ No newline at end of file

diff --git a/week6/camil/9.4.2 b/week6/camil/9.4.2
deleted file mode 100644 (file)
index bc95352..0000000
--- a/week6/camil/9.4.2
+++ /dev/null
@@ -1,24 +0,0 @@
-9.4.2 - proof by induction over xs
-
-Induction base:
-    Suppose xs = []. Then we have:
-    
-    flatten (map (map f) xs)                    // assumption xs = []
-    = flatten (map (map f) [])                  // definition of map, rule 3
-    = flatten []                                // definition of flatten, rule 5
-    = []                                        // definition of map, rule 3
-    = map f []                                  // definition of flatten, rule 5
-    = map f (flatten [])                        // assumption xs = []
-    = map f (flatten xs).
-
-Induction step:
-    Suppose flatten (map (map f) xs) = map f (flatten xs) for certain xs of finite length (induction hypothesis). Then we have:
-    
-    flatten (map (map f) [x:xs])                // definition of map, rule 4
-    = flatten [map f x : map (map f) xs]        // definition of flatten, rule 6
-    = (map f x) ++ flatten (map (map f) xs)     // induction hypothesis: assumption flatten (map (map f) xs) = map f (flatten xs)
-    = (map f x) ++ (map f (flatten xs))         // by 9.4.1
-    = map f (x ++ (flatten xs))                 // definition of flatten, rule 6
-    = map f (flatten [x:xs]).
-
-By the principle of induction we have now proven that flatten (map (map f) xs) = map f (flatten xs) for any list of finite length xs.
\ No newline at end of file

diff --git a/week6/camil/BewijsMapFlatten.icl b/week6/camil/BewijsMapFlatten.icl
new file mode 100644 (file)
index 0000000..44cf7c1
--- /dev/null
+++ b/week6/camil/BewijsMapFlatten.icl
@@ -0,0 +1,80 @@
+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 over as.\r
+\r
+Inductiebasis: \r
+Stel as = []. Dan hebben we:\r
+\r
+    map f (as ++ bs)                        // aanname as = []\r
+    = map f ([] ++ bs)                      // definitie van ++, regel 1\r
+    = map f bs                              // definitie van ++, regel 1\r
+    = [] ++ (map f bs)                      // definitie van map, regel 3\r
+    = (map f []) ++ (map f bs)              // aanname as = []\r
+    = (map f as) ++ (map f bs).\r
+\r
+Inductiestap:\r
+Stel map f (as ++ bs) = (map f as) ++ (map f bs) voor zekere as en elke bs (inductiehypothese). Dan hebben we:\r
+\r
+    map f ([a:as] ++ bs)                    // definitie van ++, regel 2\r
+    = map f [a:as ++ bs]                    // definitie van map, regel 4\r
+    = [f a : map f (as ++ bs)]              // inductiehypothese: map f (as ++ bs) = (map f as) ++ (map f bs)\r
+    = [f a : (map f as) ++ (map f bs)]      // lijst herschrijven\r
+    = [f a : map f as] ++ (map f bs)        // definitie van map, regel 4\r
+    = (map f [a:as]) ++ (map f bs).\r
+\r
+Uit het principe van volledige inductie volgt nu dat voor iedere functie f, eindige lijst as en bs:\r
+\r
+    map f (as ++ bs) = (map f as) ++ (map f bs)     (9.4.1)\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 inductie over xs.\r
+\r
+Inductiebasis:\r
+Stel xs = []. Dan hebben we:\r
+\r
+    flatten (map (map f) xs)                    // aanname xs = []\r
+    = flatten (map (map f) [])                  // definitie van map, regel 3\r
+    = flatten []                                // definitie van flatten, regel 5\r
+    = []                                        // definitie van map, regel 3\r
+    = map f []                                  // definitie van flatten, regel 5\r
+    = map f (flatten [])                        // aanname xs = []\r
+    = map f (flatten xs).\r
+\r
+Inductiestap:\r
+Stel flatten (map (map f) xs) = map f (flatten xs) voor een zekere eindige lijst xs (inductiehypothese). Dan hebben we:\r
+\r
+    flatten (map (map f) [x:xs])                // definitie van map, regel 4\r
+    = flatten [map f x : map (map f) xs]        // definitie van flatten, regel 6\r
+    = (map f x) ++ flatten (map (map f) xs)     // inductiehypothese: flatten (map (map f) xs) = map f (flatten xs)\r
+    = (map f x) ++ (map f (flatten xs))         // 9.4.1\r
+    = map f (x ++ (flatten xs))                 // definitie van flatten, regel 6\r
+    = map f (flatten [x:xs]).\r
+\r
+Uit het principe van volledige inductie volgt nu dat voor iedere functie f en eindige lijst xs geldt:\r
+\r
+    flatten (map (map f) xs) = map f (flatten xs)
\ No newline at end of file