doc-src/IsarRef/Thy/document/Proof.tex
author noschinl
Thu Oct 13 13:49:55 2011 +0200 (2011-10-13 ago)
changeset 45135 5ba2f065c6f7
parent 45103 a45121ffcfcb
child 46262 912b42e64fde
permissions -rw-r--r--
tuned markup
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Proof}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Proof\isanewline
    12 \isakeyword{imports}\ Base\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Proofs \label{ch:proofs}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 Proof commands perform transitions of Isar/VM machine
    27   configurations, which are block-structured, consisting of a stack of
    28   nodes with three main components: logical proof context, current
    29   facts, and open goals.  Isar/VM transitions are typed according to
    30   the following three different modes of operation:
    31 
    32   \begin{description}
    33 
    34   \item \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} means that a new goal has just been
    35   stated that is now to be \emph{proven}; the next command may refine
    36   it by some proof method, and enter a sub-proof to establish the
    37   actual result.
    38 
    39   \item \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is like a nested theory mode: the
    40   context may be augmented by \emph{stating} additional assumptions,
    41   intermediate results etc.
    42 
    43   \item \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is intermediate between \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}: existing facts (i.e.\
    44   the contents of the special ``\indexref{}{fact}{this}\hyperlink{fact.this}{\mbox{\isa{this}}}'' register) have been
    45   just picked up in order to be used when refining the goal claimed
    46   next.
    47 
    48   \end{description}
    49 
    50   The proof mode indicator may be understood as an instruction to the
    51   writer, telling what kind of operation may be performed next.  The
    52   corresponding typings of proof commands restricts the shape of
    53   well-formed proof texts to particular command sequences.  So dynamic
    54   arrangements of commands eventually turn out as static texts of a
    55   certain structure.
    56 
    57   \Appref{ap:refcard} gives a simplified grammar of the (extensible)
    58   language emerging that way from the different types of proof
    59   commands.  The main ideas of the overall Isar framework are
    60   explained in \chref{ch:isar-framework}.%
    61 \end{isamarkuptext}%
    62 \isamarkuptrue%
    63 %
    64 \isamarkupsection{Proof structure%
    65 }
    66 \isamarkuptrue%
    67 %
    68 \isamarkupsubsection{Formal notepad%
    69 }
    70 \isamarkuptrue%
    71 %
    72 \begin{isamarkuptext}%
    73 \begin{matharray}{rcl}
    74     \indexdef{}{command}{notepad}\hypertarget{command.notepad}{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
    75   \end{matharray}
    76 
    77   \begin{railoutput}
    78 \rail@begin{1}{}
    79 \rail@term{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}}[]
    80 \rail@term{\isa{\isakeyword{begin}}}[]
    81 \rail@end
    82 \rail@begin{1}{}
    83 \rail@term{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}}[]
    84 \rail@end
    85 \end{railoutput}
    86 
    87 
    88   \begin{description}
    89 
    90   \item \hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} opens a proof state
    91   without any goal statement.  This allows to experiment with Isar,
    92   without producing any persistent result.
    93 
    94   The notepad can be closed by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} or discontinued by
    95   \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
    96 
    97   \end{description}%
    98 \end{isamarkuptext}%
    99 \isamarkuptrue%
   100 %
   101 \isamarkupsubsection{Blocks%
   102 }
   103 \isamarkuptrue%
   104 %
   105 \begin{isamarkuptext}%
   106 \begin{matharray}{rcl}
   107     \indexdef{}{command}{next}\hypertarget{command.next}{\hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   108     \indexdef{}{command}{\{}\hypertarget{command.braceleft}{\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   109     \indexdef{}{command}{\}}\hypertarget{command.braceright}{\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isaliteral{7D}{\isacharbraceright}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   110   \end{matharray}
   111 
   112   While Isar is inherently block-structured, opening and closing
   113   blocks is mostly handled rather casually, with little explicit
   114   user-intervention.  Any local goal statement automatically opens
   115   \emph{two} internal blocks, which are closed again when concluding
   116   the sub-proof (by \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} etc.).  Sections of different
   117   context within a sub-proof may be switched via \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}},
   118   which is just a single block-close followed by block-open again.
   119   The effect of \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} is to reset the local proof context;
   120   there is no goal focus involved here!
   121 
   122   For slightly more advanced applications, there are explicit block
   123   parentheses as well.  These typically achieve a stronger forward
   124   style of reasoning.
   125 
   126   \begin{description}
   127 
   128   \item \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} switches to a fresh block within a
   129   sub-proof, resetting the local context to the initial one.
   130 
   131   \item \hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}}}} and \hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isaliteral{7D}{\isacharbraceright}}}}}} explicitly open and close
   132   blocks.  Any current facts pass through ``\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}}}}''
   133   unchanged, while ``\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isaliteral{7D}{\isacharbraceright}}}}}}'' causes any result to be
   134   \emph{exported} into the enclosing context.  Thus fixed variables
   135   are generalized, assumptions discharged, and local definitions
   136   unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
   137   of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} and \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} in this mode of
   138   forward reasoning --- in contrast to plain backward reasoning with
   139   the result exported at \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} time.
   140 
   141   \end{description}%
   142 \end{isamarkuptext}%
   143 \isamarkuptrue%
   144 %
   145 \isamarkupsubsection{Omitting proofs%
   146 }
   147 \isamarkuptrue%
   148 %
   149 \begin{isamarkuptext}%
   150 \begin{matharray}{rcl}
   151     \indexdef{}{command}{oops}\hypertarget{command.oops}{\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   152   \end{matharray}
   153 
   154   The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command discontinues the current proof
   155   attempt, while considering the partial proof text as properly
   156   processed.  This is conceptually quite different from ``faking''
   157   actual proofs via \indexref{}{command}{sorry}\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} (see
   158   \secref{sec:proof-steps}): \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not observe the
   159   proof structure at all, but goes back right to the theory level.
   160   Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
   161   --- there is no intended claim to be able to complete the proof
   162   in any way.
   163 
   164   A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
   165   \emph{within} the system itself, in conjunction with the document
   166   preparation tools of Isabelle described in \chref{ch:document-prep}.
   167   Thus partial or even wrong proof attempts can be discussed in a
   168   logically sound manner.  Note that the Isabelle {\LaTeX} macros can
   169   be easily adapted to print something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' instead of
   170   the keyword ``\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}''.
   171 
   172   \medskip The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command is undo-able, unlike
   173   \indexref{}{command}{kill}\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} (see \secref{sec:history}).  The effect is to
   174   get back to the theory just before the opening of the proof.%
   175 \end{isamarkuptext}%
   176 \isamarkuptrue%
   177 %
   178 \isamarkupsection{Statements%
   179 }
   180 \isamarkuptrue%
   181 %
   182 \isamarkupsubsection{Context elements \label{sec:proof-context}%
   183 }
   184 \isamarkuptrue%
   185 %
   186 \begin{isamarkuptext}%
   187 \begin{matharray}{rcl}
   188     \indexdef{}{command}{fix}\hypertarget{command.fix}{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   189     \indexdef{}{command}{assume}\hypertarget{command.assume}{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   190     \indexdef{}{command}{presume}\hypertarget{command.presume}{\hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   191     \indexdef{}{command}{def}\hypertarget{command.def}{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   192   \end{matharray}
   193 
   194   The logical proof context consists of fixed variables and
   195   assumptions.  The former closely correspond to Skolem constants, or
   196   meta-level universal quantification as provided by the Isabelle/Pure
   197   logical framework.  Introducing some \emph{arbitrary, but fixed}
   198   variable via ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}'' results in a local value
   199   that may be used in the subsequent proof as any other variable or
   200   constant.  Furthermore, any result \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} exported from
   201   the context will be universally closed wrt.\ \isa{x} at the
   202   outermost level: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} (this is expressed in normal
   203   form using Isabelle's meta-variables).
   204 
   205   Similarly, introducing some assumption \isa{{\isaliteral{5C3C6368693E}{\isasymchi}}} has two effects.
   206   On the one hand, a local theorem is created that may be used as a
   207   fact in subsequent proof steps.  On the other hand, any result
   208   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6368693E}{\isasymchi}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} exported from the context becomes conditional wrt.\
   209   the assumption: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C6368693E}{\isasymchi}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}.  Thus, solving an enclosing goal
   210   using such a result would basically introduce a new subgoal stemming
   211   from the assumption.  How this situation is handled depends on the
   212   version of assumption command used: while \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}
   213   insists on solving the subgoal by unification with some premise of
   214   the goal, \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves the subgoal unchanged in order
   215   to be proved later by the user.
   216 
   217   Local definitions, introduced by ``\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}'', are achieved by combining ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}'' with
   218   another version of assumption that causes any hypothetical equation
   219   \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} to be eliminated by the reflexivity rule.  Thus,
   220   exporting some result \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} yields \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
   221 
   222   \begin{railoutput}
   223 \rail@begin{2}{}
   224 \rail@term{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}}[]
   225 \rail@plus
   226 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
   227 \rail@nextplus{1}
   228 \rail@cterm{\isa{\isakeyword{and}}}[]
   229 \rail@endplus
   230 \rail@end
   231 \rail@begin{2}{}
   232 \rail@bar
   233 \rail@term{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}}[]
   234 \rail@nextbar{1}
   235 \rail@term{\hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}}[]
   236 \rail@endbar
   237 \rail@plus
   238 \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]
   239 \rail@nextplus{1}
   240 \rail@cterm{\isa{\isakeyword{and}}}[]
   241 \rail@endplus
   242 \rail@end
   243 \rail@begin{2}{}
   244 \rail@term{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}}[]
   245 \rail@plus
   246 \rail@nont{\isa{def}}[]
   247 \rail@nextplus{1}
   248 \rail@cterm{\isa{\isakeyword{and}}}[]
   249 \rail@endplus
   250 \rail@end
   251 \rail@begin{5}{\isa{def}}
   252 \rail@bar
   253 \rail@nextbar{1}
   254 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
   255 \rail@endbar
   256 \rail@cr{3}
   257 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   258 \rail@bar
   259 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
   260 \rail@nextbar{4}
   261 \rail@term{\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}}[]
   262 \rail@endbar
   263 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
   264 \rail@bar
   265 \rail@nextbar{4}
   266 \rail@nont{\hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
   267 \rail@endbar
   268 \rail@end
   269 \end{railoutput}
   270 
   271 
   272   \begin{description}
   273   
   274   \item \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x} introduces a local variable \isa{x} that is \emph{arbitrary, but fixed.}
   275   
   276   \item \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} introduce a local fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} by
   277   assumption.  Subsequent results applied to an enclosing goal (e.g.\
   278   by \indexref{}{command}{show}\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}) are handled as follows: \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} expects to be able to unify with existing premises in the
   279   goal, while \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as new subgoals.
   280   
   281   Several lists of assumptions may be given (separated by
   282   \indexref{}{keyword}{and}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}; the resulting list of current facts consists
   283   of all of these concatenated.
   284   
   285   \item \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} introduces a local
   286   (non-polymorphic) definition.  In results exported from the context,
   287   \isa{x} is replaced by \isa{t}.  Basically, ``\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}'', with the resulting
   288   hypothetical equation solved by reflexivity.
   289   
   290   The default name for the definitional equation is \isa{x{\isaliteral{5F}{\isacharunderscore}}def}.
   291   Several simultaneous definitions may be given at the same time.
   292 
   293   \end{description}
   294 
   295   The special name \indexref{}{fact}{prems}\hyperlink{fact.prems}{\mbox{\isa{prems}}} refers to all assumptions of the
   296   current context as a list of theorems.  This feature should be used
   297   with great care!  It is better avoided in final proof texts.%
   298 \end{isamarkuptext}%
   299 \isamarkuptrue%
   300 %
   301 \isamarkupsubsection{Term abbreviations \label{sec:term-abbrev}%
   302 }
   303 \isamarkuptrue%
   304 %
   305 \begin{isamarkuptext}%
   306 \begin{matharray}{rcl}
   307     \indexdef{}{command}{let}\hypertarget{command.let}{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   308     \indexdef{}{keyword}{is}\hypertarget{keyword.is}{\hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}}} & : & syntax \\
   309   \end{matharray}
   310 
   311   Abbreviations may be either bound by explicit \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} statements, or by annotating assumptions or
   312   goal statements with a list of patterns ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C49533E}{\isasymIS}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''.  In both cases, higher-order matching is invoked to
   313   bind extra-logical term variables, which may be either named
   314   schematic variables of the form \isa{{\isaliteral{3F}{\isacharquery}}x}, or nameless dummies
   315   ``\hyperlink{variable.underscore}{\mbox{\isa{{\isaliteral{5F}{\isacharunderscore}}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
   316   form the patterns occur on the left-hand side, while the \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns are in postfix position.
   317 
   318   Polymorphism of term bindings is handled in Hindley-Milner style,
   319   similar to ML.  Type variables referring to local assumptions or
   320   open goal statements are \emph{fixed}, while those of finished
   321   results or bound by \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} may occur in \emph{arbitrary}
   322   instances later.  Even though actual polymorphism should be rarely
   323   used in practice, this mechanism is essential to achieve proper
   324   incremental type-inference, as the user proceeds to build up the
   325   Isar proof text from left to right.
   326 
   327   \medskip Term abbreviations are quite different from local
   328   definitions as introduced via \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} (see
   329   \secref{sec:proof-context}).  The latter are visible within the
   330   logic as actual equations, while abbreviations disappear during the
   331   input process just after type checking.  Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
   332 
   333   \begin{railoutput}
   334 \rail@begin{3}{}
   335 \rail@term{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}}[]
   336 \rail@plus
   337 \rail@plus
   338 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
   339 \rail@nextplus{1}
   340 \rail@cterm{\isa{\isakeyword{and}}}[]
   341 \rail@endplus
   342 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
   343 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
   344 \rail@nextplus{2}
   345 \rail@cterm{\isa{\isakeyword{and}}}[]
   346 \rail@endplus
   347 \rail@end
   348 \end{railoutput}
   349 
   350 
   351   The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}} or
   352   \hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}} (see \secref{sec:term-decls}).
   353 
   354   \begin{description}
   355 
   356   \item \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} binds any
   357   text variables in patterns \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} by simultaneous
   358   higher-order matching against terms \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
   359 
   360   \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C49533E}{\isasymIS}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} resembles \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}, but
   361   matches \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} against the preceding statement.  Also
   362   note that \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} is not a separate command, but part of
   363   others (such as \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} etc.).
   364 
   365   \end{description}
   366 
   367   Some \emph{implicit} term abbreviations\index{term abbreviations}
   368   for goals and facts are available as well.  For any open goal,
   369   \indexref{}{variable}{thesis}\hyperlink{variable.thesis}{\mbox{\isa{thesis}}} refers to its object-level statement,
   370   abstracted over any meta-level parameters (if present).  Likewise,
   371   \indexref{}{variable}{this}\hyperlink{variable.this}{\mbox{\isa{this}}} is bound for fact statements resulting from
   372   assumptions or finished goals.  In case \hyperlink{variable.this}{\mbox{\isa{this}}} refers to
   373   an object-logic statement that is an application \isa{{\isaliteral{22}{\isachardoublequote}}f\ t{\isaliteral{22}{\isachardoublequote}}}, then
   374   \isa{t} is bound to the special text variable ``\hyperlink{variable.dots}{\mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}}}''
   375   (three dots).  The canonical application of this convenience are
   376   calculational proofs (see \secref{sec:calculation}).%
   377 \end{isamarkuptext}%
   378 \isamarkuptrue%
   379 %
   380 \isamarkupsubsection{Facts and forward chaining%
   381 }
   382 \isamarkuptrue%
   383 %
   384 \begin{isamarkuptext}%
   385 \begin{matharray}{rcl}
   386     \indexdef{}{command}{note}\hypertarget{command.note}{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   387     \indexdef{}{command}{then}\hypertarget{command.then}{\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   388     \indexdef{}{command}{from}\hypertarget{command.from}{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   389     \indexdef{}{command}{with}\hypertarget{command.with}{\hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   390     \indexdef{}{command}{using}\hypertarget{command.using}{\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   391     \indexdef{}{command}{unfolding}\hypertarget{command.unfolding}{\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   392   \end{matharray}
   393 
   394   New facts are established either by assumption or proof of local
   395   statements.  Any fact will usually be involved in further proofs,
   396   either as explicit arguments of proof methods, or when forward
   397   chaining towards the next goal via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} (and variants);
   398   \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}} and \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}} are composite forms
   399   involving \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}.  The \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} elements
   400   augments the collection of used facts \emph{after} a goal has been
   401   stated.  Note that the special theorem name \indexref{}{fact}{this}\hyperlink{fact.this}{\mbox{\isa{this}}} refers
   402   to the most recently established facts, but only \emph{before}
   403   issuing a follow-up claim.
   404 
   405   \begin{railoutput}
   406 \rail@begin{3}{}
   407 \rail@term{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}}[]
   408 \rail@plus
   409 \rail@bar
   410 \rail@nextbar{1}
   411 \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[]
   412 \rail@endbar
   413 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   414 \rail@nextplus{2}
   415 \rail@cterm{\isa{\isakeyword{and}}}[]
   416 \rail@endplus
   417 \rail@end
   418 \rail@begin{4}{}
   419 \rail@bar
   420 \rail@term{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}}[]
   421 \rail@nextbar{1}
   422 \rail@term{\hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}}[]
   423 \rail@nextbar{2}
   424 \rail@term{\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}}[]
   425 \rail@nextbar{3}
   426 \rail@term{\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}}[]
   427 \rail@endbar
   428 \rail@plus
   429 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   430 \rail@nextplus{1}
   431 \rail@cterm{\isa{\isakeyword{and}}}[]
   432 \rail@endplus
   433 \rail@end
   434 \end{railoutput}
   435 
   436 
   437   \begin{description}
   438 
   439   \item \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} recalls existing facts
   440   \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, binding the result as \isa{a}.  Note that
   441   attributes may be involved as well, both on the left and right hand
   442   sides.
   443 
   444   \item \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} indicates forward chaining by the current
   445   facts in order to establish the goal to be claimed next.  The
   446   initial proof method invoked to refine that will be offered the
   447   facts to do ``anything appropriate'' (see also
   448   \secref{sec:proof-steps}).  For example, method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}
   449   (see \secref{sec:pure-meth-att}) would typically do an elimination
   450   rather than an introduction.  Automatic methods usually insert the
   451   facts into the goal state before operation.  This provides a simple
   452   scheme to control relevance of facts in automated proof search.
   453   
   454   \item \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{b} abbreviates ``\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{b}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}''; thus \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} is
   455   equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}''.
   456   
   457   \item \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} abbreviates ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ this{\isaliteral{22}{\isachardoublequote}}}''; thus the forward chaining
   458   is from earlier facts together with the current ones.
   459   
   460   \item \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} augments the facts being
   461   currently indicated for use by a subsequent refinement step (such as
   462   \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} or \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).
   463   
   464   \item \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} is structurally
   465   similar to \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}, but unfolds definitional equations
   466   \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} throughout the goal state and facts.
   467 
   468   \end{description}
   469 
   470   Forward chaining with an empty list of theorems is the same as not
   471   chaining at all.  Thus ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{nothing}'' has no
   472   effect apart from entering \isa{{\isaliteral{22}{\isachardoublequote}}prove{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} mode, since
   473   \indexref{}{fact}{nothing}\hyperlink{fact.nothing}{\mbox{\isa{nothing}}} is bound to the empty list of theorems.
   474 
   475   Basic proof methods (such as \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}) expect multiple
   476   facts to be given in their proper order, corresponding to a prefix
   477   of the premises of the rule involved.  Note that positions may be
   478   easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ b{\isaliteral{22}{\isachardoublequote}}}, for example.  This involves the trivial rule
   479   \isa{{\isaliteral{22}{\isachardoublequote}}PROP\ {\isaliteral{5C3C7073693E}{\isasympsi}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ PROP\ {\isaliteral{5C3C7073693E}{\isasympsi}}{\isaliteral{22}{\isachardoublequote}}}, which is bound in Isabelle/Pure as
   480   ``\indexref{}{fact}{\_}\hyperlink{fact.underscore}{\mbox{\isa{{\isaliteral{5F}{\isacharunderscore}}}}}'' (underscore).
   481 
   482   Automated methods (such as \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.auto}{\mbox{\isa{auto}}}) just
   483   insert any given facts before their usual operation.  Depending on
   484   the kind of procedure involved, the order of facts is less
   485   significant here.%
   486 \end{isamarkuptext}%
   487 \isamarkuptrue%
   488 %
   489 \isamarkupsubsection{Goals \label{sec:goals}%
   490 }
   491 \isamarkuptrue%
   492 %
   493 \begin{isamarkuptext}%
   494 \begin{matharray}{rcl}
   495     \indexdef{}{command}{lemma}\hypertarget{command.lemma}{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   496     \indexdef{}{command}{theorem}\hypertarget{command.theorem}{\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   497     \indexdef{}{command}{corollary}\hypertarget{command.corollary}{\hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   498     \indexdef{}{command}{schematic\_lemma}\hypertarget{command.schematic-lemma}{\hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}lemma}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   499     \indexdef{}{command}{schematic\_theorem}\hypertarget{command.schematic-theorem}{\hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}theorem}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   500     \indexdef{}{command}{schematic\_corollary}\hypertarget{command.schematic-corollary}{\hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}corollary}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   501     \indexdef{}{command}{have}\hypertarget{command.have}{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   502     \indexdef{}{command}{show}\hypertarget{command.show}{\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   503     \indexdef{}{command}{hence}\hypertarget{command.hence}{\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   504     \indexdef{}{command}{thus}\hypertarget{command.thus}{\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   505     \indexdef{}{command}{print\_statement}\hypertarget{command.print-statement}{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
   506   \end{matharray}
   507 
   508   From a theory context, proof mode is entered by an initial goal
   509   command such as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}, \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, or
   510   \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}.  Within a proof, new claims may be
   511   introduced locally as well; four variants are available here to
   512   indicate whether forward chaining of facts should be performed
   513   initially (via \indexref{}{command}{then}\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}), and whether the final result
   514   is meant to solve some pending goal.
   515 
   516   Goals may consist of multiple statements, resulting in a list of
   517   facts eventually.  A pending multi-goal is internally represented as
   518   a meta-level conjunction (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{22}{\isachardoublequote}}}), which is usually
   519   split into the corresponding number of sub-goals prior to an initial
   520   method application, via \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}
   521   (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}
   522   (\secref{sec:tactic-commands}).  The \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}} method
   523   covered in \secref{sec:cases-induct} acts on multiple claims
   524   simultaneously.
   525 
   526   Claims at the theory level may be either in short or long form.  A
   527   short goal merely consists of several simultaneous propositions
   528   (often just one).  A long goal includes an explicit context
   529   specification for the subsequent conclusion, involving local
   530   parameters and assumptions.  Here the role of each part of the
   531   statement is explicitly marked by separate keywords (see also
   532   \secref{sec:locale}); the local assumptions being introduced here
   533   are available as \indexref{}{fact}{assms}\hyperlink{fact.assms}{\mbox{\isa{assms}}} in the proof.  Moreover, there
   534   are two kinds of conclusions: \indexdef{}{element}{shows}\hypertarget{element.shows}{\hyperlink{element.shows}{\mbox{\isa{\isakeyword{shows}}}}} states several
   535   simultaneous propositions (essentially a big conjunction), while
   536   \indexdef{}{element}{obtains}\hypertarget{element.obtains}{\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}}} claims several simultaneous simultaneous
   537   contexts of (essentially a big disjunction of eliminated parameters
   538   and assumptions, cf.\ \secref{sec:obtain}).
   539 
   540   \begin{railoutput}
   541 \rail@begin{6}{}
   542 \rail@bar
   543 \rail@term{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}}[]
   544 \rail@nextbar{1}
   545 \rail@term{\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}}[]
   546 \rail@nextbar{2}
   547 \rail@term{\hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}}[]
   548 \rail@nextbar{3}
   549 \rail@term{\hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}lemma}}}}}[]
   550 \rail@nextbar{4}
   551 \rail@term{\hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}theorem}}}}}[]
   552 \rail@nextbar{5}
   553 \rail@term{\hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}corollary}}}}}[]
   554 \rail@endbar
   555 \rail@bar
   556 \rail@nextbar{1}
   557 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
   558 \rail@endbar
   559 \rail@bar
   560 \rail@nont{\isa{goal}}[]
   561 \rail@nextbar{1}
   562 \rail@nont{\isa{longgoal}}[]
   563 \rail@endbar
   564 \rail@end
   565 \rail@begin{4}{}
   566 \rail@bar
   567 \rail@term{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}}[]
   568 \rail@nextbar{1}
   569 \rail@term{\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}}[]
   570 \rail@nextbar{2}
   571 \rail@term{\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}}}[]
   572 \rail@nextbar{3}
   573 \rail@term{\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}}}[]
   574 \rail@endbar
   575 \rail@nont{\isa{goal}}[]
   576 \rail@end
   577 \rail@begin{2}{}
   578 \rail@term{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}[]
   579 \rail@bar
   580 \rail@nextbar{1}
   581 \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
   582 \rail@endbar
   583 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   584 \rail@end
   585 \rail@begin{2}{\isa{goal}}
   586 \rail@plus
   587 \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]
   588 \rail@nextplus{1}
   589 \rail@cterm{\isa{\isakeyword{and}}}[]
   590 \rail@endplus
   591 \rail@end
   592 \rail@begin{2}{\isa{longgoal}}
   593 \rail@bar
   594 \rail@nextbar{1}
   595 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
   596 \rail@endbar
   597 \rail@plus
   598 \rail@nextplus{1}
   599 \rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
   600 \rail@endplus
   601 \rail@nont{\isa{conclusion}}[]
   602 \rail@end
   603 \rail@begin{4}{\isa{conclusion}}
   604 \rail@bar
   605 \rail@term{\isa{\isakeyword{shows}}}[]
   606 \rail@nont{\isa{goal}}[]
   607 \rail@nextbar{1}
   608 \rail@term{\isa{\isakeyword{obtains}}}[]
   609 \rail@plus
   610 \rail@bar
   611 \rail@nextbar{2}
   612 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
   613 \rail@endbar
   614 \rail@nont{\isa{case}}[]
   615 \rail@nextplus{3}
   616 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
   617 \rail@endplus
   618 \rail@endbar
   619 \rail@end
   620 \rail@begin{2}{\isa{case}}
   621 \rail@plus
   622 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
   623 \rail@nextplus{1}
   624 \rail@cterm{\isa{\isakeyword{and}}}[]
   625 \rail@endplus
   626 \rail@term{\isa{\isakeyword{where}}}[]
   627 \rail@plus
   628 \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]
   629 \rail@nextplus{1}
   630 \rail@cterm{\isa{\isakeyword{and}}}[]
   631 \rail@endplus
   632 \rail@end
   633 \end{railoutput}
   634 
   635 
   636   \begin{description}
   637   
   638   \item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} enters proof mode with
   639   \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as main goal, eventually resulting in some fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} to be put back into the target context.  An additional \hyperlink{syntax.context}{\mbox{\isa{context}}} specification may build up an initial proof context for the
   640   subsequent claim; this includes local definitions and syntax as
   641   well, see the definition of \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in
   642   \secref{sec:locale}.
   643   
   644   \item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}, but the facts are internally marked as
   645   being of a different kind.  This discrimination acts like a formal
   646   comment.
   647 
   648   \item \hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}lemma}}}}, \hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}theorem}}}},
   649   \hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isaliteral{5F}{\isacharunderscore}}corollary}}}} are similar to \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}},
   650   \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}, respectively but allow
   651   the statement to contain unbound schematic variables.
   652 
   653   Under normal circumstances, an Isar proof text needs to specify
   654   claims explicitly.  Schematic goals are more like goals in Prolog,
   655   where certain results are synthesized in the course of reasoning.
   656   With schematic statements, the inherent compositionality of Isar
   657   proofs is lost, which also impacts performance, because proof
   658   checking is forced into sequential mode.
   659   
   660   \item \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} claims a local goal,
   661   eventually resulting in a fact within the current logical context.
   662   This operation is completely independent of any pending sub-goals of
   663   an enclosing goal statements, so \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} may be freely
   664   used for experimental exploration of potential results within a
   665   proof body.
   666   
   667   \item \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} is like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} plus a second stage to refine some pending
   668   sub-goal for each one of the finished result, after having been
   669   exported into the corresponding context (at the head of the
   670   sub-proof of this \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} command).
   671   
   672   To accommodate interactive debugging, resulting rules are printed
   673   before being applied internally.  Even more, interactive execution
   674   of \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} predicts potential failure and displays the
   675   resulting error as a warning beforehand.  Watch out for the
   676   following message:
   677 
   678   %FIXME proper antiquitation
   679   \begin{ttbox}
   680   Problem! Local statement will fail to solve any pending goal
   681   \end{ttbox}
   682   
   683   \item \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} abbreviates ``\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}'', i.e.\ claims a local goal to be proven by forward
   684   chaining the current facts.  Note that \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} is also
   685   equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}''.
   686   
   687   \item \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} abbreviates ``\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''.  Note that \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} is also equivalent to
   688   ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''.
   689   
   690   \item \hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}~\isa{a} prints facts from the
   691   current theory or proof context in long statement form, according to
   692   the syntax for \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} given above.
   693 
   694   \end{description}
   695 
   696   Any goal statement causes some term abbreviations (such as
   697   \indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}thesis}}}) to be bound automatically, see also
   698   \secref{sec:term-abbrev}.
   699 
   700   The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold
   701   meaning: (1) during the of this claim they refer to the the local
   702   context introductions, (2) the resulting rule is annotated
   703   accordingly to support symbolic case splits when used with the
   704   \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).%
   705 \end{isamarkuptext}%
   706 \isamarkuptrue%
   707 %
   708 \isamarkupsection{Refinement steps%
   709 }
   710 \isamarkuptrue%
   711 %
   712 \isamarkupsubsection{Proof method expressions \label{sec:proof-meth}%
   713 }
   714 \isamarkuptrue%
   715 %
   716 \begin{isamarkuptext}%
   717 Proof methods are either basic ones, or expressions composed
   718   of methods via ``\verb|,|'' (sequential composition),
   719   ``\verb||\verb,|,\verb||'' (alternative choices), ``\verb|?|''
   720   (try), ``\verb|+|'' (repeat at least once), ``\verb|[|\isa{n}\verb|]|'' (restriction to first \isa{n}
   721   sub-goals, with default \isa{{\isaliteral{22}{\isachardoublequote}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}).  In practice, proof
   722   methods are usually just a comma separated list of \hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}~\hyperlink{syntax.args}{\mbox{\isa{args}}} specifications.  Note that parentheses may
   723   be dropped for single method specifications (with no arguments).
   724 
   725   \begin{railoutput}
   726 \rail@begin{5}{\indexdef{}{syntax}{method}\hypertarget{syntax.method}{\hyperlink{syntax.method}{\mbox{\isa{method}}}}}
   727 \rail@bar
   728 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
   729 \rail@nextbar{1}
   730 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
   731 \rail@nont{\isa{methods}}[]
   732 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
   733 \rail@endbar
   734 \rail@bar
   735 \rail@nextbar{1}
   736 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
   737 \rail@nextbar{2}
   738 \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
   739 \rail@nextbar{3}
   740 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
   741 \rail@bar
   742 \rail@nextbar{4}
   743 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   744 \rail@endbar
   745 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
   746 \rail@endbar
   747 \rail@end
   748 \rail@begin{4}{\isa{methods}}
   749 \rail@plus
   750 \rail@bar
   751 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
   752 \rail@nont{\hyperlink{syntax.args}{\mbox{\isa{args}}}}[]
   753 \rail@nextbar{1}
   754 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
   755 \rail@endbar
   756 \rail@nextplus{2}
   757 \rail@bar
   758 \rail@term{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
   759 \rail@nextbar{3}
   760 \rail@term{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
   761 \rail@endbar
   762 \rail@endplus
   763 \rail@end
   764 \end{railoutput}
   765 
   766 
   767   Proper Isar proof methods do \emph{not} admit arbitrary goal
   768   addressing, but refer either to the first sub-goal or all sub-goals
   769   uniformly.  The goal restriction operator ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}''
   770   evaluates a method expression within a sandbox consisting of the
   771   first \isa{n} sub-goals (which need to exist).  For example, the
   772   method ``\isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{5B}{\isacharbrackleft}}{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}'' simplifies the first three
   773   sub-goals, while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}rule\ foo{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}'' simplifies all
   774   new goals that emerge from applying rule \isa{{\isaliteral{22}{\isachardoublequote}}foo{\isaliteral{22}{\isachardoublequote}}} to the
   775   originally first one.
   776 
   777   Improper methods, notably tactic emulations, offer a separate
   778   low-level goal addressing scheme as explicit argument to the
   779   individual tactic being involved.  Here ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}'' refers to
   780   all goals, and ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{2D}{\isacharminus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}'' to all goals starting from \isa{{\isaliteral{22}{\isachardoublequote}}n{\isaliteral{22}{\isachardoublequote}}}.
   781 
   782   \begin{railoutput}
   783 \rail@begin{4}{\indexdef{}{syntax}{goal\_spec}\hypertarget{syntax.goal-spec}{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}}
   784 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
   785 \rail@bar
   786 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   787 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
   788 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   789 \rail@nextbar{1}
   790 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   791 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
   792 \rail@nextbar{2}
   793 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   794 \rail@nextbar{3}
   795 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
   796 \rail@endbar
   797 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
   798 \rail@end
   799 \end{railoutput}%
   800 \end{isamarkuptext}%
   801 \isamarkuptrue%
   802 %
   803 \isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}%
   804 }
   805 \isamarkuptrue%
   806 %
   807 \begin{isamarkuptext}%
   808 \begin{matharray}{rcl}
   809     \indexdef{}{command}{proof}\hypertarget{command.proof}{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   810     \indexdef{}{command}{qed}\hypertarget{command.qed}{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   811     \indexdef{}{command}{by}\hypertarget{command.by}{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   812     \indexdef{}{command}{..}\hypertarget{command.ddot}{\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   813     \indexdef{}{command}{.}\hypertarget{command.dot}{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   814     \indexdef{}{command}{sorry}\hypertarget{command.sorry}{\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
   815   \end{matharray}
   816 
   817   Arbitrary goal refinement via tactics is considered harmful.
   818   Structured proof composition in Isar admits proof methods to be
   819   invoked in two places only.
   820 
   821   \begin{enumerate}
   822 
   823   \item An \emph{initial} refinement step \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} reduces a newly stated goal to a number
   824   of sub-goals that are to be solved later.  Facts are passed to
   825   \isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} for forward chaining, if so indicated by \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} mode.
   826   
   827   \item A \emph{terminal} conclusion step \indexref{}{command}{qed}\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} is intended to solve remaining goals.  No facts are
   828   passed to \isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}.
   829 
   830   \end{enumerate}
   831 
   832   The only other (proper) way to affect pending goals in a proof body
   833   is by \indexref{}{command}{show}\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, which involves an explicit statement of
   834   what is to be solved eventually.  Thus we avoid the fundamental
   835   problem of unstructured tactic scripts that consist of numerous
   836   consecutive goal transformations, with invisible effects.
   837 
   838   \medskip As a general rule of thumb for good proof style, initial
   839   proof methods should either solve the goal completely, or constitute
   840   some well-understood reduction to new sub-goals.  Arbitrary
   841   automatic proof tools that are prone leave a large number of badly
   842   structured sub-goals are no help in continuing the proof document in
   843   an intelligible manner.
   844 
   845   Unless given explicitly by the user, the default initial method is
   846   \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} (or its classical variant \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}), which applies a single standard elimination or introduction
   847   rule according to the topmost symbol involved.  There is no separate
   848   default terminal method.  Any remaining goals are always solved by
   849   assumption in the very last step.
   850 
   851   \begin{railoutput}
   852 \rail@begin{2}{}
   853 \rail@term{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}}[]
   854 \rail@bar
   855 \rail@nextbar{1}
   856 \rail@nont{\isa{method}}[]
   857 \rail@endbar
   858 \rail@end
   859 \rail@begin{2}{}
   860 \rail@term{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}}[]
   861 \rail@bar
   862 \rail@nextbar{1}
   863 \rail@nont{\isa{method}}[]
   864 \rail@endbar
   865 \rail@end
   866 \rail@begin{2}{}
   867 \rail@term{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}}[]
   868 \rail@nont{\isa{method}}[]
   869 \rail@bar
   870 \rail@nextbar{1}
   871 \rail@nont{\isa{method}}[]
   872 \rail@endbar
   873 \rail@end
   874 \rail@begin{3}{}
   875 \rail@bar
   876 \rail@term{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}}[]
   877 \rail@nextbar{1}
   878 \rail@term{\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}}[]
   879 \rail@nextbar{2}
   880 \rail@term{\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}}[]
   881 \rail@endbar
   882 \rail@end
   883 \end{railoutput}
   884 
   885 
   886   \begin{description}
   887   
   888   \item \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} refines the goal by proof
   889   method \isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}; facts for forward chaining are passed if so
   890   indicated by \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} mode.
   891   
   892   \item \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} refines any remaining goals by
   893   proof method \isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} and concludes the sub-proof by assumption.
   894   If the goal had been \isa{{\isaliteral{22}{\isachardoublequote}}show{\isaliteral{22}{\isachardoublequote}}} (or \isa{{\isaliteral{22}{\isachardoublequote}}thus{\isaliteral{22}{\isachardoublequote}}}), some
   895   pending sub-goal is solved as well by the rule resulting from the
   896   result \emph{exported} into the enclosing goal context.  Thus \isa{{\isaliteral{22}{\isachardoublequote}}qed{\isaliteral{22}{\isachardoublequote}}} may fail for two reasons: either \isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} fails, or the
   897   resulting rule does not fit to any pending goal\footnote{This
   898   includes any additional ``strong'' assumptions as introduced by
   899   \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}.} of the enclosing context.  Debugging such a
   900   situation might involve temporarily changing \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} into
   901   \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, or weakening the local context by replacing
   902   occurrences of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} by \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}.
   903   
   904   \item \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} is a \emph{terminal
   905   proof}\index{proof!terminal}; it abbreviates \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}, but with
   906   backtracking across both methods.  Debugging an unsuccessful
   907   \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} command can be done by expanding its
   908   definition; in many cases \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} (or even
   909   \isa{{\isaliteral{22}{\isachardoublequote}}apply{\isaliteral{22}{\isachardoublequote}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}) is already sufficient to see the
   910   problem.
   911 
   912   \item ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' is a \emph{default
   913   proof}\index{proof!default}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{22}{\isachardoublequote}}}.
   914 
   915   \item ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' is a \emph{trivial
   916   proof}\index{proof!trivial}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}this{\isaliteral{22}{\isachardoublequote}}}.
   917   
   918   \item \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is a \emph{fake proof}\index{proof!fake}
   919   pretending to solve the pending claim without further ado.  This
   920   only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML).  Facts emerging from fake
   921   proofs are not the real thing.  Internally, each theorem container
   922   is tainted by an oracle invocation, which is indicated as ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}'' in the printed result.
   923   
   924   The most important application of \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is to support
   925   experimentation and top-down proof development.
   926 
   927   \end{description}%
   928 \end{isamarkuptext}%
   929 \isamarkuptrue%
   930 %
   931 \isamarkupsubsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
   932 }
   933 \isamarkuptrue%
   934 %
   935 \begin{isamarkuptext}%
   936 The following proof methods and attributes refer to basic logical
   937   operations of Isar.  Further methods and attributes are provided by
   938   several generic and object-logic specific tools and packages (see
   939   \chref{ch:gen-tools} and \chref{ch:hol}).
   940 
   941   \begin{matharray}{rcl}
   942     \indexdef{}{method}{-}\hypertarget{method.-}{\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}} & : & \isa{method} \\
   943     \indexdef{}{method}{fact}\hypertarget{method.fact}{\hyperlink{method.fact}{\mbox{\isa{fact}}}} & : & \isa{method} \\
   944     \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
   945     \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
   946     \indexdef{Pure}{method}{rule}\hypertarget{method.Pure.rule}{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
   947     \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
   948     \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
   949     \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
   950     \indexdef{Pure}{attribute}{rule}\hypertarget{attribute.Pure.rule}{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
   951     \indexdef{}{attribute}{OF}\hypertarget{attribute.OF}{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}} & : & \isa{attribute} \\
   952     \indexdef{}{attribute}{of}\hypertarget{attribute.of}{\hyperlink{attribute.of}{\mbox{\isa{of}}}} & : & \isa{attribute} \\
   953     \indexdef{}{attribute}{where}\hypertarget{attribute.where}{\hyperlink{attribute.where}{\mbox{\isa{where}}}} & : & \isa{attribute} \\
   954   \end{matharray}
   955 
   956   \begin{railoutput}
   957 \rail@begin{2}{}
   958 \rail@term{\hyperlink{method.fact}{\mbox{\isa{fact}}}}[]
   959 \rail@bar
   960 \rail@nextbar{1}
   961 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   962 \rail@endbar
   963 \rail@end
   964 \rail@begin{2}{}
   965 \rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
   966 \rail@bar
   967 \rail@nextbar{1}
   968 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   969 \rail@endbar
   970 \rail@end
   971 \rail@begin{4}{\isa{rulemod}}
   972 \rail@bar
   973 \rail@term{\isa{intro}}[]
   974 \rail@nextbar{1}
   975 \rail@term{\isa{elim}}[]
   976 \rail@nextbar{2}
   977 \rail@term{\isa{dest}}[]
   978 \rail@endbar
   979 \rail@bar
   980 \rail@bar
   981 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
   982 \rail@nextbar{1}
   983 \rail@nextbar{2}
   984 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
   985 \rail@endbar
   986 \rail@bar
   987 \rail@nextbar{1}
   988 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   989 \rail@endbar
   990 \rail@nextbar{3}
   991 \rail@term{\isa{del}}[]
   992 \rail@endbar
   993 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
   994 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   995 \rail@end
   996 \rail@begin{3}{}
   997 \rail@bar
   998 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
   999 \rail@nextbar{1}
  1000 \rail@term{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}}[]
  1001 \rail@nextbar{2}
  1002 \rail@term{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}}[]
  1003 \rail@endbar
  1004 \rail@bar
  1005 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
  1006 \rail@nextbar{1}
  1007 \rail@nextbar{2}
  1008 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
  1009 \rail@endbar
  1010 \rail@bar
  1011 \rail@nextbar{1}
  1012 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
  1013 \rail@endbar
  1014 \rail@end
  1015 \rail@begin{1}{}
  1016 \rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
  1017 \rail@term{\isa{del}}[]
  1018 \rail@end
  1019 \rail@begin{1}{}
  1020 \rail@term{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}}[]
  1021 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
  1022 \rail@end
  1023 \rail@begin{2}{}
  1024 \rail@term{\hyperlink{attribute.of}{\mbox{\isa{of}}}}[]
  1025 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
  1026 \rail@bar
  1027 \rail@nextbar{1}
  1028 \rail@term{\isa{concl}}[]
  1029 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
  1030 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
  1031 \rail@endbar
  1032 \rail@end
  1033 \rail@begin{6}{}
  1034 \rail@term{\hyperlink{attribute.where}{\mbox{\isa{where}}}}[]
  1035 \rail@bar
  1036 \rail@nextbar{1}
  1037 \rail@plus
  1038 \rail@bar
  1039 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1040 \rail@nextbar{2}
  1041 \rail@nont{\hyperlink{syntax.var}{\mbox{\isa{var}}}}[]
  1042 \rail@nextbar{3}
  1043 \rail@nont{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}}[]
  1044 \rail@nextbar{4}
  1045 \rail@nont{\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}}}[]
  1046 \rail@endbar
  1047 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
  1048 \rail@bar
  1049 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
  1050 \rail@nextbar{2}
  1051 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
  1052 \rail@endbar
  1053 \rail@nextplus{5}
  1054 \rail@cterm{\isa{\isakeyword{and}}}[]
  1055 \rail@endplus
  1056 \rail@endbar
  1057 \rail@end
  1058 \end{railoutput}
  1059 
  1060 
  1061   \begin{description}
  1062   
  1063   \item ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}'' (minus) does nothing but insert the forward
  1064   chaining facts as premises into the goal.  Note that command
  1065   \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} without any method actually performs a single
  1066   reduction step using the \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method; thus a plain
  1067   \emph{do-nothing} proof step would be ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' rather than \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} alone.
  1068   
  1069   \item \hyperlink{method.fact}{\mbox{\isa{fact}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} composes some fact from
  1070   \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} (or implicitly from the current proof context)
  1071   modulo unification of schematic type and term variables.  The rule
  1072   structure is not taken into account, i.e.\ meta-level implication is
  1073   considered atomic.  This is the same principle underlying literal
  1074   facts (cf.\ \secref{sec:syn-att}): ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{fact}'' is equivalent to ``\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\verb|`|\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}\verb|`|'' provided that
  1075   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} is an instance of some known \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} in the
  1076   proof context.
  1077   
  1078   \item \hyperlink{method.assumption}{\mbox{\isa{assumption}}} solves some goal by a single assumption
  1079   step.  All given facts are guaranteed to participate in the
  1080   refinement; this means there may be only 0 or 1 in the first place.
  1081   Recall that \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} (\secref{sec:proof-steps}) already
  1082   concludes any remaining sub-goals by assumption, so structured
  1083   proofs usually need not quote the \hyperlink{method.assumption}{\mbox{\isa{assumption}}} method at
  1084   all.
  1085   
  1086   \item \hyperlink{method.this}{\mbox{\isa{this}}} applies all of the current facts directly as
  1087   rules.  Recall that ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' (dot) abbreviates ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{this}''.
  1088   
  1089   \item \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some rule given as
  1090   argument in backward manner; facts are used to reduce the rule
  1091   before applying it to the goal.  Thus \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} without facts
  1092   is plain introduction, while with facts it becomes elimination.
  1093   
  1094   When no arguments are given, the \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method tries to pick
  1095   appropriate rules automatically, as declared in the current context
  1096   using the \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}},
  1097   \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} attributes (see below).  This is the
  1098   default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' 
  1099   (double-dot) steps (see \secref{sec:proof-steps}).
  1100   
  1101   \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
  1102   \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
  1103   destruct rules, to be used with method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}, and similar
  1104   tools.  Note that the latter will ignore rules declared with
  1105   ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'', while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}''  are used most aggressively.
  1106   
  1107   The classical reasoner (see \secref{sec:classical}) introduces its
  1108   own variants of these attributes; use qualified names to access the
  1109   present versions of Isabelle/Pure, i.e.\ \hyperlink{attribute.Pure.Pure.intro}{\mbox{\isa{Pure{\isaliteral{2E}{\isachardot}}intro}}}.
  1110   
  1111   \item \hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
  1112   elimination, or destruct rules.
  1113   
  1114   \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some
  1115   theorem to all of the given rules \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
  1116   (in parallel).  This corresponds to the \verb|op MRS| operation in
  1117   ML, but note the reversed order.  Positions may be effectively
  1118   skipped by including ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' (underscore) as argument.
  1119   
  1120   \item \hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} performs positional
  1121   instantiation of term variables.  The terms \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are
  1122   substituted for any schematic variables occurring in a theorem from
  1123   left to right; ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' (underscore) indicates to skip a
  1124   position.  Arguments following a ``\isa{{\isaliteral{22}{\isachardoublequote}}concl{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}'' specification
  1125   refer to positions of the conclusion of a rule.
  1126   
  1127   \item \hyperlink{attribute.where}{\mbox{\isa{where}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
  1128   performs named instantiation of schematic type and term variables
  1129   occurring in a theorem.  Schematic variables have to be specified on
  1130   the left-hand side (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}).  The question mark may
  1131   be omitted if the variable name is a plain identifier without index.
  1132   As type instantiations are inferred from term instantiations,
  1133   explicit type instantiations are seldom necessary.
  1134 
  1135   \end{description}%
  1136 \end{isamarkuptext}%
  1137 \isamarkuptrue%
  1138 %
  1139 \isamarkupsubsection{Emulating tactic scripts \label{sec:tactic-commands}%
  1140 }
  1141 \isamarkuptrue%
  1142 %
  1143 \begin{isamarkuptext}%
  1144 The Isar provides separate commands to accommodate tactic-style
  1145   proof scripts within the same system.  While being outside the
  1146   orthodox Isar proof language, these might come in handy for
  1147   interactive exploration and debugging, or even actual tactical proof
  1148   within new-style theories (to benefit from document preparation, for
  1149   example).  See also \secref{sec:tactics} for actual tactics, that
  1150   have been encapsulated as proof methods.  Proper proof methods may
  1151   be used in scripts, too.
  1152 
  1153   \begin{matharray}{rcl}
  1154     \indexdef{}{command}{apply}\hypertarget{command.apply}{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1155     \indexdef{}{command}{apply\_end}\hypertarget{command.apply-end}{\hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isaliteral{5F}{\isacharunderscore}}end}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1156     \indexdef{}{command}{done}\hypertarget{command.done}{\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1157     \indexdef{}{command}{defer}\hypertarget{command.defer}{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\
  1158     \indexdef{}{command}{prefer}\hypertarget{command.prefer}{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\
  1159     \indexdef{}{command}{back}\hypertarget{command.back}{\hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\
  1160   \end{matharray}
  1161 
  1162   \begin{railoutput}
  1163 \rail@begin{2}{}
  1164 \rail@bar
  1165 \rail@term{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}[]
  1166 \rail@nextbar{1}
  1167 \rail@term{\hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isaliteral{5F}{\isacharunderscore}}end}}}}}[]
  1168 \rail@endbar
  1169 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
  1170 \rail@end
  1171 \rail@begin{2}{}
  1172 \rail@term{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}[]
  1173 \rail@bar
  1174 \rail@nextbar{1}
  1175 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
  1176 \rail@endbar
  1177 \rail@end
  1178 \rail@begin{1}{}
  1179 \rail@term{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}[]
  1180 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
  1181 \rail@end
  1182 \end{railoutput}
  1183 
  1184 
  1185   \begin{description}
  1186 
  1187   \item \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{m} applies proof method \isa{m} in
  1188   initial position, but unlike \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} it retains ``\isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' mode.  Thus consecutive method applications may be
  1189   given just as in tactic scripts.
  1190   
  1191   Facts are passed to \isa{m} as indicated by the goal's
  1192   forward-chain mode, and are \emph{consumed} afterwards.  Thus any
  1193   further \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command would always work in a purely
  1194   backward manner.
  1195   
  1196   \item \hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isaliteral{5F}{\isacharunderscore}}end}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} applies proof method \isa{m} as if in terminal position.  Basically, this simulates a
  1197   multi-step tactic script for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, but may be given
  1198   anywhere within the proof body.
  1199   
  1200   No facts are passed to \isa{m} here.  Furthermore, the static
  1201   context is that of the enclosing goal (as for actual \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).  Thus the proof method may not refer to any assumptions
  1202   introduced in the current body, for example.
  1203   
  1204   \item \hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} completes a proof script, provided that the
  1205   current goal state is solved completely.  Note that actual
  1206   structured proof commands (e.g.\ ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' or \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}) may be used to conclude proof scripts as well.
  1207 
  1208   \item \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}~\isa{n} and \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}~\isa{n}
  1209   shuffle the list of pending goals: \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}} puts off
  1210   sub-goal \isa{n} to the end of the list (\isa{{\isaliteral{22}{\isachardoublequote}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} by
  1211   default), while \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}} brings sub-goal \isa{n} to the
  1212   front.
  1213   
  1214   \item \hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}} does back-tracking over the result sequence
  1215   of the latest proof command.  Basically, any proof command may
  1216   return multiple results.
  1217   
  1218   \end{description}
  1219 
  1220   Any proper Isar proof method may be used with tactic script commands
  1221   such as \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}.  A few additional emulations of actual
  1222   tactics are provided as well; these would be never used in actual
  1223   structured proofs, of course.%
  1224 \end{isamarkuptext}%
  1225 \isamarkuptrue%
  1226 %
  1227 \isamarkupsubsection{Defining proof methods%
  1228 }
  1229 \isamarkuptrue%
  1230 %
  1231 \begin{isamarkuptext}%
  1232 \begin{matharray}{rcl}
  1233     \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1234   \end{matharray}
  1235 
  1236   \begin{railoutput}
  1237 \rail@begin{2}{}
  1238 \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
  1239 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1240 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
  1241 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
  1242 \rail@bar
  1243 \rail@nextbar{1}
  1244 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
  1245 \rail@endbar
  1246 \rail@end
  1247 \end{railoutput}
  1248 
  1249 
  1250   \begin{description}
  1251 
  1252   \item \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ text\ description{\isaliteral{22}{\isachardoublequote}}}
  1253   defines a proof method in the current theory.  The given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} has to be an ML expression of type
  1254   \verb|(Proof.context -> Proof.method) context_parser|, cf.\
  1255   basic parsers defined in structure \verb|Args| and \verb|Attrib|.  There are also combinators like \verb|METHOD| and \verb|SIMPLE_METHOD| to turn certain tactic forms into official proof
  1256   methods; the primed versions refer to tactics with explicit goal
  1257   addressing.
  1258 
  1259   Here are some example method definitions:
  1260 
  1261   \end{description}%
  1262 \end{isamarkuptext}%
  1263 \isamarkuptrue%
  1264 %
  1265 \isadelimML
  1266 \ \ %
  1267 \endisadelimML
  1268 %
  1269 \isatagML
  1270 \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
  1271 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1272 \ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}K\ {\isaliteral{28}{\isacharparenleft}}SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1273 \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ first\ method\ {\isaliteral{28}{\isacharparenleft}}without\ any\ arguments{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
  1274 \isanewline
  1275 \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
  1276 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1277 \ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
  1278 \ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1279 \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ second\ method\ {\isaliteral{28}{\isacharparenleft}}with\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
  1280 \isanewline
  1281 \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
  1282 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1283 \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ thms{\isaliteral{3A}{\isacharcolon}}\ thm\ list\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
  1284 \ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1285 \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ third\ method\ {\isaliteral{28}{\isacharparenleft}}with\ theorem\ arguments\ and\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
  1286 \endisatagML
  1287 {\isafoldML}%
  1288 %
  1289 \isadelimML
  1290 %
  1291 \endisadelimML
  1292 %
  1293 \isamarkupsection{Generalized elimination \label{sec:obtain}%
  1294 }
  1295 \isamarkuptrue%
  1296 %
  1297 \begin{isamarkuptext}%
  1298 \begin{matharray}{rcl}
  1299     \indexdef{}{command}{obtain}\hypertarget{command.obtain}{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1300     \indexdef{}{command}{guess}\hypertarget{command.guess}{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1301   \end{matharray}
  1302 
  1303   Generalized elimination means that additional elements with certain
  1304   properties may be introduced in the current context, by virtue of a
  1305   locally proven ``soundness statement''.  Technically speaking, the
  1306   \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} language element is like a declaration of
  1307   \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} (see also see
  1308   \secref{sec:proof-context}), together with a soundness proof of its
  1309   additional claim.  According to the nature of existential reasoning,
  1310   assumptions get eliminated from any result exported from the context
  1311   later, provided that the corresponding parameters do \emph{not}
  1312   occur in the conclusion.
  1313 
  1314   \begin{railoutput}
  1315 \rail@begin{2}{}
  1316 \rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[]
  1317 \rail@bar
  1318 \rail@nextbar{1}
  1319 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
  1320 \rail@endbar
  1321 \rail@plus
  1322 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
  1323 \rail@nextplus{1}
  1324 \rail@cterm{\isa{\isakeyword{and}}}[]
  1325 \rail@endplus
  1326 \rail@term{\isa{\isakeyword{where}}}[]
  1327 \rail@plus
  1328 \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]
  1329 \rail@nextplus{1}
  1330 \rail@cterm{\isa{\isakeyword{and}}}[]
  1331 \rail@endplus
  1332 \rail@end
  1333 \rail@begin{2}{}
  1334 \rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[]
  1335 \rail@plus
  1336 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
  1337 \rail@nextplus{1}
  1338 \rail@cterm{\isa{\isakeyword{and}}}[]
  1339 \rail@endplus
  1340 \rail@end
  1341 \end{railoutput}
  1342 
  1343 
  1344   The derived Isar command \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} is defined as follows
  1345   (where \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} shall refer to (optional)
  1346   facts indicated for forward chaining).
  1347   \begin{matharray}{l}
  1348     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616E676C653E}{\isasymlangle}}using\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5C3C72616E676C653E}{\isasymrangle}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ \ {\isaliteral{5C3C6C616E676C653E}{\isasymlangle}}proof{\isaliteral{5C3C72616E676C653E}{\isasymrangle}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
  1349     \quad \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}thesis{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}} \\
  1350     \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\hyperlink{method.succeed}{\mbox{\isa{succeed}}} \\
  1351     \qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\
  1352     \qquad \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}that\ {\isaliteral{5B}{\isacharbrackleft}}Pure{\isaliteral{2E}{\isachardot}}intro{\isaliteral{3F}{\isacharquery}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}} \\
  1353     \qquad \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis} \\
  1354     \quad\qquad \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{{\isaliteral{2D}{\isacharminus}}} \\
  1355     \quad\qquad \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ \ {\isaliteral{5C3C6C616E676C653E}{\isasymlangle}}proof{\isaliteral{5C3C72616E676C653E}{\isasymrangle}}{\isaliteral{22}{\isachardoublequote}}} \\
  1356     \quad \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} \\
  1357     \quad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} \\
  1358   \end{matharray}
  1359 
  1360   Typically, the soundness proof is relatively straight-forward, often
  1361   just by canonical automated tools such as ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{simp}'' or ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{blast}''.  Accordingly, the
  1362   ``\isa{that}'' reduction above is declared as simplification and
  1363   introduction rule.
  1364 
  1365   In a sense, \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} represents at the level of Isar
  1366   proofs what would be meta-logical existential quantifiers and
  1367   conjunctions.  This concept has a broad range of useful
  1368   applications, ranging from plain elimination (or introduction) of
  1369   object-level existential and conjunctions, to elimination over
  1370   results of symbolic evaluation of recursive definitions, for
  1371   example.  Also note that \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} without parameters acts
  1372   much like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, where the result is treated as a
  1373   genuine assumption.
  1374 
  1375   An alternative name to be used instead of ``\isa{that}'' above may
  1376   be given in parentheses.
  1377 
  1378   \medskip The improper variant \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} is similar to
  1379   \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}, but derives the obtained statement from the
  1380   course of reasoning!  The proof starts with a fixed goal \isa{thesis}.  The subsequent proof may refine this to anything of the
  1381   form like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}}, but must not introduce new subgoals.  The
  1382   final goal state is then used as reduction rule for the obtain
  1383   scheme described above.  Obtained parameters \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} are marked as internal by default, which prevents the
  1384   proof context from being polluted by ad-hoc variables.  The variable
  1385   names and type constraints given as arguments for \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}
  1386   specify a prefix of obtained parameters explicitly in the text.
  1387 
  1388   It is important to note that the facts introduced by \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} and \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} may not be polymorphic: any
  1389   type-variables occurring here are fixed in the present context!%
  1390 \end{isamarkuptext}%
  1391 \isamarkuptrue%
  1392 %
  1393 \isamarkupsection{Calculational reasoning \label{sec:calculation}%
  1394 }
  1395 \isamarkuptrue%
  1396 %
  1397 \begin{isamarkuptext}%
  1398 \begin{matharray}{rcl}
  1399     \indexdef{}{command}{also}\hypertarget{command.also}{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1400     \indexdef{}{command}{finally}\hypertarget{command.finally}{\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1401     \indexdef{}{command}{moreover}\hypertarget{command.moreover}{\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1402     \indexdef{}{command}{ultimately}\hypertarget{command.ultimately}{\hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1403     \indexdef{}{command}{print\_trans\_rules}\hypertarget{command.print-trans-rules}{\hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
  1404     \hyperlink{attribute.trans}{\mbox{\isa{trans}}} & : & \isa{attribute} \\
  1405     \hyperlink{attribute.sym}{\mbox{\isa{sym}}} & : & \isa{attribute} \\
  1406     \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} & : & \isa{attribute} \\
  1407   \end{matharray}
  1408 
  1409   Calculational proof is forward reasoning with implicit application
  1410   of transitivity rules (such those of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C653E}{\isasymle}}{\isaliteral{22}{\isachardoublequote}}},
  1411   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}}).  Isabelle/Isar maintains an auxiliary fact register
  1412   \indexref{}{fact}{calculation}\hyperlink{fact.calculation}{\mbox{\isa{calculation}}} for accumulating results obtained by
  1413   transitivity composed with the current result.  Command \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} involving \hyperlink{fact.this}{\mbox{\isa{this}}}, while
  1414   \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} exhibits the final \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
  1415   forward chaining towards the next goal statement.  Both commands
  1416   require valid current facts, i.e.\ may occur only after commands
  1417   that produce theorems such as \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}, or some finished proof of \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} etc.  The \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}
  1418   commands are similar to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}},
  1419   but only collect further results in \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} without
  1420   applying any rules yet.
  1421 
  1422   Also note that the implicit term abbreviation ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' has
  1423   its canonical application with calculational proofs.  It refers to
  1424   the argument of the preceding statement. (The argument of a curried
  1425   infix expression happens to be its right-hand side.)
  1426 
  1427   Isabelle/Isar calculations are implicitly subject to block structure
  1428   in the sense that new threads of calculational reasoning are
  1429   commenced for any new block (as opened by a local goal, for
  1430   example).  This means that, apart from being able to nest
  1431   calculations, there is no separate \emph{begin-calculation} command
  1432   required.
  1433 
  1434   \medskip The Isar calculation proof commands may be defined as
  1435   follows:\footnote{We suppress internal bookkeeping such as proper
  1436   handling of block-structure.}
  1437 
  1438   \begin{matharray}{rcl}
  1439     \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}calculation\ {\isaliteral{3D}{\isacharequal}}\ this{\isaliteral{22}{\isachardoublequote}}} \\
  1440     \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}calculation\ {\isaliteral{3D}{\isacharequal}}\ trans\ {\isaliteral{5B}{\isacharbrackleft}}OF\ calculation\ this{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex]
  1441     \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} & \equiv & \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\[0.5ex]
  1442     \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}calculation\ {\isaliteral{3D}{\isacharequal}}\ calculation\ this{\isaliteral{22}{\isachardoublequote}}} \\
  1443     \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} & \equiv & \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\
  1444   \end{matharray}
  1445 
  1446   \begin{railoutput}
  1447 \rail@begin{2}{}
  1448 \rail@bar
  1449 \rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[]
  1450 \rail@nextbar{1}
  1451 \rail@term{\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}}[]
  1452 \rail@endbar
  1453 \rail@bar
  1454 \rail@nextbar{1}
  1455 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1456 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
  1457 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1458 \rail@endbar
  1459 \rail@end
  1460 \rail@begin{3}{}
  1461 \rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[]
  1462 \rail@bar
  1463 \rail@nextbar{1}
  1464 \rail@term{\isa{add}}[]
  1465 \rail@nextbar{2}
  1466 \rail@term{\isa{del}}[]
  1467 \rail@endbar
  1468 \rail@end
  1469 \end{railoutput}
  1470 
  1471 
  1472   \begin{description}
  1473 
  1474   \item \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} maintains the auxiliary
  1475   \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} register as follows.  The first occurrence of
  1476   \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} in some calculational thread initializes \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by \hyperlink{fact.this}{\mbox{\isa{this}}}. Any subsequent \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} on
  1477   the same level of block-structure updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
  1478   some transitivity rule applied to \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} and \hyperlink{fact.this}{\mbox{\isa{this}}} (in that order).  Transitivity rules are picked from the
  1479   current context, unless alternative rules are given as explicit
  1480   arguments.
  1481 
  1482   \item \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} maintaining \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} in the same way as \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}, and concludes the
  1483   current calculational thread.  The final result is exhibited as fact
  1484   for forward chaining towards the next goal. Basically, \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} just abbreviates \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\hyperlink{fact.calculation}{\mbox{\isa{calculation}}}.  Typical idioms for concluding
  1485   calculational proofs are ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isaliteral{3F}{\isacharquery}}thesis}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' and ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}''.
  1486 
  1487   \item \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} are
  1488   analogous to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}, but collect
  1489   results only, without applying rules.
  1490 
  1491   \item \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}} prints the list of transitivity
  1492   rules (for calculational commands \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}) and symmetry rules (for the \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}}
  1493   operation and single step elimination patters) of the current
  1494   context.
  1495 
  1496   \item \hyperlink{attribute.trans}{\mbox{\isa{trans}}} declares theorems as transitivity rules.
  1497 
  1498   \item \hyperlink{attribute.sym}{\mbox{\isa{sym}}} declares symmetry rules, as well as
  1499   \hyperlink{attribute.Pure.elim}{\mbox{\isa{Pure{\isaliteral{2E}{\isachardot}}elim}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} rules.
  1500 
  1501   \item \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} resolves a theorem with some rule
  1502   declared as \hyperlink{attribute.sym}{\mbox{\isa{sym}}} in the current context.  For example,
  1503   ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}}'' produces a
  1504   swapped fact derived from that assumption.
  1505 
  1506   In structured proof texts it is often more appropriate to use an
  1507   explicit single-step elimination proof, such as ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}y\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}''.
  1508 
  1509   \end{description}%
  1510 \end{isamarkuptext}%
  1511 \isamarkuptrue%
  1512 %
  1513 \isamarkupsection{Proof by cases and induction \label{sec:cases-induct}%
  1514 }
  1515 \isamarkuptrue%
  1516 %
  1517 \isamarkupsubsection{Rule contexts%
  1518 }
  1519 \isamarkuptrue%
  1520 %
  1521 \begin{isamarkuptext}%
  1522 \begin{matharray}{rcl}
  1523     \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
  1524     \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}cases}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
  1525     \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} \\
  1526     \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}} & : & \isa{attribute} \\
  1527     \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isa{attribute} \\
  1528     \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isa{attribute} \\
  1529   \end{matharray}
  1530 
  1531   The puristic way to build up Isar proof contexts is by explicit
  1532   language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},
  1533   \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}).  This is adequate
  1534   for plain natural deduction, but easily becomes unwieldy in concrete
  1535   verification tasks, which typically involve big induction rules with
  1536   several cases.
  1537 
  1538   The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a
  1539   local context symbolically: certain proof methods provide an
  1540   environment of named ``cases'' of the form \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}; the effect of ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' is then equivalent to ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''.  Term bindings may be covered as well, notably
  1541   \hyperlink{variable.?case}{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}case}}} for the main conclusion.
  1542 
  1543   By default, the ``terminology'' \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} of
  1544   a case value is marked as hidden, i.e.\ there is no way to refer to
  1545   such parameters in the subsequent proof text.  After all, original
  1546   rule parameters stem from somewhere outside of the current proof
  1547   text.  By using the explicit form ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' instead, the proof author is able to
  1548   chose local names that fit nicely into the current context.
  1549 
  1550   \medskip It is important to note that proper use of \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} does not provide means to peek at the current goal state,
  1551   which is not directly observable in Isar!  Nonetheless, goal
  1552   refinement commands do provide named cases \isa{{\isaliteral{22}{\isachardoublequote}}goal\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}}
  1553   for each subgoal \isa{{\isaliteral{22}{\isachardoublequote}}i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{22}{\isachardoublequote}}} of the resulting goal state.
  1554   Using this extra feature requires great care, because some bits of
  1555   the internal tactical machinery intrude the proof text.  In
  1556   particular, parameter names stemming from the left-over of automated
  1557   reasoning tools are usually quite unpredictable.
  1558 
  1559   Under normal circumstances, the text of cases emerge from standard
  1560   elimination or induction rules, which in turn are derived from
  1561   previous theory specifications in a canonical way (say from
  1562   \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions).
  1563 
  1564   \medskip Proper cases are only available if both the proof method
  1565   and the rules involved support this.  By using appropriate
  1566   attributes, case names, conclusions, and parameters may be also
  1567   declared by hand.  Thus variant versions of rules that have been
  1568   derived manually become ready to use in advanced case analysis
  1569   later.
  1570 
  1571   \begin{railoutput}
  1572 \rail@begin{4}{}
  1573 \rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[]
  1574 \rail@bar
  1575 \rail@nont{\isa{caseref}}[]
  1576 \rail@nextbar{1}
  1577 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1578 \rail@nont{\isa{caseref}}[]
  1579 \rail@plus
  1580 \rail@bar
  1581 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
  1582 \rail@nextbar{2}
  1583 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1584 \rail@endbar
  1585 \rail@nextplus{3}
  1586 \rail@endplus
  1587 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1588 \rail@endbar
  1589 \rail@end
  1590 \rail@begin{2}{\isa{caseref}}
  1591 \rail@nont{\isa{nameref}}[]
  1592 \rail@bar
  1593 \rail@nextbar{1}
  1594 \rail@nont{\isa{attributes}}[]
  1595 \rail@endbar
  1596 \rail@end
  1597 \rail@begin{5}{}
  1598 \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
  1599 \rail@plus
  1600 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1601 \rail@bar
  1602 \rail@nextbar{1}
  1603 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
  1604 \rail@plus
  1605 \rail@bar
  1606 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
  1607 \rail@nextbar{2}
  1608 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1609 \rail@endbar
  1610 \rail@nextplus{3}
  1611 \rail@endplus
  1612 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
  1613 \rail@endbar
  1614 \rail@nextplus{4}
  1615 \rail@endplus
  1616 \rail@end
  1617 \rail@begin{2}{}
  1618 \rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[]
  1619 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1620 \rail@plus
  1621 \rail@nextplus{1}
  1622 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1623 \rail@endplus
  1624 \rail@end
  1625 \rail@begin{3}{}
  1626 \rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[]
  1627 \rail@plus
  1628 \rail@plus
  1629 \rail@nextplus{1}
  1630 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1631 \rail@endplus
  1632 \rail@nextplus{2}
  1633 \rail@cterm{\isa{\isakeyword{and}}}[]
  1634 \rail@endplus
  1635 \rail@end
  1636 \rail@begin{2}{}
  1637 \rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[]
  1638 \rail@bar
  1639 \rail@nextbar{1}
  1640 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
  1641 \rail@endbar
  1642 \rail@end
  1643 \end{railoutput}
  1644 
  1645 
  1646   \begin{description}
  1647   
  1648   \item \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} invokes a named local
  1649   context \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}, as provided by an
  1650   appropriate proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and
  1651   \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}).  The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''.
  1652 
  1653   \item \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}cases}}}} prints all local contexts of the
  1654   current state, using Isar proof language notation.
  1655   
  1656   \item \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares names for
  1657   the local contexts of premises of a theorem; \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}}
  1658   refers to the \emph{prefix} of the list of premises. Each of the
  1659   cases \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} can be of the form \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5B}{\isacharbrackleft}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} where
  1660   the \isa{{\isaliteral{22}{\isachardoublequote}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are the names of the hypotheses in case \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}
  1661   from left to right.
  1662   
  1663   \item \hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares
  1664   names for the conclusions of a named premise \isa{c}; here \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} refers to the prefix of arguments of a logical formula
  1665   built by nesting a binary connective (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}).
  1666   
  1667   Note that proof methods such as \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} already provide a default name for the conclusion as a
  1668   whole.  The need to name subformulas only arises with cases that
  1669   split into several sub-cases, as in common co-induction rules.
  1670 
  1671   \item \hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ q\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} renames
  1672   the innermost parameters of premises \isa{{\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{22}{\isachardoublequote}}} of some
  1673   theorem.  An empty list of names may be given to skip positions,
  1674   leaving the present parameters unchanged.
  1675   
  1676   Note that the default usage of case rules does \emph{not} directly
  1677   expose parameters to the proof context.
  1678   
  1679   \item \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n} declares the number of ``major
  1680   premises'' of a rule, i.e.\ the number of facts to be consumed when
  1681   it is applied by an appropriate proof method.  The default value of
  1682   \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isaliteral{22}{\isachardoublequote}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, which is appropriate for
  1683   the usual kind of cases and induction rules for inductive sets (cf.\
  1684   \secref{sec:hol-inductive}).  Rules without any \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declaration given are treated as if \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} had been specified.
  1685   
  1686   Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only
  1687   rarely needed; this is already taken care of automatically by the
  1688   higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and
  1689   \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations.
  1690 
  1691   \end{description}%
  1692 \end{isamarkuptext}%
  1693 \isamarkuptrue%
  1694 %
  1695 \isamarkupsubsection{Proof methods%
  1696 }
  1697 \isamarkuptrue%
  1698 %
  1699 \begin{isamarkuptext}%
  1700 \begin{matharray}{rcl}
  1701     \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
  1702     \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
  1703     \indexdef{}{method}{induction}\hypertarget{method.induction}{\hyperlink{method.induction}{\mbox{\isa{induction}}}} & : & \isa{method} \\
  1704     \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
  1705   \end{matharray}
  1706 
  1707   The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, \hyperlink{method.induction}{\mbox{\isa{induction}}},
  1708   and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
  1709   methods provide a uniform interface to common proof techniques over
  1710   datatypes, inductive predicates (or sets), recursive functions etc.
  1711   The corresponding rules may be specified and instantiated in a
  1712   casual manner.  Furthermore, these methods provide named local
  1713   contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command
  1714   within the subsequent proof text.  This accommodates compact proof
  1715   texts even when reasoning about large specifications.
  1716 
  1717   The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional
  1718   infrastructure in order to be applicable to structure statements
  1719   (either using explicit meta-level connectives, or including facts
  1720   and parameters separately).  This avoids cumbersome encoding of
  1721   ``strengthened'' inductive statements within the object-logic.
  1722 
  1723   Method \hyperlink{method.induction}{\mbox{\isa{induction}}} differs from \hyperlink{method.induct}{\mbox{\isa{induct}}} only in
  1724   the names of the facts in the local context invoked by the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}
  1725   command.
  1726 
  1727   \begin{railoutput}
  1728 \rail@begin{6}{}
  1729 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
  1730 \rail@bar
  1731 \rail@nextbar{1}
  1732 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1733 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}simp}}[]
  1734 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1735 \rail@endbar
  1736 \rail@cr{3}
  1737 \rail@bar
  1738 \rail@nextbar{4}
  1739 \rail@plus
  1740 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
  1741 \rail@nextplus{5}
  1742 \rail@cterm{\isa{\isakeyword{and}}}[]
  1743 \rail@endplus
  1744 \rail@endbar
  1745 \rail@bar
  1746 \rail@nextbar{4}
  1747 \rail@nont{\isa{rule}}[]
  1748 \rail@endbar
  1749 \rail@end
  1750 \rail@begin{6}{}
  1751 \rail@bar
  1752 \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
  1753 \rail@nextbar{1}
  1754 \rail@term{\hyperlink{method.induction}{\mbox{\isa{induction}}}}[]
  1755 \rail@endbar
  1756 \rail@bar
  1757 \rail@nextbar{1}
  1758 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1759 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}simp}}[]
  1760 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1761 \rail@endbar
  1762 \rail@bar
  1763 \rail@nextbar{1}
  1764 \rail@plus
  1765 \rail@nont{\isa{definsts}}[]
  1766 \rail@nextplus{2}
  1767 \rail@cterm{\isa{\isakeyword{and}}}[]
  1768 \rail@endplus
  1769 \rail@endbar
  1770 \rail@cr{4}
  1771 \rail@bar
  1772 \rail@nextbar{5}
  1773 \rail@nont{\isa{arbitrary}}[]
  1774 \rail@endbar
  1775 \rail@bar
  1776 \rail@nextbar{5}
  1777 \rail@nont{\isa{taking}}[]
  1778 \rail@endbar
  1779 \rail@bar
  1780 \rail@nextbar{5}
  1781 \rail@nont{\isa{rule}}[]
  1782 \rail@endbar
  1783 \rail@end
  1784 \rail@begin{2}{}
  1785 \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
  1786 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
  1787 \rail@nont{\isa{taking}}[]
  1788 \rail@bar
  1789 \rail@nextbar{1}
  1790 \rail@nont{\isa{rule}}[]
  1791 \rail@endbar
  1792 \rail@end
  1793 \rail@begin{5}{\isa{rule}}
  1794 \rail@bar
  1795 \rail@bar
  1796 \rail@term{\isa{type}}[]
  1797 \rail@nextbar{1}
  1798 \rail@term{\isa{pred}}[]
  1799 \rail@nextbar{2}
  1800 \rail@term{\isa{set}}[]
  1801 \rail@endbar
  1802 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
  1803 \rail@plus
  1804 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  1805 \rail@nextplus{1}
  1806 \rail@endplus
  1807 \rail@nextbar{3}
  1808 \rail@term{\isa{rule}}[]
  1809 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
  1810 \rail@plus
  1811 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
  1812 \rail@nextplus{4}
  1813 \rail@endplus
  1814 \rail@endbar
  1815 \rail@end
  1816 \rail@begin{4}{\isa{definst}}
  1817 \rail@bar
  1818 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1819 \rail@bar
  1820 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
  1821 \rail@nextbar{1}
  1822 \rail@term{\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}}[]
  1823 \rail@endbar
  1824 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
  1825 \rail@nextbar{2}
  1826 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1827 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
  1828 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1829 \rail@nextbar{3}
  1830 \rail@nont{\hyperlink{syntax.inst}{\mbox{\isa{inst}}}}[]
  1831 \rail@endbar
  1832 \rail@end
  1833 \rail@begin{2}{\isa{definsts}}
  1834 \rail@plus
  1835 \rail@nextplus{1}
  1836 \rail@cnont{\isa{definst}}[]
  1837 \rail@endplus
  1838 \rail@end
  1839 \rail@begin{3}{\isa{arbitrary}}
  1840 \rail@term{\isa{arbitrary}}[]
  1841 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
  1842 \rail@plus
  1843 \rail@plus
  1844 \rail@nextplus{1}
  1845 \rail@cnont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
  1846 \rail@endplus
  1847 \rail@term{\isa{\isakeyword{and}}}[]
  1848 \rail@nextplus{2}
  1849 \rail@endplus
  1850 \rail@end
  1851 \rail@begin{1}{\isa{taking}}
  1852 \rail@term{\isa{taking}}[]
  1853 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
  1854 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
  1855 \rail@end
  1856 \end{railoutput}
  1857 
  1858 
  1859   \begin{description}
  1860 
  1861   \item \hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} applies method \hyperlink{method.rule}{\mbox{\isa{rule}}} with an appropriate case distinction theorem, instantiated to
  1862   the subjects \isa{insts}.  Symbolic case names are bound according
  1863   to the rule's local contexts.
  1864 
  1865   The rule is determined as follows, according to the facts and
  1866   arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method:
  1867 
  1868   \medskip
  1869   \begin{tabular}{llll}
  1870     facts           &                 & arguments   & rule \\\hline
  1871                     & \hyperlink{method.cases}{\mbox{\isa{cases}}} &             & classical case split \\
  1872                     & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t}   & datatype exhaustion (type of \isa{t}) \\
  1873     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ t{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} & inductive predicate/set elimination (of \isa{A}) \\
  1874     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}     & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ rule{\isaliteral{3A}{\isacharcolon}}\ R{\isaliteral{22}{\isachardoublequote}}} & explicit rule \isa{R} \\
  1875   \end{tabular}
  1876   \medskip
  1877 
  1878   Several instantiations may be given, referring to the \emph{suffix}
  1879   of premises of the case rule; within each premise, the \emph{prefix}
  1880   of variables is instantiated.  In most situations, only a single
  1881   term needs to be specified; this refers to the first variable of the
  1882   last premise (it is usually the same for all cases).  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification of
  1883   cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
  1884 
  1885   \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} and
  1886   \hyperlink{method.induction}{\mbox{\isa{induction}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} are analogous to the
  1887   \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refer to induction rules, which are
  1888   determined as follows:
  1889 
  1890   \medskip
  1891   \begin{tabular}{llll}
  1892     facts           &                  & arguments            & rule \\\hline
  1893                     & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}P\ x{\isaliteral{22}{\isachardoublequote}}}        & datatype induction (type of \isa{x}) \\
  1894     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ x{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}          & predicate/set induction (of \isa{A}) \\
  1895     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}     & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ rule{\isaliteral{3A}{\isacharcolon}}\ R{\isaliteral{22}{\isachardoublequote}}} & explicit rule \isa{R} \\
  1896   \end{tabular}
  1897   \medskip
  1898   
  1899   Several instantiations may be given, each referring to some part of
  1900   a mutual inductive definition or datatype --- only related partial
  1901   induction rules may be used together, though.  Any of the lists of
  1902   terms \isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} refers to the \emph{suffix} of variables
  1903   present in the induction rule.  This enables the writer to specify
  1904   only induction variables, or both predicates and variables, for
  1905   example.
  1906 
  1907   Instantiations may be definitional: equations \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}
  1908   introduce local definitions, which are inserted into the claim and
  1909   discharged after applying the induction rule.  Equalities reappear
  1910   in the inductive cases, but have been transformed according to the
  1911   induction principle being involved here.  In order to achieve
  1912   practically useful induction hypotheses, some variables occurring in
  1913   \isa{t} need to be fixed (see below).  Instantiations of the form
  1914   \isa{t}, where \isa{t} is not a variable, are taken as a
  1915   shorthand for \mbox{\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}}, where \isa{x} is a fresh
  1916   variable. If this is not intended, \isa{t} has to be enclosed in
  1917   parentheses.  By default, the equalities generated by definitional
  1918   instantiations are pre-simplified using a specific set of rules,
  1919   usually consisting of distinctness and injectivity theorems for
  1920   datatypes. This pre-simplification may cause some of the parameters
  1921   of an inductive case to disappear, or may even completely delete
  1922   some of the inductive cases, if one of the equalities occurring in
  1923   their premises can be simplified to \isa{False}.  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification.
  1924   Additional rules to be used in pre-simplification can be declared
  1925   using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}simp}}}} attribute.
  1926 
  1927   The optional ``\isa{{\isaliteral{22}{\isachardoublequote}}arbitrary{\isaliteral{3A}{\isacharcolon}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}''
  1928   specification generalizes variables \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} of the original goal before applying induction.  One can
  1929   separate variables by ``\isa{{\isaliteral{22}{\isachardoublequote}}and{\isaliteral{22}{\isachardoublequote}}}'' to generalize them in other
  1930   goals then the first. Thus induction hypotheses may become
  1931   sufficiently general to get the proof through.  Together with
  1932   definitional instantiations, one may effectively perform induction
  1933   over expressions of a certain structure.
  1934   
  1935   The optional ``\isa{{\isaliteral{22}{\isachardoublequote}}taking{\isaliteral{3A}{\isacharcolon}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''
  1936   specification provides additional instantiations of a prefix of
  1937   pending variables in the rule.  Such schematic induction rules
  1938   rarely occur in practice, though.
  1939 
  1940   \item \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}inst\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the
  1941   \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are
  1942   determined as follows:
  1943 
  1944   \medskip
  1945   \begin{tabular}{llll}
  1946     goal          &                    & arguments & rule \\\hline
  1947                   & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\
  1948     \isa{{\isaliteral{22}{\isachardoublequote}}A\ x{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} & predicate/set coinduction (of \isa{A}) \\
  1949     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}   & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ rule{\isaliteral{3A}{\isacharcolon}}\ R{\isaliteral{22}{\isachardoublequote}}} & explicit rule \isa{R} \\
  1950   \end{tabular}
  1951   
  1952   Coinduction is the dual of induction.  Induction essentially
  1953   eliminates \isa{{\isaliteral{22}{\isachardoublequote}}A\ x{\isaliteral{22}{\isachardoublequote}}} towards a generic result \isa{{\isaliteral{22}{\isachardoublequote}}P\ x{\isaliteral{22}{\isachardoublequote}}},
  1954   while coinduction introduces \isa{{\isaliteral{22}{\isachardoublequote}}A\ x{\isaliteral{22}{\isachardoublequote}}} starting with \isa{{\isaliteral{22}{\isachardoublequote}}B\ x{\isaliteral{22}{\isachardoublequote}}}, for a suitable ``bisimulation'' \isa{B}.  The cases of a
  1955   coinduct rule are typically named after the predicates or sets being
  1956   covered, while the conclusions consist of several alternatives being
  1957   named after the individual destructor patterns.
  1958   
  1959   The given instantiation refers to the \emph{suffix} of variables
  1960   occurring in the rule's major premise, or conclusion if unavailable.
  1961   An additional ``\isa{{\isaliteral{22}{\isachardoublequote}}taking{\isaliteral{3A}{\isacharcolon}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''
  1962   specification may be required in order to specify the bisimulation
  1963   to be used in the coinduction step.
  1964 
  1965   \end{description}
  1966 
  1967   Above methods produce named local contexts, as determined by the
  1968   instantiated rule as given in the text.  Beyond that, the \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} methods guess further instantiations
  1969   from the goal specification itself.  Any persisting unresolved
  1970   schematic variables of the resulting rule will render the the
  1971   corresponding case invalid.  The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}case}}} for
  1972   the conclusion will be provided with each case, provided that term
  1973   is fully specified.
  1974 
  1975   The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}cases}}}} command prints all named cases present
  1976   in the current proof state.
  1977 
  1978   \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}
  1979   and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after
  1980   instantiation, while conforming due to the usual way of monotonic
  1981   natural deduction: the context of a structured statement \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}
  1982   reappears unchanged after the case split.
  1983 
  1984   The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this
  1985   respect: the meta-level structure is passed through the
  1986   ``recursive'' course involved in the induction.  Thus the original
  1987   statement is basically replaced by separate copies, corresponding to
  1988   the induction hypotheses and conclusion; the original goal context
  1989   is no longer available.  Thus local assumptions, fixed parameters
  1990   and definitions effectively participate in the inductive rephrasing
  1991   of the original statement.
  1992 
  1993   In \hyperlink{method.induct}{\mbox{\isa{induct}}} proofs, local assumptions introduced by cases are split
  1994   into two different kinds: \isa{hyps} stemming from the rule and
  1995   \isa{prems} from the goal statement.  This is reflected in the
  1996   extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems},
  1997   as well as fact \isa{c} to hold the all-inclusive list.
  1998 
  1999   In \hyperlink{method.induction}{\mbox{\isa{induction}}} proofs, local assumptions introduced by cases are
  2000   split into three different kinds: \isa{IH}, the induction hypotheses,
  2001   \isa{hyps}, the remaining hypotheses stemming from the rule, and
  2002   \isa{prems}, the assumptions from the goal statement. The names are
  2003   \isa{c{\isaliteral{2E}{\isachardot}}IH}, \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems}, as above.
  2004 
  2005 
  2006   \medskip Facts presented to either method are consumed according to
  2007   the number of ``major premises'' of the rule involved, which is
  2008   usually 0 for plain cases and induction rules of datatypes etc.\ and
  2009   1 for rules of inductive predicates or sets and the like.  The
  2010   remaining facts are inserted into the goal verbatim before the
  2011   actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
  2012   applied.%
  2013 \end{isamarkuptext}%
  2014 \isamarkuptrue%
  2015 %
  2016 \isamarkupsubsection{Declaring rules%
  2017 }
  2018 \isamarkuptrue%
  2019 %
  2020 \begin{isamarkuptext}%
  2021 \begin{matharray}{rcl}
  2022     \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{5F}{\isacharunderscore}}rules}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
  2023     \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isa{attribute} \\
  2024     \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isa{attribute} \\
  2025     \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{attribute} \\
  2026   \end{matharray}
  2027 
  2028   \begin{railoutput}
  2029 \rail@begin{1}{}
  2030 \rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[]
  2031 \rail@nont{\isa{spec}}[]
  2032 \rail@end
  2033 \rail@begin{1}{}
  2034 \rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[]
  2035 \rail@nont{\isa{spec}}[]
  2036 \rail@end
  2037 \rail@begin{1}{}
  2038 \rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[]
  2039 \rail@nont{\isa{spec}}[]
  2040 \rail@end
  2041 \rail@begin{4}{\isa{spec}}
  2042 \rail@bar
  2043 \rail@bar
  2044 \rail@term{\isa{type}}[]
  2045 \rail@nextbar{1}
  2046 \rail@term{\isa{pred}}[]
  2047 \rail@nextbar{2}
  2048 \rail@term{\isa{set}}[]
  2049 \rail@endbar
  2050 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
  2051 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  2052 \rail@nextbar{3}
  2053 \rail@term{\isa{del}}[]
  2054 \rail@endbar
  2055 \rail@end
  2056 \end{railoutput}
  2057 
  2058 
  2059   \begin{description}
  2060 
  2061   \item \hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{5F}{\isacharunderscore}}rules}}}} prints cases and induct rules
  2062   for predicates (or sets) and types of the current context.
  2063 
  2064   \item \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} (as attributes) declare rules for reasoning about
  2065   (co)inductive predicates (or sets) and types, using the
  2066   corresponding methods of the same name.  Certain definitional
  2067   packages of object-logics usually declare emerging cases and
  2068   induction rules as expected, so users rarely need to intervene.
  2069 
  2070   Rules may be deleted via the \isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}} specification, which
  2071   covers all of the \isa{{\isaliteral{22}{\isachardoublequote}}type{\isaliteral{22}{\isachardoublequote}}}/\isa{{\isaliteral{22}{\isachardoublequote}}pred{\isaliteral{22}{\isachardoublequote}}}/\isa{{\isaliteral{22}{\isachardoublequote}}set{\isaliteral{22}{\isachardoublequote}}}
  2072   sub-categories simultaneously.  For example, \hyperlink{attribute.cases}{\mbox{\isa{cases}}}~\isa{del} removes any \hyperlink{attribute.cases}{\mbox{\isa{cases}}} rules declared for
  2073   some type, predicate, or set.
  2074   
  2075   Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
  2076   cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}
  2077   declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
  2078 
  2079   \end{description}%
  2080 \end{isamarkuptext}%
  2081 \isamarkuptrue%
  2082 %
  2083 \isadelimtheory
  2084 %
  2085 \endisadelimtheory
  2086 %
  2087 \isatagtheory
  2088 \isacommand{end}\isamarkupfalse%
  2089 %
  2090 \endisatagtheory
  2091 {\isafoldtheory}%
  2092 %
  2093 \isadelimtheory
  2094 %
  2095 \endisadelimtheory
  2096 \isanewline
  2097 \end{isabellebody}%
  2098 %%% Local Variables:
  2099 %%% mode: latex
  2100 %%% TeX-master: "root"
  2101 %%% End: