9.5 camil

diff --git a/week7/camil/BewijsMeppenEnTippen.icl b/week7/camil/BewijsMeppenEnTippen.icl
new file mode 100644 (file)
index 0000000..1e8d91c
--- /dev/null
+++ b/week7/camil/BewijsMeppenEnTippen.icl
@@ -0,0 +1,79 @@
+Zij gegeven:\r
+\r
+:: BTree a              = Tip a | Bin (BTree a) (BTree a)\r
+\r
+map                     :: (a -> b) [a] -> [b]\r
+map f []                = []                                    (1.)\r
+map f [x:xs]            = [f x : map f xs]                      (2.)\r
+\r
+mapbtree                :: (a -> b) (BTree a) -> BTree b\r
+mapbtree f (Tip a)      = Tip (f a)                             (3.)\r
+mapbtree f (Bin t1 t2)  = Bin (mapbtree f t1) (mapbtree f t2)   (4.)\r
+\r
+foldbtree               :: (a a -> a) (BTree a) -> a\r
+foldbtree f (Tip x)     = x                                     (5.)\r
+foldbtree f (Bin t1 t2) = f (foldbtree f t1) (foldbtree f t2)   (6.)\r
+\r
+tips                    :: (BTree a) -> [a]\r
+tips t                  = foldbtree (++) (mapbtree unit t)      (7.)\r
+\r
+unit                    :: a -> [a]\r
+unit x                  = [x]                                   (8.)\r
+\r
+\r
+Te bewijzen:\r
+    voor alle functies f, voor alle eindige bomen t:\r
+    \r
+        map f (tips t) = tips (mapbtree f t)\r
+\r
+Bewijs:\r
+    Met inductie over t.\r
+\r
+    Inductiebasis: stel t = Tip a.\r
+    Dan hebben we:\r
+\r
+        map f (tips t)                                          // definitie tips (7)\r
+        = map f (foldbtree (++) (mapbtree unit t))              // aanname t = Tip a\r
+        = map f (foldbtree (++) (mapbtree unit (Tip a)))        // definitie mapbtree (3)\r
+        = map f (foldbtree (++) (Tip unit a))                   // definitie foldbtree (5)\r
+        = map f (unit a)                                        // definitie unit (8)\r
+        = map f [a]                                             // herschrijven lijst\r
+        = map f [a:[]]                                          // definitie map (2)\r
+        = [f a : map f []]                                      // definitie map (1)\r
+        = [f a : []]                                            // herschrijven lijst\r
+        = [f a]                                                 // definitie unit (8)\r
+        = unit (f a)                                            // definitie foldbtree (5)\r
+        = foldbtree (++) (Tip (unit (f a)))                     // definitie mapbtree (3)\r
+        = foldbtree (++) (mapbtree unit (Tip (f a)))            // definitie tips (7)\r
+        = tips (Tip (f a))                                      // definitie mapbtree (3)\r
+        = tips (mapbtree f (Tip a))                             // aanname t = Tip a\r
+        = tips (mapbtree f t)\r
+\r
+    Dus de stelling geldt voor t = Tip a.\r
+\r
+    Inductiestap: laten we aannemen dat \r
+        map f (tips t) = tips (mapbtree f t)\r
+    voor alle f en zekere t=t1,t=t2 (inductiehypothese). \r
+    Dan hebben we:\r
+\r
+        map f (tips (Bin t1 t2))                                                                    // definitie tips (7)\r
+        = map f (foldbtree (++) (mapbtree unit (Bin t1 t2)))                                        // definitie mapbtree (4)\r
+        = map f (foldbtree (++) (Bin (mapbtree unit t1) (mapbtree unit t2)))                        // definitie foldbtree (6)\r
+        = map f ((++) (foldbtree (++) (mapbtree unit t1)) (foldbtree (++) (mapbtree unit t2)))      // definitie tips (7)\r
+        = map f ((++) (tips t1) (tips t2))                                                          // 9.4.1\r
+        = (map f (tips t1)) ++ (map f (tips t2))                                                    // inductiehypothese\r
+        = (tips (mapbtree f t1)) ++ (tips (mapbtree f t2))                                          // definitie tips (7)\r
+        = (foldbtree (++) (mapbtree unit (f t1))) ++ (foldbtree (++) (mapbtree unit (f t2)))        // herschrijven infixnotatie\r
+        = (++) (foldbtree (++) (mapbtree unit (f t1))) (foldbtree (++) (mapbtree unit (f t2)))      // definitie foldbtree (6)\r
+        = foldbtree (++) (Bin (mapbtree unit (f t1)) (mapbtree unit (f t2)))                        // definitie mapbtree (4)\r
+        = foldbtree (++) (mapbtree unit (Bin (mapbtree f t1) (mapbtree f t2)))                      // definitie tips (7)\r
+        = tips (Bin (mapbtree f t1) (mapbtree f t2))                                                // definitie mapbtree (4)\r
+        = tips (mapbtree f (Bin t1 t2))\r
+\r
+    Conclusie:\r
+    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. \r
+    Met het principe van inductie volgt nu\r
+\r
+        map f (tips t) = tips (mapbtree f t)\r
+\r
+    voor alle functies f en alle eindige bomen t.
\ No newline at end of file