61 distinguishes the two cases whether the search string is empty or not:% |
61 distinguishes the two cases whether the search string is empty or not:% |
62 \end{isamarkuptext}% |
62 \end{isamarkuptext}% |
63 \isamarkuptrue% |
63 \isamarkuptrue% |
64 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline |
64 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline |
65 \isamarkupfalse% |
65 \isamarkupfalse% |
66 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
|
67 \isamarkupfalse% |
66 \isamarkupfalse% |
68 \isacommand{done}\isamarkupfalse% |
67 \isamarkupfalse% |
69 % |
68 % |
70 \begin{isamarkuptext}% |
69 \begin{isamarkuptext}% |
71 Things begin to get interesting with the definition of an update function |
70 Things begin to get interesting with the definition of an update function |
72 that adds a new (string, value) pair to a trie, overwriting the old value |
71 that adds a new (string, value) pair to a trie, overwriting the old value |
73 associated with that string:% |
72 associated with that string:% |
108 \isa{lookup}:% |
107 \isa{lookup}:% |
109 \end{isamarkuptext}% |
108 \end{isamarkuptext}% |
110 \isamarkuptrue% |
109 \isamarkuptrue% |
111 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline |
110 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline |
112 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as{\isacharequal}bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
111 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as{\isacharequal}bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
113 % |
|
114 \begin{isamarkuptxt}% |
|
115 \noindent |
|
116 Our plan is to induct on \isa{as}; hence the remaining variables are |
|
117 quantified. From the definitions it is clear that induction on either |
|
118 \isa{as} or \isa{bs} is required. The choice of \isa{as} is |
|
119 guided by the intuition that simplification of \isa{lookup} might be easier |
|
120 if \isa{update} has already been simplified, which can only happen if |
|
121 \isa{as} is instantiated. |
|
122 The start of the proof is conventional:% |
|
123 \end{isamarkuptxt}% |
|
124 \isamarkuptrue% |
112 \isamarkuptrue% |
125 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
113 \isamarkupfalse% |
126 % |
|
127 \begin{isamarkuptxt}% |
|
128 \noindent |
|
129 Unfortunately, this time we are left with three intimidating looking subgoals: |
|
130 \begin{isabelle} |
|
131 ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline |
|
132 ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline |
|
133 ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs |
|
134 \end{isabelle} |
|
135 Clearly, if we want to make headway we have to instantiate \isa{bs} as |
|
136 well now. It turns out that instead of induction, case distinction |
|
137 suffices:% |
|
138 \end{isamarkuptxt}% |
|
139 \isamarkuptrue% |
114 \isamarkuptrue% |
140 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}\isanewline |
|
141 \isamarkupfalse% |
115 \isamarkupfalse% |
142 \isacommand{done}\isamarkupfalse% |
116 \isamarkupfalse% |
143 % |
117 % |
144 \begin{isamarkuptext}% |
118 \begin{isamarkuptext}% |
145 \noindent |
119 \noindent |
146 \index{subgoal numbering}% |
120 \index{subgoal numbering}% |
147 All methods ending in \isa{tac} take an optional first argument that |
121 All methods ending in \isa{tac} take an optional first argument that |