equal
deleted
inserted
replaced
10 \isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a |
10 \isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a |
11 theory that contains pretty much everything but lists, thus avoiding |
11 theory that contains pretty much everything but lists, thus avoiding |
12 ambiguities caused by defining lists twice.% |
12 ambiguities caused by defining lists twice.% |
13 \end{isamarkuptext}% |
13 \end{isamarkuptext}% |
14 \isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline |
14 \isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline |
15 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}% |
15 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}% |
16 \begin{isamarkuptext}% |
16 \begin{isamarkuptext}% |
17 \noindent |
17 \noindent |
18 The datatype\index{*datatype} \isaindexbold{list} introduces two |
18 The datatype\index{*datatype} \isaindexbold{list} introduces two |
19 constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the |
19 constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the |
20 empty~list and the operator that adds an element to the front of a list. For |
20 empty~list and the operator that adds an element to the front of a list. For |
39 that their syntax is highly customized. We recommend that novices should |
39 that their syntax is highly customized. We recommend that novices should |
40 not use syntax annotations in their own theories. |
40 not use syntax annotations in their own theories. |
41 \end{warn} |
41 \end{warn} |
42 Next, two functions \isa{app} and \isaindexbold{rev} are declared:% |
42 Next, two functions \isa{app} and \isaindexbold{rev} are declared:% |
43 \end{isamarkuptext}% |
43 \end{isamarkuptext}% |
44 \isacommand{consts}\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharat}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}\isanewline |
44 \isacommand{consts}\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharat}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isanewline |
45 \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}% |
45 \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}% |
46 \begin{isamarkuptext}% |
46 \begin{isamarkuptext}% |
47 \noindent |
47 \noindent |
48 In contrast to ML, Isabelle insists on explicit declarations of all functions |
48 In contrast to ML, Isabelle insists on explicit declarations of all functions |
49 (keyword \isacommand{consts}). (Apart from the declaration-before-use |
49 (keyword \isacommand{consts}). (Apart from the declaration-before-use |
154 ~$n$.~$G\sb{n}$ |
154 ~$n$.~$G\sb{n}$ |
155 \end{isabelle} |
155 \end{isabelle} |
156 where $G$ |
156 where $G$ |
157 is the overall goal that we are trying to prove, and the numbered lines |
157 is the overall goal that we are trying to prove, and the numbered lines |
158 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to |
158 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to |
159 establish $G$. At \isa{step\ \isadigit{0}} there is only one subgoal, which is |
159 establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is |
160 identical with the overall goal. Normally $G$ is constant and only serves as |
160 identical with the overall goal. Normally $G$ is constant and only serves as |
161 a reminder. Hence we rarely show it in this tutorial. |
161 a reminder. Hence we rarely show it in this tutorial. |
162 |
162 |
163 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively |
163 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively |
164 defined functions are best established by induction. In this case there is |
164 defined functions are best established by induction. In this case there is |
246 \isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}} |
246 \isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}} |
247 % |
247 % |
248 \begin{isamarkuptext}% |
248 \begin{isamarkuptext}% |
249 This time the canonical proof procedure% |
249 This time the canonical proof procedure% |
250 \end{isamarkuptext}% |
250 \end{isamarkuptext}% |
251 \isacommand{lemma}\ app{\isacharunderscore}Nil\isadigit{2}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
251 \isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
252 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
252 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
253 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% |
253 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% |
254 \begin{isamarkuptxt}% |
254 \begin{isamarkuptxt}% |
255 \noindent |
255 \noindent |
256 leads to the desired message \isa{No\ subgoals{\isacharbang}}: |
256 leads to the desired message \isa{No\ subgoals{\isacharbang}}: |
268 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done} |
268 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done} |
269 if it is obvious from the context that the proof is finished. |
269 if it is obvious from the context that the proof is finished. |
270 |
270 |
271 % Instead of \isacommand{apply} followed by a dot, you can simply write |
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. |
272 % \isacommand{by}\indexbold{by}, which we do most of the time. |
273 Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}} |
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 |
274 (as printed out after the final \isacommand{done}) the free variable \isa{xs} has been |
275 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in |
275 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in |
276 \S\ref{sec:variables}. |
276 \S\ref{sec:variables}. |
277 |
277 |
278 Going back to the proof of the first lemma% |
278 Going back to the proof of the first lemma% |
288 ~1.~{\isasymAnd}a~list.\isanewline |
288 ~1.~{\isasymAnd}a~list.\isanewline |
289 ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline |
289 ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline |
290 ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[] |
290 ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[] |
291 \end{isabelle} |
291 \end{isabelle} |
292 Now we need to remember that \isa{{\isacharat}} associates to the right, and that |
292 Now we need to remember that \isa{{\isacharat}} associates to the right, and that |
293 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{\isadigit{6}\isadigit{5}} |
293 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}} |
294 in their \isacommand{infixr} annotation). Thus the conclusion really is |
294 in their \isacommand{infixr} annotation). Thus the conclusion really is |
295 \begin{isabelle} |
295 \begin{isabelle} |
296 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[])) |
296 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[])) |
297 \end{isabelle} |
297 \end{isabelle} |
298 and the missing lemma is associativity of \isa{{\isacharat}}.% |
298 and the missing lemma is associativity of \isa{{\isacharat}}.% |