--- a/exercises/src/Exercise_10.hs	Wed Dec 19 23:22:42 2012 +0100
+++ b/exercises/src/Exercise_10.hs	Thu Dec 20 19:16:20 2012 +0100
@@ -10,50 +10,128 @@
 {- Aufgabe G10.1 -}
 
 {-
-\alpha ist wie in den Folien definiert.
-
+\alpha ist wie in den Folien definiert:
+alpha [] = {}
+alpha (y:ys) = {y} union (alpha ys)
 
 Simulationseigenschaften:
 
 R_empty: \alpha empty = {}
        : a      empty = {}
+empty = []
+
+a empty
+== a []                                 -- by def of empty
+== {}                                   -- by def of alpha
 
 
 R_insert: \alpha (insert x xs) = {x} \union \alpha xs
         : a      (insert x xs) = {x}  union a      xs
+insert x xs = (x : xs)
 
+a (insert x xs)
+== a (x : xs)                           -- by def of insert
+== {x} union (a xs)                     -- by def of alpha
 
 R_isin: isin x xs = x \in \alpha xs
-      : isin x xs = x  in a      xs
+      : isin x xs = x \in a      xs
+isin x xs = elem x xs
 
+isin x xs
+== elem x xs                            -- by implementation
+== x \in (a xs)                         -- by L_elem
 
 R_size: size xs = |\alpha xs|
-      : size xs = |a      xs|
+      : size xs = | a     xs|
+size xs = length (nub xs)
 
+size xs
+== length (nub xs)                      -- by implementation
+== |a xs|                               -- by L_length
 
 
 Hilfslemmata:
 
-L_elem(xs): elem x xs = x in a xs
+Funktionen:
+
+elem x [] = False                               -- elem_Empty
+elem x (y:ys) = x == y || elem x ys             -- elem_Cons
+
+nub [] = []                                     -- nub_Empty
+nub (y:ys) =                                    -- nub_Cons
+        if y `elem` ys then nub ys
+        else {- not elem -} y : (nub ys)
+
+---
+
+L_elem(xs): elem x xs = x \in a xs
 Proof by structural induction on xs
 
 Base case: L_elem([])
-To show:
+To show: elem x [] = x \in a []
+elem x []
+== False                                        -- by elem_Empty
+
+x \in a []
+== x \in {}                                     -- by alpha
+== False                                        -- by {}
 
-Induction step: L_elem(ys) => Lemma(y : ys)
-IH:
-To show:
+Induction step: L_elem(ys) => L_elem(y : ys)
+IH: elem x ys = x \in (a ys)
+To show: elem x (y:ys) = x \in a (y:ys)
+elem x (y:ys)
+== x == y || elem x ys                          -- by elem_Cons
+== x == y || x \in (a ys)                       -- by IH
+
+x \in a (y:ys)
+== x \in ({y} union (a ys))                     -- alpha_Cons
+== x \in {y} || x \in (a ys)                    -- by union
+== x == y || x \in (a ys)                       -- by basic property
+
+qed
+
+---
 
 
-L_length(xs): length (nub xs) = |a xs| 
+L_length(xs): length (nub xs) = |a xs|
 Proof by structural induction on xs
 
-Base case: L_elem([])
-To show:
+Base case: L_length([])
+To show: length (nub []) = |a []|
+length (nub [])
+== length []                                    -- by nub_Empty
+== 0                                            -- by def of length
+
+|a []|
+== |{}|                                         -- by alpha
+== 0                                            -- by def of ||
 
-Induction step: L_elem(ys) => Lemma(y : ys)
-IH:
-To show:
+Induction step: L_length(ys) => L_length(y : ys)
+IH: length (nub ys) = |a ys|
+To show: length (nub (y:ys)) = |a (y:ys)|
+Proof by cases
+case: y `elem` ys
+        length (nub (y:ys))
+        == length (nub ys)                      -- by nub_Cons
+        == |a ys|                               -- IH
+
+        |a (y:ys)|
+        == |{y} union a ys|                     -- alpha_Cons
+        == |(a ys)|                             -- by basic property
+
+case: not (y `elem` ys)
+        length (nub (y:ys))
+        == length (y : (nub ys))                -- by nub_Cons
+        == 1 + length [] + length (nub ys)      -- by length_Cons
+        == 1 + length (nub ys)                  -- by length_Empty
+        == 1 + |a ys|                           -- IH
+
+        |a (y:ys)|
+        == |{y} union a ys|                     -- alpha_Cons
+        == |{y}| + |a ys|                       -- by def of union, case
+        == 1 + |a ys|                           -- by def of ||
+
+qed
 
 -}
 
@@ -72,16 +150,135 @@
 {- siehe Queue.hs und SuperQueue.hs -}
 
 {-
+Simulationseigenschaften zu beweisen:
+
+    \alpha empty = []
+    isEmpty q = \alpha q == []
+    \alpha (enqueue x q) = \alpha q ++ [x]
+    ~ isEmpty q ==> \alpha (dequeue q) = (head (\alpha q), tail (\alpha q))
+    q == q' = \alpha q == \alpha q'
+
 Definition von \alpha:
 
-        \alpha (Queue front kcab) = undefined
+    \alpha (Queue front kcab) = front ++ reverse kcab
+
+Beweis fuer "empty":
+
+    \alpha empty
+      = \alpha (Queue [] [])                -- by def of empty
+      = [] ++ reverse []                    -- by def of \alpha
+      = []                                  -- by def of reverse, ++
+
+Beweis fuer "isEmpty":
+
+    Hilfssatz: q == Queue [] [] = \alpha q == []
+
+    isEmpty q
+      = q == Queue [] []                    -- by def of isEmpty
+      = \alpha q == []                      -- by lemma
+
+Beweis fuer "enqueue":
+
+    Sei q = Queue front kcab                -- by exhaustivity of constructor
 
+    \alpha (enqueue x q)
+      = \alpha (enqueue x (Queue front kcab))
+                                            -- by def of q
+      = \alpha (Queue (front (x : kcab)))   -- by def of enqueue
+      = front ++ reverse (x : kcab)         -- by def of \alpha
+      = front ++ (reverse kcab ++ [x])      -- by def of reverse
+      = (front ++ reverse kcab) ++ [x]      -- by commutativity of ++
+      = \alpha (Queue front kcab) ++ [x]    -- by def of \alpha
+      = \alpha q ++ [x]                     -- by def of q
+
+Hilfslemma L:
+
+    Zu beweisen: \alpha (Queue [] kcab) = \alpha (Queue (reverse kcab) [])
+
+    \alpha (Queue [] kcab)
+      = [] ++ reverse kcab                  -- by def of \alpha
+      = reverse kcab                        -- by def of ++
+
+    \alpha (Queue (reverse kcab) [])
+      = reverse kcab ++ []                  -- by def of \alpha
+      = reverse kcab                        -- by def of ++
+
+Beweis fuer "dequeue":
+
+    Annahme: ~ isEmpty q
+
+    Sei q = Queue front kcab
+
+    Fallunterscheidung auf front und kcab:
+
+    Fall front = [], kcab = []:
+      ~ isEmpty (Queue front kcab)
+        = ~ isEmpty (Queue [] [])
+        = False
+      Nichts mehr zu beweisen, weil die Annahme nicht erfuellt ist.
 
-Simulationseigenschaften: (5)
+    Fall front /= []:
+      \alpha (dequeue q)
+        = \alpha (dequeue (Queue front kcab))
+                                            -- def of q
+        = \alpha (head front, Queue (tail front) kcab)
+                                            -- def of dequeue (2nd equation)
+        = (head front, \alpha (Queue (tail front) kcab))
+                                            -- \alpha is an homomorphism
+
+      Es bleibt zu beweisen, dass
 
+        head front = head (\alpha q)
+        \alpha (Queue (tail front) kcab) = tail (\alpha q)
+
+        head (\alpha q)
+          = head (\alpha (Queue front kcab))  -- def of q
+          = head (front ++ reverse kcab)      -- def of \alpha
+          = head front                        -- basic prop of head, front /= []
+
+        \alpha (Queue (tail front) kcab)
+          = tail front ++ reverse kcab        -- def of \alpha
+
+        tail (\alpha q)
+          = tail (\alpha (Queue front kcab))  -- def of q
+          = tail (front ++ reverse kcab)      -- def of \alpha
+          = tail front ++ reverse kcab        -- basic prop of tail, front /= []
 
+    Fall front = [], kcab /= []:
+      \alpha (dequeue q)
+        = \alpha (dequeue (Queue front kcab)) -- def of q
+        = \alpha (dequeue (Queue [] kcab))    -- assumption front = []
+        = \alpha (dequeue (Queue (reverse kcab) []))
+                                              -- def of dequeue (1st equation)
+        = (head (\alpha (Queue (reverse kcab) [])),
+           tail (\alpha (Queue (reverse kcab) [])))
+                                              -- by reduction to already proved
+                                              -- case, reverse kcab /= []
+        = (head (\alpha (Queue [] kcab)), tail (\alpha (Queue [] kcab)))
+                                              -- by lemma L (twice)
+        = (head (\alpha q), tail (\alpha q))  -- by def of q (twice)
 
-Beweise:
+Beweis fuer ==:
+
+    Zu beweisen: q == q' = \alpha q == \alpha q'
+
+    Seien q = Queue (front kcab)
+          q' = Queue (front' kcab')
+
+    q == q'
+      = Queue (front kcab) == Queue (front' kcab')
+                                              -- by def of q, q'
+      = toList (Queue (front kcab)) == toList (Queue (front' kcab'))
+                                              -- by def of ==
+      = front ++ reverse kcab == front' ++ reverse kcab'
+                                              -- by def of toList
+
+    \alpha q == \alpha q'
+      = \alpha (Queue (front kcab)) == \alpha (Queue (front' kcab'))
+                                              -- by def of ==
+      = front ++ reverse kcab == front' ++ reverse kcab'
+                                              -- by def of \alpha
+
 -}
 
 

--- a/exercises/src/Queue.hs	Wed Dec 19 23:22:42 2012 +0100
+++ b/exercises/src/Queue.hs	Thu Dec 20 19:16:20 2012 +0100
@@ -1,4 +1,4 @@
-module Queue where
+module Queue (Queue, empty, isEmpty, enqueue, dequeue) where
 import Test.QuickCheck
 import Test.QuickCheck.Poly (A)
 
@@ -6,19 +6,20 @@
   deriving (Eq, Show)
 
 empty :: Queue a
-empty = undefined
+empty = Queue []
 
 isEmpty :: Queue a -> Bool
-isEmpty (Queue xs) = undefined
+isEmpty (Queue []) = True
+isEmpty _ = False
 
 enqueue :: a -> Queue a -> Queue a
-enqueue x (Queue xs) = undefined
+enqueue x (Queue xs) = Queue (xs ++ [x])
 
 dequeue :: Queue a -> (a, Queue a)
-dequeue (Queue (x : xs)) = undefined
+dequeue (Queue (x : xs)) = (x, Queue xs)
 
 toList :: Queue a -> [a]
-toList (Queue xs) = undefined
+toList (Queue xs) = xs
 
 
 {- QuickCheck Tests -}

--- a/exercises/src/SetPairList.hs	Wed Dec 19 23:22:42 2012 +0100
+++ b/exercises/src/SetPairList.hs	Thu Dec 20 19:16:20 2012 +0100
@@ -1,35 +1,48 @@
-module SetPairList where
+module SetPairList(Set, empty, insert, isin, size, union, delete) where
 
 -- Abstraction function
 {-
-    alpha (S x) = undefined
+    alpha :: Set a -> {a}
+    alpha (S []) = {}
+    alpha (S ((a, b):xs)) = {a..b} union (alpha xs)
 
     To show: (10 things)
+    alpha empty =  {}
+    invar s ==> alpha (insert x s) = {x} union alpha s
+    invar s ==> alpha (delete x s) = alpha s \ {x}
+    invar s ==> isin x s = x \in alpha s
+    invar s ==> size s = |alpha s|
+    invar s1, invar s2 ==> alpha (union s1 s2) = (alpha s1) union (alpha s2)
+
+    invar empty
+    invar s ==> invar (insert x s)
+    invar s ==> invar(delete x s)
+    invar s1, invar s2 ==> invar (union s1 s2)
 -}
 
 -- Interface
-newtype Set a = S (...)
+newtype Set a = S (PairList a)
 
 invar :: Integral a => Set a -> Bool
-invar (S s) = undefined
+invar (S s) = invarPL s
 
 empty :: Set a
-empty = undefined
+empty = S emptyPL
 
 insert :: Integral a => a -> Set a -> Set a
-insert n (S s) = undefined
+insert n (S s) = S (insertPL n s)
 
 isin :: Integral a => a -> Set a -> Bool
-isin n (S s) = undefined
+isin n (S s) = isinPL n s
 
 size :: Integral a => Set a -> Integer
-size (S s) = undefined
+size (S s) = sizePL s
 
 union :: Integral a => Set a -> Set a -> Set a
-union (S s1) (S s2) = undefined
+union (S s1) (S s2) = S (unionPL s1 s2)
 
 delete :: Integral a => a -> Set a -> Set a
-delete n (S s) = undefined
+delete n (S s) = S (deletePL n s)
 
 -- Implementation
 type PairList a = [(a, a)]

--- a/exercises/src/SuperQueue.hs	Wed Dec 19 23:22:42 2012 +0100
+++ b/exercises/src/SuperQueue.hs	Thu Dec 20 19:16:20 2012 +0100
@@ -1,29 +1,31 @@
-module SuperQueue where
+module SuperQueue (Queue, empty, enqueue, dequeue) where
 import Test.QuickCheck
 import Test.QuickCheck.Poly (A)
 
 data Queue a = Queue [a] [a]
 
 empty :: Queue a
-empty = undefined
+empty = Queue [] []
 
 isEmpty :: Queue a -> Bool
-isEmpty (Queue front kcab) = undefined
+isEmpty (Queue [] []) = True
+isEmpty _ = False
 
 enqueue :: a -> Queue a -> Queue a
-enqueue x (Queue front kcab) = undefined
+enqueue x (Queue front kcab) = Queue front (x : kcab)
 
 dequeue :: Queue a -> (a, Queue a)
-dequeue (Queue front kcab) = undefined
+dequeue (Queue [] kcab) = dequeue (Queue (reverse kcab) [])
+dequeue (Queue front kcab) = (head front, Queue (tail front) kcab)
 
 toList :: Queue a -> [a]
-toList (Queue front kcab) = undefined
+toList (Queue front kcab) = front ++ reverse kcab
 
 instance Eq a => Eq (Queue a) where
-  q == q' = undefined
+  q == q' = toList q == toList q'
 
 instance Show a => Show (Queue a) where
-  show = undefined
+  show = show . toList
 
 
 {- QuickCheck Tests -}