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