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 "op RS"} and
146 @{ML "op COMP"} in \cite{isabelle-implementation}).
148 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
149 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
150 definitions throughout a rule.
152 \item @{attribute rotated}~@{text n} rotate the premises of a
153 theorem by @{text n} (default 1).
155 \item @{attribute (Pure) elim_format} turns a destruction rule into
156 elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
157 (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
159 Note that the Classical Reasoner (\secref{sec:classical}) provides
160 its own version of this operation.
162 \item @{attribute standard} puts a theorem into the standard form of
163 object-rules at the outermost theory level. Note that this
164 operation violates the local proof context (including active
167 \item @{attribute no_vars} replaces schematic variables by free
168 ones; this is mainly for tuning output of pretty printed theorems.
174 subsection {* Low-level equational reasoning *}
177 \begin{matharray}{rcl}
178 @{method_def subst} & : & @{text method} \\
179 @{method_def hypsubst} & : & @{text method} \\
180 @{method_def split} & : & @{text method} \\
184 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
186 'split' ('(' 'asm' ')')? thmrefs
190 These methods provide low-level facilities for equational reasoning
191 that are intended for specialized applications only. Normally,
192 single step calculations would be performed in a structured text
193 (see also \secref{sec:calculation}), while the Simplifier methods
194 provide the canonical way for automated normalization (see
195 \secref{sec:simplifier}).
199 \item @{method subst}~@{text eq} performs a single substitution step
200 using rule @{text eq}, which may be either a meta or object
203 \item @{method subst}~@{text "(asm) eq"} substitutes in an
206 \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
207 substitutions in the conclusion. The numbers @{text i} to @{text j}
208 indicate the positions to substitute at. Positions are ordered from
209 the top of the term tree moving down from left to right. For
210 example, in @{text "(a + b) + (c + d)"} there are three positions
211 where commutativity of @{text "+"} is applicable: 1 refers to @{text
212 "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
214 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
215 (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
216 assume all substitutions are performed simultaneously. Otherwise
217 the behaviour of @{text subst} is not specified.
219 \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
220 substitutions in the assumptions. The positions refer to the
221 assumptions in order from left to right. For example, given in a
222 goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
223 commutativity of @{text "+"} is the subterm @{text "a + b"} and
224 position 2 is the subterm @{text "c + d"}.
226 \item @{method hypsubst} performs substitution using some
227 assumption; this only works for equations of the form @{text "x =
228 t"} where @{text x} is a free or bound variable.
230 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
231 splitting using the given rules. By default, splitting is performed
232 in the conclusion of a goal; the @{text "(asm)"} option indicates to
233 operate on assumptions instead.
235 Note that the @{method simp} method already involves repeated
236 application of split rules as declared in the current context.
242 subsection {* Further tactic emulations \label{sec:tactics} *}
245 The following improper proof methods emulate traditional tactics.
246 These admit direct access to the goal state, which is normally
247 considered harmful! In particular, this may involve both numbered
248 goal addressing (default 1), and dynamic instantiation within the
249 scope of some subgoal.
252 Dynamic instantiations refer to universally quantified parameters
253 of a subgoal (the dynamic context) rather than fixed variables and
254 term abbreviations of a (static) Isar context.
257 Tactic emulation methods, unlike their ML counterparts, admit
258 simultaneous instantiation from both dynamic and static contexts.
259 If names occur in both contexts goal parameters hide locally fixed
260 variables. Likewise, schematic variables refer to term
261 abbreviations, if present in the static context. Otherwise the
262 schematic variable is interpreted as a schematic variable and left
263 to be solved by unification with certain parts of the subgoal.
265 Note that the tactic emulation proof methods in Isabelle/Isar are
266 consistently named @{text foo_tac}. Note also that variable names
267 occurring on left hand sides of instantiations must be preceded by a
268 question mark if they coincide with a keyword or contain dots. This
269 is consistent with the attribute @{attribute "where"} (see
270 \secref{sec:pure-meth-att}).
272 \begin{matharray}{rcl}
273 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
274 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
275 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
276 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
277 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
278 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
279 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
280 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
281 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
282 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
283 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
287 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
288 ( insts thmref | thmrefs )
290 'subgoal\_tac' goalspec? (prop +)
292 'rename\_tac' goalspec? (name +)
294 'rotate\_tac' goalspec? int?
296 ('tactic' | 'raw_tactic') text
299 insts: ((name '=' term) + 'and') 'in'
305 \item @{method rule_tac} etc. do resolution of rules with explicit
306 instantiation. This works the same way as the ML tactics @{ML
307 res_inst_tac} etc. (see \cite{isabelle-implementation})
309 Multiple rules may be only given if there is no instantiation; then
310 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
311 \cite{isabelle-implementation}).
313 \item @{method cut_tac} inserts facts into the proof state as
314 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
315 \cite{isabelle-implementation}. Note that the scope of schematic
316 variables is spread over the main goal statement. Instantiations
317 may be given as well, see also ML tactic @{ML cut_inst_tac} in
318 \cite{isabelle-implementation}.
320 \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
321 from a subgoal; note that @{text \<phi>} may contain schematic variables.
322 See also @{ML thin_tac} in \cite{isabelle-implementation}.
324 \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
325 assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
326 subgoals_tac} in \cite{isabelle-implementation}.
328 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
329 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
330 \emph{suffix} of variables.
332 \item @{method rotate_tac}~@{text n} rotates the assumptions of a
333 goal by @{text n} positions: from right to left if @{text n} is
334 positive, and from left to right if @{text n} is negative; the
335 default value is 1. See also @{ML rotate_tac} in
336 \cite{isabelle-implementation}.
338 \item @{method tactic}~@{text "text"} produces a proof method from
339 any ML text of type @{ML_type tactic}. Apart from the usual ML
340 environment and the current proof context, the ML code may refer to
341 the locally bound values @{ML_text facts}, which indicates any
342 current facts used for forward-chaining.
344 \item @{method raw_tactic} is similar to @{method tactic}, but
345 presents the goal state in its raw internal form, where simultaneous
346 subgoals appear as conjunction of the logical framework instead of
347 the usual split into several subgoals. While feature this is useful
348 for debugging of complex method definitions, it should not never
349 appear in production theories.
355 section {* The Simplifier \label{sec:simplifier} *}
357 subsection {* Simplification methods *}
360 \begin{matharray}{rcl}
361 @{method_def simp} & : & @{text method} \\
362 @{method_def simp_all} & : & @{text method} \\
365 \indexouternonterm{simpmod}
367 ('simp' | 'simp\_all') opt? (simpmod *)
370 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
372 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
373 'split' (() | 'add' | 'del')) ':' thmrefs
379 \item @{method simp} invokes the Simplifier, after declaring
380 additional rules according to the arguments given. Note that the
381 \railtterm{only} modifier first removes all other rewrite rules,
382 congruences, and looper tactics (including splits), and then behaves
383 like \railtterm{add}.
385 \medskip The \railtterm{cong} modifiers add or delete Simplifier
386 congruence rules (see also \cite{isabelle-ref}), the default is to
389 \medskip The \railtterm{split} modifiers add or delete rules for the
390 Splitter (see also \cite{isabelle-ref}), the default is to add.
391 This works only if the Simplifier method has been properly setup to
392 include the Splitter (all major object logics such HOL, HOLCF, FOL,
395 \item @{method simp_all} is similar to @{method simp}, but acts on
396 all goals (backwards from the last to the first one).
400 By default the Simplifier methods take local assumptions fully into
401 account, using equational assumptions in the subsequent
402 normalization process, or simplifying assumptions themselves (cf.\
403 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured
404 proofs this is usually quite well behaved in practice: just the
405 local premises of the actual goal are involved, additional facts may
406 be inserted via explicit forward-chaining (via @{command "then"},
407 @{command "from"}, @{command "using"} etc.).
409 Additional Simplifier options may be specified to tune the behavior
410 further (mostly for unstructured scripts with many accidental local
411 facts): ``@{text "(no_asm)"}'' means assumptions are ignored
412 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
413 assumptions are used in the simplification of the conclusion but are
414 not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
415 "(no_asm_use)"}'' means assumptions are simplified but are not used
416 in the simplification of each other or the conclusion (cf.\ @{ML
417 full_simp_tac}). For compatibility reasons, there is also an option
418 ``@{text "(asm_lr)"}'', which means that an assumption is only used
419 for simplifying assumptions which are to the right of it (cf.\ @{ML
422 The configuration option @{text "depth_limit"} limits the number of
423 recursive invocations of the simplifier during conditional
426 \medskip The Splitter package is usually configured to work as part
427 of the Simplifier. The effect of repeatedly applying @{ML
428 split_tac} can be simulated by ``@{text "(simp only: split:
429 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split}
430 method available for single-step case splitting.
434 subsection {* Declaring rules *}
437 \begin{matharray}{rcl}
438 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
439 @{attribute_def simp} & : & @{text attribute} \\
440 @{attribute_def cong} & : & @{text attribute} \\
441 @{attribute_def split} & : & @{text attribute} \\
445 ('simp' | 'cong' | 'split') (() | 'add' | 'del')
451 \item @{command "print_simpset"} prints the collection of rules
452 declared to the Simplifier, which is also known as ``simpset''
453 internally \cite{isabelle-ref}.
455 \item @{attribute simp} declares simplification rules.
457 \item @{attribute cong} declares congruence rules.
459 \item @{attribute split} declares case split rules.
465 subsection {* Simplification procedures *}
468 \begin{matharray}{rcl}
469 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
470 simproc & : & @{text attribute} \\
474 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
477 'simproc' (('add' ':')? | 'del' ':') (name+)
483 \item @{command "simproc_setup"} defines a named simplification
484 procedure that is invoked by the Simplifier whenever any of the
485 given term patterns match the current redex. The implementation,
486 which is provided as ML source text, needs to be of type @{ML_type
487 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
488 cterm} represents the current redex @{text r} and the result is
489 supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
490 generalized version), or @{ML NONE} to indicate failure. The
491 @{ML_type simpset} argument holds the full context of the current
492 Simplifier invocation, including the actual Isar proof context. The
493 @{ML_type morphism} informs about the difference of the original
494 compilation context wrt.\ the one of the actual application later
495 on. The optional @{keyword "identifier"} specifies theorems that
496 represent the logical content of the abstract theory of this
499 Morphisms and identifiers are only relevant for simprocs that are
500 defined within a local target context, e.g.\ in a locale.
502 \item @{text "simproc add: name"} and @{text "simproc del: name"}
503 add or delete named simprocs to the current Simplifier context. The
504 default is to add a simproc. Note that @{command "simproc_setup"}
505 already adds the new simproc to the subsequent context.
511 subsection {* Forward simplification *}
514 \begin{matharray}{rcl}
515 @{attribute_def simplified} & : & @{text attribute} \\
519 'simplified' opt? thmrefs?
522 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
528 \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
529 be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
530 a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
531 The result is fully simplified by default, including assumptions and
532 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
533 the same way as the for the @{text simp} method.
535 Note that forward simplification restricts the simplifier to its
536 most basic operation of term rewriting; solver and looper tactics
537 \cite{isabelle-ref} are \emph{not} involved here. The @{text
538 simplified} attribute should be only rarely required under normal
545 section {* The Classical Reasoner \label{sec:classical} *}
547 subsection {* Basic methods *}
550 \begin{matharray}{rcl}
551 @{method_def rule} & : & @{text method} \\
552 @{method_def contradiction} & : & @{text method} \\
553 @{method_def intro} & : & @{text method} \\
554 @{method_def elim} & : & @{text method} \\
558 ('rule' | 'intro' | 'elim') thmrefs?
564 \item @{method rule} as offered by the Classical Reasoner is a
565 refinement over the primitive one (see \secref{sec:pure-meth-att}).
566 Both versions essentially work the same, but the classical version
567 observes the classical rule context in addition to that of
570 Common object logics (HOL, ZF, etc.) declare a rich collection of
571 classical rules (even if these would qualify as intuitionistic
572 ones), but only few declarations to the rule context of
573 Isabelle/Pure (\secref{sec:pure-meth-att}).
575 \item @{method contradiction} solves some goal by contradiction,
576 deriving any result from both @{text "\<not> A"} and @{text A}. Chained
577 facts, which are guaranteed to participate, may appear in either
580 \item @{method intro} and @{method elim} repeatedly refine some goal
581 by intro- or elim-resolution, after having inserted any chained
582 facts. Exactly the rules given as arguments are taken into account;
583 this allows fine-tuned decomposition of a proof problem, in contrast
584 to common automated tools.
590 subsection {* Automated methods *}
593 \begin{matharray}{rcl}
594 @{method_def blast} & : & @{text method} \\
595 @{method_def fast} & : & @{text method} \\
596 @{method_def slow} & : & @{text method} \\
597 @{method_def best} & : & @{text method} \\
598 @{method_def safe} & : & @{text method} \\
599 @{method_def clarify} & : & @{text method} \\
602 \indexouternonterm{clamod}
604 'blast' nat? (clamod *)
606 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
609 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
615 \item @{method blast} refers to the classical tableau prover (see
616 @{ML blast_tac} in \cite{isabelle-ref}). The optional argument
617 specifies a user-supplied search bound (default 20).
619 \item @{method fast}, @{method slow}, @{method best}, @{method
620 safe}, and @{method clarify} refer to the generic classical
621 reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
622 safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
627 Any of the above methods support additional modifiers of the context
628 of classical rules. Their semantics is analogous to the attributes
629 given before. Facts provided by forward chaining are inserted into
630 the goal before commencing proof search.
634 subsection {* Combined automated methods \label{sec:clasimp} *}
637 \begin{matharray}{rcl}
638 @{method_def auto} & : & @{text method} \\
639 @{method_def force} & : & @{text method} \\
640 @{method_def clarsimp} & : & @{text method} \\
641 @{method_def fastsimp} & : & @{text method} \\
642 @{method_def slowsimp} & : & @{text method} \\
643 @{method_def bestsimp} & : & @{text method} \\
646 \indexouternonterm{clasimpmod}
648 'auto' (nat nat)? (clasimpmod *)
650 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
653 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
654 ('cong' | 'split') (() | 'add' | 'del') |
655 'iff' (((() | 'add') '?'?) | 'del') |
656 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
661 \item @{method auto}, @{method force}, @{method clarsimp}, @{method
662 fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access
663 to Isabelle's combined simplification and classical reasoning
664 tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
665 clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
666 added as wrapper, see \cite{isabelle-ref} for more information. The
667 modifier arguments correspond to those given in
668 \secref{sec:simplifier} and \secref{sec:classical}. Just note that
669 the ones related to the Simplifier are prefixed by \railtterm{simp}
672 Facts provided by forward chaining are inserted into the goal before
679 subsection {* Declaring rules *}
682 \begin{matharray}{rcl}
683 @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
684 @{attribute_def intro} & : & @{text attribute} \\
685 @{attribute_def elim} & : & @{text attribute} \\
686 @{attribute_def dest} & : & @{text attribute} \\
687 @{attribute_def rule} & : & @{text attribute} \\
688 @{attribute_def iff} & : & @{text attribute} \\
692 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
696 'iff' (((() | 'add') '?'?) | 'del')
702 \item @{command "print_claset"} prints the collection of rules
703 declared to the Classical Reasoner, which is also known as
704 ``claset'' internally \cite{isabelle-ref}.
706 \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
707 declare introduction, elimination, and destruction rules,
708 respectively. By default, rules are considered as \emph{unsafe}
709 (i.e.\ not applied blindly without backtracking), while ``@{text
710 "!"}'' classifies as \emph{safe}. Rule declarations marked by
711 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
712 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
713 of the @{method rule} method). The optional natural number
714 specifies an explicit weight argument, which is ignored by automated
715 tools, but determines the search order of single rule steps.
717 \item @{attribute rule}~@{text del} deletes introduction,
718 elimination, or destruction rules from the context.
720 \item @{attribute iff} declares logical equivalences to the
721 Simplifier and the Classical reasoner at the same time.
722 Non-conditional rules result in a ``safe'' introduction and
723 elimination pair; conditional ones are considered ``unsafe''. Rules
724 with negative conclusion are automatically inverted (using @{text
725 "\<not>"}-elimination internally).
727 The ``@{text "?"}'' version of @{attribute iff} declares rules to
728 the Isabelle/Pure context only, and omits the Simplifier
735 subsection {* Classical operations *}
738 \begin{matharray}{rcl}
739 @{attribute_def swapped} & : & @{text attribute} \\
744 \item @{attribute swapped} turns an introduction rule into an
745 elimination, by resolving with the classical swap principle @{text
746 "(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}.
752 section {* Object-logic setup \label{sec:object-logic} *}
755 \begin{matharray}{rcl}
756 @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
757 @{method_def atomize} & : & @{text method} \\
758 @{attribute_def atomize} & : & @{text attribute} \\
759 @{attribute_def rule_format} & : & @{text attribute} \\
760 @{attribute_def rulify} & : & @{text attribute} \\
763 The very starting point for any Isabelle object-logic is a ``truth
764 judgment'' that links object-level statements to the meta-logic
765 (with its minimal language of @{text prop} that covers universal
766 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
768 Common object-logics are sufficiently expressive to internalize rule
769 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
770 language. This is useful in certain situations where a rule needs
771 to be viewed as an atomic statement from the meta-level perspective,
772 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
774 From the following language elements, only the @{method atomize}
775 method and @{attribute rule_format} attribute are occasionally
776 required by end-users, the rest is for those who need to setup their
777 own object-logic. In the latter case existing formulations of
778 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
780 Generic tools may refer to the information provided by object-logic
781 declarations internally.
786 'atomize' ('(' 'full' ')')?
788 'rule\_format' ('(' 'noasm' ')')?
794 \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
795 @{text c} as the truth judgment of the current object-logic. Its
796 type @{text \<sigma>} should specify a coercion of the category of
797 object-level propositions to @{text prop} of the Pure meta-logic;
798 the mixfix annotation @{text "(mx)"} would typically just link the
799 object language (internally of syntactic category @{text logic})
800 with that of @{text prop}. Only one @{command "judgment"}
801 declaration may be given in any theory development.
803 \item @{method atomize} (as a method) rewrites any non-atomic
804 premises of a sub-goal, using the meta-level equations declared via
805 @{attribute atomize} (as an attribute) beforehand. As a result,
806 heavily nested goals become amenable to fundamental operations such
807 as resolution (cf.\ the @{method rule} method). Giving the ``@{text
808 "(full)"}'' option here means to turn the whole subgoal into an
809 object-statement (if possible), including the outermost parameters
810 and assumptions as well.
812 A typical collection of @{attribute atomize} rules for a particular
813 object-logic would provide an internalization for each of the
814 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
815 Meta-level conjunction should be covered as well (this is
816 particularly important for locales, see \secref{sec:locale}).
818 \item @{attribute rule_format} rewrites a theorem by the equalities
819 declared as @{attribute rulify} rules in the current object-logic.
820 By default, the result is fully normalized, including assumptions
821 and conclusions at any depth. The @{text "(no_asm)"} option
822 restricts the transformation to the conclusion of a rule.
824 In common object-logics (HOL, FOL, ZF), the effect of @{attribute
825 rule_format} is to replace (bounded) universal quantification
826 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
827 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.