# HG changeset patch
# User Markus Kaiser <markus.kaiser@in.tum.de>
# Date 1356050685 -3600
# Node ID 34fea195e2385f0825b16e38daa331b295ebbf1c
# Parent  f9386825bf71096ff8ab8d0c924ac2cec24c5cc7
beautify layout

diff -r f9386825bf71 -r 34fea195e238 exercises/src/Exercise_10.hs
--- a/exercises/src/Exercise_10.hs	Wed Dec 19 23:22:42 2012 +0100
+++ b/exercises/src/Exercise_10.hs	Fri Dec 21 01:44:45 2012 +0100
@@ -10,50 +10,72 @@
 {- Aufgabe G10.1 -}
 
 {-
-\alpha ist wie in den Folien definiert.
+
+Abstraktionsfunktion alpha:
 
+    \alpha [] = {}                                  -- alpha_empty
+    \alpha (x:xs) = {x} \union \alpha xs            -- alpha_cons
 
 Simulationseigenschaften:
 
-R_empty: \alpha empty = {}
-       : a      empty = {}
+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
 
+Implementierung 1 - Listen mit Duplikaten:
 
-R_insert: \alpha (insert x xs) = {x} \union \alpha xs
-        : a      (insert x xs) = {x}  union a      xs
+    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_isin: isin x xs = x \in \alpha xs
-      : isin x xs = x  in a      xs
+    nub [] = []                                     -- nub_empty
+    nub (x:xs) | x `elem` xs = nub xs               -- nub_cons_elem
+               | otherwise = x : nub xs             -- nub_cons_notelem
 
+Korrektheitsbeweise:
 
-R_size: size xs = |\alpha xs|
-      : size xs = |a      xs|
-
-
+1. \alpha empty
+    =
+2. \alpha (insert x xs)
+    =
+3. isin x xs
+    =
+4. size xs
+    =
 
 Hilfslemmata:
 
-L_elem(xs): elem x xs = x in a xs
-Proof by structural induction on xs
+    elem x xs = x \in \alpha xs     -- lemma_elem
+
+        Proof by structural induction on xs
 
-Base case: L_elem([])
-To show:
+        Base case: lemma_elem([])
+        To show:
 
-Induction step: L_elem(ys) => Lemma(y : ys)
-IH:
-To show:
+        Induction step: lemma_elem(ys) => lemma_elem(y : ys)
+        IH:
+        To show:
+
+    length (nub xs) = |\alpha xs|   -- lemma_length
 
+        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_elem([])
-To show:
+        Induction step: lemma_length(ys) => lemma_length(y : ys)
+        IH:
+        To show:
 
-Induction step: L_elem(ys) => Lemma(y : ys)
-IH:
-To show:
+        Proof by cases:
+        Case:
+
+        Case:
 
 -}
 
@@ -103,4 +125,4 @@
 {---------------------------------------------------------------------}
 {- Aufgabe H10.3 -}
 
-{- siehe Morsi.hs -}
\ No newline at end of file
+{- siehe Morsi.hs -}
diff -r f9386825bf71 -r 34fea195e238 exercises/src/SetPairList.hs
--- a/exercises/src/SetPairList.hs	Wed Dec 19 23:22:42 2012 +0100
+++ b/exercises/src/SetPairList.hs	Fri Dec 21 01:44:45 2012 +0100
@@ -1,4 +1,4 @@
-module SetPairList where
+-- ?
 
 -- Abstraction function
 {-