doc-src/TutorialI/Trie/document/Trie.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,126 @@
+\begin{isabelle}%
+%
+\begin{isamarkuptext}%
+To minimize running time, each node of a trie should contain an array that maps
+letters to subtries. We have chosen a (sometimes) more space efficient
+representation where the subtries are held in an association list, i.e.\ a
+list of (letter,trie) pairs.  Abstracting over the alphabet \isa{'a} and the
+values \isa{'v} we define a trie as follows:%
+\end{isamarkuptext}%
+\isacommand{datatype}~('a,'v)trie~=~Trie~~{"}'v~option{"}~~{"}('a~*~('a,'v)trie)list{"}%
+\begin{isamarkuptext}%
+\noindent
+The first component is the optional value, the second component the
+association list of subtries.  This is an example of nested recursion involving products,
+which is fine because products are datatypes as well.
+We define two selector functions:%
+\end{isamarkuptext}%
+\isacommand{consts}~value~::~{"}('a,'v)trie~{\isasymRightarrow}~'v~option{"}\isanewline
+~~~~~~~alist~::~{"}('a,'v)trie~{\isasymRightarrow}~('a~*~('a,'v)trie)list{"}\isanewline
+\isacommand{primrec}~{"}value(Trie~ov~al)~=~ov{"}\isanewline
+\isacommand{primrec}~{"}alist(Trie~ov~al)~=~al{"}%
+\begin{isamarkuptext}%
+\noindent
+Association lists come with a generic lookup function:%
+\end{isamarkuptext}%
+\isacommand{consts}~~~assoc~::~{"}('key~*~'val)list~{\isasymRightarrow}~'key~{\isasymRightarrow}~'val~option{"}\isanewline
+\isacommand{primrec}~{"}assoc~[]~x~=~None{"}\isanewline
+~~~~~~~~{"}assoc~(p\#ps)~x~=\isanewline
+~~~~~~~~~~~(let~(a,b)~=~p~in~if~a=x~then~Some~b~else~assoc~ps~x){"}%
+\begin{isamarkuptext}%
+Now we can define the lookup function for tries. It descends into the trie
+examining the letters of the search string one by one. As
+recursion on lists is simpler than on tries, let us express this as primitive
+recursion on the search string argument:%
+\end{isamarkuptext}%
+\isacommand{consts}~~~lookup~::~{"}('a,'v)trie~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'v~option{"}\isanewline
+\isacommand{primrec}~{"}lookup~t~[]~=~value~t{"}\isanewline
+~~~~~~~~{"}lookup~t~(a\#as)~=~(case~assoc~(alist~t)~a~of\isanewline
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~None~{\isasymRightarrow}~None\isanewline
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~|~Some~at~{\isasymRightarrow}~lookup~at~as){"}%
+\begin{isamarkuptext}%
+As a first simple property we prove that looking up a string in the empty
+trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
+distinguishes the two cases whether the search string is empty or not:%
+\end{isamarkuptext}%
+\isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline
+\isacommand{apply}(cases~{"}as{"},~auto)\isacommand{.}%
+\begin{isamarkuptext}%
+Things begin to get interesting with the definition of an update function
+that adds a new (string,value) pair to a trie, overwriting the old value
+associated with that string:%
+\end{isamarkuptext}%
+\isacommand{consts}~update~::~{"}('a,'v)trie~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'v~{\isasymRightarrow}~('a,'v)trie{"}\isanewline
+\isacommand{primrec}\isanewline
+~~{"}update~t~[]~~~~~v~=~Trie~(Some~v)~(alist~t){"}\isanewline
+~~{"}update~t~(a\#as)~v~=\isanewline
+~~~~~(let~tt~=~(case~assoc~(alist~t)~a~of\isanewline
+~~~~~~~~~~~~~~~~~~None~{\isasymRightarrow}~Trie~None~[]~|~Some~at~{\isasymRightarrow}~at)\isanewline
+~~~~~~in~Trie~(value~t)~((a,update~tt~as~v)\#alist~t)){"}%
+\begin{isamarkuptext}%
+\noindent
+The base case is obvious. In the recursive case the subtrie
+\isa{tt} associated with the first letter \isa{a} is extracted,
+recursively updated, and then placed in front of the association list.
+The old subtrie associated with \isa{a} is still in the association list
+but no longer accessible via \isa{assoc}. Clearly, there is room here for
+optimizations!
+
+Before we start on any proofs about \isa{update} we tell the simplifier to
+expand all \isa{let}s and to split all \isa{case}-constructs over
+options:%
+\end{isamarkuptext}%
+\isacommand{theorems}~[simp]~=~Let\_def\isanewline
+\isacommand{theorems}~[split]~=~option.split%
+\begin{isamarkuptext}%
+\noindent
+The reason becomes clear when looking (probably after a failed proof
+attempt) at the body of \isa{update}: it contains both
+\isa{let} and a case distinction over type \isa{option}.
+
+Our main goal is to prove the correct interaction of \isa{update} and
+\isa{lookup}:%
+\end{isamarkuptext}%
+\isacommand{theorem}~{"}{\isasymforall}t~v~bs.~lookup~(update~t~as~v)~bs~=\isanewline
+~~~~~~~~~~~~~~~~~~~~(if~as=bs~then~Some~v~else~lookup~t~bs){"}%
+\begin{isamarkuptxt}%
+\noindent
+Our plan is to induct on \isa{as}; hence the remaining variables are
+quantified. From the definitions it is clear that induction on either
+\isa{as} or \isa{bs} is required. The choice of \isa{as} is merely
+guided by the intuition that simplification of \isa{lookup} might be easier
+if \isa{update} has already been simplified, which can only happen if
+\isa{as} is instantiated.
+The start of the proof is completely conventional:%
+\end{isamarkuptxt}%
+\isacommand{apply}(induct\_tac~{"}as{"},~auto)%
+\begin{isamarkuptxt}%
+\noindent
+Unfortunately, this time we are left with three intimidating looking subgoals:
+\begin{isabellepar}%
+~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
+~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
+~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
+\end{isabellepar}%
+Clearly, if we want to make headway we have to instantiate \isa{bs} as
+well now. It turns out that instead of induction, case distinction
+suffices:%
+\end{isamarkuptxt}%
+\isacommand{apply}(case\_tac[!]~bs)\isanewline
+\isacommand{apply}(auto)\isacommand{.}%
+\begin{isamarkuptext}%
+\noindent
+Both \isaindex{case_tac} and \isaindex{induct_tac}
+take an optional first argument that specifies the range of subgoals they are
+applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual
+subgoal number are also allowed.
+
+This proof may look surprisingly straightforward. However, note that this
+comes at a cost: the proof script is unreadable because the
+intermediate proof states are invisible, and we rely on the (possibly
+brittle) magic of \isa{auto} (after the induction) to split the remaining
+goals up in such a way that case distinction on \isa{bs} makes sense and
+solves the proof. Part~\ref{Isar} shows you how to write readable and stable
+proofs.%
+\end{isamarkuptext}%
+\end{isabelle}%