%

 \begin{isabellebody}%

 \def\isabellecontext{ToyList}%

 \isacommand{theory}\ ToyList\isanewline

 \isakeyword{import}\ PreList\isanewline

 \isakeyword{begin}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 HOL already has a predefined theory of lists called \isa{List} ---

 \isa{ToyList} is merely a small fragment of it chosen as an example. In

 contrast to what is recommended in \S\ref{sec:Basic:Theories},

 \isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a

 theory that contains pretty much everything but lists, thus avoiding

 ambiguities caused by defining lists twice.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline

 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 The datatype\index{datatype@\isacommand {datatype} (command)}

 \tydx{list} introduces two

 constructors \cdx{Nil} and \cdx{Cons}, the

 empty~list and the operator that adds an element to the front of a list. For

 example, the term \isa{Cons True (Cons False Nil)} is a value of

 type \isa{bool\ list}, namely the list with the elements \isa{True} and

 \isa{False}. Because this notation quickly becomes unwieldy, the

 datatype declaration is annotated with an alternative syntax: instead of

 \isa{Nil} and \isa{Cons x xs} we can write

 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and

 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this

 alternative syntax is the familiar one.  Thus the list \isa{Cons True

 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation

 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 

 means that \isa{{\isacharhash}} associates to

 the right: the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}

 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.

 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.

 \begin{warn}

   Syntax annotations can be powerful, but they are difficult to master and 

   are never necessary.  You

   could drop them from theory \isa{ToyList} and go back to the identifiers

   \isa{Nil} and \isa{Cons}.

   Novices should avoid using

   syntax annotations in their own theories.

 \end{warn}

 Next, two functions \isa{app} and \cdx{rev} are declared:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \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

 \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 In contrast to many functional programming languages,

 Isabelle insists on explicit declarations of all functions

 (keyword \commdx{consts}).  Apart from the declaration-before-use

 restriction, the order of items in a theory file is unconstrained. Function

 \isa{app} is annotated with concrete syntax too. Instead of the

 prefix syntax \isa{app\ xs\ ys} the infix

 \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred

 form. Both functions are defined recursively:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{primrec}\isanewline

 {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequote}\isanewline

 {\isachardoublequote}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequote}\isanewline

 \isanewline

 \isamarkupfalse%

 \isacommand{primrec}\isanewline

 {\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline

 {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent\index{*rev (constant)|(}\index{append function|(}

 The equations for \isa{app} and \isa{rev} hardly need comments:

 \isa{app} appends two lists and \isa{rev} reverses a list.  The

 keyword \commdx{primrec} indicates that the recursion is

 of a particularly primitive kind where each recursive call peels off a datatype

 constructor from one of the arguments.  Thus the

 recursion always terminates, i.e.\ the function is \textbf{total}.

 \index{functions!total}

 The termination requirement is absolutely essential in HOL, a logic of total

 functions. If we were to drop it, inconsistencies would quickly arise: the

 ``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting

 $f(n)$ on both sides.

 % However, this is a subtle issue that we cannot discuss here further.

 \begin{warn}

   As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only

   because of totality that reasoning in HOL is comparatively easy.  More

   generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as

   function definitions whose totality has not been proved) because they

   quickly lead to inconsistencies. Instead, fixed constructs for introducing

   types and functions are offered (such as \isacommand{datatype} and

   \isacommand{primrec}) which are guaranteed to preserve consistency.

 \end{warn}

 \index{syntax}%

 A remark about syntax.  The textual definition of a theory follows a fixed

 syntax with keywords like \isacommand{datatype} and \isacommand{end}.

 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).

 Embedded in this syntax are the types and formulae of HOL, whose syntax is

 extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.

 To distinguish the two levels, everything

 HOL-specific (terms and types) should be enclosed in

 \texttt{"}\dots\texttt{"}. 

 To lessen this burden, quotation marks around a single identifier can be

 dropped, unless the identifier happens to be a keyword, as in%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{consts}\ {\isachardoublequote}end{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 When Isabelle prints a syntax error message, it refers to the HOL syntax as

 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.

 \section{An Introductory Proof}

 \label{sec:intro-proof}

 Assuming you have input the declarations and definitions of \texttt{ToyList}

 presented so far, we are ready to prove a few simple theorems. This will

 illustrate not just the basic proof commands but also the typical proof

 process.

 \subsubsection*{Main Goal.}

 Our goal is to show that reversing a list twice produces the original

 list.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isamarkupfalse%

 %

 \begin{isamarkuptxt}%

 \index{theorem@\isacommand {theorem} (command)|bold}%

 \noindent

 This \isacommand{theorem} command does several things:

 \begin{itemize}

 \item

 It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.

 \item

 It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.

 \item

 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving

 simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by

 \isa{xs}.

 \end{itemize}

 The name and the simplification attribute are optional.

 Isabelle's response is to print the initial proof state consisting

 of some header information (like how many subgoals there are) followed by

 \begin{isabelle}%

 \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs%

 \end{isabelle}

 For compactness reasons we omit the header in this tutorial.

 Until we have finished a proof, the \rmindex{proof state} proper

 always looks like this:

 \begin{isabelle}

 ~1.~$G\sb{1}$\isanewline

 ~~\vdots~~\isanewline

 ~$n$.~$G\sb{n}$

 \end{isabelle}

 The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$

 that we need to prove to establish the main goal.\index{subgoals}

 Initially there is only one subgoal, which is identical with the

 main goal. (If you always want to see the main goal as well,

 set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}

 --- this flag used to be set by default.)

 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively

 defined functions are best established by induction. In this case there is

 nothing obvious except induction on \isa{xs}:%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse%

 %

 \begin{isamarkuptxt}%

 \noindent\index{*induct_tac (method)}%

 This tells Isabelle to perform induction on variable \isa{xs}. The suffix

 \isa{tac} stands for \textbf{tactic},\index{tactics}

 a synonym for ``theorem proving function''.

 By default, induction acts on the first subgoal. The new proof state contains

 two subgoals, namely the base case (\isa{Nil}) and the induction step

 (\isa{Cons}):

 \begin{isabelle}%

 \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline

 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline

 \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%

 \end{isabelle}

 The induction step is an example of the general format of a subgoal:\index{subgoals}

 \begin{isabelle}

 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}

 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}

 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be

 ignored most of the time, or simply treated as a list of variables local to

 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.

 The {\it assumptions}\index{assumptions!of subgoal}

 are the local assumptions for this subgoal and {\it

   conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. 

 Typical proof steps

 that add new assumptions are induction and case distinction. In our example

 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

 are multiple assumptions, they are enclosed in the bracket pair

 \indexboldpos{\isasymlbrakk}{$Isabrl} and

 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.

 Let us try to solve both goals automatically:%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%

 %

 \begin{isamarkuptxt}%

 \noindent

 This command tells Isabelle to apply a proof strategy called

 \isa{auto} to all subgoals. Essentially, \isa{auto} tries to

 simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks

 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version

 of subgoal~2 becomes the new subgoal~1:

 \begin{isabelle}%

 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline

 \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%

 \end{isabelle}

 In order to simplify this subgoal further, a lemma suggests itself.%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isamarkupfalse%

 %

 \isamarkupsubsubsection{First Lemma%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 \indexbold{abandoning a proof}\indexbold{proofs!abandoning}

 After abandoning the above proof attempt (at the shell level type

 \commdx{oops}) we start a new proof:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \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%

 %

 \begin{isamarkuptxt}%

 \noindent The keywords \commdx{theorem} and

 \commdx{lemma} are interchangeable and merely indicate

 the importance we attach to a proposition.  Therefore we use the words

 \emph{theorem} and \emph{lemma} pretty much interchangeably, too.

 There are two variables that we could induct on: \isa{xs} and

 \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on

 the first argument, \isa{xs} is the correct one:%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse%

 %

 \begin{isamarkuptxt}%

 \noindent

 This time not even the base case is solved automatically:%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%

 %

 \begin{isamarkuptxt}%

 \begin{isabelle}%

 \ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%

 \end{isabelle}

 Again, we need to abandon this proof attempt and prove another simple lemma

 first. In the future the step of abandoning an incomplete proof before

 embarking on the proof of a lemma usually remains implicit.%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isamarkupfalse%

 %

 \isamarkupsubsubsection{Second Lemma%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 We again try the canonical proof procedure:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%

 %

 \begin{isamarkuptxt}%

 \noindent

 It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:

 \begin{isabelle}%

 xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline

 No\ subgoals{\isacharbang}%

 \end{isabelle}

 We still need to confirm that the proof is now finished:%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isacommand{done}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 As a result of that final \commdx{done}, Isabelle associates the lemma just proved

 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}

 if it is obvious from the context that the proof is finished.

 % Instead of \isacommand{apply} followed by a dot, you can simply write

 % \isacommand{by}\indexbold{by}, which we do most of the time.

 Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},

 as printed out after the final \isacommand{done}, the free variable \isa{xs} has been

 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in

 \S\ref{sec:variables}.

 Going back to the proof of the first lemma%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \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

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%

 %

 \begin{isamarkuptxt}%

 \noindent

 we find that this time \isa{auto} solves the base case, but the

 induction step merely simplifies to

 \begin{isabelle}%

 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline

 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline

 \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}%

 \end{isabelle}

 Now we need to remember that \isa{{\isacharat}} associates to the right, and that

 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}

 in their \isacommand{infixr} annotation). Thus the conclusion really is

 \begin{isabelle}

 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))

 \end{isabelle}

 and the missing lemma is associativity of \isa{{\isacharat}}.%

 \end{isamarkuptxt}%

 \isamarkuptrue%

 \isamarkupfalse%

 %

 \isamarkupsubsubsection{Third Lemma%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 Abandoning the previous attempt, the canonical proof procedure

 succeeds without further ado.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \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

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{done}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 Now we can prove the first lemma:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \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

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{done}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 Finally, we prove our main theorem:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline

 \isamarkupfalse%

 \isacommand{done}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 \noindent

 The final \commdx{end} tells Isabelle to close the current theory because

 we are finished with its development:%

 \index{*rev (constant)|)}\index{append function|)}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{end}\isanewline

 \isamarkupfalse%

 \end{isabellebody}%

 %%% Local Variables:

 %%% mode: latex

 %%% TeX-master: "root"

 %%% End: