5 chapter {* Generic tools and packages \label{ch:gen-tools} *}
7 section {* Configuration options *}
9 text {* Isabelle/Pure maintains a record of named configuration
10 options within the theory or proof context, with values of type
11 @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
12 string}. Tools may declare options in ML, and then refer to these
13 values (relative to the context). Thus global reference variables
14 are easily avoided. The user may change the value of a
15 configuration option by means of an associated attribute of the same
16 name. This form of context declaration works particularly well with
17 commands such as @{command "declare"} or @{command "using"}.
19 For historical reasons, some tools cannot take the full proof
20 context into account and merely refer to the background theory.
21 This is accommodated by configuration options being declared as
22 ``global'', which may not be changed within a local context.
24 \begin{matharray}{rcll}
25 @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
29 @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
34 \item @{command "print_configs"} prints the available configuration
35 options, with names, types, and current values.
37 \item @{text "name = value"} as an attribute expression modifies the
38 named option, with the syntax of the value depending on the option's
39 type. For @{ML_type bool} the default value is @{text true}. Any
40 attempt to change a global option in a local context is ignored.
46 section {* Basic proof tools *}
48 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}
51 \begin{matharray}{rcl}
52 @{method_def unfold} & : & @{text method} \\
53 @{method_def fold} & : & @{text method} \\
54 @{method_def insert} & : & @{text method} \\[0.5ex]
55 @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
56 @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
57 @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
58 @{method_def succeed} & : & @{text method} \\
59 @{method_def fail} & : & @{text method} \\
63 (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
65 (@@{method erule} | @@{method drule} | @@{method frule})
66 ('(' @{syntax nat} ')')? @{syntax thmrefs}
71 \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
72 "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout
73 all goals; any chained facts provided are inserted into the goal and
74 subject to rewriting as well.
76 \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts
77 into all goals of the proof state. Note that current facts
78 indicated for forward chaining are ignored.
80 \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
81 drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
82 "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
83 method (see \secref{sec:pure-meth-att}), but apply rules by
84 elim-resolution, destruct-resolution, and forward-resolution,
85 respectively \cite{isabelle-implementation}. The optional natural
86 number argument (default 0) specifies additional assumption steps to
89 Note that these methods are improper ones, mainly serving for
90 experimentation and tactic script emulation. Different modes of
91 basic rule application are usually expressed in Isar at the proof
92 language level, rather than via implicit proof state manipulations.
93 For example, a proper single-step elimination would be done using
94 the plain @{method rule} method, with forward chaining of current
97 \item @{method succeed} yields a single (unchanged) result; it is
98 the identity of the ``@{text ","}'' method combinator (cf.\
99 \secref{sec:proof-meth}).
101 \item @{method fail} yields an empty result sequence; it is the
102 identity of the ``@{text "|"}'' method combinator (cf.\
103 \secref{sec:proof-meth}).
107 \begin{matharray}{rcl}
108 @{attribute_def tagged} & : & @{text attribute} \\
109 @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
110 @{attribute_def THEN} & : & @{text attribute} \\
111 @{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
112 @{attribute_def unfolded} & : & @{text attribute} \\
113 @{attribute_def folded} & : & @{text attribute} \\[0.5ex]
114 @{attribute_def rotated} & : & @{text attribute} \\
115 @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
116 @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
117 @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
121 @@{attribute tagged} @{syntax name} @{syntax name}
123 @@{attribute untagged} @{syntax name}
125 (@@{attribute THEN} | @@{attribute COMP}) ('[' @{syntax nat} ']')? @{syntax thmref}
127 (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
129 @@{attribute rotated} @{syntax int}?
134 \item @{attribute tagged}~@{text "name value"} and @{attribute
135 untagged}~@{text name} add and remove \emph{tags} of some theorem.
136 Tags may be any list of string pairs that serve as formal comment.
137 The first string is considered the tag name, the second its value.
138 Note that @{attribute untagged} removes any tags of the same name.
140 \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}
141 compose rules by resolution. @{attribute THEN} resolves with the
142 first premise of @{text a} (an alternative position may be also
143 specified); the @{attribute COMP} version skips the automatic
144 lifting process that is normally intended (cf.\ @{ML "op RS"} and
145 @{ML "op COMP"} in \cite{isabelle-implementation}).
147 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
148 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
149 definitions throughout a rule.
151 \item @{attribute rotated}~@{text n} rotate the premises of a
152 theorem by @{text n} (default 1).
154 \item @{attribute (Pure) elim_format} turns a destruction rule into
155 elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
156 (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
158 Note that the Classical Reasoner (\secref{sec:classical}) provides
159 its own version of this operation.
161 \item @{attribute standard} puts a theorem into the standard form of
162 object-rules at the outermost theory level. Note that this
163 operation violates the local proof context (including active
166 \item @{attribute no_vars} replaces schematic variables by free
167 ones; this is mainly for tuning output of pretty printed theorems.
173 subsection {* Low-level equational reasoning *}
176 \begin{matharray}{rcl}
177 @{method_def subst} & : & @{text method} \\
178 @{method_def hypsubst} & : & @{text method} \\
179 @{method_def split} & : & @{text method} \\
183 @@{method subst} ('(' 'asm' ')')? ('(' (@{syntax nat}+) ')')? @{syntax thmref}
185 @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
188 These methods provide low-level facilities for equational reasoning
189 that are intended for specialized applications only. Normally,
190 single step calculations would be performed in a structured text
191 (see also \secref{sec:calculation}), while the Simplifier methods
192 provide the canonical way for automated normalization (see
193 \secref{sec:simplifier}).
197 \item @{method subst}~@{text eq} performs a single substitution step
198 using rule @{text eq}, which may be either a meta or object
201 \item @{method subst}~@{text "(asm) eq"} substitutes in an
204 \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
205 substitutions in the conclusion. The numbers @{text i} to @{text j}
206 indicate the positions to substitute at. Positions are ordered from
207 the top of the term tree moving down from left to right. For
208 example, in @{text "(a + b) + (c + d)"} there are three positions
209 where commutativity of @{text "+"} is applicable: 1 refers to @{text
210 "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
212 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
213 (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
214 assume all substitutions are performed simultaneously. Otherwise
215 the behaviour of @{text subst} is not specified.
217 \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
218 substitutions in the assumptions. The positions refer to the
219 assumptions in order from left to right. For example, given in a
220 goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
221 commutativity of @{text "+"} is the subterm @{text "a + b"} and
222 position 2 is the subterm @{text "c + d"}.
224 \item @{method hypsubst} performs substitution using some
225 assumption; this only works for equations of the form @{text "x =
226 t"} where @{text x} is a free or bound variable.
228 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
229 splitting using the given rules. By default, splitting is performed
230 in the conclusion of a goal; the @{text "(asm)"} option indicates to
231 operate on assumptions instead.
233 Note that the @{method simp} method already involves repeated
234 application of split rules as declared in the current context.
240 subsection {* Further tactic emulations \label{sec:tactics} *}
243 The following improper proof methods emulate traditional tactics.
244 These admit direct access to the goal state, which is normally
245 considered harmful! In particular, this may involve both numbered
246 goal addressing (default 1), and dynamic instantiation within the
247 scope of some subgoal.
250 Dynamic instantiations refer to universally quantified parameters
251 of a subgoal (the dynamic context) rather than fixed variables and
252 term abbreviations of a (static) Isar context.
255 Tactic emulation methods, unlike their ML counterparts, admit
256 simultaneous instantiation from both dynamic and static contexts.
257 If names occur in both contexts goal parameters hide locally fixed
258 variables. Likewise, schematic variables refer to term
259 abbreviations, if present in the static context. Otherwise the
260 schematic variable is interpreted as a schematic variable and left
261 to be solved by unification with certain parts of the subgoal.
263 Note that the tactic emulation proof methods in Isabelle/Isar are
264 consistently named @{text foo_tac}. Note also that variable names
265 occurring on left hand sides of instantiations must be preceded by a
266 question mark if they coincide with a keyword or contain dots. This
267 is consistent with the attribute @{attribute "where"} (see
268 \secref{sec:pure-meth-att}).
270 \begin{matharray}{rcl}
271 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
272 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
273 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
274 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
275 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
276 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
277 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
278 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
279 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
280 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
281 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
285 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
286 @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}?
287 ( insts @{syntax thmref} | @{syntax thmrefs} )
289 @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
291 @@{method rename_tac} @{syntax goalspec}? (@{syntax name} +)
293 @@{method rotate_tac} @{syntax goalspec}? @{syntax int}?
295 (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
298 insts: ((@{syntax name} '=' @{syntax term}) + @'and') @'in'
299 "} % FIXME check use of insts
303 \item @{method rule_tac} etc. do resolution of rules with explicit
304 instantiation. This works the same way as the ML tactics @{ML
305 res_inst_tac} etc. (see \cite{isabelle-implementation})
307 Multiple rules may be only given if there is no instantiation; then
308 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
309 \cite{isabelle-implementation}).
311 \item @{method cut_tac} inserts facts into the proof state as
312 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
313 \cite{isabelle-implementation}. Note that the scope of schematic
314 variables is spread over the main goal statement. Instantiations
315 may be given as well, see also ML tactic @{ML cut_inst_tac} in
316 \cite{isabelle-implementation}.
318 \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
319 from a subgoal; note that @{text \<phi>} may contain schematic variables.
320 See also @{ML thin_tac} in \cite{isabelle-implementation}.
322 \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
323 assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
324 subgoals_tac} in \cite{isabelle-implementation}.
326 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
327 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
328 \emph{suffix} of variables.
330 \item @{method rotate_tac}~@{text n} rotates the assumptions of a
331 goal by @{text n} positions: from right to left if @{text n} is
332 positive, and from left to right if @{text n} is negative; the
333 default value is 1. See also @{ML rotate_tac} in
334 \cite{isabelle-implementation}.
336 \item @{method tactic}~@{text "text"} produces a proof method from
337 any ML text of type @{ML_type tactic}. Apart from the usual ML
338 environment and the current proof context, the ML code may refer to
339 the locally bound values @{ML_text facts}, which indicates any
340 current facts used for forward-chaining.
342 \item @{method raw_tactic} is similar to @{method tactic}, but
343 presents the goal state in its raw internal form, where simultaneous
344 subgoals appear as conjunction of the logical framework instead of
345 the usual split into several subgoals. While feature this is useful
346 for debugging of complex method definitions, it should not never
347 appear in production theories.
353 section {* The Simplifier \label{sec:simplifier} *}
355 subsection {* Simplification methods *}
358 \begin{matharray}{rcl}
359 @{method_def simp} & : & @{text method} \\
360 @{method_def simp_all} & : & @{text method} \\
364 (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
367 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
369 @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
370 'split' (() | 'add' | 'del')) ':' @{syntax thmrefs}
375 \item @{method simp} invokes the Simplifier, after declaring
376 additional rules according to the arguments given. Note that the
377 @{text only} modifier first removes all other rewrite rules,
378 congruences, and looper tactics (including splits), and then behaves
381 \medskip The @{text cong} modifiers add or delete Simplifier
382 congruence rules (see also \cite{isabelle-ref}), the default is to
385 \medskip The @{text split} modifiers add or delete rules for the
386 Splitter (see also \cite{isabelle-ref}), the default is to add.
387 This works only if the Simplifier method has been properly setup to
388 include the Splitter (all major object logics such HOL, HOLCF, FOL,
391 \item @{method simp_all} is similar to @{method simp}, but acts on
392 all goals (backwards from the last to the first one).
396 By default the Simplifier methods take local assumptions fully into
397 account, using equational assumptions in the subsequent
398 normalization process, or simplifying assumptions themselves (cf.\
399 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured
400 proofs this is usually quite well behaved in practice: just the
401 local premises of the actual goal are involved, additional facts may
402 be inserted via explicit forward-chaining (via @{command "then"},
403 @{command "from"}, @{command "using"} etc.).
405 Additional Simplifier options may be specified to tune the behavior
406 further (mostly for unstructured scripts with many accidental local
407 facts): ``@{text "(no_asm)"}'' means assumptions are ignored
408 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
409 assumptions are used in the simplification of the conclusion but are
410 not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
411 "(no_asm_use)"}'' means assumptions are simplified but are not used
412 in the simplification of each other or the conclusion (cf.\ @{ML
413 full_simp_tac}). For compatibility reasons, there is also an option
414 ``@{text "(asm_lr)"}'', which means that an assumption is only used
415 for simplifying assumptions which are to the right of it (cf.\ @{ML
418 The configuration option @{text "depth_limit"} limits the number of
419 recursive invocations of the simplifier during conditional
422 \medskip The Splitter package is usually configured to work as part
423 of the Simplifier. The effect of repeatedly applying @{ML
424 split_tac} can be simulated by ``@{text "(simp only: split:
425 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split}
426 method available for single-step case splitting.
430 subsection {* Declaring rules *}
433 \begin{matharray}{rcl}
434 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
435 @{attribute_def simp} & : & @{text attribute} \\
436 @{attribute_def cong} & : & @{text attribute} \\
437 @{attribute_def split} & : & @{text attribute} \\
441 (@@{attribute simp} | @@{attribute cong} | @@{attribute split}) (() | 'add' | 'del')
446 \item @{command "print_simpset"} prints the collection of rules
447 declared to the Simplifier, which is also known as ``simpset''
448 internally \cite{isabelle-ref}.
450 \item @{attribute simp} declares simplification rules.
452 \item @{attribute cong} declares congruence rules.
454 \item @{attribute split} declares case split rules.
460 subsection {* Simplification procedures *}
463 \begin{matharray}{rcl}
464 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
465 simproc & : & @{text attribute} \\
469 @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
470 @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?
473 @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
478 \item @{command "simproc_setup"} defines a named simplification
479 procedure that is invoked by the Simplifier whenever any of the
480 given term patterns match the current redex. The implementation,
481 which is provided as ML source text, needs to be of type @{ML_type
482 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
483 cterm} represents the current redex @{text r} and the result is
484 supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
485 generalized version), or @{ML NONE} to indicate failure. The
486 @{ML_type simpset} argument holds the full context of the current
487 Simplifier invocation, including the actual Isar proof context. The
488 @{ML_type morphism} informs about the difference of the original
489 compilation context wrt.\ the one of the actual application later
490 on. The optional @{keyword "identifier"} specifies theorems that
491 represent the logical content of the abstract theory of this
494 Morphisms and identifiers are only relevant for simprocs that are
495 defined within a local target context, e.g.\ in a locale.
497 \item @{text "simproc add: name"} and @{text "simproc del: name"}
498 add or delete named simprocs to the current Simplifier context. The
499 default is to add a simproc. Note that @{command "simproc_setup"}
500 already adds the new simproc to the subsequent context.
506 subsection {* Forward simplification *}
509 \begin{matharray}{rcl}
510 @{attribute_def simplified} & : & @{text attribute} \\
514 @@{attribute simplified} opt? @{syntax thmrefs}?
517 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
522 \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
523 be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
524 a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
525 The result is fully simplified by default, including assumptions and
526 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
527 the same way as the for the @{text simp} method.
529 Note that forward simplification restricts the simplifier to its
530 most basic operation of term rewriting; solver and looper tactics
531 \cite{isabelle-ref} are \emph{not} involved here. The @{text
532 simplified} attribute should be only rarely required under normal
539 section {* The Classical Reasoner \label{sec:classical} *}
541 subsection {* Basic methods *}
544 \begin{matharray}{rcl}
545 @{method_def rule} & : & @{text method} \\
546 @{method_def contradiction} & : & @{text method} \\
547 @{method_def intro} & : & @{text method} \\
548 @{method_def elim} & : & @{text method} \\
552 (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
557 \item @{method rule} as offered by the Classical Reasoner is a
558 refinement over the primitive one (see \secref{sec:pure-meth-att}).
559 Both versions essentially work the same, but the classical version
560 observes the classical rule context in addition to that of
563 Common object logics (HOL, ZF, etc.) declare a rich collection of
564 classical rules (even if these would qualify as intuitionistic
565 ones), but only few declarations to the rule context of
566 Isabelle/Pure (\secref{sec:pure-meth-att}).
568 \item @{method contradiction} solves some goal by contradiction,
569 deriving any result from both @{text "\<not> A"} and @{text A}. Chained
570 facts, which are guaranteed to participate, may appear in either
573 \item @{method intro} and @{method elim} repeatedly refine some goal
574 by intro- or elim-resolution, after having inserted any chained
575 facts. Exactly the rules given as arguments are taken into account;
576 this allows fine-tuned decomposition of a proof problem, in contrast
577 to common automated tools.
583 subsection {* Automated methods *}
586 \begin{matharray}{rcl}
587 @{method_def blast} & : & @{text method} \\
588 @{method_def fast} & : & @{text method} \\
589 @{method_def slow} & : & @{text method} \\
590 @{method_def best} & : & @{text method} \\
591 @{method_def safe} & : & @{text method} \\
592 @{method_def clarify} & : & @{text method} \\
596 @@{method blast} @{syntax nat}? (@{syntax clamod} * )
598 (@@{method fast} | @@{method slow} | @@{method best} | @@{method safe} | @@{method clarify})
599 (@{syntax clamod} * )
602 @{syntax_def clamod}:
603 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
608 \item @{method blast} refers to the classical tableau prover (see
609 @{ML blast_tac} in \cite{isabelle-ref}). The optional argument
610 specifies a user-supplied search bound (default 20).
612 \item @{method fast}, @{method slow}, @{method best}, @{method
613 safe}, and @{method clarify} refer to the generic classical
614 reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
615 safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
620 Any of the above methods support additional modifiers of the context
621 of classical rules. Their semantics is analogous to the attributes
622 given before. Facts provided by forward chaining are inserted into
623 the goal before commencing proof search.
627 subsection {* Combined automated methods \label{sec:clasimp} *}
630 \begin{matharray}{rcl}
631 @{method_def auto} & : & @{text method} \\
632 @{method_def force} & : & @{text method} \\
633 @{method_def clarsimp} & : & @{text method} \\
634 @{method_def fastsimp} & : & @{text method} \\
635 @{method_def slowsimp} & : & @{text method} \\
636 @{method_def bestsimp} & : & @{text method} \\
640 @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
642 (@@{method force} | @@{method clarsimp} | @@{method fastsimp} | @@{method slowsimp} |
643 @@{method bestsimp}) (@{syntax clasimpmod} * )
646 @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
647 ('cong' | 'split') (() | 'add' | 'del') |
648 'iff' (((() | 'add') '?'?) | 'del') |
649 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
654 \item @{method auto}, @{method force}, @{method clarsimp}, @{method
655 fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access
656 to Isabelle's combined simplification and classical reasoning
657 tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
658 clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
659 added as wrapper, see \cite{isabelle-ref} for more information. The
660 modifier arguments correspond to those given in
661 \secref{sec:simplifier} and \secref{sec:classical}. Just note that
662 the ones related to the Simplifier are prefixed by @{text simp}
665 Facts provided by forward chaining are inserted into the goal before
672 subsection {* Declaring rules *}
675 \begin{matharray}{rcl}
676 @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
677 @{attribute_def intro} & : & @{text attribute} \\
678 @{attribute_def elim} & : & @{text attribute} \\
679 @{attribute_def dest} & : & @{text attribute} \\
680 @{attribute_def rule} & : & @{text attribute} \\
681 @{attribute_def iff} & : & @{text attribute} \\
685 (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
687 @@{attribute rule} 'del'
689 @@{attribute iff} (((() | 'add') '?'?) | 'del')
694 \item @{command "print_claset"} prints the collection of rules
695 declared to the Classical Reasoner, which is also known as
696 ``claset'' internally \cite{isabelle-ref}.
698 \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
699 declare introduction, elimination, and destruction rules,
700 respectively. By default, rules are considered as \emph{unsafe}
701 (i.e.\ not applied blindly without backtracking), while ``@{text
702 "!"}'' classifies as \emph{safe}. Rule declarations marked by
703 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
704 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
705 of the @{method rule} method). The optional natural number
706 specifies an explicit weight argument, which is ignored by automated
707 tools, but determines the search order of single rule steps.
709 \item @{attribute rule}~@{text del} deletes introduction,
710 elimination, or destruction rules from the context.
712 \item @{attribute iff} declares logical equivalences to the
713 Simplifier and the Classical reasoner at the same time.
714 Non-conditional rules result in a ``safe'' introduction and
715 elimination pair; conditional ones are considered ``unsafe''. Rules
716 with negative conclusion are automatically inverted (using @{text
717 "\<not>"}-elimination internally).
719 The ``@{text "?"}'' version of @{attribute iff} declares rules to
720 the Isabelle/Pure context only, and omits the Simplifier
727 subsection {* Classical operations *}
730 \begin{matharray}{rcl}
731 @{attribute_def swapped} & : & @{text attribute} \\
736 \item @{attribute swapped} turns an introduction rule into an
737 elimination, by resolving with the classical swap principle @{text
738 "(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}.
744 section {* Object-logic setup \label{sec:object-logic} *}
747 \begin{matharray}{rcl}
748 @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
749 @{method_def atomize} & : & @{text method} \\
750 @{attribute_def atomize} & : & @{text attribute} \\
751 @{attribute_def rule_format} & : & @{text attribute} \\
752 @{attribute_def rulify} & : & @{text attribute} \\
755 The very starting point for any Isabelle object-logic is a ``truth
756 judgment'' that links object-level statements to the meta-logic
757 (with its minimal language of @{text prop} that covers universal
758 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
760 Common object-logics are sufficiently expressive to internalize rule
761 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
762 language. This is useful in certain situations where a rule needs
763 to be viewed as an atomic statement from the meta-level perspective,
764 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
766 From the following language elements, only the @{method atomize}
767 method and @{attribute rule_format} attribute are occasionally
768 required by end-users, the rest is for those who need to setup their
769 own object-logic. In the latter case existing formulations of
770 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
772 Generic tools may refer to the information provided by object-logic
773 declarations internally.
776 @@{command judgment} @{syntax constdecl}
778 @@{attribute atomize} ('(' 'full' ')')?
780 @@{attribute rule_format} ('(' 'noasm' ')')?
785 \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
786 @{text c} as the truth judgment of the current object-logic. Its
787 type @{text \<sigma>} should specify a coercion of the category of
788 object-level propositions to @{text prop} of the Pure meta-logic;
789 the mixfix annotation @{text "(mx)"} would typically just link the
790 object language (internally of syntactic category @{text logic})
791 with that of @{text prop}. Only one @{command "judgment"}
792 declaration may be given in any theory development.
794 \item @{method atomize} (as a method) rewrites any non-atomic
795 premises of a sub-goal, using the meta-level equations declared via
796 @{attribute atomize} (as an attribute) beforehand. As a result,
797 heavily nested goals become amenable to fundamental operations such
798 as resolution (cf.\ the @{method rule} method). Giving the ``@{text
799 "(full)"}'' option here means to turn the whole subgoal into an
800 object-statement (if possible), including the outermost parameters
801 and assumptions as well.
803 A typical collection of @{attribute atomize} rules for a particular
804 object-logic would provide an internalization for each of the
805 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
806 Meta-level conjunction should be covered as well (this is
807 particularly important for locales, see \secref{sec:locale}).
809 \item @{attribute rule_format} rewrites a theorem by the equalities
810 declared as @{attribute rulify} rules in the current object-logic.
811 By default, the result is fully normalized, including assumptions
812 and conclusions at any depth. The @{text "(no_asm)"} option
813 restricts the transformation to the conclusion of a rule.
815 In common object-logics (HOL, FOL, ZF), the effect of @{attribute
816 rule_format} is to replace (bounded) universal quantification
817 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
818 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.