3 \def\isabellecontext{ToyList}%
4 \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
7 HOL already has a predefined theory of lists called \isa{List} ---
8 \isa{ToyList} is merely a small fragment of it chosen as an example. In
9 contrast to what is recommended in \S\ref{sec:Basic:Theories},
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
12 ambiguities caused by defining lists twice.%
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}%
16 \begin{isamarkuptext}%
18 The datatype\index{*datatype} \isaindexbold{list} introduces two
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
21 example, the term \isa{Cons True (Cons False Nil)} is a value of
22 type \isa{bool\ list}, namely the list with the elements \isa{True} and
23 \isa{False}. Because this notation becomes unwieldy very quickly, the
24 datatype declaration is annotated with an alternative syntax: instead of
25 \isa{Nil} and \isa{Cons x xs} we can write
26 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
27 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
28 alternative syntax is the standard syntax. Thus the list \isa{Cons True
29 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
30 \isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
31 the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
32 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
33 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
36 Syntax annotations are a powerful but optional feature. You
37 could drop them from theory \isa{ToyList} and go back to the identifiers
38 \isa{Nil} and \isa{Cons}.
39 We recommend that novices avoid using
40 syntax annotations in their own theories.
42 Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
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}%
46 \begin{isamarkuptext}%
48 In contrast to many functional programming languages,
49 Isabelle insists on explicit declarations of all functions
50 (keyword \isacommand{consts}). Apart from the declaration-before-use
51 restriction, the order of items in a theory file is unconstrained. Function
52 \isa{app} is annotated with concrete syntax too. Instead of the
53 prefix syntax \isa{app\ xs\ ys} the infix
54 \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
55 form. Both functions are defined recursively:%
57 \isacommand{primrec}\isanewline
58 {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequote}\isanewline
59 {\isachardoublequote}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequote}\isanewline
61 \isacommand{primrec}\isanewline
62 {\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
63 {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
64 \begin{isamarkuptext}%
66 The equations for \isa{app} and \isa{rev} hardly need comments:
67 \isa{app} appends two lists and \isa{rev} reverses a list. The
68 keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is
69 of a particularly primitive kind where each recursive call peels off a datatype
70 constructor from one of the arguments. Thus the
71 recursion always terminates, i.e.\ the function is \textbf{total}.
72 \index{total function}
74 The termination requirement is absolutely essential in HOL, a logic of total
75 functions. If we were to drop it, inconsistencies would quickly arise: the
76 ``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
78 % However, this is a subtle issue that we cannot discuss here further.
81 As we have indicated, the requirement for total functions is not a gratuitous
82 restriction but an essential characteristic of HOL\@. It is only
83 because of totality that reasoning in HOL is comparatively easy. More
84 generally, the philosophy in HOL is not to allow arbitrary axioms (such as
85 function definitions whose totality has not been proved) because they
86 quickly lead to inconsistencies. Instead, fixed constructs for introducing
87 types and functions are offered (such as \isacommand{datatype} and
88 \isacommand{primrec}) which are guaranteed to preserve consistency.
91 A remark about syntax. The textual definition of a theory follows a fixed
92 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
93 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
94 Embedded in this syntax are the types and formulae of HOL, whose syntax is
95 extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
96 To distinguish the two levels, everything
97 HOL-specific (terms and types) should be enclosed in
98 \texttt{"}\dots\texttt{"}.
99 To lessen this burden, quotation marks around a single identifier can be
100 dropped, unless the identifier happens to be a keyword, as in%
102 \isacommand{consts}\ {\isachardoublequote}end{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
103 \begin{isamarkuptext}%
105 When Isabelle prints a syntax error message, it refers to the HOL syntax as
106 the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
109 \section{An Introductory Proof}
110 \label{sec:intro-proof}
112 Assuming you have input the declarations and definitions of \texttt{ToyList}
113 presented so far, we are ready to prove a few simple theorems. This will
114 illustrate not just the basic proof commands but also the typical proof
117 \subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
119 Our goal is to show that reversing a list twice produces the original
120 list. The input line%
122 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
123 \begin{isamarkuptxt}%
124 \index{*theorem|bold}\index{*simp (attribute)|bold}
126 does several things. It
129 establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
131 gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
134 and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
135 proved) as a simplification rule, i.e.\ all future proofs involving
136 simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
139 The name and the simplification attribute are optional.
141 Isabelle's response is to print
143 proof(prove):~step~0\isanewline
145 goal~(theorem~rev\_rev):\isanewline
146 rev~(rev~xs)~=~xs\isanewline
147 ~1.~rev~(rev~xs)~=~xs
149 The first three lines tell us that we are 0 steps into the proof of
150 theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
151 initial lines in this tutorial. The remaining lines display the current
153 Until we have finished a proof, the proof state always looks like this:
156 ~1.~$G\sb{1}$\isanewline
157 ~~\vdots~~\isanewline
161 is the overall goal that we are trying to prove, and the numbered lines
162 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
163 establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
164 identical with the overall goal. Normally $G$ is constant and only serves as
165 a reminder. Hence we rarely show it in this tutorial.
167 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
168 defined functions are best established by induction. In this case there is
169 not much choice except to induct on \isa{xs}:%
171 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
172 \begin{isamarkuptxt}%
173 \noindent\index{*induct_tac}%
174 This tells Isabelle to perform induction on variable \isa{xs}. The suffix
175 \isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
176 By default, induction acts on the first subgoal. The new proof state contains
177 two subgoals, namely the base case (\isa{Nil}) and the induction step
180 \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
181 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
182 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
185 The induction step is an example of the general format of a subgoal:
187 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
188 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
189 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
190 ignored most of the time, or simply treated as a list of variables local to
191 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
192 The {\it assumptions} are the local assumptions for this subgoal and {\it
193 conclusion} is the actual proposition to be proved. Typical proof steps
194 that add new assumptions are induction or case distinction. In our example
195 the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
196 are multiple assumptions, they are enclosed in the bracket pair
197 \indexboldpos{\isasymlbrakk}{$Isabrl} and
198 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
200 Let us try to solve both goals automatically:%
202 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
203 \begin{isamarkuptxt}%
205 This command tells Isabelle to apply a proof strategy called
206 \isa{auto} to all subgoals. Essentially, \isa{auto} tries to
207 simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
208 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
209 of subgoal~2 becomes the new subgoal~1:
211 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
212 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
214 In order to simplify this subgoal further, a lemma suggests itself.%
217 \isamarkupsubsubsection{First Lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
220 \begin{isamarkuptext}%
221 After abandoning the above proof attempt\indexbold{abandon
222 proof}\indexbold{proof!abandon} (at the shell level type
223 \isacommand{oops}\indexbold{*oops}) we start a new proof:%
225 \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}%
226 \begin{isamarkuptxt}%
227 \noindent The keywords \isacommand{theorem}\index{*theorem} and
228 \isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
229 the importance we attach to a proposition. Therefore we use the words
230 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
231 interchangeably, too.
233 There are two variables that we could induct on: \isa{xs} and
234 \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
235 the first argument, \isa{xs} is the correct one:%
237 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
238 \begin{isamarkuptxt}%
240 This time not even the base case is solved automatically:%
242 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
243 \begin{isamarkuptxt}%
245 \ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%
247 Again, we need to abandon this proof attempt and prove another simple lemma
248 first. In the future the step of abandoning an incomplete proof before
249 embarking on the proof of a lemma usually remains implicit.%
252 \isamarkupsubsubsection{Second Lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
255 \begin{isamarkuptext}%
256 This time the canonical proof procedure%
258 \isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
259 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
260 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
261 \begin{isamarkuptxt}%
263 leads to the desired message \isa{No\ subgoals{\isacharbang}}:
265 xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
266 No\ subgoals{\isacharbang}%
268 We still need to confirm that the proof is now finished:%
271 \begin{isamarkuptext}%
272 \noindent\indexbold{done}%
273 As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
274 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
275 if it is obvious from the context that the proof is finished.
277 % Instead of \isacommand{apply} followed by a dot, you can simply write
278 % \isacommand{by}\indexbold{by}, which we do most of the time.
279 Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
280 as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
281 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
282 \S\ref{sec:variables}.
284 Going back to the proof of the first lemma%
286 \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
287 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
288 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
289 \begin{isamarkuptxt}%
291 we find that this time \isa{auto} solves the base case, but the
292 induction step merely simplifies to
294 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
295 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline
296 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}%
298 Now we need to remember that \isa{{\isacharat}} associates to the right, and that
299 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
300 in their \isacommand{infixr} annotation). Thus the conclusion really is
302 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
304 and the missing lemma is associativity of \isa{{\isacharat}}.%
307 \isamarkupsubsubsection{Third Lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
310 \begin{isamarkuptext}%
311 Abandoning the previous proof, the canonical proof procedure%
313 \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
314 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
315 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
317 \begin{isamarkuptext}%
319 succeeds without further ado.
320 Now we can prove the first lemma%
322 \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
323 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
324 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
326 \begin{isamarkuptext}%
328 and then prove our main theorem:%
330 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
331 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
332 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
334 \begin{isamarkuptext}%
336 The final \isacommand{end} tells Isabelle to close the current theory because
337 we are finished with its development:%
339 \isacommand{end}\isanewline
343 %%% TeX-master: "root"