108 |
108 |
109 \subsection{The abstract type {\tt simpset}}\label{simp-simpsets} |
109 \subsection{The abstract type {\tt simpset}}\label{simp-simpsets} |
110 Simpsets are values of the abstract type \ttindexbold{simpset}. They are |
110 Simpsets are values of the abstract type \ttindexbold{simpset}. They are |
111 manipulated by the following functions: |
111 manipulated by the following functions: |
112 \index{simplification sets|bold} |
112 \index{simplification sets|bold} |
113 \begin{description} |
113 \begin{ttdescription} |
114 \item[\ttindexbold{empty_ss}] |
114 \item[\ttindexbold{empty_ss}] |
115 is the empty simpset. It has no congruence or rewrite rules and its |
115 is the empty simpset. It has no congruence or rewrite rules and its |
116 auto-tactic always fails. |
116 auto-tactic always fails. |
117 |
117 |
118 \item[\tt $ss$ \ttindexbold{addcongs} $thms$] |
118 \item[$ss$ \ttindexbold{addcongs} $thms$] |
119 is the simpset~$ss$ plus the congruence rules~$thms$. |
119 is the simpset~$ss$ plus the congruence rules~$thms$. |
120 |
120 |
121 \item[\tt $ss$ \ttindexbold{delcongs} $thms$] |
121 \item[$ss$ \ttindexbold{delcongs} $thms$] |
122 is the simpset~$ss$ minus the congruence rules~$thms$. |
122 is the simpset~$ss$ minus the congruence rules~$thms$. |
123 |
123 |
124 \item[\tt $ss$ \ttindexbold{addrews} $thms$] |
124 \item[$ss$ \ttindexbold{addrews} $thms$] |
125 is the simpset~$ss$ plus the rewrite rules~$thms$. |
125 is the simpset~$ss$ plus the rewrite rules~$thms$. |
126 |
126 |
127 \item[\tt $ss$ \ttindexbold{delrews} $thms$] |
127 \item[$ss$ \ttindexbold{delrews} $thms$] |
128 is the simpset~$ss$ minus the rewrite rules~$thms$. |
128 is the simpset~$ss$ minus the rewrite rules~$thms$. |
129 |
129 |
130 \item[\tt $ss$ \ttindexbold{setauto} $tacf$] |
130 \item[$ss$ \ttindexbold{setauto} $tacf$] |
131 is the simpset~$ss$ with $tacf$ for its auto-tactic. |
131 is the simpset~$ss$ with $tacf$ for its auto-tactic. |
132 |
132 |
133 \item[\ttindexbold{print_ss} $ss$] |
133 \item[\ttindexbold{print_ss} $ss$] |
134 prints all the congruence and rewrite rules in the simpset~$ss$. |
134 prints all the congruence and rewrite rules in the simpset~$ss$. |
135 \end{description} |
135 \end{ttdescription} |
136 Adding a rule to a simpset already containing it, or deleting one |
136 Adding a rule to a simpset already containing it, or deleting one |
137 from a simpset not containing it, generates a warning message. |
137 from a simpset not containing it, generates a warning message. |
138 |
138 |
139 In principle, any theorem can be used as a rewrite rule. Before adding a |
139 In principle, any theorem can be used as a rewrite rule. Before adding a |
140 theorem to a simpset, {\tt addrews} preprocesses the theorem to extract the |
140 theorem to a simpset, {\tt addrews} preprocesses the theorem to extract the |
169 The actual simplification work is performed by the following tactics. The |
169 The actual simplification work is performed by the following tactics. The |
170 rewriting strategy is strictly bottom up. Conditions in conditional rewrite |
170 rewriting strategy is strictly bottom up. Conditions in conditional rewrite |
171 rules are solved recursively before the rewrite rule is applied. |
171 rules are solved recursively before the rewrite rule is applied. |
172 |
172 |
173 There are two basic simplification tactics: |
173 There are two basic simplification tactics: |
174 \begin{description} |
174 \begin{ttdescription} |
175 \item[\ttindexbold{SIMP_TAC} $ss$ $i$] |
175 \item[\ttindexbold{SIMP_TAC} $ss$ $i$] |
176 simplifies subgoal~$i$ using the rules in~$ss$. It may solve the |
176 simplifies subgoal~$i$ using the rules in~$ss$. It may solve the |
177 subgoal completely if it has become trivial, using the auto-tactic |
177 subgoal completely if it has become trivial, using the auto-tactic |
178 (\S\ref{simp-simpsets}). |
178 (\S\ref{simp-simpsets}). |
179 |
179 |
180 \item[\ttindexbold{ASM_SIMP_TAC}] |
180 \item[\ttindexbold{ASM_SIMP_TAC}] |
181 is like \verb$SIMP_TAC$, but also uses assumptions as additional |
181 is like \verb$SIMP_TAC$, but also uses assumptions as additional |
182 rewrite rules. |
182 rewrite rules. |
183 \end{description} |
183 \end{ttdescription} |
184 Many logics have conditional operators like {\it if-then-else}. If the |
184 Many logics have conditional operators like {\it if-then-else}. If the |
185 simplifier has been set up with such case splits (see~\ttindex{case_splits} |
185 simplifier has been set up with such case splits (see~\ttindex{case_splits} |
186 in \S\ref{SimpFun-input}), there are tactics which automatically alternate |
186 in \S\ref{SimpFun-input}), there are tactics which automatically alternate |
187 between simplification and case splitting: |
187 between simplification and case splitting: |
188 \begin{description} |
188 \begin{ttdescription} |
189 \item[\ttindexbold{SIMP_CASE_TAC}] |
189 \item[\ttindexbold{SIMP_CASE_TAC}] |
190 is like {\tt SIMP_TAC} but also performs automatic case splits. |
190 is like {\tt SIMP_TAC} but also performs automatic case splits. |
191 More precisely, after each simplification phase the tactic tries to apply a |
191 More precisely, after each simplification phase the tactic tries to apply a |
192 theorem in \ttindex{case_splits}. If this succeeds, the tactic calls |
192 theorem in \ttindex{case_splits}. If this succeeds, the tactic calls |
193 itself recursively on the result. |
193 itself recursively on the result. |
204 tries to break up a goal using a rule in |
204 tries to break up a goal using a rule in |
205 \ttindex{case_splits}. |
205 \ttindex{case_splits}. |
206 |
206 |
207 \item[\ttindexbold{SIMP_THM}] |
207 \item[\ttindexbold{SIMP_THM}] |
208 simplifies a theorem using assumptions and case splitting. |
208 simplifies a theorem using assumptions and case splitting. |
209 \end{description} |
209 \end{ttdescription} |
210 Finally there are two useful functions for generating congruence |
210 Finally there are two useful functions for generating congruence |
211 rules for constants and free variables: |
211 rules for constants and free variables: |
212 \begin{description} |
212 \begin{ttdescription} |
213 \item[\ttindexbold{mk_congs} $thy$ $cs$] |
213 \item[\ttindexbold{mk_congs} $thy$ $cs$] |
214 computes a list of congruence rules, one for each constant in $cs$. |
214 computes a list of congruence rules, one for each constant in $cs$. |
215 Remember that the name of an infix constant |
215 Remember that the name of an infix constant |
216 \verb$+$ is \verb$op +$. |
216 \verb$+$ is \verb$op +$. |
217 |
217 |
221 can be either free variables like {\tt P}, or constants like \verb$op =$. |
221 can be either free variables like {\tt P}, or constants like \verb$op =$. |
222 For example in {\tt FOL}, the pair |
222 For example in {\tt FOL}, the pair |
223 \verb$("f","'a => 'a")$ generates the rule \verb$?x = ?y ==> f(?x) = f(?y)$. |
223 \verb$("f","'a => 'a")$ generates the rule \verb$?x = ?y ==> f(?x) = f(?y)$. |
224 Such congruence rules are necessary for goals with free variables whose |
224 Such congruence rules are necessary for goals with free variables whose |
225 arguments need to be rewritten. |
225 arguments need to be rewritten. |
226 \end{description} |
226 \end{ttdescription} |
227 Both functions work correctly only if {\tt SimpFun} has been supplied with the |
227 Both functions work correctly only if {\tt SimpFun} has been supplied with the |
228 necessary substitution rules. The details are discussed in |
228 necessary substitution rules. The details are discussed in |
229 \S\ref{SimpFun-input} under {\tt subst_thms}. |
229 \S\ref{SimpFun-input} under {\tt subst_thms}. |
230 \begin{warn} |
230 \begin{warn} |
231 Using the simplifier effectively may take a bit of experimentation. In |
231 Using the simplifier effectively may take a bit of experimentation. In |
238 |
238 |
239 |
239 |
240 \section{Example: using the simplifier} |
240 \section{Example: using the simplifier} |
241 \index{simplification!example} |
241 \index{simplification!example} |
242 Assume we are working within {\tt FOL} and that |
242 Assume we are working within {\tt FOL} and that |
243 \begin{description} |
243 \begin{ttdescription} |
244 \item[\tt Nat.thy] is a theory including the constants $0$, $Suc$ and $+$, |
244 \item[Nat.thy] is a theory including the constants $0$, $Suc$ and $+$, |
245 \item[\tt add_0] is the rewrite rule $0+n = n$, |
245 \item[add_0] is the rewrite rule $0+n = n$, |
246 \item[\tt add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$, |
246 \item[add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$, |
247 \item[\tt induct] is the induction rule |
247 \item[induct] is the induction rule |
248 $\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$. |
248 $\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$. |
249 \item[\tt FOL_ss] is a basic simpset for {\tt FOL}. |
249 \item[FOL_ss] is a basic simpset for {\tt FOL}. |
250 \end{description} |
250 \end{ttdescription} |
251 We generate congruence rules for $Suc$ and for the infix operator~$+$: |
251 We generate congruence rules for $Suc$ and for the infix operator~$+$: |
252 \begin{ttbox} |
252 \begin{ttbox} |
253 val nat_congs = mk_congs Nat.thy ["Suc", "op +"]; |
253 val nat_congs = mk_congs Nat.thy ["Suc", "op +"]; |
254 prths nat_congs; |
254 prths nat_congs; |
255 {\out ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)} |
255 {\out ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)} |
380 val trans_thms : thm list |
380 val trans_thms : thm list |
381 end; |
381 end; |
382 \end{ttbox} |
382 \end{ttbox} |
383 The components of {\tt SIMP_DATA} need to be instantiated as follows. Many |
383 The components of {\tt SIMP_DATA} need to be instantiated as follows. Many |
384 of these components are lists, and can be empty. |
384 of these components are lists, and can be empty. |
385 \begin{description} |
385 \begin{ttdescription} |
386 \item[\ttindexbold{refl_thms}] |
386 \item[\ttindexbold{refl_thms}] |
387 supplies reflexivity theorems of the form $\Var{x} \gg |
387 supplies reflexivity theorems of the form $\Var{x} \gg |
388 \Var{x}$. They must not have additional premises as, for example, |
388 \Var{x}$. They must not have additional premises as, for example, |
389 $\Var{x}\in\Var{A} \Imp \Var{x} = \Var{x}\in\Var{A}$ in type theory. |
389 $\Var{x}\in\Var{A} \Imp \Var{x} = \Var{x}\in\Var{A}$ in type theory. |
390 |
390 |
483 infix), the following definition does the job: |
483 infix), the following definition does the job: |
484 \begin{verbatim} |
484 \begin{verbatim} |
485 fun dest_red( _ $ (c $ ta $ tb) ) = (c,ta,tb); |
485 fun dest_red( _ $ (c $ ta $ tb) ) = (c,ta,tb); |
486 \end{verbatim} |
486 \end{verbatim} |
487 The wildcard pattern {\tt_} matches the coercion function. |
487 The wildcard pattern {\tt_} matches the coercion function. |
488 \end{description} |
488 \end{ttdescription} |
489 |
489 |
490 |
490 |
491 \section{A sample instantiation} |
491 \section{A sample instantiation} |
492 Here is the instantiation of {\tt SIMP_DATA} for {\FOL}. The code for {\tt |
492 Here is the instantiation of {\tt SIMP_DATA} for {\FOL}. The code for {\tt |
493 mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}. |
493 mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}. |