5 chapter {* Generic tools and packages \label{ch:gen-tools} *}
7 section {* Configuration options *}
10 Isabelle/Pure maintains a record of named configuration options
11 within the theory or proof context, with values of type @{ML_type
12 bool}, @{ML_type int}, or @{ML_type string}. Tools may declare
13 options in ML, and then refer to these values (relative to the
14 context). Thus global reference variables are easily avoided. The
15 user may change the value of a configuration option by means of an
16 associated attribute of the same name. This form of context
17 declaration works particularly well with commands such as @{command
18 "declare"} or @{command "using"}.
20 For historical reasons, some tools cannot take the full proof
21 context into account and merely refer to the background theory.
22 This is accommodated by configuration options being declared as
23 ``global'', which may not be changed within a local context.
25 \begin{matharray}{rcll}
26 @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
30 name ('=' ('true' | 'false' | int | name))?
35 \item @{command "print_configs"} prints the available configuration
36 options, with names, types, and current values.
38 \item @{text "name = value"} as an attribute expression modifies the
39 named option, with the syntax of the value depending on the option's
40 type. For @{ML_type bool} the default value is @{text true}. Any
41 attempt to change a global option in a local context is ignored.
47 section {* Basic proof tools *}
49 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}
52 \begin{matharray}{rcl}
53 @{method_def unfold} & : & @{text method} \\
54 @{method_def fold} & : & @{text method} \\
55 @{method_def insert} & : & @{text method} \\[0.5ex]
56 @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
57 @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
58 @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
59 @{method_def succeed} & : & @{text method} \\
60 @{method_def fail} & : & @{text method} \\
64 ('fold' | 'unfold' | 'insert') thmrefs
66 ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
72 \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
73 "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout
74 all goals; any chained facts provided are inserted into the goal and
75 subject to rewriting as well.
77 \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts
78 into all goals of the proof state. Note that current facts
79 indicated for forward chaining are ignored.
81 \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
82 drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
83 "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
84 method (see \secref{sec:pure-meth-att}), but apply rules by
85 elim-resolution, destruct-resolution, and forward-resolution,
86 respectively \cite{isabelle-implementation}. The optional natural
87 number argument (default 0) specifies additional assumption steps to
90 Note that these methods are improper ones, mainly serving for
91 experimentation and tactic script emulation. Different modes of
92 basic rule application are usually expressed in Isar at the proof
93 language level, rather than via implicit proof state manipulations.
94 For example, a proper single-step elimination would be done using
95 the plain @{method rule} method, with forward chaining of current
98 \item @{method succeed} yields a single (unchanged) result; it is
99 the identity of the ``@{text ","}'' method combinator (cf.\
100 \secref{sec:proof-meth}).
102 \item @{method fail} yields an empty result sequence; it is the
103 identity of the ``@{text "|"}'' method combinator (cf.\
104 \secref{sec:proof-meth}).
108 \begin{matharray}{rcl}
109 @{attribute_def tagged} & : & @{text attribute} \\
110 @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
111 @{attribute_def THEN} & : & @{text attribute} \\
112 @{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
113 @{attribute_def unfolded} & : & @{text attribute} \\
114 @{attribute_def folded} & : & @{text attribute} \\[0.5ex]
115 @{attribute_def rotated} & : & @{text attribute} \\
116 @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
117 @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
118 @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
126 ('THEN' | 'COMP') ('[' nat ']')? thmref
128 ('unfolded' | 'folded') thmrefs
135 \item @{attribute tagged}~@{text "name value"} and @{attribute
136 untagged}~@{text name} add and remove \emph{tags} of some theorem.
137 Tags may be any list of string pairs that serve as formal comment.
138 The first string is considered the tag name, the second its value.
139 Note that @{attribute untagged} removes any tags of the same name.
141 \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}
142 compose rules by resolution. @{attribute THEN} resolves with the
143 first premise of @{text a} (an alternative position may be also
144 specified); the @{attribute COMP} version skips the automatic
145 lifting process that is normally intended (cf.\ @{ML [source=false]
146 "op RS"} and @{ML [source=false] "op COMP"} in
147 \cite{isabelle-implementation}).
149 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
150 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
151 definitions throughout a rule.
153 \item @{attribute rotated}~@{text n} rotate the premises of a
154 theorem by @{text n} (default 1).
156 \item @{attribute (Pure) elim_format} turns a destruction rule into
157 elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
158 (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
160 Note that the Classical Reasoner (\secref{sec:classical}) provides
161 its own version of this operation.
163 \item @{attribute standard} puts a theorem into the standard form of
164 object-rules at the outermost theory level. Note that this
165 operation violates the local proof context (including active
168 \item @{attribute no_vars} replaces schematic variables by free
169 ones; this is mainly for tuning output of pretty printed theorems.
175 subsection {* Low-level equational reasoning *}
178 \begin{matharray}{rcl}
179 @{method_def subst} & : & @{text method} \\
180 @{method_def hypsubst} & : & @{text method} \\
181 @{method_def split} & : & @{text method} \\
185 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
187 'split' ('(' 'asm' ')')? thmrefs
191 These methods provide low-level facilities for equational reasoning
192 that are intended for specialized applications only. Normally,
193 single step calculations would be performed in a structured text
194 (see also \secref{sec:calculation}), while the Simplifier methods
195 provide the canonical way for automated normalization (see
196 \secref{sec:simplifier}).
200 \item @{method subst}~@{text eq} performs a single substitution step
201 using rule @{text eq}, which may be either a meta or object
204 \item @{method subst}~@{text "(asm) eq"} substitutes in an
207 \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
208 substitutions in the conclusion. The numbers @{text i} to @{text j}
209 indicate the positions to substitute at. Positions are ordered from
210 the top of the term tree moving down from left to right. For
211 example, in @{text "(a + b) + (c + d)"} there are three positions
212 where commutativity of @{text "+"} is applicable: 1 refers to @{text
213 "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
215 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
216 (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
217 assume all substitutions are performed simultaneously. Otherwise
218 the behaviour of @{text subst} is not specified.
220 \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
221 substitutions in the assumptions. The positions refer to the
222 assumptions in order from left to right. For example, given in a
223 goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
224 commutativity of @{text "+"} is the subterm @{text "a + b"} and
225 position 2 is the subterm @{text "c + d"}.
227 \item @{method hypsubst} performs substitution using some
228 assumption; this only works for equations of the form @{text "x =
229 t"} where @{text x} is a free or bound variable.
231 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
232 splitting using the given rules. By default, splitting is performed
233 in the conclusion of a goal; the @{text "(asm)"} option indicates to
234 operate on assumptions instead.
236 Note that the @{method simp} method already involves repeated
237 application of split rules as declared in the current context.
243 subsection {* Further tactic emulations \label{sec:tactics} *}
246 The following improper proof methods emulate traditional tactics.
247 These admit direct access to the goal state, which is normally
248 considered harmful! In particular, this may involve both numbered
249 goal addressing (default 1), and dynamic instantiation within the
250 scope of some subgoal.
253 Dynamic instantiations refer to universally quantified parameters
254 of a subgoal (the dynamic context) rather than fixed variables and
255 term abbreviations of a (static) Isar context.
258 Tactic emulation methods, unlike their ML counterparts, admit
259 simultaneous instantiation from both dynamic and static contexts.
260 If names occur in both contexts goal parameters hide locally fixed
261 variables. Likewise, schematic variables refer to term
262 abbreviations, if present in the static context. Otherwise the
263 schematic variable is interpreted as a schematic variable and left
264 to be solved by unification with certain parts of the subgoal.
266 Note that the tactic emulation proof methods in Isabelle/Isar are
267 consistently named @{text foo_tac}. Note also that variable names
268 occurring on left hand sides of instantiations must be preceded by a
269 question mark if they coincide with a keyword or contain dots. This
270 is consistent with the attribute @{attribute "where"} (see
271 \secref{sec:pure-meth-att}).
273 \begin{matharray}{rcl}
274 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
275 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
276 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
277 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
278 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
279 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
280 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
281 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
282 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
283 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
284 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
288 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
289 ( insts thmref | thmrefs )
291 'subgoal\_tac' goalspec? (prop +)
293 'rename\_tac' goalspec? (name +)
295 'rotate\_tac' goalspec? int?
297 ('tactic' | 'raw_tactic') text
300 insts: ((name '=' term) + 'and') 'in'
306 \item @{method rule_tac} etc. do resolution of rules with explicit
307 instantiation. This works the same way as the ML tactics @{ML
308 res_inst_tac} etc. (see \cite{isabelle-implementation})
310 Multiple rules may be only given if there is no instantiation; then
311 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
312 \cite{isabelle-implementation}).
314 \item @{method cut_tac} inserts facts into the proof state as
315 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
316 \cite{isabelle-implementation}. Note that the scope of schematic
317 variables is spread over the main goal statement. Instantiations
318 may be given as well, see also ML tactic @{ML cut_inst_tac} in
319 \cite{isabelle-implementation}.
321 \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
322 from a subgoal; note that @{text \<phi>} may contain schematic variables.
323 See also @{ML thin_tac} in \cite{isabelle-implementation}.
325 \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
326 assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
327 subgoals_tac} in \cite{isabelle-implementation}.
329 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
330 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
331 \emph{suffix} of variables.
333 \item @{method rotate_tac}~@{text n} rotates the assumptions of a
334 goal by @{text n} positions: from right to left if @{text n} is
335 positive, and from left to right if @{text n} is negative; the
336 default value is 1. See also @{ML rotate_tac} in
337 \cite{isabelle-implementation}.
339 \item @{method tactic}~@{text "text"} produces a proof method from
340 any ML text of type @{ML_type tactic}. Apart from the usual ML
341 environment and the current proof context, the ML code may refer to
342 the locally bound values @{ML_text facts}, which indicates any
343 current facts used for forward-chaining.
345 \item @{method raw_tactic} is similar to @{method tactic}, but
346 presents the goal state in its raw internal form, where simultaneous
347 subgoals appear as conjunction of the logical framework instead of
348 the usual split into several subgoals. While feature this is useful
349 for debugging of complex method definitions, it should not never
350 appear in production theories.
356 section {* The Simplifier \label{sec:simplifier} *}
358 subsection {* Simplification methods *}
361 \begin{matharray}{rcl}
362 @{method_def simp} & : & @{text method} \\
363 @{method_def simp_all} & : & @{text method} \\
366 \indexouternonterm{simpmod}
368 ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
371 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
373 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
374 'split' (() | 'add' | 'del')) ':' thmrefs
380 \item @{method simp} invokes the Simplifier, after declaring
381 additional rules according to the arguments given. Note that the
382 \railtterm{only} modifier first removes all other rewrite rules,
383 congruences, and looper tactics (including splits), and then behaves
384 like \railtterm{add}.
386 \medskip The \railtterm{cong} modifiers add or delete Simplifier
387 congruence rules (see also \cite{isabelle-ref}), the default is to
390 \medskip The \railtterm{split} modifiers add or delete rules for the
391 Splitter (see also \cite{isabelle-ref}), the default is to add.
392 This works only if the Simplifier method has been properly setup to
393 include the Splitter (all major object logics such HOL, HOLCF, FOL,
396 \item @{method simp_all} is similar to @{method simp}, but acts on
397 all goals (backwards from the last to the first one).
401 By default the Simplifier methods take local assumptions fully into
402 account, using equational assumptions in the subsequent
403 normalization process, or simplifying assumptions themselves (cf.\
404 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured
405 proofs this is usually quite well behaved in practice: just the
406 local premises of the actual goal are involved, additional facts may
407 be inserted via explicit forward-chaining (via @{command "then"},
408 @{command "from"}, @{command "using"} etc.). The full context of
409 premises is only included if the ``@{text "!"}'' (bang) argument is
410 given, which should be used with some care, though.
412 Additional Simplifier options may be specified to tune the behavior
413 further (mostly for unstructured scripts with many accidental local
414 facts): ``@{text "(no_asm)"}'' means assumptions are ignored
415 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
416 assumptions are used in the simplification of the conclusion but are
417 not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
418 "(no_asm_use)"}'' means assumptions are simplified but are not used
419 in the simplification of each other or the conclusion (cf.\ @{ML
420 full_simp_tac}). For compatibility reasons, there is also an option
421 ``@{text "(asm_lr)"}'', which means that an assumption is only used
422 for simplifying assumptions which are to the right of it (cf.\ @{ML
425 The configuration option @{text "depth_limit"} limits the number of
426 recursive invocations of the simplifier during conditional
429 \medskip The Splitter package is usually configured to work as part
430 of the Simplifier. The effect of repeatedly applying @{ML
431 split_tac} can be simulated by ``@{text "(simp only: split:
432 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split}
433 method available for single-step case splitting.
437 subsection {* Declaring rules *}
440 \begin{matharray}{rcl}
441 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
442 @{attribute_def simp} & : & @{text attribute} \\
443 @{attribute_def cong} & : & @{text attribute} \\
444 @{attribute_def split} & : & @{text attribute} \\
448 ('simp' | 'cong' | 'split') (() | 'add' | 'del')
454 \item @{command "print_simpset"} prints the collection of rules
455 declared to the Simplifier, which is also known as ``simpset''
456 internally \cite{isabelle-ref}.
458 \item @{attribute simp} declares simplification rules.
460 \item @{attribute cong} declares congruence rules.
462 \item @{attribute split} declares case split rules.
468 subsection {* Simplification procedures *}
471 \begin{matharray}{rcl}
472 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
473 simproc & : & @{text attribute} \\
477 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
480 'simproc' (('add' ':')? | 'del' ':') (name+)
486 \item @{command "simproc_setup"} defines a named simplification
487 procedure that is invoked by the Simplifier whenever any of the
488 given term patterns match the current redex. The implementation,
489 which is provided as ML source text, needs to be of type @{ML_type
490 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
491 cterm} represents the current redex @{text r} and the result is
492 supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
493 generalized version), or @{ML NONE} to indicate failure. The
494 @{ML_type simpset} argument holds the full context of the current
495 Simplifier invocation, including the actual Isar proof context. The
496 @{ML_type morphism} informs about the difference of the original
497 compilation context wrt.\ the one of the actual application later
498 on. The optional @{keyword "identifier"} specifies theorems that
499 represent the logical content of the abstract theory of this
502 Morphisms and identifiers are only relevant for simprocs that are
503 defined within a local target context, e.g.\ in a locale.
505 \item @{text "simproc add: name"} and @{text "simproc del: name"}
506 add or delete named simprocs to the current Simplifier context. The
507 default is to add a simproc. Note that @{command "simproc_setup"}
508 already adds the new simproc to the subsequent context.
514 subsection {* Forward simplification *}
517 \begin{matharray}{rcl}
518 @{attribute_def simplified} & : & @{text attribute} \\
522 'simplified' opt? thmrefs?
525 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
531 \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
532 be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
533 a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
534 The result is fully simplified by default, including assumptions and
535 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
536 the same way as the for the @{text simp} method.
538 Note that forward simplification restricts the simplifier to its
539 most basic operation of term rewriting; solver and looper tactics
540 \cite{isabelle-ref} are \emph{not} involved here. The @{text
541 simplified} attribute should be only rarely required under normal
548 section {* The Classical Reasoner \label{sec:classical} *}
550 subsection {* Basic methods *}
553 \begin{matharray}{rcl}
554 @{method_def rule} & : & @{text method} \\
555 @{method_def contradiction} & : & @{text method} \\
556 @{method_def intro} & : & @{text method} \\
557 @{method_def elim} & : & @{text method} \\
561 ('rule' | 'intro' | 'elim') thmrefs?
567 \item @{method rule} as offered by the Classical Reasoner is a
568 refinement over the primitive one (see \secref{sec:pure-meth-att}).
569 Both versions essentially work the same, but the classical version
570 observes the classical rule context in addition to that of
573 Common object logics (HOL, ZF, etc.) declare a rich collection of
574 classical rules (even if these would qualify as intuitionistic
575 ones), but only few declarations to the rule context of
576 Isabelle/Pure (\secref{sec:pure-meth-att}).
578 \item @{method contradiction} solves some goal by contradiction,
579 deriving any result from both @{text "\<not> A"} and @{text A}. Chained
580 facts, which are guaranteed to participate, may appear in either
583 \item @{method intro} and @{method elim} repeatedly refine some goal
584 by intro- or elim-resolution, after having inserted any chained
585 facts. Exactly the rules given as arguments are taken into account;
586 this allows fine-tuned decomposition of a proof problem, in contrast
587 to common automated tools.
593 subsection {* Automated methods *}
596 \begin{matharray}{rcl}
597 @{method_def blast} & : & @{text method} \\
598 @{method_def fast} & : & @{text method} \\
599 @{method_def slow} & : & @{text method} \\
600 @{method_def best} & : & @{text method} \\
601 @{method_def safe} & : & @{text method} \\
602 @{method_def clarify} & : & @{text method} \\
605 \indexouternonterm{clamod}
607 'blast' ('!' ?) nat? (clamod *)
609 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
612 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
618 \item @{method blast} refers to the classical tableau prover (see
619 @{ML blast_tac} in \cite{isabelle-ref}). The optional argument
620 specifies a user-supplied search bound (default 20).
622 \item @{method fast}, @{method slow}, @{method best}, @{method
623 safe}, and @{method clarify} refer to the generic classical
624 reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
625 safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
630 Any of the above methods support additional modifiers of the context
631 of classical rules. Their semantics is analogous to the attributes
632 given before. Facts provided by forward chaining are inserted into
633 the goal before commencing proof search. The ``@{text
634 "!"}''~argument causes the full context of assumptions to be
639 subsection {* Combined automated methods \label{sec:clasimp} *}
642 \begin{matharray}{rcl}
643 @{method_def auto} & : & @{text method} \\
644 @{method_def force} & : & @{text method} \\
645 @{method_def clarsimp} & : & @{text method} \\
646 @{method_def fastsimp} & : & @{text method} \\
647 @{method_def slowsimp} & : & @{text method} \\
648 @{method_def bestsimp} & : & @{text method} \\
651 \indexouternonterm{clasimpmod}
653 'auto' '!'? (nat nat)? (clasimpmod *)
655 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
658 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
659 ('cong' | 'split') (() | 'add' | 'del') |
660 'iff' (((() | 'add') '?'?) | 'del') |
661 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
666 \item @{method auto}, @{method force}, @{method clarsimp}, @{method
667 fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access
668 to Isabelle's combined simplification and classical reasoning
669 tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
670 clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
671 added as wrapper, see \cite{isabelle-ref} for more information. The
672 modifier arguments correspond to those given in
673 \secref{sec:simplifier} and \secref{sec:classical}. Just note that
674 the ones related to the Simplifier are prefixed by \railtterm{simp}
677 Facts provided by forward chaining are inserted into the goal before
678 doing the search. The ``@{text "!"}'' argument causes the full
679 context of assumptions to be included as well.
685 subsection {* Declaring rules *}
688 \begin{matharray}{rcl}
689 @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
690 @{attribute_def intro} & : & @{text attribute} \\
691 @{attribute_def elim} & : & @{text attribute} \\
692 @{attribute_def dest} & : & @{text attribute} \\
693 @{attribute_def rule} & : & @{text attribute} \\
694 @{attribute_def iff} & : & @{text attribute} \\
698 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
702 'iff' (((() | 'add') '?'?) | 'del')
708 \item @{command "print_claset"} prints the collection of rules
709 declared to the Classical Reasoner, which is also known as
710 ``claset'' internally \cite{isabelle-ref}.
712 \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
713 declare introduction, elimination, and destruction rules,
714 respectively. By default, rules are considered as \emph{unsafe}
715 (i.e.\ not applied blindly without backtracking), while ``@{text
716 "!"}'' classifies as \emph{safe}. Rule declarations marked by
717 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
718 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
719 of the @{method rule} method). The optional natural number
720 specifies an explicit weight argument, which is ignored by automated
721 tools, but determines the search order of single rule steps.
723 \item @{attribute rule}~@{text del} deletes introduction,
724 elimination, or destruction rules from the context.
726 \item @{attribute iff} declares logical equivalences to the
727 Simplifier and the Classical reasoner at the same time.
728 Non-conditional rules result in a ``safe'' introduction and
729 elimination pair; conditional ones are considered ``unsafe''. Rules
730 with negative conclusion are automatically inverted (using @{text
731 "\<not>"}-elimination internally).
733 The ``@{text "?"}'' version of @{attribute iff} declares rules to
734 the Isabelle/Pure context only, and omits the Simplifier
741 subsection {* Classical operations *}
744 \begin{matharray}{rcl}
745 @{attribute_def swapped} & : & @{text attribute} \\
750 \item @{attribute swapped} turns an introduction rule into an
751 elimination, by resolving with the classical swap principle @{text
752 "(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}.
758 section {* Object-logic setup \label{sec:object-logic} *}
761 \begin{matharray}{rcl}
762 @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
763 @{method_def atomize} & : & @{text method} \\
764 @{attribute_def atomize} & : & @{text attribute} \\
765 @{attribute_def rule_format} & : & @{text attribute} \\
766 @{attribute_def rulify} & : & @{text attribute} \\
769 The very starting point for any Isabelle object-logic is a ``truth
770 judgment'' that links object-level statements to the meta-logic
771 (with its minimal language of @{text prop} that covers universal
772 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
774 Common object-logics are sufficiently expressive to internalize rule
775 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
776 language. This is useful in certain situations where a rule needs
777 to be viewed as an atomic statement from the meta-level perspective,
778 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
780 From the following language elements, only the @{method atomize}
781 method and @{attribute rule_format} attribute are occasionally
782 required by end-users, the rest is for those who need to setup their
783 own object-logic. In the latter case existing formulations of
784 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
786 Generic tools may refer to the information provided by object-logic
787 declarations internally.
792 'atomize' ('(' 'full' ')')?
794 'rule\_format' ('(' 'noasm' ')')?
800 \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
801 @{text c} as the truth judgment of the current object-logic. Its
802 type @{text \<sigma>} should specify a coercion of the category of
803 object-level propositions to @{text prop} of the Pure meta-logic;
804 the mixfix annotation @{text "(mx)"} would typically just link the
805 object language (internally of syntactic category @{text logic})
806 with that of @{text prop}. Only one @{command "judgment"}
807 declaration may be given in any theory development.
809 \item @{method atomize} (as a method) rewrites any non-atomic
810 premises of a sub-goal, using the meta-level equations declared via
811 @{attribute atomize} (as an attribute) beforehand. As a result,
812 heavily nested goals become amenable to fundamental operations such
813 as resolution (cf.\ the @{method rule} method). Giving the ``@{text
814 "(full)"}'' option here means to turn the whole subgoal into an
815 object-statement (if possible), including the outermost parameters
816 and assumptions as well.
818 A typical collection of @{attribute atomize} rules for a particular
819 object-logic would provide an internalization for each of the
820 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
821 Meta-level conjunction should be covered as well (this is
822 particularly important for locales, see \secref{sec:locale}).
824 \item @{attribute rule_format} rewrites a theorem by the equalities
825 declared as @{attribute rulify} rules in the current object-logic.
826 By default, the result is fully normalized, including assumptions
827 and conclusions at any depth. The @{text "(no_asm)"} option
828 restricts the transformation to the conclusion of a rule.
830 In common object-logics (HOL, FOL, ZF), the effect of @{attribute
831 rule_format} is to replace (bounded) universal quantification
832 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
833 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.