From 6f604b19d3f5966e5c1d7c4fdf3703bd6ff0861c Mon Sep 17 00:00:00 2001
From: Mart Lubbers
Date: Thu, 16 Apr 2015 21:22:20 +0200
Subject: update to fp2 yay, public and licence

---
 fp1/week6/camil/BewijsMapFlatten.icl | 83 ++++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)
 create mode 100644 fp1/week6/camil/BewijsMapFlatten.icl

(limited to 'fp1/week6/camil/BewijsMapFlatten.icl')

diff --git a/fp1/week6/camil/BewijsMapFlatten.icl b/fp1/week6/camil/BewijsMapFlatten.icl
new file mode 100644
index 0000000..7f2474e
--- /dev/null
+++ b/fp1/week6/camil/BewijsMapFlatten.icl
@@ -0,0 +1,83 @@
+// Mart Lubbers, s4109503
+// Camil Staps, s4498062
+
+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)
-- 
cgit v1.2.3