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
|
12327
|
16 |
The datatype\index{datatype@\isacommand {datatype} (command)}
|
|
17 |
\tydx{list} introduces two
|
11428
|
18 |
constructors \cdx{Nil} and \cdx{Cons}, the
|
9541
|
19 |
empty~list and the operator that adds an element to the front of a list. For
|
9792
|
20 |
example, the term \isa{Cons True (Cons False Nil)} is a value of
|
|
21 |
type @{typ"bool list"}, namely the list with the elements @{term"True"} and
|
11450
|
22 |
@{term"False"}. Because this notation quickly becomes unwieldy, the
|
8745
|
23 |
datatype declaration is annotated with an alternative syntax: instead of
|
9792
|
24 |
@{term[source]Nil} and \isa{Cons x xs} we can write
|
|
25 |
@{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
|
9541
|
26 |
@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
|
11450
|
27 |
alternative syntax is the familiar one. Thus the list \isa{Cons True
|
9541
|
28 |
(Cons False Nil)} becomes @{term"True # False # []"}. The annotation
|
11428
|
29 |
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
|
|
30 |
means that @{text"#"} associates to
|
11450
|
31 |
the right: the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
|
9792
|
32 |
and not as @{text"(x # y) # z"}.
|
10971
|
33 |
The @{text 65} is the priority of the infix @{text"#"}.
|
8745
|
34 |
|
|
35 |
\begin{warn}
|
13191
|
36 |
Syntax annotations can be powerful, but they are difficult to master and
|
11456
|
37 |
are never necessary. You
|
9792
|
38 |
could drop them from theory @{text"ToyList"} and go back to the identifiers
|
10795
|
39 |
@{term[source]Nil} and @{term[source]Cons}.
|
11456
|
40 |
Novices should avoid using
|
10795
|
41 |
syntax annotations in their own theories.
|
8745
|
42 |
\end{warn}
|
11428
|
43 |
Next, two functions @{text"app"} and \cdx{rev} are declared:
|
8745
|
44 |
*}
|
|
45 |
|
10236
|
46 |
consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
|
|
47 |
rev :: "'a list \<Rightarrow> 'a list";
|
8745
|
48 |
|
|
49 |
text{*
|
|
50 |
\noindent
|
10971
|
51 |
In contrast to many functional programming languages,
|
|
52 |
Isabelle insists on explicit declarations of all functions
|
11456
|
53 |
(keyword \commdx{consts}). Apart from the declaration-before-use
|
10971
|
54 |
restriction, the order of items in a theory file is unconstrained. Function
|
10790
|
55 |
@{text"app"} is annotated with concrete syntax too. Instead of the
|
|
56 |
prefix syntax @{text"app xs ys"} the infix
|
9541
|
57 |
@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
|
8745
|
58 |
form. Both functions are defined recursively:
|
|
59 |
*}
|
|
60 |
|
|
61 |
primrec
|
|
62 |
"[] @ ys = ys"
|
|
63 |
"(x # xs) @ ys = x # (xs @ ys)";
|
|
64 |
|
|
65 |
primrec
|
|
66 |
"rev [] = []"
|
|
67 |
"rev (x # xs) = (rev xs) @ (x # [])";
|
|
68 |
|
|
69 |
text{*
|
11456
|
70 |
\noindent\index{*rev (constant)|(}\index{append function|(}
|
10790
|
71 |
The equations for @{text"app"} and @{term"rev"} hardly need comments:
|
|
72 |
@{text"app"} appends two lists and @{term"rev"} reverses a list. The
|
11428
|
73 |
keyword \commdx{primrec} indicates that the recursion is
|
10790
|
74 |
of a particularly primitive kind where each recursive call peels off a datatype
|
8771
|
75 |
constructor from one of the arguments. Thus the
|
10654
|
76 |
recursion always terminates, i.e.\ the function is \textbf{total}.
|
11428
|
77 |
\index{functions!total}
|
8745
|
78 |
|
|
79 |
The termination requirement is absolutely essential in HOL, a logic of total
|
|
80 |
functions. If we were to drop it, inconsistencies would quickly arise: the
|
|
81 |
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
|
|
82 |
$f(n)$ on both sides.
|
|
83 |
% However, this is a subtle issue that we cannot discuss here further.
|
|
84 |
|
|
85 |
\begin{warn}
|
11456
|
86 |
As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
|
8745
|
87 |
because of totality that reasoning in HOL is comparatively easy. More
|
11456
|
88 |
generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
|
8745
|
89 |
function definitions whose totality has not been proved) because they
|
|
90 |
quickly lead to inconsistencies. Instead, fixed constructs for introducing
|
|
91 |
types and functions are offered (such as \isacommand{datatype} and
|
|
92 |
\isacommand{primrec}) which are guaranteed to preserve consistency.
|
|
93 |
\end{warn}
|
|
94 |
|
11456
|
95 |
\index{syntax}%
|
8745
|
96 |
A remark about syntax. The textual definition of a theory follows a fixed
|
10971
|
97 |
syntax with keywords like \isacommand{datatype} and \isacommand{end}.
|
|
98 |
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
|
8745
|
99 |
Embedded in this syntax are the types and formulae of HOL, whose syntax is
|
12631
|
100 |
extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
|
10971
|
101 |
To distinguish the two levels, everything
|
8745
|
102 |
HOL-specific (terms and types) should be enclosed in
|
|
103 |
\texttt{"}\dots\texttt{"}.
|
|
104 |
To lessen this burden, quotation marks around a single identifier can be
|
|
105 |
dropped, unless the identifier happens to be a keyword, as in
|
|
106 |
*}
|
|
107 |
|
10236
|
108 |
consts "end" :: "'a list \<Rightarrow> 'a"
|
8745
|
109 |
|
|
110 |
text{*\noindent
|
|
111 |
When Isabelle prints a syntax error message, it refers to the HOL syntax as
|
11456
|
112 |
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
|
8745
|
113 |
|
|
114 |
|
10885
|
115 |
\section{An Introductory Proof}
|
8745
|
116 |
\label{sec:intro-proof}
|
|
117 |
|
|
118 |
Assuming you have input the declarations and definitions of \texttt{ToyList}
|
|
119 |
presented so far, we are ready to prove a few simple theorems. This will
|
|
120 |
illustrate not just the basic proof commands but also the typical proof
|
|
121 |
process.
|
|
122 |
|
11457
|
123 |
\subsubsection*{Main Goal.}
|
8745
|
124 |
|
|
125 |
Our goal is to show that reversing a list twice produces the original
|
11456
|
126 |
list.
|
8745
|
127 |
*}
|
|
128 |
|
|
129 |
theorem rev_rev [simp]: "rev(rev xs) = xs";
|
|
130 |
|
11428
|
131 |
txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
|
10795
|
132 |
\noindent
|
11456
|
133 |
This \isacommand{theorem} command does several things:
|
8745
|
134 |
\begin{itemize}
|
|
135 |
\item
|
11456
|
136 |
It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}.
|
8745
|
137 |
\item
|
11456
|
138 |
It gives that theorem the name @{text"rev_rev"}, for later reference.
|
8745
|
139 |
\item
|
11456
|
140 |
It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
|
9792
|
141 |
simplification will replace occurrences of @{term"rev(rev xs)"} by
|
|
142 |
@{term"xs"}.
|
11457
|
143 |
\end{itemize}
|
8745
|
144 |
The name and the simplification attribute are optional.
|
12332
|
145 |
Isabelle's response is to print the initial proof state consisting
|
|
146 |
of some header information (like how many subgoals there are) followed by
|
13868
|
147 |
@{subgoals[display,indent=0]}
|
12332
|
148 |
For compactness reasons we omit the header in this tutorial.
|
|
149 |
Until we have finished a proof, the \rmindex{proof state} proper
|
|
150 |
always looks like this:
|
9723
|
151 |
\begin{isabelle}
|
8745
|
152 |
~1.~$G\sb{1}$\isanewline
|
|
153 |
~~\vdots~~\isanewline
|
|
154 |
~$n$.~$G\sb{n}$
|
9723
|
155 |
\end{isabelle}
|
13868
|
156 |
The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
|
|
157 |
that we need to prove to establish the main goal.\index{subgoals}
|
|
158 |
Initially there is only one subgoal, which is identical with the
|
|
159 |
main goal. (If you always want to see the main goal as well,
|
|
160 |
set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
|
|
161 |
--- this flag used to be set by default.)
|
8745
|
162 |
|
9792
|
163 |
Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
|
8745
|
164 |
defined functions are best established by induction. In this case there is
|
11428
|
165 |
nothing obvious except induction on @{term"xs"}:
|
8745
|
166 |
*}
|
|
167 |
|
|
168 |
apply(induct_tac xs);
|
|
169 |
|
11428
|
170 |
txt{*\noindent\index{*induct_tac (method)}%
|
9792
|
171 |
This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
|
11428
|
172 |
@{term"tac"} stands for \textbf{tactic},\index{tactics}
|
|
173 |
a synonym for ``theorem proving function''.
|
8745
|
174 |
By default, induction acts on the first subgoal. The new proof state contains
|
9792
|
175 |
two subgoals, namely the base case (@{term[source]Nil}) and the induction step
|
|
176 |
(@{term[source]Cons}):
|
10971
|
177 |
@{subgoals[display,indent=0,margin=65]}
|
8745
|
178 |
|
11456
|
179 |
The induction step is an example of the general format of a subgoal:\index{subgoals}
|
9723
|
180 |
\begin{isabelle}
|
12327
|
181 |
~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
|
10328
|
182 |
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
|
8745
|
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
|
10302
|
185 |
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
|
11456
|
186 |
The {\it assumptions}\index{assumptions!of subgoal}
|
|
187 |
are the local assumptions for this subgoal and {\it
|
|
188 |
conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.
|
|
189 |
Typical proof steps
|
|
190 |
that add new assumptions are induction and case distinction. In our example
|
9541
|
191 |
the only assumption is the induction hypothesis @{term"rev (rev list) =
|
9792
|
192 |
list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
|
8745
|
193 |
are multiple assumptions, they are enclosed in the bracket pair
|
|
194 |
\indexboldpos{\isasymlbrakk}{$Isabrl} and
|
|
195 |
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
|
|
196 |
|
|
197 |
Let us try to solve both goals automatically:
|
|
198 |
*}
|
|
199 |
|
|
200 |
apply(auto);
|
|
201 |
|
|
202 |
txt{*\noindent
|
|
203 |
This command tells Isabelle to apply a proof strategy called
|
9792
|
204 |
@{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
|
10978
|
205 |
simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
|
9792
|
206 |
to the equation @{prop"rev [] = []"}) and disappears; the simplified version
|
8745
|
207 |
of subgoal~2 becomes the new subgoal~1:
|
10971
|
208 |
@{subgoals[display,indent=0,margin=70]}
|
8745
|
209 |
In order to simplify this subgoal further, a lemma suggests itself.
|
|
210 |
*}
|
|
211 |
(*<*)
|
|
212 |
oops
|
|
213 |
(*>*)
|
|
214 |
|
11428
|
215 |
subsubsection{*First Lemma*}
|
9723
|
216 |
|
8745
|
217 |
text{*
|
11428
|
218 |
\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
|
|
219 |
After abandoning the above proof attempt (at the shell level type
|
|
220 |
\commdx{oops}) we start a new proof:
|
8745
|
221 |
*}
|
|
222 |
|
|
223 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
|
|
224 |
|
11428
|
225 |
txt{*\noindent The keywords \commdx{theorem} and
|
|
226 |
\commdx{lemma} are interchangeable and merely indicate
|
10971
|
227 |
the importance we attach to a proposition. Therefore we use the words
|
11428
|
228 |
\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
|
8745
|
229 |
|
9792
|
230 |
There are two variables that we could induct on: @{term"xs"} and
|
|
231 |
@{term"ys"}. Because @{text"@"} is defined by recursion on
|
|
232 |
the first argument, @{term"xs"} is the correct one:
|
8745
|
233 |
*}
|
|
234 |
|
|
235 |
apply(induct_tac xs);
|
|
236 |
|
|
237 |
txt{*\noindent
|
|
238 |
This time not even the base case is solved automatically:
|
|
239 |
*}
|
|
240 |
|
|
241 |
apply(auto);
|
|
242 |
|
|
243 |
txt{*
|
10362
|
244 |
@{subgoals[display,indent=0,goals_limit=1]}
|
|
245 |
Again, we need to abandon this proof attempt and prove another simple lemma
|
|
246 |
first. In the future the step of abandoning an incomplete proof before
|
|
247 |
embarking on the proof of a lemma usually remains implicit.
|
8745
|
248 |
*}
|
|
249 |
(*<*)
|
|
250 |
oops
|
|
251 |
(*>*)
|
|
252 |
|
11428
|
253 |
subsubsection{*Second Lemma*}
|
9723
|
254 |
|
8745
|
255 |
text{*
|
11456
|
256 |
We again try the canonical proof procedure:
|
8745
|
257 |
*}
|
|
258 |
|
|
259 |
lemma app_Nil2 [simp]: "xs @ [] = xs";
|
|
260 |
apply(induct_tac xs);
|
|
261 |
apply(auto);
|
|
262 |
|
|
263 |
txt{*
|
|
264 |
\noindent
|
11456
|
265 |
It works, yielding the desired message @{text"No subgoals!"}:
|
10362
|
266 |
@{goals[display,indent=0]}
|
8745
|
267 |
We still need to confirm that the proof is now finished:
|
|
268 |
*}
|
|
269 |
|
10171
|
270 |
done
|
8745
|
271 |
|
11428
|
272 |
text{*\noindent
|
|
273 |
As a result of that final \commdx{done}, Isabelle associates the lemma just proved
|
10171
|
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.
|
|
276 |
|
|
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.
|
10971
|
279 |
Notice that in lemma @{thm[source]app_Nil2},
|
|
280 |
as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been
|
9792
|
281 |
replaced by the unknown @{text"?xs"}, just as explained in
|
|
282 |
\S\ref{sec:variables}.
|
8745
|
283 |
|
|
284 |
Going back to the proof of the first lemma
|
|
285 |
*}
|
|
286 |
|
|
287 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
|
|
288 |
apply(induct_tac xs);
|
|
289 |
apply(auto);
|
|
290 |
|
|
291 |
txt{*
|
|
292 |
\noindent
|
9792
|
293 |
we find that this time @{text"auto"} solves the base case, but the
|
8745
|
294 |
induction step merely simplifies to
|
10362
|
295 |
@{subgoals[display,indent=0,goals_limit=1]}
|
9792
|
296 |
Now we need to remember that @{text"@"} associates to the right, and that
|
|
297 |
@{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
|
8745
|
298 |
in their \isacommand{infixr} annotation). Thus the conclusion really is
|
9723
|
299 |
\begin{isabelle}
|
9792
|
300 |
~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
|
9723
|
301 |
\end{isabelle}
|
9792
|
302 |
and the missing lemma is associativity of @{text"@"}.
|
9723
|
303 |
*}
|
|
304 |
(*<*)oops(*>*)
|
8745
|
305 |
|
11456
|
306 |
subsubsection{*Third Lemma*}
|
8745
|
307 |
|
9723
|
308 |
text{*
|
11456
|
309 |
Abandoning the previous attempt, the canonical proof procedure
|
|
310 |
succeeds without further ado.
|
8745
|
311 |
*}
|
|
312 |
|
|
313 |
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
|
|
314 |
apply(induct_tac xs);
|
10171
|
315 |
apply(auto);
|
|
316 |
done
|
8745
|
317 |
|
|
318 |
text{*
|
|
319 |
\noindent
|
11456
|
320 |
Now we can prove the first lemma:
|
8745
|
321 |
*}
|
|
322 |
|
|
323 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
|
|
324 |
apply(induct_tac xs);
|
10171
|
325 |
apply(auto);
|
|
326 |
done
|
8745
|
327 |
|
|
328 |
text{*\noindent
|
11456
|
329 |
Finally, we prove our main theorem:
|
8745
|
330 |
*}
|
|
331 |
|
|
332 |
theorem rev_rev [simp]: "rev(rev xs) = xs";
|
|
333 |
apply(induct_tac xs);
|
10171
|
334 |
apply(auto);
|
|
335 |
done
|
8745
|
336 |
|
|
337 |
text{*\noindent
|
11456
|
338 |
The final \commdx{end} tells Isabelle to close the current theory because
|
|
339 |
we are finished with its development:%
|
|
340 |
\index{*rev (constant)|)}\index{append function|)}
|
8745
|
341 |
*}
|
|
342 |
|
|
343 |
end
|