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


text {* Anstelle von Assozationslisten k\"onnen zur Modellierung der Verzweigung in einem
Knoten auch partielle Funktioen verwendet werden, die die Zeichen des Alphabets
auf zugeh\"orige Unterb\"aume abbilden. 
Partielle Funktionen kann man mit Hilfe des Typs @{typ "'a option"} simulieren: 
Ist @{term f} eine Funktion vom Typ @{typ "'a \<Rightarrow> 'b option"}, dann ist @{term "f a = Some b"}, 
falls @{term a} ein Wert @{term b} zugeodnet werden soll, ansonsten ist @{term "f a = None"}.
*}

datatype ('a, 'v) trie = Trie  "'v option" "'a \<Rightarrow> ('a,'v) trie option";

text{* Geben Sie entsprechende Selektoren f\"ur die ver\"anderte Datenstruktur an, 
passen Sie die Funktionen @{term lookup} und @{term modify} an und beweisen wieder ihren
Zusammenhang. *}

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