doc-src/ProgProve/Thys/document/Bool_nat_list.tex

doc update

%
\begin{isabellebody}%
\def\isabellecontext{Bool{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}list}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
\vspace{-4ex}
\section{\texorpdfstring{Types \isa{bool}, \isa{nat} and \isa{list}}{Types bool, nat and list}}

These are the most important predefined types. We go through them one by one.
Based on examples we learn how to define (possibly recursive) functions and
prove theorems about them by induction and simplification.

\subsection{Type \isa{bool}}

The type of boolean values is a predefined datatype
\begin{isabelle}%
\isacommand{datatype}\ bool\ {\isaliteral{3D}{\isacharequal}}\ True\ {\isaliteral{7C}{\isacharbar}}\ False%
\end{isabelle}
with the two values \isa{True} and \isa{False} and
with many predefined functions:  \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}}, \isa{{\isaliteral{5C3C616E643E}{\isasymand}}}, \isa{{\isaliteral{5C3C6F723E}{\isasymor}}}, \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} etc. Here is how conjunction could be defined by pattern matching:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ conj\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}conj\ True\ True\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}conj\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
Both the datatype and function definitions roughly follow the syntax
of functional programming languages.

\subsection{Type \isa{nat}}

Natural numbers are another predefined datatype:
\begin{isabelle}%
\isacommand{datatype}\ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ nat%
\end{isabelle}
All values of type \isa{nat} are generated by the constructors
\isa{{\isadigit{0}}} and \isa{Suc}. Thus the values of type \isa{nat} are
\isa{{\isadigit{0}}}, \isa{Suc\ {\isadigit{0}}}, \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}} etc.
There are many predefined functions: \isa{{\isaliteral{2B}{\isacharplus}}}, \isa{{\isaliteral{2A}{\isacharasterisk}}}, \isa{{\isaliteral{5C3C6C653E}{\isasymle}}}, etc. Here is how you could define your own addition:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ add\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}add\ {\isadigit{0}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}add\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc{\isaliteral{28}{\isacharparenleft}}add\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
And here is a proof of the fact that \isa{add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ add{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}induction\ m{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
The \isacom{lemma} command starts the proof and gives the lemma
a name, \isa{add{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}{\isadigit{2}}}. Properties of recursively defined functions
need to be established by induction in most cases.
Command \isacom{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induction\ m{\isaliteral{29}{\isacharparenright}}} instructs Isabelle to
start a proof by induction on \isa{m}. In response, it will show the
following proof state:
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ add\ {\isadigit{0}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\isanewline
\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}m{\isaliteral{2E}{\isachardot}}\ add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ add\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ m%
\end{isabelle}
The numbered lines are known as \emph{subgoals}.
The first subgoal is the base case, the second one the induction step.
The prefix \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}m{\isaliteral{2E}{\isachardot}}} is Isabelle's way of saying ``for an arbitrary but fixed \isa{m}''. The \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} separates assumptions from the conclusion.
The command \isacom{apply}\isa{{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}} instructs Isabelle to try
and prove all subgoals automatically, essentially by simplifying them.
Because both subgoals are easy, Isabelle can do it.
The base case \isa{add\ {\isadigit{0}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} holds by definition of \isa{add},
and the induction step is almost as simple:
\isa{add~{\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ Suc{\isaliteral{28}{\isacharparenleft}}add\ m\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ m}
using first the definition of \isa{add} and then the induction hypothesis.
In summary, both subproofs rely on simplification with function definitions and
the induction hypothesis.
As a result of that final \isacom{done}, Isabelle associates the lemma
just proved with its name. You can now inspect the lemma with the command%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isacommand{thm}\isamarkupfalse%
\ add{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}{\isadigit{2}}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
which displays \begin{isabelle}%
add\ {\isaliteral{3F}{\isacharquery}}m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}m%
\end{isabelle} The free
variable \isa{m} has been replaced by the \concept{unknown}
\isa{{\isaliteral{3F}{\isacharquery}}m}. There is no logical difference between the two but an
operational one: unknowns can be instantiated, which is what you want after
some lemma has been proved.

Note that there is also a proof method \isa{induct}, which behaves almost
like \isa{induction}; the difference is explained in \autoref{ch:Isar}.

\begin{warn}
Terminology: We use \concept{lemma}, \concept{theorem} and \concept{rule}
interchangeably for propositions that have been proved.
\end{warn}
\begin{warn}
  Numerals (\isa{{\isadigit{0}}}, \isa{{\isadigit{1}}}, \isa{{\isadigit{2}}}, \dots) and most of the standard
  arithmetic operations (\isa{{\isaliteral{2B}{\isacharplus}}}, \isa{{\isaliteral{2D}{\isacharminus}}}, \isa{{\isaliteral{2A}{\isacharasterisk}}}, \isa{{\isaliteral{5C3C6C653E}{\isasymle}}},
  \isa{{\isaliteral{3C}{\isacharless}}} etc) are overloaded: they are available
  not just for natural numbers but for other types as well.
  For example, given the goal \isa{x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ x}, there is nothing to indicate
  that you are talking about natural numbers. Hence Isabelle can only infer
  that \isa{x} is of some arbitrary type where \isa{{\isadigit{0}}} and \isa{{\isaliteral{2B}{\isacharplus}}}
  exist. As a consequence, you will be unable to prove the
  goal. To alert you to such pitfalls, Isabelle flags numerals without a
  fixed type in its output: \isa{x\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x}.  In this particular example,
  you need to include
  an explicit type constraint, for example \isa{x{\isaliteral{2B}{\isacharplus}}{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}}. If there
  is enough contextual information this may not be necessary: \isa{Suc\ x\ {\isaliteral{3D}{\isacharequal}}\ x} automatically implies \isa{x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat} because \isa{Suc} is not
  overloaded.
\end{warn}

\subsubsection{An informal proof}

Above we gave some terse informal explanation of the proof of
\isa{add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m}. A more detailed informal exposition of the lemma
might look like this:
\bigskip

\noindent
\textbf{Lemma} \isa{add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m}

\noindent
\textbf{Proof} by induction on \isa{m}.
\begin{itemize}
\item Case \isa{{\isadigit{0}}} (the base case): \isa{add\ {\isadigit{0}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}
  holds by definition of \isa{add}.
\item Case \isa{Suc\ m} (the induction step):
  We assume \isa{add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m}, the induction hypothesis (IH),
  and we need to show \isa{add\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ m}.
  The proof is as follows:\smallskip

  \begin{tabular}{@ {}rcl@ {\quad}l@ {}}
  \isa{add\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isadigit{0}}} &\isa{{\isaliteral{3D}{\isacharequal}}}& \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}add\ m\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}}
  & by definition of \isa{add}\\
              &\isa{{\isaliteral{3D}{\isacharequal}}}& \isa{Suc\ m} & by IH
  \end{tabular}
\end{itemize}
Throughout this book, \concept{IH} will stand for ``induction hypothesis''.

We have now seen three proofs of \isa{add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}: the Isabelle one, the
terse four lines explaining the base case and the induction step, and just now a
model of a traditional inductive proof. The three proofs differ in the level
of detail given and the intended reader: the Isabelle proof is for the
machine, the informal proofs are for humans. Although this book concentrates
on Isabelle proofs, it is important to be able to rephrase those proofs
as informal text comprehensible to a reader familiar with traditional
mathematical proofs. Later on we will introduce an Isabelle proof language
that is closer to traditional informal mathematical language and is often
directly readable.

\subsection{Type \isa{list}}

Although lists are already predefined, we define our own copy just for
demonstration purposes:%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isacommand{datatype}\isamarkupfalse%
\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\begin{itemize}
\item Type \isa{{\isaliteral{27}{\isacharprime}}a\ list} is the type of lists over elements of type \isa{{\isaliteral{27}{\isacharprime}}a}. Because \isa{{\isaliteral{27}{\isacharprime}}a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
\item Lists have two constructors: \isa{Nil}, the empty list, and \isa{Cons}, which puts an element (of type \isa{{\isaliteral{27}{\isacharprime}}a}) in front of a list (of type \isa{{\isaliteral{27}{\isacharprime}}a\ list}).
Hence all lists are of the form \isa{Nil}, or \isa{Cons\ x\ Nil},
or \isa{Cons\ x\ {\isaliteral{28}{\isacharparenleft}}Cons\ y\ Nil{\isaliteral{29}{\isacharparenright}}} etc.
\item \isacom{datatype} requires no quotation marks on the
left-hand side, but on the right-hand side each of the argument
types of a constructor needs to be enclosed in quotation marks, unless
it is just an identifier (e.g.\ \isa{nat} or \isa{{\isaliteral{27}{\isacharprime}}a}).
\end{itemize}
We also define two standard functions, append and reverse:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ app\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}app\ Nil\ ys\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}app\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ Cons\ x\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{fun}\isamarkupfalse%
\ rev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}rev\ Nil\ {\isaliteral{3D}{\isacharequal}}\ Nil{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}rev\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ Nil{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
By default, variables \isa{xs}, \isa{ys} and \isa{zs} are of
\isa{list} type.

Command \isacom{value} evaluates a term. For example,%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{value}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}Cons\ True\ {\isaliteral{28}{\isacharparenleft}}Cons\ False\ Nil{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
yields the result \isa{Cons\ False\ {\isaliteral{28}{\isacharparenleft}}Cons\ True\ Nil{\isaliteral{29}{\isacharparenright}}}. This works symbolically, too:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{value}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}Cons\ a\ {\isaliteral{28}{\isacharparenleft}}Cons\ b\ Nil{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
yields \isa{Cons\ b\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}}.
\medskip

Figure~\ref{fig:MyList} shows the theory created so far.
% Notice where the
%quotations marks are needed that we mostly sweep under the carpet.  In
%particular, notice that \isacom{datatype} requires no quotation marks on the
%left-hand side, but that on the right-hand side each of the argument
%types of a constructor needs to be enclosed in quotation marks.

\begin{figure}[htbp]
\begin{alltt}
\input{Thys/MyList.thy}\end{alltt}
\caption{A Theory of Lists}
\label{fig:MyList}
\end{figure}

\subsubsection{Structural Induction for Lists}

Just as for natural numbers, there is a proof principle of induction for
lists. Induction over a list is essentially induction over the length of
the list, although the length remains implicit. To prove that some property
\isa{P} holds for all lists \isa{xs}, i.e.\ \mbox{\isa{P\ xs}},
you need to prove
\begin{enumerate}
\item the base case \isa{P\ Nil} and
\item the inductive case \isa{P\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}} under the assumption \isa{P\ xs}, for some arbitrary but fixed \isa{x} and \isa{xs}.
\end{enumerate}
This is often called \concept{structural induction}.

\subsection{The Proof Process}

We will now demonstrate the typical proof process, which involves
the formulation and proof of auxiliary lemmas.
Our goal is to show that reversing a list twice produces the original
list.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
\ rev{\isaliteral{5F}{\isacharunderscore}}rev\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
Commands \isacom{theorem} and \isacom{lemma} are
interchangeable and merely indicate the importance we attach to a
proposition. Via the bracketed attribute \isa{simp} we also tell Isabelle
to make the eventual theorem a \concept{simplification rule}: future proofs
involving simplification will replace occurrences of \isa{rev\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}} by
\isa{xs}. The proof is by induction:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}induction\ xs{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
As explained above, we obtain two subgoals, namely the base case (\isa{Nil}) and the induction step (\isa{Cons}):
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ rev\ {\isaliteral{28}{\isacharparenleft}}rev\ Nil{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Nil\isanewline
\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ xs{\isaliteral{2E}{\isachardot}}\ rev\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ rev\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Cons\ a\ xs%
\end{isabelle}
Let us try to solve both goals automatically:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
Subgoal~1 is proved, and disappears; the simplified version
of subgoal~2 becomes the new subgoal~1:
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ xs{\isaliteral{2E}{\isachardot}}\isanewline
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }rev\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }rev\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Cons\ a\ xs%
\end{isabelle}
In order to simplify this subgoal further, a lemma suggests itself.

\subsubsection{A First Lemma}

We insert the following lemma in front of the main theorem:%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
\ rev{\isaliteral{5F}{\isacharunderscore}}app\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
There are two variables that we could induct on: \isa{xs} and
\isa{ys}. Because \isa{app} is defined by recursion on
the first argument, \isa{xs} is the correct one:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}induction\ xs{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
This time not even the base case is solved automatically:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\vspace{-5ex}
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ rev\ ys\ {\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ Nil%
\end{isabelle}
Again, we need to abandon this proof attempt and prove another simple lemma
first.

\subsubsection{A Second Lemma}

We again try the canonical proof procedure:%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
\ app{\isaliteral{5F}{\isacharunderscore}}Nil{\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}app\ xs\ Nil\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}induction\ xs{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Thankfully, this worked.
Now we can continue with our stuck proof attempt of the first lemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ rev{\isaliteral{5F}{\isacharunderscore}}app\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}induction\ xs{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
We find that this time \isa{auto} solves the base case, but the
induction step merely simplifies to
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ xs{\isaliteral{2E}{\isachardot}}\isanewline
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }rev\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }app\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
The missing lemma is associativity of \isa{app},
which we insert in front of the failed lemma \isa{rev{\isaliteral{5F}{\isacharunderscore}}app}.

\subsubsection{Associativity of \isa{app}}

The canonical proof procedure succeeds without further ado:%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
\ app{\isaliteral{5F}{\isacharunderscore}}assoc\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}app\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ app\ xs\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}induction\ xs{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Finally the proofs of \isa{rev{\isaliteral{5F}{\isacharunderscore}}app} and \isa{rev{\isaliteral{5F}{\isacharunderscore}}rev}
succeed, too.

\subsubsection{Another informal proof}

Here is the informal proof of associativity of \isa{app}
corresponding to the Isabelle proof above.
\bigskip

\noindent
\textbf{Lemma} \isa{app\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ app\ xs\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}}

\noindent
\textbf{Proof} by induction on \isa{xs}.
\begin{itemize}
\item Case \isa{Nil}: \ \isa{app\ {\isaliteral{28}{\isacharparenleft}}app\ Nil\ ys{\isaliteral{29}{\isacharparenright}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ app\ ys\ zs} \isa{{\isaliteral{3D}{\isacharequal}}}
  \mbox{\isa{app\ Nil\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}}} \ holds by definition of \isa{app}.
\item Case \isa{Cons\ x\ xs}: We assume
  \begin{center} \hfill \isa{app\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ zs} \isa{{\isaliteral{3D}{\isacharequal}}}
  \isa{app\ xs\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}} \hfill (IH) \end{center}
  and we need to show
  \begin{center} \isa{app\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}\ ys{\isaliteral{29}{\isacharparenright}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}}.\end{center}
  The proof is as follows:\smallskip

  \begin{tabular}{@ {}l@ {\quad}l@ {}}
  \isa{app\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}\ ys{\isaliteral{29}{\isacharparenright}}\ zs}\\
  \isa{{\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ zs} & by definition of \isa{app}\\
  \isa{{\isaliteral{3D}{\isacharequal}}\ Cons\ x\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ zs{\isaliteral{29}{\isacharparenright}}} & by definition of \isa{app}\\
  \isa{{\isaliteral{3D}{\isacharequal}}\ Cons\ x\ {\isaliteral{28}{\isacharparenleft}}app\ xs\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} & by IH\\
  \isa{{\isaliteral{3D}{\isacharequal}}\ app\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}} & by definition of \isa{app}
  \end{tabular}
\end{itemize}
\medskip

\noindent Didn't we say earlier that all proofs are by simplification? But
in both cases, going from left to right, the last equality step is not a
simplification at all! In the base case it is \isa{app\ ys\ zs\ {\isaliteral{3D}{\isacharequal}}\ app\ Nil\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}}. It appears almost mysterious because we suddenly complicate the
term by appending \isa{Nil} on the left. What is really going on is this:
when proving some equality \mbox{\isa{s\ {\isaliteral{3D}{\isacharequal}}\ t}}, both \isa{s} and \isa{t} are
simplified to some common term \isa{u}.  This heuristic for equality proofs
works well for a functional programming context like ours. In the base case
\isa{s} is \isa{app\ {\isaliteral{28}{\isacharparenleft}}app\ Nil\ ys{\isaliteral{29}{\isacharparenright}}\ zs}, \isa{t} is \isa{app\ Nil\ {\isaliteral{28}{\isacharparenleft}}app\ ys\ zs{\isaliteral{29}{\isacharparenright}}}, and \isa{u} is \isa{app\ ys\ zs}.

\subsection{Predefined lists}
\label{sec:predeflists}

Isabelle's predefined lists are the same as the ones above, but with
more syntactic sugar:
\begin{itemize}
\item \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is \isa{Nil},
\item \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs} is \isa{Cons\ x\ xs},
\item \isa{{\isaliteral{5B}{\isacharbrackleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} is \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{23}{\isacharhash}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, and
\item \isa{xs\ {\isaliteral{40}{\isacharat}}\ ys} is \isa{app\ xs\ ys}.
\end{itemize}
There is also a large library of predefined functions.
The most important ones are the length function
\isa{length\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} (with the obvious definition),
and the map function that applies a function to all elements of a list:
\begin{isabelle}
\isacom{fun} \isa{map} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list{\isaliteral{22}{\isachardoublequote}}}\\
\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{7C}{\isacharbar}}}\\
\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs}\isa{{\isaliteral{22}{\isachardoublequote}}}
\end{isabelle}
\sem
Also useful are the \concept{head} of a list, its first element,
and the \concept{tail}, the rest of the list:
\begin{isabelle}
\isacom{fun} \isa{hd\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
\isa{hd\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x}
\end{isabelle}
\begin{isabelle}
\isacom{fun} \isa{tl\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
\isa{tl\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} \isa{{\isaliteral{7C}{\isacharbar}}}\\
\isa{tl\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs}
\end{isabelle}
Note that since HOL is a logic of total functions, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is defined,
but we do now know what the result is. That is, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is not undefined
but underdefined.
\endsem
%%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: