src/Doc/IsarRef/Generic.thy
 changeset 48985 5386df44a037 parent 48958 12afbf6eb7f9 child 50063 7e491da6bcbd
equal inserted replaced
48984:f51d4a302962 48985:5386df44a037

     1 theory Generic

     2 imports Base Main

     3 begin

     4

     5 chapter {* Generic tools and packages \label{ch:gen-tools} *}

     6

     7 section {* Configuration options \label{sec:config} *}

     8

     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

    18   this:

    19 *}

    20

    21 declare [[show_main_goal = false]]

    22

    23 notepad

    24 begin

    25   note [[show_main_goal = true]]

    26 end

    27

    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.

    32

    33   \begin{matharray}{rcll}

    34     @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\

    35   \end{matharray}

    36

    37   @{rail "

    38     @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?

    39   "}

    40

    41   \begin{description}

    42

    43   \item @{command "print_configs"} prints the available configuration

    44   options, with names, types, and current values.

    45

    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.

    50

    51   \end{description}

    52 *}

    53

    54

    55 section {* Basic proof tools *}

    56

    57 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}

    58

    59 text {*

    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} \\    71 \end{matharray}    72     73 @{rail "    74 (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}    75 ;    76 (@@{method erule} | @@{method drule} | @@{method frule})    77 ('(' @{syntax nat} ')')? @{syntax thmrefs}    78 ;    79 (@@{method intro} | @@{method elim}) @{syntax thmrefs}?    80 "}    81     82 \begin{description}    83     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.    88     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.    92     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    100 be performed here.    101     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    108 facts.    109     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.    115     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}).    119     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}).    123     124 \end{description}    125     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 unfolded} & : & @{text attribute} \\    131 @{attribute_def folded} & : & @{text attribute} \\    132 @{attribute_def abs_def} & : & @{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} \\    137 \end{matharray}    138     139 @{rail "    140 @@{attribute tagged} @{syntax name} @{syntax name}    141 ;    142 @@{attribute untagged} @{syntax name}    143 ;    144 @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}    145 ;    146 (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}    147 ;    148 @@{attribute rotated} @{syntax int}?    149 "}    150     151 \begin{description}    152     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.    158     159 \item @{attribute THEN}~@{text a} composes rules by resolution; it    160 resolves with the first premise of @{text a} (an alternative    161 position may be also specified). See also @{ML_op "RS"} in    162 \cite{isabelle-implementation}.    163     164 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute    165 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given    166 definitions throughout a rule.    167     168 \item @{attribute abs_def} turns an equation of the form @{prop "f x    169 y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method    170 simp} or @{method unfold} steps always expand it. This also works    171 for object-logic equality.    172     173 \item @{attribute rotated}~@{text n} rotate the premises of a    174 theorem by @{text n} (default 1).    175     176 \item @{attribute (Pure) elim_format} turns a destruction rule into    177 elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>    178 (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.    179     180 Note that the Classical Reasoner (\secref{sec:classical}) provides    181 its own version of this operation.    182     183 \item @{attribute standard} puts a theorem into the standard form of    184 object-rules at the outermost theory level. Note that this    185 operation violates the local proof context (including active    186 locales).    187     188 \item @{attribute no_vars} replaces schematic variables by free    189 ones; this is mainly for tuning output of pretty printed theorems.    190     191 \end{description}    192 *}    193     194     195 subsection {* Low-level equational reasoning *}    196     197 text {*    198 \begin{matharray}{rcl}    199 @{method_def subst} & : & @{text method} \\    200 @{method_def hypsubst} & : & @{text method} \\    201 @{method_def split} & : & @{text method} \\    202 \end{matharray}    203     204 @{rail "    205 @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}    206 ;    207 @@{method split} @{syntax thmrefs}    208 "}    209     210 These methods provide low-level facilities for equational reasoning    211 that are intended for specialized applications only. Normally,    212 single step calculations would be performed in a structured text    213 (see also \secref{sec:calculation}), while the Simplifier methods    214 provide the canonical way for automated normalization (see    215 \secref{sec:simplifier}).    216     217 \begin{description}    218     219 \item @{method subst}~@{text eq} performs a single substitution step    220 using rule @{text eq}, which may be either a meta or object    221 equality.    222     223 \item @{method subst}~@{text "(asm) eq"} substitutes in an    224 assumption.    225     226 \item @{method subst}~@{text "(i \<dots> j) eq"} performs several    227 substitutions in the conclusion. The numbers @{text i} to @{text j}    228 indicate the positions to substitute at. Positions are ordered from    229 the top of the term tree moving down from left to right. For    230 example, in @{text "(a + b) + (c + d)"} there are three positions    231 where commutativity of @{text "+"} is applicable: 1 refers to @{text    232 "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.    233     234 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping    235 (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may    236 assume all substitutions are performed simultaneously. Otherwise    237 the behaviour of @{text subst} is not specified.    238     239 \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the    240 substitutions in the assumptions. The positions refer to the    241 assumptions in order from left to right. For example, given in a    242 goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of    243 commutativity of @{text "+"} is the subterm @{text "a + b"} and    244 position 2 is the subterm @{text "c + d"}.    245     246 \item @{method hypsubst} performs substitution using some    247 assumption; this only works for equations of the form @{text "x =    248 t"} where @{text x} is a free or bound variable.    249     250 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case    251 splitting using the given rules. Splitting is performed in the    252 conclusion or some assumption of the subgoal, depending of the    253 structure of the rule.    254     255 Note that the @{method simp} method already involves repeated    256 application of split rules as declared in the current context, using    257 @{attribute split}, for example.    258     259 \end{description}    260 *}    261     262     263 subsection {* Further tactic emulations \label{sec:tactics} *}    264     265 text {*    266 The following improper proof methods emulate traditional tactics.    267 These admit direct access to the goal state, which is normally    268 considered harmful! In particular, this may involve both numbered    269 goal addressing (default 1), and dynamic instantiation within the    270 scope of some subgoal.    271     272 \begin{warn}    273 Dynamic instantiations refer to universally quantified parameters    274 of a subgoal (the dynamic context) rather than fixed variables and    275 term abbreviations of a (static) Isar context.    276 \end{warn}    277     278 Tactic emulation methods, unlike their ML counterparts, admit    279 simultaneous instantiation from both dynamic and static contexts.    280 If names occur in both contexts goal parameters hide locally fixed    281 variables. Likewise, schematic variables refer to term    282 abbreviations, if present in the static context. Otherwise the    283 schematic variable is interpreted as a schematic variable and left    284 to be solved by unification with certain parts of the subgoal.    285     286 Note that the tactic emulation proof methods in Isabelle/Isar are    287 consistently named @{text foo_tac}. Note also that variable names    288 occurring on left hand sides of instantiations must be preceded by a    289 question mark if they coincide with a keyword or contain dots. This    290 is consistent with the attribute @{attribute "where"} (see    291 \secref{sec:pure-meth-att}).    292     293 \begin{matharray}{rcl}    294 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\    295 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\    296 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\    297 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\    298 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\    299 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\    300 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\    301 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\    302 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\    303 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\    304 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\    305 \end{matharray}    306     307 @{rail "    308 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |    309 @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\    310 ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )    311 ;    312 @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)    313 ;    314 @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)    315 ;    316 @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?    317 ;    318 (@@{method tactic} | @@{method raw_tactic}) @{syntax text}    319 ;    320     321 dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')    322 "}    323     324 \begin{description}    325     326 \item @{method rule_tac} etc. do resolution of rules with explicit    327 instantiation. This works the same way as the ML tactics @{ML    328 res_inst_tac} etc. (see \cite{isabelle-implementation})    329     330 Multiple rules may be only given if there is no instantiation; then    331 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see    332 \cite{isabelle-implementation}).    333     334 \item @{method cut_tac} inserts facts into the proof state as    335 assumption of a subgoal; instantiations may be given as well. Note    336 that the scope of schematic variables is spread over the main goal    337 statement and rule premises are turned into new subgoals. This is    338 in contrast to the regular method @{method insert} which inserts    339 closed rule statements.    340     341 \item @{method thin_tac}~@{text \<phi>} deletes the specified premise    342 from a subgoal. Note that @{text \<phi>} may contain schematic    343 variables, to abbreviate the intended proposition; the first    344 matching subgoal premise will be deleted. Removing useless premises    345 from a subgoal increases its readability and can make search tactics    346 run faster.    347     348 \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions    349 @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same    350 as new subgoals (in the original context).    351     352 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a    353 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the    354 \emph{suffix} of variables.    355     356 \item @{method rotate_tac}~@{text n} rotates the premises of a    357 subgoal by @{text n} positions: from right to left if @{text n} is    358 positive, and from left to right if @{text n} is negative; the    359 default value is 1.    360     361 \item @{method tactic}~@{text "text"} produces a proof method from    362 any ML text of type @{ML_type tactic}. Apart from the usual ML    363 environment and the current proof context, the ML code may refer to    364 the locally bound values @{ML_text facts}, which indicates any    365 current facts used for forward-chaining.    366     367 \item @{method raw_tactic} is similar to @{method tactic}, but    368 presents the goal state in its raw internal form, where simultaneous    369 subgoals appear as conjunction of the logical framework instead of    370 the usual split into several subgoals. While feature this is useful    371 for debugging of complex method definitions, it should not never    372 appear in production theories.    373     374 \end{description}    375 *}    376     377     378 section {* The Simplifier \label{sec:simplifier} *}    379     380 subsection {* Simplification methods *}    381     382 text {*    383 \begin{matharray}{rcl}    384 @{method_def simp} & : & @{text method} \\    385 @{method_def simp_all} & : & @{text method} \\    386 \end{matharray}    387     388 @{rail "    389 (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )    390 ;    391     392 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'    393 ;    394 @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |    395 'split' (() | 'add' | 'del')) ':' @{syntax thmrefs}    396 "}    397     398 \begin{description}    399     400 \item @{method simp} invokes the Simplifier, after declaring    401 additional rules according to the arguments given. Note that the    402 @{text only} modifier first removes all other rewrite rules,    403 congruences, and looper tactics (including splits), and then behaves    404 like @{text add}.    405     406 \medskip The @{text cong} modifiers add or delete Simplifier    407 congruence rules (see also \secref{sec:simp-cong}), the default is    408 to add.    409     410 \medskip The @{text split} modifiers add or delete rules for the    411 Splitter (see also \cite{isabelle-ref}), the default is to add.    412 This works only if the Simplifier method has been properly setup to    413 include the Splitter (all major object logics such HOL, HOLCF, FOL,    414 ZF do this already).    415     416 \item @{method simp_all} is similar to @{method simp}, but acts on    417 all goals (backwards from the last to the first one).    418     419 \end{description}    420     421 By default the Simplifier methods take local assumptions fully into    422 account, using equational assumptions in the subsequent    423 normalization process, or simplifying assumptions themselves (cf.\    424 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured    425 proofs this is usually quite well behaved in practice: just the    426 local premises of the actual goal are involved, additional facts may    427 be inserted via explicit forward-chaining (via @{command "then"},    428 @{command "from"}, @{command "using"} etc.).    429     430 Additional Simplifier options may be specified to tune the behavior    431 further (mostly for unstructured scripts with many accidental local    432 facts): @{text "(no_asm)"}'' means assumptions are ignored    433 completely (cf.\ @{ML simp_tac}), @{text "(no_asm_simp)"}'' means    434 assumptions are used in the simplification of the conclusion but are    435 not themselves simplified (cf.\ @{ML asm_simp_tac}), and @{text    436 "(no_asm_use)"}'' means assumptions are simplified but are not used    437 in the simplification of each other or the conclusion (cf.\ @{ML    438 full_simp_tac}). For compatibility reasons, there is also an option    439 @{text "(asm_lr)"}'', which means that an assumption is only used    440 for simplifying assumptions which are to the right of it (cf.\ @{ML    441 asm_lr_simp_tac}).    442     443 The configuration option @{text "depth_limit"} limits the number of    444 recursive invocations of the simplifier during conditional    445 rewriting.    446     447 \medskip The Splitter package is usually configured to work as part    448 of the Simplifier. The effect of repeatedly applying @{ML    449 split_tac} can be simulated by @{text "(simp only: split:    450 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split}    451 method available for single-step case splitting.    452 *}    453     454     455 subsection {* Declaring rules *}    456     457 text {*    458 \begin{matharray}{rcl}    459 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\    460 @{attribute_def simp} & : & @{text attribute} \\    461 @{attribute_def split} & : & @{text attribute} \\    462 \end{matharray}    463     464 @{rail "    465 (@@{attribute simp} | @@{attribute split}) (() | 'add' | 'del')    466 "}    467     468 \begin{description}    469     470 \item @{command "print_simpset"} prints the collection of rules    471 declared to the Simplifier, which is also known as simpset''    472 internally \cite{isabelle-ref}.    473     474 \item @{attribute simp} declares simplification rules.    475     476 \item @{attribute split} declares case split rules.    477     478 \end{description}    479 *}    480     481     482 subsection {* Congruence rules\label{sec:simp-cong} *}    483     484 text {*    485 \begin{matharray}{rcl}    486 @{attribute_def cong} & : & @{text attribute} \\    487 \end{matharray}    488     489 @{rail "    490 @@{attribute cong} (() | 'add' | 'del')    491 "}    492     493 \begin{description}    494     495 \item @{attribute cong} declares congruence rules to the Simplifier    496 context.    497     498 \end{description}    499     500 Congruence rules are equalities of the form @{text [display]    501 "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}    502     503 This controls the simplification of the arguments of @{text f}. For    504 example, some arguments can be simplified under additional    505 assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>    506 (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}    507     508 Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts    509 rewrite rules from it when simplifying @{text "?P\<^sub>2"}. Such local    510 assumptions are effective for rewriting formulae such as @{text "x =    511 0 \<longrightarrow> y + x = y"}.    512     513 %FIXME    514 %The local assumptions are also provided as theorems to the solver;    515 %see \secref{sec:simp-solver} below.    516     517 \medskip The following congruence rule for bounded quantifiers also    518 supplies contextual information --- about the bound variable:    519 @{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>    520 (\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"}    521     522 \medskip This congruence rule for conditional expressions can    523 supply contextual information for simplifying the arms:    524 @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>    525 (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}    526     527 A congruence rule can also \emph{prevent} simplification of some    528 arguments. Here is an alternative congruence rule for conditional    529 expressions that conforms to non-strict functional evaluation:    530 @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}    531     532 Only the first argument is simplified; the others remain unchanged.    533 This can make simplification much faster, but may require an extra    534 case split over the condition @{text "?q"} to prove the goal.    535 *}    536     537     538 subsection {* Simplification procedures *}    539     540 text {* Simplification procedures are ML functions that produce proven    541 rewrite rules on demand. They are associated with higher-order    542 patterns that approximate the left-hand sides of equations. The    543 Simplifier first matches the current redex against one of the LHS    544 patterns; if this succeeds, the corresponding ML function is    545 invoked, passing the Simplifier context and redex term. Thus rules    546 may be specifically fashioned for particular situations, resulting    547 in a more powerful mechanism than term rewriting by a fixed set of    548 rules.    549     550 Any successful result needs to be a (possibly conditional) rewrite    551 rule @{text "t \<equiv> u"} that is applicable to the current redex. The    552 rule will be applied just as any ordinary rewrite rule. It is    553 expected to be already in \emph{internal form}, bypassing the    554 automatic preprocessing of object-level equivalences.    555     556 \begin{matharray}{rcl}    557 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\    558 simproc & : & @{text attribute} \\    559 \end{matharray}    560     561 @{rail "    562 @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='    563 @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?    564 ;    565     566 @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)    567 "}    568     569 \begin{description}    570     571 \item @{command "simproc_setup"} defines a named simplification    572 procedure that is invoked by the Simplifier whenever any of the    573 given term patterns match the current redex. The implementation,    574 which is provided as ML source text, needs to be of type @{ML_type    575 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type    576 cterm} represents the current redex @{text r} and the result is    577 supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a    578 generalized version), or @{ML NONE} to indicate failure. The    579 @{ML_type simpset} argument holds the full context of the current    580 Simplifier invocation, including the actual Isar proof context. The    581 @{ML_type morphism} informs about the difference of the original    582 compilation context wrt.\ the one of the actual application later    583 on. The optional @{keyword "identifier"} specifies theorems that    584 represent the logical content of the abstract theory of this    585 simproc.    586     587 Morphisms and identifiers are only relevant for simprocs that are    588 defined within a local target context, e.g.\ in a locale.    589     590 \item @{text "simproc add: name"} and @{text "simproc del: name"}    591 add or delete named simprocs to the current Simplifier context. The    592 default is to add a simproc. Note that @{command "simproc_setup"}    593 already adds the new simproc to the subsequent context.    594     595 \end{description}    596 *}    597     598     599 subsubsection {* Example *}    600     601 text {* The following simplification procedure for @{thm    602 [source=false, show_types] unit_eq} in HOL performs fine-grained    603 control over rule application, beyond higher-order pattern matching.    604 Declaring @{thm unit_eq} as @{attribute simp} directly would make    605 the simplifier loop! Note that a version of this simplification    606 procedure is already active in Isabelle/HOL. *}    607     608 simproc_setup unit ("x::unit") = {*    609 fn _ => fn _ => fn ct =>    610 if HOLogic.is_unit (term_of ct) then NONE    611 else SOME (mk_meta_eq @{thm unit_eq})    612 *}    613     614 text {* Since the Simplifier applies simplification procedures    615 frequently, it is important to make the failure check in ML    616 reasonably fast. *}    617     618     619 subsection {* Forward simplification *}    620     621 text {*    622 \begin{matharray}{rcl}    623 @{attribute_def simplified} & : & @{text attribute} \\    624 \end{matharray}    625     626 @{rail "    627 @@{attribute simplified} opt? @{syntax thmrefs}?    628 ;    629     630 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'    631 "}    632     633 \begin{description}    634     635 \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to    636 be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,    637 a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.    638 The result is fully simplified by default, including assumptions and    639 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in    640 the same way as the for the @{text simp} method.    641     642 Note that forward simplification restricts the simplifier to its    643 most basic operation of term rewriting; solver and looper tactics    644 \cite{isabelle-ref} are \emph{not} involved here. The @{text    645 simplified} attribute should be only rarely required under normal    646 circumstances.    647     648 \end{description}    649 *}    650     651     652 section {* The Classical Reasoner \label{sec:classical} *}    653     654 subsection {* Basic concepts *}    655     656 text {* Although Isabelle is generic, many users will be working in    657 some extension of classical first-order logic. Isabelle/ZF is built    658 upon theory FOL, while Isabelle/HOL conceptually contains    659 first-order logic as a fragment. Theorem-proving in predicate logic    660 is undecidable, but many automated strategies have been developed to    661 assist in this task.    662     663 Isabelle's classical reasoner is a generic package that accepts    664 certain information about a logic and delivers a suite of automatic    665 proof tools, based on rules that are classified and declared in the    666 context. These proof procedures are slow and simplistic compared    667 with high-end automated theorem provers, but they can save    668 considerable time and effort in practice. They can prove theorems    669 such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few    670 milliseconds (including full proof reconstruction): *}    671     672 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)"    673 by blast    674     675 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)"    676 by blast    677     678 text {* The proof tools are generic. They are not restricted to    679 first-order logic, and have been heavily used in the development of    680 the Isabelle/HOL library and applications. The tactics can be    681 traced, and their components can be called directly; in this manner,    682 any proof can be viewed interactively. *}    683     684     685 subsubsection {* The sequent calculus *}    686     687 text {* Isabelle supports natural deduction, which is easy to use for    688 interactive proof. But natural deduction does not easily lend    689 itself to automation, and has a bias towards intuitionism. For    690 certain proofs in classical logic, it can not be called natural.    691 The \emph{sequent calculus}, a generalization of natural deduction,    692 is easier to automate.    693     694 A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}    695 and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order    696 logic, sequents can equivalently be made from lists or multisets of    697 formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is    698 \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>    699 Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which    700 is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A    701 sequent is \textbf{basic} if its left and right sides have a common    702 formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially    703 valid.    704     705 Sequent rules are classified as \textbf{right} or \textbf{left},    706 indicating which side of the @{text "\<turnstile>"} symbol they operate on.    707 Rules that operate on the right side are analogous to natural    708 deduction's introduction rules, and left rules are analogous to    709 elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"}    710 is the rule    711 \[    712 \infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}}    713$

   714   Applying the rule backwards, this breaks down some implication on

   715   the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for

   716   the sets of formulae that are unaffected by the inference.  The

   717   analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the

   718   single rule

   719   $    720 \infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}}    721$

   722   This breaks down some disjunction on the right side, replacing it by

   723   both disjuncts.  Thus, the sequent calculus is a kind of

   724   multiple-conclusion logic.

   725

   726   To illustrate the use of multiple formulae on the right, let us

   727   prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}.  Working

   728   backwards, we reduce this formula to a basic sequent:

   729   $    730 \infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}}    731 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}}    732 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}}    733 {@{text "P, Q \<turnstile> Q, P"}}}}    734$

   735

   736   This example is typical of the sequent calculus: start with the

   737   desired theorem and apply rules backwards in a fairly arbitrary

   738   manner.  This yields a surprisingly effective proof procedure.

   739   Quantifiers add only few complications, since Isabelle handles

   740   parameters and schematic variables.  See \cite[Chapter

   741   10]{paulson-ml2} for further discussion.  *}

   742

   743

   744 subsubsection {* Simulating sequents by natural deduction *}

   745

   746 text {* Isabelle can represent sequents directly, as in the

   747   object-logic LK.  But natural deduction is easier to work with, and

   748   most object-logics employ it.  Fortunately, we can simulate the

   749   sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula

   750   @{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

   751   the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary.

   752   Elim-resolution plays a key role in simulating sequent proofs.

   753

   754   We can easily handle reasoning on the left.  Elim-resolution with

   755   the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves

   756   a similar effect as the corresponding sequent rules.  For the other

   757   connectives, we use sequent-style elimination rules instead of

   758   destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}.

   759   But note that the rule @{text "(\<not>L)"} has no effect under our

   760   representation of sequents!

   761   $    762 \infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}}    763$

   764

   765   What about reasoning on the right?  Introduction rules can only

   766   affect the formula in the conclusion, namely @{text "Q\<^sub>1"}.  The

   767   other right-side formulae are represented as negated assumptions,

   768   @{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}.  In order to operate on one of these, it

   769   must first be exchanged with @{text "Q\<^sub>1"}.  Elim-resolution with the

   770   @{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"}

   771

   772   To ensure that swaps occur only when necessary, each introduction

   773   rule is converted into a swapped form: it is resolved with the

   774   second premise of @{text "(swap)"}.  The swapped form of @{text

   775   "(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is

   776   @{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"}

   777

   778   Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is

   779   @{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"}

   780

   781   Swapped introduction rules are applied using elim-resolution, which

   782   deletes the negated formula.  Our representation of sequents also

   783   requires the use of ordinary introduction rules.  If we had no

   784   regard for readability of intermediate goal states, we could treat

   785   the right side more uniformly by representing sequents as @{text

   786   [display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"}

   787 *}

   788

   789

   790 subsubsection {* Extra rules for the sequent calculus *}

   791

   792 text {* As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and

   793   @{text "(\<forall>E)"} must be replaced by sequent-style elimination rules.

   794   In addition, we need rules to embody the classical equivalence

   795   between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}.  The introduction

   796   rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates

   797   @{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"}

   798

   799   The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display]

   800   "(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"}

   801

   802   Quantifier replication also requires special rules.  In classical

   803   logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"};

   804   the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual:

   805   $    806 \infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}}    807 \qquad    808 \infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}    809$

   810   Thus both kinds of quantifier may be replicated.  Theorems requiring

   811   multiple uses of a universal formula are easy to invent; consider

   812   @{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any

   813   @{text "n > 1"}.  Natural examples of the multiple use of an

   814   existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x

   815   \<longrightarrow> P y"}.

   816

   817   Forgoing quantifier replication loses completeness, but gains

   818   decidability, since the search space becomes finite.  Many useful

   819   theorems can be proved without replication, and the search generally

   820   delivers its verdict in a reasonable time.  To adopt this approach,

   821   represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and

   822   @{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"},

   823   respectively, and put @{text "(\<forall>E)"} into elimination form: @{text

   824   [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"}

   825

   826   Elim-resolution with this rule will delete the universal formula

   827   after a single use.  To replicate universal quantifiers, replace the

   828   rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"}

   829

   830   To replicate existential quantifiers, replace @{text "(\<exists>I)"} by

   831   @{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"}

   832

   833   All introduction rules mentioned above are also useful in swapped

   834   form.

   835

   836   Replication makes the search space infinite; we must apply the rules

   837   with care.  The classical reasoner distinguishes between safe and

   838   unsafe rules, applying the latter only when there is no alternative.

   839   Depth-first search may well go down a blind alley; best-first search

   840   is better behaved in an infinite search space.  However, quantifier

   841   replication is too expensive to prove any but the simplest theorems.

   842 *}

   843

   844

   845 subsection {* Rule declarations *}

   846

   847 text {* The proof tools of the Classical Reasoner depend on

   848   collections of rules declared in the context, which are classified

   849   as introduction, elimination or destruction and as \emph{safe} or

   850   \emph{unsafe}.  In general, safe rules can be attempted blindly,

   851   while unsafe rules must be used with care.  A safe rule must never

   852   reduce a provable goal to an unprovable set of subgoals.

   853

   854   The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P

   855   \<or> Q"} to @{text "P"}, which might turn out as premature choice of an

   856   unprovable subgoal.  Any rule is unsafe whose premises contain new

   857   unknowns.  The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is

   858   unsafe, since it is applied via elim-resolution, which discards the

   859   assumption @{text "\<forall>x. P x"} and replaces it by the weaker

   860   assumption @{text "P t"}.  The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is

   861   unsafe for similar reasons.  The quantifier duplication rule @{text

   862   "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:

   863   since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to

   864   looping.  In classical first-order logic, all rules are safe except

   865   those mentioned above.

   866

   867   The safe~/ unsafe distinction is vague, and may be regarded merely

   868   as a way of giving some rules priority over others.  One could argue

   869   that @{text "(\<or>E)"} is unsafe, because repeated application of it

   870   could generate exponentially many subgoals.  Induction rules are

   871   unsafe because inductive proofs are difficult to set up

   872   automatically.  Any inference is unsafe that instantiates an unknown

   873   in the proof state --- thus matching must be used, rather than

   874   unification.  Even proof by assumption is unsafe if it instantiates

   875   unknowns shared with other subgoals.

   876

   877   \begin{matharray}{rcl}

   878     @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

   879     @{attribute_def intro} & : & @{text attribute} \\

   880     @{attribute_def elim} & : & @{text attribute} \\

   881     @{attribute_def dest} & : & @{text attribute} \\

   882     @{attribute_def rule} & : & @{text attribute} \\

   883     @{attribute_def iff} & : & @{text attribute} \\

   884     @{attribute_def swapped} & : & @{text attribute} \\

   885   \end{matharray}

   886

   887   @{rail "

   888     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?

   889     ;

   890     @@{attribute rule} 'del'

   891     ;

   892     @@{attribute iff} (((() | 'add') '?'?) | 'del')

   893   "}

   894

   895   \begin{description}

   896

   897   \item @{command "print_claset"} prints the collection of rules

   898   declared to the Classical Reasoner, i.e.\ the @{ML_type claset}

   899   within the context.

   900

   901   \item @{attribute intro}, @{attribute elim}, and @{attribute dest}

   902   declare introduction, elimination, and destruction rules,

   903   respectively.  By default, rules are considered as \emph{unsafe}

   904   (i.e.\ not applied blindly without backtracking), while @{text

   905   "!"}'' classifies as \emph{safe}.  Rule declarations marked by

   906   @{text "?"}'' coincide with those of Isabelle/Pure, cf.\

   907   \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps

   908   of the @{method rule} method).  The optional natural number

   909   specifies an explicit weight argument, which is ignored by the

   910   automated reasoning tools, but determines the search order of single

   911   rule steps.

   912

   913   Introduction rules are those that can be applied using ordinary

   914   resolution.  Their swapped forms are generated internally, which

   915   will be applied using elim-resolution.  Elimination rules are

   916   applied using elim-resolution.  Rules are sorted by the number of

   917   new subgoals they will yield; rules that generate the fewest

   918   subgoals will be tried first.  Otherwise, later declarations take

   919   precedence over earlier ones.

   920

   921   Rules already present in the context with the same classification

   922   are ignored.  A warning is printed if the rule has already been

   923   added with some other classification, but the rule is added anyway

   924   as requested.

   925

   926   \item @{attribute rule}~@{text del} deletes all occurrences of a

   927   rule from the classical context, regardless of its classification as

   928   introduction~/ elimination~/ destruction and safe~/ unsafe.

   929

   930   \item @{attribute iff} declares logical equivalences to the

   931   Simplifier and the Classical reasoner at the same time.

   932   Non-conditional rules result in a safe introduction and elimination

   933   pair; conditional ones are considered unsafe.  Rules with negative

   934   conclusion are automatically inverted (using @{text "\<not>"}-elimination

   935   internally).

   936

   937   The @{text "?"}'' version of @{attribute iff} declares rules to

   938   the Isabelle/Pure context only, and omits the Simplifier

   939   declaration.

   940

   941   \item @{attribute swapped} turns an introduction rule into an

   942   elimination, by resolving with the classical swap principle @{text

   943   "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position.  This is mainly for

   944   illustrative purposes: the Classical Reasoner already swaps rules

   945   internally as explained above.

   946

   947   \end{description}

   948 *}

   949

   950

   951 subsection {* Structured methods *}

   952

   953 text {*

   954   \begin{matharray}{rcl}

   955     @{method_def rule} & : & @{text method} \\

   956     @{method_def contradiction} & : & @{text method} \\

   957   \end{matharray}

   958

   959   @{rail "

   960     @@{method rule} @{syntax thmrefs}?

   961   "}

   962

   963   \begin{description}

   964

   965   \item @{method rule} as offered by the Classical Reasoner is a

   966   refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both

   967   versions work the same, but the classical version observes the

   968   classical rule context in addition to that of Isabelle/Pure.

   969

   970   Common object logics (HOL, ZF, etc.) declare a rich collection of

   971   classical rules (even if these would qualify as intuitionistic

   972   ones), but only few declarations to the rule context of

   973   Isabelle/Pure (\secref{sec:pure-meth-att}).

   974

   975   \item @{method contradiction} solves some goal by contradiction,

   976   deriving any result from both @{text "\<not> A"} and @{text A}.  Chained

   977   facts, which are guaranteed to participate, may appear in either

   978   order.

   979

   980   \end{description}

   981 *}

   982

   983

   984 subsection {* Automated methods *}

   985

   986 text {*

   987   \begin{matharray}{rcl}

   988     @{method_def blast} & : & @{text method} \\

   989     @{method_def auto} & : & @{text method} \\

   990     @{method_def force} & : & @{text method} \\

   991     @{method_def fast} & : & @{text method} \\

   992     @{method_def slow} & : & @{text method} \\

   993     @{method_def best} & : & @{text method} \\

   994     @{method_def fastforce} & : & @{text method} \\

   995     @{method_def slowsimp} & : & @{text method} \\

   996     @{method_def bestsimp} & : & @{text method} \\

   997     @{method_def deepen} & : & @{text method} \\

   998   \end{matharray}

   999

  1000   @{rail "

  1001     @@{method blast} @{syntax nat}? (@{syntax clamod} * )

  1002     ;

  1003     @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )

  1004     ;

  1005     @@{method force} (@{syntax clasimpmod} * )

  1006     ;

  1007     (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * )

  1008     ;

  1009     (@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp})

  1010       (@{syntax clasimpmod} * )

  1011     ;

  1012     @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )

  1013     ;

  1014     @{syntax_def clamod}:

  1015       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}

  1016     ;

  1017     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |

  1018       ('cong' | 'split') (() | 'add' | 'del') |

  1019       'iff' (((() | 'add') '?'?) | 'del') |

  1020       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}

  1021   "}

  1022

  1023   \begin{description}

  1024

  1025   \item @{method blast} is a separate classical tableau prover that

  1026   uses the same classical rule declarations as explained before.

  1027

  1028   Proof search is coded directly in ML using special data structures.

  1029   A successful proof is then reconstructed using regular Isabelle

  1030   inferences.  It is faster and more powerful than the other classical

  1031   reasoning tools, but has major limitations too.

  1032

  1033   \begin{itemize}

  1034

  1035   \item It does not use the classical wrapper tacticals, such as the

  1036   integration with the Simplifier of @{method fastforce}.

  1037

  1038   \item It does not perform higher-order unification, as needed by the

  1039   rule @{thm [source=false] rangeI} in HOL.  There are often

  1040   alternatives to such rules, for example @{thm [source=false]

  1041   range_eqI}.

  1042

  1043   \item Function variables may only be applied to parameters of the

  1044   subgoal.  (This restriction arises because the prover does not use

  1045   higher-order unification.)  If other function variables are present

  1046   then the prover will fail with the message \texttt{Function Var's

  1047   argument not a bound variable}.

  1048

  1049   \item Its proof strategy is more general than @{method fast} but can

  1050   be slower.  If @{method blast} fails or seems to be running forever,

  1051   try @{method fast} and the other proof tools described below.

  1052

  1053   \end{itemize}

  1054

  1055   The optional integer argument specifies a bound for the number of

  1056   unsafe steps used in a proof.  By default, @{method blast} starts

  1057   with a bound of 0 and increases it successively to 20.  In contrast,

  1058   @{text "(blast lim)"} tries to prove the goal using a search bound

  1059   of @{text "lim"}.  Sometimes a slow proof using @{method blast} can

  1060   be made much faster by supplying the successful search bound to this

  1061   proof method instead.

  1062

  1063   \item @{method auto} combines classical reasoning with

  1064   simplification.  It is intended for situations where there are a lot

  1065   of mostly trivial subgoals; it proves all the easy ones, leaving the

  1066   ones it cannot prove.  Occasionally, attempting to prove the hard

  1067   ones may take a long time.

  1068

  1069   The optional depth arguments in @{text "(auto m n)"} refer to its

  1070   builtin classical reasoning procedures: @{text m} (default 4) is for

  1071   @{method blast}, which is tried first, and @{text n} (default 2) is

  1072   for a slower but more general alternative that also takes wrappers

  1073   into account.

  1074

  1075   \item @{method force} is intended to prove the first subgoal

  1076   completely, using many fancy proof tools and performing a rather

  1077   exhaustive search.  As a result, proof attempts may take rather long

  1078   or diverge easily.

  1079

  1080   \item @{method fast}, @{method best}, @{method slow} attempt to

  1081   prove the first subgoal using sequent-style reasoning as explained

  1082   before.  Unlike @{method blast}, they construct proofs directly in

  1083   Isabelle.

  1084

  1085   There is a difference in search strategy and back-tracking: @{method

  1086   fast} uses depth-first search and @{method best} uses best-first

  1087   search (guided by a heuristic function: normally the total size of

  1088   the proof state).

  1089

  1090   Method @{method slow} is like @{method fast}, but conducts a broader

  1091   search: it may, when backtracking from a failed proof attempt, undo

  1092   even the step of proving a subgoal by assumption.

  1093

  1094   \item @{method fastforce}, @{method slowsimp}, @{method bestsimp}

  1095   are like @{method fast}, @{method slow}, @{method best},

  1096   respectively, but use the Simplifier as additional wrapper. The name

  1097   @{method fastforce}, reflects the behaviour of this popular method

  1098   better without requiring an understanding of its implementation.

  1099

  1100   \item @{method deepen} works by exhaustive search up to a certain

  1101   depth.  The start depth is 4 (unless specified explicitly), and the

  1102   depth is increased iteratively up to 10.  Unsafe rules are modified

  1103   to preserve the formula they act on, so that it be used repeatedly.

  1104   This method can prove more goals than @{method fast}, but is much

  1105   slower, for example if the assumptions have many universal

  1106   quantifiers.

  1107

  1108   \end{description}

  1109

  1110   Any of the above methods support additional modifiers of the context

  1111   of classical (and simplifier) rules, but the ones related to the

  1112   Simplifier are explicitly prefixed by @{text simp} here.  The

  1113   semantics of these ad-hoc rule declarations is analogous to the

  1114   attributes given before.  Facts provided by forward chaining are

  1115   inserted into the goal before commencing proof search.

  1116 *}

  1117

  1118

  1119 subsection {* Semi-automated methods *}

  1120

  1121 text {* These proof methods may help in situations when the

  1122   fully-automated tools fail.  The result is a simpler subgoal that

  1123   can be tackled by other means, such as by manual instantiation of

  1124   quantifiers.

  1125

  1126   \begin{matharray}{rcl}

  1127     @{method_def safe} & : & @{text method} \\

  1128     @{method_def clarify} & : & @{text method} \\

  1129     @{method_def clarsimp} & : & @{text method} \\

  1130   \end{matharray}

  1131

  1132   @{rail "

  1133     (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )

  1134     ;

  1135     @@{method clarsimp} (@{syntax clasimpmod} * )

  1136   "}

  1137

  1138   \begin{description}

  1139

  1140   \item @{method safe} repeatedly performs safe steps on all subgoals.

  1141   It is deterministic, with at most one outcome.

  1142

  1143   \item @{method clarify} performs a series of safe steps without

  1144   splitting subgoals; see also @{ML clarify_step_tac}.

  1145

  1146   \item @{method clarsimp} acts like @{method clarify}, but also does

  1147   simplification.  Note that if the Simplifier context includes a

  1148   splitter for the premises, the subgoal may still be split.

  1149

  1150   \end{description}

  1151 *}

  1152

  1153

  1154 subsection {* Single-step tactics *}

  1155

  1156 text {*

  1157   \begin{matharray}{rcl}

  1158     @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\

  1159     @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\

  1160     @{index_ML step_tac: "Proof.context -> int -> tactic"} \\

  1161     @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\

  1162     @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\

  1163   \end{matharray}

  1164

  1165   These are the primitive tactics behind the (semi)automated proof

  1166   methods of the Classical Reasoner.  By calling them yourself, you

  1167   can execute these procedures one step at a time.

  1168

  1169   \begin{description}

  1170

  1171   \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on

  1172   subgoal @{text i}.  The safe wrapper tacticals are applied to a

  1173   tactic that may include proof by assumption or Modus Ponens (taking

  1174   care not to instantiate unknowns), or substitution.

  1175

  1176   \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows

  1177   unknowns to be instantiated.

  1178

  1179   \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof

  1180   procedure.  The unsafe wrapper tacticals are applied to a tactic

  1181   that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe

  1182   rule from the context.

  1183

  1184   \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows

  1185   backtracking between using safe rules with instantiation (@{ML

  1186   inst_step_tac}) and using unsafe rules.  The resulting search space

  1187   is larger.

  1188

  1189   \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step

  1190   on subgoal @{text i}.  No splitting step is applied; for example,

  1191   the subgoal @{text "A \<and> B"} is left as a conjunction.  Proof by

  1192   assumption, Modus Ponens, etc., may be performed provided they do

  1193   not instantiate unknowns.  Assumptions of the form @{text "x = t"}

  1194   may be eliminated.  The safe wrapper tactical is applied.

  1195

  1196   \end{description}

  1197 *}

  1198

  1199

  1200 section {* Object-logic setup \label{sec:object-logic} *}

  1201

  1202 text {*

  1203   \begin{matharray}{rcl}

  1204     @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\

  1205     @{method_def atomize} & : & @{text method} \\

  1206     @{attribute_def atomize} & : & @{text attribute} \\

  1207     @{attribute_def rule_format} & : & @{text attribute} \\

  1208     @{attribute_def rulify} & : & @{text attribute} \\

  1209   \end{matharray}

  1210

  1211   The very starting point for any Isabelle object-logic is a truth

  1212   judgment'' that links object-level statements to the meta-logic

  1213   (with its minimal language of @{text prop} that covers universal

  1214   quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).

  1215

  1216   Common object-logics are sufficiently expressive to internalize rule

  1217   statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own

  1218   language.  This is useful in certain situations where a rule needs

  1219   to be viewed as an atomic statement from the meta-level perspective,

  1220   e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.

  1221

  1222   From the following language elements, only the @{method atomize}

  1223   method and @{attribute rule_format} attribute are occasionally

  1224   required by end-users, the rest is for those who need to setup their

  1225   own object-logic.  In the latter case existing formulations of

  1226   Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.

  1227

  1228   Generic tools may refer to the information provided by object-logic

  1229   declarations internally.

  1230

  1231   @{rail "

  1232     @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?

  1233     ;

  1234     @@{attribute atomize} ('(' 'full' ')')?

  1235     ;

  1236     @@{attribute rule_format} ('(' 'noasm' ')')?

  1237   "}

  1238

  1239   \begin{description}

  1240

  1241   \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant

  1242   @{text c} as the truth judgment of the current object-logic.  Its

  1243   type @{text \<sigma>} should specify a coercion of the category of

  1244   object-level propositions to @{text prop} of the Pure meta-logic;

  1245   the mixfix annotation @{text "(mx)"} would typically just link the

  1246   object language (internally of syntactic category @{text logic})

  1247   with that of @{text prop}.  Only one @{command "judgment"}

  1248   declaration may be given in any theory development.

  1249

  1250   \item @{method atomize} (as a method) rewrites any non-atomic

  1251   premises of a sub-goal, using the meta-level equations declared via

  1252   @{attribute atomize} (as an attribute) beforehand.  As a result,

  1253   heavily nested goals become amenable to fundamental operations such

  1254   as resolution (cf.\ the @{method (Pure) rule} method).  Giving the @{text

  1255   "(full)"}'' option here means to turn the whole subgoal into an

  1256   object-statement (if possible), including the outermost parameters

  1257   and assumptions as well.

  1258

  1259   A typical collection of @{attribute atomize} rules for a particular

  1260   object-logic would provide an internalization for each of the

  1261   connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.

  1262   Meta-level conjunction should be covered as well (this is

  1263   particularly important for locales, see \secref{sec:locale}).

  1264

  1265   \item @{attribute rule_format} rewrites a theorem by the equalities

  1266   declared as @{attribute rulify} rules in the current object-logic.

  1267   By default, the result is fully normalized, including assumptions

  1268   and conclusions at any depth.  The @{text "(no_asm)"} option

  1269   restricts the transformation to the conclusion of a rule.

  1270

  1271   In common object-logics (HOL, FOL, ZF), the effect of @{attribute

  1272   rule_format} is to replace (bounded) universal quantification

  1273   (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding

  1274   rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.

  1275

  1276   \end{description}

  1277 *}

  1278

  1279 end