259 No~subgoals! |
259 No~subgoals! |
260 \end{isabelle} |
260 \end{isabelle} |
261 |
261 |
262 We still need to confirm that the proof is now finished:% |
262 We still need to confirm that the proof is now finished:% |
263 \end{isamarkuptxt}% |
263 \end{isamarkuptxt}% |
264 \isacommand{{\isachardot}}% |
264 \isacommand{done}% |
265 \begin{isamarkuptext}% |
265 \begin{isamarkuptext}% |
266 \noindent\indexbold{$Isar@\texttt{.}}% |
266 \noindent\indexbold{done}% |
267 As a result of that final dot, Isabelle associates the lemma |
267 As a result of that final \isacommand{done}, Isabelle associates the lemma just proved |
268 just proved with its name. Instead of \isacommand{apply} |
268 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done} |
269 followed by a dot, you can simply write \isacommand{by}\indexbold{by}, |
269 if it is obvious from the context that the proof is finished. |
270 which we do most of the time. Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}} |
270 |
271 (as printed out after the final dot) the free variable \isa{xs} has been |
271 % Instead of \isacommand{apply} followed by a dot, you can simply write |
|
272 % \isacommand{by}\indexbold{by}, which we do most of the time. |
|
273 Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}} |
|
274 (as printed out after the final \isacommand{done}) the free variable \isa{xs} has been |
272 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in |
275 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in |
273 \S\ref{sec:variables}. |
276 \S\ref{sec:variables}. |
274 |
277 |
275 Going back to the proof of the first lemma% |
278 Going back to the proof of the first lemma% |
276 \end{isamarkuptext}% |
279 \end{isamarkuptext}% |
300 \begin{isamarkuptext}% |
303 \begin{isamarkuptext}% |
301 Abandoning the previous proof, the canonical proof procedure% |
304 Abandoning the previous proof, the canonical proof procedure% |
302 \end{isamarkuptext}% |
305 \end{isamarkuptext}% |
303 \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline |
306 \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline |
304 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
307 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
305 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}% |
308 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
309 \isacommand{done}% |
306 \begin{isamarkuptext}% |
310 \begin{isamarkuptext}% |
307 \noindent |
311 \noindent |
308 succeeds without further ado. |
312 succeeds without further ado. |
309 Now we can go back and prove the first lemma% |
313 Now we can go back and prove the first lemma% |
310 \end{isamarkuptext}% |
314 \end{isamarkuptext}% |
311 \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
315 \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
312 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
316 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
313 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}% |
317 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
318 \isacommand{done}% |
314 \begin{isamarkuptext}% |
319 \begin{isamarkuptext}% |
315 \noindent |
320 \noindent |
316 and then solve our main theorem:% |
321 and then solve our main theorem:% |
317 \end{isamarkuptext}% |
322 \end{isamarkuptext}% |
318 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
323 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
319 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
324 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
320 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}% |
325 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
326 \isacommand{done}% |
321 \begin{isamarkuptext}% |
327 \begin{isamarkuptext}% |
322 \noindent |
328 \noindent |
323 The final \isacommand{end} tells Isabelle to close the current theory because |
329 The final \isacommand{end} tells Isabelle to close the current theory because |
324 we are finished with its development:% |
330 we are finished with its development:% |
325 \end{isamarkuptext}% |
331 \end{isamarkuptext}% |