(*<*)
theory Trie1 = Main:;
(*>*)

text {*
In Kapitel 3.4.4 des Tutorials wird eine Fallstudie \"uber sogenannte Tries 
durchgef\"uhrt, das sind Datenstrukturen zur schnellen Indizierung mit Strings, 
d.h. f\"uer gewisse Strings wird in einem zeichenweise verzweigten Baum ein Wert 
zugeordnet.

Lesen Sie den Abschnitt 3.4.4 im Tutorial. 

Der Datentyp der Tries \"uber dem Alphabet-Typ @{typ 'a} und dem Werte-Typ @{typ 'v} 
wird dort auf die folgende Weise definiert. *}

datatype ('a, 'v) trie = Trie  "'v option"  "('a * ('a,'v) trie) list";

text {* Ein Trie besteht also aus einem optionalen Wert und
einer Assoziationsliste, die Zeichen des Alphabets auf Unterb\"aume
abbildet. Zur Modellierung optionaler Werte wird der Datentyp @{typ "'a option"}
%\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%
verwendet (siehe Tutorial, 2.5.3). 

Ferner werden dort zugeh\"orige Selektor-Funktionen @{term value} und 
@{term alist} definiert. *}

consts value :: "('a, 'v) trie \<Rightarrow> 'v option"
primrec "value (Trie ov al) = ov"; 

consts alist :: "('a, 'v) trie \<Rightarrow> ('a * ('a,'v) trie) list";
primrec "alist (Trie ov al) = al";

text {* Au{\ss}erdem ist die Funktion @{term lookup} f\"ur Tries 
gegeben, die mit Hilfe der generischen Such-Funktion @{term assoc} 
f\"ur Assoziationslisten definiert wird. *}

consts assoc ::  "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option";
primrec "assoc [] x = None"
        "assoc (p#ps) x =
           (let (a, b) = p in if a = x then Some b else assoc ps x)";

consts lookup :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option";
primrec "lookup t [] = value t"
        "lookup t (a#as) = (case assoc (alist t) a of
                              None \<Rightarrow> None
                            | Some at \<Rightarrow> lookup at as)";

text {* Die Funktion @{term update} f\"ugt einen neuen Wert zu einem String
in einen Trie ein, indem sie den alten Wert, der dem String zugeordnet 
war, \"uberschreibt.

Zun\"achst nochmal die Definition der Funktion @{term update} aus dem Tutorial. *}

consts update :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a, 'v) trie";
primrec
  "update t []     v = Trie (Some v) (alist t)"
  "update t (a#as) v =
     (let tt = (case assoc (alist t) a of
                  None \<Rightarrow> Trie None [] 
                | Some at \<Rightarrow> at)
      in Trie (value t) ((a, update tt as v) # alist t))";

text {* Das folgende Theorem besagt, dass sich die Funktion @{term update} so verh\"alt, 
wie man es erwartet: *}

theorem "\<forall>t v bs. lookup (update t as v) bs =
                    (if as = bs then Some v else lookup t bs)"; sorry

text {* 
Definieren Sie eine Funktion *}

consts modify :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie";

text{*
mit der man sowohl Elemente einf\"ugen als auch l\"oschen kann. 
Beweisen Sie f\"ur diese Funktion eine abgewandelte Version des obigen Theorems.
*}

(*<*)
end;
(*>*)