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