3 \def\isabellecontext{Generic}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Main\isanewline
21 \isamarkupchapter{Generic tools and packages \label{ch:gen-tools}%
25 \isamarkupsection{Configuration options%
29 \begin{isamarkuptext}%
30 Isabelle/Pure maintains a record of named configuration options
31 within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|. Tools may declare
32 options in ML, and then refer to these values (relative to the
33 context). Thus global reference variables are easily avoided. The
34 user may change the value of a configuration option by means of an
35 associated attribute of the same name. This form of context
36 declaration works particularly well with commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
38 For historical reasons, some tools cannot take the full proof
39 context into account and merely refer to the background theory.
40 This is accommodated by configuration options being declared as
41 ``global'', which may not be changed within a local context.
43 \begin{matharray}{rcll}
44 \indexdef{}{command}{print\_configs}\hypertarget{command.print-configs}{\hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
48 name ('=' ('true' | 'false' | int | name))?
53 \item \hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}} prints the available configuration
54 options, with names, types, and current values.
56 \item \isa{{\isachardoublequote}name\ {\isacharequal}\ value{\isachardoublequote}} as an attribute expression modifies the
57 named option, with the syntax of the value depending on the option's
58 type. For \verb|bool| the default value is \isa{true}. Any
59 attempt to change a global option in a local context is ignored.
65 \isamarkupsection{Basic proof tools%
69 \isamarkupsubsection{Miscellaneous methods and attributes \label{sec:misc-meth-att}%
73 \begin{isamarkuptext}%
74 \begin{matharray}{rcl}
75 \indexdef{}{method}{unfold}\hypertarget{method.unfold}{\hyperlink{method.unfold}{\mbox{\isa{unfold}}}} & : & \isa{method} \\
76 \indexdef{}{method}{fold}\hypertarget{method.fold}{\hyperlink{method.fold}{\mbox{\isa{fold}}}} & : & \isa{method} \\
77 \indexdef{}{method}{insert}\hypertarget{method.insert}{\hyperlink{method.insert}{\mbox{\isa{insert}}}} & : & \isa{method} \\[0.5ex]
78 \indexdef{}{method}{erule}\hypertarget{method.erule}{\hyperlink{method.erule}{\mbox{\isa{erule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
79 \indexdef{}{method}{drule}\hypertarget{method.drule}{\hyperlink{method.drule}{\mbox{\isa{drule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
80 \indexdef{}{method}{frule}\hypertarget{method.frule}{\hyperlink{method.frule}{\mbox{\isa{frule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
81 \indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
82 \indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
86 ('fold' | 'unfold' | 'insert') thmrefs
88 ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
94 \item \hyperlink{method.unfold}{\mbox{\isa{unfold}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{method.fold}{\mbox{\isa{fold}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} expand (or fold back) the given definitions throughout
95 all goals; any chained facts provided are inserted into the goal and
96 subject to rewriting as well.
98 \item \hyperlink{method.insert}{\mbox{\isa{insert}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} inserts theorems as facts
99 into all goals of the proof state. Note that current facts
100 indicated for forward chaining are ignored.
102 \item \hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} are similar to the basic \hyperlink{method.rule}{\mbox{\isa{rule}}}
103 method (see \secref{sec:pure-meth-att}), but apply rules by
104 elim-resolution, destruct-resolution, and forward-resolution,
105 respectively \cite{isabelle-implementation}. The optional natural
106 number argument (default 0) specifies additional assumption steps to
109 Note that these methods are improper ones, mainly serving for
110 experimentation and tactic script emulation. Different modes of
111 basic rule application are usually expressed in Isar at the proof
112 language level, rather than via implicit proof state manipulations.
113 For example, a proper single-step elimination would be done using
114 the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
117 \item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
118 the identity of the ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' method combinator (cf.\
119 \secref{sec:proof-meth}).
121 \item \hyperlink{method.fail}{\mbox{\isa{fail}}} yields an empty result sequence; it is the
122 identity of the ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' method combinator (cf.\
123 \secref{sec:proof-meth}).
127 \begin{matharray}{rcl}
128 \indexdef{}{attribute}{tagged}\hypertarget{attribute.tagged}{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}} & : & \isa{attribute} \\
129 \indexdef{}{attribute}{untagged}\hypertarget{attribute.untagged}{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}} & : & \isa{attribute} \\[0.5ex]
130 \indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isa{attribute} \\
131 \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isa{attribute} \\[0.5ex]
132 \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isa{attribute} \\
133 \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\[0.5ex]
134 \indexdef{}{attribute}{rotated}\hypertarget{attribute.rotated}{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}} & : & \isa{attribute} \\
135 \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim-format}{\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}}} & : & \isa{attribute} \\
136 \indexdef{}{attribute}{standard}\hypertarget{attribute.standard}{\hyperlink{attribute.standard}{\mbox{\isa{standard}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\
137 \indexdef{}{attribute}{no\_vars}\hypertarget{attribute.no-vars}{\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\
145 ('THEN' | 'COMP') ('[' nat ']')? thmref
147 ('unfolded' | 'folded') thmrefs
154 \item \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}~\isa{{\isachardoublequote}name\ value{\isachardoublequote}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}~\isa{name} add and remove \emph{tags} of some theorem.
155 Tags may be any list of string pairs that serve as formal comment.
156 The first string is considered the tag name, the second its value.
157 Note that \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} removes any tags of the same name.
159 \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} and \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}~\isa{a}
160 compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
161 first premise of \isa{a} (an alternative position may be also
162 specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
163 lifting process that is normally intended (cf.\ \verb|op RS| and
164 \verb|op COMP| in \cite{isabelle-implementation}).
166 \item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} expand and fold back again the given
167 definitions throughout a rule.
169 \item \hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n} rotate the premises of a
170 theorem by \isa{n} (default 1).
172 \item \hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}} turns a destruction rule into
173 elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
175 Note that the Classical Reasoner (\secref{sec:classical}) provides
176 its own version of this operation.
178 \item \hyperlink{attribute.standard}{\mbox{\isa{standard}}} puts a theorem into the standard form of
179 object-rules at the outermost theory level. Note that this
180 operation violates the local proof context (including active
183 \item \hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} replaces schematic variables by free
184 ones; this is mainly for tuning output of pretty printed theorems.
190 \isamarkupsubsection{Low-level equational reasoning%
194 \begin{isamarkuptext}%
195 \begin{matharray}{rcl}
196 \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}} & : & \isa{method} \\
197 \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}} & : & \isa{method} \\
198 \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}} & : & \isa{method} \\
202 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
204 'split' ('(' 'asm' ')')? thmrefs
208 These methods provide low-level facilities for equational reasoning
209 that are intended for specialized applications only. Normally,
210 single step calculations would be performed in a structured text
211 (see also \secref{sec:calculation}), while the Simplifier methods
212 provide the canonical way for automated normalization (see
213 \secref{sec:simplifier}).
217 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq} performs a single substitution step
218 using rule \isa{eq}, which may be either a meta or object
221 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}} substitutes in an
224 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}} performs several
225 substitutions in the conclusion. The numbers \isa{i} to \isa{j}
226 indicate the positions to substitute at. Positions are ordered from
227 the top of the term tree moving down from left to right. For
228 example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions
229 where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}}, 2 to the whole term, and 3 to \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
231 If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping
232 (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may
233 assume all substitutions are performed simultaneously. Otherwise
234 the behaviour of \isa{subst} is not specified.
236 \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}} performs the
237 substitutions in the assumptions. The positions refer to the
238 assumptions in order from left to right. For example, given in a
239 goal of the form \isa{{\isachardoublequote}P\ {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}}, position 1 of
240 commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is the subterm \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}} and
241 position 2 is the subterm \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
243 \item \hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}} performs substitution using some
244 assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable.
246 \item \hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} performs single-step case
247 splitting using the given rules. By default, splitting is performed
248 in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to
249 operate on assumptions instead.
251 Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
252 application of split rules as declared in the current context.
258 \isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
262 \begin{isamarkuptext}%
263 The following improper proof methods emulate traditional tactics.
264 These admit direct access to the goal state, which is normally
265 considered harmful! In particular, this may involve both numbered
266 goal addressing (default 1), and dynamic instantiation within the
267 scope of some subgoal.
270 Dynamic instantiations refer to universally quantified parameters
271 of a subgoal (the dynamic context) rather than fixed variables and
272 term abbreviations of a (static) Isar context.
275 Tactic emulation methods, unlike their ML counterparts, admit
276 simultaneous instantiation from both dynamic and static contexts.
277 If names occur in both contexts goal parameters hide locally fixed
278 variables. Likewise, schematic variables refer to term
279 abbreviations, if present in the static context. Otherwise the
280 schematic variable is interpreted as a schematic variable and left
281 to be solved by unification with certain parts of the subgoal.
283 Note that the tactic emulation proof methods in Isabelle/Isar are
284 consistently named \isa{foo{\isacharunderscore}tac}. Note also that variable names
285 occurring on left hand sides of instantiations must be preceded by a
286 question mark if they coincide with a keyword or contain dots. This
287 is consistent with the attribute \hyperlink{attribute.where}{\mbox{\isa{where}}} (see
288 \secref{sec:pure-meth-att}).
290 \begin{matharray}{rcl}
291 \indexdef{}{method}{rule\_tac}\hypertarget{method.rule-tac}{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
292 \indexdef{}{method}{erule\_tac}\hypertarget{method.erule-tac}{\hyperlink{method.erule-tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
293 \indexdef{}{method}{drule\_tac}\hypertarget{method.drule-tac}{\hyperlink{method.drule-tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
294 \indexdef{}{method}{frule\_tac}\hypertarget{method.frule-tac}{\hyperlink{method.frule-tac}{\mbox{\isa{frule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
295 \indexdef{}{method}{cut\_tac}\hypertarget{method.cut-tac}{\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
296 \indexdef{}{method}{thin\_tac}\hypertarget{method.thin-tac}{\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
297 \indexdef{}{method}{subgoal\_tac}\hypertarget{method.subgoal-tac}{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
298 \indexdef{}{method}{rename\_tac}\hypertarget{method.rename-tac}{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
299 \indexdef{}{method}{rotate\_tac}\hypertarget{method.rotate-tac}{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
300 \indexdef{}{method}{tactic}\hypertarget{method.tactic}{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
301 \indexdef{}{method}{raw\_tactic}\hypertarget{method.raw-tactic}{\hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isacharunderscore}tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
305 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
306 ( insts thmref | thmrefs )
308 'subgoal\_tac' goalspec? (prop +)
310 'rename\_tac' goalspec? (name +)
312 'rotate\_tac' goalspec? int?
314 ('tactic' | 'raw_tactic') text
317 insts: ((name '=' term) + 'and') 'in'
323 \item \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc. do resolution of rules with explicit
324 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite{isabelle-implementation})
326 Multiple rules may be only given if there is no instantiation; then
327 \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
328 \cite{isabelle-implementation}).
330 \item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}} inserts facts into the proof state as
331 assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
332 \cite{isabelle-implementation}. Note that the scope of schematic
333 variables is spread over the main goal statement. Instantiations
334 may be given as well, see also ML tactic \verb|cut_inst_tac| in
335 \cite{isabelle-implementation}.
337 \item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}} deletes the specified assumption
338 from a subgoal; note that \isa{{\isasymphi}} may contain schematic variables.
339 See also \verb|thin_tac| in \cite{isabelle-implementation}.
341 \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}} adds \isa{{\isasymphi}} as an
342 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
344 \item \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} renames parameters of a
345 goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the
346 \emph{suffix} of variables.
348 \item \hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n} rotates the assumptions of a
349 goal by \isa{n} positions: from right to left if \isa{n} is
350 positive, and from left to right if \isa{n} is negative; the
351 default value is 1. See also \verb|rotate_tac| in
352 \cite{isabelle-implementation}.
354 \item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} produces a proof method from
355 any ML text of type \verb|tactic|. Apart from the usual ML
356 environment and the current proof context, the ML code may refer to
357 the locally bound values \verb|facts|, which indicates any
358 current facts used for forward-chaining.
360 \item \hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isacharunderscore}tactic}}} is similar to \hyperlink{method.tactic}{\mbox{\isa{tactic}}}, but
361 presents the goal state in its raw internal form, where simultaneous
362 subgoals appear as conjunction of the logical framework instead of
363 the usual split into several subgoals. While feature this is useful
364 for debugging of complex method definitions, it should not never
365 appear in production theories.
371 \isamarkupsection{The Simplifier \label{sec:simplifier}%
375 \isamarkupsubsection{Simplification methods%
379 \begin{isamarkuptext}%
380 \begin{matharray}{rcl}
381 \indexdef{}{method}{simp}\hypertarget{method.simp}{\hyperlink{method.simp}{\mbox{\isa{simp}}}} & : & \isa{method} \\
382 \indexdef{}{method}{simp\_all}\hypertarget{method.simp-all}{\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}} & : & \isa{method} \\
385 \indexouternonterm{simpmod}
387 ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
390 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
392 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
393 'split' (() | 'add' | 'del')) ':' thmrefs
399 \item \hyperlink{method.simp}{\mbox{\isa{simp}}} invokes the Simplifier, after declaring
400 additional rules according to the arguments given. Note that the
401 \railtterm{only} modifier first removes all other rewrite rules,
402 congruences, and looper tactics (including splits), and then behaves
403 like \railtterm{add}.
405 \medskip The \railtterm{cong} modifiers add or delete Simplifier
406 congruence rules (see also \cite{isabelle-ref}), the default is to
409 \medskip The \railtterm{split} modifiers add or delete rules for the
410 Splitter (see also \cite{isabelle-ref}), the default is to add.
411 This works only if the Simplifier method has been properly setup to
412 include the Splitter (all major object logics such HOL, HOLCF, FOL,
415 \item \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} is similar to \hyperlink{method.simp}{\mbox{\isa{simp}}}, but acts on
416 all goals (backwards from the last to the first one).
420 By default the Simplifier methods take local assumptions fully into
421 account, using equational assumptions in the subsequent
422 normalization process, or simplifying assumptions themselves (cf.\
423 \verb|asm_full_simp_tac| in \cite{isabelle-ref}). In structured
424 proofs this is usually quite well behaved in practice: just the
425 local premises of the actual goal are involved, additional facts may
426 be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
427 \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full context of
428 premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is
429 given, which should be used with some care, though.
431 Additional Simplifier options may be specified to tune the behavior
432 further (mostly for unstructured scripts with many accidental local
433 facts): ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}}'' means assumptions are ignored
434 completely (cf.\ \verb|simp_tac|), ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}}'' means
435 assumptions are used in the simplification of the conclusion but are
436 not themselves simplified (cf.\ \verb|asm_simp_tac|), and ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}}'' means assumptions are simplified but are not used
437 in the simplification of each other or the conclusion (cf.\ \verb|full_simp_tac|). For compatibility reasons, there is also an option
438 ``\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}}'', which means that an assumption is only used
439 for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
441 The configuration option \isa{{\isachardoublequote}depth{\isacharunderscore}limit{\isachardoublequote}} limits the number of
442 recursive invocations of the simplifier during conditional
445 \medskip The Splitter package is usually configured to work as part
446 of the Simplifier. The effect of repeatedly applying \verb|split_tac| can be simulated by ``\isa{{\isachardoublequote}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. There is also a separate \isa{split}
447 method available for single-step case splitting.%
451 \isamarkupsubsection{Declaring rules%
455 \begin{isamarkuptext}%
456 \begin{matharray}{rcl}
457 \indexdef{}{command}{print\_simpset}\hypertarget{command.print-simpset}{\hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
458 \indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isa{attribute} \\
459 \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
460 \indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isa{attribute} \\
464 ('simp' | 'cong' | 'split') (() | 'add' | 'del')
470 \item \hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}} prints the collection of rules
471 declared to the Simplifier, which is also known as ``simpset''
472 internally \cite{isabelle-ref}.
474 \item \hyperlink{attribute.simp}{\mbox{\isa{simp}}} declares simplification rules.
476 \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules.
478 \item \hyperlink{attribute.split}{\mbox{\isa{split}}} declares case split rules.
484 \isamarkupsubsection{Simplification procedures%
488 \begin{isamarkuptext}%
489 \begin{matharray}{rcl}
490 \indexdef{}{command}{simproc\_setup}\hypertarget{command.simproc-setup}{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
491 simproc & : & \isa{attribute} \\
495 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
498 'simproc' (('add' ':')? | 'del' ':') (name+)
504 \item \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}} defines a named simplification
505 procedure that is invoked by the Simplifier whenever any of the
506 given term patterns match the current redex. The implementation,
507 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
508 supposed to be some proven rewrite rule \isa{{\isachardoublequote}r\ {\isasymequiv}\ r{\isacharprime}{\isachardoublequote}} (or a
509 generalized version), or \verb|NONE| to indicate failure. The
510 \verb|simpset| argument holds the full context of the current
511 Simplifier invocation, including the actual Isar proof context. The
512 \verb|morphism| informs about the difference of the original
513 compilation context wrt.\ the one of the actual application later
514 on. The optional \hyperlink{keyword.identifier}{\mbox{\isa{\isakeyword{identifier}}}} specifies theorems that
515 represent the logical content of the abstract theory of this
518 Morphisms and identifiers are only relevant for simprocs that are
519 defined within a local target context, e.g.\ in a locale.
521 \item \isa{{\isachardoublequote}simproc\ add{\isacharcolon}\ name{\isachardoublequote}} and \isa{{\isachardoublequote}simproc\ del{\isacharcolon}\ name{\isachardoublequote}}
522 add or delete named simprocs to the current Simplifier context. The
523 default is to add a simproc. Note that \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}
524 already adds the new simproc to the subsequent context.
530 \isamarkupsubsection{Forward simplification%
534 \begin{isamarkuptext}%
535 \begin{matharray}{rcl}
536 \indexdef{}{attribute}{simplified}\hypertarget{attribute.simplified}{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}} & : & \isa{attribute} \\
540 'simplified' opt? thmrefs?
543 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
549 \item \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} causes a theorem to
550 be simplified, either by exactly the specified rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}, or the implicit Simplifier context if no arguments are given.
551 The result is fully simplified by default, including assumptions and
552 conclusion; the options \isa{no{\isacharunderscore}asm} etc.\ tune the Simplifier in
553 the same way as the for the \isa{simp} method.
555 Note that forward simplification restricts the simplifier to its
556 most basic operation of term rewriting; solver and looper tactics
557 \cite{isabelle-ref} are \emph{not} involved here. The \isa{simplified} attribute should be only rarely required under normal
564 \isamarkupsection{The Classical Reasoner \label{sec:classical}%
568 \isamarkupsubsection{Basic methods%
572 \begin{isamarkuptext}%
573 \begin{matharray}{rcl}
574 \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
575 \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
576 \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
577 \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
581 ('rule' | 'intro' | 'elim') thmrefs?
587 \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
588 refinement over the primitive one (see \secref{sec:pure-meth-att}).
589 Both versions essentially work the same, but the classical version
590 observes the classical rule context in addition to that of
593 Common object logics (HOL, ZF, etc.) declare a rich collection of
594 classical rules (even if these would qualify as intuitionistic
595 ones), but only few declarations to the rule context of
596 Isabelle/Pure (\secref{sec:pure-meth-att}).
598 \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
599 deriving any result from both \isa{{\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}} and \isa{A}. Chained
600 facts, which are guaranteed to participate, may appear in either
603 \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
604 by intro- or elim-resolution, after having inserted any chained
605 facts. Exactly the rules given as arguments are taken into account;
606 this allows fine-tuned decomposition of a proof problem, in contrast
607 to common automated tools.
613 \isamarkupsubsection{Automated methods%
617 \begin{isamarkuptext}%
618 \begin{matharray}{rcl}
619 \indexdef{}{method}{blast}\hypertarget{method.blast}{\hyperlink{method.blast}{\mbox{\isa{blast}}}} & : & \isa{method} \\
620 \indexdef{}{method}{fast}\hypertarget{method.fast}{\hyperlink{method.fast}{\mbox{\isa{fast}}}} & : & \isa{method} \\
621 \indexdef{}{method}{slow}\hypertarget{method.slow}{\hyperlink{method.slow}{\mbox{\isa{slow}}}} & : & \isa{method} \\
622 \indexdef{}{method}{best}\hypertarget{method.best}{\hyperlink{method.best}{\mbox{\isa{best}}}} & : & \isa{method} \\
623 \indexdef{}{method}{safe}\hypertarget{method.safe}{\hyperlink{method.safe}{\mbox{\isa{safe}}}} & : & \isa{method} \\
624 \indexdef{}{method}{clarify}\hypertarget{method.clarify}{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}} & : & \isa{method} \\
627 \indexouternonterm{clamod}
629 'blast' ('!' ?) nat? (clamod *)
631 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
634 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
640 \item \hyperlink{method.blast}{\mbox{\isa{blast}}} refers to the classical tableau prover (see
641 \verb|blast_tac| in \cite{isabelle-ref}). The optional argument
642 specifies a user-supplied search bound (default 20).
644 \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
645 reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite{isabelle-ref} for more
650 Any of the above methods support additional modifiers of the context
651 of classical rules. Their semantics is analogous to the attributes
652 given before. Facts provided by forward chaining are inserted into
653 the goal before commencing proof search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''~argument causes the full context of assumptions to be
658 \isamarkupsubsection{Combined automated methods \label{sec:clasimp}%
662 \begin{isamarkuptext}%
663 \begin{matharray}{rcl}
664 \indexdef{}{method}{auto}\hypertarget{method.auto}{\hyperlink{method.auto}{\mbox{\isa{auto}}}} & : & \isa{method} \\
665 \indexdef{}{method}{force}\hypertarget{method.force}{\hyperlink{method.force}{\mbox{\isa{force}}}} & : & \isa{method} \\
666 \indexdef{}{method}{clarsimp}\hypertarget{method.clarsimp}{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}} & : & \isa{method} \\
667 \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
668 \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
669 \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
672 \indexouternonterm{clasimpmod}
674 'auto' '!'? (nat nat)? (clasimpmod *)
676 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
679 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
680 ('cong' | 'split') (() | 'add' | 'del') |
681 'iff' (((() | 'add') '?'?) | 'del') |
682 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
687 \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
688 to Isabelle's combined simplification and classical reasoning
689 tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
690 added as wrapper, see \cite{isabelle-ref} for more information. The
691 modifier arguments correspond to those given in
692 \secref{sec:simplifier} and \secref{sec:classical}. Just note that
693 the ones related to the Simplifier are prefixed by \railtterm{simp}
696 Facts provided by forward chaining are inserted into the goal before
697 doing the search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' argument causes the full
698 context of assumptions to be included as well.
704 \isamarkupsubsection{Declaring rules%
708 \begin{isamarkuptext}%
709 \begin{matharray}{rcl}
710 \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
711 \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
712 \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
713 \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
714 \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\
715 \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\
719 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
723 'iff' (((() | 'add') '?'?) | 'del')
729 \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}} prints the collection of rules
730 declared to the Classical Reasoner, which is also known as
731 ``claset'' internally \cite{isabelle-ref}.
733 \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}}
734 declare introduction, elimination, and destruction rules,
735 respectively. By default, rules are considered as \emph{unsafe}
736 (i.e.\ not applied blindly without backtracking), while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' classifies as \emph{safe}. Rule declarations marked by
737 ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' coincide with those of Isabelle/Pure, cf.\
738 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
739 of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number
740 specifies an explicit weight argument, which is ignored by automated
741 tools, but determines the search order of single rule steps.
743 \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes introduction,
744 elimination, or destruction rules from the context.
746 \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the
747 Simplifier and the Classical reasoner at the same time.
748 Non-conditional rules result in a ``safe'' introduction and
749 elimination pair; conditional ones are considered ``unsafe''. Rules
750 with negative conclusion are automatically inverted (using \isa{{\isachardoublequote}{\isasymnot}{\isachardoublequote}}-elimination internally).
752 The ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to
753 the Isabelle/Pure context only, and omits the Simplifier
760 \isamarkupsubsection{Classical operations%
764 \begin{isamarkuptext}%
765 \begin{matharray}{rcl}
766 \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\
771 \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an
772 elimination, by resolving with the classical swap principle \isa{{\isachardoublequote}{\isacharparenleft}{\isasymnot}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ B{\isacharparenright}{\isachardoublequote}}.
778 \isamarkupsection{Object-logic setup \label{sec:object-logic}%
782 \begin{isamarkuptext}%
783 \begin{matharray}{rcl}
784 \indexdef{}{command}{judgment}\hypertarget{command.judgment}{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
785 \indexdef{}{method}{atomize}\hypertarget{method.atomize}{\hyperlink{method.atomize}{\mbox{\isa{atomize}}}} & : & \isa{method} \\
786 \indexdef{}{attribute}{atomize}\hypertarget{attribute.atomize}{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}} & : & \isa{attribute} \\
787 \indexdef{}{attribute}{rule\_format}\hypertarget{attribute.rule-format}{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}}} & : & \isa{attribute} \\
788 \indexdef{}{attribute}{rulify}\hypertarget{attribute.rulify}{\hyperlink{attribute.rulify}{\mbox{\isa{rulify}}}} & : & \isa{attribute} \\
791 The very starting point for any Isabelle object-logic is a ``truth
792 judgment'' that links object-level statements to the meta-logic
793 (with its minimal language of \isa{prop} that covers universal
794 quantification \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and implication \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}).
796 Common object-logics are sufficiently expressive to internalize rule
797 statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} within their own
798 language. This is useful in certain situations where a rule needs
799 to be viewed as an atomic statement from the meta-level perspective,
800 e.g.\ \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}} versus \isa{{\isachardoublequote}{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x{\isachardoublequote}}.
802 From the following language elements, only the \hyperlink{method.atomize}{\mbox{\isa{atomize}}}
803 method and \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} attribute are occasionally
804 required by end-users, the rest is for those who need to setup their
805 own object-logic. In the latter case existing formulations of
806 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
808 Generic tools may refer to the information provided by object-logic
809 declarations internally.
814 'atomize' ('(' 'full' ')')?
816 'rule\_format' ('(' 'noasm' ')')?
822 \item \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} declares constant
823 \isa{c} as the truth judgment of the current object-logic. Its
824 type \isa{{\isasymsigma}} should specify a coercion of the category of
825 object-level propositions to \isa{prop} of the Pure meta-logic;
826 the mixfix annotation \isa{{\isachardoublequote}{\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} would typically just link the
827 object language (internally of syntactic category \isa{logic})
828 with that of \isa{prop}. Only one \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}
829 declaration may be given in any theory development.
831 \item \hyperlink{method.atomize}{\mbox{\isa{atomize}}} (as a method) rewrites any non-atomic
832 premises of a sub-goal, using the meta-level equations declared via
833 \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} (as an attribute) beforehand. As a result,
834 heavily nested goals become amenable to fundamental operations such
835 as resolution (cf.\ the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). Giving the ``\isa{{\isachardoublequote}{\isacharparenleft}full{\isacharparenright}{\isachardoublequote}}'' option here means to turn the whole subgoal into an
836 object-statement (if possible), including the outermost parameters
837 and assumptions as well.
839 A typical collection of \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} rules for a particular
840 object-logic would provide an internalization for each of the
841 connectives of \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}}.
842 Meta-level conjunction should be covered as well (this is
843 particularly important for locales, see \secref{sec:locale}).
845 \item \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} rewrites a theorem by the equalities
846 declared as \hyperlink{attribute.rulify}{\mbox{\isa{rulify}}} rules in the current object-logic.
847 By default, the result is fully normalized, including assumptions
848 and conclusions at any depth. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} option
849 restricts the transformation to the conclusion of a rule.
851 In common object-logics (HOL, FOL, ZF), the effect of \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} is to replace (bounded) universal quantification
852 (\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}}) and implication (\isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}}) by the corresponding
853 rule statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}.
864 \isacommand{end}\isamarkupfalse%
876 %%% TeX-master: "root"