Put w6 in format

3 files changed, 80 insertions, 47 deletions

diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1
deleted file mode 100644
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
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
index 0000000..44cf7c1
--- /dev/null
+++ b/week6/camil/BewijsMapFlatten.icl
@@ -0,0 +1,80 @@
+Zij gegeven:

+

+(++) :: [a] [a] -> [a]

+(++) []     xs = xs                (1)

+(++) [y:ys] xs = [y : ys ++ xs]    (2)

+

+map :: (a -> b) [a] -> [b]

+map f []       = []                (3)

+map f [x:xs]   = [f x : map f xs]  (4)

+

+flatten :: [[a]] -> [a]

+flatten []     = []                (5)

+flatten [x:xs] = x ++ (flatten xs) (6)

+

+1. 

+Te bewijzen: 

+	voor iedere functie f, eindige lijst as en bs:

+		

+		map f (as ++ bs) = (map f as) ++ (map f bs)

+

+Bewijs:

+Met inductie over as.

+

+Inductiebasis: 

+Stel as = []. Dan hebben we:

+

+    map f (as ++ bs)                        // aanname as = []

+    = map f ([] ++ bs)                      // definitie van ++, regel 1

+    = map f bs                              // definitie van ++, regel 1

+    = [] ++ (map f bs)                      // definitie van map, regel 3

+    = (map f []) ++ (map f bs)              // aanname as = []

+    = (map f as) ++ (map f bs).

+

+Inductiestap:

+Stel map f (as ++ bs) = (map f as) ++ (map f bs) voor zekere as en elke bs (inductiehypothese). Dan hebben we:

+

+    map f ([a:as] ++ bs)                    // definitie van ++, regel 2

+    = map f [a:as ++ bs]                    // definitie van map, regel 4

+    = [f a : map f (as ++ bs)]              // inductiehypothese: map f (as ++ bs) = (map f as) ++ (map f bs)

+    = [f a : (map f as) ++ (map f bs)]      // lijst herschrijven

+    = [f a : map f as] ++ (map f bs)        // definitie van map, regel 4

+    = (map f [a:as]) ++ (map f bs).

+

+Uit het principe van volledige inductie volgt nu dat voor iedere functie f, eindige lijst as en bs:

+

+    map f (as ++ bs) = (map f as) ++ (map f bs)     (9.4.1)

+

+2. 

+Te bewijzen:

+	voor iedere functie f, voor iedere eindige lijst xs:

+	

+		flatten (map (map f) xs) = map f (flatten xs)

+

+Bewijs:

+Met inductie over xs.

+

+Inductiebasis:

+Stel xs = []. Dan hebben we:

+

+    flatten (map (map f) xs)                    // aanname xs = []

+    = flatten (map (map f) [])                  // definitie van map, regel 3

+    = flatten []                                // definitie van flatten, regel 5

+    = []                                        // definitie van map, regel 3

+    = map f []                                  // definitie van flatten, regel 5

+    = map f (flatten [])                        // aanname xs = []

+    = map f (flatten xs).

+

+Inductiestap:

+Stel flatten (map (map f) xs) = map f (flatten xs) voor een zekere eindige lijst xs (inductiehypothese). Dan hebben we:

+

+    flatten (map (map f) [x:xs])                // definitie van map, regel 4

+    = flatten [map f x : map (map f) xs]        // definitie van flatten, regel 6

+    = (map f x) ++ flatten (map (map f) xs)     // inductiehypothese: flatten (map (map f) xs) = map f (flatten xs)

+    = (map f x) ++ (map f (flatten xs))         // 9.4.1

+    = map f (x ++ (flatten xs))                 // definitie van flatten, regel 6

+    = map f (flatten [x:xs]).

+

+Uit het principe van volledige inductie volgt nu dat voor iedere functie f en eindige lijst xs geldt:

+

+    flatten (map (map f) xs) = map f (flatten xs)
\ No newline at end of file