3 \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
6 HOL already has a predefined theory of lists called \isa{List} ---
7 \isa{ToyList} is merely a small fragment of it chosen as an example. In
8 contrast to what is recommended in \S\ref{sec:Basic:Theories},
9 \isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
10 theory that contains pretty much everything but lists, thus avoiding
11 ambiguities caused by defining lists twice.%
13 \isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline
14 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}%
15 \begin{isamarkuptext}%
17 The datatype\index{*datatype} \isaindexbold{list} introduces two
18 constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
19 empty~list and the operator that adds an element to the front of a list. For
20 example, the term \isa{Cons True (Cons False Nil)} is a value of
21 type \isa{bool\ list}, namely the list with the elements \isa{True} and
22 \isa{False}. Because this notation becomes unwieldy very quickly, the
23 datatype declaration is annotated with an alternative syntax: instead of
24 \isa{Nil} and \isa{Cons x xs} we can write
25 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
26 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
27 alternative syntax is the standard syntax. Thus the list \isa{Cons True
28 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
29 \isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
30 the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
31 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
34 Syntax annotations are a powerful but completely optional feature. You
35 could drop them from theory \isa{ToyList} and go back to the identifiers
36 \isa{Nil} and \isa{Cons}. However, lists are such a
38 that their syntax is highly customized. We recommend that novices should
39 not use syntax annotations in their own theories.
41 Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
43 \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 \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
45 \begin{isamarkuptext}%
47 In contrast to ML, Isabelle insists on explicit declarations of all functions
48 (keyword \isacommand{consts}). (Apart from the declaration-before-use
49 restriction, the order of items in a theory file is unconstrained.) Function
50 \isa{op\ {\isacharat}} is annotated with concrete syntax too. Instead of the prefix
51 syntax \isa{app xs ys} the infix
52 \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
53 form. Both functions are defined recursively:%
55 \isacommand{primrec}\isanewline
56 {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequote}\isanewline
57 {\isachardoublequote}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequote}\isanewline
59 \isacommand{primrec}\isanewline
60 {\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
61 {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
62 \begin{isamarkuptext}%
64 The equations for \isa{op\ {\isacharat}} and \isa{rev} hardly need comments:
65 \isa{op\ {\isacharat}} appends two lists and \isa{rev} reverses a list. The keyword
66 \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
67 particularly primitive kind where each recursive call peels off a datatype
68 constructor from one of the arguments. Thus the
69 recursion always terminates, i.e.\ the function is \bfindex{total}.
71 The termination requirement is absolutely essential in HOL, a logic of total
72 functions. If we were to drop it, inconsistencies would quickly arise: the
73 ``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
75 % However, this is a subtle issue that we cannot discuss here further.
78 As we have indicated, the desire for total functions is not a gratuitously
79 imposed restriction but an essential characteristic of HOL. It is only
80 because of totality that reasoning in HOL is comparatively easy. More
81 generally, the philosophy in HOL is not to allow arbitrary axioms (such as
82 function definitions whose totality has not been proved) because they
83 quickly lead to inconsistencies. Instead, fixed constructs for introducing
84 types and functions are offered (such as \isacommand{datatype} and
85 \isacommand{primrec}) which are guaranteed to preserve consistency.
88 A remark about syntax. The textual definition of a theory follows a fixed
89 syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
90 Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
91 Embedded in this syntax are the types and formulae of HOL, whose syntax is
92 extensible, e.g.\ by new user-defined infix operators
93 (see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
94 HOL-specific (terms and types) should be enclosed in
95 \texttt{"}\dots\texttt{"}.
96 To lessen this burden, quotation marks around a single identifier can be
97 dropped, unless the identifier happens to be a keyword, as in%
99 \isacommand{consts}\ {\isachardoublequote}end{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
100 \begin{isamarkuptext}%
102 When Isabelle prints a syntax error message, it refers to the HOL syntax as
103 the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
106 \section{An introductory proof}
107 \label{sec:intro-proof}
109 Assuming you have input the declarations and definitions of \texttt{ToyList}
110 presented so far, we are ready to prove a few simple theorems. This will
111 illustrate not just the basic proof commands but also the typical proof
114 \subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}}
116 Our goal is to show that reversing a list twice produces the original
117 list. The input line%
119 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
120 \begin{isamarkuptxt}%
121 \index{*theorem|bold}\index{*simp (attribute)|bold}
124 establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
126 gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
129 and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
130 proved) as a simplification rule, i.e.\ all future proofs involving
131 simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
134 The name and the simplification attribute are optional.
136 Isabelle's response is to print
138 proof(prove):~step~0\isanewline
140 goal~(theorem~rev\_rev):\isanewline
141 rev~(rev~xs)~=~xs\isanewline
142 ~1.~rev~(rev~xs)~=~xs
144 The first three lines tell us that we are 0 steps into the proof of
145 theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
146 initial lines in this tutorial. The remaining lines display the current
148 Until we have finished a proof, the proof state always looks like this:
151 ~1.~$G\sb{1}$\isanewline
152 ~~\vdots~~\isanewline
156 is the overall goal that we are trying to prove, and the numbered lines
157 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
158 establish $G$. At \isa{step\ \isadigit{0}} there is only one subgoal, which is
159 identical with the overall goal. Normally $G$ is constant and only serves as
160 a reminder. Hence we rarely show it in this tutorial.
162 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
163 defined functions are best established by induction. In this case there is
164 not much choice except to induct on \isa{xs}:%
166 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
167 \begin{isamarkuptxt}%
168 \noindent\index{*induct_tac}%
169 This tells Isabelle to perform induction on variable \isa{xs}. The suffix
170 \isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
171 By default, induction acts on the first subgoal. The new proof state contains
172 two subgoals, namely the base case (\isa{Nil}) and the induction step
175 ~1.~rev~(rev~[])~=~[]\isanewline
176 ~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
179 The induction step is an example of the general format of a subgoal:
181 ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
183 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
184 ignored most of the time, or simply treated as a list of variables local to
185 this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
186 The {\it assumptions} are the local assumptions for this subgoal and {\it
187 conclusion} is the actual proposition to be proved. Typical proof steps
188 that add new assumptions are induction or case distinction. In our example
189 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
190 are multiple assumptions, they are enclosed in the bracket pair
191 \indexboldpos{\isasymlbrakk}{$Isabrl} and
192 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
194 Let us try to solve both goals automatically:%
196 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
197 \begin{isamarkuptxt}%
199 This command tells Isabelle to apply a proof strategy called
200 \isa{auto} to all subgoals. Essentially, \isa{auto} tries to
201 ``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
202 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
203 of subgoal~2 becomes the new subgoal~1:
205 ~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
207 In order to simplify this subgoal further, a lemma suggests itself.%
210 \isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}}
212 \begin{isamarkuptext}%
213 After abandoning the above proof attempt\indexbold{abandon
214 proof}\indexbold{proof!abandon} (at the shell level type
215 \isacommand{oops}\indexbold{*oops}) we start a new proof:%
217 \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}%
218 \begin{isamarkuptxt}%
219 \noindent The keywords \isacommand{theorem}\index{*theorem} and
220 \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
221 the importance we attach to a proposition. In general, we use the words
222 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
225 There are two variables that we could induct on: \isa{xs} and
226 \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
227 the first argument, \isa{xs} is the correct one:%
229 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
230 \begin{isamarkuptxt}%
232 This time not even the base case is solved automatically:%
234 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
235 \begin{isamarkuptxt}%
237 ~1.~rev~ys~=~rev~ys~@~[]\isanewline
240 Again, we need to abandon this proof attempt and prove another simple lemma first.
241 In the future the step of abandoning an incomplete proof before embarking on
242 the proof of a lemma usually remains implicit.%
245 \isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
247 \begin{isamarkuptext}%
248 This time the canonical proof procedure%
250 \isacommand{lemma}\ app{\isacharunderscore}Nil\isadigit{2}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
251 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
252 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
253 \begin{isamarkuptxt}%
255 leads to the desired message \isa{No\ subgoals{\isacharbang}}:
257 xs~@~[]~=~xs\isanewline
261 We still need to confirm that the proof is now finished:%
263 \isacommand{{\isachardot}}%
264 \begin{isamarkuptext}%
265 \noindent\indexbold{$Isar@\texttt{.}}%
266 As a result of that final dot, Isabelle associates the lemma
267 just proved with its name. Instead of \isacommand{apply}
268 followed by a dot, you can simply write \isacommand{by}\indexbold{by},
269 which we do most of the time. Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
270 (as printed out after the final dot) the free variable \isa{xs} has been
271 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
272 \S\ref{sec:variables}.
274 Going back to the proof of the first lemma%
276 \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
277 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
278 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
279 \begin{isamarkuptxt}%
281 we find that this time \isa{auto} solves the base case, but the
282 induction step merely simplifies to
284 ~1.~{\isasymAnd}a~list.\isanewline
285 ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
286 ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
288 Now we need to remember that \isa{{\isacharat}} associates to the right, and that
289 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{\isadigit{6}\isadigit{5}}
290 in their \isacommand{infixr} annotation). Thus the conclusion really is
292 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
294 and the missing lemma is associativity of \isa{{\isacharat}}.%
297 \isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}}
299 \begin{isamarkuptext}%
300 Abandoning the previous proof, the canonical proof procedure%
302 \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
303 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
304 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
305 \begin{isamarkuptext}%
307 succeeds without further ado.
308 Now we can go back and prove the first lemma%
310 \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
311 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
312 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
313 \begin{isamarkuptext}%
315 and then solve our main theorem:%
317 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
318 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
319 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
320 \begin{isamarkuptext}%
322 The final \isacommand{end} tells Isabelle to close the current theory because
323 we are finished with its development:%
325 \isacommand{end}\isanewline
329 %%% TeX-master: "root"