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: