more uniform treatment of options and attributes, preferring formal markup over old-style LaTeX macros;
3 \def\isabellecontext{Proof}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Main\isanewline
21 \isamarkupchapter{Proofs \label{ch:proofs}%
25 \begin{isamarkuptext}%
26 Proof commands perform transitions of Isar/VM machine
27 configurations, which are block-structured, consisting of a stack of
28 nodes with three main components: logical proof context, current
29 facts, and open goals. Isar/VM transitions are typed according to
30 the following three different modes of operation:
34 \item \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} means that a new goal has just been
35 stated that is now to be \emph{proven}; the next command may refine
36 it by some proof method, and enter a sub-proof to establish the
39 \item \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} is like a nested theory mode: the
40 context may be augmented by \emph{stating} additional assumptions,
41 intermediate results etc.
43 \item \isa{{\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.\
44 the contents of the special ``\indexref{}{fact}{this}\hyperlink{fact.this}{\mbox{\isa{this}}}'' register) have been
45 just picked up in order to be used when refining the goal claimed
50 The proof mode indicator may be understood as an instruction to the
51 writer, telling what kind of operation may be performed next. The
52 corresponding typings of proof commands restricts the shape of
53 well-formed proof texts to particular command sequences. So dynamic
54 arrangements of commands eventually turn out as static texts of a
57 \Appref{ap:refcard} gives a simplified grammar of the (extensible)
58 language emerging that way from the different types of proof
59 commands. The main ideas of the overall Isar framework are
60 explained in \chref{ch:isar-framework}.%
64 \isamarkupsection{Proof structure%
68 \isamarkupsubsection{Example proofs%
72 \begin{isamarkuptext}%
73 \begin{matharray}{rcl}
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}} \\
79 \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body. This
80 allows to experiment with Isar, without producing any persistent
83 Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
84 followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the
85 example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
86 discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
92 \isamarkupsubsection{Blocks%
96 \begin{isamarkuptext}%
97 \begin{matharray}{rcl}
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}} \\
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}} \\
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}} \\
103 While Isar is inherently block-structured, opening and closing
104 blocks is mostly handled rather casually, with little explicit
105 user-intervention. Any local goal statement automatically opens
106 \emph{two} internal blocks, which are closed again when concluding
107 the sub-proof (by \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} etc.). Sections of different
108 context within a sub-proof may be switched via \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}},
109 which is just a single block-close followed by block-open again.
110 The effect of \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} is to reset the local proof context;
111 there is no goal focus involved here!
113 For slightly more advanced applications, there are explicit block
114 parentheses as well. These typically achieve a stronger forward
119 \item \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} switches to a fresh block within a
120 sub-proof, resetting the local context to the initial one.
122 \item \hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}} and \hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}} explicitly open and close
123 blocks. Any current facts pass through ``\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}}''
124 unchanged, while ``\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}}'' causes any result to be
125 \emph{exported} into the enclosing context. Thus fixed variables
126 are generalized, assumptions discharged, and local definitions
127 unfolded (cf.\ \secref{sec:proof-context}). There is no difference
128 of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} and \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} in this mode of
129 forward reasoning --- in contrast to plain backward reasoning with
130 the result exported at \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} time.
136 \isamarkupsubsection{Omitting proofs%
140 \begin{isamarkuptext}%
141 \begin{matharray}{rcl}
142 \indexdef{}{command}{oops}\hypertarget{command.oops}{\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ local{\isacharunderscore}theory\ {\isacharbar}\ theory{\isachardoublequote}} \\
145 The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command discontinues the current proof
146 attempt, while considering the partial proof text as properly
147 processed. This is conceptually quite different from ``faking''
148 actual proofs via \indexref{}{command}{sorry}\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} (see
149 \secref{sec:proof-steps}): \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not observe the
150 proof structure at all, but goes back right to the theory level.
151 Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
152 --- there is no intended claim to be able to complete the proof
155 A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
156 \emph{within} the system itself, in conjunction with the document
157 preparation tools of Isabelle described in \chref{ch:document-prep}.
158 Thus partial or even wrong proof attempts can be discussed in a
159 logically sound manner. Note that the Isabelle {\LaTeX} macros can
160 be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of
161 the keyword ``\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}''.
163 \medskip The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command is undo-able, unlike
164 \indexref{}{command}{kill}\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} (see \secref{sec:history}). The effect is to
165 get back to the theory just before the opening of the proof.%
169 \isamarkupsection{Statements%
173 \isamarkupsubsection{Context elements \label{sec:proof-context}%
177 \begin{isamarkuptext}%
178 \begin{matharray}{rcl}
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}} \\
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}} \\
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}} \\
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}} \\
185 The logical proof context consists of fixed variables and
186 assumptions. The former closely correspond to Skolem constants, or
187 meta-level universal quantification as provided by the Isabelle/Pure
188 logical framework. Introducing some \emph{arbitrary, but fixed}
189 variable via ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}'' results in a local value
190 that may be used in the subsequent proof as any other variable or
191 constant. Furthermore, any result \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} exported from
192 the context will be universally closed wrt.\ \isa{x} at the
193 outermost level: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} (this is expressed in normal
194 form using Isabelle's meta-variables).
196 Similarly, introducing some assumption \isa{{\isasymchi}} has two effects.
197 On the one hand, a local theorem is created that may be used as a
198 fact in subsequent proof steps. On the other hand, any result
199 \isa{{\isachardoublequote}{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} exported from the context becomes conditional wrt.\
200 the assumption: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}{\isachardoublequote}}. Thus, solving an enclosing goal
201 using such a result would basically introduce a new subgoal stemming
202 from the assumption. How this situation is handled depends on the
203 version of assumption command used: while \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}
204 insists on solving the subgoal by unification with some premise of
205 the goal, \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves the subgoal unchanged in order
206 to be proved later by the user.
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
209 another version of assumption that causes any hypothetical equation
210 \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} to be eliminated by the reflexivity rule. Thus,
211 exporting some result \isa{{\isachardoublequote}x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} yields \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}{\isachardoublequote}}.
216 ('assume' | 'presume') (props + 'and')
220 def: thmdecl? \\ name ('==' | equiv) term termpat?
226 \item \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x} introduces a local variable \isa{x} that is \emph{arbitrary, but fixed.}
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
229 assumption. Subsequent results applied to an enclosing goal (e.g.\
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
231 goal, while \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves \isa{{\isasymphi}} as new subgoals.
233 Several lists of assumptions may be given (separated by
234 \indexref{}{keyword}{and}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}; the resulting list of current facts consists
235 of all of these concatenated.
237 \item \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} introduces a local
238 (non-polymorphic) definition. In results exported from the context,
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
240 hypothetical equation solved by reflexivity.
242 The default name for the definitional equation is \isa{x{\isacharunderscore}def}.
243 Several simultaneous definitions may be given at the same time.
247 The special name \indexref{}{fact}{prems}\hyperlink{fact.prems}{\mbox{\isa{prems}}} refers to all assumptions of the
248 current context as a list of theorems. This feature should be used
249 with great care! It is better avoided in final proof texts.%
253 \isamarkupsubsection{Term abbreviations \label{sec:term-abbrev}%
257 \begin{isamarkuptext}%
258 \begin{matharray}{rcl}
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}} \\
260 \indexdef{}{keyword}{is}\hypertarget{keyword.is}{\hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}}} & : & syntax \\
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
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
265 bind extra-logical term variables, which may be either named
266 schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
267 ``\hyperlink{variable.underscore}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
268 form the patterns occur on the left-hand side, while the \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns are in postfix position.
270 Polymorphism of term bindings is handled in Hindley-Milner style,
271 similar to ML. Type variables referring to local assumptions or
272 open goal statements are \emph{fixed}, while those of finished
273 results or bound by \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} may occur in \emph{arbitrary}
274 instances later. Even though actual polymorphism should be rarely
275 used in practice, this mechanism is essential to achieve proper
276 incremental type-inference, as the user proceeds to build up the
277 Isar proof text from left to right.
279 \medskip Term abbreviations are quite different from local
280 definitions as introduced via \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} (see
281 \secref{sec:proof-context}). The latter are visible within the
282 logic as actual equations, while abbreviations disappear during the
283 input process just after type checking. Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
286 'let' ((term + 'and') '=' term + 'and')
290 The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \railnonterm{termpat}
291 or \railnonterm{proppat} (see \secref{sec:term-decls}).
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
296 text variables in patterns \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} by simultaneous
297 higher-order matching against terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}}.
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
300 matches \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} against the preceding statement. Also
301 note that \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} is not a separate command, but part of
302 others (such as \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} etc.).
306 Some \emph{implicit} term abbreviations\index{term abbreviations}
307 for goals and facts are available as well. For any open goal,
308 \indexref{}{variable}{thesis}\hyperlink{variable.thesis}{\mbox{\isa{thesis}}} refers to its object-level statement,
309 abstracted over any meta-level parameters (if present). Likewise,
310 \indexref{}{variable}{this}\hyperlink{variable.this}{\mbox{\isa{this}}} is bound for fact statements resulting from
311 assumptions or finished goals. In case \hyperlink{variable.this}{\mbox{\isa{this}}} refers to
312 an object-logic statement that is an application \isa{{\isachardoublequote}f\ t{\isachardoublequote}}, then
313 \isa{t} is bound to the special text variable ``\hyperlink{variable.dots}{\mbox{\isa{{\isasymdots}}}}''
314 (three dots). The canonical application of this convenience are
315 calculational proofs (see \secref{sec:calculation}).%
319 \isamarkupsubsection{Facts and forward chaining%
323 \begin{isamarkuptext}%
324 \begin{matharray}{rcl}
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
333 New facts are established either by assumption or proof of local
334 statements. Any fact will usually be involved in further proofs,
335 either as explicit arguments of proof methods, or when forward
336 chaining towards the next goal via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} (and variants);
337 \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}} and \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}} are composite forms
338 involving \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}. The \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} elements
339 augments the collection of used facts \emph{after} a goal has been
340 stated. Note that the special theorem name \indexref{}{fact}{this}\hyperlink{fact.this}{\mbox{\isa{this}}} refers
341 to the most recently established facts, but only \emph{before}
342 issuing a follow-up claim.
345 'note' (thmdef? thmrefs + 'and')
347 ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
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
354 \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n{\isachardoublequote}}, binding the result as \isa{a}. Note that
355 attributes may be involved as well, both on the left and right hand
358 \item \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} indicates forward chaining by the current
359 facts in order to establish the goal to be claimed next. The
360 initial proof method invoked to refine that will be offered the
361 facts to do ``anything appropriate'' (see also
362 \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}
363 (see \secref{sec:pure-meth-att}) would typically do an elimination
364 rather than an introduction. Automatic methods usually insert the
365 facts into the goal state before operation. This provides a simple
366 scheme to control relevance of facts in automated proof search.
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
369 equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}''.
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
372 is from earlier facts together with the current ones.
374 \item \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} augments the facts being
375 currently indicated for use by a subsequent refinement step (such as
376 \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} or \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).
378 \item \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} is structurally
379 similar to \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}, but unfolds definitional equations
380 \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} throughout the goal state and facts.
384 Forward chaining with an empty list of theorems is the same as not
385 chaining at all. Thus ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{nothing}'' has no
386 effect apart from entering \isa{{\isachardoublequote}prove{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode, since
387 \indexref{}{fact}{nothing}\hyperlink{fact.nothing}{\mbox{\isa{nothing}}} is bound to the empty list of theorems.
389 Basic proof methods (such as \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}) expect multiple
390 facts to be given in their proper order, corresponding to a prefix
391 of the premises of the rule involved. Note that positions may be
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
393 \isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
394 ``\indexref{}{fact}{\_}\hyperlink{fact.underscore}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore).
396 Automated methods (such as \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.auto}{\mbox{\isa{auto}}}) just
397 insert any given facts before their usual operation. Depending on
398 the kind of procedure involved, the order of facts is less
403 \isamarkupsubsection{Goals \label{sec:goals}%
407 \begin{isamarkuptext}%
408 \begin{matharray}{rcl}
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
422 From a theory context, proof mode is entered by an initial goal
423 command such as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}, \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, or
424 \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}. Within a proof, new claims may be
425 introduced locally as well; four variants are available here to
426 indicate whether forward chaining of facts should be performed
427 initially (via \indexref{}{command}{then}\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}), and whether the final result
428 is meant to solve some pending goal.
430 Goals may consist of multiple statements, resulting in a list of
431 facts eventually. A pending multi-goal is internally represented as
432 a meta-level conjunction (\isa{{\isachardoublequote}{\isacharampersand}{\isacharampersand}{\isacharampersand}{\isachardoublequote}}), which is usually
433 split into the corresponding number of sub-goals prior to an initial
434 method application, via \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}
435 (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}
436 (\secref{sec:tactic-commands}). The \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}} method
437 covered in \secref{sec:cases-induct} acts on multiple claims
440 Claims at the theory level may be either in short or long form. A
441 short goal merely consists of several simultaneous propositions
442 (often just one). A long goal includes an explicit context
443 specification for the subsequent conclusion, involving local
444 parameters and assumptions. Here the role of each part of the
445 statement is explicitly marked by separate keywords (see also
446 \secref{sec:locale}); the local assumptions being introduced here
447 are available as \indexref{}{fact}{assms}\hyperlink{fact.assms}{\mbox{\isa{assms}}} in the proof. Moreover, there
448 are two kinds of conclusions: \indexdef{}{element}{shows}\hypertarget{element.shows}{\hyperlink{element.shows}{\mbox{\isa{\isakeyword{shows}}}}} states several
449 simultaneous propositions (essentially a big conjunction), while
450 \indexdef{}{element}{obtains}\hypertarget{element.obtains}{\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}}} claims several simultaneous simultaneous
451 contexts of (essentially a big disjunction of eliminated parameters
452 and assumptions, cf.\ \secref{sec:obtain}).
455 ('lemma' | 'theorem' | 'corollary' |
456 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
458 ('have' | 'show' | 'hence' | 'thus') goal
460 'print\_statement' modes? thmrefs
463 goal: (props + 'and')
465 longgoal: thmdecl? (contextelem *) conclusion
467 conclusion: 'shows' goal | 'obtains' (parname? case + '|')
469 case: (vars + 'and') 'where' (props + 'and')
475 \item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} enters proof mode with
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
477 \railnonterm{context} specification may build up an initial proof
478 context for the subsequent claim; this includes local definitions
479 and syntax as well, see the definition of \hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}} in
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
483 being of a different kind. This discrimination acts like a formal
486 \item \hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}lemma}}}}, \hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}theorem}}}},
487 \hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}corollary}}}} are similar to \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}},
488 \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}, respectively but allow
489 the statement to contain unbound schematic variables.
491 Under normal circumstances, an Isar proof text needs to specify
492 claims explicitly. Schematic goals are more like goals in Prolog,
493 where certain results are synthesized in the course of reasoning.
494 With schematic statements, the inherent compositionality of Isar
495 proofs is lost, which also impacts performance, because proof
496 checking is forced into sequential mode.
498 \item \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} claims a local goal,
499 eventually resulting in a fact within the current logical context.
500 This operation is completely independent of any pending sub-goals of
501 an enclosing goal statements, so \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} may be freely
502 used for experimental exploration of potential results within a
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
506 sub-goal for each one of the finished result, after having been
507 exported into the corresponding context (at the head of the
508 sub-proof of this \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} command).
510 To accommodate interactive debugging, resulting rules are printed
511 before being applied internally. Even more, interactive execution
512 of \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} predicts potential failure and displays the
513 resulting error as a warning beforehand. Watch out for the
516 %FIXME proper antiquitation
518 Problem! Local statement will fail to solve any pending goal
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
522 chaining the current facts. Note that \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} is also
523 equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}''.
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
526 ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''.
528 \item \hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}~\isa{a} prints facts from the
529 current theory or proof context in long statement form, according to
530 the syntax for \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} given above.
534 Any goal statement causes some term abbreviations (such as
535 \indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isacharquery}thesis}}}) to be bound automatically, see also
536 \secref{sec:term-abbrev}.
538 The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold
539 meaning: (1) during the of this claim they refer to the the local
540 context introductions, (2) the resulting rule is annotated
541 accordingly to support symbolic case splits when used with the
542 \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).%
546 \isamarkupsection{Refinement steps%
550 \isamarkupsubsection{Proof method expressions \label{sec:proof-meth}%
554 \begin{isamarkuptext}%
555 Proof methods are either basic ones, or expressions composed of
556 methods via ``\verb|,|'' (sequential composition),
557 ``\verb||\verb,|,\verb||'' (alternative choices), ``\verb|?|''
558 (try), ``\verb|+|'' (repeat at least once), ``\verb|[|\isa{n}\verb|]|'' (restriction to first \isa{n}
559 sub-goals, with default \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}). In practice, proof
560 methods are usually just a comma separated list of
561 \railqtok{nameref}~\railnonterm{args} specifications. Note that
562 parentheses may be dropped for single method specifications (with no
565 \indexouternonterm{method}
567 method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
569 methods: (nameref args | method) + (',' | '|')
573 Proper Isar proof methods do \emph{not} admit arbitrary goal
574 addressing, but refer either to the first sub-goal or all sub-goals
575 uniformly. The goal restriction operator ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharbrackright}{\isachardoublequote}}''
576 evaluates a method expression within a sandbox consisting of the
577 first \isa{n} sub-goals (which need to exist). For example, the
578 method ``\isa{{\isachardoublequote}simp{\isacharunderscore}all{\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isachardoublequote}}'' simplifies the first three
579 sub-goals, while ``\isa{{\isachardoublequote}{\isacharparenleft}rule\ foo{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}'' simplifies all
580 new goals that emerge from applying rule \isa{{\isachardoublequote}foo{\isachardoublequote}} to the
581 originally first one.
583 Improper methods, notably tactic emulations, offer a separate
584 low-level goal addressing scheme as explicit argument to the
585 individual tactic being involved. Here ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' refers to
586 all goals, and ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharminus}{\isacharbrackright}{\isachardoublequote}}'' to all goals starting from \isa{{\isachardoublequote}n{\isachardoublequote}}.
588 \indexouternonterm{goalspec}
590 goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
596 \isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}%
600 \begin{isamarkuptext}%
601 \begin{matharray}{rcl}
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
610 Arbitrary goal refinement via tactics is considered harmful.
611 Structured proof composition in Isar admits proof methods to be
612 invoked in two places only.
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
617 of sub-goals that are to be solved later. Facts are passed to
618 \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} for forward chaining, if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
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
621 passed to \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
625 The only other (proper) way to affect pending goals in a proof body
626 is by \indexref{}{command}{show}\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, which involves an explicit statement of
627 what is to be solved eventually. Thus we avoid the fundamental
628 problem of unstructured tactic scripts that consist of numerous
629 consecutive goal transformations, with invisible effects.
631 \medskip As a general rule of thumb for good proof style, initial
632 proof methods should either solve the goal completely, or constitute
633 some well-understood reduction to new sub-goals. Arbitrary
634 automatic proof tools that are prone leave a large number of badly
635 structured sub-goals are no help in continuing the proof document in
636 an intelligible manner.
638 Unless given explicitly by the user, the default initial method is
639 ``\indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}'', which applies a single standard elimination
640 or introduction rule according to the topmost symbol involved.
641 There is no separate default terminal method. Any remaining goals
642 are always solved by assumption in the very last step.
651 ('.' | '..' | 'sorry')
657 \item \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} refines the goal by proof
658 method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}; facts for forward chaining are passed if so
659 indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
661 \item \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} refines any remaining goals by
662 proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} and concludes the sub-proof by assumption.
663 If the goal had been \isa{{\isachardoublequote}show{\isachardoublequote}} (or \isa{{\isachardoublequote}thus{\isachardoublequote}}), some
664 pending sub-goal is solved as well by the rule resulting from the
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
666 resulting rule does not fit to any pending goal\footnote{This
667 includes any additional ``strong'' assumptions as introduced by
668 \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}.} of the enclosing context. Debugging such a
669 situation might involve temporarily changing \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} into
670 \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, or weakening the local context by replacing
671 occurrences of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} by \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}.
673 \item \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} is a \emph{terminal
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
675 backtracking across both methods. Debugging an unsuccessful
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
677 definition; in many cases \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} (or even
678 \isa{{\isachardoublequote}apply{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}) is already sufficient to see the
681 \item ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' is a \emph{default
682 proof}\index{proof!default}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}rule{\isachardoublequote}}.
684 \item ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' is a \emph{trivial
685 proof}\index{proof!trivial}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}this{\isachardoublequote}}.
687 \item \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is a \emph{fake proof}\index{proof!fake}
688 pretending to solve the pending claim without further ado. This
689 only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML). Facts emerging from fake
690 proofs are not the real thing. Internally, each theorem container
691 is tainted by an oracle invocation, which is indicated as ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' in the printed result.
693 The most important application of \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is to support
694 experimentation and top-down proof development.
700 \isamarkupsubsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
704 \begin{isamarkuptext}%
705 The following proof methods and attributes refer to basic logical
706 operations of Isar. Further methods and attributes are provided by
707 several generic and object-logic specific tools and packages (see
708 \chref{ch:gen-tools} and \chref{ch:hol}).
710 \begin{matharray}{rcl}
711 \indexdef{}{method}{-}\hypertarget{method.-}{\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}} & : & \isa{method} \\
712 \indexdef{}{method}{fact}\hypertarget{method.fact}{\hyperlink{method.fact}{\mbox{\isa{fact}}}} & : & \isa{method} \\
713 \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
714 \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
715 \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
716 \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
717 \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
718 \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
719 \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
720 \indexdef{}{attribute}{OF}\hypertarget{attribute.OF}{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}} & : & \isa{attribute} \\
721 \indexdef{}{attribute}{of}\hypertarget{attribute.of}{\hyperlink{attribute.of}{\mbox{\isa{of}}}} & : & \isa{attribute} \\
722 \indexdef{}{attribute}{where}\hypertarget{attribute.where}{\hyperlink{attribute.where}{\mbox{\isa{where}}}} & : & \isa{attribute} \\
730 rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
732 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
738 'of' insts ('concl' ':' insts)?
740 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
746 \item ``\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}'' (minus) does nothing but insert the forward
747 chaining facts as premises into the goal. Note that command
748 \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} without any method actually performs a single
749 reduction step using the \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}} method; thus a plain
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.
752 \item \hyperlink{method.fact}{\mbox{\isa{fact}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} composes some fact from
753 \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} (or implicitly from the current proof context)
754 modulo unification of schematic type and term variables. The rule
755 structure is not taken into account, i.e.\ meta-level implication is
756 considered atomic. This is the same principle underlying literal
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
758 \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} is an instance of some known \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} in the
761 \item \hyperlink{method.assumption}{\mbox{\isa{assumption}}} solves some goal by a single assumption
762 step. All given facts are guaranteed to participate in the
763 refinement; this means there may be only 0 or 1 in the first place.
764 Recall that \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} (\secref{sec:proof-steps}) already
765 concludes any remaining sub-goals by assumption, so structured
766 proofs usually need not quote the \hyperlink{method.assumption}{\mbox{\isa{assumption}}} method at
769 \item \hyperlink{method.this}{\mbox{\isa{this}}} applies all of the current facts directly as
770 rules. Recall that ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' (dot) abbreviates ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{this}''.
772 \item \hyperlink{method.rule}{\mbox{\isa{rule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some rule given as
773 argument in backward manner; facts are used to reduce the rule
774 before applying it to the goal. Thus \hyperlink{method.rule}{\mbox{\isa{rule}}} without facts
775 is plain introduction, while with facts it becomes elimination.
777 When no arguments are given, the \hyperlink{method.rule}{\mbox{\isa{rule}}} method tries to pick
778 appropriate rules automatically, as declared in the current context
779 using the \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}},
780 \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} attributes (see below). This is the
781 default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''
782 (double-dot) steps (see \secref{sec:proof-steps}).
784 \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
785 \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
786 destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
787 tools. Note that the latter will ignore rules declared with
788 ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most aggressively.
790 The classical reasoner (see \secref{sec:classical}) introduces its
791 own variants of these attributes; use qualified names to access the
792 present versions of Isabelle/Pure, i.e.\ \hyperlink{attribute.Pure.Pure.intro}{\mbox{\isa{Pure{\isachardot}intro}}}.
794 \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
795 elimination, or destruct rules.
797 \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some
798 theorem to all of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}
799 (in parallel). This corresponds to the \verb|op MRS| operation in
800 ML, but note the reversed order. Positions may be effectively
801 skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
803 \item \hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}} performs positional
804 instantiation of term variables. The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are
805 substituted for any schematic variables occurring in a theorem from
806 left to right; ``\isa{{\isacharunderscore}}'' (underscore) indicates to skip a
807 position. Arguments following a ``\isa{{\isachardoublequote}concl{\isacharcolon}{\isachardoublequote}}'' specification
808 refer to positions of the conclusion of a rule.
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}}
811 performs named instantiation of schematic type and term variables
812 occurring in a theorem. Schematic variables have to be specified on
813 the left-hand side (e.g.\ \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}{\isachardoublequote}}). The question mark may
814 be omitted if the variable name is a plain identifier without index.
815 As type instantiations are inferred from term instantiations,
816 explicit type instantiations are seldom necessary.
822 \isamarkupsubsection{Emulating tactic scripts \label{sec:tactic-commands}%
826 \begin{isamarkuptext}%
827 The Isar provides separate commands to accommodate tactic-style
828 proof scripts within the same system. While being outside the
829 orthodox Isar proof language, these might come in handy for
830 interactive exploration and debugging, or even actual tactical proof
831 within new-style theories (to benefit from document preparation, for
832 example). See also \secref{sec:tactics} for actual tactics, that
833 have been encapsulated as proof methods. Proper proof methods may
834 be used in scripts, too.
836 \begin{matharray}{rcl}
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
846 ( 'apply' | 'apply\_end' ) method
856 \item \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{m} applies proof method \isa{m} in
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
858 given just as in tactic scripts.
860 Facts are passed to \isa{m} as indicated by the goal's
861 forward-chain mode, and are \emph{consumed} afterwards. Thus any
862 further \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command would always work in a purely
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
866 multi-step tactic script for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, but may be given
867 anywhere within the proof body.
869 No facts are passed to \isa{m} here. Furthermore, the static
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
871 introduced in the current body, for example.
873 \item \hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} completes a proof script, provided that the
874 current goal state is solved completely. Note that actual
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.
877 \item \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}~\isa{n} and \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}~\isa{n}
878 shuffle the list of pending goals: \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}} puts off
879 sub-goal \isa{n} to the end of the list (\isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}} by
880 default), while \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}} brings sub-goal \isa{n} to the
883 \item \hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}} does back-tracking over the result sequence
884 of the latest proof command. Basically, any proof command may
885 return multiple results.
889 Any proper Isar proof method may be used with tactic script commands
890 such as \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}. A few additional emulations of actual
891 tactics are provided as well; these would be never used in actual
892 structured proofs, of course.%
896 \isamarkupsubsection{Defining proof methods%
900 \begin{isamarkuptext}%
901 \begin{matharray}{rcl}
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}} \\
906 'method\_setup' name '=' text text
912 \item \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
913 defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
914 \verb|(Proof.context -> Proof.method) context_parser|, cf.\
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
916 methods; the primed versions refer to tactics with explicit goal
919 Here are some example method definitions:
930 \isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
931 \ my{\isacharunderscore}method{\isadigit{1}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
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
933 \ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ first\ method\ {\isacharparenleft}without\ any\ arguments{\isacharparenright}{\isachardoublequoteclose}\isanewline
935 \ \ \ \ \isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
936 \ my{\isacharunderscore}method{\isadigit{2}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
937 \ \ \ \ \ \ Scan{\isachardot}succeed\ {\isacharparenleft}fn\ ctxt{\isacharcolon}\ Proof{\isachardot}context\ {\isacharequal}{\isachargreater}\isanewline
938 \ \ \ \ \ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}\isanewline
939 \ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ second\ method\ {\isacharparenleft}with\ context{\isacharparenright}{\isachardoublequoteclose}\isanewline
941 \ \ \ \ \isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
942 \ my{\isacharunderscore}method{\isadigit{3}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
943 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ thms{\isacharcolon}\ thm\ list\ {\isacharequal}{\isachargreater}\ fn\ ctxt{\isacharcolon}\ Proof{\isachardot}context\ {\isacharequal}{\isachargreater}\isanewline
944 \ \ \ \ \ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}\isanewline
945 \ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ third\ method\ {\isacharparenleft}with\ theorem\ arguments\ and\ context{\isacharparenright}{\isachardoublequoteclose}%
953 \isamarkupsection{Generalized elimination \label{sec:obtain}%
957 \begin{isamarkuptext}%
958 \begin{matharray}{rcl}
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}} \\
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}} \\
963 Generalized elimination means that additional elements with certain
964 properties may be introduced in the current context, by virtue of a
965 locally proven ``soundness statement''. Technically speaking, the
966 \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} language element is like a declaration of
967 \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} (see also see
968 \secref{sec:proof-context}), together with a soundness proof of its
969 additional claim. According to the nature of existential reasoning,
970 assumptions get eliminated from any result exported from the context
971 later, provided that the corresponding parameters do \emph{not}
972 occur in the conclusion.
975 'obtain' parname? (vars + 'and') 'where' (props + 'and')
977 'guess' (vars + 'and')
981 The derived Isar command \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} is defined as follows
982 (where \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k{\isachardoublequote}} shall refer to (optional)
983 facts indicated for forward chaining).
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]
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}} \\
987 \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\hyperlink{method.succeed}{\mbox{\isa{succeed}}} \\
988 \qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\
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}} \\
990 \qquad \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis} \\
991 \quad\qquad \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{{\isacharminus}} \\
992 \quad\qquad \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
993 \quad \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} \\
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}} \\
997 Typically, the soundness proof is relatively straight-forward, often
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
999 ``\isa{that}'' reduction above is declared as simplification and
1002 In a sense, \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} represents at the level of Isar
1003 proofs what would be meta-logical existential quantifiers and
1004 conjunctions. This concept has a broad range of useful
1005 applications, ranging from plain elimination (or introduction) of
1006 object-level existential and conjunctions, to elimination over
1007 results of symbolic evaluation of recursive definitions, for
1008 example. Also note that \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} without parameters acts
1009 much like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, where the result is treated as a
1012 An alternative name to be used instead of ``\isa{that}'' above may
1013 be given in parentheses.
1015 \medskip The improper variant \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} is similar to
1016 \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}, but derives the obtained statement from the
1017 course of reasoning! The proof starts with a fixed goal \isa{thesis}. The subsequent proof may refine this to anything of the
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
1019 final goal state is then used as reduction rule for the obtain
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
1021 proof context from being polluted by ad-hoc variables. The variable
1022 names and type constraints given as arguments for \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}
1023 specify a prefix of obtained parameters explicitly in the text.
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
1026 type-variables occurring here are fixed in the present context!%
1027 \end{isamarkuptext}%
1030 \isamarkupsection{Calculational reasoning \label{sec:calculation}%
1034 \begin{isamarkuptext}%
1035 \begin{matharray}{rcl}
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}} \\
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}} \\
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}} \\
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}} \\
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}} \\
1041 \hyperlink{attribute.trans}{\mbox{\isa{trans}}} & : & \isa{attribute} \\
1042 \hyperlink{attribute.sym}{\mbox{\isa{sym}}} & : & \isa{attribute} \\
1043 \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} & : & \isa{attribute} \\
1046 Calculational proof is forward reasoning with implicit application
1047 of transitivity rules (such those of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}},
1048 \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}). Isabelle/Isar maintains an auxiliary fact register
1049 \indexref{}{fact}{calculation}\hyperlink{fact.calculation}{\mbox{\isa{calculation}}} for accumulating results obtained by
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
1051 \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} exhibits the final \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
1052 forward chaining towards the next goal statement. Both commands
1053 require valid current facts, i.e.\ may occur only after commands
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}}}}
1055 commands are similar to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}},
1056 but only collect further results in \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} without
1057 applying any rules yet.
1059 Also note that the implicit term abbreviation ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' has
1060 its canonical application with calculational proofs. It refers to
1061 the argument of the preceding statement. (The argument of a curried
1062 infix expression happens to be its right-hand side.)
1064 Isabelle/Isar calculations are implicitly subject to block structure
1065 in the sense that new threads of calculational reasoning are
1066 commenced for any new block (as opened by a local goal, for
1067 example). This means that, apart from being able to nest
1068 calculations, there is no separate \emph{begin-calculation} command
1071 \medskip The Isar calculation proof commands may be defined as
1072 follows:\footnote{We suppress internal bookkeeping such as proper
1073 handling of block-structure.}
1075 \begin{matharray}{rcl}
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}} \\
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]
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]
1079 \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
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} \\
1084 ('also' | 'finally') ('(' thmrefs ')')?
1086 'trans' (() | 'add' | 'del')
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
1093 \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} register as follows. The first occurrence of
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
1095 the same level of block-structure updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
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
1097 current context, unless alternative rules are given as explicit
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
1101 current calculational thread. The final result is exhibited as fact
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
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}}}}}''.
1105 \item \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} are
1106 analogous to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}, but collect
1107 results only, without applying rules.
1109 \item \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}} prints the list of transitivity
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}}}
1111 operation and single step elimination patters) of the current
1114 \item \hyperlink{attribute.trans}{\mbox{\isa{trans}}} declares theorems as transitivity rules.
1116 \item \hyperlink{attribute.sym}{\mbox{\isa{sym}}} declares symmetry rules, as well as
1117 \hyperlink{attribute.Pure.elim}{\mbox{\isa{Pure{\isachardot}elim}}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}} rules.
1119 \item \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} resolves a theorem with some rule
1120 declared as \hyperlink{attribute.sym}{\mbox{\isa{sym}}} in the current context. For example,
1121 ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y{\isachardoublequote}}'' produces a
1122 swapped fact derived from that assumption.
1124 In structured proof texts it is often more appropriate to use an
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}}}}}''.
1128 \end{isamarkuptext}%
1131 \isamarkupsection{Proof by cases and induction \label{sec:cases-induct}%
1135 \isamarkupsubsection{Rule contexts%
1139 \begin{isamarkuptext}%
1140 \begin{matharray}{rcl}
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}} \\
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}} \\
1143 \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isa{attribute} \\
1144 \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isa{attribute} \\
1145 \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isa{attribute} \\
1146 \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isa{attribute} \\
1149 The puristic way to build up Isar proof contexts is by explicit
1150 language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},
1151 \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}). This is adequate
1152 for plain natural deduction, but easily becomes unwieldy in concrete
1153 verification tasks, which typically involve big induction rules with
1156 The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a
1157 local context symbolically: certain proof methods provide an
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
1159 \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for the main conclusion.
1161 By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of
1162 a case value is marked as hidden, i.e.\ there is no way to refer to
1163 such parameters in the subsequent proof text. After all, original
1164 rule parameters stem from somewhere outside of the current proof
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
1166 chose local names that fit nicely into the current context.
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,
1169 which is not directly observable in Isar! Nonetheless, goal
1170 refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}}
1171 for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state.
1172 Using this extra feature requires great care, because some bits of
1173 the internal tactical machinery intrude the proof text. In
1174 particular, parameter names stemming from the left-over of automated
1175 reasoning tools are usually quite unpredictable.
1177 Under normal circumstances, the text of cases emerge from standard
1178 elimination or induction rules, which in turn are derived from
1179 previous theory specifications in a canonical way (say from
1180 \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions).
1182 \medskip Proper cases are only available if both the proof method
1183 and the rules involved support this. By using appropriate
1184 attributes, case names, conclusions, and parameters may be also
1185 declared by hand. Thus variant versions of rules that have been
1186 derived manually become ready to use in advanced case analysis
1190 'case' (caseref | '(' caseref ((name | underscore) +) ')')
1192 caseref: nameref attributes?
1195 'case\_names' (name +)
1197 'case\_conclusion' name (name *)
1199 'params' ((name *) + 'and')
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
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
1209 appropriate proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and
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}}''.
1212 \item \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} prints all local contexts of the
1213 current state, using Isar proof language notation.
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
1216 the local contexts of premises of a theorem; \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}}
1217 refers to the \emph{suffix} of the list of premises.
1219 \item \hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}} declares
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
1221 built by nesting a binary connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}).
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
1224 whole. The need to name subformulas only arises with cases that
1225 split into several sub-cases, as in common co-induction rules.
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
1228 the innermost parameters of premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some
1229 theorem. An empty list of names may be given to skip positions,
1230 leaving the present parameters unchanged.
1232 Note that the default usage of case rules does \emph{not} directly
1233 expose parameters to the proof context.
1235 \item \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n} declares the number of ``major
1236 premises'' of a rule, i.e.\ the number of facts to be consumed when
1237 it is applied by an appropriate proof method. The default value of
1238 \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is appropriate for
1239 the usual kind of cases and induction rules for inductive sets (cf.\
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.
1242 Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only
1243 rarely needed; this is already taken care of automatically by the
1244 higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and
1245 \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations.
1248 \end{isamarkuptext}%
1251 \isamarkupsubsection{Proof methods%
1255 \begin{isamarkuptext}%
1256 \begin{matharray}{rcl}
1257 \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
1258 \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
1259 \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
1262 The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
1263 methods provide a uniform interface to common proof techniques over
1264 datatypes, inductive predicates (or sets), recursive functions etc.
1265 The corresponding rules may be specified and instantiated in a
1266 casual manner. Furthermore, these methods provide named local
1267 contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command
1268 within the subsequent proof text. This accommodates compact proof
1269 texts even when reasoning about large specifications.
1271 The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional
1272 infrastructure in order to be applicable to structure statements
1273 (either using explicit meta-level connectives, or including facts
1274 and parameters separately). This avoids cumbersome encoding of
1275 ``strengthened'' inductive statements within the object-logic.
1278 'cases' '(no_simp)'? (insts * 'and') rule?
1280 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
1282 'coinduct' insts taking rule?
1285 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
1287 definst: name ('==' | equiv) term | '(' term ')' | inst
1289 definsts: ( definst *)
1291 arbitrary: 'arbitrary' ':' ((term *) 'and' +)
1293 taking: 'taking' ':' insts
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
1300 the subjects \isa{insts}. Symbolic case names are bound according
1301 to the rule's local contexts.
1303 The rule is determined as follows, according to the facts and
1304 arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method:
1307 \begin{tabular}{llll}
1308 facts & & arguments & rule \\\hline
1309 & \hyperlink{method.cases}{\mbox{\isa{cases}}} & & classical case split \\
1310 & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\
1311 \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\
1312 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
1316 Several instantiations may be given, referring to the \emph{suffix}
1317 of premises of the case rule; within each premise, the \emph{prefix}
1318 of variables is instantiated. In most situations, only a single
1319 term needs to be specified; this refers to the first variable of the
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
1321 cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
1323 \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
1324 \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
1325 determined as follows:
1328 \begin{tabular}{llll}
1329 facts & & arguments & rule \\\hline
1330 & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}} & datatype induction (type of \isa{x}) \\
1331 \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set induction (of \isa{A}) \\
1332 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
1336 Several instantiations may be given, each referring to some part of
1337 a mutual inductive definition or datatype --- only related partial
1338 induction rules may be used together, though. Any of the lists of
1339 terms \isa{{\isachardoublequote}P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} refers to the \emph{suffix} of variables
1340 present in the induction rule. This enables the writer to specify
1341 only induction variables, or both predicates and variables, for
1344 Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
1345 introduce local definitions, which are inserted into the claim and
1346 discharged after applying the induction rule. Equalities reappear
1347 in the inductive cases, but have been transformed according to the
1348 induction principle being involved here. In order to achieve
1349 practically useful induction hypotheses, some variables occurring in
1350 \isa{t} need to be fixed (see below). Instantiations of the form
1351 \isa{t}, where \isa{t} is not a variable, are taken as a
1352 shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh
1353 variable. If this is not intended, \isa{t} has to be enclosed in
1354 parentheses. By default, the equalities generated by definitional
1355 instantiations are pre-simplified using a specific set of rules,
1356 usually consisting of distinctness and injectivity theorems for
1357 datatypes. This pre-simplification may cause some of the parameters
1358 of an inductive case to disappear, or may even completely delete
1359 some of the inductive cases, if one of the equalities occurring in
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.
1361 Additional rules to be used in pre-simplification can be declared
1362 using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute.
1364 The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
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
1366 induction hypotheses may become sufficiently general to get the
1367 proof through. Together with definitional instantiations, one may
1368 effectively perform induction over expressions of a certain
1371 The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
1372 specification provides additional instantiations of a prefix of
1373 pending variables in the rule. Such schematic induction rules
1374 rarely occur in practice, though.
1376 \item \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}} is analogous to the
1377 \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are
1378 determined as follows:
1381 \begin{tabular}{llll}
1382 goal & & arguments & rule \\\hline
1383 & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\
1384 \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\
1385 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
1388 Coinduction is the dual of induction. Induction essentially
1389 eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}},
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
1391 coinduct rule are typically named after the predicates or sets being
1392 covered, while the conclusions consist of several alternatives being
1393 named after the individual destructor patterns.
1395 The given instantiation refers to the \emph{suffix} of variables
1396 occurring in the rule's major premise, or conclusion if unavailable.
1397 An additional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
1398 specification may be required in order to specify the bisimulation
1399 to be used in the coinduction step.
1403 Above methods produce named local contexts, as determined by the
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
1405 from the goal specification itself. Any persisting unresolved
1406 schematic variables of the resulting rule will render the the
1407 corresponding case invalid. The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for
1408 the conclusion will be provided with each case, provided that term
1411 The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present
1412 in the current proof state.
1414 \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}
1415 and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after
1416 instantiation, while conforming due to the usual way of monotonic
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}}
1418 reappears unchanged after the case split.
1420 The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this
1421 respect: the meta-level structure is passed through the
1422 ``recursive'' course involved in the induction. Thus the original
1423 statement is basically replaced by separate copies, corresponding to
1424 the induction hypotheses and conclusion; the original goal context
1425 is no longer available. Thus local assumptions, fixed parameters
1426 and definitions effectively participate in the inductive rephrasing
1427 of the original statement.
1429 In induction proofs, local assumptions introduced by cases are split
1430 into two different kinds: \isa{hyps} stemming from the rule and
1431 \isa{prems} from the goal statement. This is reflected in the
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},
1433 as well as fact \isa{c} to hold the all-inclusive list.
1435 \medskip Facts presented to either method are consumed according to
1436 the number of ``major premises'' of the rule involved, which is
1437 usually 0 for plain cases and induction rules of datatypes etc.\ and
1438 1 for rules of inductive predicates or sets and the like. The
1439 remaining facts are inserted into the goal verbatim before the
1440 actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
1442 \end{isamarkuptext}%
1445 \isamarkupsubsection{Declaring rules%
1449 \begin{isamarkuptext}%
1450 \begin{matharray}{rcl}
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}} \\
1452 \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isa{attribute} \\
1453 \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isa{attribute} \\
1454 \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{attribute} \\
1465 spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
1471 \item \hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}} prints cases and induct rules
1472 for predicates (or sets) and types of the current context.
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
1475 (co)inductive predicates (or sets) and types, using the
1476 corresponding methods of the same name. Certain definitional
1477 packages of object-logics usually declare emerging cases and
1478 induction rules as expected, so users rarely need to intervene.
1480 Rules may be deleted via the \isa{{\isachardoublequote}del{\isachardoublequote}} specification, which
1481 covers all of the \isa{{\isachardoublequote}type{\isachardoublequote}}/\isa{{\isachardoublequote}pred{\isachardoublequote}}/\isa{{\isachardoublequote}set{\isachardoublequote}}
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
1483 some type, predicate, or set.
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
1486 cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}
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.
1490 \end{isamarkuptext}%
1498 \isacommand{end}\isamarkupfalse%
1508 %%% Local Variables:
1510 %%% TeX-master: "root"