3 \def\isabellecontext{Generic}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Base\ Main\isanewline
21 \isamarkupchapter{Generic tools and packages \label{ch:gen-tools}%
25 \isamarkupsection{Configuration options \label{sec:config}%
29 \begin{isamarkuptext}%
30 Isabelle/Pure maintains a record of named configuration
31 options within the theory or proof context, with values of type
32 \verb|bool|, \verb|int|, \verb|real|, or \verb|string|. Tools may declare options in ML, and then refer to these
33 values (relative to the context). Thus global reference variables
34 are easily avoided. The user may change the value of a
35 configuration option by means of an associated attribute of the same
36 name. This form of context declaration works particularly well with
37 commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} like
41 \isacommand{declare}\isamarkupfalse%
42 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
44 \isacommand{notepad}\isamarkupfalse%
46 \isakeyword{begin}\isanewline
53 \isacommand{note}\isamarkupfalse%
54 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%
62 \isacommand{end}\isamarkupfalse%
64 \begin{isamarkuptext}%
65 For historical reasons, some tools cannot take the full proof
66 context into account and merely refer to the background theory.
67 This is accommodated by configuration options being declared as
68 ``global'', which may not be changed within a local context.
70 \begin{matharray}{rcll}
71 \indexdef{}{command}{print\_configs}\hypertarget{command.print-configs}{\hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}configs}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
76 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
79 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
81 \rail@term{\isa{true}}[]
83 \rail@term{\isa{false}}[]
85 \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
87 \rail@nont{\hyperlink{syntax.float}{\mbox{\isa{float}}}}[]
89 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
98 \item \hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}configs}}}} prints the available configuration
99 options, with names, types, and current values.
101 \item \isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ value{\isaliteral{22}{\isachardoublequote}}} as an attribute expression modifies the
102 named option, with the syntax of the value depending on the option's
103 type. For \verb|bool| the default value is \isa{true}. Any
104 attempt to change a global option in a local context is ignored.
110 \isamarkupsection{Basic proof tools%
114 \isamarkupsubsection{Miscellaneous methods and attributes \label{sec:misc-meth-att}%
118 \begin{isamarkuptext}%
119 \begin{matharray}{rcl}
120 \indexdef{}{method}{unfold}\hypertarget{method.unfold}{\hyperlink{method.unfold}{\mbox{\isa{unfold}}}} & : & \isa{method} \\
121 \indexdef{}{method}{fold}\hypertarget{method.fold}{\hyperlink{method.fold}{\mbox{\isa{fold}}}} & : & \isa{method} \\
122 \indexdef{}{method}{insert}\hypertarget{method.insert}{\hyperlink{method.insert}{\mbox{\isa{insert}}}} & : & \isa{method} \\[0.5ex]
123 \indexdef{}{method}{erule}\hypertarget{method.erule}{\hyperlink{method.erule}{\mbox{\isa{erule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
124 \indexdef{}{method}{drule}\hypertarget{method.drule}{\hyperlink{method.drule}{\mbox{\isa{drule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
125 \indexdef{}{method}{frule}\hypertarget{method.frule}{\hyperlink{method.frule}{\mbox{\isa{frule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
126 \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
127 \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
128 \indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
129 \indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
135 \rail@term{\hyperlink{method.fold}{\mbox{\isa{fold}}}}[]
137 \rail@term{\hyperlink{method.unfold}{\mbox{\isa{unfold}}}}[]
139 \rail@term{\hyperlink{method.insert}{\mbox{\isa{insert}}}}[]
141 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
145 \rail@term{\hyperlink{method.erule}{\mbox{\isa{erule}}}}[]
147 \rail@term{\hyperlink{method.drule}{\mbox{\isa{drule}}}}[]
149 \rail@term{\hyperlink{method.frule}{\mbox{\isa{frule}}}}[]
153 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
154 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
155 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
157 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
161 \rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
163 \rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
167 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
175 \item \hyperlink{method.unfold}{\mbox{\isa{unfold}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{method.fold}{\mbox{\isa{fold}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} expand (or fold back) the given definitions throughout
176 all goals; any chained facts provided are inserted into the goal and
177 subject to rewriting as well.
179 \item \hyperlink{method.insert}{\mbox{\isa{insert}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} inserts theorems as facts
180 into all goals of the proof state. Note that current facts
181 indicated for forward chaining are ignored.
183 \item \hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are similar to the basic \hyperlink{method.rule}{\mbox{\isa{rule}}}
184 method (see \secref{sec:pure-meth-att}), but apply rules by
185 elim-resolution, destruct-resolution, and forward-resolution,
186 respectively \cite{isabelle-implementation}. The optional natural
187 number argument (default 0) specifies additional assumption steps to
190 Note that these methods are improper ones, mainly serving for
191 experimentation and tactic script emulation. Different modes of
192 basic rule application are usually expressed in Isar at the proof
193 language level, rather than via implicit proof state manipulations.
194 For example, a proper single-step elimination would be done using
195 the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
198 \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
199 by intro- or elim-resolution, after having inserted any chained
200 facts. Exactly the rules given as arguments are taken into account;
201 this allows fine-tuned decomposition of a proof problem, in contrast
202 to common automated tools.
204 \item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
205 the identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
206 \secref{sec:proof-meth}).
208 \item \hyperlink{method.fail}{\mbox{\isa{fail}}} yields an empty result sequence; it is the
209 identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
210 \secref{sec:proof-meth}).
214 \begin{matharray}{rcl}
215 \indexdef{}{attribute}{tagged}\hypertarget{attribute.tagged}{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}} & : & \isa{attribute} \\
216 \indexdef{}{attribute}{untagged}\hypertarget{attribute.untagged}{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}} & : & \isa{attribute} \\[0.5ex]
217 \indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isa{attribute} \\
218 \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isa{attribute} \\[0.5ex]
219 \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isa{attribute} \\
220 \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\[0.5ex]
221 \indexdef{}{attribute}{rotated}\hypertarget{attribute.rotated}{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}} & : & \isa{attribute} \\
222 \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim-format}{\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}format}}}} & : & \isa{attribute} \\
223 \indexdef{}{attribute}{standard}\hypertarget{attribute.standard}{\hyperlink{attribute.standard}{\mbox{\isa{standard}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\
224 \indexdef{}{attribute}{no\_vars}\hypertarget{attribute.no-vars}{\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isaliteral{5F}{\isacharunderscore}}vars}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\
229 \rail@term{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}}[]
230 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
231 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
234 \rail@term{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}}[]
235 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
239 \rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[]
241 \rail@term{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}}[]
245 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
246 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
247 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
249 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
253 \rail@term{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}}[]
255 \rail@term{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}}[]
257 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
260 \rail@term{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}}[]
263 \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
271 \item \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ value{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}~\isa{name} add and remove \emph{tags} of some theorem.
272 Tags may be any list of string pairs that serve as formal comment.
273 The first string is considered the tag name, the second its value.
274 Note that \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} removes any tags of the same name.
276 \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} and \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}~\isa{a}
277 compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
278 first premise of \isa{a} (an alternative position may be also
279 specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
280 lifting process that is normally intended (cf.\ \verb|op RS| and
281 \verb|op COMP| in \cite{isabelle-implementation}).
283 \item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} expand and fold back again the given
284 definitions throughout a rule.
286 \item \hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n} rotate the premises of a
287 theorem by \isa{n} (default 1).
289 \item \hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}format}}} turns a destruction rule into
290 elimination rule format, by resolving with the rule \isa{{\isaliteral{22}{\isachardoublequote}}PROP\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}PROP\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ PROP\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ PROP\ B{\isaliteral{22}{\isachardoublequote}}}.
292 Note that the Classical Reasoner (\secref{sec:classical}) provides
293 its own version of this operation.
295 \item \hyperlink{attribute.standard}{\mbox{\isa{standard}}} puts a theorem into the standard form of
296 object-rules at the outermost theory level. Note that this
297 operation violates the local proof context (including active
300 \item \hyperlink{attribute.no-vars}{\mbox{\isa{no{\isaliteral{5F}{\isacharunderscore}}vars}}} replaces schematic variables by free
301 ones; this is mainly for tuning output of pretty printed theorems.
307 \isamarkupsubsection{Low-level equational reasoning%
311 \begin{isamarkuptext}%
312 \begin{matharray}{rcl}
313 \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}} & : & \isa{method} \\
314 \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}} & : & \isa{method} \\
315 \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}} & : & \isa{method} \\
320 \rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[]
323 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
324 \rail@term{\isa{asm}}[]
325 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
330 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
332 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
335 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
337 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
340 \rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
341 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
346 These methods provide low-level facilities for equational reasoning
347 that are intended for specialized applications only. Normally,
348 single step calculations would be performed in a structured text
349 (see also \secref{sec:calculation}), while the Simplifier methods
350 provide the canonical way for automated normalization (see
351 \secref{sec:simplifier}).
355 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq} performs a single substitution step
356 using rule \isa{eq}, which may be either a meta or object
359 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}\ eq{\isaliteral{22}{\isachardoublequote}}} substitutes in an
362 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ j{\isaliteral{29}{\isacharparenright}}\ eq{\isaliteral{22}{\isachardoublequote}}} performs several
363 substitutions in the conclusion. The numbers \isa{i} to \isa{j}
364 indicate the positions to substitute at. Positions are ordered from
365 the top of the term tree moving down from left to right. For
366 example, in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} there are three positions
367 where commutativity of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} is applicable: 1 refers to \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{22}{\isachardoublequote}}}, 2 to the whole term, and 3 to \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{22}{\isachardoublequote}}}.
369 If the positions in the list \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} are non-overlapping
370 (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}) you may
371 assume all substitutions are performed simultaneously. Otherwise
372 the behaviour of \isa{subst} is not specified.
374 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ j{\isaliteral{29}{\isacharparenright}}\ eq{\isaliteral{22}{\isachardoublequote}}} performs the
375 substitutions in the assumptions. The positions refer to the
376 assumptions in order from left to right. For example, given in a
377 goal of the form \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}, position 1 of
378 commutativity of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} is the subterm \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{22}{\isachardoublequote}}} and
379 position 2 is the subterm \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{22}{\isachardoublequote}}}.
381 \item \hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}} performs substitution using some
382 assumption; this only works for equations of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} where \isa{x} is a free or bound variable.
384 \item \hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} performs single-step case
385 splitting using the given rules. Splitting is performed in the
386 conclusion or some assumption of the subgoal, depending of the
387 structure of the rule.
389 Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
390 application of split rules as declared in the current context, using
391 \hyperlink{attribute.split}{\mbox{\isa{split}}}, for example.
397 \isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
401 \begin{isamarkuptext}%
402 The following improper proof methods emulate traditional tactics.
403 These admit direct access to the goal state, which is normally
404 considered harmful! In particular, this may involve both numbered
405 goal addressing (default 1), and dynamic instantiation within the
406 scope of some subgoal.
409 Dynamic instantiations refer to universally quantified parameters
410 of a subgoal (the dynamic context) rather than fixed variables and
411 term abbreviations of a (static) Isar context.
414 Tactic emulation methods, unlike their ML counterparts, admit
415 simultaneous instantiation from both dynamic and static contexts.
416 If names occur in both contexts goal parameters hide locally fixed
417 variables. Likewise, schematic variables refer to term
418 abbreviations, if present in the static context. Otherwise the
419 schematic variable is interpreted as a schematic variable and left
420 to be solved by unification with certain parts of the subgoal.
422 Note that the tactic emulation proof methods in Isabelle/Isar are
423 consistently named \isa{foo{\isaliteral{5F}{\isacharunderscore}}tac}. Note also that variable names
424 occurring on left hand sides of instantiations must be preceded by a
425 question mark if they coincide with a keyword or contain dots. This
426 is consistent with the attribute \hyperlink{attribute.where}{\mbox{\isa{where}}} (see
427 \secref{sec:pure-meth-att}).
429 \begin{matharray}{rcl}
430 \indexdef{}{method}{rule\_tac}\hypertarget{method.rule-tac}{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
431 \indexdef{}{method}{erule\_tac}\hypertarget{method.erule-tac}{\hyperlink{method.erule-tac}{\mbox{\isa{erule{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
432 \indexdef{}{method}{drule\_tac}\hypertarget{method.drule-tac}{\hyperlink{method.drule-tac}{\mbox{\isa{drule{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
433 \indexdef{}{method}{frule\_tac}\hypertarget{method.frule-tac}{\hyperlink{method.frule-tac}{\mbox{\isa{frule{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
434 \indexdef{}{method}{cut\_tac}\hypertarget{method.cut-tac}{\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
435 \indexdef{}{method}{thin\_tac}\hypertarget{method.thin-tac}{\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
436 \indexdef{}{method}{subgoal\_tac}\hypertarget{method.subgoal-tac}{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
437 \indexdef{}{method}{rename\_tac}\hypertarget{method.rename-tac}{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
438 \indexdef{}{method}{rotate\_tac}\hypertarget{method.rotate-tac}{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
439 \indexdef{}{method}{tactic}\hypertarget{method.tactic}{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
440 \indexdef{}{method}{raw\_tactic}\hypertarget{method.raw-tactic}{\hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isaliteral{5F}{\isacharunderscore}}tactic}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
446 \rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
448 \rail@term{\hyperlink{method.erule-tac}{\mbox{\isa{erule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
450 \rail@term{\hyperlink{method.drule-tac}{\mbox{\isa{drule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
452 \rail@term{\hyperlink{method.frule-tac}{\mbox{\isa{frule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
454 \rail@term{\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
456 \rail@term{\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
460 \rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
464 \rail@nont{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}[]
465 \rail@term{\isa{\isakeyword{in}}}[]
466 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
468 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
472 \rail@term{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
475 \rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
478 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
483 \rail@term{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
486 \rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
489 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
494 \rail@term{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
497 \rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
501 \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
506 \rail@term{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}[]
508 \rail@term{\hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isaliteral{5F}{\isacharunderscore}}tactic}}}}[]
510 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
512 \rail@begin{2}{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}
514 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
515 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
516 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
518 \rail@cterm{\isa{\isakeyword{and}}}[]
526 \item \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} etc. do resolution of rules with explicit
527 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite{isabelle-implementation})
529 Multiple rules may be only given if there is no instantiation; then
530 \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} is the same as \verb|resolve_tac| in ML (see
531 \cite{isabelle-implementation}).
533 \item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isaliteral{5F}{\isacharunderscore}}tac}}} inserts facts into the proof state as
534 assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
535 \cite{isabelle-implementation}. Note that the scope of schematic
536 variables is spread over the main goal statement. Instantiations
537 may be given as well, see also ML tactic \verb|cut_inst_tac| in
538 \cite{isabelle-implementation}.
540 \item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} deletes the specified assumption
541 from a subgoal; note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain schematic variables.
542 See also \verb|thin_tac| in \cite{isabelle-implementation}.
544 \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} adds \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as an
545 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
547 \item \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} renames parameters of a
548 goal according to the list \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, which refers to the
549 \emph{suffix} of variables.
551 \item \hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{n} rotates the assumptions of a
552 goal by \isa{n} positions: from right to left if \isa{n} is
553 positive, and from left to right if \isa{n} is negative; the
554 default value is 1. See also \verb|rotate_tac| in
555 \cite{isabelle-implementation}.
557 \item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} produces a proof method from
558 any ML text of type \verb|tactic|. Apart from the usual ML
559 environment and the current proof context, the ML code may refer to
560 the locally bound values \verb|facts|, which indicates any
561 current facts used for forward-chaining.
563 \item \hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isaliteral{5F}{\isacharunderscore}}tactic}}} is similar to \hyperlink{method.tactic}{\mbox{\isa{tactic}}}, but
564 presents the goal state in its raw internal form, where simultaneous
565 subgoals appear as conjunction of the logical framework instead of
566 the usual split into several subgoals. While feature this is useful
567 for debugging of complex method definitions, it should not never
568 appear in production theories.
574 \isamarkupsection{The Simplifier \label{sec:simplifier}%
578 \isamarkupsubsection{Simplification methods%
582 \begin{isamarkuptext}%
583 \begin{matharray}{rcl}
584 \indexdef{}{method}{simp}\hypertarget{method.simp}{\hyperlink{method.simp}{\mbox{\isa{simp}}}} & : & \isa{method} \\
585 \indexdef{}{method}{simp\_all}\hypertarget{method.simp-all}{\hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}}} & : & \isa{method} \\
591 \rail@term{\hyperlink{method.simp}{\mbox{\isa{simp}}}}[]
593 \rail@term{\hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}}}[]
597 \rail@nont{\isa{opt}}[]
601 \rail@cnont{\hyperlink{syntax.simpmod}{\mbox{\isa{simpmod}}}}[]
604 \rail@begin{4}{\isa{opt}}
605 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
607 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm}}[]
609 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp}}[]
611 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use}}[]
613 \rail@term{\isa{asm{\isaliteral{5F}{\isacharunderscore}}lr}}[]
615 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
617 \rail@begin{9}{\indexdef{}{syntax}{simpmod}\hypertarget{syntax.simpmod}{\hyperlink{syntax.simpmod}{\mbox{\isa{simpmod}}}}}
619 \rail@term{\isa{add}}[]
621 \rail@term{\isa{del}}[]
623 \rail@term{\isa{only}}[]
625 \rail@term{\isa{cong}}[]
628 \rail@term{\isa{add}}[]
630 \rail@term{\isa{del}}[]
633 \rail@term{\isa{split}}[]
636 \rail@term{\isa{add}}[]
638 \rail@term{\isa{del}}[]
641 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
642 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
649 \item \hyperlink{method.simp}{\mbox{\isa{simp}}} invokes the Simplifier, after declaring
650 additional rules according to the arguments given. Note that the
651 \isa{only} modifier first removes all other rewrite rules,
652 congruences, and looper tactics (including splits), and then behaves
655 \medskip The \isa{cong} modifiers add or delete Simplifier
656 congruence rules (see also \cite{isabelle-ref}), the default is to
659 \medskip The \isa{split} modifiers add or delete rules for the
660 Splitter (see also \cite{isabelle-ref}), the default is to add.
661 This works only if the Simplifier method has been properly setup to
662 include the Splitter (all major object logics such HOL, HOLCF, FOL,
665 \item \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} is similar to \hyperlink{method.simp}{\mbox{\isa{simp}}}, but acts on
666 all goals (backwards from the last to the first one).
670 By default the Simplifier methods take local assumptions fully into
671 account, using equational assumptions in the subsequent
672 normalization process, or simplifying assumptions themselves (cf.\
673 \verb|asm_full_simp_tac| in \cite{isabelle-ref}). In structured
674 proofs this is usually quite well behaved in practice: just the
675 local premises of the actual goal are involved, additional facts may
676 be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
677 \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).
679 Additional Simplifier options may be specified to tune the behavior
680 further (mostly for unstructured scripts with many accidental local
681 facts): ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' means assumptions are ignored
682 completely (cf.\ \verb|simp_tac|), ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' means
683 assumptions are used in the simplification of the conclusion but are
684 not themselves simplified (cf.\ \verb|asm_simp_tac|), and ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' means assumptions are simplified but are not used
685 in the simplification of each other or the conclusion (cf.\ \verb|full_simp_tac|). For compatibility reasons, there is also an option
686 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{5F}{\isacharunderscore}}lr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'', which means that an assumption is only used
687 for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
689 The configuration option \isa{{\isaliteral{22}{\isachardoublequote}}depth{\isaliteral{5F}{\isacharunderscore}}limit{\isaliteral{22}{\isachardoublequote}}} limits the number of
690 recursive invocations of the simplifier during conditional
693 \medskip The Splitter package is usually configured to work as part
694 of the Simplifier. The effect of repeatedly applying \verb|split_tac| can be simulated by ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{3A}{\isacharcolon}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''. There is also a separate \isa{split}
695 method available for single-step case splitting.%
699 \isamarkupsubsection{Declaring rules%
703 \begin{isamarkuptext}%
704 \begin{matharray}{rcl}
705 \indexdef{}{command}{print\_simpset}\hypertarget{command.print-simpset}{\hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}simpset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
706 \indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isa{attribute} \\
707 \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
708 \indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isa{attribute} \\
714 \rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[]
716 \rail@term{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}}[]
718 \rail@term{\hyperlink{attribute.split}{\mbox{\isa{split}}}}[]
722 \rail@term{\isa{add}}[]
724 \rail@term{\isa{del}}[]
732 \item \hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}simpset}}}} prints the collection of rules
733 declared to the Simplifier, which is also known as ``simpset''
734 internally \cite{isabelle-ref}.
736 \item \hyperlink{attribute.simp}{\mbox{\isa{simp}}} declares simplification rules.
738 \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules.
740 \item \hyperlink{attribute.split}{\mbox{\isa{split}}} declares case split rules.
746 \isamarkupsubsection{Simplification procedures%
750 \begin{isamarkuptext}%
751 Simplification procedures are ML functions that produce proven
752 rewrite rules on demand. They are associated with higher-order
753 patterns that approximate the left-hand sides of equations. The
754 Simplifier first matches the current redex against one of the LHS
755 patterns; if this succeeds, the corresponding ML function is
756 invoked, passing the Simplifier context and redex term. Thus rules
757 may be specifically fashioned for particular situations, resulting
758 in a more powerful mechanism than term rewriting by a fixed set of
761 Any successful result needs to be a (possibly conditional) rewrite
762 rule \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u{\isaliteral{22}{\isachardoublequote}}} that is applicable to the current redex. The
763 rule will be applied just as any ordinary rewrite rule. It is
764 expected to be already in \emph{internal form}, bypassing the
765 automatic preprocessing of object-level equivalences.
767 \begin{matharray}{rcl}
768 \indexdef{}{command}{simproc\_setup}\hypertarget{command.simproc-setup}{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
769 simproc & : & \isa{attribute} \\
774 \rail@term{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
775 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
776 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
778 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
780 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
782 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
783 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
784 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
788 \rail@term{\isa{\isakeyword{identifier}}}[]
790 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
796 \rail@term{\hyperlink{attribute.simproc}{\mbox{\isa{simproc}}}}[]
800 \rail@term{\isa{add}}[]
801 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
804 \rail@term{\isa{del}}[]
805 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
808 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
817 \item \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}} defines a named simplification
818 procedure that is invoked by the Simplifier whenever any of the
819 given term patterns match the current redex. The implementation,
820 which is provided as ML source text, needs to be of type \verb|morphism -> simpset -> cterm -> thm option|, where the \verb|cterm| represents the current redex \isa{r} and the result is
821 supposed to be some proven rewrite rule \isa{{\isaliteral{22}{\isachardoublequote}}r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} (or a
822 generalized version), or \verb|NONE| to indicate failure. The
823 \verb|simpset| argument holds the full context of the current
824 Simplifier invocation, including the actual Isar proof context. The
825 \verb|morphism| informs about the difference of the original
826 compilation context wrt.\ the one of the actual application later
827 on. The optional \hyperlink{keyword.identifier}{\mbox{\isa{\isakeyword{identifier}}}} specifies theorems that
828 represent the logical content of the abstract theory of this
831 Morphisms and identifiers are only relevant for simprocs that are
832 defined within a local target context, e.g.\ in a locale.
834 \item \isa{{\isaliteral{22}{\isachardoublequote}}simproc\ add{\isaliteral{3A}{\isacharcolon}}\ name{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}simproc\ del{\isaliteral{3A}{\isacharcolon}}\ name{\isaliteral{22}{\isachardoublequote}}}
835 add or delete named simprocs to the current Simplifier context. The
836 default is to add a simproc. Note that \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}
837 already adds the new simproc to the subsequent context.
843 \isamarkupsubsubsection{Example%
847 \begin{isamarkuptext}%
848 The following simplification procedure for \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}u{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}unit{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}} in HOL performs fine-grained
849 control over rule application, beyond higher-order pattern matching.
850 Declaring \isa{unit{\isaliteral{5F}{\isacharunderscore}}eq} as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} directly would make
851 the simplifier loop! Note that a version of this simplification
852 procedure is already active in Isabelle/HOL.%
861 \isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
862 \ unit\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}unit{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
863 \ \ fn\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ct\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
864 \ \ \ \ if\ HOLogic{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}unit\ {\isaliteral{28}{\isacharparenleft}}term{\isaliteral{5F}{\isacharunderscore}}of\ ct{\isaliteral{29}{\isacharparenright}}\ then\ NONE\isanewline
865 \ \ \ \ else\ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}meta{\isaliteral{5F}{\isacharunderscore}}eq\ %
867 thm\ unit{\isaliteral{5F}{\isacharunderscore}}eq{}%
869 {\isaliteral{29}{\isacharparenright}}\isanewline
870 {\isaliteral{2A7D}{\isacharverbatimclose}}%
878 \begin{isamarkuptext}%
879 Since the Simplifier applies simplification procedures
880 frequently, it is important to make the failure check in ML
885 \isamarkupsubsection{Forward simplification%
889 \begin{isamarkuptext}%
890 \begin{matharray}{rcl}
891 \indexdef{}{attribute}{simplified}\hypertarget{attribute.simplified}{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}} & : & \isa{attribute} \\
896 \rail@term{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}}[]
899 \rail@nont{\isa{opt}}[]
903 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
906 \rail@begin{3}{\isa{opt}}
907 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
909 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm}}[]
911 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp}}[]
913 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use}}[]
915 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
922 \item \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} causes a theorem to
923 be simplified, either by exactly the specified rules \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, or the implicit Simplifier context if no arguments are given.
924 The result is fully simplified by default, including assumptions and
925 conclusion; the options \isa{no{\isaliteral{5F}{\isacharunderscore}}asm} etc.\ tune the Simplifier in
926 the same way as the for the \isa{simp} method.
928 Note that forward simplification restricts the simplifier to its
929 most basic operation of term rewriting; solver and looper tactics
930 \cite{isabelle-ref} are \emph{not} involved here. The \isa{simplified} attribute should be only rarely required under normal
937 \isamarkupsection{The Classical Reasoner \label{sec:classical}%
941 \isamarkupsubsection{Basic concepts%
945 \begin{isamarkuptext}%
946 Although Isabelle is generic, many users will be working in
947 some extension of classical first-order logic. Isabelle/ZF is built
948 upon theory FOL, while Isabelle/HOL conceptually contains
949 first-order logic as a fragment. Theorem-proving in predicate logic
950 is undecidable, but many automated strategies have been developed to
953 Isabelle's classical reasoner is a generic package that accepts
954 certain information about a logic and delivers a suite of automatic
955 proof tools, based on rules that are classified and declared in the
956 context. These proof procedures are slow and simplistic compared
957 with high-end automated theorem provers, but they can save
958 considerable time and effort in practice. They can prove theorems
959 such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few
960 milliseconds (including full proof reconstruction):%
963 \isacommand{lemma}\isamarkupfalse%
964 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F\ x\ y\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ F\ x\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}z{\isaliteral{2E}{\isachardot}}\ F\ z\ y\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F\ z\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
971 \isacommand{by}\isamarkupfalse%
981 \isacommand{lemma}\isamarkupfalse%
982 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}z{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ y\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ f\ x\ z\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ f\ x\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}z{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
989 \isacommand{by}\isamarkupfalse%
998 \begin{isamarkuptext}%
999 The proof tools are generic. They are not restricted to
1000 first-order logic, and have been heavily used in the development of
1001 the Isabelle/HOL library and applications. The tactics can be
1002 traced, and their components can be called directly; in this manner,
1003 any proof can be viewed interactively.%
1004 \end{isamarkuptext}%
1007 \isamarkupsubsubsection{The sequent calculus%
1011 \begin{isamarkuptext}%
1012 Isabelle supports natural deduction, which is easy to use for
1013 interactive proof. But natural deduction does not easily lend
1014 itself to automation, and has a bias towards intuitionism. For
1015 certain proofs in classical logic, it can not be called natural.
1016 The \emph{sequent calculus}, a generalization of natural deduction,
1017 is easier to automate.
1019 A \textbf{sequent} has the form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{22}{\isachardoublequote}}}
1020 and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{22}{\isachardoublequote}}} are sets of formulae.\footnote{For first-order
1021 logic, sequents can equivalently be made from lists or multisets of
1022 formulae.} The sequent \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} is
1023 \textbf{valid} if \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} implies \isa{{\isaliteral{22}{\isachardoublequote}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}. Thus \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} represent assumptions, each of which
1024 is true, while \isa{{\isaliteral{22}{\isachardoublequote}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} represent alternative goals. A
1025 sequent is \textbf{basic} if its left and right sides have a common
1026 formula, as in \isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{2C}{\isacharcomma}}\ Q\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q{\isaliteral{2C}{\isacharcomma}}\ R{\isaliteral{22}{\isachardoublequote}}}; basic sequents are trivially
1029 Sequent rules are classified as \textbf{right} or \textbf{left},
1030 indicating which side of the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}{\isaliteral{22}{\isachardoublequote}}} symbol they operate on.
1031 Rules that operate on the right side are analogous to natural
1032 deduction's introduction rules, and left rules are analogous to
1033 elimination rules. The sequent calculus analogue of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}I{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
1036 \infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{2C}{\isacharcomma}}\ P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{2C}{\isacharcomma}}\ Q{\isaliteral{22}{\isachardoublequote}}}}
1038 Applying the rule backwards, this breaks down some implication on
1039 the right side of a sequent; \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{22}{\isachardoublequote}}} stand for
1040 the sets of formulae that are unaffected by the inference. The
1041 analogue of the pair \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}I{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}I{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is the
1044 \infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{2C}{\isacharcomma}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{2C}{\isacharcomma}}\ P{\isaliteral{2C}{\isacharcomma}}\ Q{\isaliteral{22}{\isachardoublequote}}}}
1046 This breaks down some disjunction on the right side, replacing it by
1047 both disjuncts. Thus, the sequent calculus is a kind of
1048 multiple-conclusion logic.
1050 To illustrate the use of multiple formulae on the right, let us
1051 prove the classical theorem \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Working
1052 backwards, we reduce this formula to a basic sequent:
1054 \infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}
1055 {\infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}
1056 {\infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}
1057 {\isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{2C}{\isacharcomma}}\ Q\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q{\isaliteral{2C}{\isacharcomma}}\ P{\isaliteral{22}{\isachardoublequote}}}}}}
1060 This example is typical of the sequent calculus: start with the
1061 desired theorem and apply rules backwards in a fairly arbitrary
1062 manner. This yields a surprisingly effective proof procedure.
1063 Quantifiers add only few complications, since Isabelle handles
1064 parameters and schematic variables. See \cite[Chapter
1065 10]{paulson-ml2} for further discussion.%
1066 \end{isamarkuptext}%
1069 \isamarkupsubsubsection{Simulating sequents by natural deduction%
1073 \begin{isamarkuptext}%
1074 Isabelle can represent sequents directly, as in the
1075 object-logic LK. But natural deduction is easier to work with, and
1076 most object-logics employ it. Fortunately, we can simulate the
1077 sequent \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} by the Isabelle formula
1078 \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} where the order of
1079 the assumptions and the choice of \isa{{\isaliteral{22}{\isachardoublequote}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} are arbitrary.
1080 Elim-resolution plays a key role in simulating sequent proofs.
1082 We can easily handle reasoning on the left. Elim-resolution with
1083 the rules \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} achieves
1084 a similar effect as the corresponding sequent rules. For the other
1085 connectives, we use sequent-style elimination rules instead of
1086 destruction rules such as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616E643E}{\isasymand}}E{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
1087 But note that the rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} has no effect under our
1088 representation of sequents!
1090 \infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{2C}{\isacharcomma}}\ P{\isaliteral{22}{\isachardoublequote}}}}
1093 What about reasoning on the right? Introduction rules can only
1094 affect the formula in the conclusion, namely \isa{{\isaliteral{22}{\isachardoublequote}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}. The
1095 other right-side formulae are represented as negated assumptions,
1096 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}. In order to operate on one of these, it
1097 must first be exchanged with \isa{{\isaliteral{22}{\isachardoublequote}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}. Elim-resolution with the
1098 \isa{swap} rule has this effect: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ R\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequote}}}
1100 To ensure that swaps occur only when necessary, each introduction
1101 rule is converted into a swapped form: it is resolved with the
1102 second premise of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}swap{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. The swapped form of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616E643E}{\isasymand}}I{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, which might be called \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{5C3C616E643E}{\isasymand}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, is
1104 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ R\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ R\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequote}}%
1107 Similarly, the swapped form of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}I{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is
1109 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ R\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequote}}%
1112 Swapped introduction rules are applied using elim-resolution, which
1113 deletes the negated formula. Our representation of sequents also
1114 requires the use of ordinary introduction rules. If we had no
1115 regard for readability of intermediate goal states, we could treat
1116 the right side more uniformly by representing sequents as \begin{isabelle}%
1117 {\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequote}}%
1119 \end{isamarkuptext}%
1122 \isamarkupsubsubsection{Extra rules for the sequent calculus%
1126 \begin{isamarkuptext}%
1127 As mentioned, destruction rules such as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616E643E}{\isasymand}}E{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and
1128 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} must be replaced by sequent-style elimination rules.
1129 In addition, we need rules to embody the classical equivalence
1130 between \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}}. The introduction
1131 rules \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}I{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} are replaced by a rule that simulates
1132 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}: \begin{isabelle}%
1133 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}%
1136 The destruction rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is replaced by \begin{isabelle}%
1137 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequote}}%
1140 Quantifier replication also requires special rules. In classical
1141 logic, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} is equivalent to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}};
1142 the rules \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} are dual:
1144 \infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{2C}{\isacharcomma}}\ P\ t{\isaliteral{22}{\isachardoublequote}}}}
1146 \infer[\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}P\ t{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}{\isaliteral{22}{\isachardoublequote}}}}
1148 Thus both kinds of quantifier may be replicated. Theorems requiring
1149 multiple uses of a universal formula are easy to invent; consider
1151 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ P\ a\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}f\isaliteral{5C3C5E7375703E}{}\isactrlsup n\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
1152 \end{isabelle} for any
1153 \isa{{\isaliteral{22}{\isachardoublequote}}n\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}. Natural examples of the multiple use of an
1154 existential formula are rare; a standard one is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ y{\isaliteral{22}{\isachardoublequote}}}.
1156 Forgoing quantifier replication loses completeness, but gains
1157 decidability, since the search space becomes finite. Many useful
1158 theorems can be proved without replication, and the search generally
1159 delivers its verdict in a reasonable time. To adopt this approach,
1160 represent the sequent rules \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and
1161 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}R{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}I{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}I{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}},
1162 respectively, and put \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} into elimination form: \begin{isabelle}%
1163 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}%
1166 Elim-resolution with this rule will delete the universal formula
1167 after a single use. To replicate universal quantifiers, replace the
1168 rule by \begin{isabelle}%
1169 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}%
1172 To replicate existential quantifiers, replace \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}I{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} by
1174 {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}%
1177 All introduction rules mentioned above are also useful in swapped
1180 Replication makes the search space infinite; we must apply the rules
1181 with care. The classical reasoner distinguishes between safe and
1182 unsafe rules, applying the latter only when there is no alternative.
1183 Depth-first search may well go down a blind alley; best-first search
1184 is better behaved in an infinite search space. However, quantifier
1185 replication is too expensive to prove any but the simplest theorems.%
1186 \end{isamarkuptext}%
1189 \isamarkupsubsection{Rule declarations%
1193 \begin{isamarkuptext}%
1194 The proof tools of the Classical Reasoner depend on
1195 collections of rules declared in the context, which are classified
1196 as introduction, elimination or destruction and as \emph{safe} or
1197 \emph{unsafe}. In general, safe rules can be attempted blindly,
1198 while unsafe rules must be used with care. A safe rule must never
1199 reduce a provable goal to an unprovable set of subgoals.
1201 The rule \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} is unsafe because it reduces \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} to \isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{22}{\isachardoublequote}}}, which might turn out as premature choice of an
1202 unprovable subgoal. Any rule is unsafe whose premises contain new
1203 unknowns. The elimination rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} is
1204 unsafe, since it is applied via elim-resolution, which discards the
1205 assumption \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} and replaces it by the weaker
1206 assumption \isa{{\isaliteral{22}{\isachardoublequote}}P\ t{\isaliteral{22}{\isachardoublequote}}}. The rule \isa{{\isaliteral{22}{\isachardoublequote}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} is
1207 unsafe for similar reasons. The quantifier duplication rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} is unsafe in a different sense:
1208 since it keeps the assumption \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}, it is prone to
1209 looping. In classical first-order logic, all rules are safe except
1210 those mentioned above.
1212 The safe~/ unsafe distinction is vague, and may be regarded merely
1213 as a way of giving some rules priority over others. One could argue
1214 that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is unsafe, because repeated application of it
1215 could generate exponentially many subgoals. Induction rules are
1216 unsafe because inductive proofs are difficult to set up
1217 automatically. Any inference is unsafe that instantiates an unknown
1218 in the proof state --- thus matching must be used, rather than
1219 unification. Even proof by assumption is unsafe if it instantiates
1220 unknowns shared with other subgoals.
1222 \begin{matharray}{rcl}
1223 \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1224 \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
1225 \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
1226 \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
1227 \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\
1228 \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\
1229 \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\
1235 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
1237 \rail@term{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}}[]
1239 \rail@term{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}}[]
1242 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
1245 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1249 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1253 \rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
1254 \rail@term{\isa{del}}[]
1257 \rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[]
1261 \rail@term{\isa{add}}[]
1265 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1268 \rail@term{\isa{del}}[]
1276 \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}} prints the collection of rules
1277 declared to the Classical Reasoner, i.e.\ the \verb|claset|
1280 \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}}
1281 declare introduction, elimination, and destruction rules,
1282 respectively. By default, rules are considered as \emph{unsafe}
1283 (i.e.\ not applied blindly without backtracking), while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' classifies as \emph{safe}. Rule declarations marked by
1284 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' coincide with those of Isabelle/Pure, cf.\
1285 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
1286 of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number
1287 specifies an explicit weight argument, which is ignored by the
1288 automated reasoning tools, but determines the search order of single
1291 Introduction rules are those that can be applied using ordinary
1292 resolution. Their swapped forms are generated internally, which
1293 will be applied using elim-resolution. Elimination rules are
1294 applied using elim-resolution. Rules are sorted by the number of
1295 new subgoals they will yield; rules that generate the fewest
1296 subgoals will be tried first. Otherwise, later declarations take
1297 precedence over earlier ones.
1299 Rules already present in the context with the same classification
1300 are ignored. A warning is printed if the rule has already been
1301 added with some other classification, but the rule is added anyway
1304 \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes all occurrences of a
1305 rule from the classical context, regardless of its classification as
1306 introduction~/ elimination~/ destruction and safe~/ unsafe.
1308 \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the
1309 Simplifier and the Classical reasoner at the same time.
1310 Non-conditional rules result in a safe introduction and elimination
1311 pair; conditional ones are considered unsafe. Rules with negative
1312 conclusion are automatically inverted (using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{22}{\isachardoublequote}}}-elimination
1315 The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to
1316 the Isabelle/Pure context only, and omits the Simplifier
1319 \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an
1320 elimination, by resolving with the classical swap principle \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ R\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequote}}} in the second position. This is mainly for
1321 illustrative purposes: the Classical Reasoner already swaps rules
1322 internally as explained above.
1325 \end{isamarkuptext}%
1328 \isamarkupsubsection{Structured methods%
1332 \begin{isamarkuptext}%
1333 \begin{matharray}{rcl}
1334 \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
1335 \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
1340 \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
1343 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1351 \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
1352 refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
1353 versions work the same, but the classical version observes the
1354 classical rule context in addition to that of Isabelle/Pure.
1356 Common object logics (HOL, ZF, etc.) declare a rich collection of
1357 classical rules (even if these would qualify as intuitionistic
1358 ones), but only few declarations to the rule context of
1359 Isabelle/Pure (\secref{sec:pure-meth-att}).
1361 \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
1362 deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
1363 facts, which are guaranteed to participate, may appear in either
1367 \end{isamarkuptext}%
1370 \isamarkupsubsection{Automated methods%
1374 \begin{isamarkuptext}%
1375 \begin{matharray}{rcl}
1376 \indexdef{}{method}{blast}\hypertarget{method.blast}{\hyperlink{method.blast}{\mbox{\isa{blast}}}} & : & \isa{method} \\
1377 \indexdef{}{method}{auto}\hypertarget{method.auto}{\hyperlink{method.auto}{\mbox{\isa{auto}}}} & : & \isa{method} \\
1378 \indexdef{}{method}{force}\hypertarget{method.force}{\hyperlink{method.force}{\mbox{\isa{force}}}} & : & \isa{method} \\
1379 \indexdef{}{method}{fast}\hypertarget{method.fast}{\hyperlink{method.fast}{\mbox{\isa{fast}}}} & : & \isa{method} \\
1380 \indexdef{}{method}{slow}\hypertarget{method.slow}{\hyperlink{method.slow}{\mbox{\isa{slow}}}} & : & \isa{method} \\
1381 \indexdef{}{method}{best}\hypertarget{method.best}{\hyperlink{method.best}{\mbox{\isa{best}}}} & : & \isa{method} \\
1382 \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
1383 \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
1384 \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
1385 \indexdef{}{method}{deepen}\hypertarget{method.deepen}{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}} & : & \isa{method} \\
1390 \rail@term{\hyperlink{method.blast}{\mbox{\isa{blast}}}}[]
1393 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1397 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
1401 \rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[]
1404 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1405 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1409 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1413 \rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[]
1416 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1421 \rail@term{\hyperlink{method.fast}{\mbox{\isa{fast}}}}[]
1423 \rail@term{\hyperlink{method.slow}{\mbox{\isa{slow}}}}[]
1425 \rail@term{\hyperlink{method.best}{\mbox{\isa{best}}}}[]
1429 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
1434 \rail@term{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}}[]
1436 \rail@term{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}}[]
1438 \rail@term{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}}[]
1442 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1446 \rail@term{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}}[]
1449 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1453 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
1456 \rail@begin{4}{\indexdef{}{syntax}{clamod}\hypertarget{syntax.clamod}{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}}
1459 \rail@term{\isa{intro}}[]
1461 \rail@term{\isa{elim}}[]
1463 \rail@term{\isa{dest}}[]
1466 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
1469 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1472 \rail@term{\isa{del}}[]
1474 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1475 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1477 \rail@begin{14}{\indexdef{}{syntax}{clasimpmod}\hypertarget{syntax.clasimpmod}{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}}
1479 \rail@term{\isa{simp}}[]
1482 \rail@term{\isa{add}}[]
1484 \rail@term{\isa{del}}[]
1486 \rail@term{\isa{only}}[]
1490 \rail@term{\isa{cong}}[]
1492 \rail@term{\isa{split}}[]
1496 \rail@term{\isa{add}}[]
1498 \rail@term{\isa{del}}[]
1501 \rail@term{\isa{iff}}[]
1505 \rail@term{\isa{add}}[]
1509 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1512 \rail@term{\isa{del}}[]
1517 \rail@term{\isa{intro}}[]
1519 \rail@term{\isa{elim}}[]
1521 \rail@term{\isa{dest}}[]
1524 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
1527 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1530 \rail@term{\isa{del}}[]
1533 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1534 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1541 \item \hyperlink{method.blast}{\mbox{\isa{blast}}} is a separate classical tableau prover that
1542 uses the same classical rule declarations as explained before.
1544 Proof search is coded directly in ML using special data structures.
1545 A successful proof is then reconstructed using regular Isabelle
1546 inferences. It is faster and more powerful than the other classical
1547 reasoning tools, but has major limitations too.
1551 \item It does not use the classical wrapper tacticals, such as the
1552 integration with the Simplifier of \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}.
1554 \item It does not perform higher-order unification, as needed by the
1555 rule \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f} in HOL. There are often
1556 alternatives to such rules, for example \isa{{\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f}.
1558 \item Function variables may only be applied to parameters of the
1559 subgoal. (This restriction arises because the prover does not use
1560 higher-order unification.) If other function variables are present
1561 then the prover will fail with the message \texttt{Function Var's
1562 argument not a bound variable}.
1564 \item Its proof strategy is more general than \hyperlink{method.fast}{\mbox{\isa{fast}}} but can
1565 be slower. If \hyperlink{method.blast}{\mbox{\isa{blast}}} fails or seems to be running forever,
1566 try \hyperlink{method.fast}{\mbox{\isa{fast}}} and the other proof tools described below.
1570 The optional integer argument specifies a bound for the number of
1571 unsafe steps used in a proof. By default, \hyperlink{method.blast}{\mbox{\isa{blast}}} starts
1572 with a bound of 0 and increases it successively to 20. In contrast,
1573 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}blast\ lim{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} tries to prove the goal using a search bound
1574 of \isa{{\isaliteral{22}{\isachardoublequote}}lim{\isaliteral{22}{\isachardoublequote}}}. Sometimes a slow proof using \hyperlink{method.blast}{\mbox{\isa{blast}}} can
1575 be made much faster by supplying the successful search bound to this
1576 proof method instead.
1578 \item \hyperlink{method.auto}{\mbox{\isa{auto}}} combines classical reasoning with
1579 simplification. It is intended for situations where there are a lot
1580 of mostly trivial subgoals; it proves all the easy ones, leaving the
1581 ones it cannot prove. Occasionally, attempting to prove the hard
1582 ones may take a long time.
1584 The optional depth arguments in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}auto\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} refer to its
1585 builtin classical reasoning procedures: \isa{m} (default 4) is for
1586 \hyperlink{method.blast}{\mbox{\isa{blast}}}, which is tried first, and \isa{n} (default 2) is
1587 for a slower but more general alternative that also takes wrappers
1590 \item \hyperlink{method.force}{\mbox{\isa{force}}} is intended to prove the first subgoal
1591 completely, using many fancy proof tools and performing a rather
1592 exhaustive search. As a result, proof attempts may take rather long
1595 \item \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}} attempt to
1596 prove the first subgoal using sequent-style reasoning as explained
1597 before. Unlike \hyperlink{method.blast}{\mbox{\isa{blast}}}, they construct proofs directly in
1600 There is a difference in search strategy and back-tracking: \hyperlink{method.fast}{\mbox{\isa{fast}}} uses depth-first search and \hyperlink{method.best}{\mbox{\isa{best}}} uses best-first
1601 search (guided by a heuristic function: normally the total size of
1604 Method \hyperlink{method.slow}{\mbox{\isa{slow}}} is like \hyperlink{method.fast}{\mbox{\isa{fast}}}, but conducts a broader
1605 search: it may, when backtracking from a failed proof attempt, undo
1606 even the step of proving a subgoal by assumption.
1608 \item \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are
1609 like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
1610 but use the Simplifier as additional wrapper.
1612 \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
1613 depth. The start depth is 4 (unless specified explicitly), and the
1614 depth is increased iteratively up to 10. Unsafe rules are modified
1615 to preserve the formula they act on, so that it be used repeatedly.
1616 This method can prove more goals than \hyperlink{method.fast}{\mbox{\isa{fast}}}, but is much
1617 slower, for example if the assumptions have many universal
1622 Any of the above methods support additional modifiers of the context
1623 of classical (and simplifier) rules, but the ones related to the
1624 Simplifier are explicitly prefixed by \isa{simp} here. The
1625 semantics of these ad-hoc rule declarations is analogous to the
1626 attributes given before. Facts provided by forward chaining are
1627 inserted into the goal before commencing proof search.%
1628 \end{isamarkuptext}%
1631 \isamarkupsubsection{Semi-automated methods%
1635 \begin{isamarkuptext}%
1636 These proof methods may help in situations when the
1637 fully-automated tools fail. The result is a simpler subgoal that
1638 can be tackled by other means, such as by manual instantiation of
1641 \begin{matharray}{rcl}
1642 \indexdef{}{method}{safe}\hypertarget{method.safe}{\hyperlink{method.safe}{\mbox{\isa{safe}}}} & : & \isa{method} \\
1643 \indexdef{}{method}{clarify}\hypertarget{method.clarify}{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}} & : & \isa{method} \\
1644 \indexdef{}{method}{clarsimp}\hypertarget{method.clarsimp}{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}} & : & \isa{method} \\
1650 \rail@term{\hyperlink{method.safe}{\mbox{\isa{safe}}}}[]
1652 \rail@term{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}}[]
1656 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
1660 \rail@term{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}}[]
1663 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1671 \item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
1672 It is deterministic, with at most one outcome.
1674 \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps without
1675 splitting subgoals; see also \verb|clarify_step_tac|.
1677 \item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
1678 simplification. Note that if the Simplifier context includes a
1679 splitter for the premises, the subgoal may still be split.
1682 \end{isamarkuptext}%
1685 \isamarkupsubsection{Single-step tactics%
1689 \begin{isamarkuptext}%
1690 \begin{matharray}{rcl}
1691 \indexdef{}{ML}{safe\_step\_tac}\verb|safe_step_tac: Proof.context -> int -> tactic| \\
1692 \indexdef{}{ML}{inst\_step\_tac}\verb|inst_step_tac: Proof.context -> int -> tactic| \\
1693 \indexdef{}{ML}{step\_tac}\verb|step_tac: Proof.context -> int -> tactic| \\
1694 \indexdef{}{ML}{slow\_step\_tac}\verb|slow_step_tac: Proof.context -> int -> tactic| \\
1695 \indexdef{}{ML}{clarify\_step\_tac}\verb|clarify_step_tac: Proof.context -> int -> tactic| \\
1698 These are the primitive tactics behind the (semi)automated proof
1699 methods of the Classical Reasoner. By calling them yourself, you
1700 can execute these procedures one step at a time.
1704 \item \verb|safe_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step on
1705 subgoal \isa{i}. The safe wrapper tacticals are applied to a
1706 tactic that may include proof by assumption or Modus Ponens (taking
1707 care not to instantiate unknowns), or substitution.
1709 \item \verb|inst_step_tac| is like \verb|safe_step_tac|, but allows
1710 unknowns to be instantiated.
1712 \item \verb|step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} is the basic step of the proof
1713 procedure. The unsafe wrapper tacticals are applied to a tactic
1714 that tries \verb|safe_tac|, \verb|inst_step_tac|, or applies an unsafe
1715 rule from the context.
1717 \item \verb|slow_step_tac| resembles \verb|step_tac|, but allows
1718 backtracking between using safe rules with instantiation (\verb|inst_step_tac|) and using unsafe rules. The resulting search space
1721 \item \verb|clarify_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step
1722 on subgoal \isa{i}. No splitting step is applied; for example,
1723 the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction. Proof by
1724 assumption, Modus Ponens, etc., may be performed provided they do
1725 not instantiate unknowns. Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}}
1726 may be eliminated. The safe wrapper tactical is applied.
1729 \end{isamarkuptext}%
1732 \isamarkupsection{Object-logic setup \label{sec:object-logic}%
1736 \begin{isamarkuptext}%
1737 \begin{matharray}{rcl}
1738 \indexdef{}{command}{judgment}\hypertarget{command.judgment}{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1739 \indexdef{}{method}{atomize}\hypertarget{method.atomize}{\hyperlink{method.atomize}{\mbox{\isa{atomize}}}} & : & \isa{method} \\
1740 \indexdef{}{attribute}{atomize}\hypertarget{attribute.atomize}{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}} & : & \isa{attribute} \\
1741 \indexdef{}{attribute}{rule\_format}\hypertarget{attribute.rule-format}{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}} & : & \isa{attribute} \\
1742 \indexdef{}{attribute}{rulify}\hypertarget{attribute.rulify}{\hyperlink{attribute.rulify}{\mbox{\isa{rulify}}}} & : & \isa{attribute} \\
1745 The very starting point for any Isabelle object-logic is a ``truth
1746 judgment'' that links object-level statements to the meta-logic
1747 (with its minimal language of \isa{prop} that covers universal
1748 quantification \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and implication \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}}).
1750 Common object-logics are sufficiently expressive to internalize rule
1751 statements over \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} within their own
1752 language. This is useful in certain situations where a rule needs
1753 to be viewed as an atomic statement from the meta-level perspective,
1754 e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} versus \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}.
1756 From the following language elements, only the \hyperlink{method.atomize}{\mbox{\isa{atomize}}}
1757 method and \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}} attribute are occasionally
1758 required by end-users, the rest is for those who need to setup their
1759 own object-logic. In the latter case existing formulations of
1760 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
1762 Generic tools may refer to the information provided by object-logic
1763 declarations internally.
1767 \rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
1768 \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
1771 \rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
1774 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1775 \rail@term{\isa{full}}[]
1776 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1780 \rail@term{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1783 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1784 \rail@term{\isa{noasm}}[]
1785 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1793 \item \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} declares constant
1794 \isa{c} as the truth judgment of the current object-logic. Its
1795 type \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}} should specify a coercion of the category of
1796 object-level propositions to \isa{prop} of the Pure meta-logic;
1797 the mixfix annotation \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} would typically just link the
1798 object language (internally of syntactic category \isa{logic})
1799 with that of \isa{prop}. Only one \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}
1800 declaration may be given in any theory development.
1802 \item \hyperlink{method.atomize}{\mbox{\isa{atomize}}} (as a method) rewrites any non-atomic
1803 premises of a sub-goal, using the meta-level equations declared via
1804 \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} (as an attribute) beforehand. As a result,
1805 heavily nested goals become amenable to fundamental operations such
1806 as resolution (cf.\ the \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method). Giving the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}full{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option here means to turn the whole subgoal into an
1807 object-statement (if possible), including the outermost parameters
1808 and assumptions as well.
1810 A typical collection of \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} rules for a particular
1811 object-logic would provide an internalization for each of the
1812 connectives of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}}.
1813 Meta-level conjunction should be covered as well (this is
1814 particularly important for locales, see \secref{sec:locale}).
1816 \item \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}} rewrites a theorem by the equalities
1817 declared as \hyperlink{attribute.rulify}{\mbox{\isa{rulify}}} rules in the current object-logic.
1818 By default, the result is fully normalized, including assumptions
1819 and conclusions at any depth. The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option
1820 restricts the transformation to the conclusion of a rule.
1822 In common object-logics (HOL, FOL, ZF), the effect of \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}} is to replace (bounded) universal quantification
1823 (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}) and implication (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequote}}}) by the corresponding
1824 rule statements over \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}}.
1827 \end{isamarkuptext}%
1835 \isacommand{end}\isamarkupfalse%
1845 %%% Local Variables:
1847 %%% TeX-master: "root"