1 |
1 |
2 \chapter{Simplification} |
2 \chapter{Simplification} |
3 \label{chap:simplification} |
3 \label{chap:simplification} |
4 \index{simplification|(} |
4 \index{simplification|(} |
5 |
5 |
6 This chapter describes Isabelle's generic simplification package. It performs |
|
7 conditional and unconditional rewriting and uses contextual information |
|
8 (`local assumptions'). It provides several general hooks, which can provide |
|
9 automatic case splits during rewriting, for example. The simplifier is |
|
10 already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF. |
|
11 |
|
12 The first section is a quick introduction to the simplifier that |
|
13 should be sufficient to get started. The later sections explain more |
|
14 advanced features. |
|
15 |
|
16 |
6 |
17 \section{Simplification for dummies} |
7 \section{Simplification for dummies} |
18 \label{sec:simp-for-dummies} |
8 \label{sec:simp-for-dummies} |
19 |
|
20 Basic use of the simplifier is particularly easy because each theory |
|
21 is equipped with sensible default information controlling the rewrite |
|
22 process --- namely the implicit {\em current |
|
23 simpset}\index{simpset!current}. A suite of simple commands is |
|
24 provided that refer to the implicit simpset of the current theory |
|
25 context. |
|
26 |
|
27 \begin{warn} |
|
28 Make sure that you are working within the correct theory context. |
|
29 Executing proofs interactively, or loading them from ML files |
|
30 without associated theories may require setting the current theory |
|
31 manually via the \ttindex{context} command. |
|
32 \end{warn} |
|
33 |
9 |
34 \subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs} |
10 \subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs} |
35 \begin{ttbox} |
11 \begin{ttbox} |
36 Simp_tac : int -> tactic |
12 Simp_tac : int -> tactic |
37 Asm_simp_tac : int -> tactic |
13 Asm_simp_tac : int -> tactic |
38 Full_simp_tac : int -> tactic |
14 Full_simp_tac : int -> tactic |
39 Asm_full_simp_tac : int -> tactic |
15 Asm_full_simp_tac : int -> tactic |
40 trace_simp : bool ref \hfill{\bf initially false} |
|
41 debug_simp : bool ref \hfill{\bf initially false} |
|
42 \end{ttbox} |
16 \end{ttbox} |
43 |
17 |
44 \begin{ttdescription} |
18 \begin{ttdescription} |
45 \item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the |
19 \item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the |
46 current simpset. It may solve the subgoal completely if it has |
20 current simpset. It may solve the subgoal completely if it has |
58 but also simplifies the assumptions. In particular, assumptions can |
32 but also simplifies the assumptions. In particular, assumptions can |
59 simplify each other. |
33 simplify each other. |
60 \footnote{\texttt{Asm_full_simp_tac} used to process the assumptions from |
34 \footnote{\texttt{Asm_full_simp_tac} used to process the assumptions from |
61 left to right. For backwards compatibilty reasons only there is now |
35 left to right. For backwards compatibilty reasons only there is now |
62 \texttt{Asm_lr_simp_tac} that behaves like the old \texttt{Asm_full_simp_tac}.} |
36 \texttt{Asm_lr_simp_tac} that behaves like the old \texttt{Asm_full_simp_tac}.} |
63 \item[set \ttindexbold{trace_simp};] makes the simplifier output internal |
|
64 operations. This includes rewrite steps, but also bookkeeping like |
|
65 modifications of the simpset. |
|
66 \item[set \ttindexbold{debug_simp};] makes the simplifier output some extra |
|
67 information about internal operations. This includes any attempted |
|
68 invocation of simplification procedures. |
|
69 \end{ttdescription} |
37 \end{ttdescription} |
70 |
38 |
71 \medskip |
39 \medskip |
72 |
40 |
73 As an example, consider the theory of arithmetic in HOL. The (rather trivial) |
41 As an example, consider the theory of arithmetic in HOL. The (rather trivial) |
119 whereas applying the same tactic to |
87 whereas applying the same tactic to |
120 \begin{ttbox} |
88 \begin{ttbox} |
121 {\out 1. [| y = x; f x = f y; P (f x) |] ==> Q} |
89 {\out 1. [| y = x; f x = f y; P (f x) |] ==> Q} |
122 \end{ttbox} |
90 \end{ttbox} |
123 terminates. |
91 terminates. |
124 |
|
125 \medskip |
|
126 |
|
127 Using the simplifier effectively may take a bit of experimentation. |
|
128 Set the \verb$trace_simp$\index{tracing!of simplification} flag to get |
|
129 a better idea of what is going on. The resulting output can be |
|
130 enormous, especially since invocations of the simplifier are often |
|
131 nested (e.g.\ when solving conditions of rewrite rules). |
|
132 |
92 |
133 |
93 |
134 \subsection{Modifying the current simpset} |
94 \subsection{Modifying the current simpset} |
135 \begin{ttbox} |
95 \begin{ttbox} |
136 Addsimps : thm list -> unit |
96 Addsimps : thm list -> unit |