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

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   in any way.

   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.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]

   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.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}} or

   352   \hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}} (see \secref{sec:term-decls}).

   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}{goal\_spec}\hypertarget{syntax.goal-spec}{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}}

   784 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]

   785 \rail@bar

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

   787 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

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

   789 \rail@nextbar{1}

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

   791 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

   792 \rail@nextbar{2}

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

   794 \rail@nextbar{3}

   795 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]

   796 \rail@endbar

   797 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]

   798 \rail@end

   799 \end{railoutput}%

   800 \end{isamarkuptext}%

   801 \isamarkuptrue%

   802 %

   803 \isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}%

   804 }

   805 \isamarkuptrue%

   806 %

   807 \begin{isamarkuptext}%

   808 \begin{matharray}{rcl}

   809     \indexdef{}{command}{proof}\hypertarget{command.proof}{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   810     \indexdef{}{command}{qed}\hypertarget{command.qed}{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   811     \indexdef{}{command}{by}\hypertarget{command.by}{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   812     \indexdef{}{command}{..}\hypertarget{command.ddot}{\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   813     \indexdef{}{command}{.}\hypertarget{command.dot}{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   814     \indexdef{}{command}{sorry}\hypertarget{command.sorry}{\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{7C}{\isacharbar}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   815   \end{matharray}

   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{2}{}

  1238 \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]

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

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

  1241 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  1242 \rail@bar

  1243 \rail@nextbar{1}

  1244 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  1245 \rail@endbar

  1246 \rail@end

  1247 \end{railoutput}

  1250   \begin{description}

  1252   \item \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ text\ description{\isaliteral{22}{\isachardoublequote}}}

  1253   defines a proof method in the current theory.  The given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} has to be an ML expression of type

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

  1255   basic parsers defined in structure \verb|Args| and \verb|Attrib|.  There are also combinators like \verb|METHOD| and \verb|SIMPLE_METHOD| to turn certain tactic forms into official proof

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

  1257   addressing.

  1259   Here are some example method definitions:

  1261   \end{description}%

  1262 \end{isamarkuptext}%

  1263 \isamarkuptrue%

  1264 %

  1265 \isadelimML

  1266 \ \ %

  1267 \endisadelimML

  1268 %

  1269 \isatagML

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

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

  1272 \ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}K\ {\isaliteral{28}{\isacharparenleft}}SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline

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

  1274 \isanewline

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

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

  1277 \ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline

  1278 \ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline

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

  1280 \isanewline

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

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

  1283 \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ thms{\isaliteral{3A}{\isacharcolon}}\ thm\ list\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline

  1284 \ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline

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

  1286 \endisatagML

  1287 {\isafoldML}%

  1288 %

  1289 \isadelimML

  1290 %

  1291 \endisadelimML

  1292 %

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

  1294 }

  1295 \isamarkuptrue%

  1296 %

  1297 \begin{isamarkuptext}%

  1298 \begin{matharray}{rcl}

  1299     \indexdef{}{command}{obtain}\hypertarget{command.obtain}{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1300     \indexdef{}{command}{guess}\hypertarget{command.guess}{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1301   \end{matharray}

  1303   Generalized elimination means that additional elements with certain

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

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

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

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

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

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

  1310   assumptions get eliminated from any result exported from the context

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

  1312   occur in the conclusion.

  1314   \begin{railoutput}

  1315 \rail@begin{2}{}

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

  1317 \rail@bar

  1318 \rail@nextbar{1}

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

  1320 \rail@endbar

  1321 \rail@plus

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

  1323 \rail@nextplus{1}

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

  1325 \rail@endplus

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

  1327 \rail@plus

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

  1329 \rail@nextplus{1}

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

  1331 \rail@endplus

  1332 \rail@end

  1333 \rail@begin{2}{}

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

  1335 \rail@plus

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

  1337 \rail@nextplus{1}

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

  1339 \rail@endplus

  1340 \rail@end

  1341 \end{railoutput}

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

  1345   (where \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} shall refer to (optional)

  1346   facts indicated for forward chaining).

  1347   \begin{matharray}{l}

  1348     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616E676C653E}{\isasymlangle}}using\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5C3C72616E676C653E}{\isasymrangle}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ \ {\isaliteral{5C3C6C616E676C653E}{\isasymlangle}}proof{\isaliteral{5C3C72616E676C653E}{\isasymrangle}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]

  1349     \quad \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}thesis{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}} \\

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

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

  1352     \qquad \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}that\ {\isaliteral{5B}{\isacharbrackleft}}Pure{\isaliteral{2E}{\isachardot}}intro{\isaliteral{3F}{\isacharquery}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}} \\

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

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

  1355     \quad\qquad \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ \ {\isaliteral{5C3C6C616E676C653E}{\isasymlangle}}proof{\isaliteral{5C3C72616E676C653E}{\isasymrangle}}{\isaliteral{22}{\isachardoublequote}}} \\

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

  1357     \quad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} \\

  1358   \end{matharray}

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

  1361   just by canonical automated tools such as ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{simp}'' or ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{blast}''.  Accordingly, the

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

  1363   introduction rule.

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

  1366   proofs what would be meta-logical existential quantifiers and

  1367   conjunctions.  This concept has a broad range of useful

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

  1369   object-level existential and conjunctions, to elimination over

  1370   results of symbolic evaluation of recursive definitions, for

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

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

  1373   genuine assumption.

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

  1376   be given in parentheses.

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

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

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

  1381   form like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}}, but must not introduce new subgoals.  The

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

  1383   scheme described above.  Obtained parameters \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} are marked as internal by default, which prevents the

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

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

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

  1388   It is important to note that the facts introduced by \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} and \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} may not be polymorphic: any

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

  1390 \end{isamarkuptext}%

  1391 \isamarkuptrue%

  1392 %

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

  1394 }

  1395 \isamarkuptrue%

  1396 %

  1397 \begin{isamarkuptext}%

  1398 \begin{matharray}{rcl}

  1399     \indexdef{}{command}{also}\hypertarget{command.also}{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1400     \indexdef{}{command}{finally}\hypertarget{command.finally}{\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1401     \indexdef{}{command}{moreover}\hypertarget{command.moreover}{\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1402     \indexdef{}{command}{ultimately}\hypertarget{command.ultimately}{\hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1403     \indexdef{}{command}{print\_trans\_rules}\hypertarget{command.print-trans-rules}{\hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

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

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

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

  1407   \end{matharray}

  1409   Calculational proof is forward reasoning with implicit application

  1410   of transitivity rules (such those of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C653E}{\isasymle}}{\isaliteral{22}{\isachardoublequote}}},

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

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

  1413   transitivity composed with the current result.  Command \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} involving \hyperlink{fact.this}{\mbox{\isa{this}}}, while

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

  1415   forward chaining towards the next goal statement.  Both commands

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

  1417   that produce theorems such as \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}, or some finished proof of \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} etc.  The \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}

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

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

  1420   applying any rules yet.

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

  1423   its canonical application with calculational proofs.  It refers to

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

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

  1427   Isabelle/Isar calculations are implicitly subject to block structure

  1428   in the sense that new threads of calculational reasoning are

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

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

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

  1432   required.

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

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

  1436   handling of block-structure.}

  1438   \begin{matharray}{rcl}

  1439     \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}calculation\ {\isaliteral{3D}{\isacharequal}}\ this{\isaliteral{22}{\isachardoublequote}}} \\

  1440     \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}calculation\ {\isaliteral{3D}{\isacharequal}}\ trans\ {\isaliteral{5B}{\isacharbrackleft}}OF\ calculation\ this{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex]

  1441     \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} & \equiv & \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\[0.5ex]

  1442     \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}calculation\ {\isaliteral{3D}{\isacharequal}}\ calculation\ this{\isaliteral{22}{\isachardoublequote}}} \\

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

  1444   \end{matharray}

  1446   \begin{railoutput}

  1447 \rail@begin{2}{}

  1448 \rail@bar

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

  1450 \rail@nextbar{1}

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

  1452 \rail@endbar

  1453 \rail@bar

  1454 \rail@nextbar{1}

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

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

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

  1458 \rail@endbar

  1459 \rail@end

  1460 \rail@begin{3}{}

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

  1462 \rail@bar

  1463 \rail@nextbar{1}

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

  1465 \rail@nextbar{2}

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

  1467 \rail@endbar

  1468 \rail@end

  1469 \end{railoutput}

  1472   \begin{description}

  1474   \item \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} maintains the auxiliary

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

  1476   \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} in some calculational thread initializes \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by \hyperlink{fact.this}{\mbox{\isa{this}}}. Any subsequent \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} on

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

  1478   some transitivity rule applied to \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} and \hyperlink{fact.this}{\mbox{\isa{this}}} (in that order).  Transitivity rules are picked from the

  1479   current context, unless alternative rules are given as explicit

  1480   arguments.

  1482   \item \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} maintaining \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} in the same way as \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}, and concludes the

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

  1484   for forward chaining towards the next goal. Basically, \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} just abbreviates \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\hyperlink{fact.calculation}{\mbox{\isa{calculation}}}.  Typical idioms for concluding

  1485   calculational proofs are ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isaliteral{3F}{\isacharquery}}thesis}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' and ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}''.

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

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

  1489   results only, without applying rules.

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

  1492   rules (for calculational commands \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}) and symmetry rules (for the \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}}

  1493   operation and single step elimination patters) of the current

  1494   context.

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

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

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

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

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

  1503   ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}}'' produces a

  1504   swapped fact derived from that assumption.

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

  1507   explicit single-step elimination proof, such as ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}y\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}''.

  1509   \end{description}%

  1510 \end{isamarkuptext}%

  1511 \isamarkuptrue%

  1512 %

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

  1514 }

  1515 \isamarkuptrue%

  1516 %

  1517 \isamarkupsubsection{Rule contexts%

  1518 }

  1519 \isamarkuptrue%

  1520 %

  1521 \begin{isamarkuptext}%

  1522 \begin{matharray}{rcl}

  1523     \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1524     \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}cases}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

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

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

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

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

  1529   \end{matharray}

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

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

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

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

  1535   verification tasks, which typically involve big induction rules with

  1536   several cases.

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

  1539   local context symbolically: certain proof methods provide an

  1540   environment of named ``cases'' of the form \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}; the effect of ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' is then equivalent to ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''.  Term bindings may be covered as well, notably

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

  1543   By default, the ``terminology'' \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} of

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

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

  1546   rule parameters stem from somewhere outside of the current proof

  1547   text.  By using the explicit form ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' instead, the proof author is able to

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

  1550   \medskip It is important to note that proper use of \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} does not provide means to peek at the current goal state,

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

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

  1553   for each subgoal \isa{{\isaliteral{22}{\isachardoublequote}}i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{22}{\isachardoublequote}}} of the resulting goal state.

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

  1555   the internal tactical machinery intrude the proof text.  In

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

  1557   reasoning tools are usually quite unpredictable.

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

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

  1561   previous theory specifications in a canonical way (say from

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

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

  1565   and the rules involved support this.  By using appropriate

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

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

  1568   derived manually become ready to use in advanced case analysis

  1569   later.

  1571   \begin{railoutput}

  1572 \rail@begin{4}{}

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

  1574 \rail@bar

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

  1576 \rail@nextbar{1}

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

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

  1579 \rail@plus

  1580 \rail@bar

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

  1582 \rail@nextbar{2}

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

  1584 \rail@endbar

  1585 \rail@nextplus{3}

  1586 \rail@endplus

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

  1588 \rail@endbar

  1589 \rail@end

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

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

  1592 \rail@bar

  1593 \rail@nextbar{1}

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

  1595 \rail@endbar

  1596 \rail@end

  1597 \rail@begin{5}{}

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

  1599 \rail@plus

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

  1601 \rail@bar

  1602 \rail@nextbar{1}

  1603 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]

  1604 \rail@plus

  1605 \rail@bar

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

  1607 \rail@nextbar{2}

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

  1609 \rail@endbar

  1610 \rail@nextplus{3}

  1611 \rail@endplus

  1612 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]

  1613 \rail@endbar

  1614 \rail@nextplus{4}

  1615 \rail@endplus

  1616 \rail@end

  1617 \rail@begin{2}{}

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

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

  1620 \rail@plus

  1621 \rail@nextplus{1}

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

  1623 \rail@endplus

  1624 \rail@end

  1625 \rail@begin{3}{}

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

  1627 \rail@plus

  1628 \rail@plus

  1629 \rail@nextplus{1}

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

  1631 \rail@endplus

  1632 \rail@nextplus{2}

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

  1634 \rail@endplus

  1635 \rail@end

  1636 \rail@begin{2}{}

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

  1638 \rail@bar

  1639 \rail@nextbar{1}

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

  1641 \rail@endbar

  1642 \rail@end

  1643 \end{railoutput}

  1646   \begin{description}

  1648   \item \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} invokes a named local

  1649   context \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}, as provided by an

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

  1651   \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}).  The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''.

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

  1654   current state, using Isar proof language notation.

  1656   \item \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares names for

  1657   the local contexts of premises of a theorem; \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}}

  1658   refers to the \emph{prefix} of the list of premises. Each of the

  1659   cases \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} can be of the form \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5B}{\isacharbrackleft}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} where

  1660   the \isa{{\isaliteral{22}{\isachardoublequote}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are the names of the hypotheses in case \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}

  1661   from left to right.

  1663   \item \hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares

  1664   names for the conclusions of a named premise \isa{c}; here \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} refers to the prefix of arguments of a logical formula

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

  1667   Note that proof methods such as \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} already provide a default name for the conclusion as a

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

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

  1671   \item \hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ q\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} renames

  1672   the innermost parameters of premises \isa{{\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{22}{\isachardoublequote}}} of some

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

  1674   leaving the present parameters unchanged.

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

  1677   expose parameters to the proof context.

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

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

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

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

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

  1684   \secref{sec:hol-inductive}).  Rules without any \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declaration given are treated as if \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} had been specified.

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

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

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

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

  1691   \end{description}%

  1692 \end{isamarkuptext}%

  1693 \isamarkuptrue%

  1694 %

  1695 \isamarkupsubsection{Proof methods%

  1696 }

  1697 \isamarkuptrue%

  1698 %

  1699 \begin{isamarkuptext}%

  1700 \begin{matharray}{rcl}

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

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

  1703     \indexdef{}{method}{induction}\hypertarget{method.induction}{\hyperlink{method.induction}{\mbox{\isa{induction}}}} & : & \isa{method} \\

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

  1705   \end{matharray}

  1707   The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, \hyperlink{method.induction}{\mbox{\isa{induction}}},

  1708   and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}

  1709   methods provide a uniform interface to common proof techniques over

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

  1711   The corresponding rules may be specified and instantiated in a

  1712   casual manner.  Furthermore, these methods provide named local

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

  1714   within the subsequent proof text.  This accommodates compact proof

  1715   texts even when reasoning about large specifications.

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

  1718   infrastructure in order to be applicable to structure statements

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

  1720   and parameters separately).  This avoids cumbersome encoding of

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

  1723   Method \hyperlink{method.induction}{\mbox{\isa{induction}}} differs from \hyperlink{method.induct}{\mbox{\isa{induct}}} only in

  1724   the names of the facts in the local context invoked by the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}

  1725   command.

  1727   \begin{railoutput}

  1728 \rail@begin{6}{}

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

  1730 \rail@bar

  1731 \rail@nextbar{1}

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

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

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

  1735 \rail@endbar

  1736 \rail@cr{3}

  1737 \rail@bar

  1738 \rail@nextbar{4}

  1739 \rail@plus

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

  1741 \rail@nextplus{5}

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

  1743 \rail@endplus

  1744 \rail@endbar

  1745 \rail@bar

  1746 \rail@nextbar{4}

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

  1748 \rail@endbar

  1749 \rail@end

  1750 \rail@begin{6}{}

  1751 \rail@bar

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

  1753 \rail@nextbar{1}

  1754 \rail@term{\hyperlink{method.induction}{\mbox{\isa{induction}}}}[]

  1755 \rail@endbar

  1756 \rail@bar

  1757 \rail@nextbar{1}

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

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

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

  1761 \rail@endbar

  1762 \rail@bar

  1763 \rail@nextbar{1}

  1764 \rail@plus

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

  1766 \rail@nextplus{2}

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

  1768 \rail@endplus

  1769 \rail@endbar

  1770 \rail@cr{4}

  1771 \rail@bar

  1772 \rail@nextbar{5}

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

  1774 \rail@endbar

  1775 \rail@bar

  1776 \rail@nextbar{5}

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

  1778 \rail@endbar

  1779 \rail@bar

  1780 \rail@nextbar{5}

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

  1782 \rail@endbar

  1783 \rail@end

  1784 \rail@begin{2}{}

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

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

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

  1788 \rail@bar

  1789 \rail@nextbar{1}

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

  1791 \rail@endbar

  1792 \rail@end

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

  1794 \rail@bar

  1795 \rail@bar

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

  1797 \rail@nextbar{1}

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

  1799 \rail@nextbar{2}

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

  1801 \rail@endbar

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

  1803 \rail@plus

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

  1805 \rail@nextplus{1}

  1806 \rail@endplus

  1807 \rail@nextbar{3}

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

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

  1810 \rail@plus

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

  1812 \rail@nextplus{4}

  1813 \rail@endplus

  1814 \rail@endbar

  1815 \rail@end

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

  1817 \rail@bar

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

  1819 \rail@bar

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

  1821 \rail@nextbar{1}

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

  1823 \rail@endbar

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

  1825 \rail@nextbar{2}

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

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

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

  1829 \rail@nextbar{3}

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

  1831 \rail@endbar

  1832 \rail@end

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

  1834 \rail@plus

  1835 \rail@nextplus{1}

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

  1837 \rail@endplus

  1838 \rail@end

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

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

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

  1842 \rail@plus

  1843 \rail@plus

  1844 \rail@nextplus{1}

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

  1846 \rail@endplus

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

  1848 \rail@nextplus{2}

  1849 \rail@endplus

  1850 \rail@end

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

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

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

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

  1855 \rail@end

  1856 \end{railoutput}

  1859   \begin{description}

  1861   \item \hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} applies method \hyperlink{method.rule}{\mbox{\isa{rule}}} with an appropriate case distinction theorem, instantiated to

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

  1863   to the rule's local contexts.

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

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

  1868   \medskip

  1869   \begin{tabular}{llll}

  1870     facts           &                 & arguments   & rule \\\hline

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

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

  1873     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ t{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} & inductive predicate/set elimination (of \isa{A}) \\

  1874     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}     & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ rule{\isaliteral{3A}{\isacharcolon}}\ R{\isaliteral{22}{\isachardoublequote}}} & explicit rule \isa{R} \\

  1875   \end{tabular}

  1876   \medskip

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

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

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

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

  1882   last premise (it is usually the same for all cases).  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification of

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

  1885   \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} and

  1886   \hyperlink{method.induction}{\mbox{\isa{induction}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} are analogous to the

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

  1888   determined as follows:

  1890   \medskip

  1891   \begin{tabular}{llll}

  1892     facts           &                  & arguments            & rule \\\hline

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

  1894     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ x{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}          & predicate/set induction (of \isa{A}) \\

  1895     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}     & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ rule{\isaliteral{3A}{\isacharcolon}}\ R{\isaliteral{22}{\isachardoublequote}}} & explicit rule \isa{R} \\

  1896   \end{tabular}

  1897   \medskip

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

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

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

  1902   terms \isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} refers to the \emph{suffix} of variables

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

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

  1905   example.

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

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

  1909   discharged after applying the induction rule.  Equalities reappear

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

  1911   induction principle being involved here.  In order to achieve

  1912   practically useful induction hypotheses, some variables occurring in

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

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

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

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

  1917   parentheses.  By default, the equalities generated by definitional

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

  1919   usually consisting of distinctness and injectivity theorems for

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

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

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

  1923   their premises can be simplified to \isa{False}.  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification.

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

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

  1927   The optional ``\isa{{\isaliteral{22}{\isachardoublequote}}arbitrary{\isaliteral{3A}{\isacharcolon}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}''

  1928   specification generalizes variables \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} of the original goal before applying induction.  One can

  1929   separate variables by ``\isa{{\isaliteral{22}{\isachardoublequote}}and{\isaliteral{22}{\isachardoublequote}}}'' to generalize them in other

  1930   goals then the first. Thus induction hypotheses may become

  1931   sufficiently general to get the proof through.  Together with

  1932   definitional instantiations, one may effectively perform induction

  1933   over expressions of a certain structure.

  1935   The optional ``\isa{{\isaliteral{22}{\isachardoublequote}}taking{\isaliteral{3A}{\isacharcolon}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''

  1936   specification provides additional instantiations of a prefix of

  1937   pending variables in the rule.  Such schematic induction rules

  1938   rarely occur in practice, though.

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

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

  1942   determined as follows:

  1944   \medskip

  1945   \begin{tabular}{llll}

  1946     goal          &                    & arguments & rule \\\hline

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

  1948     \isa{{\isaliteral{22}{\isachardoublequote}}A\ x{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} & predicate/set coinduction (of \isa{A}) \\

  1949     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}   & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ rule{\isaliteral{3A}{\isacharcolon}}\ R{\isaliteral{22}{\isachardoublequote}}} & explicit rule \isa{R} \\

  1950   \end{tabular}

  1952   Coinduction is the dual of induction.  Induction essentially

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

  1954   while coinduction introduces \isa{{\isaliteral{22}{\isachardoublequote}}A\ x{\isaliteral{22}{\isachardoublequote}}} starting with \isa{{\isaliteral{22}{\isachardoublequote}}B\ x{\isaliteral{22}{\isachardoublequote}}}, for a suitable ``bisimulation'' \isa{B}.  The cases of a

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

  1956   covered, while the conclusions consist of several alternatives being

  1957   named after the individual destructor patterns.

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

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

  1961   An additional ``\isa{{\isaliteral{22}{\isachardoublequote}}taking{\isaliteral{3A}{\isacharcolon}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}''

  1962   specification may be required in order to specify the bisimulation

  1963   to be used in the coinduction step.

  1965   \end{description}

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

  1968   instantiated rule as given in the text.  Beyond that, the \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} methods guess further instantiations

  1969   from the goal specification itself.  Any persisting unresolved

  1970   schematic variables of the resulting rule will render the the

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

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

  1973   is fully specified.

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

  1976   in the current proof state.

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

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

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

  1981   natural deduction: the context of a structured statement \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}

  1982   reappears unchanged after the case split.

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

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

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

  1987   statement is basically replaced by separate copies, corresponding to

  1988   the induction hypotheses and conclusion; the original goal context

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

  1990   and definitions effectively participate in the inductive rephrasing

  1991   of the original statement.

  1993   In \hyperlink{method.induct}{\mbox{\isa{induct}}} proofs, local assumptions introduced by cases are split

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

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

  1996   extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems},

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

  1999   In \hyperlink{method.induction}{\mbox{\isa{induction}}} proofs, local assumptions introduced by cases are

  2000   split into three different kinds: \isa{IH}, the induction hypotheses,

  2001   \isa{hyps}, the remaining hypotheses stemming from the rule, and

  2002   \isa{prems}, the assumptions from the goal statement. The names are

  2003   \isa{c{\isaliteral{2E}{\isachardot}}IH}, \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems}, as above.

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

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

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

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

  2010   remaining facts are inserted into the goal verbatim before the

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

  2012   applied.%

  2013 \end{isamarkuptext}%

  2014 \isamarkuptrue%

  2015 %

  2016 \isamarkupsubsection{Declaring rules%

  2017 }

  2018 \isamarkuptrue%

  2019 %

  2020 \begin{isamarkuptext}%

  2021 \begin{matharray}{rcl}

  2022     \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{5F}{\isacharunderscore}}rules}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

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

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

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

  2026   \end{matharray}

  2028   \begin{railoutput}

  2029 \rail@begin{1}{}

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

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

  2032 \rail@end

  2033 \rail@begin{1}{}

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

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

  2036 \rail@end

  2037 \rail@begin{1}{}

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

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

  2040 \rail@end

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

  2042 \rail@bar

  2043 \rail@bar

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

  2045 \rail@nextbar{1}

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

  2047 \rail@nextbar{2}

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

  2049 \rail@endbar

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

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

  2052 \rail@nextbar{3}

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

  2054 \rail@endbar

  2055 \rail@end

  2056 \end{railoutput}

  2059   \begin{description}

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

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

  2064   \item \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} (as attributes) declare rules for reasoning about

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

  2066   corresponding methods of the same name.  Certain definitional

  2067   packages of object-logics usually declare emerging cases and

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

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

  2071   covers all of the \isa{{\isaliteral{22}{\isachardoublequote}}type{\isaliteral{22}{\isachardoublequote}}}/\isa{{\isaliteral{22}{\isachardoublequote}}pred{\isaliteral{22}{\isachardoublequote}}}/\isa{{\isaliteral{22}{\isachardoublequote}}set{\isaliteral{22}{\isachardoublequote}}}

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

  2073   some type, predicate, or set.

  2075   Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of

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

  2077   declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.

  2079   \end{description}%

  2080 \end{isamarkuptext}%

  2081 \isamarkuptrue%

  2082 %

  2083 \isadelimtheory

  2084 %

  2085 \endisadelimtheory

  2086 %

  2087 \isatagtheory

  2088 \isacommand{end}\isamarkupfalse%

  2089 %

  2090 \endisatagtheory

  2091 {\isafoldtheory}%

  2092 %

  2093 \isadelimtheory

  2094 %

  2095 \endisadelimtheory

  2096 \isanewline

  2097 \end{isabellebody}%

  2098 %%% Local Variables:

  2099 %%% mode: latex

  2100 %%% TeX-master: "root"

  2101 %%% End:

author	wenzelm
	Mon, 03 Oct 2011 11:14:19 +0200
changeset 45988	a45121ffcfcb
parent 45885	0e847655b2d8
child 46006	5ba2f065c6f7
permissions	-rw-r--r--