--- a/doc-src/TutorialI/Trie/Trie.thy Thu May 10 09:48:50 2001 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Thu May 10 13:44:44 2001 +0200
@@ -134,8 +134,114 @@
of the induction up in such a way that case distinction on @{term bs} makes
sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
and stable proofs.
+
+\begin{exercise}
+ Modify @{term 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 @{term 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
+ @{term 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 @{typ "('a * ('a,'v)trie)list"}
+ with @{typ"'a \<Rightarrow> ('a,'v)trie option"}.
+\end{exercise}
+
*};
(*<*)
+
+(* Exercise 1. Solution by Getrud Bauer *)
+
+consts update1 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
+primrec
+ "update1 t [] vo = Trie vo (alist t)"
+ "update1 t (a#as) vo =
+ (let tt = (case assoc (alist t) a of
+ None \<Rightarrow> Trie None []
+ | Some at \<Rightarrow> at)
+ in Trie (value t) ((a, update1 tt as vo) # alist t))"
+
+theorem [simp]: "\<forall>t v bs. lookup (update1 t as v) bs =
+ (if as = bs then v else lookup t bs)";
+apply (induct_tac as, auto);
+apply (case_tac[!] bs, auto);
+done
+
+
+(* Exercise 2. Solution by Getrud Bauer *)
+
+consts overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list"
+primrec
+ "overwrite a v [] = [(a,v)]"
+ "overwrite a v (p#ps) = (if a = fst p then (a,v)#ps else p # overwrite a v ps)"
+
+lemma [simp]: "\<forall> a v b. assoc (overwrite a v ps) b = assoc ((a,v)#ps) b"
+apply (induct_tac ps, auto)
+apply (case_tac[!] a)
+done
+
+consts update2 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie";
+primrec
+ "update2 t [] vo = Trie vo (alist t)"
+ "update2 t (a#as) vo =
+ (let tt = (case assoc (alist t) a of
+ None \<Rightarrow> Trie None []
+ | Some at \<Rightarrow> at)
+ in Trie (value t) (overwrite a (update2 tt as vo) (alist t)))";
+
+theorem "\<forall>t v bs. lookup (update2 t as vo) bs =
+ (if as = bs then vo else lookup t bs)";
+apply (induct_tac as, auto);
+apply (case_tac[!] bs, auto);
+done
+
+
+(* Exercise 3. Solution by Getrud Bauer *)
+datatype ('a,'v) triem = Triem "'v option" "'a \<Rightarrow> ('a,'v) triem option";
+
+consts valuem :: "('a, 'v) triem \<Rightarrow> 'v option"
+primrec "valuem (Triem ov m) = ov";
+
+consts mapping :: "('a,'v) triem \<Rightarrow> 'a \<Rightarrow> ('a, 'v) triem option";
+primrec "mapping (Triem ov m) = m";
+
+consts lookupm :: "('a,'v) triem \<Rightarrow> 'a list \<Rightarrow> 'v option"
+primrec
+ "lookupm t [] = valuem t"
+ "lookupm t (a#as) = (case mapping t a of
+ None \<Rightarrow> None
+ | Some at \<Rightarrow> lookupm at as)";
+
+lemma [simp]: "lookupm (Triem None (\<lambda>c. None)) as = None";
+apply (case_tac as, simp_all);
+done
+
+consts updatem :: "('a,'v)triem \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)triem"
+primrec
+ "updatem t [] v = Triem (Some v) (mapping t)"
+ "updatem t (a#as) v =
+ (let tt = (case mapping t a of
+ None \<Rightarrow> Triem None (\<lambda>c. None)
+ | Some at \<Rightarrow> at)
+ in Triem (valuem t)
+ (\<lambda>c. if c = a then Some (updatem tt as v) else mapping t c))";
+
+theorem "\<forall>t v bs. lookupm (updatem t as v) bs =
+ (if as = bs then Some v else lookupm t bs)";
+apply (induct_tac as, auto);
+apply (case_tac[!] bs, auto);
+done
+
end;
(*>*)
--- 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:
--- a/doc-src/TutorialI/fp.tex Thu May 10 09:48:50 2001 +0200
+++ b/doc-src/TutorialI/fp.tex Thu May 10 13:44:44 2001 +0200
@@ -467,20 +467,6 @@
of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
\input{Trie/document/Trie.tex}
-\begin{exercise}
- Write an improved version of \isa{update} that does not suffer from the
- space leak in the version above. Prove the main theorem for your improved
- \isa{update}.
-\end{exercise}
-
-\begin{exercise}
- Write a function to \emph{delete} entries from a trie. An easy solution is
- a clever modification of \isa{update} which allows both insertion and
- deletion 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}
-
\section{Total Recursive Functions}
\label{sec:recdef}
\index{*recdef|(}