1 %% $Id$ |
1 %% $Id$ |
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 |
6 This chapter describes Isabelle's generic simplification package. It performs |
7 performs conditional and unconditional rewriting and uses contextual |
7 conditional and unconditional rewriting and uses contextual information |
8 information (`local assumptions'). It provides several general hooks, |
8 (`local assumptions'). It provides several general hooks, which can provide |
9 which can provide automatic case splits during rewriting, for example. |
9 automatic case splits during rewriting, for example. The simplifier is |
10 The simplifier is already set up for many of Isabelle's logics: \FOL, |
10 already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF. |
11 \ZF, \HOL, \HOLCF. |
|
12 |
11 |
13 The first section is a quick introduction to the simplifier that |
12 The first section is a quick introduction to the simplifier that |
14 should be sufficient to get started. The later sections explain more |
13 should be sufficient to get started. The later sections explain more |
15 advanced features. |
14 advanced features. |
16 |
15 |
69 invocation of simplification procedures. |
68 invocation of simplification procedures. |
70 \end{ttdescription} |
69 \end{ttdescription} |
71 |
70 |
72 \medskip |
71 \medskip |
73 |
72 |
74 As an example, consider the theory of arithmetic in \HOL. The (rather |
73 As an example, consider the theory of arithmetic in HOL. The (rather trivial) |
75 trivial) goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call |
74 goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call of |
76 of \texttt{Simp_tac} as follows: |
75 \texttt{Simp_tac} as follows: |
77 \begin{ttbox} |
76 \begin{ttbox} |
78 context Arith.thy; |
77 context Arith.thy; |
79 Goal "0 + (x + 0) = x + 0 + 0"; |
78 Goal "0 + (x + 0) = x + 0 + 0"; |
80 {\out 1. 0 + (x + 0) = x + 0 + 0} |
79 {\out 1. 0 + (x + 0) = x + 0 + 0} |
81 by (Simp_tac 1); |
80 by (Simp_tac 1); |
179 \item[\ttindexbold{Delsplits} $thms$;] deletes splitting rules from the |
178 \item[\ttindexbold{Delsplits} $thms$;] deletes splitting rules from the |
180 current simpset. |
179 current simpset. |
181 |
180 |
182 \end{ttdescription} |
181 \end{ttdescription} |
183 |
182 |
184 When a new theory is built, its implicit simpset is initialized by the |
183 When a new theory is built, its implicit simpset is initialized by the union |
185 union of the respective simpsets of its parent theories. In addition, |
184 of the respective simpsets of its parent theories. In addition, certain |
186 certain theory definition constructs (e.g.\ \ttindex{datatype} and |
185 theory definition constructs (e.g.\ \ttindex{datatype} and \ttindex{primrec} |
187 \ttindex{primrec} in \HOL) implicitly augment the current simpset. |
186 in HOL) implicitly augment the current simpset. Ordinary definitions are not |
188 Ordinary definitions are not added automatically! |
187 added automatically! |
189 |
188 |
190 It is up the user to manipulate the current simpset further by |
189 It is up the user to manipulate the current simpset further by |
191 explicitly adding or deleting theorems and simplification procedures. |
190 explicitly adding or deleting theorems and simplification procedures. |
192 |
191 |
193 \medskip |
192 \medskip |
251 empty_ss : simpset |
250 empty_ss : simpset |
252 merge_ss : simpset * simpset -> simpset |
251 merge_ss : simpset * simpset -> simpset |
253 \end{ttbox} |
252 \end{ttbox} |
254 \begin{ttdescription} |
253 \begin{ttdescription} |
255 |
254 |
256 \item[\ttindexbold{empty_ss}] is the empty simpset. This is not very |
255 \item[\ttindexbold{empty_ss}] is the empty simpset. This is not very useful |
257 useful under normal circumstances because it doesn't contain |
256 under normal circumstances because it doesn't contain suitable tactics |
258 suitable tactics (subgoaler etc.). When setting up the simplifier |
257 (subgoaler etc.). When setting up the simplifier for a particular |
259 for a particular object-logic, one will typically define a more |
258 object-logic, one will typically define a more appropriate ``almost empty'' |
260 appropriate ``almost empty'' simpset. For example, in \HOL\ this is |
259 simpset. For example, in HOL this is called \ttindexbold{HOL_basic_ss}. |
261 called \ttindexbold{HOL_basic_ss}. |
|
262 |
260 |
263 \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ |
261 \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ |
264 and $ss@2$ by building the union of their respective rewrite rules, |
262 and $ss@2$ by building the union of their respective rewrite rules, |
265 simplification procedures and congruences. The other components |
263 simplification procedures and congruences. The other components |
266 (tactics etc.) cannot be merged, though; they are taken from either |
264 (tactics etc.) cannot be merged, though; they are taken from either |
1075 examples; other algebraic structures are amenable to ordered rewriting, |
1073 examples; other algebraic structures are amenable to ordered rewriting, |
1076 such as boolean rings. |
1074 such as boolean rings. |
1077 |
1075 |
1078 \subsection{Example: sums of natural numbers} |
1076 \subsection{Example: sums of natural numbers} |
1079 |
1077 |
1080 This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}). |
1078 This example is again set in HOL (see \texttt{HOL/ex/NatSum}). Theory |
1081 Theory \thydx{Arith} contains natural numbers arithmetic. Its |
1079 \thydx{Arith} contains natural numbers arithmetic. Its associated simpset |
1082 associated simpset contains many arithmetic laws including |
1080 contains many arithmetic laws including distributivity of~$\times$ over~$+$, |
1083 distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list |
1081 while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on |
1084 consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let |
1082 type \texttt{nat}. Let us prove the theorem |
1085 us prove the theorem |
|
1086 \[ \sum@{i=1}^n i = n\times(n+1)/2. \] |
1083 \[ \sum@{i=1}^n i = n\times(n+1)/2. \] |
1087 % |
1084 % |
1088 A functional~\texttt{sum} represents the summation operator under the |
1085 A functional~\texttt{sum} represents the summation operator under the |
1089 interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We |
1086 interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We |
1090 extend \texttt{Arith} as follows: |
1087 extend \texttt{Arith} as follows: |
1214 As an example of how to write your own simplification procedures, |
1211 As an example of how to write your own simplification procedures, |
1215 consider eta-expansion of pair abstraction (see also |
1212 consider eta-expansion of pair abstraction (see also |
1216 \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external |
1213 \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external |
1217 model checker syntax). |
1214 model checker syntax). |
1218 |
1215 |
1219 The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an |
1216 The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator |
1220 operator \texttt{split} together with some concrete syntax supporting |
1217 \texttt{split} together with some concrete syntax supporting |
1221 $\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a |
1218 $\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a tactic |
1222 tactic that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of |
1219 that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type) |
1223 some pair type) to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule |
1220 to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule is: |
1224 is: |
|
1225 \begin{ttbox} |
1221 \begin{ttbox} |
1226 pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) |
1222 pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) |
1227 \end{ttbox} |
1223 \end{ttbox} |
1228 Unfortunately, term rewriting using this rule directly would not |
1224 Unfortunately, term rewriting using this rule directly would not |
1229 terminate! We now use the simplification procedure mechanism in order |
1225 terminate! We now use the simplification procedure mechanism in order |
1296 \subsection{A collection of standard rewrite rules} |
1292 \subsection{A collection of standard rewrite rules} |
1297 |
1293 |
1298 We first prove lots of standard rewrite rules about the logical |
1294 We first prove lots of standard rewrite rules about the logical |
1299 connectives. These include cancellation and associative laws. We |
1295 connectives. These include cancellation and associative laws. We |
1300 define a function that echoes the desired law and then supplies it the |
1296 define a function that echoes the desired law and then supplies it the |
1301 prover for intuitionistic \FOL: |
1297 prover for intuitionistic FOL: |
1302 \begin{ttbox} |
1298 \begin{ttbox} |
1303 fun int_prove_fun s = |
1299 fun int_prove_fun s = |
1304 (writeln s; |
1300 (writeln s; |
1305 prove_goal IFOL.thy s |
1301 prove_goal IFOL.thy s |
1306 (fn prems => [ (cut_facts_tac prems 1), |
1302 (fn prems => [ (cut_facts_tac prems 1), |
1435 \begin{ttbox} |
1431 \begin{ttbox} |
1436 val notFalseI = int_prove_fun "~False"; |
1432 val notFalseI = int_prove_fun "~False"; |
1437 val triv_rls = [TrueI,refl,iff_refl,notFalseI]; |
1433 val triv_rls = [TrueI,refl,iff_refl,notFalseI]; |
1438 \end{ttbox} |
1434 \end{ttbox} |
1439 % |
1435 % |
1440 The basic simpset for intuitionistic \FOL{} is |
1436 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It |
1441 \ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt |
1437 preprocess rewrites using {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}. |
1442 gen_all}, \texttt{atomize} and \texttt{mk_eq}. It solves simplified |
1438 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by |
1443 subgoals using \texttt{triv_rls} and assumptions, and by detecting |
1439 detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals |
1444 contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of |
1440 of conditional rewrites. |
1445 conditional rewrites. |
|
1446 |
1441 |
1447 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. |
1442 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. |
1448 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt |
1443 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt |
1449 IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later |
1444 IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later |
1450 extend \texttt{IFOL_ss} with classical rewrite rules such as $\lnot\lnot |
1445 extend \texttt{IFOL_ss} with classical rewrite rules such as $\lnot\lnot |