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