377 \end{matharray} |
377 \end{matharray} |
378 |
378 |
379 \railalias{simpall}{simp\_all} |
379 \railalias{simpall}{simp\_all} |
380 \railterm{simpall} |
380 \railterm{simpall} |
381 |
381 |
382 \begin{rail} |
382 \railalias{noasm}{no\_asm} |
383 ('simp' | simpall) ('!' ?) (simpmod * ) |
383 \railterm{noasm} |
384 ; |
384 |
385 |
385 \railalias{noasmsimp}{no\_asm\_simp} |
|
386 \railterm{noasmsimp} |
|
387 |
|
388 \railalias{noasmuse}{no\_asm\_use} |
|
389 \railterm{noasmuse} |
|
390 |
|
391 \begin{rail} |
|
392 ('simp' | simpall) ('!' ?) simpopt? (simpmod * ) |
|
393 ; |
|
394 |
|
395 simpopt: (noasm | noasmsimp | noasmuse) ':' |
|
396 ; |
386 simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs |
397 simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs |
387 ; |
398 ; |
388 \end{rail} |
399 \end{rail} |
389 |
400 |
390 \begin{descr} |
401 \begin{descr} |
402 additional kinds of rules may be declared by including appropriate |
413 additional kinds of rules may be declared by including appropriate |
403 attributes in the specification. |
414 attributes in the specification. |
404 \item [$simp_all$] is similar to $simp$, but acts on all goals. |
415 \item [$simp_all$] is similar to $simp$, but acts on all goals. |
405 \end{descr} |
416 \end{descr} |
406 |
417 |
407 Internally, the $simp$ method is based on \texttt{asm_full_simp_tac} |
418 By default, the Simplifier methods are based on \texttt{asm_full_simp_tac} |
408 \cite[\S10]{isabelle-ref}, but is much better behaved in practice. Just the |
419 internally \cite[\S10]{isabelle-ref}. In structured proofs this is usually |
409 local premises of the actual goal are involved by default. Additional facts |
420 quite well behaved in practice: just the local premises of the actual goal are |
410 may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The |
421 involved, additional facts may inserted via explicit forward-chaining (using |
411 full context of assumptions is only included in the $simp!$ version, which |
422 $\THEN$, $\FROMNAME$ etc.). The full context of assumptions is only included |
412 should be used with some care, though. |
423 if the ``$!$'' (bang) argument is given, which should be used with some care, |
413 |
424 though. |
414 Note that there is no separate $split$ method. The effect of |
425 |
415 \texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~\vec a)$. |
426 Additional Simplifier options may be specified to tune the behavior even |
|
427 further: $no_asm$ means assumptions are ignored completely (cf.\ |
|
428 \texttt{simp_tac}), $no_asm_simp$ means assumptions are used in the |
|
429 simplification of the conclusion but are not themselves simplified (cf.\ |
|
430 \texttt{asm_simp_tac}), and $no_asm_use$ means assumptions are simplified but |
|
431 are not used in the simplification of each other or the conclusion (cf. |
|
432 \texttt{full_simp_tac}). |
|
433 |
|
434 \medskip |
|
435 |
|
436 The Splitter package is usually configured to work as part of the Simplifier. |
|
437 There is no separate $split$ method available. The effect of repeatedly |
|
438 applying \texttt{split_tac} can be simulated by |
|
439 $(simp~only\colon~split\colon~\vec a)$. |
416 |
440 |
417 |
441 |
418 \subsection{Declaring rules} |
442 \subsection{Declaring rules} |
419 |
443 |
420 \indexisarcmd{print-simpset} |
444 \indexisarcmd{print-simpset} |