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