78 \isamarkuptrue% |
78 \isamarkuptrue% |
79 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline |
79 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline |
80 \ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline |
80 \ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline |
81 \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline |
81 \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline |
82 \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
82 \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
83 % |
83 \isamarkuptrue% |
84 \begin{isamarkuptxt}% |
84 \isamarkupfalse% |
85 \noindent |
|
86 These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} |
|
87 holds. Remember that on lists \isa{size} and \isa{length} are synonymous. |
|
88 |
|
89 The proof itself is by rule induction and afterwards automatic:% |
|
90 \end{isamarkuptxt}% |
|
91 \isamarkuptrue% |
|
92 \isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
|
93 % |
85 % |
94 \begin{isamarkuptext}% |
86 \begin{isamarkuptext}% |
95 \noindent |
87 \noindent |
96 This may seem surprising at first, and is indeed an indication of the power |
88 This may seem surprising at first, and is indeed an indication of the power |
97 of inductive definitions. But it is also quite straightforward. For example, |
89 of inductive definitions. But it is also quite straightforward. For example, |
126 \end{isamarkuptext}% |
118 \end{isamarkuptext}% |
127 \isamarkuptrue% |
119 \isamarkuptrue% |
128 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
120 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
129 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
121 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
130 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
122 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
131 % |
123 \isamarkuptrue% |
132 \begin{isamarkuptxt}% |
124 \isamarkupfalse% |
133 \noindent |
125 \isamarkupfalse% |
134 The lemma is a bit hard to read because of the coercion function |
126 \isamarkupfalse% |
135 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns |
|
136 a natural number, but subtraction on type~\isa{nat} will do the wrong thing. |
|
137 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of |
|
138 length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which |
|
139 is what remains after that prefix has been dropped from \isa{xs}. |
|
140 |
|
141 The proof is by induction on \isa{w}, with a trivial base case, and a not |
|
142 so trivial induction step. Since it is essentially just arithmetic, we do not |
|
143 discuss it.% |
|
144 \end{isamarkuptxt}% |
|
145 \isamarkuptrue% |
|
146 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
|
147 \ \isamarkupfalse% |
|
148 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
149 \isamarkupfalse% |
|
150 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}\isamarkupfalse% |
|
151 % |
127 % |
152 \begin{isamarkuptext}% |
128 \begin{isamarkuptext}% |
153 Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:% |
129 Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:% |
154 \end{isamarkuptext}% |
130 \end{isamarkuptext}% |
155 \isamarkuptrue% |
131 \isamarkuptrue% |
156 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
132 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
157 \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline |
133 \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline |
158 \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
134 \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
159 % |
135 \isamarkuptrue% |
160 \begin{isamarkuptxt}% |
136 \isamarkupfalse% |
161 \noindent |
137 \isamarkupfalse% |
162 This is proved by \isa{force} with the help of the intermediate value theorem, |
|
163 instantiated appropriately and with its first premise disposed of by lemma |
|
164 \isa{step{\isadigit{1}}}:% |
|
165 \end{isamarkuptxt}% |
|
166 \isamarkuptrue% |
|
167 \isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline |
|
168 \isamarkupfalse% |
|
169 \isacommand{by}\ force\isamarkupfalse% |
|
170 % |
138 % |
171 \begin{isamarkuptext}% |
139 \begin{isamarkuptext}% |
172 \noindent |
140 \noindent |
173 |
141 |
174 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
142 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
212 \isamarkuptrue% |
180 \isamarkuptrue% |
213 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline |
181 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline |
214 \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline |
182 \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline |
215 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline |
183 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline |
216 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
184 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
217 % |
185 \isamarkuptrue% |
218 \begin{isamarkuptxt}% |
186 \isamarkupfalse% |
219 \noindent |
187 \isamarkupfalse% |
220 The proof is by induction on \isa{w}. Structural induction would fail here |
188 \isamarkuptrue% |
221 because, as we can see from the grammar, we need to make bigger steps than |
189 \isamarkupfalse% |
222 merely appending a single letter at the front. Hence we induct on the length |
190 \isamarkupfalse% |
223 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:% |
191 \isamarkupfalse% |
224 \end{isamarkuptxt}% |
192 \isamarkuptrue% |
225 \isamarkuptrue% |
193 \isamarkupfalse% |
226 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% |
194 \isamarkupfalse% |
227 \isamarkupfalse% |
195 \isamarkupfalse% |
228 % |
196 \isamarkupfalse% |
229 \begin{isamarkuptxt}% |
197 \isamarkuptrue% |
230 \noindent |
198 \isamarkupfalse% |
231 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction |
199 \isamarkupfalse% |
232 rule to use. For details see \S\ref{sec:complete-ind} below. |
200 \isamarkuptrue% |
233 In this case the result is that we may assume the lemma already |
201 \isamarkupfalse% |
234 holds for all words shorter than \isa{w}. |
202 \isamarkuptrue% |
235 |
203 \isamarkupfalse% |
236 The proof continues with a case distinction on \isa{w}, |
204 \isamarkuptrue% |
237 on whether \isa{w} is empty or not.% |
205 \isamarkupfalse% |
238 \end{isamarkuptxt}% |
206 \isamarkupfalse% |
239 \isamarkuptrue% |
207 \isamarkuptrue% |
240 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
208 \isamarkupfalse% |
241 \ \isamarkupfalse% |
209 \isamarkupfalse% |
242 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
210 \isamarkupfalse% |
243 \isamarkupfalse% |
211 \isamarkupfalse% |
244 % |
212 \isamarkupfalse% |
245 \begin{isamarkuptxt}% |
213 \isamarkupfalse% |
246 \noindent |
214 \isamarkupfalse% |
247 Simplification disposes of the base case and leaves only a conjunction |
215 \isamarkupfalse% |
248 of two step cases to be proved: |
216 \isamarkupfalse% |
249 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}% |
|
250 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}% |
|
251 \end{isabelle} then |
|
252 \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}. |
|
253 We only consider the first case in detail. |
|
254 |
|
255 After breaking the conjunction up into two cases, we can apply |
|
256 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.% |
|
257 \end{isamarkuptxt}% |
|
258 \isamarkuptrue% |
|
259 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
|
260 \ \isamarkupfalse% |
|
261 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
262 \ \isamarkupfalse% |
|
263 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
264 \ \isamarkupfalse% |
|
265 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isamarkupfalse% |
|
266 % |
|
267 \begin{isamarkuptxt}% |
|
268 \noindent |
|
269 This yields an index \isa{i\ {\isasymle}\ length\ v} such that |
|
270 \begin{isabelle}% |
|
271 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% |
|
272 \end{isabelle} |
|
273 With the help of \isa{part{\isadigit{2}}} it follows that |
|
274 \begin{isabelle}% |
|
275 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% |
|
276 \end{isabelle}% |
|
277 \end{isamarkuptxt}% |
|
278 \ \isamarkuptrue% |
|
279 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
280 \ \ \isamarkupfalse% |
|
281 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isamarkupfalse% |
|
282 % |
|
283 \begin{isamarkuptxt}% |
|
284 \noindent |
|
285 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A} |
|
286 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},% |
|
287 \end{isamarkuptxt}% |
|
288 \ \isamarkuptrue% |
|
289 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isamarkupfalse% |
|
290 % |
|
291 \begin{isamarkuptxt}% |
|
292 \noindent |
|
293 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the |
|
294 theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}) |
|
295 after which the appropriate rule of the grammar reduces the goal |
|
296 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:% |
|
297 \end{isamarkuptxt}% |
|
298 \ \isamarkuptrue% |
|
299 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isamarkupfalse% |
|
300 % |
|
301 \begin{isamarkuptxt}% |
|
302 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:% |
|
303 \end{isamarkuptxt}% |
|
304 \ \ \isamarkuptrue% |
|
305 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
|
306 \ \isamarkupfalse% |
|
307 \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% |
|
308 % |
|
309 \begin{isamarkuptxt}% |
|
310 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:% |
|
311 \end{isamarkuptxt}% |
|
312 \isamarkuptrue% |
|
313 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
314 \isamarkupfalse% |
|
315 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
316 \isamarkupfalse% |
|
317 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
318 \isamarkupfalse% |
|
319 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
320 \ \isamarkupfalse% |
|
321 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
|
322 \isamarkupfalse% |
|
323 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline |
|
324 \isamarkupfalse% |
|
325 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
|
326 \ \isamarkupfalse% |
|
327 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
|
328 \isamarkupfalse% |
|
329 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% |
|
330 % |
217 % |
331 \begin{isamarkuptext}% |
218 \begin{isamarkuptext}% |
332 We conclude this section with a comparison of our proof with |
219 We conclude this section with a comparison of our proof with |
333 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
220 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
334 \cite[p.\ts81]{HopcroftUllman}. |
221 \cite[p.\ts81]{HopcroftUllman}. |