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