(*<*) theory TotalRecursion imports Main begin (*>*)

text {*
\section*{1. Listen zusammenf\"ugen}


In dieser Aufgabe soll eine Funktion @{text zip} definiert werden, welche
zwei Listen durch Verschachtelung zusammenf\"ugt.
Beispiel:
@{text "zip [a1, a2, a3]  [b1, b2, b3] = [a1, b1, a2, b2, a3, b3]"} 
 und
@{text "zip [a1] [b1, b2, b3] = [a1, b1, b2, b3]"}.
Verwenden Sie dazu das totale Rekursion.
*}


text {*
  Zeigen Sie, dass @{text zipr} distributiv \"uber @{text append} (also @{text @}) 
  ist.
*}


text {*
\section*{2. Merge Sort}


  Wir arbeiten im Folgenden nur auf Listen \"uber nat\"urlichen Zahlen.

  Definieren Sie ein Pr\"adikat @{term sorted}, welches pr\"uft, ob
  jedes Element kleiner oder gleich den folgenden ist; @{term "le n
  xs"} ist @{text True} g.d.w. @{term n} kleiner oder gleich allen
  Elementen in @{text xs}.


*}

consts 
  le     :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
  sorted :: "nat list \<Rightarrow> bool"

text{*
  Implementieren Sie nun \emph{Merge Sort}: Eine Liste wird durch
  Aufteilung in zwei Listen sortiert, welche einzeln sortiert und wieder
  zusammengef\"ugt werden.

  Definieren Sie mittels @{text fun} zwei Funktionen
*}

consts merge :: "nat list \<Rightarrow> nat list \<Rightarrow> nat list"
       msort :: "nat list \<Rightarrow> nat list"


text {* und zeigen Sie *}

theorem "sorted (msort xs)"
oops

text {*
  Sie werden daf\"ur Hilfslemmas \"uber @{text le} und @{text sorted} beweisen 
  m\"ussen.

Hinweise:
  \begin{itemize}

  \item Um eine Liste in zwei fast gleichlange H\"alften zu zerteilen, k\"onnen
  See die Funktionen \mbox{@{text "n div 2"}}, @{term take} und @{term drop}
  verwenden, wobei @{term "take n xs"} die ersten @{text n} Elemente von @{text xs}
  zur\"uckgibt, @{text "drop n xs"} den Rest.

  \item Versuchen Sie erstmal, das Lemma alleine zu l\"osen und selbst herauszufinden,
  welche Hilfslemmas Sie daf\"ur brauchen. Falls Sie so nicht weiterkommen, hier ein 
  paar \"Uberlegungen: 
  \begin{itemize}
  \item wie verh\"alt sich @{text le}, wenn der erste Parameter kleiner wird?
  \item was muss gelten, wenn der zweite Parameter von @{text le} @{text merge}
  ist?
  \item was muss gelten, damit @{text merge} @{text sorted} ist?
  \end{itemize}
  
  \end{itemize}
*}


(*<*) end (*>*)