wneuper/isa: doc-src/IsarRef/Thy/document/Proof.tex@2080fe35abea

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:

    32   \begin{description}

    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.

    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.

    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.

    48   \end{description}

    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.

    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}

    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}

    88   \begin{description}

    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.

    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}}}}.

    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}

   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!

   122   For slightly more advanced applications, there are explicit block

   123   parentheses as well.  These typically achieve a stronger forward

   124   style of reasoning.

   126   \begin{description}

   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.

   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.

   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}

   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   anyhow.

   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}}}}''.

   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}

   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).

   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.

   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}}}.

   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.termpat}{\mbox{\isa{termpat}}}}[]

   267 \rail@endbar

   268 \rail@end

   269 \end{railoutput}

   272   \begin{description}

   274   \item \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x} introduces a local variable \isa{x} that is \emph{arbitrary, but fixed.}

   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.

   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.

   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.

   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.

   293   \end{description}

   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}

   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.

   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.

   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.

   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}

   351   The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \hyperlink{syntax.termpat}{\mbox{\isa{termpat}}} or

   352   \hyperlink{syntax.proppat}{\mbox{\isa{proppat}}} (see \secref{sec:term-decls}).

   354   \begin{description}

   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}}}.

   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.).

   365   \end{description}

   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}

   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.

   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}

   437   \begin{description}

   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.

   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.

   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}''.

   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.

   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}}}}).

   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.

   468   \end{description}

   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.

   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).

   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}

   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.

   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.

   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}).

   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}

   636   \begin{description}

   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}.

   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.

   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.

   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.

   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.

   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).

   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:

   678   %FIXME proper antiquitation

   679   \begin{ttbox}

   680   Problem! Local statement will fail to solve any pending goal

   681   \end{ttbox}

   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}}}}''.

   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}}}}''.

   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.

   694   \end{description}

   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}.

   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).

   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}

   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.

   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}}}.

   782   \begin{railoutput}

   783 \rail@begin{4}{\indexdef{}{syntax}{goalspec}\hypertarget{syntax.goalspec}{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}}

   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}

   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.

   821   \begin{enumerate}

   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.

   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}}}.

   830   \end{enumerate}

   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.

   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.

   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.

   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}

   886   \begin{description}

   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.

   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}}}}.

   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}}}~\isa{{\isaliteral{22}{\isachardoublequote}}qed{\isaliteral{22}{\isachardoublequote}}}~\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.

   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}}}.

   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}}}.

   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.

   924   The most important application of \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is to support

   925   experimentation and top-down proof development.

   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}).

   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}

   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}

  1061   \begin{description}

  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.

  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.

  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.

  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}''.

  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.

  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}).

  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.

  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}}}.

  1111   \item \hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,

  1112   elimination, or destruct rules.

  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.

  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.

  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.

  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.

  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}

  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}

  1185   \begin{description}

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  1218   \end{description}

  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}

  1236   \begin{railoutput}

  1237 \rail@begin{1}{}

  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@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  1243 \rail@end

  1244 \end{railoutput}

  1247   \begin{description}

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

  1250   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

  1251   \verb|(Proof.context -> Proof.method) context_parser|, cf.\

  1252   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

  1253   methods; the primed versions refer to tactics with explicit goal

  1254   addressing.

  1256   Here are some example method definitions:

  1258   \end{description}%

  1259 \end{isamarkuptext}%

  1260 \isamarkuptrue%

  1261 %

  1262 \isadelimML

  1263 \ \ \ \ %

  1264 \endisadelimML

  1265 %

  1266 \isatagML

  1267 \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%

  1268 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

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

  1270 \ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ first\ method\ {\isaliteral{28}{\isacharparenleft}}without\ any\ arguments{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1271 \isanewline

  1272 \ \ \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%

  1273 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

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

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

  1276 \ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ second\ method\ {\isaliteral{28}{\isacharparenleft}}with\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1277 \isanewline

  1278 \ \ \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%

  1279 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

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

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

  1282 \ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ third\ method\ {\isaliteral{28}{\isacharparenleft}}with\ theorem\ arguments\ and\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%

  1283 \endisatagML

  1284 {\isafoldML}%

  1285 %

  1286 \isadelimML

  1287 %

  1288 \endisadelimML

  1289 %

  1290 \isamarkupsection{Generalized elimination \label{sec:obtain}%

  1291 }

  1292 \isamarkuptrue%

  1293 %

  1294 \begin{isamarkuptext}%

  1295 \begin{matharray}{rcl}

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

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

  1298   \end{matharray}

  1300   Generalized elimination means that additional elements with certain

  1301   properties may be introduced in the current context, by virtue of a

  1302   locally proven ``soundness statement''.  Technically speaking, the

  1303   \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} language element is like a declaration of

  1304   \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} (see also see

  1305   \secref{sec:proof-context}), together with a soundness proof of its

  1306   additional claim.  According to the nature of existential reasoning,

  1307   assumptions get eliminated from any result exported from the context

  1308   later, provided that the corresponding parameters do \emph{not}

  1309   occur in the conclusion.

  1311   \begin{railoutput}

  1312 \rail@begin{2}{}

  1313 \rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[]

  1314 \rail@bar

  1315 \rail@nextbar{1}

  1316 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]

  1317 \rail@endbar

  1318 \rail@plus

  1319 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]

  1320 \rail@nextplus{1}

  1321 \rail@cterm{\isa{\isakeyword{and}}}[]

  1322 \rail@endplus

  1323 \rail@term{\isa{\isakeyword{where}}}[]

  1324 \rail@plus

  1325 \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]

  1326 \rail@nextplus{1}

  1327 \rail@cterm{\isa{\isakeyword{and}}}[]

  1328 \rail@endplus

  1329 \rail@end

  1330 \rail@begin{2}{}

  1331 \rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[]

  1332 \rail@plus

  1333 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]

  1334 \rail@nextplus{1}

  1335 \rail@cterm{\isa{\isakeyword{and}}}[]

  1336 \rail@endplus

  1337 \rail@end

  1338 \end{railoutput}

  1341   The derived Isar command \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} is defined as follows

  1342   (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)

  1343   facts indicated for forward chaining).

  1344   \begin{matharray}{l}

  1345     \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]

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

  1347     \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\hyperlink{method.succeed}{\mbox{\isa{succeed}}} \\

  1348     \qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\

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

  1350     \qquad \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis} \\

  1351     \quad\qquad \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{{\isaliteral{2D}{\isacharminus}}} \\

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

  1353     \quad \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} \\

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

  1355   \end{matharray}

  1357   Typically, the soundness proof is relatively straight-forward, often

  1358   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

  1359   ``\isa{that}'' reduction above is declared as simplification and

  1360   introduction rule.

  1362   In a sense, \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} represents at the level of Isar

  1363   proofs what would be meta-logical existential quantifiers and

  1364   conjunctions.  This concept has a broad range of useful

  1365   applications, ranging from plain elimination (or introduction) of

  1366   object-level existential and conjunctions, to elimination over

  1367   results of symbolic evaluation of recursive definitions, for

  1368   example.  Also note that \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} without parameters acts

  1369   much like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, where the result is treated as a

  1370   genuine assumption.

  1372   An alternative name to be used instead of ``\isa{that}'' above may

  1373   be given in parentheses.

  1375   \medskip The improper variant \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} is similar to

  1376   \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}, but derives the obtained statement from the

  1377   course of reasoning!  The proof starts with a fixed goal \isa{thesis}.  The subsequent proof may refine this to anything of the

  1378   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

  1379   final goal state is then used as reduction rule for the obtain

  1380   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

  1381   proof context from being polluted by ad-hoc variables.  The variable

  1382   names and type constraints given as arguments for \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}

  1383   specify a prefix of obtained parameters explicitly in the text.

  1385   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

  1386   type-variables occurring here are fixed in the present context!%

  1387 \end{isamarkuptext}%

  1388 \isamarkuptrue%

  1389 %

  1390 \isamarkupsection{Calculational reasoning \label{sec:calculation}%

  1391 }

  1392 \isamarkuptrue%

  1393 %

  1394 \begin{isamarkuptext}%

  1395 \begin{matharray}{rcl}

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

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

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

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

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

  1401     \hyperlink{attribute.trans}{\mbox{\isa{trans}}} & : & \isa{attribute} \\

  1402     \hyperlink{attribute.sym}{\mbox{\isa{sym}}} & : & \isa{attribute} \\

  1403     \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} & : & \isa{attribute} \\

  1404   \end{matharray}

  1406   Calculational proof is forward reasoning with implicit application

  1407   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}}},

  1408   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}}).  Isabelle/Isar maintains an auxiliary fact register

  1409   \indexref{}{fact}{calculation}\hyperlink{fact.calculation}{\mbox{\isa{calculation}}} for accumulating results obtained by

  1410   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

  1411   \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} exhibits the final \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by

  1412   forward chaining towards the next goal statement.  Both commands

  1413   require valid current facts, i.e.\ may occur only after commands

  1414   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}}}}

  1415   commands are similar to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}},

  1416   but only collect further results in \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} without

  1417   applying any rules yet.

  1419   Also note that the implicit term abbreviation ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' has

  1420   its canonical application with calculational proofs.  It refers to

  1421   the argument of the preceding statement. (The argument of a curried

  1422   infix expression happens to be its right-hand side.)

  1424   Isabelle/Isar calculations are implicitly subject to block structure

  1425   in the sense that new threads of calculational reasoning are

  1426   commenced for any new block (as opened by a local goal, for

  1427   example).  This means that, apart from being able to nest

  1428   calculations, there is no separate \emph{begin-calculation} command

  1429   required.

  1431   \medskip The Isar calculation proof commands may be defined as

  1432   follows:\footnote{We suppress internal bookkeeping such as proper

  1433   handling of block-structure.}

  1435   \begin{matharray}{rcl}

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

  1437     \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]

  1438     \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]

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

  1440     \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} & \equiv & \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\

  1441   \end{matharray}

  1443   \begin{railoutput}

  1444 \rail@begin{2}{}

  1445 \rail@bar

  1446 \rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[]

  1447 \rail@nextbar{1}

  1448 \rail@term{\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}}[]

  1449 \rail@endbar

  1450 \rail@bar

  1451 \rail@nextbar{1}

  1452 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1453 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

  1454 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1455 \rail@endbar

  1456 \rail@end

  1457 \rail@begin{3}{}

  1458 \rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[]

  1459 \rail@bar

  1460 \rail@nextbar{1}

  1461 \rail@term{\isa{add}}[]

  1462 \rail@nextbar{2}

  1463 \rail@term{\isa{del}}[]

  1464 \rail@endbar

  1465 \rail@end

  1466 \end{railoutput}

  1469   \begin{description}

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

  1472   \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} register as follows.  The first occurrence of

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

  1474   the same level of block-structure updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by

  1475   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

  1476   current context, unless alternative rules are given as explicit

  1477   arguments.

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

  1480   current calculational thread.  The final result is exhibited as fact

  1481   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

  1482   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}}}}}}''.

  1484   \item \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} are

  1485   analogous to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}, but collect

  1486   results only, without applying rules.

  1488   \item \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}} prints the list of transitivity

  1489   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}}}

  1490   operation and single step elimination patters) of the current

  1491   context.

  1493   \item \hyperlink{attribute.trans}{\mbox{\isa{trans}}} declares theorems as transitivity rules.

  1495   \item \hyperlink{attribute.sym}{\mbox{\isa{sym}}} declares symmetry rules, as well as

  1496   \hyperlink{attribute.Pure.elim}{\mbox{\isa{Pure{\isaliteral{2E}{\isachardot}}elim}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} rules.

  1498   \item \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} resolves a theorem with some rule

  1499   declared as \hyperlink{attribute.sym}{\mbox{\isa{sym}}} in the current context.  For example,

  1500   ``\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

  1501   swapped fact derived from that assumption.

  1503   In structured proof texts it is often more appropriate to use an

  1504   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}}}}}}''.

  1506   \end{description}%

  1507 \end{isamarkuptext}%

  1508 \isamarkuptrue%

  1509 %

  1510 \isamarkupsection{Proof by cases and induction \label{sec:cases-induct}%

  1511 }

  1512 \isamarkuptrue%

  1513 %

  1514 \isamarkupsubsection{Rule contexts%

  1515 }

  1516 \isamarkuptrue%

  1517 %

  1518 \begin{isamarkuptext}%

  1519 \begin{matharray}{rcl}

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

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

  1522     \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} \\

  1523     \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}} & : & \isa{attribute} \\

  1524     \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isa{attribute} \\

  1525     \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isa{attribute} \\

  1526   \end{matharray}

  1528   The puristic way to build up Isar proof contexts is by explicit

  1529   language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},

  1530   \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}).  This is adequate

  1531   for plain natural deduction, but easily becomes unwieldy in concrete

  1532   verification tasks, which typically involve big induction rules with

  1533   several cases.

  1535   The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a

  1536   local context symbolically: certain proof methods provide an

  1537   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

  1538   \hyperlink{variable.?case}{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}case}}} for the main conclusion.

  1540   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

  1541   a case value is marked as hidden, i.e.\ there is no way to refer to

  1542   such parameters in the subsequent proof text.  After all, original

  1543   rule parameters stem from somewhere outside of the current proof

  1544   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

  1545   chose local names that fit nicely into the current context.

  1547   \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,

  1548   which is not directly observable in Isar!  Nonetheless, goal

  1549   refinement commands do provide named cases \isa{{\isaliteral{22}{\isachardoublequote}}goal\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}}

  1550   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.

  1551   Using this extra feature requires great care, because some bits of

  1552   the internal tactical machinery intrude the proof text.  In

  1553   particular, parameter names stemming from the left-over of automated

  1554   reasoning tools are usually quite unpredictable.

  1556   Under normal circumstances, the text of cases emerge from standard

  1557   elimination or induction rules, which in turn are derived from

  1558   previous theory specifications in a canonical way (say from

  1559   \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions).

  1561   \medskip Proper cases are only available if both the proof method

  1562   and the rules involved support this.  By using appropriate

  1563   attributes, case names, conclusions, and parameters may be also

  1564   declared by hand.  Thus variant versions of rules that have been

  1565   derived manually become ready to use in advanced case analysis

  1566   later.

  1568   \begin{railoutput}

  1569 \rail@begin{4}{}

  1570 \rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[]

  1571 \rail@bar

  1572 \rail@nont{\isa{caseref}}[]

  1573 \rail@nextbar{1}

  1574 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1575 \rail@nont{\isa{caseref}}[]

  1576 \rail@plus

  1577 \rail@bar

  1578 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]

  1579 \rail@nextbar{2}

  1580 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1581 \rail@endbar

  1582 \rail@nextplus{3}

  1583 \rail@endplus

  1584 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1585 \rail@endbar

  1586 \rail@end

  1587 \rail@begin{2}{\isa{caseref}}

  1588 \rail@nont{\isa{nameref}}[]

  1589 \rail@bar

  1590 \rail@nextbar{1}

  1591 \rail@nont{\isa{attributes}}[]

  1592 \rail@endbar

  1593 \rail@end

  1594 \rail@begin{2}{}

  1595 \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]

  1596 \rail@plus

  1597 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1598 \rail@nextplus{1}

  1599 \rail@endplus

  1600 \rail@end

  1601 \rail@begin{2}{}

  1602 \rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[]

  1603 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1604 \rail@plus

  1605 \rail@nextplus{1}

  1606 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1607 \rail@endplus

  1608 \rail@end

  1609 \rail@begin{3}{}

  1610 \rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[]

  1611 \rail@plus

  1612 \rail@plus

  1613 \rail@nextplus{1}

  1614 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1615 \rail@endplus

  1616 \rail@nextplus{2}

  1617 \rail@cterm{\isa{\isakeyword{and}}}[]

  1618 \rail@endplus

  1619 \rail@end

  1620 \rail@begin{2}{}

  1621 \rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[]

  1622 \rail@bar

  1623 \rail@nextbar{1}

  1624 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

  1625 \rail@endbar

  1626 \rail@end

  1627 \end{railoutput}

  1630   \begin{description}

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

  1633   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

  1634   appropriate proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and

  1635   \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}}}''.

  1637   \item \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}cases}}}} prints all local contexts of the

  1638   current state, using Isar proof language notation.

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

  1641   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}}}

  1642   refers to the \emph{suffix} of the list of premises.

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

  1645   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

  1646   built by nesting a binary connective (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}).

  1648   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

  1649   whole.  The need to name subformulas only arises with cases that

  1650   split into several sub-cases, as in common co-induction rules.

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

  1653   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

  1654   theorem.  An empty list of names may be given to skip positions,

  1655   leaving the present parameters unchanged.

  1657   Note that the default usage of case rules does \emph{not} directly

  1658   expose parameters to the proof context.

  1660   \item \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n} declares the number of ``major

  1661   premises'' of a rule, i.e.\ the number of facts to be consumed when

  1662   it is applied by an appropriate proof method.  The default value of

  1663   \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isaliteral{22}{\isachardoublequote}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, which is appropriate for

  1664   the usual kind of cases and induction rules for inductive sets (cf.\

  1665   \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.

  1667   Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only

  1668   rarely needed; this is already taken care of automatically by the

  1669   higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and

  1670   \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations.

  1672   \end{description}%

  1673 \end{isamarkuptext}%

  1674 \isamarkuptrue%

  1675 %

  1676 \isamarkupsubsection{Proof methods%

  1677 }

  1678 \isamarkuptrue%

  1679 %

  1680 \begin{isamarkuptext}%

  1681 \begin{matharray}{rcl}

  1682     \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\

  1683     \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\

  1684     \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\

  1685   \end{matharray}

  1687   The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}

  1688   methods provide a uniform interface to common proof techniques over

  1689   datatypes, inductive predicates (or sets), recursive functions etc.

  1690   The corresponding rules may be specified and instantiated in a

  1691   casual manner.  Furthermore, these methods provide named local

  1692   contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command

  1693   within the subsequent proof text.  This accommodates compact proof

  1694   texts even when reasoning about large specifications.

  1696   The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional

  1697   infrastructure in order to be applicable to structure statements

  1698   (either using explicit meta-level connectives, or including facts

  1699   and parameters separately).  This avoids cumbersome encoding of

  1700   ``strengthened'' inductive statements within the object-logic.

  1702   \begin{railoutput}

  1703 \rail@begin{3}{}

  1704 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]

  1705 \rail@bar

  1706 \rail@nextbar{1}

  1707 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1708 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}simp}}[]

  1709 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1710 \rail@endbar

  1711 \rail@bar

  1712 \rail@nextbar{1}

  1713 \rail@plus

  1714 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]

  1715 \rail@nextplus{2}

  1716 \rail@cterm{\isa{\isakeyword{and}}}[]

  1717 \rail@endplus

  1718 \rail@endbar

  1719 \rail@bar

  1720 \rail@nextbar{1}

  1721 \rail@nont{\isa{rule}}[]

  1722 \rail@endbar

  1723 \rail@end

  1724 \rail@begin{6}{}

  1725 \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]

  1726 \rail@bar

  1727 \rail@nextbar{1}

  1728 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1729 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}simp}}[]

  1730 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1731 \rail@endbar

  1732 \rail@bar

  1733 \rail@nextbar{1}

  1734 \rail@plus

  1735 \rail@nont{\isa{definsts}}[]

  1736 \rail@nextplus{2}

  1737 \rail@cterm{\isa{\isakeyword{and}}}[]

  1738 \rail@endplus

  1739 \rail@endbar

  1740 \rail@cr{4}

  1741 \rail@bar

  1742 \rail@nextbar{5}

  1743 \rail@nont{\isa{arbitrary}}[]

  1744 \rail@endbar

  1745 \rail@bar

  1746 \rail@nextbar{5}

  1747 \rail@nont{\isa{taking}}[]

  1748 \rail@endbar

  1749 \rail@bar

  1750 \rail@nextbar{5}

  1751 \rail@nont{\isa{rule}}[]

  1752 \rail@endbar

  1753 \rail@end

  1754 \rail@begin{2}{}

  1755 \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]

  1756 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]

  1757 \rail@nont{\isa{taking}}[]

  1758 \rail@bar

  1759 \rail@nextbar{1}

  1760 \rail@nont{\isa{rule}}[]

  1761 \rail@endbar

  1762 \rail@end

  1763 \rail@begin{5}{\isa{rule}}

  1764 \rail@bar

  1765 \rail@bar

  1766 \rail@term{\isa{type}}[]

  1767 \rail@nextbar{1}

  1768 \rail@term{\isa{pred}}[]

  1769 \rail@nextbar{2}

  1770 \rail@term{\isa{set}}[]

  1771 \rail@endbar

  1772 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1773 \rail@plus

  1774 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1775 \rail@nextplus{1}

  1776 \rail@endplus

  1777 \rail@nextbar{3}

  1778 \rail@term{\isa{rule}}[]

  1779 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1780 \rail@plus

  1781 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]

  1782 \rail@nextplus{4}

  1783 \rail@endplus

  1784 \rail@endbar

  1785 \rail@end

  1786 \rail@begin{4}{\isa{definst}}

  1787 \rail@bar

  1788 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1789 \rail@bar

  1790 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]

  1791 \rail@nextbar{1}

  1792 \rail@term{\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}}[]

  1793 \rail@endbar

  1794 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1795 \rail@nextbar{2}

  1796 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1797 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1798 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1799 \rail@nextbar{3}

  1800 \rail@nont{\hyperlink{syntax.inst}{\mbox{\isa{inst}}}}[]

  1801 \rail@endbar

  1802 \rail@end

  1803 \rail@begin{2}{\isa{definsts}}

  1804 \rail@plus

  1805 \rail@nextplus{1}

  1806 \rail@cnont{\isa{definst}}[]

  1807 \rail@endplus

  1808 \rail@end

  1809 \rail@begin{3}{\isa{arbitrary}}

  1810 \rail@term{\isa{arbitrary}}[]

  1811 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1812 \rail@plus

  1813 \rail@plus

  1814 \rail@nextplus{1}

  1815 \rail@cnont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1816 \rail@endplus

  1817 \rail@term{\isa{\isakeyword{and}}}[]

  1818 \rail@nextplus{2}

  1819 \rail@endplus

  1820 \rail@end

  1821 \rail@begin{1}{\isa{taking}}

  1822 \rail@term{\isa{taking}}[]

  1823 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1824 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]

  1825 \rail@end

  1826 \end{railoutput}

  1829   \begin{description}

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

  1832   the subjects \isa{insts}.  Symbolic case names are bound according

  1833   to the rule's local contexts.

  1835   The rule is determined as follows, according to the facts and

  1836   arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method:

  1838   \medskip

  1839   \begin{tabular}{llll}

  1840     facts           &                 & arguments   & rule \\\hline

  1841                     & \hyperlink{method.cases}{\mbox{\isa{cases}}} &             & classical case split \\

  1842                     & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t}   & datatype exhaustion (type of \isa{t}) \\

  1843     \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}) \\

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

  1845   \end{tabular}

  1846   \medskip

  1848   Several instantiations may be given, referring to the \emph{suffix}

  1849   of premises of the case rule; within each premise, the \emph{prefix}

  1850   of variables is instantiated.  In most situations, only a single

  1851   term needs to be specified; this refers to the first variable of the

  1852   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

  1853   cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).

  1855   \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the

  1856   \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are

  1857   determined as follows:

  1859   \medskip

  1860   \begin{tabular}{llll}

  1861     facts           &                  & arguments            & rule \\\hline

  1862                     & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}P\ x{\isaliteral{22}{\isachardoublequote}}}        & datatype induction (type of \isa{x}) \\

  1863     \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}) \\

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

  1865   \end{tabular}

  1866   \medskip

  1868   Several instantiations may be given, each referring to some part of

  1869   a mutual inductive definition or datatype --- only related partial

  1870   induction rules may be used together, though.  Any of the lists of

  1871   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

  1872   present in the induction rule.  This enables the writer to specify

  1873   only induction variables, or both predicates and variables, for

  1874   example.

  1876   Instantiations may be definitional: equations \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}

  1877   introduce local definitions, which are inserted into the claim and

  1878   discharged after applying the induction rule.  Equalities reappear

  1879   in the inductive cases, but have been transformed according to the

  1880   induction principle being involved here.  In order to achieve

  1881   practically useful induction hypotheses, some variables occurring in

  1882   \isa{t} need to be fixed (see below).  Instantiations of the form

  1883   \isa{t}, where \isa{t} is not a variable, are taken as a

  1884   shorthand for \mbox{\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}}, where \isa{x} is a fresh

  1885   variable. If this is not intended, \isa{t} has to be enclosed in

  1886   parentheses.  By default, the equalities generated by definitional

  1887   instantiations are pre-simplified using a specific set of rules,

  1888   usually consisting of distinctness and injectivity theorems for

  1889   datatypes. This pre-simplification may cause some of the parameters

  1890   of an inductive case to disappear, or may even completely delete

  1891   some of the inductive cases, if one of the equalities occurring in

  1892   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.

  1893   Additional rules to be used in pre-simplification can be declared

  1894   using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}simp}}}} attribute.

  1896   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}}}''

  1897   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.  Thus

  1898   induction hypotheses may become sufficiently general to get the

  1899   proof through.  Together with definitional instantiations, one may

  1900   effectively perform induction over expressions of a certain

  1901   structure.

  1903   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}}}''

  1904   specification provides additional instantiations of a prefix of

  1905   pending variables in the rule.  Such schematic induction rules

  1906   rarely occur in practice, though.

  1908   \item \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}inst\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the

  1909   \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are

  1910   determined as follows:

  1912   \medskip

  1913   \begin{tabular}{llll}

  1914     goal          &                    & arguments & rule \\\hline

  1915                   & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\

  1916     \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}) \\

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

  1918   \end{tabular}

  1920   Coinduction is the dual of induction.  Induction essentially

  1921   eliminates \isa{{\isaliteral{22}{\isachardoublequote}}A\ x{\isaliteral{22}{\isachardoublequote}}} towards a generic result \isa{{\isaliteral{22}{\isachardoublequote}}P\ x{\isaliteral{22}{\isachardoublequote}}},

  1922   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

  1923   coinduct rule are typically named after the predicates or sets being

  1924   covered, while the conclusions consist of several alternatives being

  1925   named after the individual destructor patterns.

  1927   The given instantiation refers to the \emph{suffix} of variables

  1928   occurring in the rule's major premise, or conclusion if unavailable.

  1929   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}}}''

  1930   specification may be required in order to specify the bisimulation

  1931   to be used in the coinduction step.

  1933   \end{description}

  1935   Above methods produce named local contexts, as determined by the

  1936   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

  1937   from the goal specification itself.  Any persisting unresolved

  1938   schematic variables of the resulting rule will render the the

  1939   corresponding case invalid.  The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}case}}} for

  1940   the conclusion will be provided with each case, provided that term

  1941   is fully specified.

  1943   The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}cases}}}} command prints all named cases present

  1944   in the current proof state.

  1946   \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}

  1947   and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after

  1948   instantiation, while conforming due to the usual way of monotonic

  1949   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}}}

  1950   reappears unchanged after the case split.

  1952   The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this

  1953   respect: the meta-level structure is passed through the

  1954   ``recursive'' course involved in the induction.  Thus the original

  1955   statement is basically replaced by separate copies, corresponding to

  1956   the induction hypotheses and conclusion; the original goal context

  1957   is no longer available.  Thus local assumptions, fixed parameters

  1958   and definitions effectively participate in the inductive rephrasing

  1959   of the original statement.

  1961   In induction proofs, local assumptions introduced by cases are split

  1962   into two different kinds: \isa{hyps} stemming from the rule and

  1963   \isa{prems} from the goal statement.  This is reflected in the

  1964   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},

  1965   as well as fact \isa{c} to hold the all-inclusive list.

  1967   \medskip Facts presented to either method are consumed according to

  1968   the number of ``major premises'' of the rule involved, which is

  1969   usually 0 for plain cases and induction rules of datatypes etc.\ and

  1970   1 for rules of inductive predicates or sets and the like.  The

  1971   remaining facts are inserted into the goal verbatim before the

  1972   actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is

  1973   applied.%

  1974 \end{isamarkuptext}%

  1975 \isamarkuptrue%

  1976 %

  1977 \isamarkupsubsection{Declaring rules%

  1978 }

  1979 \isamarkuptrue%

  1980 %

  1981 \begin{isamarkuptext}%

  1982 \begin{matharray}{rcl}

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

  1984     \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isa{attribute} \\

  1985     \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isa{attribute} \\

  1986     \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{attribute} \\

  1987   \end{matharray}

  1989   \begin{railoutput}

  1990 \rail@begin{1}{}

  1991 \rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[]

  1992 \rail@nont{\isa{spec}}[]

  1993 \rail@end

  1994 \rail@begin{1}{}

  1995 \rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[]

  1996 \rail@nont{\isa{spec}}[]

  1997 \rail@end

  1998 \rail@begin{1}{}

  1999 \rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[]

  2000 \rail@nont{\isa{spec}}[]

  2001 \rail@end

  2002 \rail@begin{4}{\isa{spec}}

  2003 \rail@bar

  2004 \rail@bar

  2005 \rail@term{\isa{type}}[]

  2006 \rail@nextbar{1}

  2007 \rail@term{\isa{pred}}[]

  2008 \rail@nextbar{2}

  2009 \rail@term{\isa{set}}[]

  2010 \rail@endbar

  2011 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  2012 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  2013 \rail@nextbar{3}

  2014 \rail@term{\isa{del}}[]

  2015 \rail@endbar

  2016 \rail@end

  2017 \end{railoutput}

  2020   \begin{description}

  2022   \item \hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{5F}{\isacharunderscore}}rules}}}} prints cases and induct rules

  2023   for predicates (or sets) and types of the current context.

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

  2026   (co)inductive predicates (or sets) and types, using the

  2027   corresponding methods of the same name.  Certain definitional

  2028   packages of object-logics usually declare emerging cases and

  2029   induction rules as expected, so users rarely need to intervene.

  2031   Rules may be deleted via the \isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}} specification, which

  2032   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}}}

  2033   sub-categories simultaneously.  For example, \hyperlink{attribute.cases}{\mbox{\isa{cases}}}~\isa{del} removes any \hyperlink{attribute.cases}{\mbox{\isa{cases}}} rules declared for

  2034   some type, predicate, or set.

  2036   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

  2037   cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}

  2038   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.

  2040   \end{description}%

  2041 \end{isamarkuptext}%

  2042 \isamarkuptrue%

  2043 %

  2044 \isadelimtheory

  2045 %

  2046 \endisadelimtheory

  2047 %

  2048 \isatagtheory

  2049 \isacommand{end}\isamarkupfalse%

  2050 %

  2051 \endisatagtheory

  2052 {\isafoldtheory}%

  2053 %

  2054 \isadelimtheory

  2055 %

  2056 \endisadelimtheory

  2057 \isanewline

  2058 \end{isabellebody}%

  2059 %%% Local Variables:

  2060 %%% mode: latex

  2061 %%% TeX-master: "root"

  2062 %%% End:

author	wenzelm
	Tue, 03 May 2011 21:07:24 +0200
changeset 43535	2080fe35abea
parent 43522	e3fdb7c96be5
child 43575	3f19e324ff59
permissions	-rw-r--r--