9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{ToyList}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
17175
|
10 |
\isacommand{theory}\isamarkupfalse%
|
|
11 |
\ ToyList\isanewline
|
15141
|
12 |
\isakeyword{imports}\ PreList\isanewline
|
17056
|
13 |
\isakeyword{begin}%
|
|
14 |
\endisatagtheory
|
|
15 |
{\isafoldtheory}%
|
|
16 |
%
|
|
17 |
\isadelimtheory
|
|
18 |
%
|
|
19 |
\endisadelimtheory
|
11866
|
20 |
%
|
8749
|
21 |
\begin{isamarkuptext}%
|
|
22 |
\noindent
|
8771
|
23 |
HOL already has a predefined theory of lists called \isa{List} ---
|
|
24 |
\isa{ToyList} is merely a small fragment of it chosen as an example. In
|
8749
|
25 |
contrast to what is recommended in \S\ref{sec:Basic:Theories},
|
8771
|
26 |
\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
|
8749
|
27 |
theory that contains pretty much everything but lists, thus avoiding
|
|
28 |
ambiguities caused by defining lists twice.%
|
|
29 |
\end{isamarkuptext}%
|
17175
|
30 |
\isamarkuptrue%
|
|
31 |
\isacommand{datatype}\isamarkupfalse%
|
|
32 |
\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
|
|
33 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharhash}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}%
|
8749
|
34 |
\begin{isamarkuptext}%
|
|
35 |
\noindent
|
12327
|
36 |
The datatype\index{datatype@\isacommand {datatype} (command)}
|
|
37 |
\tydx{list} introduces two
|
11428
|
38 |
constructors \cdx{Nil} and \cdx{Cons}, the
|
9541
|
39 |
empty~list and the operator that adds an element to the front of a list. For
|
9792
|
40 |
example, the term \isa{Cons True (Cons False Nil)} is a value of
|
|
41 |
type \isa{bool\ list}, namely the list with the elements \isa{True} and
|
11450
|
42 |
\isa{False}. Because this notation quickly becomes unwieldy, the
|
8749
|
43 |
datatype declaration is annotated with an alternative syntax: instead of
|
9541
|
44 |
\isa{Nil} and \isa{Cons x xs} we can write
|
15364
|
45 |
\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\isa{[]}|bold} and
|
|
46 |
\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this
|
11450
|
47 |
alternative syntax is the familiar one. Thus the list \isa{Cons True
|
9674
|
48 |
(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
|
11428
|
49 |
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
|
|
50 |
means that \isa{{\isacharhash}} associates to
|
11450
|
51 |
the right: the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
|
9792
|
52 |
and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
|
10971
|
53 |
The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
|
8749
|
54 |
|
|
55 |
\begin{warn}
|
13191
|
56 |
Syntax annotations can be powerful, but they are difficult to master and
|
11456
|
57 |
are never necessary. You
|
8771
|
58 |
could drop them from theory \isa{ToyList} and go back to the identifiers
|
10795
|
59 |
\isa{Nil} and \isa{Cons}.
|
11456
|
60 |
Novices should avoid using
|
10795
|
61 |
syntax annotations in their own theories.
|
8749
|
62 |
\end{warn}
|
11428
|
63 |
Next, two functions \isa{app} and \cdx{rev} are declared:%
|
8749
|
64 |
\end{isamarkuptext}%
|
17175
|
65 |
\isamarkuptrue%
|
|
66 |
\isacommand{consts}\isamarkupfalse%
|
|
67 |
\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharat}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isanewline
|
|
68 |
\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
|
8749
|
69 |
\begin{isamarkuptext}%
|
|
70 |
\noindent
|
10971
|
71 |
In contrast to many functional programming languages,
|
|
72 |
Isabelle insists on explicit declarations of all functions
|
11456
|
73 |
(keyword \commdx{consts}). Apart from the declaration-before-use
|
10971
|
74 |
restriction, the order of items in a theory file is unconstrained. Function
|
10790
|
75 |
\isa{app} is annotated with concrete syntax too. Instead of the
|
|
76 |
prefix syntax \isa{app\ xs\ ys} the infix
|
15364
|
77 |
\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
|
8749
|
78 |
form. Both functions are defined recursively:%
|
|
79 |
\end{isamarkuptext}%
|
17175
|
80 |
\isamarkuptrue%
|
|
81 |
\isacommand{primrec}\isamarkupfalse%
|
8749
|
82 |
\isanewline
|
17175
|
83 |
{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
|
|
84 |
{\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
85 |
\isanewline
|
|
86 |
\isacommand{primrec}\isamarkupfalse%
|
|
87 |
\isanewline
|
|
88 |
{\isachardoublequoteopen}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
|
89 |
{\isachardoublequoteopen}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
|
8749
|
90 |
\begin{isamarkuptext}%
|
11456
|
91 |
\noindent\index{*rev (constant)|(}\index{append function|(}
|
10790
|
92 |
The equations for \isa{app} and \isa{rev} hardly need comments:
|
|
93 |
\isa{app} appends two lists and \isa{rev} reverses a list. The
|
11428
|
94 |
keyword \commdx{primrec} indicates that the recursion is
|
10790
|
95 |
of a particularly primitive kind where each recursive call peels off a datatype
|
8771
|
96 |
constructor from one of the arguments. Thus the
|
10654
|
97 |
recursion always terminates, i.e.\ the function is \textbf{total}.
|
11428
|
98 |
\index{functions!total}
|
8749
|
99 |
|
|
100 |
The termination requirement is absolutely essential in HOL, a logic of total
|
|
101 |
functions. If we were to drop it, inconsistencies would quickly arise: the
|
|
102 |
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
|
|
103 |
$f(n)$ on both sides.
|
|
104 |
% However, this is a subtle issue that we cannot discuss here further.
|
|
105 |
|
|
106 |
\begin{warn}
|
11456
|
107 |
As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
|
8749
|
108 |
because of totality that reasoning in HOL is comparatively easy. More
|
11456
|
109 |
generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
|
8749
|
110 |
function definitions whose totality has not been proved) because they
|
|
111 |
quickly lead to inconsistencies. Instead, fixed constructs for introducing
|
|
112 |
types and functions are offered (such as \isacommand{datatype} and
|
|
113 |
\isacommand{primrec}) which are guaranteed to preserve consistency.
|
|
114 |
\end{warn}
|
|
115 |
|
11456
|
116 |
\index{syntax}%
|
8749
|
117 |
A remark about syntax. The textual definition of a theory follows a fixed
|
10971
|
118 |
syntax with keywords like \isacommand{datatype} and \isacommand{end}.
|
|
119 |
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
|
8749
|
120 |
Embedded in this syntax are the types and formulae of HOL, whose syntax is
|
12627
|
121 |
extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
|
10971
|
122 |
To distinguish the two levels, everything
|
8749
|
123 |
HOL-specific (terms and types) should be enclosed in
|
|
124 |
\texttt{"}\dots\texttt{"}.
|
|
125 |
To lessen this burden, quotation marks around a single identifier can be
|
|
126 |
dropped, unless the identifier happens to be a keyword, as in%
|
|
127 |
\end{isamarkuptext}%
|
17175
|
128 |
\isamarkuptrue%
|
|
129 |
\isacommand{consts}\isamarkupfalse%
|
|
130 |
\ {\isachardoublequoteopen}end{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}%
|
8749
|
131 |
\begin{isamarkuptext}%
|
|
132 |
\noindent
|
|
133 |
When Isabelle prints a syntax error message, it refers to the HOL syntax as
|
11456
|
134 |
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
|
8749
|
135 |
|
|
136 |
|
10878
|
137 |
\section{An Introductory Proof}
|
8749
|
138 |
\label{sec:intro-proof}
|
|
139 |
|
16409
|
140 |
Assuming you have processed the declarations and definitions of
|
|
141 |
\texttt{ToyList} presented so far, we are ready to prove a few simple
|
|
142 |
theorems. This will illustrate not just the basic proof commands but
|
|
143 |
also the typical proof process.
|
8749
|
144 |
|
11457
|
145 |
\subsubsection*{Main Goal.}
|
8749
|
146 |
|
|
147 |
Our goal is to show that reversing a list twice produces the original
|
11456
|
148 |
list.%
|
8749
|
149 |
\end{isamarkuptext}%
|
17175
|
150 |
\isamarkuptrue%
|
|
151 |
\isacommand{theorem}\isamarkupfalse%
|
|
152 |
\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequoteclose}%
|
17056
|
153 |
\isadelimproof
|
|
154 |
%
|
|
155 |
\endisadelimproof
|
|
156 |
%
|
|
157 |
\isatagproof
|
16069
|
158 |
%
|
|
159 |
\begin{isamarkuptxt}%
|
|
160 |
\index{theorem@\isacommand {theorem} (command)|bold}%
|
|
161 |
\noindent
|
|
162 |
This \isacommand{theorem} command does several things:
|
|
163 |
\begin{itemize}
|
|
164 |
\item
|
|
165 |
It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
|
|
166 |
\item
|
|
167 |
It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.
|
|
168 |
\item
|
|
169 |
It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
|
|
170 |
simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
|
|
171 |
\isa{xs}.
|
|
172 |
\end{itemize}
|
|
173 |
The name and the simplification attribute are optional.
|
|
174 |
Isabelle's response is to print the initial proof state consisting
|
|
175 |
of some header information (like how many subgoals there are) followed by
|
|
176 |
\begin{isabelle}%
|
|
177 |
\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs%
|
|
178 |
\end{isabelle}
|
|
179 |
For compactness reasons we omit the header in this tutorial.
|
|
180 |
Until we have finished a proof, the \rmindex{proof state} proper
|
|
181 |
always looks like this:
|
|
182 |
\begin{isabelle}
|
|
183 |
~1.~$G\sb{1}$\isanewline
|
|
184 |
~~\vdots~~\isanewline
|
|
185 |
~$n$.~$G\sb{n}$
|
|
186 |
\end{isabelle}
|
|
187 |
The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
|
|
188 |
that we need to prove to establish the main goal.\index{subgoals}
|
|
189 |
Initially there is only one subgoal, which is identical with the
|
|
190 |
main goal. (If you always want to see the main goal as well,
|
|
191 |
set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
|
|
192 |
--- this flag used to be set by default.)
|
|
193 |
|
|
194 |
Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
|
|
195 |
defined functions are best established by induction. In this case there is
|
|
196 |
nothing obvious except induction on \isa{xs}:%
|
|
197 |
\end{isamarkuptxt}%
|
17175
|
198 |
\isamarkuptrue%
|
|
199 |
\isacommand{apply}\isamarkupfalse%
|
|
200 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
|
16069
|
201 |
\begin{isamarkuptxt}%
|
|
202 |
\noindent\index{*induct_tac (method)}%
|
|
203 |
This tells Isabelle to perform induction on variable \isa{xs}. The suffix
|
|
204 |
\isa{tac} stands for \textbf{tactic},\index{tactics}
|
|
205 |
a synonym for ``theorem proving function''.
|
|
206 |
By default, induction acts on the first subgoal. The new proof state contains
|
|
207 |
two subgoals, namely the base case (\isa{Nil}) and the induction step
|
|
208 |
(\isa{Cons}):
|
|
209 |
\begin{isabelle}%
|
|
210 |
\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
|
|
211 |
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
|
|
212 |
\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%
|
|
213 |
\end{isabelle}
|
|
214 |
|
|
215 |
The induction step is an example of the general format of a subgoal:\index{subgoals}
|
|
216 |
\begin{isabelle}
|
|
217 |
~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
|
|
218 |
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
|
|
219 |
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
|
|
220 |
ignored most of the time, or simply treated as a list of variables local to
|
|
221 |
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
|
|
222 |
The {\it assumptions}\index{assumptions!of subgoal}
|
|
223 |
are the local assumptions for this subgoal and {\it
|
|
224 |
conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.
|
|
225 |
Typical proof steps
|
|
226 |
that add new assumptions are induction and case distinction. In our example
|
|
227 |
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
|
|
228 |
are multiple assumptions, they are enclosed in the bracket pair
|
|
229 |
\indexboldpos{\isasymlbrakk}{$Isabrl} and
|
|
230 |
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
|
|
231 |
|
|
232 |
Let us try to solve both goals automatically:%
|
|
233 |
\end{isamarkuptxt}%
|
17175
|
234 |
\isamarkuptrue%
|
|
235 |
\isacommand{apply}\isamarkupfalse%
|
|
236 |
{\isacharparenleft}auto{\isacharparenright}%
|
16069
|
237 |
\begin{isamarkuptxt}%
|
|
238 |
\noindent
|
|
239 |
This command tells Isabelle to apply a proof strategy called
|
|
240 |
\isa{auto} to all subgoals. Essentially, \isa{auto} tries to
|
|
241 |
simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
|
|
242 |
to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
|
|
243 |
of subgoal~2 becomes the new subgoal~1:
|
|
244 |
\begin{isabelle}%
|
|
245 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
|
|
246 |
\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%
|
|
247 |
\end{isabelle}
|
|
248 |
In order to simplify this subgoal further, a lemma suggests itself.%
|
|
249 |
\end{isamarkuptxt}%
|
17175
|
250 |
\isamarkuptrue%
|
17056
|
251 |
%
|
|
252 |
\endisatagproof
|
|
253 |
{\isafoldproof}%
|
|
254 |
%
|
|
255 |
\isadelimproof
|
|
256 |
%
|
|
257 |
\endisadelimproof
|
8749
|
258 |
%
|
11428
|
259 |
\isamarkupsubsubsection{First Lemma%
|
10395
|
260 |
}
|
11866
|
261 |
\isamarkuptrue%
|
9723
|
262 |
%
|
8749
|
263 |
\begin{isamarkuptext}%
|
11428
|
264 |
\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
|
|
265 |
After abandoning the above proof attempt (at the shell level type
|
|
266 |
\commdx{oops}) we start a new proof:%
|
8749
|
267 |
\end{isamarkuptext}%
|
17175
|
268 |
\isamarkuptrue%
|
|
269 |
\isacommand{lemma}\isamarkupfalse%
|
|
270 |
\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}%
|
17056
|
271 |
\isadelimproof
|
|
272 |
%
|
|
273 |
\endisadelimproof
|
|
274 |
%
|
|
275 |
\isatagproof
|
16069
|
276 |
%
|
|
277 |
\begin{isamarkuptxt}%
|
|
278 |
\noindent The keywords \commdx{theorem} and
|
|
279 |
\commdx{lemma} are interchangeable and merely indicate
|
|
280 |
the importance we attach to a proposition. Therefore we use the words
|
|
281 |
\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
|
|
282 |
|
|
283 |
There are two variables that we could induct on: \isa{xs} and
|
|
284 |
\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
|
|
285 |
the first argument, \isa{xs} is the correct one:%
|
|
286 |
\end{isamarkuptxt}%
|
17175
|
287 |
\isamarkuptrue%
|
|
288 |
\isacommand{apply}\isamarkupfalse%
|
|
289 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
|
16069
|
290 |
\begin{isamarkuptxt}%
|
|
291 |
\noindent
|
|
292 |
This time not even the base case is solved automatically:%
|
|
293 |
\end{isamarkuptxt}%
|
17175
|
294 |
\isamarkuptrue%
|
|
295 |
\isacommand{apply}\isamarkupfalse%
|
|
296 |
{\isacharparenleft}auto{\isacharparenright}%
|
16069
|
297 |
\begin{isamarkuptxt}%
|
|
298 |
\begin{isabelle}%
|
|
299 |
\ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%
|
|
300 |
\end{isabelle}
|
|
301 |
Again, we need to abandon this proof attempt and prove another simple lemma
|
|
302 |
first. In the future the step of abandoning an incomplete proof before
|
|
303 |
embarking on the proof of a lemma usually remains implicit.%
|
|
304 |
\end{isamarkuptxt}%
|
17175
|
305 |
\isamarkuptrue%
|
17056
|
306 |
%
|
|
307 |
\endisatagproof
|
|
308 |
{\isafoldproof}%
|
|
309 |
%
|
|
310 |
\isadelimproof
|
|
311 |
%
|
|
312 |
\endisadelimproof
|
8749
|
313 |
%
|
11428
|
314 |
\isamarkupsubsubsection{Second Lemma%
|
10395
|
315 |
}
|
11866
|
316 |
\isamarkuptrue%
|
9723
|
317 |
%
|
8749
|
318 |
\begin{isamarkuptext}%
|
11456
|
319 |
We again try the canonical proof procedure:%
|
8749
|
320 |
\end{isamarkuptext}%
|
17175
|
321 |
\isamarkuptrue%
|
|
322 |
\isacommand{lemma}\isamarkupfalse%
|
|
323 |
\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
|
17056
|
324 |
%
|
|
325 |
\isadelimproof
|
|
326 |
%
|
|
327 |
\endisadelimproof
|
|
328 |
%
|
|
329 |
\isatagproof
|
17175
|
330 |
\isacommand{apply}\isamarkupfalse%
|
|
331 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
|
|
332 |
\isacommand{apply}\isamarkupfalse%
|
|
333 |
{\isacharparenleft}auto{\isacharparenright}%
|
16069
|
334 |
\begin{isamarkuptxt}%
|
|
335 |
\noindent
|
|
336 |
It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:
|
|
337 |
\begin{isabelle}%
|
|
338 |
xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
|
|
339 |
No\ subgoals{\isacharbang}%
|
|
340 |
\end{isabelle}
|
|
341 |
We still need to confirm that the proof is now finished:%
|
|
342 |
\end{isamarkuptxt}%
|
17175
|
343 |
\isamarkuptrue%
|
|
344 |
\isacommand{done}\isamarkupfalse%
|
|
345 |
%
|
17056
|
346 |
\endisatagproof
|
|
347 |
{\isafoldproof}%
|
|
348 |
%
|
|
349 |
\isadelimproof
|
|
350 |
%
|
|
351 |
\endisadelimproof
|
11866
|
352 |
%
|
8749
|
353 |
\begin{isamarkuptext}%
|
11428
|
354 |
\noindent
|
|
355 |
As a result of that final \commdx{done}, Isabelle associates the lemma just proved
|
10171
|
356 |
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
|
|
357 |
if it is obvious from the context that the proof is finished.
|
|
358 |
|
|
359 |
% Instead of \isacommand{apply} followed by a dot, you can simply write
|
|
360 |
% \isacommand{by}\indexbold{by}, which we do most of the time.
|
10971
|
361 |
Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
|
|
362 |
as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
|
9792
|
363 |
replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
|
|
364 |
\S\ref{sec:variables}.
|
8749
|
365 |
|
|
366 |
Going back to the proof of the first lemma%
|
|
367 |
\end{isamarkuptext}%
|
17175
|
368 |
\isamarkuptrue%
|
|
369 |
\isacommand{lemma}\isamarkupfalse%
|
|
370 |
\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
371 |
%
|
|
372 |
\isadelimproof
|
|
373 |
%
|
|
374 |
\endisadelimproof
|
|
375 |
%
|
|
376 |
\isatagproof
|
17175
|
377 |
\isacommand{apply}\isamarkupfalse%
|
|
378 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
|
|
379 |
\isacommand{apply}\isamarkupfalse%
|
|
380 |
{\isacharparenleft}auto{\isacharparenright}%
|
16069
|
381 |
\begin{isamarkuptxt}%
|
|
382 |
\noindent
|
|
383 |
we find that this time \isa{auto} solves the base case, but the
|
|
384 |
induction step merely simplifies to
|
|
385 |
\begin{isabelle}%
|
|
386 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
|
|
387 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline
|
|
388 |
\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}%
|
|
389 |
\end{isabelle}
|
|
390 |
Now we need to remember that \isa{{\isacharat}} associates to the right, and that
|
|
391 |
\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
|
|
392 |
in their \isacommand{infixr} annotation). Thus the conclusion really is
|
|
393 |
\begin{isabelle}
|
|
394 |
~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
|
|
395 |
\end{isabelle}
|
|
396 |
and the missing lemma is associativity of \isa{{\isacharat}}.%
|
|
397 |
\end{isamarkuptxt}%
|
17175
|
398 |
\isamarkuptrue%
|
17056
|
399 |
%
|
|
400 |
\endisatagproof
|
|
401 |
{\isafoldproof}%
|
|
402 |
%
|
|
403 |
\isadelimproof
|
|
404 |
%
|
|
405 |
\endisadelimproof
|
8749
|
406 |
%
|
11456
|
407 |
\isamarkupsubsubsection{Third Lemma%
|
10395
|
408 |
}
|
11866
|
409 |
\isamarkuptrue%
|
9723
|
410 |
%
|
|
411 |
\begin{isamarkuptext}%
|
11456
|
412 |
Abandoning the previous attempt, the canonical proof procedure
|
|
413 |
succeeds without further ado.%
|
9723
|
414 |
\end{isamarkuptext}%
|
17175
|
415 |
\isamarkuptrue%
|
|
416 |
\isacommand{lemma}\isamarkupfalse%
|
|
417 |
\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
418 |
%
|
|
419 |
\isadelimproof
|
|
420 |
%
|
|
421 |
\endisadelimproof
|
|
422 |
%
|
|
423 |
\isatagproof
|
17175
|
424 |
\isacommand{apply}\isamarkupfalse%
|
|
425 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
|
|
426 |
\isacommand{apply}\isamarkupfalse%
|
|
427 |
{\isacharparenleft}auto{\isacharparenright}\isanewline
|
|
428 |
\isacommand{done}\isamarkupfalse%
|
|
429 |
%
|
17056
|
430 |
\endisatagproof
|
|
431 |
{\isafoldproof}%
|
|
432 |
%
|
|
433 |
\isadelimproof
|
|
434 |
%
|
|
435 |
\endisadelimproof
|
11866
|
436 |
%
|
8749
|
437 |
\begin{isamarkuptext}%
|
|
438 |
\noindent
|
11456
|
439 |
Now we can prove the first lemma:%
|
8749
|
440 |
\end{isamarkuptext}%
|
17175
|
441 |
\isamarkuptrue%
|
|
442 |
\isacommand{lemma}\isamarkupfalse%
|
|
443 |
\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
444 |
%
|
|
445 |
\isadelimproof
|
|
446 |
%
|
|
447 |
\endisadelimproof
|
|
448 |
%
|
|
449 |
\isatagproof
|
17175
|
450 |
\isacommand{apply}\isamarkupfalse%
|
|
451 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
|
|
452 |
\isacommand{apply}\isamarkupfalse%
|
|
453 |
{\isacharparenleft}auto{\isacharparenright}\isanewline
|
|
454 |
\isacommand{done}\isamarkupfalse%
|
|
455 |
%
|
17056
|
456 |
\endisatagproof
|
|
457 |
{\isafoldproof}%
|
|
458 |
%
|
|
459 |
\isadelimproof
|
|
460 |
%
|
|
461 |
\endisadelimproof
|
11866
|
462 |
%
|
8749
|
463 |
\begin{isamarkuptext}%
|
|
464 |
\noindent
|
11456
|
465 |
Finally, we prove our main theorem:%
|
8749
|
466 |
\end{isamarkuptext}%
|
17175
|
467 |
\isamarkuptrue%
|
|
468 |
\isacommand{theorem}\isamarkupfalse%
|
|
469 |
\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
|
17056
|
470 |
%
|
|
471 |
\isadelimproof
|
|
472 |
%
|
|
473 |
\endisadelimproof
|
|
474 |
%
|
|
475 |
\isatagproof
|
17175
|
476 |
\isacommand{apply}\isamarkupfalse%
|
|
477 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
|
|
478 |
\isacommand{apply}\isamarkupfalse%
|
|
479 |
{\isacharparenleft}auto{\isacharparenright}\isanewline
|
|
480 |
\isacommand{done}\isamarkupfalse%
|
|
481 |
%
|
17056
|
482 |
\endisatagproof
|
|
483 |
{\isafoldproof}%
|
|
484 |
%
|
|
485 |
\isadelimproof
|
|
486 |
%
|
|
487 |
\endisadelimproof
|
11866
|
488 |
%
|
8749
|
489 |
\begin{isamarkuptext}%
|
|
490 |
\noindent
|
11456
|
491 |
The final \commdx{end} tells Isabelle to close the current theory because
|
8749
|
492 |
we are finished with its development:%
|
11456
|
493 |
\index{*rev (constant)|)}\index{append function|)}%
|
8749
|
494 |
\end{isamarkuptext}%
|
17175
|
495 |
\isamarkuptrue%
|
17056
|
496 |
%
|
|
497 |
\isadelimtheory
|
|
498 |
%
|
|
499 |
\endisadelimtheory
|
|
500 |
%
|
|
501 |
\isatagtheory
|
17175
|
502 |
\isacommand{end}\isamarkupfalse%
|
|
503 |
%
|
17056
|
504 |
\endisatagtheory
|
|
505 |
{\isafoldtheory}%
|
|
506 |
%
|
|
507 |
\isadelimtheory
|
|
508 |
%
|
|
509 |
\endisadelimtheory
|
|
510 |
\isanewline
|
9722
|
511 |
\end{isabellebody}%
|
9145
|
512 |
%%% Local Variables:
|
|
513 |
%%% mode: latex
|
|
514 |
%%% TeX-master: "root"
|
|
515 |
%%% End:
|