(*<*)
theory a2 = Main:
(*>*)

text {*
  \section*{Sortieren auf Listen}

  Der erste Teil des Blattes beschäftigt sich mit einem
  einfachen Sortieralgorithmus auf Listen von natürlichen Zahlen.
  Ihre Aufgabe ist es, den Sortieralgorithmus in Isabelle zu
  programmieren und zu zeigen, dass Ihre Implementierung korrekt ist.

  Der Algorithmus lässt sich in folgende Funktionen zerlegen:
*}
consts 
  insort :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
  sort   :: "nat list \<Rightarrow> nat list"
  le     :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
  sorted :: "nat list \<Rightarrow> bool"
text {*
  Hierbei soll @{term "insort x xs"} eine Zahl @{term x} in eine
  sortierte Liste @{text xs} einfügen, und die Funktion @{term "sort ys"}
  (aufbauend auf @{text insort}) die sortierte Version von @{text ys}
  liefern.

  Um zu zeigen, dass die resultierende Liste tatsächlich sortiert
  ist, benötigen sie das Prädikat @{term "sorted xs"}, das überprüft
  ob jedes Element der Liste kleiner ist als alle folgenden Elemente
  der Liste. Die Funktion @{term "le n xs"} soll genau dann wahr sein,
  wenn @{term n} kleiner oder gleich allen Elementen von @{text xs}
  ist. 

  Zeigen Sie zu Beginn folgendes Monotonie-Lemma über @{term le}. Die
  Formulierung des Lemmas ist aus technischen Gründen (über die sie
  später im Praktikum mehr erfahren werden) etwas ungewohnt:
*} 
lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs"
  oops

text {*
  Zeigen Sie dann folgendes Korrektheits-Theorem:
*}
theorem "sorted (sort xs)"
  oops 

text  {*
  Das Theorem sagt zwar aus, dass Ihr Algorithmus eine sortierte
  Liste zurückgibt, es gibt Ihnen aber nicht die Sicherheit, dass die sortierte
  Liste auch die gleichen Elemente wie das Original enthält. Formulieren Sie deswegen
  eine Funktion @{term "count xs x"}, die zählt, wie oft die Zahl
  @{term x} in @{term xs} vorkommt. 
  
  Zeigen Sie:
*}
theorem "count (sort xs) x = count xs x"
  oops

text {*
  \section*{Sortieren mit Bäumen}

  Der zweite Teil des Blattes beschäftigt sich mit einem
  Sortieralgorithmus, der Bäume verwendet.
  Definieren Sie dazu zuerst den Datentyp @{text bintree} der
  Binärbäume. Für diese Aufgabe sind Binärbäume entweder leer, oder
  bestehen aus einem
  Knoten mit einer natürlichen Zahl und zwei Unterbäumen.  

  Schreiben Sie dann eine Funktion @{text tsorted}, die feststellt, ob
  ein Binärbaum geordnet ist. Sie werden dazu zwei Hilfsfunktionen
  @{text tge} und @{text tle} benötigen, die überprüfen ob eine Zahl
  grössergleich/kleinergleich als alle Elemente eines Baumes sind.

  Formulieren Sie schliesslich eine Funktion @{text tree_of}, die zu einer
  (unsortierten) Liste den geordneten Binärbaum zurückgibt. Stützen Sie
  sich dabei auf eine Funktion @{term "ins n b"}, die eine Zahl @{term
  n} in einen geordneten Binärbaum @{term b} einfügt.  

  Zeigen Sie:
*}
theorem [simp]: "tsorted (tree_of xs)"
  oops

text {* 
  Auch bei diesem Algorithmus müssen wir noch zeigen, dass keine
  Elemente beim Sortieren verloren gehen (oder erfunden werden). Formulieren
  Sie analog zu den Listen eine Funktion @{term "tcount x b"}, die zählt, wie
  oft die Zahl @{term x} im Baum @{term b} vorkommt.

  Zeigen Sie:
*} 
theorem "tcount (tree_of xs) x = count xs x"
  oops

text {*
  Die eigentliche Aufgabe war es, Listen zu sortieren. Bis jetzt haben
  wir lediglich einen Algorithmus, der Listen in geordnete Bäume
  transformiert. Definieren Sie deswegen eine Funktion @{text
  list_of}, die zu einen (geordneten) Baum eine (geordnete) Liste liefert.
  
  Zeigen Sie: ({\bf Achtung Update!})
*}
theorem "sorted (list_of (tree_of xs))"
  oops

theorem "count (list_of (tree_of xs)) n = count xs n"    
  oops

text {*
  \newpage
  \emph{Hinweise:}
  \begin{itemize}
  \item 
  Bevor Sie mit den Korrektheitsbeweisen anfangen, sollten Sie an
  einigen konkreten, kleinen Beispielen überprüfen, ob ihre Funktionen
  das tun, was sie erwarten.

  \item
  Die @{text auto}-Methode kann zwar mit Implikationen umgehen, für dieses
  Blatt eignen sich aber Gleichungen am besten. Versuchen Sie, alle Lemmas
  als Gleichungen zu formulieren, und sie so
  aufzuschreiben (ggf.~statt @{term "a=b"} einfach \mbox{@{term "b=a"}}),
  dass die rechte Seite `einfacher' ist als die linke.

  \item
  Für den letzen Teil müssen Sie @{text sorted} auf Listen und @{text tsorted}
  auf Bäumen zueinander in Beziehung setzen. Sie benötigen dazu eine
  Funktion @{text ge} auf Listen (analog zu @{text tge} auf Bäumen)
  und folgendes Lemma (das sie noch beweisen müssen):

  @{term "sorted (a@x#b) = (sorted a \<and> sorted b \<and> ge x a \<and> le x b)"}
  
  \item
  Nutzen Sie frühzeitig die Betreuungsangebote, wenn Sie
  Schwierigkeiten haben. Die Aufgabe lässt sich nicht an einem
  Nachmittag lösen.
  
  \item
  Wir möchten Schwierigkeit und Aufwand dieser Aufgabe genauer evaluieren.
  Wir sind v.a.~an Fehlern (Zahl und Art) in 
  Funktionsdefinitionen interessiert, auf die Sie
  während der Beweisarbeit stossen. Heben Sie deswegen bitte 
  falsche Versionen Ihrer Definitionen auf, wenn Sie eine Änderung
  vornehmen -- am einfachsten ist es, die alte Version
  auszukommentieren, und die neue Version darunter zu
  schreiben. Kommentare sind in Isabelle in \texttt{(*{}}
  und \texttt{{}*)} eingeschlossen. Die Fehler fließen
  selbstverständlich \emph{nicht} in Ihre Bewertung mit ein -- im
  Gegenteil, Sie machen es sich und nachfolgenden Generationen einfacher,
  wenn sie alle Änderungen möglichst genau dokumentieren.
  
  \end{itemize}
*}

(*<*)
end
(*>*)