changeset 22:498aea38199b

week 9 tutorial
author Markus Kaiser <markus.kaiser@in.tum.de>
date Wed, 19 Dec 2012 23:20:55 +0100
parents 3fea6fff7265
children f9386825bf71
files exercises/src/Exercise_9.hs
diffstat 1 files changed, 33 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/exercises/src/Exercise_9.hs	Wed Dec 12 20:32:09 2012 +0100
+++ b/exercises/src/Exercise_9.hs	Wed Dec 19 23:20:55 2012 +0100
@@ -55,18 +55,26 @@
 {- Aufgabe G9.1 -}
 
 {-
-Lemma mirror (mirror t) = t
+Lemma(t): mirror (mirror t) = t
 Proof by structural induction on t
 
-Base case:
-To show:
+Base case: Lemma(Empty)
+To show: mirror (mirror Empty) = Empty
+mirror (mirror Empty)
+= mirror Empty                          mirror_Empty
+= Empty                                 mirror_Empty
 
-Induction step:
-IH1:
-IH2:
-To show:
+Induction step: Lemma(l), Lemma(r) => Lemma((Node x l r))
+IH1: mirror (mirror l) = l
+IH2: mirror (mirror r) = r
+To show: mirror (mirror (Node x l r)) = Node x l r
+mirror (mirror (Node x l r))
+= mirror (Node x (mirror r) (mirror l))                 mirror_Node
+= Node x (mirror (mirror l)) (mirror (mirror r))        mirror_Node
+= Node x l (mirror (mirror r))                          IH1
+= Node x l r                                            IH2
 
-QED?
+QED!
 -}
 
 
@@ -75,7 +83,10 @@
 {- Aufgabe G9.2 -}
 
 balanced :: Tree a -> Bool
-balanced t = undefined
+balanced t = dist max t - dist min t <= 1
+        where
+        dist f (Node _ l r) = 1 + f (dist f l) (dist f r)
+        dist _ Empty = 0
 
 
 
@@ -83,13 +94,23 @@
 {- Aufgabe G9.3 -}
 
 type Coords = (Int, Int)
-data Shape = Missing
+data Shape =
+        Line Coords Coords
+        | Circle Coords Int
+
 
 move :: Coords -> Shape -> Shape
-move (x,y) _ = undefined
+move (x,y) (Line (a,b) (c,d)) = Line (a+x, b+y) (c+x, d+y)
+move (x,y) (Circle (a,b) r)   = Circle (a+x, b+y) r
+
 
 polygon :: [Shape] -> Bool
-polygon _ = undefined
+polygon ((Line from to) : ss) = polygon' from to ss
+        where
+        polygon' f t [] = f == t
+        polygon' f t ((Line lf lt) : ss) = t == lf && polygon' f lt ss
+        polygon' _ _ _ = False
+polygon _ = False