# HG changeset patch
# User nipkow
# Date 989495084 -7200
# Node ID 16481a4cc9f3e2be8702136706b962f7d5901cde
# Parent  6878bb02a7f90cb102367f73a745530e406d8b11
*** empty log message ***

diff -r 6878bb02a7f9 -r 16481a4cc9f3 doc-src/TutorialI/Trie/Trie.thy
--- 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;
 (*>*)
diff -r 6878bb02a7f9 -r 16481a4cc9f3 doc-src/TutorialI/Trie/document/Trie.tex
--- 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:
diff -r 6878bb02a7f9 -r 16481a4cc9f3 doc-src/TutorialI/fp.tex
--- 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|(}