362 @{method_def simp_all} & : & @{text method} \\ |
362 @{method_def simp_all} & : & @{text method} \\ |
363 \end{matharray} |
363 \end{matharray} |
364 |
364 |
365 \indexouternonterm{simpmod} |
365 \indexouternonterm{simpmod} |
366 \begin{rail} |
366 \begin{rail} |
367 ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *) |
367 ('simp' | 'simp\_all') opt? (simpmod *) |
368 ; |
368 ; |
369 |
369 |
370 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')' |
370 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')' |
371 ; |
371 ; |
372 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
372 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
402 normalization process, or simplifying assumptions themselves (cf.\ |
402 normalization process, or simplifying assumptions themselves (cf.\ |
403 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured |
403 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured |
404 proofs this is usually quite well behaved in practice: just the |
404 proofs this is usually quite well behaved in practice: just the |
405 local premises of the actual goal are involved, additional facts may |
405 local premises of the actual goal are involved, additional facts may |
406 be inserted via explicit forward-chaining (via @{command "then"}, |
406 be inserted via explicit forward-chaining (via @{command "then"}, |
407 @{command "from"}, @{command "using"} etc.). The full context of |
407 @{command "from"}, @{command "using"} etc.). |
408 premises is only included if the ``@{text "!"}'' (bang) argument is |
|
409 given, which should be used with some care, though. |
|
410 |
408 |
411 Additional Simplifier options may be specified to tune the behavior |
409 Additional Simplifier options may be specified to tune the behavior |
412 further (mostly for unstructured scripts with many accidental local |
410 further (mostly for unstructured scripts with many accidental local |
413 facts): ``@{text "(no_asm)"}'' means assumptions are ignored |
411 facts): ``@{text "(no_asm)"}'' means assumptions are ignored |
414 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means |
412 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means |
601 @{method_def clarify} & : & @{text method} \\ |
599 @{method_def clarify} & : & @{text method} \\ |
602 \end{matharray} |
600 \end{matharray} |
603 |
601 |
604 \indexouternonterm{clamod} |
602 \indexouternonterm{clamod} |
605 \begin{rail} |
603 \begin{rail} |
606 'blast' ('!' ?) nat? (clamod *) |
604 'blast' nat? (clamod *) |
607 ; |
605 ; |
608 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *) |
606 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *) |
609 ; |
607 ; |
610 |
608 |
611 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs |
609 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs |
612 ; |
610 ; |
613 \end{rail} |
611 \end{rail} |
627 \end{description} |
625 \end{description} |
628 |
626 |
629 Any of the above methods support additional modifiers of the context |
627 Any of the above methods support additional modifiers of the context |
630 of classical rules. Their semantics is analogous to the attributes |
628 of classical rules. Their semantics is analogous to the attributes |
631 given before. Facts provided by forward chaining are inserted into |
629 given before. Facts provided by forward chaining are inserted into |
632 the goal before commencing proof search. The ``@{text |
630 the goal before commencing proof search. |
633 "!"}''~argument causes the full context of assumptions to be |
|
634 included as well. |
|
635 *} |
631 *} |
636 |
632 |
637 |
633 |
638 subsection {* Combined automated methods \label{sec:clasimp} *} |
634 subsection {* Combined automated methods \label{sec:clasimp} *} |
639 |
635 |
647 @{method_def bestsimp} & : & @{text method} \\ |
643 @{method_def bestsimp} & : & @{text method} \\ |
648 \end{matharray} |
644 \end{matharray} |
649 |
645 |
650 \indexouternonterm{clasimpmod} |
646 \indexouternonterm{clasimpmod} |
651 \begin{rail} |
647 \begin{rail} |
652 'auto' '!'? (nat nat)? (clasimpmod *) |
648 'auto' (nat nat)? (clasimpmod *) |
653 ; |
649 ; |
654 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *) |
650 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *) |
655 ; |
651 ; |
656 |
652 |
657 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | |
653 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | |
658 ('cong' | 'split') (() | 'add' | 'del') | |
654 ('cong' | 'split') (() | 'add' | 'del') | |
659 'iff' (((() | 'add') '?'?) | 'del') | |
655 'iff' (((() | 'add') '?'?) | 'del') | |