header {* B\"aume *}

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

text{*Definieren Sie einen Datentyp @{text"'a tree"} f\"ur
Bin\"arb\"aume, bei denen nur die Bl\"atter Information enthalten
k\"onnen.*};

datatype 'a tree(*<*) \<guillemotleft>! FILL IN !\<guillemotright> (*>*)

text{*Definieren Sie eine Funktion @{term leaves}, die die Information
an den Bl\"attern des Baumes von links nach rechts ausgibt.*};
(*<*)consts(*>*)
  leaves :: "'a tree \<Rightarrow> 'a list"
text{*Definieren Sie eine Funktion: *}(*<*)consts(*>*)
  plant :: "'a list \<Rightarrow> 'a tree"
text{* so dass die folgende Eigenschaft gilt.*};
theorem "leaves (plant xs) = xs"
(*<*)oops(*>*)
text{*Definieren Sie eine Funktion @{term mirror}, die das Spiegelbild eines Baums berechnet. *};
  (*<*)consts(*>*)
  mirror :: "'a tree \<Rightarrow> 'a tree" 

text {* Beweisen oder widerlegen Sie (mit Gegenbeispiel) nun folgende
Behauptungen.*};

theorem "leaves (mirror xt) = rev (leaves xt)"
(*<*)oops(*>*)

theorem "leaves (mirror (plant xs)) = rev xs"
(*<*)oops(*>*) 
theorem "plant (rev (leaves xt)) = mirror xt"
(*<*)oops(*>*) 

text {*Sei @{term Branch} Ihr Konstruktor f\"ur B\"aume *}
theorem "leaves (Branch (plant xs) (plant ys)) = (xs @ ys)"
(*<*)oops(*>*) 
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
(*<*)oops(*>*) 

text{* Jetzt arbeiten wir mit Bin\"arb\"aumen, deren Bl\"atter und
Knoten Information enthalten. Definieren Sie einen Datentype @{text"'a
ntree"} f\"ur solche Bin\"arb\"aume.*};
datatype 'a ntree(*<*)\<guillemotleft>! FILL IN !\<guillemotright> (*>*)
text{*Definieren Sie Funktionen @{term preOrder}, @{term
postOrder} und @{term inOrder}, die B\"aume in der entsprechende
Reihenfolge durchgehen.*}
(*<*)consts(*>*)
  preOrder :: "'a ntree \<Rightarrow> 'a list"
  postOrder :: "'a ntree \<Rightarrow> 'a list"
  inOrder :: "'a ntree \<Rightarrow> 'a list"
text{*Definieren Sie eine Funktion @{term nmirror}, die das
Spiegelbild solcher B\"aume berechnet.*}; 
(*<*)consts(*>*)
  nmirror :: "'a ntree \<Rightarrow> 'a ntree"

text{*Sei @{term xOrder} und @{term yOrder} jeweils eine von den
Funktionen @{term preOrder}, @{term postOrder} oder @{term
inOrder}. Formulieren und beweisen Sie alle g\"ultigen Eigenschaften
der Form \mbox{@{text "xOrder (mirror xt) = rev (yOrder xt)"}}.*}

text{*Definieren Sie Funktionen @{term root}, @{term leftmost} und
@{term rightmost}, die die Wurzel, das Element ganz links, bzw. das
Elemente ganz rechts im Baum liefern.*}
(*<*)consts(*>*)
  root :: "'a ntree \<Rightarrow> 'a"
  leftmost :: "'a ntree \<Rightarrow> 'a"
  rightmost :: "'a ntree \<Rightarrow> 'a"
text {* Beweisen oder widerlegen Sie (mit Gegenbeispiel) nun folgende Behauptungen.
Eventuell m\"ussen Sie dazu erst einige Lemmas beweisen.*};

theorem "last(inOrder xt) = rightmost xt"
(*<*)oops(*>*) 
theorem "hd (inOrder xt) = leftmost xt "
(*<*)oops(*>*) 
theorem "hd(preOrder xt) = last(postOrder xt)"
(*<*)oops(*>*) 
theorem "hd(preOrder xt) = root xt"
(*<*)oops(*>*) 
theorem "hd(inOrder xt) = root xt "
(*<*)oops(*>*) 
theorem "last(postOrder xt) = root xt"
(*<*)oops(*>*) 


(*<*)end(*>*)