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

text {*
  Dies ist das letzte reguläre Übungsblatt in diesem Semester. In den
  folgenden Wochen wollen wir uns dann einem kleinen
  Verifikationsprojekt widmen, nämlich der Verifikation von
  Rot-Schwarz-Bäumen.

  Rot-Schwarz-Bäume sind binäre Suchbäume mit einer zusätzlichen
  Invariante, die garantiert, dass die Bäume immer so balanciert
  bleiben, dass alle Operationen mit der Worst-Case-Zeitkomplexität
  $O(\log n)$ laufen.
*}


section {* Binäre Suchbäume *}

text {*
  Heute formalisieren wir zum Einstieg normale binäre Suchbäume.
  Wir definieren den Datentyp aber schon so, dass wir in Zukunft
  Rot-Schwarz-Bäume damit implementieren können. Also hat jeder Knoten
  zusätlich eine Farbe @{text R} oder @{text B}.
*}

datatype color = R | B

datatype rbt =
  E
| T color rbt nat rbt


text {*
  Wie immer konzentrieren wir uns aufs Wesentliche: Unsere Bäume
  speichern nur die Schlüssel (vom Typ @{typ nat}), und keine weiteren
  Daten. Dementsprechend repräsentiert ein Baum eine Menge von
  natürlichen Zahlen.

  $\rhd$ Definieren Sie eine Operation @{text "in_tree :: nat => rbt =>
  bool"}, die testet, ob ein Element in einem (beliebigen) Baum enthalten ist.
*}



text {*
  Suchbäume erfüllen im allgemeinen die Invariante, dass der in einem
  Knoten gespeicherte Wert größer als jedes Element des linken
  Teilbaums ist und kleiner als jedes Element des rechten Teilbaums.

  $\rhd$ Definieren Sie eine Funktion @{text "st :: rbt => bool"}, die diese
  Invariante beschreibt.
*}


text {*
  Der Sinn dieser Invariante ist natürlich, dass man ein Element
  schneller finden kann. 

  $\rhd$ Schreiben Sie eine Funktion @{text "lookup :: nat => rbt =>
  bool"}, die prüft, ob ein Element in einem Suchbaum enthalten ist. 
*}


text {*
  $\rhd$ Zeigen Sie, dass sich @{text lookup} wie @{text in_tree},
  verhält, wenn der Baum ein Suchbaum ist. Dazu werden wie üblich
  ggfs.\ weitere Hilfsfunktionen und Lemmata benötigt.
*}

lemma lookup_st:
  "st t ==> lookup x t = in_tree x t"
sorry
(*<*)
end
(*>*)