theory RedBlackTree
imports Main
begin

datatype color = R | B
datatype rbt = E | Tr color rbt nat rbt

(* Farbe der Wurzel *)
consts
  treec :: "rbt \<Rightarrow> color"
primrec
  "treec E = B"
  "treec (Tr c lb v rb) = c"

(** 
 * Invariante 1: Kein roter Knoten hat einen roten Vater
 * \<Longleftrightarrow> Rote Knoten haben nur schwarze Kinder
 * \<Longleftrightarrow> Beide Kinder sind schwarz oder der Knoten selbst ist schwarz
 *)
consts
  inv1 :: "rbt \<Rightarrow> bool"
primrec
  "inv1 E = True"
  "inv1 (Tr c lt v rt) = (inv1 lt \<and> inv1 rt \<and> (c = B \<or> treec lt = B \<and> treec rt = B))"

(**
 * Invariante 2: Jeder Pfad von der Wurzel zu den Blättern enthält gleich viele schwarze Knoten
 * Zum Überprüfen dieser Invariante wird inv2_h verwendet. Dieses berechnet rekursiv:
 *   1. Ob alle Pfade zu den Blättern gleich viele schwarze Knoten enthalten,
 *   2. Wieviele schwarze Knoten in jedem solchen Pfad enthalten sind.
 *      Dabei werden Blätter nicht gezählt, denn diese sind sowieso immer schwarz.
 * Dabei ist der Wert in 2. natürlich nur von Bedeutung wenn 1. wahr ist.
 *)
consts
  inv2_h :: "rbt \<Rightarrow> (bool \<times> nat)"
primrec
  "inv2_h E = (True, 0)"
  "inv2_h (Tr c lt v rt) = (let il = inv2_h lt; ir = inv2_h rt 
                           in (fst il \<and> fst ir \<and> snd il = snd ir, if c = B then snd il + 1 else snd il))"
constdefs
  inv2 :: "rbt \<Rightarrow> bool"
  [simp]: "inv2 t == fst (inv2_h t)"

(* Ein gültiger Rot-Schwarz-Baum liegt vor, wenn Invariante 1 und Invariante 2 erfüllt sind und die Wurzel schwarz ist. *)
  isrbt :: "rbt \<Rightarrow> bool"
  [simp]: "isrbt t == (inv1 t \<and> inv2 t \<and> treec t = B)"

(* Blätter sind gültige Rot-Schwarz-Bäume *)
lemma "isrbt E" by simp


(* Beide Invarianten gelten auch für die beiden Teilbäume.
  (folgt direkt aus den Definitionen)
*)
lemma inv1_child: 
  assumes inv: "inv1 (Tr c lt v rt)"
  shows "inv1 lt \<and> inv1 rt" 
  using inv by simp

lemma inv2_child: 
  assumes inv: "inv2 (Tr c lt v rt)"
  shows "inv2 lt \<and> inv2 rt" 
  using inv by(simp add: Let_def)

(* Projektionen von inv2_h auf die beiden Komponenten. 
    bh = Schwarz-Tiefe des Baums
    bheq = Ist die Invariante erfüllt
*)
constdefs
  bh :: "rbt \<Rightarrow> nat"  
  bh_def: "bh t == snd (inv2_h t)"

  bheq :: "rbt \<Rightarrow> bool"
  bheq_def: "bheq t == fst (inv2_h t)"


(* Simp-Regeln für das rekursive Auffalten von bh und bheq: *)

(* Die folgenden Lemmas sollten i.A. ausreichend sein, um ohne bh_def und  bheq_def auszukommen.
   Falls man beim Beweisen nicht weiterkommt empfehle ich ein "unfolding bheq_def2" als Debugging ;) (Markus) *)
lemma [simp]: "bheq E = True" unfolding bheq_def by simp
lemma [simp]: "bh E = 0" unfolding bh_def by simp
lemma bheq_def2 [simp]: "bheq (Tr c lt v rt) = (bheq lt \<and> bheq rt \<and> bh lt = bh rt)"
  unfolding bheq_def bh_def by (simp add: Let_def)
lemma [simp]: "bh (Tr c lt v rt) = (if c = B then bh lt + 1 else bh lt)" 
  unfolding bh_def by (simp add: Let_def)
lemma inv2_bheq: "inv2 t = bheq t" unfolding bheq_def by simp

(* Ein Lemma zur Fallunterscheidung über rbts *)
lemma rbt_case: "t = E \<or> (\<exists>lt v rt. t = Tr R lt v rt) \<or> (\<exists>lt v rt. t = Tr B lt v rt)"
proof -
  have "t = E \<or> (\<exists>c lt v rt. t = Tr c lt v rt)" by (cases t) simp+
  thus ?thesis
  proof
    assume "t = E" thus ?thesis by simp
  next
    assume "\<exists>c lt v rt. t = Tr c lt v rt"
    then obtain c lt v rt where "t = Tr c lt v rt" by blast
    hence "t = Tr R lt v rt \<or> t = Tr B lt v rt" by (cases c) simp+
    thus ?thesis by auto
  qed
qed



end