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

--- a/doc-src/TutorialI/Trie/document/Trie.tex	Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Wed May 25 09:04:24 2005 +0200
@@ -63,8 +63,9 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline
 \isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Things begin to get interesting with the definition of an update function
@@ -109,11 +110,36 @@
 \isamarkuptrue%
 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as{\isacharequal}bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\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 
+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 conventional:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+Unfortunately, this time we are left with three intimidating looking subgoals:
+\begin{isabelle}
+~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{isabelle}
+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}%
+\isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -158,28 +184,16 @@
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isanewline
-\isanewline
-\isanewline
-\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isanewline
-\isamarkupfalse%
-\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isanewline
-\isanewline
-\isanewline
-\isamarkupfalse%
-\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
@@ -188,14 +202,16 @@
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%