5 chapter {* Generic tools and packages \label{ch:gen-tools} *}
7 section {* Configuration options \label{sec:config} *}
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"} like
21 declare [[show_main_goal = false]]
25 note [[show_main_goal = true]]
28 text {* For historical reasons, some tools cannot take the full proof
29 context into account and merely refer to the background theory.
30 This is accommodated by configuration options being declared as
31 ``global'', which may not be changed within a local context.
33 \begin{matharray}{rcll}
34 @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
38 @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
43 \item @{command "print_configs"} prints the available configuration
44 options, with names, types, and current values.
46 \item @{text "name = value"} as an attribute expression modifies the
47 named option, with the syntax of the value depending on the option's
48 type. For @{ML_type bool} the default value is @{text true}. Any
49 attempt to change a global option in a local context is ignored.
55 section {* Basic proof tools *}
57 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}
60 \begin{matharray}{rcl}
61 @{method_def unfold} & : & @{text method} \\
62 @{method_def fold} & : & @{text method} \\
63 @{method_def insert} & : & @{text method} \\[0.5ex]
64 @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
65 @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
66 @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
67 @{method_def intro} & : & @{text method} \\
68 @{method_def elim} & : & @{text method} \\
69 @{method_def succeed} & : & @{text method} \\
70 @{method_def fail} & : & @{text method} \\
74 (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
76 (@@{method erule} | @@{method drule} | @@{method frule})
77 ('(' @{syntax nat} ')')? @{syntax thmrefs}
79 (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
84 \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
85 "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout
86 all goals; any chained facts provided are inserted into the goal and
87 subject to rewriting as well.
89 \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts
90 into all goals of the proof state. Note that current facts
91 indicated for forward chaining are ignored.
93 \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
94 drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
95 "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
96 method (see \secref{sec:pure-meth-att}), but apply rules by
97 elim-resolution, destruct-resolution, and forward-resolution,
98 respectively \cite{isabelle-implementation}. The optional natural
99 number argument (default 0) specifies additional assumption steps to
102 Note that these methods are improper ones, mainly serving for
103 experimentation and tactic script emulation. Different modes of
104 basic rule application are usually expressed in Isar at the proof
105 language level, rather than via implicit proof state manipulations.
106 For example, a proper single-step elimination would be done using
107 the plain @{method rule} method, with forward chaining of current
110 \item @{method intro} and @{method elim} repeatedly refine some goal
111 by intro- or elim-resolution, after having inserted any chained
112 facts. Exactly the rules given as arguments are taken into account;
113 this allows fine-tuned decomposition of a proof problem, in contrast
114 to common automated tools.
116 \item @{method succeed} yields a single (unchanged) result; it is
117 the identity of the ``@{text ","}'' method combinator (cf.\
118 \secref{sec:proof-meth}).
120 \item @{method fail} yields an empty result sequence; it is the
121 identity of the ``@{text "|"}'' method combinator (cf.\
122 \secref{sec:proof-meth}).
126 \begin{matharray}{rcl}
127 @{attribute_def tagged} & : & @{text attribute} \\
128 @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
129 @{attribute_def THEN} & : & @{text attribute} \\
130 @{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
131 @{attribute_def unfolded} & : & @{text attribute} \\
132 @{attribute_def folded} & : & @{text attribute} \\[0.5ex]
133 @{attribute_def rotated} & : & @{text attribute} \\
134 @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
135 @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
136 @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
140 @@{attribute tagged} @{syntax name} @{syntax name}
142 @@{attribute untagged} @{syntax name}
144 (@@{attribute THEN} | @@{attribute COMP}) ('[' @{syntax nat} ']')? @{syntax thmref}
146 (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
148 @@{attribute rotated} @{syntax int}?
153 \item @{attribute tagged}~@{text "name value"} and @{attribute
154 untagged}~@{text name} add and remove \emph{tags} of some theorem.
155 Tags may be any list of string pairs that serve as formal comment.
156 The first string is considered the tag name, the second its value.
157 Note that @{attribute untagged} removes any tags of the same name.
159 \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}
160 compose rules by resolution. @{attribute THEN} resolves with the
161 first premise of @{text a} (an alternative position may be also
162 specified); the @{attribute COMP} version skips the automatic
163 lifting process that is normally intended (cf.\ @{ML "op RS"} and
164 @{ML "op COMP"} in \cite{isabelle-implementation}).
166 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
167 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
168 definitions throughout a rule.
170 \item @{attribute rotated}~@{text n} rotate the premises of a
171 theorem by @{text n} (default 1).
173 \item @{attribute (Pure) elim_format} turns a destruction rule into
174 elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
175 (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
177 Note that the Classical Reasoner (\secref{sec:classical}) provides
178 its own version of this operation.
180 \item @{attribute standard} puts a theorem into the standard form of
181 object-rules at the outermost theory level. Note that this
182 operation violates the local proof context (including active
185 \item @{attribute no_vars} replaces schematic variables by free
186 ones; this is mainly for tuning output of pretty printed theorems.
192 subsection {* Low-level equational reasoning *}
195 \begin{matharray}{rcl}
196 @{method_def subst} & : & @{text method} \\
197 @{method_def hypsubst} & : & @{text method} \\
198 @{method_def split} & : & @{text method} \\
202 @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
204 @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
207 These methods provide low-level facilities for equational reasoning
208 that are intended for specialized applications only. Normally,
209 single step calculations would be performed in a structured text
210 (see also \secref{sec:calculation}), while the Simplifier methods
211 provide the canonical way for automated normalization (see
212 \secref{sec:simplifier}).
216 \item @{method subst}~@{text eq} performs a single substitution step
217 using rule @{text eq}, which may be either a meta or object
220 \item @{method subst}~@{text "(asm) eq"} substitutes in an
223 \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
224 substitutions in the conclusion. The numbers @{text i} to @{text j}
225 indicate the positions to substitute at. Positions are ordered from
226 the top of the term tree moving down from left to right. For
227 example, in @{text "(a + b) + (c + d)"} there are three positions
228 where commutativity of @{text "+"} is applicable: 1 refers to @{text
229 "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
231 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
232 (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
233 assume all substitutions are performed simultaneously. Otherwise
234 the behaviour of @{text subst} is not specified.
236 \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
237 substitutions in the assumptions. The positions refer to the
238 assumptions in order from left to right. For example, given in a
239 goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
240 commutativity of @{text "+"} is the subterm @{text "a + b"} and
241 position 2 is the subterm @{text "c + d"}.
243 \item @{method hypsubst} performs substitution using some
244 assumption; this only works for equations of the form @{text "x =
245 t"} where @{text x} is a free or bound variable.
247 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
248 splitting using the given rules. By default, splitting is performed
249 in the conclusion of a goal; the @{text "(asm)"} option indicates to
250 operate on assumptions instead.
252 Note that the @{method simp} method already involves repeated
253 application of split rules as declared in the current context.
259 subsection {* Further tactic emulations \label{sec:tactics} *}
262 The following improper proof methods emulate traditional tactics.
263 These admit direct access to the goal state, which is normally
264 considered harmful! In particular, this may involve both numbered
265 goal addressing (default 1), and dynamic instantiation within the
266 scope of some subgoal.
269 Dynamic instantiations refer to universally quantified parameters
270 of a subgoal (the dynamic context) rather than fixed variables and
271 term abbreviations of a (static) Isar context.
274 Tactic emulation methods, unlike their ML counterparts, admit
275 simultaneous instantiation from both dynamic and static contexts.
276 If names occur in both contexts goal parameters hide locally fixed
277 variables. Likewise, schematic variables refer to term
278 abbreviations, if present in the static context. Otherwise the
279 schematic variable is interpreted as a schematic variable and left
280 to be solved by unification with certain parts of the subgoal.
282 Note that the tactic emulation proof methods in Isabelle/Isar are
283 consistently named @{text foo_tac}. Note also that variable names
284 occurring on left hand sides of instantiations must be preceded by a
285 question mark if they coincide with a keyword or contain dots. This
286 is consistent with the attribute @{attribute "where"} (see
287 \secref{sec:pure-meth-att}).
289 \begin{matharray}{rcl}
290 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
291 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
292 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
293 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
294 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
295 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
296 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
297 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
298 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
299 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
300 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
304 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
305 @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\
306 ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
308 @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
310 @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
312 @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
314 (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
317 dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
322 \item @{method rule_tac} etc. do resolution of rules with explicit
323 instantiation. This works the same way as the ML tactics @{ML
324 res_inst_tac} etc. (see \cite{isabelle-implementation})
326 Multiple rules may be only given if there is no instantiation; then
327 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
328 \cite{isabelle-implementation}).
330 \item @{method cut_tac} inserts facts into the proof state as
331 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
332 \cite{isabelle-implementation}. Note that the scope of schematic
333 variables is spread over the main goal statement. Instantiations
334 may be given as well, see also ML tactic @{ML cut_inst_tac} in
335 \cite{isabelle-implementation}.
337 \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
338 from a subgoal; note that @{text \<phi>} may contain schematic variables.
339 See also @{ML thin_tac} in \cite{isabelle-implementation}.
341 \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
342 assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
343 subgoals_tac} in \cite{isabelle-implementation}.
345 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
346 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
347 \emph{suffix} of variables.
349 \item @{method rotate_tac}~@{text n} rotates the assumptions of a
350 goal by @{text n} positions: from right to left if @{text n} is
351 positive, and from left to right if @{text n} is negative; the
352 default value is 1. See also @{ML rotate_tac} in
353 \cite{isabelle-implementation}.
355 \item @{method tactic}~@{text "text"} produces a proof method from
356 any ML text of type @{ML_type tactic}. Apart from the usual ML
357 environment and the current proof context, the ML code may refer to
358 the locally bound values @{ML_text facts}, which indicates any
359 current facts used for forward-chaining.
361 \item @{method raw_tactic} is similar to @{method tactic}, but
362 presents the goal state in its raw internal form, where simultaneous
363 subgoals appear as conjunction of the logical framework instead of
364 the usual split into several subgoals. While feature this is useful
365 for debugging of complex method definitions, it should not never
366 appear in production theories.
372 section {* The Simplifier \label{sec:simplifier} *}
374 subsection {* Simplification methods *}
377 \begin{matharray}{rcl}
378 @{method_def simp} & : & @{text method} \\
379 @{method_def simp_all} & : & @{text method} \\
383 (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
386 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
388 @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
389 'split' (() | 'add' | 'del')) ':' @{syntax thmrefs}
394 \item @{method simp} invokes the Simplifier, after declaring
395 additional rules according to the arguments given. Note that the
396 @{text only} modifier first removes all other rewrite rules,
397 congruences, and looper tactics (including splits), and then behaves
400 \medskip The @{text cong} modifiers add or delete Simplifier
401 congruence rules (see also \cite{isabelle-ref}), the default is to
404 \medskip The @{text split} modifiers add or delete rules for the
405 Splitter (see also \cite{isabelle-ref}), the default is to add.
406 This works only if the Simplifier method has been properly setup to
407 include the Splitter (all major object logics such HOL, HOLCF, FOL,
410 \item @{method simp_all} is similar to @{method simp}, but acts on
411 all goals (backwards from the last to the first one).
415 By default the Simplifier methods take local assumptions fully into
416 account, using equational assumptions in the subsequent
417 normalization process, or simplifying assumptions themselves (cf.\
418 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured
419 proofs this is usually quite well behaved in practice: just the
420 local premises of the actual goal are involved, additional facts may
421 be inserted via explicit forward-chaining (via @{command "then"},
422 @{command "from"}, @{command "using"} etc.).
424 Additional Simplifier options may be specified to tune the behavior
425 further (mostly for unstructured scripts with many accidental local
426 facts): ``@{text "(no_asm)"}'' means assumptions are ignored
427 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
428 assumptions are used in the simplification of the conclusion but are
429 not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
430 "(no_asm_use)"}'' means assumptions are simplified but are not used
431 in the simplification of each other or the conclusion (cf.\ @{ML
432 full_simp_tac}). For compatibility reasons, there is also an option
433 ``@{text "(asm_lr)"}'', which means that an assumption is only used
434 for simplifying assumptions which are to the right of it (cf.\ @{ML
437 The configuration option @{text "depth_limit"} limits the number of
438 recursive invocations of the simplifier during conditional
441 \medskip The Splitter package is usually configured to work as part
442 of the Simplifier. The effect of repeatedly applying @{ML
443 split_tac} can be simulated by ``@{text "(simp only: split:
444 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split}
445 method available for single-step case splitting.
449 subsection {* Declaring rules *}
452 \begin{matharray}{rcl}
453 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
454 @{attribute_def simp} & : & @{text attribute} \\
455 @{attribute_def cong} & : & @{text attribute} \\
456 @{attribute_def split} & : & @{text attribute} \\
460 (@@{attribute simp} | @@{attribute cong} | @@{attribute split}) (() | 'add' | 'del')
465 \item @{command "print_simpset"} prints the collection of rules
466 declared to the Simplifier, which is also known as ``simpset''
467 internally \cite{isabelle-ref}.
469 \item @{attribute simp} declares simplification rules.
471 \item @{attribute cong} declares congruence rules.
473 \item @{attribute split} declares case split rules.
479 subsection {* Simplification procedures *}
481 text {* Simplification procedures are ML functions that produce proven
482 rewrite rules on demand. They are associated with higher-order
483 patterns that approximate the left-hand sides of equations. The
484 Simplifier first matches the current redex against one of the LHS
485 patterns; if this succeeds, the corresponding ML function is
486 invoked, passing the Simplifier context and redex term. Thus rules
487 may be specifically fashioned for particular situations, resulting
488 in a more powerful mechanism than term rewriting by a fixed set of
491 Any successful result needs to be a (possibly conditional) rewrite
492 rule @{text "t \<equiv> u"} that is applicable to the current redex. The
493 rule will be applied just as any ordinary rewrite rule. It is
494 expected to be already in \emph{internal form}, bypassing the
495 automatic preprocessing of object-level equivalences.
497 \begin{matharray}{rcl}
498 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
499 simproc & : & @{text attribute} \\
503 @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
504 @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?
507 @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
512 \item @{command "simproc_setup"} defines a named simplification
513 procedure that is invoked by the Simplifier whenever any of the
514 given term patterns match the current redex. The implementation,
515 which is provided as ML source text, needs to be of type @{ML_type
516 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
517 cterm} represents the current redex @{text r} and the result is
518 supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
519 generalized version), or @{ML NONE} to indicate failure. The
520 @{ML_type simpset} argument holds the full context of the current
521 Simplifier invocation, including the actual Isar proof context. The
522 @{ML_type morphism} informs about the difference of the original
523 compilation context wrt.\ the one of the actual application later
524 on. The optional @{keyword "identifier"} specifies theorems that
525 represent the logical content of the abstract theory of this
528 Morphisms and identifiers are only relevant for simprocs that are
529 defined within a local target context, e.g.\ in a locale.
531 \item @{text "simproc add: name"} and @{text "simproc del: name"}
532 add or delete named simprocs to the current Simplifier context. The
533 default is to add a simproc. Note that @{command "simproc_setup"}
534 already adds the new simproc to the subsequent context.
540 subsubsection {* Example *}
542 text {* The following simplification procedure for @{thm
543 [source=false, show_types] unit_eq} in HOL performs fine-grained
544 control over rule application, beyond higher-order pattern matching.
545 Declaring @{thm unit_eq} as @{attribute simp} directly would make
546 the simplifier loop! Note that a version of this simplification
547 procedure is already active in Isabelle/HOL. *}
549 simproc_setup unit ("x::unit") = {*
550 fn _ => fn _ => fn ct =>
551 if HOLogic.is_unit (term_of ct) then NONE
552 else SOME (mk_meta_eq @{thm unit_eq})
555 text {* Since the Simplifier applies simplification procedures
556 frequently, it is important to make the failure check in ML
560 subsection {* Forward simplification *}
563 \begin{matharray}{rcl}
564 @{attribute_def simplified} & : & @{text attribute} \\
568 @@{attribute simplified} opt? @{syntax thmrefs}?
571 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
576 \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
577 be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
578 a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
579 The result is fully simplified by default, including assumptions and
580 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
581 the same way as the for the @{text simp} method.
583 Note that forward simplification restricts the simplifier to its
584 most basic operation of term rewriting; solver and looper tactics
585 \cite{isabelle-ref} are \emph{not} involved here. The @{text
586 simplified} attribute should be only rarely required under normal
593 section {* The Classical Reasoner \label{sec:classical} *}
595 subsection {* Basic concepts *}
597 text {* Although Isabelle is generic, many users will be working in
598 some extension of classical first-order logic. Isabelle/ZF is built
599 upon theory FOL, while Isabelle/HOL conceptually contains
600 first-order logic as a fragment. Theorem-proving in predicate logic
601 is undecidable, but many automated strategies have been developed to
604 Isabelle's classical reasoner is a generic package that accepts
605 certain information about a logic and delivers a suite of automatic
606 proof tools, based on rules that are classified and declared in the
607 context. These proof procedures are slow and simplistic compared
608 with high-end automated theorem provers, but they can save
609 considerable time and effort in practice. They can prove theorems
610 such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few
611 milliseconds (including full proof reconstruction): *}
613 lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)"
616 lemma "(\<forall>z. \<exists>y. \<forall>x. f x y \<longleftrightarrow> f x z \<and> \<not> f x x) \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)"
619 text {* The proof tools are generic. They are not restricted to
620 first-order logic, and have been heavily used in the development of
621 the Isabelle/HOL library and applications. The tactics can be
622 traced, and their components can be called directly; in this manner,
623 any proof can be viewed interactively. *}
626 subsubsection {* The sequent calculus *}
628 text {* Isabelle supports natural deduction, which is easy to use for
629 interactive proof. But natural deduction does not easily lend
630 itself to automation, and has a bias towards intuitionism. For
631 certain proofs in classical logic, it can not be called natural.
632 The \emph{sequent calculus}, a generalization of natural deduction,
633 is easier to automate.
635 A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}
636 and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order
637 logic, sequents can equivalently be made from lists or multisets of
638 formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is
639 \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>
640 Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which
641 is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A
642 sequent is \textbf{basic} if its left and right sides have a common
643 formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially
646 Sequent rules are classified as \textbf{right} or \textbf{left},
647 indicating which side of the @{text "\<turnstile>"} symbol they operate on.
648 Rules that operate on the right side are analogous to natural
649 deduction's introduction rules, and left rules are analogous to
650 elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"}
653 \infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}}
655 Applying the rule backwards, this breaks down some implication on
656 the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for
657 the sets of formulae that are unaffected by the inference. The
658 analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the
661 \infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}}
663 This breaks down some disjunction on the right side, replacing it by
664 both disjuncts. Thus, the sequent calculus is a kind of
665 multiple-conclusion logic.
667 To illustrate the use of multiple formulae on the right, let us
668 prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}. Working
669 backwards, we reduce this formula to a basic sequent:
671 \infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}}
672 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}}
673 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}}
674 {@{text "P, Q \<turnstile> Q, P"}}}}
677 This example is typical of the sequent calculus: start with the
678 desired theorem and apply rules backwards in a fairly arbitrary
679 manner. This yields a surprisingly effective proof procedure.
680 Quantifiers add only few complications, since Isabelle handles
681 parameters and schematic variables. See \cite[Chapter
682 10]{paulson-ml2} for further discussion. *}
685 subsubsection {* Simulating sequents by natural deduction *}
687 text {* Isabelle can represent sequents directly, as in the
688 object-logic LK. But natural deduction is easier to work with, and
689 most object-logics employ it. Fortunately, we can simulate the
690 sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula
691 @{text "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>2 \<Longrightarrow> ... \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> Q\<^sub>1"} where the order of
692 the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary.
693 Elim-resolution plays a key role in simulating sequent proofs.
695 We can easily handle reasoning on the left. Elim-resolution with
696 the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves
697 a similar effect as the corresponding sequent rules. For the other
698 connectives, we use sequent-style elimination rules instead of
699 destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}.
700 But note that the rule @{text "(\<not>L)"} has no effect under our
701 representation of sequents!
703 \infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}}
706 What about reasoning on the right? Introduction rules can only
707 affect the formula in the conclusion, namely @{text "Q\<^sub>1"}. The
708 other right-side formulae are represented as negated assumptions,
709 @{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}. In order to operate on one of these, it
710 must first be exchanged with @{text "Q\<^sub>1"}. Elim-resolution with the
711 @{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"}
713 To ensure that swaps occur only when necessary, each introduction
714 rule is converted into a swapped form: it is resolved with the
715 second premise of @{text "(swap)"}. The swapped form of @{text
716 "(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is
717 @{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"}
719 Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is
720 @{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"}
722 Swapped introduction rules are applied using elim-resolution, which
723 deletes the negated formula. Our representation of sequents also
724 requires the use of ordinary introduction rules. If we had no
725 regard for readability of intermediate goal states, we could treat
726 the right side more uniformly by representing sequents as @{text
727 [display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"}
731 subsubsection {* Extra rules for the sequent calculus *}
733 text {* As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and
734 @{text "(\<forall>E)"} must be replaced by sequent-style elimination rules.
735 In addition, we need rules to embody the classical equivalence
736 between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}. The introduction
737 rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates
738 @{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"}
740 The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display]
741 "(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"}
743 Quantifier replication also requires special rules. In classical
744 logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"};
745 the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual:
747 \infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}}
749 \infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}
751 Thus both kinds of quantifier may be replicated. Theorems requiring
752 multiple uses of a universal formula are easy to invent; consider
753 @{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any
754 @{text "n > 1"}. Natural examples of the multiple use of an
755 existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x
756 \<longrightarrow> P y"}.
758 Forgoing quantifier replication loses completeness, but gains
759 decidability, since the search space becomes finite. Many useful
760 theorems can be proved without replication, and the search generally
761 delivers its verdict in a reasonable time. To adopt this approach,
762 represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and
763 @{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"},
764 respectively, and put @{text "(\<forall>E)"} into elimination form: @{text
765 [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"}
767 Elim-resolution with this rule will delete the universal formula
768 after a single use. To replicate universal quantifiers, replace the
769 rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"}
771 To replicate existential quantifiers, replace @{text "(\<exists>I)"} by
772 @{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"}
774 All introduction rules mentioned above are also useful in swapped
777 Replication makes the search space infinite; we must apply the rules
778 with care. The classical reasoner distinguishes between safe and
779 unsafe rules, applying the latter only when there is no alternative.
780 Depth-first search may well go down a blind alley; best-first search
781 is better behaved in an infinite search space. However, quantifier
782 replication is too expensive to prove any but the simplest theorems.
786 subsection {* Rule declarations *}
788 text {* The proof tools of the Classical Reasoner depend on
789 collections of rules declared in the context, which are classified
790 as introduction, elimination or destruction and as \emph{safe} or
791 \emph{unsafe}. In general, safe rules can be attempted blindly,
792 while unsafe rules must be used with care. A safe rule must never
793 reduce a provable goal to an unprovable set of subgoals.
795 The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P
796 \<or> Q"} to @{text "P"}, which might turn out as premature choice of an
797 unprovable subgoal. Any rule is unsafe whose premises contain new
798 unknowns. The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is
799 unsafe, since it is applied via elim-resolution, which discards the
800 assumption @{text "\<forall>x. P x"} and replaces it by the weaker
801 assumption @{text "P t"}. The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is
802 unsafe for similar reasons. The quantifier duplication rule @{text
803 "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:
804 since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to
805 looping. In classical first-order logic, all rules are safe except
806 those mentioned above.
808 The safe~/ unsafe distinction is vague, and may be regarded merely
809 as a way of giving some rules priority over others. One could argue
810 that @{text "(\<or>E)"} is unsafe, because repeated application of it
811 could generate exponentially many subgoals. Induction rules are
812 unsafe because inductive proofs are difficult to set up
813 automatically. Any inference is unsafe that instantiates an unknown
814 in the proof state --- thus matching must be used, rather than
815 unification. Even proof by assumption is unsafe if it instantiates
816 unknowns shared with other subgoals.
818 \begin{matharray}{rcl}
819 @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
820 @{attribute_def intro} & : & @{text attribute} \\
821 @{attribute_def elim} & : & @{text attribute} \\
822 @{attribute_def dest} & : & @{text attribute} \\
823 @{attribute_def rule} & : & @{text attribute} \\
824 @{attribute_def iff} & : & @{text attribute} \\
825 @{attribute_def swapped} & : & @{text attribute} \\
829 (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
831 @@{attribute rule} 'del'
833 @@{attribute iff} (((() | 'add') '?'?) | 'del')
838 \item @{command "print_claset"} prints the collection of rules
839 declared to the Classical Reasoner, i.e.\ the @{ML_type claset}
842 \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
843 declare introduction, elimination, and destruction rules,
844 respectively. By default, rules are considered as \emph{unsafe}
845 (i.e.\ not applied blindly without backtracking), while ``@{text
846 "!"}'' classifies as \emph{safe}. Rule declarations marked by
847 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
848 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
849 of the @{method rule} method). The optional natural number
850 specifies an explicit weight argument, which is ignored by the
851 automated reasoning tools, but determines the search order of single
854 Introduction rules are those that can be applied using ordinary
855 resolution. Their swapped forms are generated internally, which
856 will be applied using elim-resolution. Elimination rules are
857 applied using elim-resolution. Rules are sorted by the number of
858 new subgoals they will yield; rules that generate the fewest
859 subgoals will be tried first. Otherwise, later declarations take
860 precedence over earlier ones.
862 Rules already present in the context with the same classification
863 are ignored. A warning is printed if the rule has already been
864 added with some other classification, but the rule is added anyway
867 \item @{attribute rule}~@{text del} deletes all occurrences of a
868 rule from the classical context, regardless of its classification as
869 introduction~/ elimination~/ destruction and safe~/ unsafe.
871 \item @{attribute iff} declares logical equivalences to the
872 Simplifier and the Classical reasoner at the same time.
873 Non-conditional rules result in a safe introduction and elimination
874 pair; conditional ones are considered unsafe. Rules with negative
875 conclusion are automatically inverted (using @{text "\<not>"}-elimination
878 The ``@{text "?"}'' version of @{attribute iff} declares rules to
879 the Isabelle/Pure context only, and omits the Simplifier
882 \item @{attribute swapped} turns an introduction rule into an
883 elimination, by resolving with the classical swap principle @{text
884 "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for
885 illustrative purposes: the Classical Reasoner already swaps rules
886 internally as explained above.
892 subsection {* Structured methods *}
895 \begin{matharray}{rcl}
896 @{method_def rule} & : & @{text method} \\
897 @{method_def contradiction} & : & @{text method} \\
901 @@{method rule} @{syntax thmrefs}?
906 \item @{method rule} as offered by the Classical Reasoner is a
907 refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
908 versions work the same, but the classical version observes the
909 classical rule context in addition to that of Isabelle/Pure.
911 Common object logics (HOL, ZF, etc.) declare a rich collection of
912 classical rules (even if these would qualify as intuitionistic
913 ones), but only few declarations to the rule context of
914 Isabelle/Pure (\secref{sec:pure-meth-att}).
916 \item @{method contradiction} solves some goal by contradiction,
917 deriving any result from both @{text "\<not> A"} and @{text A}. Chained
918 facts, which are guaranteed to participate, may appear in either
925 subsection {* Automated methods *}
928 \begin{matharray}{rcl}
929 @{method_def blast} & : & @{text method} \\
930 @{method_def auto} & : & @{text method} \\
931 @{method_def force} & : & @{text method} \\
932 @{method_def fast} & : & @{text method} \\
933 @{method_def slow} & : & @{text method} \\
934 @{method_def best} & : & @{text method} \\
935 @{method_def fastsimp} & : & @{text method} \\
936 @{method_def slowsimp} & : & @{text method} \\
937 @{method_def bestsimp} & : & @{text method} \\
938 @{method_def deepen} & : & @{text method} \\
942 @@{method blast} @{syntax nat}? (@{syntax clamod} * )
944 @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
946 @@{method force} (@{syntax clasimpmod} * )
948 (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * )
950 (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp})
951 (@{syntax clasimpmod} * )
953 @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
955 @{syntax_def clamod}:
956 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
958 @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
959 ('cong' | 'split') (() | 'add' | 'del') |
960 'iff' (((() | 'add') '?'?) | 'del') |
961 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
966 \item @{method blast} is a separate classical tableau prover that
967 uses the same classical rule declarations as explained before.
969 Proof search is coded directly in ML using special data structures.
970 A successful proof is then reconstructed using regular Isabelle
971 inferences. It is faster and more powerful than the other classical
972 reasoning tools, but has major limitations too.
976 \item It does not use the classical wrapper tacticals, such as the
977 integration with the Simplifier of @{method fastsimp}.
979 \item It does not perform higher-order unification, as needed by the
980 rule @{thm [source=false] rangeI} in HOL. There are often
981 alternatives to such rules, for example @{thm [source=false]
984 \item Function variables may only be applied to parameters of the
985 subgoal. (This restriction arises because the prover does not use
986 higher-order unification.) If other function variables are present
987 then the prover will fail with the message \texttt{Function Var's
988 argument not a bound variable}.
990 \item Its proof strategy is more general than @{method fast} but can
991 be slower. If @{method blast} fails or seems to be running forever,
992 try @{method fast} and the other proof tools described below.
996 The optional integer argument specifies a bound for the number of
997 unsafe steps used in a proof. By default, @{method blast} starts
998 with a bound of 0 and increases it successively to 20. In contrast,
999 @{text "(blast lim)"} tries to prove the goal using a search bound
1000 of @{text "lim"}. Sometimes a slow proof using @{method blast} can
1001 be made much faster by supplying the successful search bound to this
1002 proof method instead.
1004 \item @{method auto} combines classical reasoning with
1005 simplification. It is intended for situations where there are a lot
1006 of mostly trivial subgoals; it proves all the easy ones, leaving the
1007 ones it cannot prove. Occasionally, attempting to prove the hard
1008 ones may take a long time.
1010 The optional depth arguments in @{text "(auto m n)"} refer to its
1011 builtin classical reasoning procedures: @{text m} (default 4) is for
1012 @{method blast}, which is tried first, and @{text n} (default 2) is
1013 for a slower but more general alternative that also takes wrappers
1016 \item @{method force} is intended to prove the first subgoal
1017 completely, using many fancy proof tools and performing a rather
1018 exhaustive search. As a result, proof attempts may take rather long
1021 \item @{method fast}, @{method best}, @{method slow} attempt to
1022 prove the first subgoal using sequent-style reasoning as explained
1023 before. Unlike @{method blast}, they construct proofs directly in
1026 There is a difference in search strategy and back-tracking: @{method
1027 fast} uses depth-first search and @{method best} uses best-first
1028 search (guided by a heuristic function: normally the total size of
1031 Method @{method slow} is like @{method fast}, but conducts a broader
1032 search: it may, when backtracking from a failed proof attempt, undo
1033 even the step of proving a subgoal by assumption.
1035 \item @{method fastsimp}, @{method slowsimp}, @{method bestsimp} are
1036 like @{method fast}, @{method slow}, @{method best}, respectively,
1037 but use the Simplifier as additional wrapper.
1039 \item @{method deepen} works by exhaustive search up to a certain
1040 depth. The start depth is 4 (unless specified explicitly), and the
1041 depth is increased iteratively up to 10. Unsafe rules are modified
1042 to preserve the formula they act on, so that it be used repeatedly.
1043 This method can prove more goals than @{method fast}, but is much
1044 slower, for example if the assumptions have many universal
1049 Any of the above methods support additional modifiers of the context
1050 of classical (and simplifier) rules, but the ones related to the
1051 Simplifier are explicitly prefixed by @{text simp} here. The
1052 semantics of these ad-hoc rule declarations is analogous to the
1053 attributes given before. Facts provided by forward chaining are
1054 inserted into the goal before commencing proof search.
1058 subsection {* Semi-automated methods *}
1060 text {* These proof methods may help in situations when the
1061 fully-automated tools fail. The result is a simpler subgoal that
1062 can be tackled by other means, such as by manual instantiation of
1065 \begin{matharray}{rcl}
1066 @{method_def safe} & : & @{text method} \\
1067 @{method_def clarify} & : & @{text method} \\
1068 @{method_def clarsimp} & : & @{text method} \\
1072 (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
1074 @@{method clarsimp} (@{syntax clasimpmod} * )
1079 \item @{method safe} repeatedly performs safe steps on all subgoals.
1080 It is deterministic, with at most one outcome.
1082 \item @{method clarify} performs a series of safe steps without
1083 splitting subgoals; see also @{ML clarify_step_tac}.
1085 \item @{method clarsimp} acts like @{method clarify}, but also does
1086 simplification. Note that if the Simplifier context includes a
1087 splitter for the premises, the subgoal may still be split.
1093 subsection {* Single-step tactics *}
1096 \begin{matharray}{rcl}
1097 @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
1098 @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
1099 @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
1100 @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
1101 @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
1104 These are the primitive tactics behind the (semi)automated proof
1105 methods of the Classical Reasoner. By calling them yourself, you
1106 can execute these procedures one step at a time.
1110 \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
1111 subgoal @{text i}. The safe wrapper tacticals are applied to a
1112 tactic that may include proof by assumption or Modus Ponens (taking
1113 care not to instantiate unknowns), or substitution.
1115 \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
1116 unknowns to be instantiated.
1118 \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
1119 procedure. The unsafe wrapper tacticals are applied to a tactic
1120 that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
1121 rule from the context.
1123 \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
1124 backtracking between using safe rules with instantiation (@{ML
1125 inst_step_tac}) and using unsafe rules. The resulting search space
1128 \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
1129 on subgoal @{text i}. No splitting step is applied; for example,
1130 the subgoal @{text "A \<and> B"} is left as a conjunction. Proof by
1131 assumption, Modus Ponens, etc., may be performed provided they do
1132 not instantiate unknowns. Assumptions of the form @{text "x = t"}
1133 may be eliminated. The safe wrapper tactical is applied.
1139 section {* Object-logic setup \label{sec:object-logic} *}
1142 \begin{matharray}{rcl}
1143 @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
1144 @{method_def atomize} & : & @{text method} \\
1145 @{attribute_def atomize} & : & @{text attribute} \\
1146 @{attribute_def rule_format} & : & @{text attribute} \\
1147 @{attribute_def rulify} & : & @{text attribute} \\
1150 The very starting point for any Isabelle object-logic is a ``truth
1151 judgment'' that links object-level statements to the meta-logic
1152 (with its minimal language of @{text prop} that covers universal
1153 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
1155 Common object-logics are sufficiently expressive to internalize rule
1156 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
1157 language. This is useful in certain situations where a rule needs
1158 to be viewed as an atomic statement from the meta-level perspective,
1159 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
1161 From the following language elements, only the @{method atomize}
1162 method and @{attribute rule_format} attribute are occasionally
1163 required by end-users, the rest is for those who need to setup their
1164 own object-logic. In the latter case existing formulations of
1165 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
1167 Generic tools may refer to the information provided by object-logic
1168 declarations internally.
1171 @@{command judgment} @{syntax constdecl}
1173 @@{attribute atomize} ('(' 'full' ')')?
1175 @@{attribute rule_format} ('(' 'noasm' ')')?
1180 \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
1181 @{text c} as the truth judgment of the current object-logic. Its
1182 type @{text \<sigma>} should specify a coercion of the category of
1183 object-level propositions to @{text prop} of the Pure meta-logic;
1184 the mixfix annotation @{text "(mx)"} would typically just link the
1185 object language (internally of syntactic category @{text logic})
1186 with that of @{text prop}. Only one @{command "judgment"}
1187 declaration may be given in any theory development.
1189 \item @{method atomize} (as a method) rewrites any non-atomic
1190 premises of a sub-goal, using the meta-level equations declared via
1191 @{attribute atomize} (as an attribute) beforehand. As a result,
1192 heavily nested goals become amenable to fundamental operations such
1193 as resolution (cf.\ the @{method (Pure) rule} method). Giving the ``@{text
1194 "(full)"}'' option here means to turn the whole subgoal into an
1195 object-statement (if possible), including the outermost parameters
1196 and assumptions as well.
1198 A typical collection of @{attribute atomize} rules for a particular
1199 object-logic would provide an internalization for each of the
1200 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
1201 Meta-level conjunction should be covered as well (this is
1202 particularly important for locales, see \secref{sec:locale}).
1204 \item @{attribute rule_format} rewrites a theorem by the equalities
1205 declared as @{attribute rulify} rules in the current object-logic.
1206 By default, the result is fully normalized, including assumptions
1207 and conclusions at any depth. The @{text "(no_asm)"} option
1208 restricts the transformation to the conclusion of a rule.
1210 In common object-logics (HOL, FOL, ZF), the effect of @{attribute
1211 rule_format} is to replace (bounded) universal quantification
1212 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
1213 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.