35 holding. Class axioms may not contain more than one type variable. The |
35 holding. Class axioms may not contain more than one type variable. The |
36 class axioms (with implicit sort constraints added) are bound to the given |
36 class axioms (with implicit sort constraints added) are bound to the given |
37 names. Furthermore a class introduction rule is generated, which is |
37 names. Furthermore a class introduction rule is generated, which is |
38 employed by method $intro_classes$ to support instantiation proofs of this |
38 employed by method $intro_classes$ to support instantiation proofs of this |
39 class. |
39 class. |
40 |
40 |
41 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: |
41 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: |
42 (\vec s)c$] setup a goal stating a class relation or type arity. The proof |
42 (\vec s)c$] setup a goal stating a class relation or type arity. The proof |
43 would usually proceed by $intro_classes$, and then establish the |
43 would usually proceed by $intro_classes$, and then establish the |
44 characteristic theorems of the type classes involved. After finishing the |
44 characteristic theorems of the type classes involved. After finishing the |
45 proof, the theory will be augmented by a type signature declaration |
45 proof, the theory will be augmented by a type signature declaration |
117 initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same |
117 initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same |
118 level of block-structure updates $calculation$ by some transitivity rule |
118 level of block-structure updates $calculation$ by some transitivity rule |
119 applied to $calculation$ and $this$ (in that order). Transitivity rules are |
119 applied to $calculation$ and $this$ (in that order). Transitivity rules are |
120 picked from the current context plus those given as explicit arguments (the |
120 picked from the current context plus those given as explicit arguments (the |
121 latter have precedence). |
121 latter have precedence). |
122 |
122 |
123 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as |
123 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as |
124 $\ALSO$, and concludes the current calculational thread. The final result |
124 $\ALSO$, and concludes the current calculational thread. The final result |
125 is exhibited as fact for forward chaining towards the next goal. Basically, |
125 is exhibited as fact for forward chaining towards the next goal. Basically, |
126 $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that |
126 $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that |
127 ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and |
127 ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and |
128 ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding |
128 ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding |
129 calculational proofs. |
129 calculational proofs. |
130 |
130 |
131 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, |
131 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, |
132 but collect results only, without applying rules. |
132 but collect results only, without applying rules. |
133 |
133 |
134 \item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity |
134 \item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity |
135 rules declared in the current context. |
135 rules declared in the current context. |
136 |
136 |
137 \item [$trans$] declares theorems as transitivity rules. |
137 \item [$trans$] declares theorems as transitivity rules. |
138 |
138 |
139 \end{descr} |
139 \end{descr} |
140 |
140 |
141 |
141 |
142 \section{Named local contexts (cases)}\label{sec:cases} |
142 \section{Named local contexts (cases)}\label{sec:cases} |
143 |
143 |
202 \item [$case_names~\vec c$] declares names for the local contexts of premises |
202 \item [$case_names~\vec c$] declares names for the local contexts of premises |
203 of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises. |
203 of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises. |
204 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
204 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
205 premises $1, \dots, n$ of some theorem. An empty list of names may be given |
205 premises $1, \dots, n$ of some theorem. An empty list of names may be given |
206 to skip positions, leaving the present parameters unchanged. |
206 to skip positions, leaving the present parameters unchanged. |
207 \end{descr} |
207 |
208 |
208 Note that the default usage of case rules does \emph{not} directly expose |
209 |
209 parameters to the proof context (see also \S\ref{sec:induct-method-proper}). |
210 \section{Generalized existence} |
210 \end{descr} |
|
211 |
|
212 |
|
213 \section{Generalized existence}\label{sec:obtain} |
211 |
214 |
212 \indexisarcmd{obtain} |
215 \indexisarcmd{obtain} |
213 \begin{matharray}{rcl} |
216 \begin{matharray}{rcl} |
214 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
217 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
215 \end{matharray} |
218 \end{matharray} |
285 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the |
288 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the |
286 basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by |
289 basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by |
287 elim-resolution, destruct-resolution, and forward-resolution, respectively |
290 elim-resolution, destruct-resolution, and forward-resolution, respectively |
288 \cite{isabelle-ref}. These are improper method, mainly for experimentation |
291 \cite{isabelle-ref}. These are improper method, mainly for experimentation |
289 and emulating tactic scripts. |
292 and emulating tactic scripts. |
290 |
293 |
291 Different modes of basic rule application are usually expressed in Isar at |
294 Different modes of basic rule application are usually expressed in Isar at |
292 the proof language level, rather than via implicit proof state |
295 the proof language level, rather than via implicit proof state |
293 manipulations. For example, a proper single-step elimination would be done |
296 manipulations. For example, a proper single-step elimination would be done |
294 using the basic $rule$ method, with forward chaining of current facts. |
297 using the basic $rule$ method, with forward chaining of current facts. |
295 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof |
298 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof |
303 |
306 |
304 \indexisaratt{standard} |
307 \indexisaratt{standard} |
305 \indexisaratt{elimify} |
308 \indexisaratt{elimify} |
306 \indexisaratt{no-vars} |
309 \indexisaratt{no-vars} |
307 |
310 |
308 \indexisaratt{RS}\indexisaratt{COMP} |
311 \indexisaratt{THEN}\indexisaratt{COMP} |
309 \indexisaratt{where} |
312 \indexisaratt{where} |
310 \indexisaratt{tag}\indexisaratt{untag} |
313 \indexisaratt{tag}\indexisaratt{untag} |
311 \indexisaratt{export} |
314 \indexisaratt{export} |
312 \indexisaratt{unfold}\indexisaratt{fold} |
315 \indexisaratt{unfold}\indexisaratt{fold} |
313 \begin{matharray}{rcl} |
316 \begin{matharray}{rcl} |
314 tag & : & \isaratt \\ |
317 tag & : & \isaratt \\ |
315 untag & : & \isaratt \\[0.5ex] |
318 untag & : & \isaratt \\[0.5ex] |
316 RS & : & \isaratt \\ |
319 THEN & : & \isaratt \\ |
317 COMP & : & \isaratt \\[0.5ex] |
320 COMP & : & \isaratt \\[0.5ex] |
318 where & : & \isaratt \\[0.5ex] |
321 where & : & \isaratt \\[0.5ex] |
319 unfold & : & \isaratt \\ |
322 unfold & : & \isaratt \\ |
320 fold & : & \isaratt \\[0.5ex] |
323 fold & : & \isaratt \\[0.5ex] |
321 standard & : & \isaratt \\ |
324 standard & : & \isaratt \\ |
341 \item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some |
344 \item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some |
342 theorem. Tags may be any list of strings that serve as comment for some |
345 theorem. Tags may be any list of strings that serve as comment for some |
343 tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the |
346 tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the |
344 result). The first string is considered the tag name, the rest its |
347 result). The first string is considered the tag name, the rest its |
345 arguments. Note that untag removes any tags of the same name. |
348 arguments. Note that untag removes any tags of the same name. |
346 \item [$RS~n~a$ and $COMP~n~a$] compose rules. $RS$ resolves with the $n$-th |
349 \item [$THEN~n~a$ and $COMP~n~a$] compose rules. $THEN$ resolves with the |
347 premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting |
350 $n$-th premise of $a$; the $COMP$ version skips the automatic lifting |
348 process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in |
351 process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in |
349 \cite[\S5]{isabelle-ref}). |
352 \cite[\S5]{isabelle-ref}). |
350 \item [$where~\vec x = \vec t$] perform named instantiation of schematic |
353 \item [$where~\vec x = \vec t$] perform named instantiation of schematic |
351 variables occurring in a theorem. Unlike instantiation tactics such as |
354 variables occurring in a theorem. Unlike instantiation tactics such as |
352 $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables |
355 $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables |
353 have to be specified (e.g.\ $\Var{x@3}$). |
356 have to be specified (e.g.\ $\Var{x@3}$). |
354 |
357 |
355 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given |
358 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given |
356 meta-level definitions throughout a rule. |
359 meta-level definitions throughout a rule. |
357 |
360 |
358 \item [$standard$] puts a theorem into the standard form of object-rules, just |
361 \item [$standard$] puts a theorem into the standard form of object-rules, just |
359 as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}). |
362 as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}). |
360 |
363 |
361 \item [$elimify$] turns an destruction rule into an elimination, just as the |
364 \item [$elimify$] turns an destruction rule into an elimination, just as the |
362 ML function \texttt{make\_elim} (see \cite{isabelle-ref}). |
365 ML function \texttt{make\_elim} (see \cite{isabelle-ref}). |
363 |
366 |
364 \item [$no_vars$] replaces schematic variables by free ones; this is mainly |
367 \item [$no_vars$] replaces schematic variables by free ones; this is mainly |
365 for tuning output of pretty printed theorems. |
368 for tuning output of pretty printed theorems. |
366 |
369 |
367 \item [$export$] lifts a local result out of the current proof context, |
370 \item [$export$] lifts a local result out of the current proof context, |
368 generalizing all fixed variables and discharging all assumptions. Note that |
371 generalizing all fixed variables and discharging all assumptions. Note that |
369 proper incremental export is already done as part of the basic Isar |
372 proper incremental export is already done as part of the basic Isar |
370 machinery. This attribute is mainly for experimentation. |
373 machinery. This attribute is mainly for experimentation. |
371 |
374 |
372 \end{descr} |
375 \end{descr} |
373 |
376 |
374 |
377 |
375 \section{Tactic emulations}\label{sec:tactics} |
378 \section{Tactic emulations}\label{sec:tactics} |
376 |
379 |
391 named $foo_tac$. |
394 named $foo_tac$. |
392 |
395 |
393 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac} |
396 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac} |
394 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac} |
397 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac} |
395 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac} |
398 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac} |
396 \indexisarmeth{subgoal-tac}\indexisarmeth{tactic} |
399 \indexisarmeth{subgoal-tac}\indexisarmeth{rename_tac} |
|
400 \indexisarmeth{rotate-tac}\indexisarmeth{tactic} |
397 \begin{matharray}{rcl} |
401 \begin{matharray}{rcl} |
398 rule_tac^* & : & \isarmeth \\ |
402 rule_tac^* & : & \isarmeth \\ |
399 erule_tac^* & : & \isarmeth \\ |
403 erule_tac^* & : & \isarmeth \\ |
400 drule_tac^* & : & \isarmeth \\ |
404 drule_tac^* & : & \isarmeth \\ |
401 frule_tac^* & : & \isarmeth \\ |
405 frule_tac^* & : & \isarmeth \\ |
402 cut_tac^* & : & \isarmeth \\ |
406 cut_tac^* & : & \isarmeth \\ |
403 thin_tac^* & : & \isarmeth \\ |
407 thin_tac^* & : & \isarmeth \\ |
404 subgoal_tac^* & : & \isarmeth \\ |
408 subgoal_tac^* & : & \isarmeth \\ |
|
409 rename_tac^* & : & \isarmeth \\ |
|
410 rotate_tac^* & : & \isarmeth \\ |
405 tactic^* & : & \isarmeth \\ |
411 tactic^* & : & \isarmeth \\ |
406 \end{matharray} |
412 \end{matharray} |
407 |
413 |
408 \railalias{ruletac}{rule\_tac} |
414 \railalias{ruletac}{rule\_tac} |
409 \railterm{ruletac} |
415 \railterm{ruletac} |
424 \railterm{thintac} |
430 \railterm{thintac} |
425 |
431 |
426 \railalias{subgoaltac}{subgoal\_tac} |
432 \railalias{subgoaltac}{subgoal\_tac} |
427 \railterm{subgoaltac} |
433 \railterm{subgoaltac} |
428 |
434 |
|
435 \railalias{renametac}{rename\_tac} |
|
436 \railterm{renametac} |
|
437 |
|
438 \railalias{rotatetac}{rotate\_tac} |
|
439 \railterm{rotatetac} |
|
440 |
429 \begin{rail} |
441 \begin{rail} |
430 ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec? |
442 ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec? |
431 ( insts thmref | thmrefs ) |
443 ( insts thmref | thmrefs ) |
432 ; |
444 ; |
433 subgoaltac goalspec? (prop +) |
445 subgoaltac goalspec? (prop +) |
|
446 ; |
|
447 renametac goalspec? (name +) |
|
448 ; |
|
449 rotatetac goalspec? int? |
434 ; |
450 ; |
435 'tactic' text |
451 'tactic' text |
436 ; |
452 ; |
437 |
453 |
438 insts: ((name '=' term) + 'and') 'in' |
454 insts: ((name '=' term) + 'and') 'in' |
441 |
457 |
442 \begin{descr} |
458 \begin{descr} |
443 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. |
459 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. |
444 This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see |
460 This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see |
445 \cite[\S3]{isabelle-ref}). |
461 \cite[\S3]{isabelle-ref}). |
446 |
462 |
447 Note that multiple rules may be only given there is no instantiation. Then |
463 Note that multiple rules may be only given there is no instantiation. Then |
448 $rule_tac$ is the same as \texttt{resolve_tac} in ML (see |
464 $rule_tac$ is the same as \texttt{resolve_tac} in ML (see |
449 \cite[\S3]{isabelle-ref}). |
465 \cite[\S3]{isabelle-ref}). |
450 \item [$cut_tac$] inserts facts into the proof state as assumption of a |
466 \item [$cut_tac$] inserts facts into the proof state as assumption of a |
451 subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note |
467 subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note |
456 that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in |
472 that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in |
457 \cite[\S3]{isabelle-ref}. |
473 \cite[\S3]{isabelle-ref}. |
458 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See |
474 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See |
459 also \texttt{subgoal_tac} and \texttt{subgoals_tac} in |
475 also \texttt{subgoal_tac} and \texttt{subgoals_tac} in |
460 \cite[\S3]{isabelle-ref}. |
476 \cite[\S3]{isabelle-ref}. |
|
477 \item [$rename_tac~\vec x$] renames parameters of a goal according to the list |
|
478 $\vec x$, which refers to the \emph{suffix} of variables. |
|
479 \item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions: |
|
480 from right to left if $n$ is positive, and from left to right if $n$ is |
|
481 negative; the default value is $1$. See also \texttt{rotate_tac} in |
|
482 \cite[\S3]{isabelle-ref}. |
461 \item [$tactic~text$] produces a proof method from any ML text of type |
483 \item [$tactic~text$] produces a proof method from any ML text of type |
462 \texttt{tactic}. Apart from the usual ML environment and the current |
484 \texttt{tactic}. Apart from the usual ML environment and the current |
463 implicit theory context, the ML code may refer to the following locally |
485 implicit theory context, the ML code may refer to the following locally |
464 bound values: |
486 bound values: |
465 |
487 |
512 \begin{descr} |
534 \begin{descr} |
513 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules |
535 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules |
514 according to the arguments given. Note that the \railtterm{only} modifier |
536 according to the arguments given. Note that the \railtterm{only} modifier |
515 first removes all other rewrite rules, congruences, and looper tactics |
537 first removes all other rewrite rules, congruences, and looper tactics |
516 (including splits), and then behaves like \railtterm{add}. |
538 (including splits), and then behaves like \railtterm{add}. |
517 |
539 |
518 The \railtterm{split} modifiers add or delete rules for the Splitter (see |
540 The \railtterm{split} modifiers add or delete rules for the Splitter (see |
519 also \cite{isabelle-ref}), the default is to add. This works only if the |
541 also \cite{isabelle-ref}), the default is to add. This works only if the |
520 Simplifier method has been properly setup to include the Splitter (all major |
542 Simplifier method has been properly setup to include the Splitter (all major |
521 object logics such HOL, HOLCF, FOL, ZF do this already). |
543 object logics such HOL, HOLCF, FOL, ZF do this already). |
522 |
544 |
523 The \railtterm{other} modifier ignores its arguments. Nevertheless, |
545 The \railtterm{other} modifier ignores its arguments. Nevertheless, |
524 additional kinds of rules may be declared by including appropriate |
546 additional kinds of rules may be declared by including appropriate |
525 attributes in the specification. |
547 attributes in the specification. |
526 \item [$simp_all$] is similar to $simp$, but acts on all goals. |
548 \item [$simp_all$] is similar to $simp$, but acts on all goals. |
527 \end{descr} |
549 \end{descr} |
534 forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The full context of |
556 forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The full context of |
535 assumptions is only included if the ``$!$'' (bang) argument is given, which |
557 assumptions is only included if the ``$!$'' (bang) argument is given, which |
536 should be used with some care, though. |
558 should be used with some care, though. |
537 |
559 |
538 Additional Simplifier options may be specified to tune the behavior even |
560 Additional Simplifier options may be specified to tune the behavior even |
539 further: $(no_asm)$ means assumptions are ignored completely (cf.\ |
561 further: $(no_asm)$ means assumptions are ignored completely (cf.\ |
540 \texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the |
562 \texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the |
541 simplification of the conclusion but are not themselves simplified (cf.\ |
563 simplification of the conclusion but are not themselves simplified (cf.\ |
542 \texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified |
564 \texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified |
543 but are not used in the simplification of each other or the conclusion (cf. |
565 but are not used in the simplification of each other or the conclusion (cf. |
544 \texttt{full_simp_tac}). |
566 \texttt{full_simp_tac}). |
545 |
567 |
546 \medskip |
568 \medskip |
592 used only very rarely. There are no separate options for declaring |
614 used only very rarely. There are no separate options for declaring |
593 simplification rules locally. |
615 simplification rules locally. |
594 |
616 |
595 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more |
617 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more |
596 information. |
618 information. |
|
619 |
|
620 |
|
621 \section{Basic equational reasoning} |
|
622 |
|
623 \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisaratt{symmetric} |
|
624 \begin{matharray}{rcl} |
|
625 subst & : & \isarmeth \\ |
|
626 hypsubst^* & : & \isarmeth \\ |
|
627 symmetric & : & \isaratt \\ |
|
628 \end{matharray} |
|
629 |
|
630 \begin{rail} |
|
631 'subst' thmref |
|
632 ; |
|
633 \end{rail} |
|
634 |
|
635 These methods and attributes provide basic facilities for equational reasoning |
|
636 that are intended for specialized applications only. Normally, single step |
|
637 reasoning would be performed by calculation (see \S\ref{sec:calculation}), |
|
638 while the Simplifier is the canonical tool for automated normalization (see |
|
639 \S\ref{sec:simplifier}). |
|
640 |
|
641 \begin{descr} |
|
642 \item [$subst~thm$] performs a single substitution step using rule $thm$, |
|
643 which may be either a meta or object equality. |
|
644 \item [$hypsubst$] performs substitution using some assumption. |
|
645 \item [$symmetric$] applies the symmetry rule of meta or object equality. |
|
646 \end{descr} |
597 |
647 |
598 |
648 |
599 \section{The Classical Reasoner} |
649 \section{The Classical Reasoner} |
600 |
650 |
601 \subsection{Basic methods}\label{sec:classical-basic} |
651 \subsection{Basic methods}\label{sec:classical-basic} |
620 provided as arguments, it automatically determines elimination and |
670 provided as arguments, it automatically determines elimination and |
621 introduction rules from the context (see also \S\ref{sec:classical-mod}). |
671 introduction rules from the context (see also \S\ref{sec:classical-mod}). |
622 This is made the default method for basic proof steps, such as $\PROOFNAME$ |
672 This is made the default method for basic proof steps, such as $\PROOFNAME$ |
623 and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and |
673 and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and |
624 \S\ref{sec:pure-meth-att}. |
674 \S\ref{sec:pure-meth-att}. |
625 |
675 |
626 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
676 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
627 elim-resolution, after having inserted any facts. Omitting the arguments |
677 elim-resolution, after having inserted any facts. Omitting the arguments |
628 refers to any suitable rules declared in the context, otherwise only the |
678 refers to any suitable rules declared in the context, otherwise only the |
629 explicitly given ones may be applied. The latter form admits better control |
679 explicitly given ones may be applied. The latter form admits better control |
630 of what actually happens, thus it is very appropriate as an initial method |
680 of what actually happens, thus it is very appropriate as an initial method |
631 for $\PROOFNAME$ that splits up certain connectives of the goal, before |
681 for $\PROOFNAME$ that splits up certain connectives of the goal, before |
632 entering the actual sub-proof. |
682 entering the actual sub-proof. |
633 |
683 |
634 \item [$contradiction$] solves some goal by contradiction, deriving any result |
684 \item [$contradiction$] solves some goal by contradiction, deriving any result |
635 from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may |
685 from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may |
636 appear in either order. |
686 appear in either order. |
637 \end{descr} |
687 \end{descr} |
638 |
688 |
706 \texttt{fast_tac} (with the Simplifier added as wrapper), see |
756 \texttt{fast_tac} (with the Simplifier added as wrapper), see |
707 \cite[\S11]{isabelle-ref} for more information. The modifier arguments |
757 \cite[\S11]{isabelle-ref} for more information. The modifier arguments |
708 correspond to those given in \S\ref{sec:simp} and |
758 correspond to those given in \S\ref{sec:simp} and |
709 \S\ref{sec:classical-auto}. Just note that the ones related to the |
759 \S\ref{sec:classical-auto}. Just note that the ones related to the |
710 Simplifier are prefixed by \railtterm{simp} here. |
760 Simplifier are prefixed by \railtterm{simp} here. |
711 |
761 |
712 Facts provided by forward chaining are inserted into the goal before doing |
762 Facts provided by forward chaining are inserted into the goal before doing |
713 the search. The ``!''~argument causes the full context of assumptions to be |
763 the search. The ``!''~argument causes the full context of assumptions to be |
714 included as well. |
764 included as well. |
715 \end{descr} |
765 \end{descr} |
716 |
766 |
743 destruct rules, respectively. By default, rules are considered as |
793 destruct rules, respectively. By default, rules are considered as |
744 \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a |
794 \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a |
745 single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not |
795 single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not |
746 applied in the search-oriented automated methods, but only in single-step |
796 applied in the search-oriented automated methods, but only in single-step |
747 methods such as $rule$). |
797 methods such as $rule$). |
748 |
798 |
749 \item [$iff$] declares equations both as rules for the Simplifier and |
799 \item [$iff$] declares equations both as rules for the Simplifier and |
750 Classical Reasoner. |
800 Classical Reasoner. |
751 |
801 |
752 \item [$delrule$] deletes introduction or elimination rules from the context. |
802 \item [$delrule$] deletes introduction or elimination rules from the context. |
753 Note that destruction rules would have to be turned into elimination rules |
803 Note that destruction rules would have to be turned into elimination rules |
754 first, e.g.\ by using the $elimify$ attribute. |
804 first, e.g.\ by using the $elimify$ attribute. |
755 \end{descr} |
805 \end{descr} |
756 |
806 |
757 |
807 |
758 %%% Local Variables: |
808 %%% Local Variables: |
759 %%% mode: latex |
809 %%% mode: latex |
760 %%% TeX-master: "isar-ref" |
810 %%% TeX-master: "isar-ref" |
761 %%% End: |
811 %%% End: |