doc-src/IsarRef/Thy/document/Proof.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 37364 dfca6c4cd1e8
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
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@26869
    12
\isakeyword{imports}\ 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@28788
    34
  \item \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\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@28788
    39
  \item \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\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@28788
    43
  \item \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} is intermediate between \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} and \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\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@36356
    68
\isamarkupsubsection{Example proofs%
wenzelm@36356
    69
}
wenzelm@36356
    70
\isamarkuptrue%
wenzelm@36356
    71
%
wenzelm@36356
    72
\begin{isamarkuptext}%
wenzelm@36356
    73
\begin{matharray}{rcl}
wenzelm@36356
    74
    \indexdef{}{command}{example\_proof}\hypertarget{command.example-proof}{\hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@36356
    75
  \end{matharray}
wenzelm@36356
    76
wenzelm@36356
    77
  \begin{description}
wenzelm@36356
    78
wenzelm@36356
    79
  \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body.  This
wenzelm@36356
    80
  allows to experiment with Isar, without producing any persistent
wenzelm@36356
    81
  result.
wenzelm@36356
    82
wenzelm@36356
    83
  Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
wenzelm@36356
    84
  followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the
wenzelm@36356
    85
  example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
wenzelm@36356
    86
  discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
wenzelm@36356
    87
wenzelm@36356
    88
  \end{description}%
wenzelm@36356
    89
\end{isamarkuptext}%
wenzelm@36356
    90
\isamarkuptrue%
wenzelm@36356
    91
%
wenzelm@28788
    92
\isamarkupsubsection{Blocks%
wenzelm@26870
    93
}
wenzelm@26870
    94
\isamarkuptrue%
wenzelm@26870
    95
%
wenzelm@26870
    96
\begin{isamarkuptext}%
wenzelm@26870
    97
\begin{matharray}{rcl}
wenzelm@28788
    98
    \indexdef{}{command}{next}\hypertarget{command.next}{\hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
    99
    \indexdef{}{command}{\{}\hypertarget{command.braceleft}{\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   100
    \indexdef{}{command}{\}}\hypertarget{command.braceright}{\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   101
  \end{matharray}
wenzelm@28788
   102
wenzelm@28788
   103
  While Isar is inherently block-structured, opening and closing
wenzelm@28788
   104
  blocks is mostly handled rather casually, with little explicit
wenzelm@28788
   105
  user-intervention.  Any local goal statement automatically opens
wenzelm@28788
   106
  \emph{two} internal blocks, which are closed again when concluding
wenzelm@28788
   107
  the sub-proof (by \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} etc.).  Sections of different
wenzelm@28788
   108
  context within a sub-proof may be switched via \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}},
wenzelm@28788
   109
  which is just a single block-close followed by block-open again.
wenzelm@28788
   110
  The effect of \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} is to reset the local proof context;
wenzelm@28788
   111
  there is no goal focus involved here!
wenzelm@28788
   112
wenzelm@28788
   113
  For slightly more advanced applications, there are explicit block
wenzelm@28788
   114
  parentheses as well.  These typically achieve a stronger forward
wenzelm@28788
   115
  style of reasoning.
wenzelm@28788
   116
wenzelm@28788
   117
  \begin{description}
wenzelm@28788
   118
wenzelm@28788
   119
  \item \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} switches to a fresh block within a
wenzelm@28788
   120
  sub-proof, resetting the local context to the initial one.
wenzelm@28788
   121
wenzelm@28788
   122
  \item \hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}} and \hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}} explicitly open and close
wenzelm@28788
   123
  blocks.  Any current facts pass through ``\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}}''
wenzelm@28788
   124
  unchanged, while ``\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}}'' causes any result to be
wenzelm@28788
   125
  \emph{exported} into the enclosing context.  Thus fixed variables
wenzelm@28788
   126
  are generalized, assumptions discharged, and local definitions
wenzelm@28788
   127
  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
wenzelm@28788
   128
  of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} and \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} in this mode of
wenzelm@28788
   129
  forward reasoning --- in contrast to plain backward reasoning with
wenzelm@28788
   130
  the result exported at \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} time.
wenzelm@28788
   131
wenzelm@28788
   132
  \end{description}%
wenzelm@28788
   133
\end{isamarkuptext}%
wenzelm@28788
   134
\isamarkuptrue%
wenzelm@28788
   135
%
wenzelm@28788
   136
\isamarkupsubsection{Omitting proofs%
wenzelm@28788
   137
}
wenzelm@28788
   138
\isamarkuptrue%
wenzelm@28788
   139
%
wenzelm@28788
   140
\begin{isamarkuptext}%
wenzelm@28788
   141
\begin{matharray}{rcl}
wenzelm@28788
   142
    \indexdef{}{command}{oops}\hypertarget{command.oops}{\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
wenzelm@28788
   143
  \end{matharray}
wenzelm@28788
   144
wenzelm@28788
   145
  The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command discontinues the current proof
wenzelm@28788
   146
  attempt, while considering the partial proof text as properly
wenzelm@28788
   147
  processed.  This is conceptually quite different from ``faking''
wenzelm@28788
   148
  actual proofs via \indexref{}{command}{sorry}\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} (see
wenzelm@28788
   149
  \secref{sec:proof-steps}): \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not observe the
wenzelm@28788
   150
  proof structure at all, but goes back right to the theory level.
wenzelm@28788
   151
  Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
wenzelm@28788
   152
  --- there is no intended claim to be able to complete the proof
wenzelm@28788
   153
  anyhow.
wenzelm@28788
   154
wenzelm@28788
   155
  A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
wenzelm@28788
   156
  \emph{within} the system itself, in conjunction with the document
wenzelm@28838
   157
  preparation tools of Isabelle described in \chref{ch:document-prep}.
wenzelm@28788
   158
  Thus partial or even wrong proof attempts can be discussed in a
wenzelm@28788
   159
  logically sound manner.  Note that the Isabelle {\LaTeX} macros can
wenzelm@28788
   160
  be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of
wenzelm@28788
   161
  the keyword ``\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}''.
wenzelm@28788
   162
wenzelm@28788
   163
  \medskip The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command is undo-able, unlike
wenzelm@28788
   164
  \indexref{}{command}{kill}\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} (see \secref{sec:history}).  The effect is to
wenzelm@28788
   165
  get back to the theory just before the opening of the proof.%
wenzelm@28788
   166
\end{isamarkuptext}%
wenzelm@28788
   167
\isamarkuptrue%
wenzelm@28788
   168
%
wenzelm@28788
   169
\isamarkupsection{Statements%
wenzelm@28788
   170
}
wenzelm@28788
   171
\isamarkuptrue%
wenzelm@28788
   172
%
wenzelm@28788
   173
\isamarkupsubsection{Context elements \label{sec:proof-context}%
wenzelm@28788
   174
}
wenzelm@28788
   175
\isamarkuptrue%
wenzelm@28788
   176
%
wenzelm@28788
   177
\begin{isamarkuptext}%
wenzelm@28788
   178
\begin{matharray}{rcl}
wenzelm@28788
   179
    \indexdef{}{command}{fix}\hypertarget{command.fix}{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   180
    \indexdef{}{command}{assume}\hypertarget{command.assume}{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   181
    \indexdef{}{command}{presume}\hypertarget{command.presume}{\hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   182
    \indexdef{}{command}{def}\hypertarget{command.def}{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@26870
   183
  \end{matharray}
wenzelm@26870
   184
wenzelm@26870
   185
  The logical proof context consists of fixed variables and
wenzelm@26870
   186
  assumptions.  The former closely correspond to Skolem constants, or
wenzelm@26870
   187
  meta-level universal quantification as provided by the Isabelle/Pure
wenzelm@26870
   188
  logical framework.  Introducing some \emph{arbitrary, but fixed}
wenzelm@26902
   189
  variable via ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}'' results in a local value
wenzelm@26870
   190
  that may be used in the subsequent proof as any other variable or
wenzelm@26870
   191
  constant.  Furthermore, any result \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} exported from
wenzelm@26870
   192
  the context will be universally closed wrt.\ \isa{x} at the
wenzelm@26870
   193
  outermost level: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} (this is expressed in normal
wenzelm@26870
   194
  form using Isabelle's meta-variables).
wenzelm@26870
   195
wenzelm@26870
   196
  Similarly, introducing some assumption \isa{{\isasymchi}} has two effects.
wenzelm@26870
   197
  On the one hand, a local theorem is created that may be used as a
wenzelm@26870
   198
  fact in subsequent proof steps.  On the other hand, any result
wenzelm@26870
   199
  \isa{{\isachardoublequote}{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} exported from the context becomes conditional wrt.\
wenzelm@26870
   200
  the assumption: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}{\isachardoublequote}}.  Thus, solving an enclosing goal
wenzelm@26870
   201
  using such a result would basically introduce a new subgoal stemming
wenzelm@26870
   202
  from the assumption.  How this situation is handled depends on the
wenzelm@26902
   203
  version of assumption command used: while \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}
wenzelm@26870
   204
  insists on solving the subgoal by unification with some premise of
wenzelm@26902
   205
  the goal, \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves the subgoal unchanged in order
wenzelm@26870
   206
  to be proved later by the user.
wenzelm@26870
   207
wenzelm@26902
   208
  Local definitions, introduced by ``\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', are achieved by combining ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}'' with
wenzelm@26870
   209
  another version of assumption that causes any hypothetical equation
wenzelm@26870
   210
  \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} to be eliminated by the reflexivity rule.  Thus,
wenzelm@26870
   211
  exporting some result \isa{{\isachardoublequote}x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} yields \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}{\isachardoublequote}}.
wenzelm@26870
   212
wenzelm@26870
   213
  \begin{rail}
wenzelm@26870
   214
    'fix' (vars + 'and')
wenzelm@26870
   215
    ;
wenzelm@26870
   216
    ('assume' | 'presume') (props + 'and')
wenzelm@26870
   217
    ;
wenzelm@26870
   218
    'def' (def + 'and')
wenzelm@26870
   219
    ;
wenzelm@26870
   220
    def: thmdecl? \\ name ('==' | equiv) term termpat?
wenzelm@26870
   221
    ;
wenzelm@26870
   222
  \end{rail}
wenzelm@26870
   223
wenzelm@28788
   224
  \begin{description}
wenzelm@26870
   225
  
wenzelm@28788
   226
  \item \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x} introduces a local variable \isa{x} that is \emph{arbitrary, but fixed.}
wenzelm@26870
   227
  
wenzelm@28788
   228
  \item \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduce a local fact \isa{{\isachardoublequote}{\isasymphi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} by
wenzelm@26870
   229
  assumption.  Subsequent results applied to an enclosing goal (e.g.\
wenzelm@26902
   230
  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@26902
   231
  goal, while \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves \isa{{\isasymphi}} as new subgoals.
wenzelm@26870
   232
  
wenzelm@26870
   233
  Several lists of assumptions may be given (separated by
wenzelm@26902
   234
  \indexref{}{keyword}{and}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}; the resulting list of current facts consists
wenzelm@26870
   235
  of all of these concatenated.
wenzelm@26870
   236
  
wenzelm@28788
   237
  \item \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} introduces a local
wenzelm@26870
   238
  (non-polymorphic) definition.  In results exported from the context,
wenzelm@26902
   239
  \isa{x} is replaced by \isa{t}.  Basically, ``\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', with the resulting
wenzelm@26870
   240
  hypothetical equation solved by reflexivity.
wenzelm@26870
   241
  
wenzelm@26870
   242
  The default name for the definitional equation is \isa{x{\isacharunderscore}def}.
wenzelm@26870
   243
  Several simultaneous definitions may be given at the same time.
wenzelm@26870
   244
wenzelm@28788
   245
  \end{description}
wenzelm@26870
   246
wenzelm@26902
   247
  The special name \indexref{}{fact}{prems}\hyperlink{fact.prems}{\mbox{\isa{prems}}} refers to all assumptions of the
wenzelm@26870
   248
  current context as a list of theorems.  This feature should be used
wenzelm@26870
   249
  with great care!  It is better avoided in final proof texts.%
wenzelm@26870
   250
\end{isamarkuptext}%
wenzelm@26870
   251
\isamarkuptrue%
wenzelm@26870
   252
%
wenzelm@28788
   253
\isamarkupsubsection{Term abbreviations \label{sec:term-abbrev}%
wenzelm@26870
   254
}
wenzelm@26870
   255
\isamarkuptrue%
wenzelm@26870
   256
%
wenzelm@26870
   257
\begin{isamarkuptext}%
wenzelm@26870
   258
\begin{matharray}{rcl}
wenzelm@28788
   259
    \indexdef{}{command}{let}\hypertarget{command.let}{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   260
    \indexdef{}{keyword}{is}\hypertarget{keyword.is}{\hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}}} & : & syntax \\
wenzelm@28788
   261
  \end{matharray}
wenzelm@28788
   262
wenzelm@28788
   263
  Abbreviations may be either bound by explicit \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isachardoublequote}p\ {\isasymequiv}\ t{\isachardoublequote}} statements, or by annotating assumptions or
wenzelm@28788
   264
  goal statements with a list of patterns ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''.  In both cases, higher-order matching is invoked to
wenzelm@28788
   265
  bind extra-logical term variables, which may be either named
wenzelm@28788
   266
  schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
wenzelm@28788
   267
  ``\hyperlink{variable.underscore}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
wenzelm@28788
   268
  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
   269
wenzelm@28788
   270
  Polymorphism of term bindings is handled in Hindley-Milner style,
wenzelm@28788
   271
  similar to ML.  Type variables referring to local assumptions or
wenzelm@28788
   272
  open goal statements are \emph{fixed}, while those of finished
wenzelm@28788
   273
  results or bound by \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} may occur in \emph{arbitrary}
wenzelm@28788
   274
  instances later.  Even though actual polymorphism should be rarely
wenzelm@28788
   275
  used in practice, this mechanism is essential to achieve proper
wenzelm@28788
   276
  incremental type-inference, as the user proceeds to build up the
wenzelm@28788
   277
  Isar proof text from left to right.
wenzelm@28788
   278
wenzelm@28788
   279
  \medskip Term abbreviations are quite different from local
wenzelm@28788
   280
  definitions as introduced via \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} (see
wenzelm@28788
   281
  \secref{sec:proof-context}).  The latter are visible within the
wenzelm@28788
   282
  logic as actual equations, while abbreviations disappear during the
wenzelm@28788
   283
  input process just after type checking.  Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
wenzelm@28788
   284
wenzelm@28788
   285
  \begin{rail}
wenzelm@28788
   286
    'let' ((term + 'and') '=' term + 'and')
wenzelm@28788
   287
    ;  
wenzelm@28788
   288
  \end{rail}
wenzelm@28788
   289
wenzelm@28788
   290
  The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \railnonterm{termpat}
wenzelm@28788
   291
  or \railnonterm{proppat} (see \secref{sec:term-decls}).
wenzelm@28788
   292
wenzelm@28788
   293
  \begin{description}
wenzelm@28788
   294
wenzelm@28788
   295
  \item \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ p\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}} binds any
wenzelm@28788
   296
  text variables in patterns \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} by simultaneous
wenzelm@28788
   297
  higher-order matching against terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}}.
wenzelm@28788
   298
wenzelm@28788
   299
  \item \isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}} resembles \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}, but
wenzelm@28788
   300
  matches \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} against the preceding statement.  Also
wenzelm@28788
   301
  note that \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} is not a separate command, but part of
wenzelm@28788
   302
  others (such as \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} etc.).
wenzelm@28788
   303
wenzelm@28788
   304
  \end{description}
wenzelm@28788
   305
wenzelm@28788
   306
  Some \emph{implicit} term abbreviations\index{term abbreviations}
wenzelm@28788
   307
  for goals and facts are available as well.  For any open goal,
wenzelm@28788
   308
  \indexref{}{variable}{thesis}\hyperlink{variable.thesis}{\mbox{\isa{thesis}}} refers to its object-level statement,
wenzelm@28788
   309
  abstracted over any meta-level parameters (if present).  Likewise,
wenzelm@28788
   310
  \indexref{}{variable}{this}\hyperlink{variable.this}{\mbox{\isa{this}}} is bound for fact statements resulting from
wenzelm@28788
   311
  assumptions or finished goals.  In case \hyperlink{variable.this}{\mbox{\isa{this}}} refers to
wenzelm@28788
   312
  an object-logic statement that is an application \isa{{\isachardoublequote}f\ t{\isachardoublequote}}, then
wenzelm@28788
   313
  \isa{t} is bound to the special text variable ``\hyperlink{variable.dots}{\mbox{\isa{{\isasymdots}}}}''
wenzelm@28788
   314
  (three dots).  The canonical application of this convenience are
wenzelm@28788
   315
  calculational proofs (see \secref{sec:calculation}).%
wenzelm@28788
   316
\end{isamarkuptext}%
wenzelm@28788
   317
\isamarkuptrue%
wenzelm@28788
   318
%
wenzelm@28788
   319
\isamarkupsubsection{Facts and forward chaining%
wenzelm@28788
   320
}
wenzelm@28788
   321
\isamarkuptrue%
wenzelm@28788
   322
%
wenzelm@28788
   323
\begin{isamarkuptext}%
wenzelm@28788
   324
\begin{matharray}{rcl}
wenzelm@28788
   325
    \indexdef{}{command}{note}\hypertarget{command.note}{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   326
    \indexdef{}{command}{then}\hypertarget{command.then}{\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   327
    \indexdef{}{command}{from}\hypertarget{command.from}{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   328
    \indexdef{}{command}{with}\hypertarget{command.with}{\hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   329
    \indexdef{}{command}{using}\hypertarget{command.using}{\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   330
    \indexdef{}{command}{unfolding}\hypertarget{command.unfolding}{\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@26870
   331
  \end{matharray}
wenzelm@26870
   332
wenzelm@26870
   333
  New facts are established either by assumption or proof of local
wenzelm@26870
   334
  statements.  Any fact will usually be involved in further proofs,
wenzelm@26870
   335
  either as explicit arguments of proof methods, or when forward
wenzelm@26902
   336
  chaining towards the next goal via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} (and variants);
wenzelm@26902
   337
  \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}} and \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}} are composite forms
wenzelm@26902
   338
  involving \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}.  The \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} elements
wenzelm@26870
   339
  augments the collection of used facts \emph{after} a goal has been
wenzelm@26902
   340
  stated.  Note that the special theorem name \indexref{}{fact}{this}\hyperlink{fact.this}{\mbox{\isa{this}}} refers
wenzelm@26870
   341
  to the most recently established facts, but only \emph{before}
wenzelm@26870
   342
  issuing a follow-up claim.
wenzelm@26870
   343
wenzelm@26870
   344
  \begin{rail}
wenzelm@26870
   345
    'note' (thmdef? thmrefs + 'and')
wenzelm@26870
   346
    ;
wenzelm@26870
   347
    ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
wenzelm@26870
   348
    ;
wenzelm@26870
   349
  \end{rail}
wenzelm@26870
   350
wenzelm@28788
   351
  \begin{description}
wenzelm@26870
   352
wenzelm@28788
   353
  \item \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} recalls existing facts
wenzelm@28788
   354
  \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n{\isachardoublequote}}, binding the result as \isa{a}.  Note that
wenzelm@28788
   355
  attributes may be involved as well, both on the left and right hand
wenzelm@28788
   356
  sides.
wenzelm@26870
   357
wenzelm@28788
   358
  \item \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} indicates forward chaining by the current
wenzelm@26870
   359
  facts in order to establish the goal to be claimed next.  The
wenzelm@26870
   360
  initial proof method invoked to refine that will be offered the
wenzelm@26870
   361
  facts to do ``anything appropriate'' (see also
wenzelm@26902
   362
  \secref{sec:proof-steps}).  For example, method \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}
wenzelm@26870
   363
  (see \secref{sec:pure-meth-att}) would typically do an elimination
wenzelm@26870
   364
  rather than an introduction.  Automatic methods usually insert the
wenzelm@26870
   365
  facts into the goal state before operation.  This provides a simple
wenzelm@26870
   366
  scheme to control relevance of facts in automated proof search.
wenzelm@26870
   367
  
wenzelm@28788
   368
  \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
   369
  equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}''.
wenzelm@26870
   370
  
wenzelm@28788
   371
  \item \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} abbreviates ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n\ {\isasymAND}\ this{\isachardoublequote}}''; thus the forward chaining
wenzelm@28788
   372
  is from earlier facts together with the current ones.
wenzelm@26870
   373
  
wenzelm@28788
   374
  \item \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} augments the facts being
wenzelm@28788
   375
  currently indicated for use by a subsequent refinement step (such as
wenzelm@28788
   376
  \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} or \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).
wenzelm@26870
   377
  
wenzelm@28788
   378
  \item \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} is structurally
wenzelm@28788
   379
  similar to \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}, but unfolds definitional equations
wenzelm@28788
   380
  \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} throughout the goal state and facts.
wenzelm@26870
   381
wenzelm@28788
   382
  \end{description}
wenzelm@26870
   383
wenzelm@26870
   384
  Forward chaining with an empty list of theorems is the same as not
wenzelm@26902
   385
  chaining at all.  Thus ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{nothing}'' has no
wenzelm@26870
   386
  effect apart from entering \isa{{\isachardoublequote}prove{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode, since
wenzelm@26902
   387
  \indexref{}{fact}{nothing}\hyperlink{fact.nothing}{\mbox{\isa{nothing}}} is bound to the empty list of theorems.
wenzelm@26870
   388
wenzelm@26902
   389
  Basic proof methods (such as \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}) expect multiple
wenzelm@26870
   390
  facts to be given in their proper order, corresponding to a prefix
wenzelm@26870
   391
  of the premises of the rule involved.  Note that positions may be
wenzelm@26902
   392
  easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example.  This involves the trivial rule
wenzelm@26870
   393
  \isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
wenzelm@26912
   394
  ``\indexref{}{fact}{\_}\hyperlink{fact.underscore}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore).
wenzelm@26870
   395
wenzelm@26902
   396
  Automated methods (such as \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.auto}{\mbox{\isa{auto}}}) just
wenzelm@26870
   397
  insert any given facts before their usual operation.  Depending on
wenzelm@26870
   398
  the kind of procedure involved, the order of facts is less
wenzelm@26870
   399
  significant here.%
wenzelm@26870
   400
\end{isamarkuptext}%
wenzelm@26870
   401
\isamarkuptrue%
wenzelm@26870
   402
%
wenzelm@28788
   403
\isamarkupsubsection{Goals \label{sec:goals}%
wenzelm@26870
   404
}
wenzelm@26870
   405
\isamarkuptrue%
wenzelm@26870
   406
%
wenzelm@26870
   407
\begin{isamarkuptext}%
wenzelm@26870
   408
\begin{matharray}{rcl}
wenzelm@28788
   409
    \indexdef{}{command}{lemma}\hypertarget{command.lemma}{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   410
    \indexdef{}{command}{theorem}\hypertarget{command.theorem}{\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   411
    \indexdef{}{command}{corollary}\hypertarget{command.corollary}{\hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@36321
   412
    \indexdef{}{command}{schematic\_lemma}\hypertarget{command.schematic-lemma}{\hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}lemma}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@36321
   413
    \indexdef{}{command}{schematic\_theorem}\hypertarget{command.schematic-theorem}{\hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}theorem}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@36321
   414
    \indexdef{}{command}{schematic\_corollary}\hypertarget{command.schematic-corollary}{\hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}corollary}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   415
    \indexdef{}{command}{have}\hypertarget{command.have}{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   416
    \indexdef{}{command}{show}\hypertarget{command.show}{\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   417
    \indexdef{}{command}{hence}\hypertarget{command.hence}{\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   418
    \indexdef{}{command}{thus}\hypertarget{command.thus}{\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   419
    \indexdef{}{command}{print\_statement}\hypertarget{command.print-statement}{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@26870
   420
  \end{matharray}
wenzelm@26870
   421
wenzelm@26870
   422
  From a theory context, proof mode is entered by an initial goal
wenzelm@26902
   423
  command such as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}, \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, or
wenzelm@26902
   424
  \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}.  Within a proof, new claims may be
wenzelm@26870
   425
  introduced locally as well; four variants are available here to
wenzelm@26870
   426
  indicate whether forward chaining of facts should be performed
wenzelm@26902
   427
  initially (via \indexref{}{command}{then}\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}), and whether the final result
wenzelm@26870
   428
  is meant to solve some pending goal.
wenzelm@26870
   429
wenzelm@26870
   430
  Goals may consist of multiple statements, resulting in a list of
wenzelm@26870
   431
  facts eventually.  A pending multi-goal is internally represented as
wenzelm@28857
   432
  a meta-level conjunction (\isa{{\isachardoublequote}{\isacharampersand}{\isacharampersand}{\isacharampersand}{\isachardoublequote}}), which is usually
wenzelm@26870
   433
  split into the corresponding number of sub-goals prior to an initial
wenzelm@26902
   434
  method application, via \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}
wenzelm@26902
   435
  (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}
wenzelm@26902
   436
  (\secref{sec:tactic-commands}).  The \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}} method
wenzelm@26870
   437
  covered in \secref{sec:cases-induct} acts on multiple claims
wenzelm@26870
   438
  simultaneously.
wenzelm@26870
   439
wenzelm@26870
   440
  Claims at the theory level may be either in short or long form.  A
wenzelm@26870
   441
  short goal merely consists of several simultaneous propositions
wenzelm@26870
   442
  (often just one).  A long goal includes an explicit context
wenzelm@26870
   443
  specification for the subsequent conclusion, involving local
wenzelm@26870
   444
  parameters and assumptions.  Here the role of each part of the
wenzelm@26870
   445
  statement is explicitly marked by separate keywords (see also
wenzelm@26870
   446
  \secref{sec:locale}); the local assumptions being introduced here
wenzelm@26902
   447
  are available as \indexref{}{fact}{assms}\hyperlink{fact.assms}{\mbox{\isa{assms}}} in the proof.  Moreover, there
wenzelm@26902
   448
  are two kinds of conclusions: \indexdef{}{element}{shows}\hypertarget{element.shows}{\hyperlink{element.shows}{\mbox{\isa{\isakeyword{shows}}}}} states several
wenzelm@26870
   449
  simultaneous propositions (essentially a big conjunction), while
wenzelm@26902
   450
  \indexdef{}{element}{obtains}\hypertarget{element.obtains}{\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}}} claims several simultaneous simultaneous
wenzelm@26870
   451
  contexts of (essentially a big disjunction of eliminated parameters
wenzelm@26870
   452
  and assumptions, cf.\ \secref{sec:obtain}).
wenzelm@26870
   453
wenzelm@26870
   454
  \begin{rail}
wenzelm@36321
   455
    ('lemma' | 'theorem' | 'corollary' |
wenzelm@40255
   456
     'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
wenzelm@26870
   457
    ;
wenzelm@26870
   458
    ('have' | 'show' | 'hence' | 'thus') goal
wenzelm@26870
   459
    ;
wenzelm@40255
   460
    'print_statement' modes? thmrefs
wenzelm@26870
   461
    ;
wenzelm@26870
   462
  
wenzelm@26870
   463
    goal: (props + 'and')
wenzelm@26870
   464
    ;
wenzelm@26870
   465
    longgoal: thmdecl? (contextelem *) conclusion
wenzelm@26870
   466
    ;
wenzelm@26870
   467
    conclusion: 'shows' goal | 'obtains' (parname? case + '|')
wenzelm@26870
   468
    ;
wenzelm@26870
   469
    case: (vars + 'and') 'where' (props + 'and')
wenzelm@26870
   470
    ;
wenzelm@26870
   471
  \end{rail}
wenzelm@26870
   472
wenzelm@28788
   473
  \begin{description}
wenzelm@26870
   474
  
wenzelm@28788
   475
  \item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} enters proof mode with
wenzelm@26870
   476
  \isa{{\isasymphi}} as main goal, eventually resulting in some fact \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} to be put back into the target context.  An additional
wenzelm@26870
   477
  \railnonterm{context} specification may build up an initial proof
wenzelm@26870
   478
  context for the subsequent claim; this includes local definitions
wenzelm@26902
   479
  and syntax as well, see the definition of \hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}} in
wenzelm@26870
   480
  \secref{sec:locale}.
wenzelm@26870
   481
  
wenzelm@28788
   482
  \item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}, but the facts are internally marked as
wenzelm@26870
   483
  being of a different kind.  This discrimination acts like a formal
wenzelm@26870
   484
  comment.
wenzelm@36321
   485
wenzelm@36321
   486
  \item \hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}lemma}}}}, \hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}theorem}}}},
wenzelm@36321
   487
  \hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}corollary}}}} are similar to \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}},
wenzelm@36321
   488
  \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}, respectively but allow
wenzelm@36321
   489
  the statement to contain unbound schematic variables.
wenzelm@36321
   490
wenzelm@36321
   491
  Under normal circumstances, an Isar proof text needs to specify
wenzelm@36321
   492
  claims explicitly.  Schematic goals are more like goals in Prolog,
wenzelm@36321
   493
  where certain results are synthesized in the course of reasoning.
wenzelm@36321
   494
  With schematic statements, the inherent compositionality of Isar
wenzelm@36321
   495
  proofs is lost, which also impacts performance, because proof
wenzelm@36321
   496
  checking is forced into sequential mode.
wenzelm@26870
   497
  
wenzelm@28788
   498
  \item \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} claims a local goal,
wenzelm@26870
   499
  eventually resulting in a fact within the current logical context.
wenzelm@26870
   500
  This operation is completely independent of any pending sub-goals of
wenzelm@26902
   501
  an enclosing goal statements, so \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} may be freely
wenzelm@26870
   502
  used for experimental exploration of potential results within a
wenzelm@26870
   503
  proof body.
wenzelm@26870
   504
  
wenzelm@28788
   505
  \item \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} is like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} plus a second stage to refine some pending
wenzelm@26870
   506
  sub-goal for each one of the finished result, after having been
wenzelm@26870
   507
  exported into the corresponding context (at the head of the
wenzelm@26902
   508
  sub-proof of this \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} command).
wenzelm@26870
   509
  
wenzelm@26870
   510
  To accommodate interactive debugging, resulting rules are printed
wenzelm@26870
   511
  before being applied internally.  Even more, interactive execution
wenzelm@26902
   512
  of \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} predicts potential failure and displays the
wenzelm@26870
   513
  resulting error as a warning beforehand.  Watch out for the
wenzelm@26870
   514
  following message:
wenzelm@26870
   515
wenzelm@26870
   516
  %FIXME proper antiquitation
wenzelm@26870
   517
  \begin{ttbox}
wenzelm@26870
   518
  Problem! Local statement will fail to solve any pending goal
wenzelm@26870
   519
  \end{ttbox}
wenzelm@26870
   520
  
wenzelm@28788
   521
  \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
   522
  chaining the current facts.  Note that \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} is also
wenzelm@26902
   523
  equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}''.
wenzelm@26870
   524
  
wenzelm@28788
   525
  \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
   526
  ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''.
wenzelm@26870
   527
  
wenzelm@28788
   528
  \item \hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}~\isa{a} prints facts from the
wenzelm@26870
   529
  current theory or proof context in long statement form, according to
wenzelm@26902
   530
  the syntax for \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} given above.
wenzelm@26870
   531
wenzelm@28788
   532
  \end{description}
wenzelm@26870
   533
wenzelm@26870
   534
  Any goal statement causes some term abbreviations (such as
wenzelm@26902
   535
  \indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isacharquery}thesis}}}) to be bound automatically, see also
wenzelm@26961
   536
  \secref{sec:term-abbrev}.
wenzelm@26870
   537
wenzelm@26902
   538
  The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold
wenzelm@26870
   539
  meaning: (1) during the of this claim they refer to the the local
wenzelm@26870
   540
  context introductions, (2) the resulting rule is annotated
wenzelm@26870
   541
  accordingly to support symbolic case splits when used with the
wenzelm@36321
   542
  \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).%
wenzelm@26870
   543
\end{isamarkuptext}%
wenzelm@26870
   544
\isamarkuptrue%
wenzelm@26870
   545
%
wenzelm@28788
   546
\isamarkupsection{Refinement steps%
wenzelm@28788
   547
}
wenzelm@28788
   548
\isamarkuptrue%
wenzelm@28788
   549
%
wenzelm@28788
   550
\isamarkupsubsection{Proof method expressions \label{sec:proof-meth}%
wenzelm@28788
   551
}
wenzelm@28788
   552
\isamarkuptrue%
wenzelm@28788
   553
%
wenzelm@28788
   554
\begin{isamarkuptext}%
wenzelm@28788
   555
Proof methods are either basic ones, or expressions composed of
wenzelm@28788
   556
  methods via ``\verb|,|'' (sequential composition),
wenzelm@28788
   557
  ``\verb||\verb,|,\verb||'' (alternative choices), ``\verb|?|'' 
wenzelm@28788
   558
  (try), ``\verb|+|'' (repeat at least once), ``\verb|[|\isa{n}\verb|]|'' (restriction to first \isa{n}
wenzelm@28788
   559
  sub-goals, with default \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}).  In practice, proof
wenzelm@28788
   560
  methods are usually just a comma separated list of
wenzelm@28788
   561
  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
wenzelm@28788
   562
  parentheses may be dropped for single method specifications (with no
wenzelm@28788
   563
  arguments).
wenzelm@28788
   564
wenzelm@28788
   565
  \indexouternonterm{method}
wenzelm@28788
   566
  \begin{rail}
wenzelm@28788
   567
    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
wenzelm@28788
   568
    ;
wenzelm@28788
   569
    methods: (nameref args | method) + (',' | '|')
wenzelm@28788
   570
    ;
wenzelm@28788
   571
  \end{rail}
wenzelm@28788
   572
wenzelm@28788
   573
  Proper Isar proof methods do \emph{not} admit arbitrary goal
wenzelm@28788
   574
  addressing, but refer either to the first sub-goal or all sub-goals
wenzelm@28788
   575
  uniformly.  The goal restriction operator ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharbrackright}{\isachardoublequote}}''
wenzelm@28788
   576
  evaluates a method expression within a sandbox consisting of the
wenzelm@28788
   577
  first \isa{n} sub-goals (which need to exist).  For example, the
wenzelm@28788
   578
  method ``\isa{{\isachardoublequote}simp{\isacharunderscore}all{\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isachardoublequote}}'' simplifies the first three
wenzelm@28788
   579
  sub-goals, while ``\isa{{\isachardoublequote}{\isacharparenleft}rule\ foo{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}'' simplifies all
wenzelm@28788
   580
  new goals that emerge from applying rule \isa{{\isachardoublequote}foo{\isachardoublequote}} to the
wenzelm@28788
   581
  originally first one.
wenzelm@28788
   582
wenzelm@28788
   583
  Improper methods, notably tactic emulations, offer a separate
wenzelm@28788
   584
  low-level goal addressing scheme as explicit argument to the
wenzelm@28788
   585
  individual tactic being involved.  Here ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' refers to
wenzelm@28788
   586
  all goals, and ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharminus}{\isacharbrackright}{\isachardoublequote}}'' to all goals starting from \isa{{\isachardoublequote}n{\isachardoublequote}}.
wenzelm@28788
   587
wenzelm@28788
   588
  \indexouternonterm{goalspec}
wenzelm@28788
   589
  \begin{rail}
wenzelm@28788
   590
    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
wenzelm@28788
   591
    ;
wenzelm@28788
   592
  \end{rail}%
wenzelm@28788
   593
\end{isamarkuptext}%
wenzelm@28788
   594
\isamarkuptrue%
wenzelm@28788
   595
%
wenzelm@28788
   596
\isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}%
wenzelm@26870
   597
}
wenzelm@26870
   598
\isamarkuptrue%
wenzelm@26870
   599
%
wenzelm@26870
   600
\begin{isamarkuptext}%
wenzelm@26870
   601
\begin{matharray}{rcl}
wenzelm@28788
   602
    \indexdef{}{command}{proof}\hypertarget{command.proof}{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   603
    \indexdef{}{command}{qed}\hypertarget{command.qed}{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
wenzelm@28788
   604
    \indexdef{}{command}{by}\hypertarget{command.by}{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
wenzelm@28788
   605
    \indexdef{}{command}{..}\hypertarget{command.ddot}{\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
wenzelm@28788
   606
    \indexdef{}{command}{.}\hypertarget{command.dot}{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
wenzelm@28788
   607
    \indexdef{}{command}{sorry}\hypertarget{command.sorry}{\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
wenzelm@26870
   608
  \end{matharray}
wenzelm@26870
   609
wenzelm@26870
   610
  Arbitrary goal refinement via tactics is considered harmful.
wenzelm@26870
   611
  Structured proof composition in Isar admits proof methods to be
wenzelm@26870
   612
  invoked in two places only.
wenzelm@26870
   613
wenzelm@26870
   614
  \begin{enumerate}
wenzelm@26870
   615
wenzelm@26902
   616
  \item An \emph{initial} refinement step \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} reduces a newly stated goal to a number
wenzelm@26870
   617
  of sub-goals that are to be solved later.  Facts are passed to
wenzelm@26870
   618
  \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} for forward chaining, if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
wenzelm@26870
   619
  
wenzelm@26902
   620
  \item A \emph{terminal} conclusion step \indexref{}{command}{qed}\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} is intended to solve remaining goals.  No facts are
wenzelm@26870
   621
  passed to \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
wenzelm@26870
   622
wenzelm@26870
   623
  \end{enumerate}
wenzelm@26870
   624
wenzelm@26870
   625
  The only other (proper) way to affect pending goals in a proof body
wenzelm@26902
   626
  is by \indexref{}{command}{show}\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, which involves an explicit statement of
wenzelm@26870
   627
  what is to be solved eventually.  Thus we avoid the fundamental
wenzelm@26870
   628
  problem of unstructured tactic scripts that consist of numerous
wenzelm@26870
   629
  consecutive goal transformations, with invisible effects.
wenzelm@26870
   630
wenzelm@26870
   631
  \medskip As a general rule of thumb for good proof style, initial
wenzelm@26870
   632
  proof methods should either solve the goal completely, or constitute
wenzelm@26870
   633
  some well-understood reduction to new sub-goals.  Arbitrary
wenzelm@26870
   634
  automatic proof tools that are prone leave a large number of badly
wenzelm@26870
   635
  structured sub-goals are no help in continuing the proof document in
wenzelm@26870
   636
  an intelligible manner.
wenzelm@26870
   637
wenzelm@26870
   638
  Unless given explicitly by the user, the default initial method is
wenzelm@26902
   639
  ``\indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}'', which applies a single standard elimination
wenzelm@26870
   640
  or introduction rule according to the topmost symbol involved.
wenzelm@26870
   641
  There is no separate default terminal method.  Any remaining goals
wenzelm@26870
   642
  are always solved by assumption in the very last step.
wenzelm@26870
   643
wenzelm@26870
   644
  \begin{rail}
wenzelm@26870
   645
    'proof' method?
wenzelm@26870
   646
    ;
wenzelm@26870
   647
    'qed' method?
wenzelm@26870
   648
    ;
wenzelm@26870
   649
    'by' method method?
wenzelm@26870
   650
    ;
wenzelm@26870
   651
    ('.' | '..' | 'sorry')
wenzelm@26870
   652
    ;
wenzelm@26870
   653
  \end{rail}
wenzelm@26870
   654
wenzelm@28788
   655
  \begin{description}
wenzelm@26870
   656
  
wenzelm@28788
   657
  \item \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} refines the goal by proof
wenzelm@28788
   658
  method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}; facts for forward chaining are passed if so
wenzelm@28788
   659
  indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
wenzelm@26870
   660
  
wenzelm@28788
   661
  \item \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} refines any remaining goals by
wenzelm@28788
   662
  proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} and concludes the sub-proof by assumption.
wenzelm@28788
   663
  If the goal had been \isa{{\isachardoublequote}show{\isachardoublequote}} (or \isa{{\isachardoublequote}thus{\isachardoublequote}}), some
wenzelm@28788
   664
  pending sub-goal is solved as well by the rule resulting from the
wenzelm@28788
   665
  result \emph{exported} into the enclosing goal context.  Thus \isa{{\isachardoublequote}qed{\isachardoublequote}} may fail for two reasons: either \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} fails, or the
wenzelm@28788
   666
  resulting rule does not fit to any pending goal\footnote{This
wenzelm@28788
   667
  includes any additional ``strong'' assumptions as introduced by
wenzelm@28788
   668
  \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}.} of the enclosing context.  Debugging such a
wenzelm@28788
   669
  situation might involve temporarily changing \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} into
wenzelm@28788
   670
  \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, or weakening the local context by replacing
wenzelm@28788
   671
  occurrences of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} by \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}.
wenzelm@26870
   672
  
wenzelm@28788
   673
  \item \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} is a \emph{terminal
wenzelm@28788
   674
  proof}\index{proof!terminal}; it abbreviates \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\isa{{\isachardoublequote}qed{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}, but with
wenzelm@28788
   675
  backtracking across both methods.  Debugging an unsuccessful
wenzelm@28788
   676
  \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} command can be done by expanding its
wenzelm@28788
   677
  definition; in many cases \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} (or even
wenzelm@28788
   678
  \isa{{\isachardoublequote}apply{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}) is already sufficient to see the
wenzelm@26870
   679
  problem.
wenzelm@26870
   680
wenzelm@28788
   681
  \item ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' is a \emph{default
wenzelm@26902
   682
  proof}\index{proof!default}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}rule{\isachardoublequote}}.
wenzelm@26870
   683
wenzelm@28788
   684
  \item ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' is a \emph{trivial
wenzelm@26902
   685
  proof}\index{proof!trivial}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}this{\isachardoublequote}}.
wenzelm@26870
   686
  
wenzelm@28788
   687
  \item \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is a \emph{fake proof}\index{proof!fake}
wenzelm@26870
   688
  pretending to solve the pending claim without further ado.  This
wenzelm@26870
   689
  only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML).  Facts emerging from fake
wenzelm@26870
   690
  proofs are not the real thing.  Internally, each theorem container
wenzelm@26870
   691
  is tainted by an oracle invocation, which is indicated as ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' in the printed result.
wenzelm@26870
   692
  
wenzelm@26902
   693
  The most important application of \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is to support
wenzelm@26870
   694
  experimentation and top-down proof development.
wenzelm@26870
   695
wenzelm@28788
   696
  \end{description}%
wenzelm@26870
   697
\end{isamarkuptext}%
wenzelm@26870
   698
\isamarkuptrue%
wenzelm@26870
   699
%
wenzelm@28788
   700
\isamarkupsubsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
wenzelm@26870
   701
}
wenzelm@26870
   702
\isamarkuptrue%
wenzelm@26870
   703
%
wenzelm@26870
   704
\begin{isamarkuptext}%
wenzelm@26870
   705
The following proof methods and attributes refer to basic logical
wenzelm@26870
   706
  operations of Isar.  Further methods and attributes are provided by
wenzelm@26870
   707
  several generic and object-logic specific tools and packages (see
wenzelm@26870
   708
  \chref{ch:gen-tools} and \chref{ch:hol}).
wenzelm@26870
   709
wenzelm@26870
   710
  \begin{matharray}{rcl}
wenzelm@28788
   711
    \indexdef{}{method}{-}\hypertarget{method.-}{\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}} & : & \isa{method} \\
wenzelm@28788
   712
    \indexdef{}{method}{fact}\hypertarget{method.fact}{\hyperlink{method.fact}{\mbox{\isa{fact}}}} & : & \isa{method} \\
wenzelm@28788
   713
    \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
wenzelm@28788
   714
    \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
wenzelm@28788
   715
    \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
wenzelm@28788
   716
    \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
wenzelm@28788
   717
    \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
wenzelm@28788
   718
    \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
wenzelm@28788
   719
    \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
wenzelm@28788
   720
    \indexdef{}{attribute}{OF}\hypertarget{attribute.OF}{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}} & : & \isa{attribute} \\
wenzelm@28788
   721
    \indexdef{}{attribute}{of}\hypertarget{attribute.of}{\hyperlink{attribute.of}{\mbox{\isa{of}}}} & : & \isa{attribute} \\
wenzelm@28788
   722
    \indexdef{}{attribute}{where}\hypertarget{attribute.where}{\hyperlink{attribute.where}{\mbox{\isa{where}}}} & : & \isa{attribute} \\
wenzelm@26870
   723
  \end{matharray}
wenzelm@26870
   724
wenzelm@26870
   725
  \begin{rail}
wenzelm@26870
   726
    'fact' thmrefs?
wenzelm@26870
   727
    ;
wenzelm@26870
   728
    'rule' thmrefs?
wenzelm@26870
   729
    ;
wenzelm@26870
   730
    rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
wenzelm@26870
   731
    ;
wenzelm@26870
   732
    ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
wenzelm@26870
   733
    ;
wenzelm@26870
   734
    'rule' 'del'
wenzelm@26870
   735
    ;
wenzelm@26870
   736
    'OF' thmrefs
wenzelm@26870
   737
    ;
wenzelm@26870
   738
    'of' insts ('concl' ':' insts)?
wenzelm@26870
   739
    ;
wenzelm@26870
   740
    'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
wenzelm@26870
   741
    ;
wenzelm@26870
   742
  \end{rail}
wenzelm@26870
   743
wenzelm@28788
   744
  \begin{description}
wenzelm@26870
   745
  
wenzelm@28788
   746
  \item ``\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}'' (minus) does nothing but insert the forward
wenzelm@28788
   747
  chaining facts as premises into the goal.  Note that command
wenzelm@26902
   748
  \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} without any method actually performs a single
wenzelm@26902
   749
  reduction step using the \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}} method; thus a plain
wenzelm@26902
   750
  \emph{do-nothing} proof step would be ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' rather than \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} alone.
wenzelm@26870
   751
  
wenzelm@28788
   752
  \item \hyperlink{method.fact}{\mbox{\isa{fact}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} composes some fact from
wenzelm@28788
   753
  \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} (or implicitly from the current proof context)
wenzelm@28788
   754
  modulo unification of schematic type and term variables.  The rule
wenzelm@28788
   755
  structure is not taken into account, i.e.\ meta-level implication is
wenzelm@28788
   756
  considered atomic.  This is the same principle underlying literal
wenzelm@28788
   757
  facts (cf.\ \secref{sec:syn-att}): ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{fact}'' is equivalent to ``\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\verb|`|\isa{{\isasymphi}}\verb|`|'' provided that
wenzelm@28788
   758
  \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} is an instance of some known \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} in the
wenzelm@28788
   759
  proof context.
wenzelm@26870
   760
  
wenzelm@28788
   761
  \item \hyperlink{method.assumption}{\mbox{\isa{assumption}}} solves some goal by a single assumption
wenzelm@26870
   762
  step.  All given facts are guaranteed to participate in the
wenzelm@26870
   763
  refinement; this means there may be only 0 or 1 in the first place.
wenzelm@26902
   764
  Recall that \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} (\secref{sec:proof-steps}) already
wenzelm@26870
   765
  concludes any remaining sub-goals by assumption, so structured
wenzelm@26902
   766
  proofs usually need not quote the \hyperlink{method.assumption}{\mbox{\isa{assumption}}} method at
wenzelm@26870
   767
  all.
wenzelm@26870
   768
  
wenzelm@28788
   769
  \item \hyperlink{method.this}{\mbox{\isa{this}}} applies all of the current facts directly as
wenzelm@26902
   770
  rules.  Recall that ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' (dot) abbreviates ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{this}''.
wenzelm@26870
   771
  
wenzelm@28788
   772
  \item \hyperlink{method.rule}{\mbox{\isa{rule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some rule given as
wenzelm@28788
   773
  argument in backward manner; facts are used to reduce the rule
wenzelm@28788
   774
  before applying it to the goal.  Thus \hyperlink{method.rule}{\mbox{\isa{rule}}} without facts
wenzelm@28788
   775
  is plain introduction, while with facts it becomes elimination.
wenzelm@26870
   776
  
wenzelm@26902
   777
  When no arguments are given, the \hyperlink{method.rule}{\mbox{\isa{rule}}} method tries to pick
wenzelm@26870
   778
  appropriate rules automatically, as declared in the current context
wenzelm@26902
   779
  using the \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}},
wenzelm@26902
   780
  \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} attributes (see below).  This is the
wenzelm@26902
   781
  default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' 
wenzelm@26902
   782
  (double-dot) steps (see \secref{sec:proof-steps}).
wenzelm@26870
   783
  
wenzelm@28788
   784
  \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
wenzelm@28788
   785
  \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
wenzelm@30172
   786
  destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
wenzelm@30172
   787
  tools.  Note that the latter will ignore rules declared with
wenzelm@30172
   788
  ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  are used most aggressively.
wenzelm@26870
   789
  
wenzelm@26870
   790
  The classical reasoner (see \secref{sec:classical}) introduces its
wenzelm@26870
   791
  own variants of these attributes; use qualified names to access the
wenzelm@26902
   792
  present versions of Isabelle/Pure, i.e.\ \hyperlink{attribute.Pure.Pure.intro}{\mbox{\isa{Pure{\isachardot}intro}}}.
wenzelm@26870
   793
  
wenzelm@28788
   794
  \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
wenzelm@26870
   795
  elimination, or destruct rules.
wenzelm@26870
   796
  
wenzelm@30463
   797
  \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some
wenzelm@30463
   798
  theorem to all of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}
wenzelm@30463
   799
  (in parallel).  This corresponds to the \verb|op MRS| operation in
wenzelm@30463
   800
  ML, but note the reversed order.  Positions may be effectively
wenzelm@30463
   801
  skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
wenzelm@26870
   802
  
wenzelm@28788
   803
  \item \hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}} performs positional
wenzelm@28788
   804
  instantiation of term variables.  The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are
wenzelm@28788
   805
  substituted for any schematic variables occurring in a theorem from
wenzelm@28788
   806
  left to right; ``\isa{{\isacharunderscore}}'' (underscore) indicates to skip a
wenzelm@28788
   807
  position.  Arguments following a ``\isa{{\isachardoublequote}concl{\isacharcolon}{\isachardoublequote}}'' specification
wenzelm@28788
   808
  refer to positions of the conclusion of a rule.
wenzelm@26870
   809
  
wenzelm@28788
   810
  \item \hyperlink{attribute.where}{\mbox{\isa{where}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}
wenzelm@28788
   811
  performs named instantiation of schematic type and term variables
wenzelm@28788
   812
  occurring in a theorem.  Schematic variables have to be specified on
wenzelm@28788
   813
  the left-hand side (e.g.\ \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}{\isachardoublequote}}).  The question mark may
wenzelm@28788
   814
  be omitted if the variable name is a plain identifier without index.
wenzelm@28788
   815
  As type instantiations are inferred from term instantiations,
wenzelm@28788
   816
  explicit type instantiations are seldom necessary.
wenzelm@26870
   817
wenzelm@28788
   818
  \end{description}%
wenzelm@26870
   819
\end{isamarkuptext}%
wenzelm@26870
   820
\isamarkuptrue%
wenzelm@26870
   821
%
wenzelm@28788
   822
\isamarkupsubsection{Emulating tactic scripts \label{sec:tactic-commands}%
wenzelm@26870
   823
}
wenzelm@26870
   824
\isamarkuptrue%
wenzelm@26870
   825
%
wenzelm@26870
   826
\begin{isamarkuptext}%
wenzelm@26870
   827
The Isar provides separate commands to accommodate tactic-style
wenzelm@26870
   828
  proof scripts within the same system.  While being outside the
wenzelm@26870
   829
  orthodox Isar proof language, these might come in handy for
wenzelm@26870
   830
  interactive exploration and debugging, or even actual tactical proof
wenzelm@26870
   831
  within new-style theories (to benefit from document preparation, for
wenzelm@26870
   832
  example).  See also \secref{sec:tactics} for actual tactics, that
wenzelm@26870
   833
  have been encapsulated as proof methods.  Proper proof methods may
wenzelm@26870
   834
  be used in scripts, too.
wenzelm@26870
   835
wenzelm@26870
   836
  \begin{matharray}{rcl}
wenzelm@28788
   837
    \indexdef{}{command}{apply}\hypertarget{command.apply}{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   838
    \indexdef{}{command}{apply\_end}\hypertarget{command.apply-end}{\hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   839
    \indexdef{}{command}{done}\hypertarget{command.done}{\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
wenzelm@28788
   840
    \indexdef{}{command}{defer}\hypertarget{command.defer}{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@28788
   841
    \indexdef{}{command}{prefer}\hypertarget{command.prefer}{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@28788
   842
    \indexdef{}{command}{back}\hypertarget{command.back}{\hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@26870
   843
  \end{matharray}
wenzelm@26870
   844
wenzelm@26870
   845
  \begin{rail}
wenzelm@40255
   846
    ( 'apply' | 'apply_end' ) method
wenzelm@26870
   847
    ;
wenzelm@26870
   848
    'defer' nat?
wenzelm@26870
   849
    ;
wenzelm@26870
   850
    'prefer' nat
wenzelm@26870
   851
    ;
wenzelm@26870
   852
  \end{rail}
wenzelm@26870
   853
wenzelm@28788
   854
  \begin{description}
wenzelm@26870
   855
wenzelm@28788
   856
  \item \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{m} applies proof method \isa{m} in
wenzelm@28788
   857
  initial position, but unlike \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} it retains ``\isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}'' mode.  Thus consecutive method applications may be
wenzelm@28788
   858
  given just as in tactic scripts.
wenzelm@26870
   859
  
wenzelm@26870
   860
  Facts are passed to \isa{m} as indicated by the goal's
wenzelm@26870
   861
  forward-chain mode, and are \emph{consumed} afterwards.  Thus any
wenzelm@26902
   862
  further \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command would always work in a purely
wenzelm@26870
   863
  backward manner.
wenzelm@26870
   864
  
wenzelm@28788
   865
  \item \hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}~\isa{{\isachardoublequote}m{\isachardoublequote}} applies proof method \isa{m} as if in terminal position.  Basically, this simulates a
wenzelm@26902
   866
  multi-step tactic script for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, but may be given
wenzelm@26870
   867
  anywhere within the proof body.
wenzelm@26870
   868
  
wenzelm@26895
   869
  No facts are passed to \isa{m} here.  Furthermore, the static
wenzelm@26902
   870
  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
   871
  introduced in the current body, for example.
wenzelm@26870
   872
  
wenzelm@28788
   873
  \item \hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} completes a proof script, provided that the
wenzelm@28788
   874
  current goal state is solved completely.  Note that actual
wenzelm@26902
   875
  structured proof commands (e.g.\ ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' or \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}) may be used to conclude proof scripts as well.
wenzelm@26870
   876
wenzelm@28788
   877
  \item \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}~\isa{n} and \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}~\isa{n}
wenzelm@28788
   878
  shuffle the list of pending goals: \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}} puts off
wenzelm@26870
   879
  sub-goal \isa{n} to the end of the list (\isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}} by
wenzelm@26902
   880
  default), while \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}} brings sub-goal \isa{n} to the
wenzelm@26870
   881
  front.
wenzelm@26870
   882
  
wenzelm@28788
   883
  \item \hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}} does back-tracking over the result sequence
wenzelm@28788
   884
  of the latest proof command.  Basically, any proof command may
wenzelm@28788
   885
  return multiple results.
wenzelm@26870
   886
  
wenzelm@28788
   887
  \end{description}
wenzelm@26870
   888
wenzelm@26870
   889
  Any proper Isar proof method may be used with tactic script commands
wenzelm@26902
   890
  such as \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}.  A few additional emulations of actual
wenzelm@26870
   891
  tactics are provided as well; these would be never used in actual
wenzelm@26870
   892
  structured proofs, of course.%
wenzelm@26870
   893
\end{isamarkuptext}%
wenzelm@26870
   894
\isamarkuptrue%
wenzelm@26870
   895
%
wenzelm@28788
   896
\isamarkupsubsection{Defining proof methods%
wenzelm@26870
   897
}
wenzelm@26870
   898
\isamarkuptrue%
wenzelm@26870
   899
%
wenzelm@26870
   900
\begin{isamarkuptext}%
wenzelm@26870
   901
\begin{matharray}{rcl}
wenzelm@28788
   902
    \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@26870
   903
  \end{matharray}
wenzelm@26870
   904
wenzelm@28788
   905
  \begin{rail}
wenzelm@40255
   906
    'method_setup' name '=' text text
wenzelm@28788
   907
    ;
wenzelm@28788
   908
  \end{rail}
wenzelm@28788
   909
wenzelm@28788
   910
  \begin{description}
wenzelm@28788
   911
wenzelm@28788
   912
  \item \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
wenzelm@30548
   913
  defines a proof method in the current theory.  The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
wenzelm@30548
   914
  \verb|(Proof.context -> Proof.method) context_parser|, cf.\
wenzelm@30548
   915
  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
   916
  methods; the primed versions refer to tactics with explicit goal
wenzelm@30548
   917
  addressing.
wenzelm@26870
   918
wenzelm@30548
   919
  Here are some example method definitions:
wenzelm@28788
   920
wenzelm@28788
   921
  \end{description}%
wenzelm@26870
   922
\end{isamarkuptext}%
wenzelm@26870
   923
\isamarkuptrue%
wenzelm@26870
   924
%
wenzelm@30548
   925
\isadelimML
wenzelm@30548
   926
\ \ \ \ %
wenzelm@30548
   927
\endisadelimML
wenzelm@30548
   928
%
wenzelm@30548
   929
\isatagML
wenzelm@30548
   930
\isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
wenzelm@30548
   931
\ my{\isacharunderscore}method{\isadigit{1}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
wenzelm@30548
   932
\ \ \ \ \ \ Scan{\isachardot}succeed\ {\isacharparenleft}K\ {\isacharparenleft}SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
wenzelm@30548
   933
\ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ first\ method\ {\isacharparenleft}without\ any\ arguments{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@30548
   934
\isanewline
wenzelm@30548
   935
\ \ \ \ \isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
wenzelm@30548
   936
\ my{\isacharunderscore}method{\isadigit{2}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
wenzelm@30548
   937
\ \ \ \ \ \ Scan{\isachardot}succeed\ {\isacharparenleft}fn\ ctxt{\isacharcolon}\ Proof{\isachardot}context\ {\isacharequal}{\isachargreater}\isanewline
wenzelm@30548
   938
\ \ \ \ \ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}\isanewline
wenzelm@30548
   939
\ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ second\ method\ {\isacharparenleft}with\ context{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@30548
   940
\isanewline
wenzelm@30548
   941
\ \ \ \ \isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
wenzelm@30548
   942
\ my{\isacharunderscore}method{\isadigit{3}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
wenzelm@30548
   943
\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ thms{\isacharcolon}\ thm\ list\ {\isacharequal}{\isachargreater}\ fn\ ctxt{\isacharcolon}\ Proof{\isachardot}context\ {\isacharequal}{\isachargreater}\isanewline
wenzelm@30548
   944
\ \ \ \ \ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}\isanewline
wenzelm@30548
   945
\ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ third\ method\ {\isacharparenleft}with\ theorem\ arguments\ and\ context{\isacharparenright}{\isachardoublequoteclose}%
wenzelm@30548
   946
\endisatagML
wenzelm@30548
   947
{\isafoldML}%
wenzelm@30548
   948
%
wenzelm@30548
   949
\isadelimML
wenzelm@30548
   950
%
wenzelm@30548
   951
\endisadelimML
wenzelm@30548
   952
%
wenzelm@26870
   953
\isamarkupsection{Generalized elimination \label{sec:obtain}%
wenzelm@26870
   954
}
wenzelm@26870
   955
\isamarkuptrue%
wenzelm@26870
   956
%
wenzelm@26870
   957
\begin{isamarkuptext}%
wenzelm@26870
   958
\begin{matharray}{rcl}
wenzelm@28788
   959
    \indexdef{}{command}{obtain}\hypertarget{command.obtain}{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
   960
    \indexdef{}{command}{guess}\hypertarget{command.guess}{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
wenzelm@26870
   961
  \end{matharray}
wenzelm@26870
   962
wenzelm@26870
   963
  Generalized elimination means that additional elements with certain
wenzelm@26870
   964
  properties may be introduced in the current context, by virtue of a
wenzelm@26870
   965
  locally proven ``soundness statement''.  Technically speaking, the
wenzelm@26902
   966
  \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} language element is like a declaration of
wenzelm@26902
   967
  \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} (see also see
wenzelm@26870
   968
  \secref{sec:proof-context}), together with a soundness proof of its
wenzelm@26870
   969
  additional claim.  According to the nature of existential reasoning,
wenzelm@26870
   970
  assumptions get eliminated from any result exported from the context
wenzelm@26870
   971
  later, provided that the corresponding parameters do \emph{not}
wenzelm@26870
   972
  occur in the conclusion.
wenzelm@26870
   973
wenzelm@26870
   974
  \begin{rail}
wenzelm@26870
   975
    'obtain' parname? (vars + 'and') 'where' (props + 'and')
wenzelm@26870
   976
    ;
wenzelm@26870
   977
    'guess' (vars + 'and')
wenzelm@26870
   978
    ;
wenzelm@26870
   979
  \end{rail}
wenzelm@26870
   980
wenzelm@26902
   981
  The derived Isar command \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} is defined as follows
wenzelm@26870
   982
  (where \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k{\isachardoublequote}} shall refer to (optional)
wenzelm@26870
   983
  facts indicated for forward chaining).
wenzelm@26870
   984
  \begin{matharray}{l}
wenzelm@26902
   985
    \isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[1ex]
wenzelm@26902
   986
    \quad \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
wenzelm@29731
   987
    \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\hyperlink{method.succeed}{\mbox{\isa{succeed}}} \\
wenzelm@26902
   988
    \qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\
wenzelm@26902
   989
    \qquad \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
wenzelm@26902
   990
    \qquad \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis} \\
wenzelm@26902
   991
    \quad\qquad \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{{\isacharminus}} \\
wenzelm@26902
   992
    \quad\qquad \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
wenzelm@26902
   993
    \quad \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} \\
wenzelm@26902
   994
    \quad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} \\
wenzelm@26870
   995
  \end{matharray}
wenzelm@26870
   996
wenzelm@26870
   997
  Typically, the soundness proof is relatively straight-forward, often
wenzelm@26902
   998
  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
   999
  ``\isa{that}'' reduction above is declared as simplification and
wenzelm@26870
  1000
  introduction rule.
wenzelm@26870
  1001
wenzelm@26902
  1002
  In a sense, \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} represents at the level of Isar
wenzelm@26870
  1003
  proofs what would be meta-logical existential quantifiers and
wenzelm@26870
  1004
  conjunctions.  This concept has a broad range of useful
wenzelm@26870
  1005
  applications, ranging from plain elimination (or introduction) of
wenzelm@26870
  1006
  object-level existential and conjunctions, to elimination over
wenzelm@26870
  1007
  results of symbolic evaluation of recursive definitions, for
wenzelm@26902
  1008
  example.  Also note that \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} without parameters acts
wenzelm@26902
  1009
  much like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, where the result is treated as a
wenzelm@26870
  1010
  genuine assumption.
wenzelm@26870
  1011
wenzelm@26870
  1012
  An alternative name to be used instead of ``\isa{that}'' above may
wenzelm@26870
  1013
  be given in parentheses.
wenzelm@26870
  1014
wenzelm@26902
  1015
  \medskip The improper variant \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} is similar to
wenzelm@26902
  1016
  \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}, but derives the obtained statement from the
wenzelm@26870
  1017
  course of reasoning!  The proof starts with a fixed goal \isa{thesis}.  The subsequent proof may refine this to anything of the
wenzelm@26870
  1018
  form like \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}}, but must not introduce new subgoals.  The
wenzelm@26870
  1019
  final goal state is then used as reduction rule for the obtain
wenzelm@26870
  1020
  scheme described above.  Obtained parameters \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} are marked as internal by default, which prevents the
wenzelm@26870
  1021
  proof context from being polluted by ad-hoc variables.  The variable
wenzelm@26902
  1022
  names and type constraints given as arguments for \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}
wenzelm@26870
  1023
  specify a prefix of obtained parameters explicitly in the text.
wenzelm@26870
  1024
wenzelm@26902
  1025
  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
  1026
  type-variables occurring here are fixed in the present context!%
wenzelm@26870
  1027
\end{isamarkuptext}%
wenzelm@26870
  1028
\isamarkuptrue%
wenzelm@26870
  1029
%
wenzelm@26870
  1030
\isamarkupsection{Calculational reasoning \label{sec:calculation}%
wenzelm@26870
  1031
}
wenzelm@26870
  1032
\isamarkuptrue%
wenzelm@26870
  1033
%
wenzelm@26870
  1034
\begin{isamarkuptext}%
wenzelm@26870
  1035
\begin{matharray}{rcl}
wenzelm@28788
  1036
    \indexdef{}{command}{also}\hypertarget{command.also}{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
  1037
    \indexdef{}{command}{finally}\hypertarget{command.finally}{\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
  1038
    \indexdef{}{command}{moreover}\hypertarget{command.moreover}{\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
  1039
    \indexdef{}{command}{ultimately}\hypertarget{command.ultimately}{\hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
  1040
    \indexdef{}{command}{print\_trans\_rules}\hypertarget{command.print-trans-rules}{\hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28788
  1041
    \hyperlink{attribute.trans}{\mbox{\isa{trans}}} & : & \isa{attribute} \\
wenzelm@28788
  1042
    \hyperlink{attribute.sym}{\mbox{\isa{sym}}} & : & \isa{attribute} \\
wenzelm@28788
  1043
    \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} & : & \isa{attribute} \\
wenzelm@26870
  1044
  \end{matharray}
wenzelm@26870
  1045
wenzelm@26870
  1046
  Calculational proof is forward reasoning with implicit application
wenzelm@26870
  1047
  of transitivity rules (such those of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}},
wenzelm@26870
  1048
  \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}).  Isabelle/Isar maintains an auxiliary fact register
wenzelm@26902
  1049
  \indexref{}{fact}{calculation}\hyperlink{fact.calculation}{\mbox{\isa{calculation}}} for accumulating results obtained by
wenzelm@26902
  1050
  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
  1051
  \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} exhibits the final \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
wenzelm@26870
  1052
  forward chaining towards the next goal statement.  Both commands
wenzelm@26870
  1053
  require valid current facts, i.e.\ may occur only after commands
wenzelm@26902
  1054
  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
  1055
  commands are similar to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}},
wenzelm@26902
  1056
  but only collect further results in \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} without
wenzelm@26870
  1057
  applying any rules yet.
wenzelm@26870
  1058
wenzelm@26870
  1059
  Also note that the implicit term abbreviation ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' has
wenzelm@26870
  1060
  its canonical application with calculational proofs.  It refers to
wenzelm@26870
  1061
  the argument of the preceding statement. (The argument of a curried
wenzelm@26870
  1062
  infix expression happens to be its right-hand side.)
wenzelm@26870
  1063
wenzelm@26870
  1064
  Isabelle/Isar calculations are implicitly subject to block structure
wenzelm@26870
  1065
  in the sense that new threads of calculational reasoning are
wenzelm@26870
  1066
  commenced for any new block (as opened by a local goal, for
wenzelm@26870
  1067
  example).  This means that, apart from being able to nest
wenzelm@26870
  1068
  calculations, there is no separate \emph{begin-calculation} command
wenzelm@26870
  1069
  required.
wenzelm@26870
  1070
wenzelm@26870
  1071
  \medskip The Isar calculation proof commands may be defined as
wenzelm@26870
  1072
  follows:\footnote{We suppress internal bookkeeping such as proper
wenzelm@26870
  1073
  handling of block-structure.}
wenzelm@26870
  1074
wenzelm@26870
  1075
  \begin{matharray}{rcl}
wenzelm@26902
  1076
    \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
wenzelm@30548
  1077
    \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub n{\isacharplus}{\isadigit{1}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
wenzelm@26902
  1078
    \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@26902
  1079
    \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
wenzelm@26902
  1080
    \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
  1081
  \end{matharray}
wenzelm@26870
  1082
wenzelm@26870
  1083
  \begin{rail}
wenzelm@26870
  1084
    ('also' | 'finally') ('(' thmrefs ')')?
wenzelm@26870
  1085
    ;
wenzelm@26870
  1086
    'trans' (() | 'add' | 'del')
wenzelm@26870
  1087
    ;
wenzelm@26870
  1088
  \end{rail}
wenzelm@26870
  1089
wenzelm@28788
  1090
  \begin{description}
wenzelm@26870
  1091
wenzelm@28788
  1092
  \item \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}} maintains the auxiliary
wenzelm@28788
  1093
  \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} register as follows.  The first occurrence of
wenzelm@28788
  1094
  \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
  1095
  the same level of block-structure updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
wenzelm@28788
  1096
  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
  1097
  current context, unless alternative rules are given as explicit
wenzelm@28788
  1098
  arguments.
wenzelm@26870
  1099
wenzelm@28788
  1100
  \item \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\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
  1101
  current calculational thread.  The final result is exhibited as fact
wenzelm@28788
  1102
  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@28788
  1103
  calculational proofs are ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isacharquery}thesis}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' and ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isasymphi}}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}''.
wenzelm@26870
  1104
wenzelm@28788
  1105
  \item \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} are
wenzelm@26902
  1106
  analogous to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}, but collect
wenzelm@26870
  1107
  results only, without applying rules.
wenzelm@26870
  1108
wenzelm@28788
  1109
  \item \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}} prints the list of transitivity
wenzelm@28788
  1110
  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
  1111
  operation and single step elimination patters) of the current
wenzelm@28788
  1112
  context.
wenzelm@26870
  1113
wenzelm@28788
  1114
  \item \hyperlink{attribute.trans}{\mbox{\isa{trans}}} declares theorems as transitivity rules.
wenzelm@26870
  1115
wenzelm@28788
  1116
  \item \hyperlink{attribute.sym}{\mbox{\isa{sym}}} declares symmetry rules, as well as
wenzelm@26902
  1117
  \hyperlink{attribute.Pure.elim}{\mbox{\isa{Pure{\isachardot}elim}}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}} rules.
wenzelm@26870
  1118
wenzelm@28788
  1119
  \item \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} resolves a theorem with some rule
wenzelm@26902
  1120
  declared as \hyperlink{attribute.sym}{\mbox{\isa{sym}}} in the current context.  For example,
wenzelm@26902
  1121
  ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y{\isachardoublequote}}'' produces a
wenzelm@26870
  1122
  swapped fact derived from that assumption.
wenzelm@26870
  1123
wenzelm@26870
  1124
  In structured proof texts it is often more appropriate to use an
wenzelm@26902
  1125
  explicit single-step elimination proof, such as ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}y\ {\isacharequal}\ x{\isachardoublequote}}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''.
wenzelm@26870
  1126
wenzelm@28788
  1127
  \end{description}%
wenzelm@26870
  1128
\end{isamarkuptext}%
wenzelm@26870
  1129
\isamarkuptrue%
wenzelm@26870
  1130
%
wenzelm@27042
  1131
\isamarkupsection{Proof by cases and induction \label{sec:cases-induct}%
wenzelm@27042
  1132
}
wenzelm@27042
  1133
\isamarkuptrue%
wenzelm@27042
  1134
%
wenzelm@27042
  1135
\isamarkupsubsection{Rule contexts%
wenzelm@27042
  1136
}
wenzelm@27042
  1137
\isamarkuptrue%
wenzelm@27042
  1138
%
wenzelm@27042
  1139
\begin{isamarkuptext}%
wenzelm@27042
  1140
\begin{matharray}{rcl}
wenzelm@28788
  1141
    \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28788
  1142
    \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28788
  1143
    \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isa{attribute} \\
wenzelm@28788
  1144
    \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isa{attribute} \\
wenzelm@28788
  1145
    \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isa{attribute} \\
wenzelm@28788
  1146
    \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isa{attribute} \\
wenzelm@27042
  1147
  \end{matharray}
wenzelm@27042
  1148
wenzelm@27042
  1149
  The puristic way to build up Isar proof contexts is by explicit
wenzelm@27042
  1150
  language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},
wenzelm@27042
  1151
  \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}).  This is adequate
wenzelm@27042
  1152
  for plain natural deduction, but easily becomes unwieldy in concrete
wenzelm@27042
  1153
  verification tasks, which typically involve big induction rules with
wenzelm@27042
  1154
  several cases.
wenzelm@27042
  1155
wenzelm@27042
  1156
  The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a
wenzelm@27042
  1157
  local context symbolically: certain proof methods provide an
wenzelm@27042
  1158
  environment of named ``cases'' of the form \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\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{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.  Term bindings may be covered as well, notably
wenzelm@27042
  1159
  \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for the main conclusion.
wenzelm@27042
  1160
wenzelm@27042
  1161
  By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of
wenzelm@27042
  1162
  a case value is marked as hidden, i.e.\ there is no way to refer to
wenzelm@27042
  1163
  such parameters in the subsequent proof text.  After all, original
wenzelm@27042
  1164
  rule parameters stem from somewhere outside of the current proof
wenzelm@27042
  1165
  text.  By using the explicit form ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' instead, the proof author is able to
wenzelm@27042
  1166
  chose local names that fit nicely into the current context.
wenzelm@27042
  1167
wenzelm@27042
  1168
  \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
  1169
  which is not directly observable in Isar!  Nonetheless, goal
wenzelm@27042
  1170
  refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}}
wenzelm@27042
  1171
  for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state.
wenzelm@27042
  1172
  Using this extra feature requires great care, because some bits of
wenzelm@27042
  1173
  the internal tactical machinery intrude the proof text.  In
wenzelm@27042
  1174
  particular, parameter names stemming from the left-over of automated
wenzelm@27042
  1175
  reasoning tools are usually quite unpredictable.
wenzelm@27042
  1176
wenzelm@27042
  1177
  Under normal circumstances, the text of cases emerge from standard
wenzelm@27042
  1178
  elimination or induction rules, which in turn are derived from
wenzelm@27042
  1179
  previous theory specifications in a canonical way (say from
wenzelm@27042
  1180
  \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions).
wenzelm@27042
  1181
wenzelm@27042
  1182
  \medskip Proper cases are only available if both the proof method
wenzelm@27042
  1183
  and the rules involved support this.  By using appropriate
wenzelm@27042
  1184
  attributes, case names, conclusions, and parameters may be also
wenzelm@27042
  1185
  declared by hand.  Thus variant versions of rules that have been
wenzelm@27042
  1186
  derived manually become ready to use in advanced case analysis
wenzelm@27042
  1187
  later.
wenzelm@27042
  1188
wenzelm@27042
  1189
  \begin{rail}
wenzelm@27042
  1190
    'case' (caseref | '(' caseref ((name | underscore) +) ')')
wenzelm@27042
  1191
    ;
wenzelm@27042
  1192
    caseref: nameref attributes?
wenzelm@27042
  1193
    ;
wenzelm@27042
  1194
wenzelm@40255
  1195
    'case_names' (name +)
wenzelm@27042
  1196
    ;
wenzelm@40255
  1197
    'case_conclusion' name (name *)
wenzelm@27042
  1198
    ;
wenzelm@27042
  1199
    'params' ((name *) + 'and')
wenzelm@27042
  1200
    ;
wenzelm@27042
  1201
    'consumes' nat?
wenzelm@27042
  1202
    ;
wenzelm@27042
  1203
  \end{rail}
wenzelm@27042
  1204
wenzelm@28788
  1205
  \begin{description}
wenzelm@27042
  1206
  
wenzelm@28788
  1207
  \item \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}} invokes a named local
wenzelm@28788
  1208
  context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an
wenzelm@28788
  1209
  appropriate proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and
wenzelm@28788
  1210
  \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}).  The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.
wenzelm@27042
  1211
wenzelm@28788
  1212
  \item \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} prints all local contexts of the
wenzelm@27042
  1213
  current state, using Isar proof language notation.
wenzelm@27042
  1214
  
wenzelm@28788
  1215
  \item \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}} declares names for
wenzelm@28788
  1216
  the local contexts of premises of a theorem; \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}}
wenzelm@28788
  1217
  refers to the \emph{suffix} of the list of premises.
wenzelm@27042
  1218
  
wenzelm@28788
  1219
  \item \hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}} declares
wenzelm@28788
  1220
  names for the conclusions of a named premise \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the prefix of arguments of a logical formula
wenzelm@28788
  1221
  built by nesting a binary connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}).
wenzelm@27042
  1222
  
wenzelm@27042
  1223
  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
  1224
  whole.  The need to name subformulas only arises with cases that
wenzelm@27042
  1225
  split into several sub-cases, as in common co-induction rules.
wenzelm@27042
  1226
wenzelm@28788
  1227
  \item \hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}} renames
wenzelm@28788
  1228
  the innermost parameters of premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some
wenzelm@28788
  1229
  theorem.  An empty list of names may be given to skip positions,
wenzelm@28788
  1230
  leaving the present parameters unchanged.
wenzelm@27042
  1231
  
wenzelm@27042
  1232
  Note that the default usage of case rules does \emph{not} directly
wenzelm@27042
  1233
  expose parameters to the proof context.
wenzelm@27042
  1234
  
wenzelm@28788
  1235
  \item \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n} declares the number of ``major
wenzelm@28788
  1236
  premises'' of a rule, i.e.\ the number of facts to be consumed when
wenzelm@28788
  1237
  it is applied by an appropriate proof method.  The default value of
wenzelm@28788
  1238
  \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is appropriate for
wenzelm@28788
  1239
  the usual kind of cases and induction rules for inductive sets (cf.\
wenzelm@28788
  1240
  \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
  1241
  
wenzelm@27042
  1242
  Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only
wenzelm@27042
  1243
  rarely needed; this is already taken care of automatically by the
wenzelm@27042
  1244
  higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and
wenzelm@27042
  1245
  \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations.
wenzelm@27042
  1246
wenzelm@28788
  1247
  \end{description}%
wenzelm@27042
  1248
\end{isamarkuptext}%
wenzelm@27042
  1249
\isamarkuptrue%
wenzelm@27042
  1250
%
wenzelm@27042
  1251
\isamarkupsubsection{Proof methods%
wenzelm@27042
  1252
}
wenzelm@27042
  1253
\isamarkuptrue%
wenzelm@27042
  1254
%
wenzelm@27042
  1255
\begin{isamarkuptext}%
wenzelm@27042
  1256
\begin{matharray}{rcl}
wenzelm@28788
  1257
    \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
wenzelm@28788
  1258
    \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
wenzelm@28788
  1259
    \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
wenzelm@27042
  1260
  \end{matharray}
wenzelm@27042
  1261
wenzelm@27042
  1262
  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
wenzelm@27042
  1263
  methods provide a uniform interface to common proof techniques over
wenzelm@27042
  1264
  datatypes, inductive predicates (or sets), recursive functions etc.
wenzelm@27042
  1265
  The corresponding rules may be specified and instantiated in a
wenzelm@27042
  1266
  casual manner.  Furthermore, these methods provide named local
wenzelm@27042
  1267
  contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command
wenzelm@27042
  1268
  within the subsequent proof text.  This accommodates compact proof
wenzelm@27042
  1269
  texts even when reasoning about large specifications.
wenzelm@27042
  1270
wenzelm@27042
  1271
  The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional
wenzelm@27042
  1272
  infrastructure in order to be applicable to structure statements
wenzelm@27042
  1273
  (either using explicit meta-level connectives, or including facts
wenzelm@27042
  1274
  and parameters separately).  This avoids cumbersome encoding of
wenzelm@27042
  1275
  ``strengthened'' inductive statements within the object-logic.
wenzelm@27042
  1276
wenzelm@27042
  1277
  \begin{rail}
berghofe@37361
  1278
    'cases' '(no_simp)'? (insts * 'and') rule?
wenzelm@27042
  1279
    ;
berghofe@37361
  1280
    'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
wenzelm@27042
  1281
    ;
wenzelm@27042
  1282
    'coinduct' insts taking rule?
wenzelm@27042
  1283
    ;
wenzelm@27042
  1284
wenzelm@27042
  1285
    rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
wenzelm@27042
  1286
    ;
berghofe@37361
  1287
    definst: name ('==' | equiv) term | '(' term ')' | inst
wenzelm@27042
  1288
    ;
wenzelm@27042
  1289
    definsts: ( definst *)
wenzelm@27042
  1290
    ;
wenzelm@27042
  1291
    arbitrary: 'arbitrary' ':' ((term *) 'and' +)
wenzelm@27042
  1292
    ;
wenzelm@27042
  1293
    taking: 'taking' ':' insts
wenzelm@27042
  1294
    ;
wenzelm@27042
  1295
  \end{rail}
wenzelm@27042
  1296
wenzelm@28788
  1297
  \begin{description}
wenzelm@27042
  1298
wenzelm@28788
  1299
  \item \hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} applies method \hyperlink{method.rule}{\mbox{\isa{rule}}} with an appropriate case distinction theorem, instantiated to
wenzelm@27042
  1300
  the subjects \isa{insts}.  Symbolic case names are bound according
wenzelm@27042
  1301
  to the rule's local contexts.
wenzelm@27042
  1302
wenzelm@27042
  1303
  The rule is determined as follows, according to the facts and
wenzelm@27042
  1304
  arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method:
wenzelm@27042
  1305
wenzelm@27042
  1306
  \medskip
wenzelm@27042
  1307
  \begin{tabular}{llll}
wenzelm@27042
  1308
    facts           &                 & arguments   & rule \\\hline
wenzelm@27042
  1309
                    & \hyperlink{method.cases}{\mbox{\isa{cases}}} &             & classical case split \\
wenzelm@27042
  1310
                    & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t}   & datatype exhaustion (type of \isa{t}) \\
wenzelm@27042
  1311
    \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\
wenzelm@27042
  1312
    \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}     & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
wenzelm@27042
  1313
  \end{tabular}
wenzelm@27042
  1314
  \medskip
wenzelm@27042
  1315
wenzelm@27042
  1316
  Several instantiations may be given, referring to the \emph{suffix}
wenzelm@27042
  1317
  of premises of the case rule; within each premise, the \emph{prefix}
wenzelm@27042
  1318
  of variables is instantiated.  In most situations, only a single
wenzelm@27042
  1319
  term needs to be specified; this refers to the first variable of the
wenzelm@37364
  1320
  last premise (it is usually the same for all cases).  The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification of
wenzelm@37364
  1321
  cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
wenzelm@27042
  1322
wenzelm@28788
  1323
  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
wenzelm@27042
  1324
  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
wenzelm@27042
  1325
  determined as follows:
wenzelm@27042
  1326
wenzelm@27042
  1327
  \medskip
wenzelm@27042
  1328
  \begin{tabular}{llll}
wenzelm@27042
  1329
    facts           &                  & arguments            & rule \\\hline
wenzelm@27042
  1330
                    & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}}        & datatype induction (type of \isa{x}) \\
wenzelm@27042
  1331
    \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}          & predicate/set induction (of \isa{A}) \\
wenzelm@27042
  1332
    \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}     & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
wenzelm@27042
  1333
  \end{tabular}
wenzelm@27042
  1334
  \medskip
wenzelm@27042
  1335
  
wenzelm@27042
  1336
  Several instantiations may be given, each referring to some part of
wenzelm@27042
  1337
  a mutual inductive definition or datatype --- only related partial
wenzelm@27042
  1338
  induction rules may be used together, though.  Any of the lists of
wenzelm@27042
  1339
  terms \isa{{\isachardoublequote}P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} refers to the \emph{suffix} of variables
wenzelm@27042
  1340
  present in the induction rule.  This enables the writer to specify
wenzelm@27042
  1341
  only induction variables, or both predicates and variables, for
wenzelm@27042
  1342
  example.
wenzelm@37364
  1343
wenzelm@27042
  1344
  Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
wenzelm@27042
  1345
  introduce local definitions, which are inserted into the claim and
wenzelm@27042
  1346
  discharged after applying the induction rule.  Equalities reappear
wenzelm@27042
  1347
  in the inductive cases, but have been transformed according to the
wenzelm@27042
  1348
  induction principle being involved here.  In order to achieve
wenzelm@27042
  1349
  practically useful induction hypotheses, some variables occurring in
wenzelm@37364
  1350
  \isa{t} need to be fixed (see below).  Instantiations of the form
wenzelm@37364
  1351
  \isa{t}, where \isa{t} is not a variable, are taken as a
wenzelm@37364
  1352
  shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh
wenzelm@37364
  1353
  variable. If this is not intended, \isa{t} has to be enclosed in
wenzelm@37364
  1354
  parentheses.  By default, the equalities generated by definitional
wenzelm@37364
  1355
  instantiations are pre-simplified using a specific set of rules,
wenzelm@37364
  1356
  usually consisting of distinctness and injectivity theorems for
wenzelm@37364
  1357
  datatypes. This pre-simplification may cause some of the parameters
wenzelm@37364
  1358
  of an inductive case to disappear, or may even completely delete
wenzelm@37364
  1359
  some of the inductive cases, if one of the equalities occurring in
wenzelm@37364
  1360
  their premises can be simplified to \isa{False}.  The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification.
wenzelm@37364
  1361
  Additional rules to be used in pre-simplification can be declared
wenzelm@37364
  1362
  using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute.
wenzelm@37364
  1363
wenzelm@27042
  1364
  The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
wenzelm@27042
  1365
  specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction.  Thus
wenzelm@27042
  1366
  induction hypotheses may become sufficiently general to get the
wenzelm@27042
  1367
  proof through.  Together with definitional instantiations, one may
wenzelm@27042
  1368
  effectively perform induction over expressions of a certain
wenzelm@27042
  1369
  structure.
wenzelm@27042
  1370
  
wenzelm@27042
  1371
  The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
wenzelm@27042
  1372
  specification provides additional instantiations of a prefix of
wenzelm@27042
  1373
  pending variables in the rule.  Such schematic induction rules
wenzelm@27042
  1374
  rarely occur in practice, though.
wenzelm@27042
  1375
wenzelm@28788
  1376
  \item \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}} is analogous to the
wenzelm@27042
  1377
  \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are
wenzelm@27042
  1378
  determined as follows:
wenzelm@27042
  1379
wenzelm@27042
  1380
  \medskip
wenzelm@27042
  1381
  \begin{tabular}{llll}
wenzelm@27042
  1382
    goal          &                    & arguments & rule \\\hline
wenzelm@27042
  1383
                  & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\
wenzelm@27042
  1384
    \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\
wenzelm@27042
  1385
    \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}   & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
wenzelm@27042
  1386
  \end{tabular}
wenzelm@27042
  1387
  
wenzelm@27042
  1388
  Coinduction is the dual of induction.  Induction essentially
wenzelm@27042
  1389
  eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}},
wenzelm@27042
  1390
  while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, for a suitable ``bisimulation'' \isa{B}.  The cases of a
wenzelm@27042
  1391
  coinduct rule are typically named after the predicates or sets being
wenzelm@27042
  1392
  covered, while the conclusions consist of several alternatives being
wenzelm@27042
  1393
  named after the individual destructor patterns.
wenzelm@27042
  1394
  
wenzelm@27042
  1395
  The given instantiation refers to the \emph{suffix} of variables
wenzelm@27042
  1396
  occurring in the rule's major premise, or conclusion if unavailable.
wenzelm@27042
  1397
  An additional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
wenzelm@27042
  1398
  specification may be required in order to specify the bisimulation
wenzelm@27042
  1399
  to be used in the coinduction step.
wenzelm@27042
  1400
wenzelm@28788
  1401
  \end{description}
wenzelm@27042
  1402
wenzelm@27042
  1403
  Above methods produce named local contexts, as determined by the
wenzelm@27042
  1404
  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
  1405
  from the goal specification itself.  Any persisting unresolved
wenzelm@27042
  1406
  schematic variables of the resulting rule will render the the
wenzelm@27042
  1407
  corresponding case invalid.  The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for
wenzelm@27042
  1408
  the conclusion will be provided with each case, provided that term
wenzelm@27042
  1409
  is fully specified.
wenzelm@27042
  1410
wenzelm@27042
  1411
  The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present
wenzelm@27042
  1412
  in the current proof state.
wenzelm@27042
  1413
wenzelm@27042
  1414
  \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}
wenzelm@27042
  1415
  and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after
wenzelm@27042
  1416
  instantiation, while conforming due to the usual way of monotonic
wenzelm@27042
  1417
  natural deduction: the context of a structured statement \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}}
wenzelm@27042
  1418
  reappears unchanged after the case split.
wenzelm@27042
  1419
wenzelm@27042
  1420
  The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this
wenzelm@27042
  1421
  respect: the meta-level structure is passed through the
wenzelm@27042
  1422
  ``recursive'' course involved in the induction.  Thus the original
wenzelm@27042
  1423
  statement is basically replaced by separate copies, corresponding to
wenzelm@27042
  1424
  the induction hypotheses and conclusion; the original goal context
wenzelm@27042
  1425
  is no longer available.  Thus local assumptions, fixed parameters
wenzelm@27042
  1426
  and definitions effectively participate in the inductive rephrasing
wenzelm@27042
  1427
  of the original statement.
wenzelm@27042
  1428
wenzelm@27042
  1429
  In induction proofs, local assumptions introduced by cases are split
wenzelm@27042
  1430
  into two different kinds: \isa{hyps} stemming from the rule and
wenzelm@27042
  1431
  \isa{prems} from the goal statement.  This is reflected in the
wenzelm@27042
  1432
  extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems},
wenzelm@27042
  1433
  as well as fact \isa{c} to hold the all-inclusive list.
wenzelm@27042
  1434
wenzelm@27042
  1435
  \medskip Facts presented to either method are consumed according to
wenzelm@27042
  1436
  the number of ``major premises'' of the rule involved, which is
wenzelm@27042
  1437
  usually 0 for plain cases and induction rules of datatypes etc.\ and
wenzelm@27042
  1438
  1 for rules of inductive predicates or sets and the like.  The
wenzelm@27042
  1439
  remaining facts are inserted into the goal verbatim before the
wenzelm@27042
  1440
  actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
wenzelm@27042
  1441
  applied.%
wenzelm@27042
  1442
\end{isamarkuptext}%
wenzelm@27042
  1443
\isamarkuptrue%
wenzelm@27042
  1444
%
wenzelm@27042
  1445
\isamarkupsubsection{Declaring rules%
wenzelm@27042
  1446
}
wenzelm@27042
  1447
\isamarkuptrue%
wenzelm@27042
  1448
%
wenzelm@27042
  1449
\begin{isamarkuptext}%
wenzelm@27042
  1450
\begin{matharray}{rcl}
wenzelm@28788
  1451
    \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28788
  1452
    \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isa{attribute} \\
wenzelm@28788
  1453
    \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isa{attribute} \\
wenzelm@28788
  1454
    \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{attribute} \\
wenzelm@27042
  1455
  \end{matharray}
wenzelm@27042
  1456
wenzelm@27042
  1457
  \begin{rail}
wenzelm@27042
  1458
    'cases' spec
wenzelm@27042
  1459
    ;
wenzelm@27042
  1460
    'induct' spec
wenzelm@27042
  1461
    ;
wenzelm@27042
  1462
    'coinduct' spec
wenzelm@27042
  1463
    ;
wenzelm@27042
  1464
wenzelm@27142
  1465
    spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
wenzelm@27042
  1466
    ;
wenzelm@27042
  1467
  \end{rail}
wenzelm@27042
  1468
wenzelm@28788
  1469
  \begin{description}
wenzelm@27042
  1470
wenzelm@28788
  1471
  \item \hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}} prints cases and induct rules
wenzelm@28788
  1472
  for predicates (or sets) and types of the current context.
wenzelm@27042
  1473
  
wenzelm@28788
  1474
  \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
  1475
  (co)inductive predicates (or sets) and types, using the
wenzelm@27142
  1476
  corresponding methods of the same name.  Certain definitional
wenzelm@27142
  1477
  packages of object-logics usually declare emerging cases and
wenzelm@27142
  1478
  induction rules as expected, so users rarely need to intervene.
wenzelm@27142
  1479
wenzelm@27142
  1480
  Rules may be deleted via the \isa{{\isachardoublequote}del{\isachardoublequote}} specification, which
wenzelm@27142
  1481
  covers all of the \isa{{\isachardoublequote}type{\isachardoublequote}}/\isa{{\isachardoublequote}pred{\isachardoublequote}}/\isa{{\isachardoublequote}set{\isachardoublequote}}
wenzelm@27142
  1482
  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
  1483
  some type, predicate, or set.
wenzelm@27042
  1484
  
wenzelm@27042
  1485
  Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
wenzelm@27042
  1486
  cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}
wenzelm@27042
  1487
  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
  1488
wenzelm@28788
  1489
  \end{description}%
wenzelm@27042
  1490
\end{isamarkuptext}%
wenzelm@27042
  1491
\isamarkuptrue%
wenzelm@27042
  1492
%
wenzelm@26869
  1493
\isadelimtheory
wenzelm@26869
  1494
%
wenzelm@26869
  1495
\endisadelimtheory
wenzelm@26869
  1496
%
wenzelm@26869
  1497
\isatagtheory
wenzelm@26869
  1498
\isacommand{end}\isamarkupfalse%
wenzelm@26869
  1499
%
wenzelm@26869
  1500
\endisatagtheory
wenzelm@26869
  1501
{\isafoldtheory}%
wenzelm@26869
  1502
%
wenzelm@26869
  1503
\isadelimtheory
wenzelm@26869
  1504
%
wenzelm@26869
  1505
\endisadelimtheory
wenzelm@26869
  1506
\isanewline
wenzelm@26869
  1507
\end{isabellebody}%
wenzelm@26869
  1508
%%% Local Variables:
wenzelm@26869
  1509
%%% mode: latex
wenzelm@26869
  1510
%%% TeX-master: "root"
wenzelm@26869
  1511
%%% End: