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}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
127 \indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
133 \rail@term{\hyperlink{method.fold}{\mbox{\isa{fold}}}}[]
135 \rail@term{\hyperlink{method.unfold}{\mbox{\isa{unfold}}}}[]
137 \rail@term{\hyperlink{method.insert}{\mbox{\isa{insert}}}}[]
139 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
143 \rail@term{\hyperlink{method.erule}{\mbox{\isa{erule}}}}[]
145 \rail@term{\hyperlink{method.drule}{\mbox{\isa{drule}}}}[]
147 \rail@term{\hyperlink{method.frule}{\mbox{\isa{frule}}}}[]
151 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
152 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
153 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
155 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
162 \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
163 all goals; any chained facts provided are inserted into the goal and
164 subject to rewriting as well.
166 \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
167 into all goals of the proof state. Note that current facts
168 indicated for forward chaining are ignored.
170 \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}}}
171 method (see \secref{sec:pure-meth-att}), but apply rules by
172 elim-resolution, destruct-resolution, and forward-resolution,
173 respectively \cite{isabelle-implementation}. The optional natural
174 number argument (default 0) specifies additional assumption steps to
177 Note that these methods are improper ones, mainly serving for
178 experimentation and tactic script emulation. Different modes of
179 basic rule application are usually expressed in Isar at the proof
180 language level, rather than via implicit proof state manipulations.
181 For example, a proper single-step elimination would be done using
182 the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
185 \item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
186 the identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
187 \secref{sec:proof-meth}).
189 \item \hyperlink{method.fail}{\mbox{\isa{fail}}} yields an empty result sequence; it is the
190 identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
191 \secref{sec:proof-meth}).
195 \begin{matharray}{rcl}
196 \indexdef{}{attribute}{tagged}\hypertarget{attribute.tagged}{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}} & : & \isa{attribute} \\
197 \indexdef{}{attribute}{untagged}\hypertarget{attribute.untagged}{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}} & : & \isa{attribute} \\[0.5ex]
198 \indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isa{attribute} \\
199 \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isa{attribute} \\[0.5ex]
200 \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isa{attribute} \\
201 \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\[0.5ex]
202 \indexdef{}{attribute}{rotated}\hypertarget{attribute.rotated}{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}} & : & \isa{attribute} \\
203 \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim-format}{\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}format}}}} & : & \isa{attribute} \\
204 \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} \\
205 \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} \\
210 \rail@term{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}}[]
211 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
212 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
215 \rail@term{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}}[]
216 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
220 \rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[]
222 \rail@term{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}}[]
226 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
227 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
228 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
230 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
234 \rail@term{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}}[]
236 \rail@term{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}}[]
238 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
241 \rail@term{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}}[]
244 \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
252 \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.
253 Tags may be any list of string pairs that serve as formal comment.
254 The first string is considered the tag name, the second its value.
255 Note that \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} removes any tags of the same name.
257 \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} and \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}~\isa{a}
258 compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
259 first premise of \isa{a} (an alternative position may be also
260 specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
261 lifting process that is normally intended (cf.\ \verb|op RS| and
262 \verb|op COMP| in \cite{isabelle-implementation}).
264 \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
265 definitions throughout a rule.
267 \item \hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n} rotate the premises of a
268 theorem by \isa{n} (default 1).
270 \item \hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}format}}} turns a destruction rule into
271 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}}}.
273 Note that the Classical Reasoner (\secref{sec:classical}) provides
274 its own version of this operation.
276 \item \hyperlink{attribute.standard}{\mbox{\isa{standard}}} puts a theorem into the standard form of
277 object-rules at the outermost theory level. Note that this
278 operation violates the local proof context (including active
281 \item \hyperlink{attribute.no-vars}{\mbox{\isa{no{\isaliteral{5F}{\isacharunderscore}}vars}}} replaces schematic variables by free
282 ones; this is mainly for tuning output of pretty printed theorems.
288 \isamarkupsubsection{Low-level equational reasoning%
292 \begin{isamarkuptext}%
293 \begin{matharray}{rcl}
294 \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}} & : & \isa{method} \\
295 \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}} & : & \isa{method} \\
296 \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}} & : & \isa{method} \\
301 \rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[]
304 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
305 \rail@term{\isa{asm}}[]
306 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
310 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
312 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
315 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
317 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
320 \rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
323 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
324 \rail@term{\isa{asm}}[]
325 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
327 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
332 These methods provide low-level facilities for equational reasoning
333 that are intended for specialized applications only. Normally,
334 single step calculations would be performed in a structured text
335 (see also \secref{sec:calculation}), while the Simplifier methods
336 provide the canonical way for automated normalization (see
337 \secref{sec:simplifier}).
341 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq} performs a single substitution step
342 using rule \isa{eq}, which may be either a meta or object
345 \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
348 \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
349 substitutions in the conclusion. The numbers \isa{i} to \isa{j}
350 indicate the positions to substitute at. Positions are ordered from
351 the top of the term tree moving down from left to right. For
352 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
353 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}}}.
355 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
356 (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
357 assume all substitutions are performed simultaneously. Otherwise
358 the behaviour of \isa{subst} is not specified.
360 \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
361 substitutions in the assumptions. The positions refer to the
362 assumptions in order from left to right. For example, given in a
363 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
364 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
365 position 2 is the subterm \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{22}{\isachardoublequote}}}.
367 \item \hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}} performs substitution using some
368 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.
370 \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
371 splitting using the given rules. By default, splitting is performed
372 in the conclusion of a goal; the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option indicates to
373 operate on assumptions instead.
375 Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
376 application of split rules as declared in the current context.
382 \isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
386 \begin{isamarkuptext}%
387 The following improper proof methods emulate traditional tactics.
388 These admit direct access to the goal state, which is normally
389 considered harmful! In particular, this may involve both numbered
390 goal addressing (default 1), and dynamic instantiation within the
391 scope of some subgoal.
394 Dynamic instantiations refer to universally quantified parameters
395 of a subgoal (the dynamic context) rather than fixed variables and
396 term abbreviations of a (static) Isar context.
399 Tactic emulation methods, unlike their ML counterparts, admit
400 simultaneous instantiation from both dynamic and static contexts.
401 If names occur in both contexts goal parameters hide locally fixed
402 variables. Likewise, schematic variables refer to term
403 abbreviations, if present in the static context. Otherwise the
404 schematic variable is interpreted as a schematic variable and left
405 to be solved by unification with certain parts of the subgoal.
407 Note that the tactic emulation proof methods in Isabelle/Isar are
408 consistently named \isa{foo{\isaliteral{5F}{\isacharunderscore}}tac}. Note also that variable names
409 occurring on left hand sides of instantiations must be preceded by a
410 question mark if they coincide with a keyword or contain dots. This
411 is consistent with the attribute \hyperlink{attribute.where}{\mbox{\isa{where}}} (see
412 \secref{sec:pure-meth-att}).
414 \begin{matharray}{rcl}
415 \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} \\
416 \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} \\
417 \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} \\
418 \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} \\
419 \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} \\
420 \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} \\
421 \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} \\
422 \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} \\
423 \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} \\
424 \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} \\
425 \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} \\
431 \rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
433 \rail@term{\hyperlink{method.erule-tac}{\mbox{\isa{erule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
435 \rail@term{\hyperlink{method.drule-tac}{\mbox{\isa{drule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
437 \rail@term{\hyperlink{method.frule-tac}{\mbox{\isa{frule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
439 \rail@term{\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
441 \rail@term{\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
445 \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
448 \rail@nont{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}[]
449 \rail@term{\isa{\isakeyword{in}}}[]
450 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
452 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
456 \rail@term{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
459 \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
462 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
467 \rail@term{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
470 \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
473 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
478 \rail@term{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
481 \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
485 \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
490 \rail@term{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}[]
492 \rail@term{\hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isaliteral{5F}{\isacharunderscore}}tactic}}}}[]
494 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
496 \rail@begin{2}{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}
498 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
499 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
500 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
502 \rail@cterm{\isa{\isakeyword{and}}}[]
510 \item \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} etc. do resolution of rules with explicit
511 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite{isabelle-implementation})
513 Multiple rules may be only given if there is no instantiation; then
514 \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} is the same as \verb|resolve_tac| in ML (see
515 \cite{isabelle-implementation}).
517 \item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isaliteral{5F}{\isacharunderscore}}tac}}} inserts facts into the proof state as
518 assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
519 \cite{isabelle-implementation}. Note that the scope of schematic
520 variables is spread over the main goal statement. Instantiations
521 may be given as well, see also ML tactic \verb|cut_inst_tac| in
522 \cite{isabelle-implementation}.
524 \item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} deletes the specified assumption
525 from a subgoal; note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain schematic variables.
526 See also \verb|thin_tac| in \cite{isabelle-implementation}.
528 \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} adds \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as an
529 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
531 \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
532 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
533 \emph{suffix} of variables.
535 \item \hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{n} rotates the assumptions of a
536 goal by \isa{n} positions: from right to left if \isa{n} is
537 positive, and from left to right if \isa{n} is negative; the
538 default value is 1. See also \verb|rotate_tac| in
539 \cite{isabelle-implementation}.
541 \item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} produces a proof method from
542 any ML text of type \verb|tactic|. Apart from the usual ML
543 environment and the current proof context, the ML code may refer to
544 the locally bound values \verb|facts|, which indicates any
545 current facts used for forward-chaining.
547 \item \hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isaliteral{5F}{\isacharunderscore}}tactic}}} is similar to \hyperlink{method.tactic}{\mbox{\isa{tactic}}}, but
548 presents the goal state in its raw internal form, where simultaneous
549 subgoals appear as conjunction of the logical framework instead of
550 the usual split into several subgoals. While feature this is useful
551 for debugging of complex method definitions, it should not never
552 appear in production theories.
558 \isamarkupsection{The Simplifier \label{sec:simplifier}%
562 \isamarkupsubsection{Simplification methods%
566 \begin{isamarkuptext}%
567 \begin{matharray}{rcl}
568 \indexdef{}{method}{simp}\hypertarget{method.simp}{\hyperlink{method.simp}{\mbox{\isa{simp}}}} & : & \isa{method} \\
569 \indexdef{}{method}{simp\_all}\hypertarget{method.simp-all}{\hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}}} & : & \isa{method} \\
575 \rail@term{\hyperlink{method.simp}{\mbox{\isa{simp}}}}[]
577 \rail@term{\hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}}}[]
581 \rail@nont{\isa{opt}}[]
585 \rail@cnont{\hyperlink{syntax.simpmod}{\mbox{\isa{simpmod}}}}[]
588 \rail@begin{4}{\isa{opt}}
589 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
591 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm}}[]
593 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp}}[]
595 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use}}[]
597 \rail@term{\isa{asm{\isaliteral{5F}{\isacharunderscore}}lr}}[]
599 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
601 \rail@begin{9}{\indexdef{}{syntax}{simpmod}\hypertarget{syntax.simpmod}{\hyperlink{syntax.simpmod}{\mbox{\isa{simpmod}}}}}
603 \rail@term{\isa{add}}[]
605 \rail@term{\isa{del}}[]
607 \rail@term{\isa{only}}[]
609 \rail@term{\isa{cong}}[]
612 \rail@term{\isa{add}}[]
614 \rail@term{\isa{del}}[]
617 \rail@term{\isa{split}}[]
620 \rail@term{\isa{add}}[]
622 \rail@term{\isa{del}}[]
625 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
626 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
633 \item \hyperlink{method.simp}{\mbox{\isa{simp}}} invokes the Simplifier, after declaring
634 additional rules according to the arguments given. Note that the
635 \isa{only} modifier first removes all other rewrite rules,
636 congruences, and looper tactics (including splits), and then behaves
639 \medskip The \isa{cong} modifiers add or delete Simplifier
640 congruence rules (see also \cite{isabelle-ref}), the default is to
643 \medskip The \isa{split} modifiers add or delete rules for the
644 Splitter (see also \cite{isabelle-ref}), the default is to add.
645 This works only if the Simplifier method has been properly setup to
646 include the Splitter (all major object logics such HOL, HOLCF, FOL,
649 \item \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} is similar to \hyperlink{method.simp}{\mbox{\isa{simp}}}, but acts on
650 all goals (backwards from the last to the first one).
654 By default the Simplifier methods take local assumptions fully into
655 account, using equational assumptions in the subsequent
656 normalization process, or simplifying assumptions themselves (cf.\
657 \verb|asm_full_simp_tac| in \cite{isabelle-ref}). In structured
658 proofs this is usually quite well behaved in practice: just the
659 local premises of the actual goal are involved, additional facts may
660 be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
661 \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).
663 Additional Simplifier options may be specified to tune the behavior
664 further (mostly for unstructured scripts with many accidental local
665 facts): ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' means assumptions are ignored
666 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
667 assumptions are used in the simplification of the conclusion but are
668 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
669 in the simplification of each other or the conclusion (cf.\ \verb|full_simp_tac|). For compatibility reasons, there is also an option
670 ``\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
671 for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
673 The configuration option \isa{{\isaliteral{22}{\isachardoublequote}}depth{\isaliteral{5F}{\isacharunderscore}}limit{\isaliteral{22}{\isachardoublequote}}} limits the number of
674 recursive invocations of the simplifier during conditional
677 \medskip The Splitter package is usually configured to work as part
678 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}
679 method available for single-step case splitting.%
683 \isamarkupsubsection{Declaring rules%
687 \begin{isamarkuptext}%
688 \begin{matharray}{rcl}
689 \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}}} \\
690 \indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isa{attribute} \\
691 \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
692 \indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isa{attribute} \\
698 \rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[]
700 \rail@term{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}}[]
702 \rail@term{\hyperlink{attribute.split}{\mbox{\isa{split}}}}[]
706 \rail@term{\isa{add}}[]
708 \rail@term{\isa{del}}[]
716 \item \hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}simpset}}}} prints the collection of rules
717 declared to the Simplifier, which is also known as ``simpset''
718 internally \cite{isabelle-ref}.
720 \item \hyperlink{attribute.simp}{\mbox{\isa{simp}}} declares simplification rules.
722 \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules.
724 \item \hyperlink{attribute.split}{\mbox{\isa{split}}} declares case split rules.
730 \isamarkupsubsection{Simplification procedures%
734 \begin{isamarkuptext}%
735 \begin{matharray}{rcl}
736 \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}}} \\
737 simproc & : & \isa{attribute} \\
742 \rail@term{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
743 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
744 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
746 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
748 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
750 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
751 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
752 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
756 \rail@term{\isa{\isakeyword{identifier}}}[]
758 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
764 \rail@term{\hyperlink{attribute.simproc}{\mbox{\isa{simproc}}}}[]
768 \rail@term{\isa{add}}[]
769 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
772 \rail@term{\isa{del}}[]
773 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
776 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
785 \item \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}} defines a named simplification
786 procedure that is invoked by the Simplifier whenever any of the
787 given term patterns match the current redex. The implementation,
788 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
789 supposed to be some proven rewrite rule \isa{{\isaliteral{22}{\isachardoublequote}}r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} (or a
790 generalized version), or \verb|NONE| to indicate failure. The
791 \verb|simpset| argument holds the full context of the current
792 Simplifier invocation, including the actual Isar proof context. The
793 \verb|morphism| informs about the difference of the original
794 compilation context wrt.\ the one of the actual application later
795 on. The optional \hyperlink{keyword.identifier}{\mbox{\isa{\isakeyword{identifier}}}} specifies theorems that
796 represent the logical content of the abstract theory of this
799 Morphisms and identifiers are only relevant for simprocs that are
800 defined within a local target context, e.g.\ in a locale.
802 \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}}}
803 add or delete named simprocs to the current Simplifier context. The
804 default is to add a simproc. Note that \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}
805 already adds the new simproc to the subsequent context.
811 \isamarkupsubsection{Forward simplification%
815 \begin{isamarkuptext}%
816 \begin{matharray}{rcl}
817 \indexdef{}{attribute}{simplified}\hypertarget{attribute.simplified}{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}} & : & \isa{attribute} \\
822 \rail@term{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}}[]
825 \rail@nont{\isa{opt}}[]
829 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
832 \rail@begin{3}{\isa{opt}}
833 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
835 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm}}[]
837 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp}}[]
839 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use}}[]
841 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
848 \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
849 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.
850 The result is fully simplified by default, including assumptions and
851 conclusion; the options \isa{no{\isaliteral{5F}{\isacharunderscore}}asm} etc.\ tune the Simplifier in
852 the same way as the for the \isa{simp} method.
854 Note that forward simplification restricts the simplifier to its
855 most basic operation of term rewriting; solver and looper tactics
856 \cite{isabelle-ref} are \emph{not} involved here. The \isa{simplified} attribute should be only rarely required under normal
863 \isamarkupsection{The Classical Reasoner \label{sec:classical}%
867 \isamarkupsubsection{Basic methods%
871 \begin{isamarkuptext}%
872 \begin{matharray}{rcl}
873 \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
874 \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
875 \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
876 \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
882 \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
884 \rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
886 \rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
890 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
898 \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
899 refinement over the primitive one (see \secref{sec:pure-meth-att}).
900 Both versions essentially work the same, but the classical version
901 observes the classical rule context in addition to that of
904 Common object logics (HOL, ZF, etc.) declare a rich collection of
905 classical rules (even if these would qualify as intuitionistic
906 ones), but only few declarations to the rule context of
907 Isabelle/Pure (\secref{sec:pure-meth-att}).
909 \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
910 deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
911 facts, which are guaranteed to participate, may appear in either
914 \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
915 by intro- or elim-resolution, after having inserted any chained
916 facts. Exactly the rules given as arguments are taken into account;
917 this allows fine-tuned decomposition of a proof problem, in contrast
918 to common automated tools.
924 \isamarkupsubsection{Automated methods%
928 \begin{isamarkuptext}%
929 \begin{matharray}{rcl}
930 \indexdef{}{method}{blast}\hypertarget{method.blast}{\hyperlink{method.blast}{\mbox{\isa{blast}}}} & : & \isa{method} \\
931 \indexdef{}{method}{fast}\hypertarget{method.fast}{\hyperlink{method.fast}{\mbox{\isa{fast}}}} & : & \isa{method} \\
932 \indexdef{}{method}{slow}\hypertarget{method.slow}{\hyperlink{method.slow}{\mbox{\isa{slow}}}} & : & \isa{method} \\
933 \indexdef{}{method}{best}\hypertarget{method.best}{\hyperlink{method.best}{\mbox{\isa{best}}}} & : & \isa{method} \\
934 \indexdef{}{method}{safe}\hypertarget{method.safe}{\hyperlink{method.safe}{\mbox{\isa{safe}}}} & : & \isa{method} \\
935 \indexdef{}{method}{clarify}\hypertarget{method.clarify}{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}} & : & \isa{method} \\
940 \rail@term{\hyperlink{method.blast}{\mbox{\isa{blast}}}}[]
943 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
947 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
952 \rail@term{\hyperlink{method.fast}{\mbox{\isa{fast}}}}[]
954 \rail@term{\hyperlink{method.slow}{\mbox{\isa{slow}}}}[]
956 \rail@term{\hyperlink{method.best}{\mbox{\isa{best}}}}[]
958 \rail@term{\hyperlink{method.safe}{\mbox{\isa{safe}}}}[]
960 \rail@term{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}}[]
964 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
967 \rail@begin{4}{\indexdef{}{syntax}{clamod}\hypertarget{syntax.clamod}{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}}
970 \rail@term{\isa{intro}}[]
972 \rail@term{\isa{elim}}[]
974 \rail@term{\isa{dest}}[]
977 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
980 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
983 \rail@term{\isa{del}}[]
985 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
986 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
993 \item \hyperlink{method.blast}{\mbox{\isa{blast}}} refers to the classical tableau prover (see
994 \verb|blast_tac| in \cite{isabelle-ref}). The optional argument
995 specifies a user-supplied search bound (default 20).
997 \item \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, \hyperlink{method.safe}{\mbox{\isa{safe}}}, and \hyperlink{method.clarify}{\mbox{\isa{clarify}}} refer to the generic classical
998 reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite{isabelle-ref} for more
1003 Any of the above methods support additional modifiers of the context
1004 of classical rules. Their semantics is analogous to the attributes
1005 given before. Facts provided by forward chaining are inserted into
1006 the goal before commencing proof search.%
1007 \end{isamarkuptext}%
1010 \isamarkupsubsection{Combined automated methods \label{sec:clasimp}%
1014 \begin{isamarkuptext}%
1015 \begin{matharray}{rcl}
1016 \indexdef{}{method}{auto}\hypertarget{method.auto}{\hyperlink{method.auto}{\mbox{\isa{auto}}}} & : & \isa{method} \\
1017 \indexdef{}{method}{force}\hypertarget{method.force}{\hyperlink{method.force}{\mbox{\isa{force}}}} & : & \isa{method} \\
1018 \indexdef{}{method}{clarsimp}\hypertarget{method.clarsimp}{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}} & : & \isa{method} \\
1019 \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
1020 \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
1021 \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
1026 \rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[]
1029 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1030 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1034 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1039 \rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[]
1041 \rail@term{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}}[]
1043 \rail@term{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}}[]
1045 \rail@term{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}}[]
1047 \rail@term{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}}[]
1051 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1054 \rail@begin{14}{\indexdef{}{syntax}{clasimpmod}\hypertarget{syntax.clasimpmod}{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}}
1056 \rail@term{\isa{simp}}[]
1059 \rail@term{\isa{add}}[]
1061 \rail@term{\isa{del}}[]
1063 \rail@term{\isa{only}}[]
1067 \rail@term{\isa{cong}}[]
1069 \rail@term{\isa{split}}[]
1073 \rail@term{\isa{add}}[]
1075 \rail@term{\isa{del}}[]
1078 \rail@term{\isa{iff}}[]
1082 \rail@term{\isa{add}}[]
1086 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1089 \rail@term{\isa{del}}[]
1094 \rail@term{\isa{intro}}[]
1096 \rail@term{\isa{elim}}[]
1098 \rail@term{\isa{dest}}[]
1101 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
1104 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1107 \rail@term{\isa{del}}[]
1110 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1111 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1118 \item \hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.force}{\mbox{\isa{force}}}, \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}, \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, and \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} provide access
1119 to Isabelle's combined simplification and classical reasoning
1120 tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
1121 added as wrapper, see \cite{isabelle-ref} for more information. The
1122 modifier arguments correspond to those given in
1123 \secref{sec:simplifier} and \secref{sec:classical}. Just note that
1124 the ones related to the Simplifier are prefixed by \isa{simp}
1127 Facts provided by forward chaining are inserted into the goal before
1131 \end{isamarkuptext}%
1134 \isamarkupsubsection{Declaring rules%
1138 \begin{isamarkuptext}%
1139 \begin{matharray}{rcl}
1140 \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}}} \\
1141 \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
1142 \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
1143 \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
1144 \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\
1145 \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\
1151 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
1153 \rail@term{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}}[]
1155 \rail@term{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}}[]
1158 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
1161 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1165 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1169 \rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
1170 \rail@term{\isa{del}}[]
1173 \rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[]
1177 \rail@term{\isa{add}}[]
1181 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
1184 \rail@term{\isa{del}}[]
1192 \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}} prints the collection of rules
1193 declared to the Classical Reasoner, which is also known as
1194 ``claset'' internally \cite{isabelle-ref}.
1196 \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}}
1197 declare introduction, elimination, and destruction rules,
1198 respectively. By default, rules are considered as \emph{unsafe}
1199 (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
1200 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' coincide with those of Isabelle/Pure, cf.\
1201 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
1202 of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number
1203 specifies an explicit weight argument, which is ignored by automated
1204 tools, but determines the search order of single rule steps.
1206 \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes introduction,
1207 elimination, or destruction rules from the context.
1209 \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the
1210 Simplifier and the Classical reasoner at the same time.
1211 Non-conditional rules result in a ``safe'' introduction and
1212 elimination pair; conditional ones are considered ``unsafe''. Rules
1213 with negative conclusion are automatically inverted (using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{22}{\isachardoublequote}}}-elimination internally).
1215 The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to
1216 the Isabelle/Pure context only, and omits the Simplifier
1220 \end{isamarkuptext}%
1223 \isamarkupsubsection{Classical operations%
1227 \begin{isamarkuptext}%
1228 \begin{matharray}{rcl}
1229 \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\
1234 \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an
1235 elimination, by resolving with the classical swap principle \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
1238 \end{isamarkuptext}%
1241 \isamarkupsection{Object-logic setup \label{sec:object-logic}%
1245 \begin{isamarkuptext}%
1246 \begin{matharray}{rcl}
1247 \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}}} \\
1248 \indexdef{}{method}{atomize}\hypertarget{method.atomize}{\hyperlink{method.atomize}{\mbox{\isa{atomize}}}} & : & \isa{method} \\
1249 \indexdef{}{attribute}{atomize}\hypertarget{attribute.atomize}{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}} & : & \isa{attribute} \\
1250 \indexdef{}{attribute}{rule\_format}\hypertarget{attribute.rule-format}{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}} & : & \isa{attribute} \\
1251 \indexdef{}{attribute}{rulify}\hypertarget{attribute.rulify}{\hyperlink{attribute.rulify}{\mbox{\isa{rulify}}}} & : & \isa{attribute} \\
1254 The very starting point for any Isabelle object-logic is a ``truth
1255 judgment'' that links object-level statements to the meta-logic
1256 (with its minimal language of \isa{prop} that covers universal
1257 quantification \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and implication \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}}).
1259 Common object-logics are sufficiently expressive to internalize rule
1260 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
1261 language. This is useful in certain situations where a rule needs
1262 to be viewed as an atomic statement from the meta-level perspective,
1263 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}}}.
1265 From the following language elements, only the \hyperlink{method.atomize}{\mbox{\isa{atomize}}}
1266 method and \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}} attribute are occasionally
1267 required by end-users, the rest is for those who need to setup their
1268 own object-logic. In the latter case existing formulations of
1269 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
1271 Generic tools may refer to the information provided by object-logic
1272 declarations internally.
1276 \rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
1277 \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
1280 \rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
1283 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1284 \rail@term{\isa{full}}[]
1285 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1289 \rail@term{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1292 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1293 \rail@term{\isa{noasm}}[]
1294 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1302 \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
1303 \isa{c} as the truth judgment of the current object-logic. Its
1304 type \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}} should specify a coercion of the category of
1305 object-level propositions to \isa{prop} of the Pure meta-logic;
1306 the mixfix annotation \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} would typically just link the
1307 object language (internally of syntactic category \isa{logic})
1308 with that of \isa{prop}. Only one \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}
1309 declaration may be given in any theory development.
1311 \item \hyperlink{method.atomize}{\mbox{\isa{atomize}}} (as a method) rewrites any non-atomic
1312 premises of a sub-goal, using the meta-level equations declared via
1313 \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} (as an attribute) beforehand. As a result,
1314 heavily nested goals become amenable to fundamental operations such
1315 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
1316 object-statement (if possible), including the outermost parameters
1317 and assumptions as well.
1319 A typical collection of \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} rules for a particular
1320 object-logic would provide an internalization for each of the
1321 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}}}.
1322 Meta-level conjunction should be covered as well (this is
1323 particularly important for locales, see \secref{sec:locale}).
1325 \item \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}} rewrites a theorem by the equalities
1326 declared as \hyperlink{attribute.rulify}{\mbox{\isa{rulify}}} rules in the current object-logic.
1327 By default, the result is fully normalized, including assumptions
1328 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
1329 restricts the transformation to the conclusion of a rule.
1331 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
1332 (\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
1333 rule statements over \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}}.
1336 \end{isamarkuptext}%
1344 \isacommand{end}\isamarkupfalse%
1354 %%% Local Variables:
1356 %%% TeX-master: "root"