--- a/doc-src/TutorialI/Trie/document/Trie.tex Thu May 10 09:48:50 2001 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Thu May 10 13:44:44 2001 +0200
@@ -123,7 +123,29 @@
\isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
of the induction up in such a way that case distinction on \isa{bs} makes
sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
-and stable proofs.%
+and stable proofs.
+
+\begin{exercise}
+ Modify \isa{update} (and its type) such that it allows both insertion and
+ deletion of entries with a single function. Prove (a modified version of)
+ the main theorem above.
+ Optimize you function such that it shrinks tries after
+ deletion, if possible.
+\end{exercise}
+
+\begin{exercise}
+ Write an improved version of \isa{update} that does not suffer from the
+ space leak (pointed out above) caused by not deleting overwritten entries
+ from the association list. Prove the main theorem for your improved
+ \isa{update}.
+\end{exercise}
+
+\begin{exercise}
+ Conceptually, each node contains a mapping from letters to optional
+ subtries. Above we have implemented this by means of an association
+ list. Replay the development replacing \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list}
+ with \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ option}.
+\end{exercise}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables: