--- 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