7 chapter {* Generic tools and packages \label{ch:gen-tools} *}
9 section {* Configuration options *}
12 Isabelle/Pure maintains a record of named configuration options
13 within the theory or proof context, with values of type @{ML_type
14 bool}, @{ML_type int}, or @{ML_type string}. Tools may declare
15 options in ML, and then refer to these values (relative to the
16 context). Thus global reference variables are easily avoided. The
17 user may change the value of a configuration option by means of an
18 associated attribute of the same name. This form of context
19 declaration works particularly well with commands such as @{command
20 "declare"} or @{command "using"}.
22 For historical reasons, some tools cannot take the full proof
23 context into account and merely refer to the background theory.
24 This is accommodated by configuration options being declared as
25 ``global'', which may not be changed within a local context.
27 \begin{matharray}{rcll}
28 @{command_def "print_configs"} & : & \isarkeep{theory~|~proof} \\
32 name ('=' ('true' | 'false' | int | name))?
37 \item [@{command "print_configs"}] prints the available
38 configuration options, with names, types, and current values.
40 \item [@{text "name = value"}] as an attribute expression modifies
41 the named option, with the syntax of the value depending on the
42 option's type. For @{ML_type bool} the default value is @{text
43 true}. Any attempt to change a global option in a local context is
50 section {* Basic proof tools *}
52 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}
55 \begin{matharray}{rcl}
56 @{method_def unfold} & : & \isarmeth \\
57 @{method_def fold} & : & \isarmeth \\
58 @{method_def insert} & : & \isarmeth \\[0.5ex]
59 @{method_def erule}@{text "\<^sup>*"} & : & \isarmeth \\
60 @{method_def drule}@{text "\<^sup>*"} & : & \isarmeth \\
61 @{method_def frule}@{text "\<^sup>*"} & : & \isarmeth \\
62 @{method_def succeed} & : & \isarmeth \\
63 @{method_def fail} & : & \isarmeth \\
67 ('fold' | 'unfold' | 'insert') thmrefs
69 ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
75 \item [@{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method
76 fold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] expand (or fold back) the
77 given definitions throughout all goals; any chained facts provided
78 are inserted into the goal and subject to rewriting as well.
80 \item [@{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] inserts
81 theorems as facts into all goals of the proof state. Note that
82 current facts indicated for forward chaining are ignored.
84 \item [@{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
85 drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
86 "a\<^sub>1 \<dots> a\<^sub>n"}] are similar to the basic @{method rule}
87 method (see \secref{sec:pure-meth-att}), but apply rules by
88 elim-resolution, destruct-resolution, and forward-resolution,
89 respectively \cite{isabelle-ref}. The optional natural number
90 argument (default 0) specifies additional assumption steps to be
93 Note that these methods are improper ones, mainly serving for
94 experimentation and tactic script emulation. Different modes of
95 basic rule application are usually expressed in Isar at the proof
96 language level, rather than via implicit proof state manipulations.
97 For example, a proper single-step elimination would be done using
98 the plain @{method rule} method, with forward chaining of current
101 \item [@{method succeed}] yields a single (unchanged) result; it is
102 the identity of the ``@{text ","}'' method combinator (cf.\
103 \secref{sec:syn-meth}).
105 \item [@{method fail}] yields an empty result sequence; it is the
106 identity of the ``@{text "|"}'' method combinator (cf.\
107 \secref{sec:syn-meth}).
111 \begin{matharray}{rcl}
112 @{attribute_def tagged} & : & \isaratt \\
113 @{attribute_def untagged} & : & \isaratt \\[0.5ex]
114 @{attribute_def THEN} & : & \isaratt \\
115 @{attribute_def COMP} & : & \isaratt \\[0.5ex]
116 @{attribute_def unfolded} & : & \isaratt \\
117 @{attribute_def folded} & : & \isaratt \\[0.5ex]
118 @{attribute_def rotated} & : & \isaratt \\
119 @{attribute_def (Pure) elim_format} & : & \isaratt \\
120 @{attribute_def standard}@{text "\<^sup>*"} & : & \isaratt \\
121 @{attribute_def no_vars}@{text "\<^sup>*"} & : & \isaratt \\
129 ('THEN' | 'COMP') ('[' nat ']')? thmref
131 ('unfolded' | 'folded') thmrefs
138 \item [@{attribute tagged}~@{text "name arg"} and @{attribute
139 untagged}~@{text name}] add and remove \emph{tags} of some theorem.
140 Tags may be any list of string pairs that serve as formal comment.
141 The first string is considered the tag name, the second its
142 argument. Note that @{attribute untagged} removes any tags of the
145 \item [@{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}]
146 compose rules by resolution. @{attribute THEN} resolves with the
147 first premise of @{text a} (an alternative position may be also
148 specified); the @{attribute COMP} version skips the automatic
149 lifting process that is normally intended (cf.\ @{ML "op RS"} and
150 @{ML "op COMP"} in \cite[\S5]{isabelle-ref}).
152 \item [@{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and
153 @{attribute folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] expand and fold
154 back again the given definitions throughout a rule.
156 \item [@{attribute rotated}~@{text n}] rotate the premises of a
157 theorem by @{text n} (default 1).
159 \item [@{attribute (Pure) elim_format}] turns a destruction rule
160 into elimination rule format, by resolving with the rule @{prop
161 "PROP A \<Longrightarrow> (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
163 Note that the Classical Reasoner (\secref{sec:classical}) provides
164 its own version of this operation.
166 \item [@{attribute standard}] puts a theorem into the standard form
167 of object-rules at the outermost theory level. Note that this
168 operation violates the local proof context (including active
171 \item [@{attribute no_vars}] replaces schematic variables by free
172 ones; this is mainly for tuning output of pretty printed theorems.
178 subsection {* Low-level equational reasoning *}
181 \begin{matharray}{rcl}
182 @{method_def subst} & : & \isarmeth \\
183 @{method_def hypsubst} & : & \isarmeth \\
184 @{method_def split} & : & \isarmeth \\
188 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
190 'split' ('(' 'asm' ')')? thmrefs
194 These methods provide low-level facilities for equational reasoning
195 that are intended for specialized applications only. Normally,
196 single step calculations would be performed in a structured text
197 (see also \secref{sec:calculation}), while the Simplifier methods
198 provide the canonical way for automated normalization (see
199 \secref{sec:simplifier}).
203 \item [@{method subst}~@{text eq}] performs a single substitution
204 step using rule @{text eq}, which may be either a meta or object
207 \item [@{method subst}~@{text "(asm) eq"}] substitutes in an
210 \item [@{method subst}~@{text "(i \<dots> j) eq"}] performs several
211 substitutions in the conclusion. The numbers @{text i} to @{text j}
212 indicate the positions to substitute at. Positions are ordered from
213 the top of the term tree moving down from left to right. For
214 example, in @{text "(a + b) + (c + d)"} there are three positions
215 where commutativity of @{text "+"} is applicable: 1 refers to
216 @{text "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
218 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
219 (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
220 assume all substitutions are performed simultaneously. Otherwise
221 the behaviour of @{text subst} is not specified.
223 \item [@{method subst}~@{text "(asm) (i \<dots> j) eq"}] performs the
224 substitutions in the assumptions. The positions refer to the
225 assumptions in order from left to right. For example, given in a
226 goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
227 commutativity of @{text "+"} is the subterm @{text "a + b"} and
228 position 2 is the subterm @{text "c + d"}.
230 \item [@{method hypsubst}] performs substitution using some
231 assumption; this only works for equations of the form @{text "x =
232 t"} where @{text x} is a free or bound variable.
234 \item [@{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] performs
235 single-step case splitting using the given rules. By default,
236 splitting is performed in the conclusion of a goal; the @{text
237 "(asm)"} option indicates to operate on assumptions instead.
239 Note that the @{method simp} method already involves repeated
240 application of split rules as declared in the current context.
246 subsection {* Further tactic emulations \label{sec:tactics} *}
249 The following improper proof methods emulate traditional tactics.
250 These admit direct access to the goal state, which is normally
251 considered harmful! In particular, this may involve both numbered
252 goal addressing (default 1), and dynamic instantiation within the
253 scope of some subgoal.
256 Dynamic instantiations refer to universally quantified parameters
257 of a subgoal (the dynamic context) rather than fixed variables and
258 term abbreviations of a (static) Isar context.
261 Tactic emulation methods, unlike their ML counterparts, admit
262 simultaneous instantiation from both dynamic and static contexts.
263 If names occur in both contexts goal parameters hide locally fixed
264 variables. Likewise, schematic variables refer to term
265 abbreviations, if present in the static context. Otherwise the
266 schematic variable is interpreted as a schematic variable and left
267 to be solved by unification with certain parts of the subgoal.
269 Note that the tactic emulation proof methods in Isabelle/Isar are
270 consistently named @{text foo_tac}. Note also that variable names
271 occurring on left hand sides of instantiations must be preceded by a
272 question mark if they coincide with a keyword or contain dots. This
273 is consistent with the attribute @{attribute "where"} (see
274 \secref{sec:pure-meth-att}).
276 \begin{matharray}{rcl}
277 @{method_def rule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
278 @{method_def erule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
279 @{method_def drule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
280 @{method_def frule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
281 @{method_def cut_tac}@{text "\<^sup>*"} & : & \isarmeth \\
282 @{method_def thin_tac}@{text "\<^sup>*"} & : & \isarmeth \\
283 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & \isarmeth \\
284 @{method_def rename_tac}@{text "\<^sup>*"} & : & \isarmeth \\
285 @{method_def rotate_tac}@{text "\<^sup>*"} & : & \isarmeth \\
286 @{method_def tactic}@{text "\<^sup>*"} & : & \isarmeth \\
287 @{method_def raw_tactic}@{text "\<^sup>*"} & : & \isarmeth \\
291 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
292 ( insts thmref | thmrefs )
294 'subgoal\_tac' goalspec? (prop +)
296 'rename\_tac' goalspec? (name +)
298 'rotate\_tac' goalspec? int?
300 ('tactic' | 'raw_tactic') text
303 insts: ((name '=' term) + 'and') 'in'
309 \item [@{method rule_tac} etc.] do resolution of rules with explicit
310 instantiation. This works the same way as the ML tactics @{ML
311 res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
313 Multiple rules may be only given if there is no instantiation; then
314 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
315 \cite[\S3]{isabelle-ref}).
317 \item [@{method cut_tac}] inserts facts into the proof state as
318 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
319 \cite[\S3]{isabelle-ref}. Note that the scope of schematic
320 variables is spread over the main goal statement. Instantiations
321 may be given as well, see also ML tactic @{ML Tactic.cut_inst_tac}
322 in \cite[\S3]{isabelle-ref}.
324 \item [@{method thin_tac}~@{text \<phi>}] deletes the specified
325 assumption from a subgoal; note that @{text \<phi>} may contain schematic
326 variables. See also @{ML thin_tac} in
327 \cite[\S3]{isabelle-ref}.
329 \item [@{method subgoal_tac}~@{text \<phi>}] adds @{text \<phi>} as an
330 assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
331 subgoals_tac} in \cite[\S3]{isabelle-ref}.
333 \item [@{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"}] renames
334 parameters of a goal according to the list @{text "x\<^sub>1, \<dots>,
335 x\<^sub>n"}, which refers to the \emph{suffix} of variables.
337 \item [@{method rotate_tac}~@{text n}] rotates the assumptions of a
338 goal by @{text n} positions: from right to left if @{text n} is
339 positive, and from left to right if @{text n} is negative; the
340 default value is 1. See also @{ML rotate_tac} in
341 \cite[\S3]{isabelle-ref}.
343 \item [@{method tactic}~@{text "text"}] produces a proof method from
344 any ML text of type @{ML_type tactic}. Apart from the usual ML
345 environment and the current proof context, the ML code may refer to
346 the locally bound values @{ML_text facts}, which indicates any
347 current facts used for forward-chaining.
349 \item [@{method raw_tactic}] is similar to @{method tactic}, but
350 presents the goal state in its raw internal form, where simultaneous
351 subgoals appear as conjunction of the logical framework instead of
352 the usual split into several subgoals. While feature this is useful
353 for debugging of complex method definitions, it should not never
354 appear in production theories.
360 section {* The Simplifier \label{sec:simplifier} *}
362 subsection {* Simplification methods *}
365 \begin{matharray}{rcl}
366 @{method_def simp} & : & \isarmeth \\
367 @{method_def simp_all} & : & \isarmeth \\
370 \indexouternonterm{simpmod}
372 ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
375 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
377 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
378 'split' (() | 'add' | 'del')) ':' thmrefs
384 \item [@{method simp}] invokes the Simplifier, after declaring
385 additional rules according to the arguments given. Note that the
386 \railtterm{only} modifier first removes all other rewrite rules,
387 congruences, and looper tactics (including splits), and then behaves
388 like \railtterm{add}.
390 \medskip The \railtterm{cong} modifiers add or delete Simplifier
391 congruence rules (see also \cite{isabelle-ref}), the default is to
394 \medskip The \railtterm{split} modifiers add or delete rules for the
395 Splitter (see also \cite{isabelle-ref}), the default is to add.
396 This works only if the Simplifier method has been properly setup to
397 include the Splitter (all major object logics such HOL, HOLCF, FOL,
400 \item [@{method simp_all}] is similar to @{method simp}, but acts on
401 all goals (backwards from the last to the first one).
405 By default the Simplifier methods take local assumptions fully into
406 account, using equational assumptions in the subsequent
407 normalization process, or simplifying assumptions themselves (cf.\
408 @{ML asm_full_simp_tac} in \cite[\S10]{isabelle-ref}). In
409 structured proofs this is usually quite well behaved in practice:
410 just the local premises of the actual goal are involved, additional
411 facts may be inserted via explicit forward-chaining (via @{command
412 "then"}, @{command "from"}, @{command "using"} etc.). The full
413 context of premises is only included if the ``@{text "!"}'' (bang)
414 argument is given, which should be used with some care, though.
416 Additional Simplifier options may be specified to tune the behavior
417 further (mostly for unstructured scripts with many accidental local
418 facts): ``@{text "(no_asm)"}'' means assumptions are ignored
419 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
420 assumptions are used in the simplification of the conclusion but are
421 not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
422 "(no_asm_use)"}'' means assumptions are simplified but are not used
423 in the simplification of each other or the conclusion (cf.\ @{ML
424 full_simp_tac}). For compatibility reasons, there is also an option
425 ``@{text "(asm_lr)"}'', which means that an assumption is only used
426 for simplifying assumptions which are to the right of it (cf.\ @{ML
429 The configuration option @{text "depth_limit"} limits the number of
430 recursive invocations of the simplifier during conditional
433 \medskip The Splitter package is usually configured to work as part
434 of the Simplifier. The effect of repeatedly applying @{ML
435 split_tac} can be simulated by ``@{text "(simp only: split:
436 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split}
437 method available for single-step case splitting.
441 subsection {* Declaring rules *}
444 \begin{matharray}{rcl}
445 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
446 @{attribute_def simp} & : & \isaratt \\
447 @{attribute_def cong} & : & \isaratt \\
448 @{attribute_def split} & : & \isaratt \\
452 ('simp' | 'cong' | 'split') (() | 'add' | 'del')
458 \item [@{command "print_simpset"}] prints the collection of rules
459 declared to the Simplifier, which is also known as ``simpset''
460 internally \cite{isabelle-ref}.
462 \item [@{attribute simp}] declares simplification rules.
464 \item [@{attribute cong}] declares congruence rules.
466 \item [@{attribute split}] declares case split rules.
472 subsection {* Simplification procedures *}
475 \begin{matharray}{rcl}
476 @{command_def "simproc_setup"} & : & \isarkeep{local{\dsh}theory} \\
477 simproc & : & \isaratt \\
481 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
484 'simproc' (('add' ':')? | 'del' ':') (name+)
490 \item [@{command "simproc_setup"}] defines a named simplification
491 procedure that is invoked by the Simplifier whenever any of the
492 given term patterns match the current redex. The implementation,
493 which is provided as ML source text, needs to be of type @{ML_type
494 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
495 cterm} represents the current redex @{text r} and the result is
496 supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
497 generalized version), or @{ML NONE} to indicate failure. The
498 @{ML_type simpset} argument holds the full context of the current
499 Simplifier invocation, including the actual Isar proof context. The
500 @{ML_type morphism} informs about the difference of the original
501 compilation context wrt.\ the one of the actual application later
502 on. The optional @{keyword "identifier"} specifies theorems that
503 represent the logical content of the abstract theory of this
506 Morphisms and identifiers are only relevant for simprocs that are
507 defined within a local target context, e.g.\ in a locale.
509 \item [@{text "simproc add: name"} and @{text "simproc del: name"}]
510 add or delete named simprocs to the current Simplifier context. The
511 default is to add a simproc. Note that @{command "simproc_setup"}
512 already adds the new simproc to the subsequent context.
518 subsection {* Forward simplification *}
521 \begin{matharray}{rcl}
522 @{attribute_def simplified} & : & \isaratt \\
526 'simplified' opt? thmrefs?
529 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
535 \item [@{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
536 causes a theorem to be simplified, either by exactly the specified
537 rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}, or the implicit Simplifier
538 context if no arguments are given. The result is fully simplified
539 by default, including assumptions and conclusion; the options @{text
540 no_asm} etc.\ tune the Simplifier in the same way as the for the
543 Note that forward simplification restricts the simplifier to its
544 most basic operation of term rewriting; solver and looper tactics
545 \cite{isabelle-ref} are \emph{not} involved here. The @{text
546 simplified} attribute should be only rarely required under normal
553 section {* The Classical Reasoner \label{sec:classical} *}
555 subsection {* Basic methods *}
558 \begin{matharray}{rcl}
559 @{method_def rule} & : & \isarmeth \\
560 @{method_def contradiction} & : & \isarmeth \\
561 @{method_def intro} & : & \isarmeth \\
562 @{method_def elim} & : & \isarmeth \\
566 ('rule' | 'intro' | 'elim') thmrefs?
572 \item [@{method rule}] as offered by the Classical Reasoner is a
573 refinement over the primitive one (see \secref{sec:pure-meth-att}).
574 Both versions essentially work the same, but the classical version
575 observes the classical rule context in addition to that of
578 Common object logics (HOL, ZF, etc.) declare a rich collection of
579 classical rules (even if these would qualify as intuitionistic
580 ones), but only few declarations to the rule context of
581 Isabelle/Pure (\secref{sec:pure-meth-att}).
583 \item [@{method contradiction}] solves some goal by contradiction,
584 deriving any result from both @{text "\<not> A"} and @{text A}. Chained
585 facts, which are guaranteed to participate, may appear in either
588 \item [@{method intro} and @{method elim}] repeatedly refine some
589 goal by intro- or elim-resolution, after having inserted any chained
590 facts. Exactly the rules given as arguments are taken into account;
591 this allows fine-tuned decomposition of a proof problem, in contrast
592 to common automated tools.
598 subsection {* Automated methods *}
601 \begin{matharray}{rcl}
602 @{method_def blast} & : & \isarmeth \\
603 @{method_def fast} & : & \isarmeth \\
604 @{method_def slow} & : & \isarmeth \\
605 @{method_def best} & : & \isarmeth \\
606 @{method_def safe} & : & \isarmeth \\
607 @{method_def clarify} & : & \isarmeth \\
610 \indexouternonterm{clamod}
612 'blast' ('!' ?) nat? (clamod *)
614 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
617 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
623 \item [@{method blast}] refers to the classical tableau prover (see
624 @{ML blast_tac} in \cite[\S11]{isabelle-ref}). The optional
625 argument specifies a user-supplied search bound (default 20).
627 \item [@{method fast}, @{method slow}, @{method best}, @{method
628 safe}, and @{method clarify}] refer to the generic classical
629 reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
630 safe_tac}, and @{ML clarify_tac} in \cite[\S11]{isabelle-ref} for
635 Any of the above methods support additional modifiers of the context
636 of classical rules. Their semantics is analogous to the attributes
637 given before. Facts provided by forward chaining are inserted into
638 the goal before commencing proof search. The ``@{text
639 "!"}''~argument causes the full context of assumptions to be
644 subsection {* Combined automated methods \label{sec:clasimp} *}
647 \begin{matharray}{rcl}
648 @{method_def auto} & : & \isarmeth \\
649 @{method_def force} & : & \isarmeth \\
650 @{method_def clarsimp} & : & \isarmeth \\
651 @{method_def fastsimp} & : & \isarmeth \\
652 @{method_def slowsimp} & : & \isarmeth \\
653 @{method_def bestsimp} & : & \isarmeth \\
656 \indexouternonterm{clasimpmod}
658 'auto' '!'? (nat nat)? (clasimpmod *)
660 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
663 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
664 ('cong' | 'split') (() | 'add' | 'del') |
665 'iff' (((() | 'add') '?'?) | 'del') |
666 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
671 \item [@{method auto}, @{method force}, @{method clarsimp}, @{method
672 fastsimp}, @{method slowsimp}, and @{method bestsimp}] provide
673 access to Isabelle's combined simplification and classical reasoning
674 tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
675 clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
676 added as wrapper, see \cite[\S11]{isabelle-ref} for more
677 information. The modifier arguments correspond to those given in
678 \secref{sec:simplifier} and \secref{sec:classical}. Just note that
679 the ones related to the Simplifier are prefixed by \railtterm{simp}
682 Facts provided by forward chaining are inserted into the goal before
683 doing the search. The ``@{text "!"}'' argument causes the full
684 context of assumptions to be included as well.
690 subsection {* Declaring rules *}
693 \begin{matharray}{rcl}
694 @{command_def "print_claset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
695 @{attribute_def intro} & : & \isaratt \\
696 @{attribute_def elim} & : & \isaratt \\
697 @{attribute_def dest} & : & \isaratt \\
698 @{attribute_def rule} & : & \isaratt \\
699 @{attribute_def iff} & : & \isaratt \\
703 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
707 'iff' (((() | 'add') '?'?) | 'del')
713 \item [@{command "print_claset"}] prints the collection of rules
714 declared to the Classical Reasoner, which is also known as
715 ``claset'' internally \cite{isabelle-ref}.
717 \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
718 declare introduction, elimination, and destruction rules,
719 respectively. By default, rules are considered as \emph{unsafe}
720 (i.e.\ not applied blindly without backtracking), while ``@{text
721 "!"}'' classifies as \emph{safe}. Rule declarations marked by
722 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
723 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
724 of the @{method rule} method). The optional natural number
725 specifies an explicit weight argument, which is ignored by automated
726 tools, but determines the search order of single rule steps.
728 \item [@{attribute rule}~@{text del}] deletes introduction,
729 elimination, or destruction rules from the context.
731 \item [@{attribute iff}] declares logical equivalences to the
732 Simplifier and the Classical reasoner at the same time.
733 Non-conditional rules result in a ``safe'' introduction and
734 elimination pair; conditional ones are considered ``unsafe''. Rules
735 with negative conclusion are automatically inverted (using @{text
736 "\<not>"}-elimination internally).
738 The ``@{text "?"}'' version of @{attribute iff} declares rules to
739 the Isabelle/Pure context only, and omits the Simplifier
746 subsection {* Classical operations *}
749 \begin{matharray}{rcl}
750 @{attribute_def swapped} & : & \isaratt \\
755 \item [@{attribute swapped}] turns an introduction rule into an
756 elimination, by resolving with the classical swap principle @{text
757 "(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}.
763 section {* Object-logic setup \label{sec:object-logic} *}
766 \begin{matharray}{rcl}
767 @{command_def "judgment"} & : & \isartrans{theory}{theory} \\
768 @{method_def atomize} & : & \isarmeth \\
769 @{attribute_def atomize} & : & \isaratt \\
770 @{attribute_def rule_format} & : & \isaratt \\
771 @{attribute_def rulify} & : & \isaratt \\
774 The very starting point for any Isabelle object-logic is a ``truth
775 judgment'' that links object-level statements to the meta-logic
776 (with its minimal language of @{text prop} that covers universal
777 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
779 Common object-logics are sufficiently expressive to internalize rule
780 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
781 language. This is useful in certain situations where a rule needs
782 to be viewed as an atomic statement from the meta-level perspective,
783 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
785 From the following language elements, only the @{method atomize}
786 method and @{attribute rule_format} attribute are occasionally
787 required by end-users, the rest is for those who need to setup their
788 own object-logic. In the latter case existing formulations of
789 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
791 Generic tools may refer to the information provided by object-logic
792 declarations internally.
797 'atomize' ('(' 'full' ')')?
799 'rule\_format' ('(' 'noasm' ')')?
805 \item [@{command "judgment"}~@{text "c :: \<sigma> (mx)"}] declares
806 constant @{text c} as the truth judgment of the current
807 object-logic. Its type @{text \<sigma>} should specify a coercion of the
808 category of object-level propositions to @{text prop} of the Pure
809 meta-logic; the mixfix annotation @{text "(mx)"} would typically
810 just link the object language (internally of syntactic category
811 @{text logic}) with that of @{text prop}. Only one @{command
812 "judgment"} declaration may be given in any theory development.
814 \item [@{method atomize} (as a method)] rewrites any non-atomic
815 premises of a sub-goal, using the meta-level equations declared via
816 @{attribute atomize} (as an attribute) beforehand. As a result,
817 heavily nested goals become amenable to fundamental operations such
818 as resolution (cf.\ the @{method rule} method). Giving the ``@{text
819 "(full)"}'' option here means to turn the whole subgoal into an
820 object-statement (if possible), including the outermost parameters
821 and assumptions as well.
823 A typical collection of @{attribute atomize} rules for a particular
824 object-logic would provide an internalization for each of the
825 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
826 Meta-level conjunction should be covered as well (this is
827 particularly important for locales, see \secref{sec:locale}).
829 \item [@{attribute rule_format}] rewrites a theorem by the
830 equalities declared as @{attribute rulify} rules in the current
831 object-logic. By default, the result is fully normalized, including
832 assumptions and conclusions at any depth. The @{text "(no_asm)"}
833 option restricts the transformation to the conclusion of a rule.
835 In common object-logics (HOL, FOL, ZF), the effect of @{attribute
836 rule_format} is to replace (bounded) universal quantification
837 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
838 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.