--- a/exercises/src/Exercise_10.hs	Fri Dec 21 01:44:45 2012 +0100
+++ b/exercises/src/Exercise_10.hs	Wed Jan 09 19:45:47 2013 +0100
@@ -10,72 +10,128 @@
 {- Aufgabe G10.1 -}
 
 {-
-
-Abstraktionsfunktion alpha:
-
-    \alpha [] = {}                                  -- alpha_empty
-    \alpha (x:xs) = {x} \union \alpha xs            -- alpha_cons
+\alpha ist wie in den Folien definiert:
+alpha [] = {}
+alpha (y:ys) = {y} union (alpha ys)
 
 Simulationseigenschaften:
 
-1.  \alpha empty = {}                               -- sim_empty
-2.  \alpha (insert x xs) = {x} \union \alpha xs     -- sim_insert
-3.  isin x xs = x \in \alpha xs                     -- sim_isin
-4.  size xs = |\alpha xs|                           -- sim_size
+R_empty: \alpha empty = {}
+       : a      empty = {}
+empty = []
 
-Implementierung 1 - Listen mit Duplikaten:
+a empty
+== a []                                 -- by def of empty
+== {}                                   -- by def of alpha
 
-    empty = []                                      -- imp_empty
-    insert x xs = x : xs                            -- imp_insert
-    isin x xs = elem x xs                           -- imp_isin
-    size xs = length (nub xs)                       -- imp_size
 
-    elem _ [] = False                               -- elem_empty
-    elem x (y:ys) = x == y || elem x ys             -- elem_cons
+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
 
-    nub [] = []                                     -- nub_empty
-    nub (x:xs) | x `elem` xs = nub xs               -- nub_cons_elem
-               | otherwise = x : nub xs             -- nub_cons_notelem
+R_isin: isin x xs = x \in \alpha xs
+      : isin x xs = x \in a      xs
+isin x xs = elem x xs
 
-Korrektheitsbeweise:
+isin x xs
+== elem x xs                            -- by implementation
+== x \in (a xs)                         -- by L_elem
 
-1. \alpha empty
-    =
-2. \alpha (insert x xs)
-    =
-3. isin x xs
-    =
-4. size xs
-    =
+R_size: size xs = |\alpha xs|
+      : size xs = | a     xs|
+size xs = length (nub xs)
+
+size xs
+== length (nub xs)                      -- by implementation
+== |a xs|                               -- by L_length
+
 
 Hilfslemmata:
 
-    elem x xs = x \in \alpha xs     -- lemma_elem
+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)
 
-        Proof by structural induction on xs
+---
+
+L_elem(xs): elem x xs = x \in a xs
+Proof by structural induction on xs
+
+Base case: L_elem([])
+To show: elem x [] = x \in a []
+elem x []
+== False                                        -- by elem_Empty
 
-        Base case: lemma_elem([])
-        To show:
+x \in a []
+== x \in {}                                     -- by alpha
+== False                                        -- by {}
 
-        Induction step: lemma_elem(ys) => lemma_elem(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
 
-    length (nub xs) = |\alpha xs|   -- lemma_length
+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
+
+---
 
-        Proof by structural induction on xs
+
+L_length(xs): length (nub xs) = |a xs|
+Proof by structural induction on xs
 
-        Base case: lemma_length([])
-        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: lemma_length(ys) => lemma_length(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
 
-        Proof by cases:
-        Case:
+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
 
-        Case:
+        |a (y:ys)|
+        == |{y} union a ys|                     -- alpha_Cons
+        == |{y}| + |a ys|                       -- by def of union, case
+        == 1 + |a ys|                           -- by def of ||
+
+qed
 
 -}
 
@@ -94,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
+
 -}
 
 
@@ -125,4 +300,4 @@
 {---------------------------------------------------------------------}
 {- Aufgabe H10.3 -}
 
-{- siehe Morsi.hs -}
+{- siehe Morsi.hs -}
\ No newline at end of file

--- a/exercises/src/Queue.hs	Fri Dec 21 01:44:45 2012 +0100
+++ b/exercises/src/Queue.hs	Wed Jan 09 19:45:47 2013 +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	Fri Dec 21 01:44:45 2012 +0100
+++ b/exercises/src/SetPairList.hs	Wed Jan 09 19:45:47 2013 +0100
@@ -1,35 +1,48 @@
--- ?
+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	Fri Dec 21 01:44:45 2012 +0100
+++ b/exercises/src/SuperQueue.hs	Wed Jan 09 19:45:47 2013 +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 -}