module Exercise_10 (module Join, module SafeMap) where

{- Library DO NOT CHANGE -}
import SafeMap (SafeMap, empty, update, lookup)
import Join (Field, doJoin, doJoinFormat, parseFormat)
{- End Library -}


{---------------------------------------------------------------------}
{- Aufgabe G10.1 -}

{-

Abstraktionsfunktion alpha:

    \alpha [] = {}                                  -- alpha_empty
    \alpha (x:xs) = {x} \union \alpha xs            -- alpha_cons

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

Implementierung 1 - Listen mit Duplikaten:

    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

    nub [] = []                                     -- nub_empty
    nub (x:xs) | x `elem` xs = nub xs               -- nub_cons_elem
               | otherwise = x : nub xs             -- nub_cons_notelem

Korrektheitsbeweise:

1. \alpha empty
    =
2. \alpha (insert x xs)
    =
3. isin x xs
    =
4. size xs
    =

Hilfslemmata:

    elem x xs = x \in \alpha xs     -- lemma_elem

        Proof by structural induction on xs

        Base case: lemma_elem([])
        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

        Base case: lemma_length([])
        To show:

        Induction step: lemma_length(ys) => lemma_length(y : ys)
        IH:
        To show:

        Proof by cases:
        Case:

        Case:

-}



{---------------------------------------------------------------------}
{- Aufgabe G10.2 -}

{- siehe SetPairList.hs -}



{---------------------------------------------------------------------}
{- Aufgabe G10.3 -}

{- siehe Queue.hs und SuperQueue.hs -}

{-
Definition von \alpha:

        \alpha (Queue front kcab) = undefined


Simulationseigenschaften: (5)



Beweise:
-}



{---------------------------------------------------------------------}
{- Aufgabe H10.1 -}

{- siehe SafeMap.hs -}



{---------------------------------------------------------------------}
{- Aufgabe H10.2 -}

{- siehe Join.hs -}



{---------------------------------------------------------------------}
{- Aufgabe H10.3 -}

{- siehe Morsi.hs -}