# HG changeset patch # User wenzelm # Date 881943065 -3600 # Node ID a2b7262770508c213a1083ffe198aa08cb2e2f73 # Parent c24a1bbd3cf3eccf63489387a6d396440c3ff9e5 major update; diff -r c24a1bbd3cf3 -r a2b726277050 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Fri Dec 12 17:10:40 1997 +0100 +++ b/doc-src/Ref/simplifier.tex Fri Dec 12 17:11:05 1997 +0100 @@ -3,204 +3,383 @@ \label{chap:simplification} \index{simplification|(} -This chapter describes Isabelle's generic simplification package, which -provides a suite of simplification tactics. It performs conditional and -unconditional rewriting and uses contextual information (`local -assumptions'). It provides a few general hooks, which can provide -automatic case splits during rewriting, for example. The simplifier is set -up for many of Isabelle's logics: \FOL, \ZF, \HOL\ and \HOLCF. +This chapter describes Isabelle's generic simplification package. It +performs conditional and unconditional rewriting and uses contextual +information (`local assumptions'). It provides several general hooks, +which can provide automatic case splits during rewriting, for example. +The simplifier is already set up for many of Isabelle's logics: \FOL, +\ZF, \HOL, \HOLCF. -The next section is a quick introduction to the simplifier, the later -sections explain advanced features. +The first section is a quick introduction to the simplifier that +should be sufficient to get started. The later sections explain more +advanced features. + \section{Simplification for dummies} \label{sec:simp-for-dummies} -In some logics (\FOL, {\HOL} and \ZF), the simplifier is particularly easy to -use because it supports the concept of a {\em current - simpset}\index{simpset!current}. This is a default set of simplification -rules. All commands are interpreted relative to the current simpset. For -example, in the theory of arithmetic the goal +Basic use of the simplifier is particularly easy because each theory +is equipped with an implicit {\em current + simpset}\index{simpset!current}. This provides sensible default +information in many cases. A suite of commands refer to the implicit +simpset of the current theory context. + +\begin{warn} + Make sure that you are working within the correct theory context. + Executing proofs interactively, or loading them from ML files + without associated theories may require setting the current theory + manually via the \ttindex{context} command. +\end{warn} + +\subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs} \begin{ttbox} +Simp_tac : int -> tactic +Asm_simp_tac : int -> tactic +Full_simp_tac : int -> tactic +Asm_full_simp_tac : int -> tactic +trace_simp : bool ref \hfill{\bf initially false} +\end{ttbox} + +\begin{ttdescription} +\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the + current simpset. It may solve the subgoal completely if it has + become trivial, using the simpset's solver tactic. + +\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification} + is like \verb$Simp_tac$, but extracts additional rewrite rules from + the local assumptions. + +\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also + simplifies the assumptions (without using the assumptions to + simplify each other or the actual goal). + +\item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$, + but also simplifies the assumptions one by one. Working from + \emph{left to right}, it uses each assumption in the simplification + of those following. + +\item[set \ttindexbold{trace_simp};] makes the simplifier output + internal operations. This includes rewrite steps, but also + bookkeeping like modifications of the simpset. +\end{ttdescription} + +\medskip + +As an example, consider the theory of arithmetic in \HOL. The (rather +trivial) goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call +of \texttt{Simp_tac} as follows: +\begin{ttbox} +context Arith.thy; +goal Arith.thy "0 + (x + 0) = x + 0 + 0"; {\out 1. 0 + (x + 0) = x + 0 + 0} +by (Simp_tac 1); +{\out Level 1} +{\out 0 + (x + 0) = x + 0 + 0} +{\out No subgoals!} \end{ttbox} -can be solved by a single -\begin{ttbox} -by (Simp_tac 1); -\end{ttbox} -The simplifier uses the current simpset, which in the case of arithmetic -contains the required theorems $\Var{n}+0 = \Var{n}$ and $0+\Var{n} = + +The simplifier uses the current simpset of \texttt{Arith.thy}, which +contains suitable theorems like $\Var{n}+0 = \Var{n}$ and $0+\Var{n} = \Var{n}$. -If assumptions of the subgoal are also needed in the simplification -process, as in +\medskip In many cases, assumptions of a subgoal are also needed in +the simplification process. For example, \texttt{x = 0 ==> x + x = 0} +is solved by \texttt{Asm_simp_tac} as follows: \begin{ttbox} {\out 1. x = 0 ==> x + x = 0} -\end{ttbox} -then there is the more powerful -\begin{ttbox} by (Asm_simp_tac 1); \end{ttbox} -which solves the above goal. -There are four basic simplification tactics: -\begin{ttdescription} -\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the current - simpset. It may solve the subgoal completely if it has become trivial, - using the solver. - -\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification} - is like \verb$Simp_tac$, but extracts additional rewrite rules from the - assumptions. - -\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also - simplifies the assumptions (but without using the assumptions to simplify - each other or the actual goal.) - -\item[\ttindexbold{Asm_full_simp_tac}] - is like \verb$Asm_simp_tac$, but also simplifies the assumptions one by - one. {\em Working from left to right, it uses each assumption in the - simplification of those following.} -\end{ttdescription} - -{\tt Asm_full_simp_tac} is the most powerful of this quartet but may also -loop where some of the others terminate. For example, +\medskip {\tt Asm_full_simp_tac} is the most powerful of this quartet +of tactics but may also loop where some of the others terminate. For +example, \begin{ttbox} -{\out 1. ALL x. f(x) = g(f(g(x))) ==> f(0) = f(0)+0} +{\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0} \end{ttbox} -is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt Asm_simp_tac} -loop because the rewrite rule $f(\Var{x}) = f(g(f(\Var{x})))$ extracted from -the assumption does not terminate. Isabelle notices certain simple forms of -nontermination, but not this one. +is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt + Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} = +g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not +terminate. Isabelle notices certain simple forms of nontermination, +but not this one. \begin{warn} Since \verb$Asm_full_simp_tac$ works from left to right, it sometimes misses opportunities for simplification: given the subgoal \begin{ttbox} -{\out [| P(f(a)); f(a) = t |] ==> ...} +{\out [| P (f a); f a = t |] ==> \dots} \end{ttbox} \verb$Asm_full_simp_tac$ will not simplify the first assumption using the second but will leave the assumptions unchanged. See \S\ref{sec:reordering-asms} for ways around this problem. \end{warn} +\medskip + Using the simplifier effectively may take a bit of experimentation. -\index{tracing!of simplification}\index{*trace_simp} The tactics can -be traced by setting \verb$trace_simp$. +Set the \verb$trace_simp$\index{tracing!of simplification} flag to get +a better idea of what is going on. The resulting output can be +enormous, especially since invocations of the simplifier are often +nested (e.g.\ when solving conditions of rewrite rules). + + +\subsection{Modifying the current simpset} +\begin{ttbox} +Addsimps : thm list -> unit +Delsimps : thm list -> unit +Addsimprocs : simproc list -> unit +Delsimprocs : simproc list -> unit +Addcongs : thm list -> unit +Delcongs : thm list -> unit +\end{ttbox} -There is not just one global current simpset, but one associated with each -theory as well. How are these simpset built up? -\begin{enumerate} -\item When loading {\tt T.thy}, the current simpset is initialized with the - union of the simpsets associated with all the ancestors of {\tt T}. In - addition, certain constructs in {\tt T} may add new rules to the simpset, - e.g.\ \ttindex{datatype} and \ttindex{primrec} in \HOL. Definitions are not - added automatically! -\item The script in {\tt T.ML} may manipulate the current simpset further by - explicitly adding/deleting theorems to/from it (see below). -\item After {\tt T.ML} has been read, the current simpset is associated with - theory {\tt T}. -\end{enumerate} -The current simpset is manipulated by -\begin{ttbox} -Addsimps, Delsimps: thm list -> unit -\end{ttbox} +Depending on the theory context, the \texttt{Add} and \texttt{Del} +functions manipulate basic components of the associated current +simpset. Internally, all rewrite rules have to be expressed as +(conditional) meta-equalities. This form is derived automatically +from object-level equations that are supplied by the user. Another +source of rewrite rules are \emph{simplification procedures}, that is +\ML\ functions that produce suitable theorems on demand, depending on +the current redex. Congruences are a more advanced feature; see +\S\ref{sec:simp-congs}. + \begin{ttdescription} -\item[\ttindexbold{Addsimps} $thms$] adds $thms$ to the current simpset -\item[\ttindexbold{Delsimps} $thms$] deletes $thms$ from the current simpset + +\item[\ttindexbold{Addsimps} $thms$;] adds rewrite rules derived from + $thms$ to the current simpset. + +\item[\ttindexbold{Delsimps} $thms$;] deletes rewrite rules derived + from $thms$ from the current simpset. + +\item[\ttindexbold{Addsimprocs} $procs$;] adds simplification + procedures $procs$ to the current simpset. + +\item[\ttindexbold{Delsimprocs} $procs$;] deletes simplification + procedures $procs$ from the current simpset. + +\item[\ttindexbold{Addcongs} $thms$;] adds congruence rules to the + current simpset. + +\item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules to the + current simpset. + \end{ttdescription} -Generally useful simplification rules $\Var{n}+0 = \Var{n}$ should be added -to the current simpset right after they have been proved. Those of a more -specific nature (e.g.\ the laws of de~Morgan, which alter the structure of a -formula) should only be added for specific proofs and deleted again -afterwards. Conversely, it may also happen that a generally useful rule needs -to be removed for a certain proof and is added again afterwards. Well -designed simpsets need few temporary additions or deletions. +When a new theory is built, its implicit simpset is initialized by the +union of the respective simpsets of its parent theories. In addition, +certain theory definition constructs (e.g.\ \ttindex{datatype} and +\ttindex{primrec} in \HOL) implicitly augment the current simpset. +Ordinary definitions are not added automatically! + +It is up the user to manipulate the current simpset further by +explicitly adding or deleting theorems and simplification procedures. + +\medskip + +Good simpsets are hard to design. As a rule of thump, generally +useful ``simplification rules'' like $\Var{n}+0 = \Var{n}$ should be +added to the current simpset right after they have been proved. Those +of a more specific nature (e.g.\ the laws of de~Morgan, which alter +the structure of a formula) should only be added for specific proofs +and deleted again afterwards. Conversely, it may also happen that a +generally useful rule needs to be removed for a certain proof and is +added again afterwards. The need of frequent temporary additions or +deletions may indicate a badly designed simpset. \begin{warn} - The union of the ancestor simpsets (as described above) is not always a good - simpset for the new theory. If some ancestors have deleted simplification - rules because they are no longer wanted, while others have left those rules - in, then the union will contain the unwanted rules. If the ancestor - simpsets differ in other components (the subgoaler, solver, looper or rule - preprocessor: see below), then you cannot be sure which version of that - component will be inherited. You may have to set the component explicitly - for the new theory's simpset by an assignment of the form - {\tt simpset := \dots}. -\end{warn} - -\begin{warn} - If you execute proofs interactively, or load them from an ML file without - associated {\tt .thy} file, you must set the current simpset by calling - \ttindex{set_current_thy}~{\tt"}$T${\tt"}, where $T$ is the name of the - theory you want to work in. If you have just loaded $T$, this is not - necessary. + The union of the parent simpsets (as described above) is not always + a good starting point for the new theory. If some ancestors have + deleted simplification rules because they are no longer wanted, + while others have left those rules in, then the union will contain + the unwanted rules. \end{warn} \section{Simplification sets}\index{simplification sets} -The simplification tactics are controlled by {\bf simpsets}. These -consist of several components, including rewrite rules, congruence -rules, the subgoaler, the solver and the looper. The simplifier -should be set up with sensible defaults so that most simplifier calls -specify only rewrite rules. Experienced users can exploit the other -components to streamline proofs. + +The simplifier is controlled by information contained in {\bf + simpsets}. These consist of several components, including rewrite +rules, simplification procedures, congruence rules, and the subgoaler, +solver and looper tactics. The simplifier should be set up with +sensible defaults so that most simplifier calls specify only rewrite +rules or simplification procedures. Experienced users can exploit the +other components to streamline proofs in more sophisticated manners. + +\subsection{Inspecting simpsets} +\begin{ttbox} +print_ss : simpset -> unit +\end{ttbox} +\begin{ttdescription} + +\item[\ttindexbold{print_ss} $ss$;] displays the printable contents of + simpset $ss$. This includes the rewrite rules and congruences in + their internal form expressed as meta-equalities. The names of the + simplification procedures and the patterns they are invoked on are + also shown. The other parts, functions and tactics, are + non-printable. + +\end{ttdescription} + -Logics like \HOL, which support a current -simpset\index{simpset!current}, store its value in an ML reference -variable called {\tt simpset}\index{simpset@{\tt simpset} ML value}. +\subsection{Building simpsets} +\begin{ttbox} +empty_ss : simpset +merge_ss : simpset * simpset -> simpset +\end{ttbox} +\begin{ttdescription} + +\item[\ttindexbold{empty_ss}] is the empty simpset. This is not very + useful under normal circumstances because it doesn't contain + suitable tactics (subgoaler etc.). When setting up the simplifier + for a particular object-logic, one will typically define a more + appropriate ``almost empty'' simpset. For example, in \HOL\ this is + called \ttindexbold{HOL_basic_ss}. + +\item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ + and $ss@2$ by building the union of their respective rewrite rules, + simplification procedures and congruences. The other components + (tactics etc.) cannot be merged, though; they are simply inherited + from either simpset. + +\end{ttdescription} + + +\subsection{Accessing the current simpset} + +\begin{ttbox} +simpset : unit -> simpset +simpset_ref : unit -> simpset ref +simpset_of : theory -> simpset +simpset_ref_of : theory -> simpset ref +print_simpset : theory -> unit +\end{ttbox} + +Each theory contains a current simpset\index{simpset!current} stored +within a private ML reference variable. This can be retrieved and +modified as follows. + +\begin{ttdescription} + +\item[\ttindexbold{simpset}();] retrieves the simpset value from the + current theory context. + +\item[\ttindexbold{simpset_ref}();] retrieves the simpset reference + variable from the current theory context. This can be assigned to + by using \texttt{:=} in ML. + +\item[\ttindexbold{simpset_of} $thy$;] retrieves the simpset value + from theory $thy$. + +\item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset + reference variable from theory $thy$. + +\item[\ttindexbold{print_simpset} $thy$;] prints the current simpset + of theory $thy$ in the same way as \texttt{print_ss}. + +\end{ttdescription} + \subsection{Rewrite rules} -\index{rewrite rules|(} -Rewrite rules are theorems expressing some form of equality: +\begin{ttbox} +addsimps : simpset * thm list -> simpset \hfill{\bf infix 4} +delsimps : simpset * thm list -> simpset \hfill{\bf infix 4} +\end{ttbox} + +\index{rewrite rules|(} Rewrite rules are theorems expressing some +form of equality, for example: \begin{eqnarray*} Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\ \Var{P}\conj\Var{P} &\bimp& \Var{P} \\ \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\} \end{eqnarray*} Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = -0$ are permitted; the conditions can be arbitrary formulas. +0$ are also permitted; the conditions can be arbitrary formulas. -Internally, all rewrite rules are translated into meta-equalities, theorems -with conclusion $lhs \equiv rhs$. Each simpset contains a function for -extracting equalities from arbitrary theorems. For example, -$\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} \equiv -False$. This function can be installed using \ttindex{setmksimps} but only -the definer of a logic should need to do this; see \S\ref{sec:setmksimps}. -The function processes theorems added by \ttindex{addsimps} as well as -local assumptions. +Internally, all rewrite rules are translated into meta-equalities, +theorems with conclusion $lhs \equiv rhs$. Each simpset contains a +function for extracting equalities from arbitrary theorems. For +example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} +\equiv False$. This function can be installed using +\ttindex{setmksimps} but only the definer of a logic should need to do +this; see \S\ref{sec:setmksimps}. The function processes theorems +added by \texttt{addsimps} as well as local assumptions. +\begin{ttdescription} + +\item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived + from $thms$ to the simpset $ss$. + +\item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules + derived from $thms$ from the simpset $ss$. + +\end{ttdescription} \begin{warn} -The simplifier will accept all standard rewrite rules: those -where all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} = -{(\Var{i}+\Var{j})+\Var{k}}$ is ok. - -It will also deal gracefully with all rules whose left-hand sides are -so-called {\em higher-order patterns}~\cite{nipkow-patterns}. -\indexbold{higher-order pattern}\indexbold{pattern, higher-order} -These are terms in $\beta$-normal form (this will always be the case unless -you have done something strange) where each occurrence of an unknown is of -the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound -variables. Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall -x.\Var{P}(x)) \land (\forall x.\Var{Q}(x))$ is also ok, in both directions. - -In some rare cases the rewriter will even deal with quite general rules: for -example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ rewrites $g(a) \in -range(g)$ to $True$, but will fail to match $g(h(b)) \in range(\lambda -x.g(h(x)))$. However, you can replace the offending subterms (in our case -$\Var{f}(\Var{x})$, which is not a pattern) by adding new variables and -conditions: $\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) -= True$ is acceptable as a conditional rewrite rule since conditions can -be arbitrary terms. - -There is no restriction on the form of the right-hand sides. + The simplifier will accept all standard rewrite rules: those where + all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} = + {(\Var{i}+\Var{j})+\Var{k}}$ is OK. + + It will also deal gracefully with all rules whose left-hand sides + are so-called {\em higher-order patterns}~\cite{nipkow-patterns}. + \indexbold{higher-order pattern}\indexbold{pattern, higher-order} + These are terms in $\beta$-normal form (this will always be the case + unless you have done something strange) where each occurrence of an + unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are + distinct bound variables. Hence $(\forall x.\Var{P}(x) \land + \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) \land (\forall + x.\Var{Q}(x))$ is also OK, in both directions. + + In some rare cases the rewriter will even deal with quite general + rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ + rewrites $g(a) \in range(g)$ to $True$, but will fail to match + $g(h(b)) \in range(\lambda x.g(h(x)))$. However, you can replace + the offending subterms (in our case $\Var{f}(\Var{x})$, which is not + a pattern) by adding new variables and conditions: $\Var{y} = + \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) = True$ is + acceptable as a conditional rewrite rule since conditions can be + arbitrary terms. + + There is basically no restriction on the form of the right-hand + sides. They may not contain extraneous term or type variables, + though. \end{warn} - \index{rewrite rules|)} -\subsection{*Congruence rules}\index{congruence rules} + +\subsection{Simplification procedures} +\begin{ttbox} +addsimprocs : simpset * simproc list -> simpset +delsimprocs : simpset * simproc list -> simpset +\end{ttbox} + +Simplification procedures are {\ML} functions that may produce +\emph{proven} rewrite rules on demand. They are associated with +certain patterns that conceptually represent left-hand sides of +equations; these are shown by \texttt{print_ss}. During its +operation, the simplifier may offer a simplification procedure the +current redex and ask for a suitable rewrite rule. Thus rules may be +specifically fashioned for particular situations, resulting in a more +powerful mechanism than term rewriting by a fixed set of rules. + + +\begin{ttdescription} + +\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds simplification + procedures $procs$ to the current simpset. + +\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification + procedures $procs$ from the current simpset. + +\end{ttdescription} + + +\subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs} +\begin{ttbox} +addcongs : simpset * thm list -> simpset \hfill{\bf infix 4} +delcongs : simpset * thm list -> simpset \hfill{\bf infix 4} +addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4} +deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4} +\end{ttbox} + Congruence rules are meta-equalities of the form \[ \dots \Imp f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). @@ -210,13 +389,36 @@ \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2}) \] -Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules -from it when simplifying~$P@2$. Such local assumptions are effective for -rewriting formulae such as $x=0\imp y+x=y$. The local assumptions are also -provided as theorems to the solver; see page~\pageref{sec:simp-solver} below. +Given this rule, the simplifier assumes $Q@1$ and extracts rewrite +rules from it when simplifying~$P@2$. Such local assumptions are +effective for rewriting formulae such as $x=0\imp y+x=y$. The local +assumptions are also provided as theorems to the solver; see +\S~\ref{sec:simp-solver} below. -Here are some more examples. The congruence rule for bounded quantifiers -also supplies contextual information, this time about the bound variable: +\begin{ttdescription} + +\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the + simpset $ss$. These are derived from $thms$ in an appropriate way, + depending on the underlying object-logic. + +\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules + derived from $thms$. + +\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in + their internal form (conclusions using meta-equality) to simpset + $ss$. This is the basic mechanism that \texttt{addcongs} is built + on. It should be rarely used directly. + +\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules + in internal form from simpset $ss$. + +\end{ttdescription} + +\medskip + +Here are some more examples. The congruence rule for bounded +quantifiers also supplies contextual information, this time about the +bound variable: \begin{eqnarray*} &&\List{\Var{A}=\Var{B};\; \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\ @@ -238,41 +440,57 @@ This can make simplification much faster, but may require an extra case split to prove the goal. -Congruence rules are added/deleted using -\ttindexbold{addeqcongs}/\ttindex{deleqcongs}. -Their conclusion must be a meta-equality, as in the examples above. It is more -natural to derive the rules with object-logic equality, for example -\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} - \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}), -\] -Each object-logic should define operators called \ttindex{addcongs} and -\ttindex{delcongs} that expects object-equalities and translates them into -meta-equalities. -\subsection{*The subgoaler} +\subsection{*The subgoaler}\label{sec:simp-subgoaler} +\begin{ttbox} +setsubgoaler : simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4} +prems_of_ss : simpset -> thm list +\end{ttbox} + The subgoaler is the tactic used to solve subgoals arising out of conditional rewrite rules or congruence rules. The default should be -simplification itself. Occasionally this strategy needs to be changed. For -example, if the premise of a conditional rule is an instance of its -conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the -default strategy could loop. +simplification itself. Occasionally this strategy needs to be +changed. For example, if the premise of a conditional rule is an +instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} +< \Var{n}$, the default strategy could loop. -The subgoaler can be set explicitly with \ttindex{setsubgoaler}. For -example, the subgoaler +\begin{ttdescription} + +\item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of + $ss$ to $tacf$. The function $tacf$ will be applied to the current + simplifier context expressed as a simpset. + +\item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of + premises from simplifier context $ss$. This may be non-empty only + if the simplifier has been told to utilize local assumptions in the + first place, e.g.\ if invoked via \texttt{asm_simp_tac}. + +\end{ttdescription} + +As an example, consider the following subgoaler: \begin{ttbox} -fun subgoal_tac ss = assume_tac ORELSE' - resolve_tac (prems_of_ss ss) ORELSE' - asm_simp_tac ss; +fun subgoaler ss = + assume_tac ORELSE' + resolve_tac (prems_of_ss ss) ORELSE' + asm_simp_tac ss; \end{ttbox} -tries to solve the subgoal by assumption or with one of the premises, calling -simplification only if that fails; here {\tt prems_of_ss} extracts the -current premises from a simpset. +This tactic first tries to solve the subgoal by assumption or by +resolving with with one of the premises, calling simplification only +if that fails. + \subsection{*The solver}\label{sec:simp-solver} +\begin{ttbox} +setSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} +addSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} +setSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} +addSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} +\end{ttbox} + The solver is a pair of tactics that attempt to solve a subgoal after -simplification. Typically it just proves trivial subgoals such as {\tt - True} and $t=t$. It could use sophisticated means such as {\tt - blast_tac}, though that could make simplification expensive. +simplification. Typically it just proves trivial subgoals such as +{\tt True} and $t=t$. It could use sophisticated means such as {\tt + blast_tac}, though that could make simplification expensive. Rewriting does not instantiate unknowns. For example, rewriting cannot prove $a\in \Var{A}$ since this requires @@ -281,43 +499,66 @@ simplifier can handle a conditional rewrite rule whose condition contains extra variables. When a simplification tactic is to be combined with other provers, especially with the classical reasoner, -it is important whether it can be considered safe or not. Therefore, -the solver is split into a safe and an unsafe part. Both parts can be -set independently, using either \ttindex{setSSolver} with a safe -tactic as argument, or \ttindex{setSolver} with an unsafe tactic. -Additional solvers, which are tried after the already set solvers, may -be added using \ttindex{addSSolver} and \ttindex{addSolver}. +it is important whether it can be considered safe or not. For this +reason the solver is split into a safe and an unsafe part. The standard simplification strategy solely uses the unsafe solver, -which is appropriate in most cases. But for special applications where +which is appropriate in most cases. For special applications where the simplification process is not allowed to instantiate unknowns -within the goal, the tactic \ttindexbold{safe_asm_full_simp_tac} is -provided. It uses the \emph{safe} solver for the current subgoal, but -applies ordinary unsafe {\tt asm_full_simp_tac} for recursive internal -simplifications (for conditional rules or congruences). +within the goal, simplification starts with the safe solver, but may +still apply the ordinary unsafe one in nested simplifications for +conditional rules or congruences. + +\begin{ttdescription} + +\item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the + \emph{safe} solver of $ss$. + +\item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an + additional \emph{safe} solver; it will be tried after the solvers + which had already been present in $ss$. + +\item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the + unsafe solver of $ss$. + +\item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an + additional unsafe solver; it will be tried after the solvers which + had already been present in $ss$. -\index{assumptions!in simplification} -The tactic is presented with the full goal, including the asssumptions. -Hence it can use those assumptions (say by calling {\tt assume_tac}) even -inside {\tt simp_tac}, which otherwise does not use assumptions. The -solver is also supplied a list of theorems, namely assumptions that hold in -the local context. +\end{ttdescription} + +\medskip -The subgoaler is also used to solve the premises of congruence rules, which -are usually of the form $s = \Var{x}$, where $s$ needs to be simplified and -$\Var{x}$ needs to be instantiated with the result. Hence the subgoaler -should call the simplifier at some point. The simplifier will then call the -solver, which must therefore be prepared to solve goals of the form $t = -\Var{x}$, usually by reflexivity. In particular, reflexivity should be -tried before any of the fancy tactics like {\tt blast_tac}. +\index{assumptions!in simplification} The solver tactic is invoked +with a list of theorems, namely assumptions that hold in the local +context. This may be non-empty only if the simplifier has been told +to utilize local assumptions in the first place, e.g.\ if invoked via +\texttt{asm_simp_tac}. The solver is also presented the full goal +including its assumptions in any case. Thus it can use these (e.g.\ +by calling \texttt{assume_tac}), even if the list of premises is not +passed. + +\medskip + +As explained in \S\ref{sec:simp-subgoaler}, the subgoaler is also used +to solve the premises of congruence rules. These are usually of the +form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$ +needs to be instantiated with the result. Typically, the subgoaler +will invoke the simplifier at some point, which will eventually call +the solver. For this reason, solver tactics must be prepared to solve +goals of the form $t = \Var{x}$, usually by reflexivity. In +particular, reflexivity should be tried before any of the fancy +tactics like {\tt blast_tac}. It may even happen that due to simplification the subgoal is no longer an equality. For example $False \bimp \Var{Q}$ could be rewritten to $\neg\Var{Q}$. To cover this case, the solver could try resolving with the theorem $\neg False$. +\medskip + \begin{warn} - If the simplifier aborts with the message {\tt Failed congruence + If the simplifier aborts with the message \texttt{Failed congruence proof!}, then the subgoaler or solver has failed to prove a premise of a congruence rule. This should never occur under normal circumstances; it indicates that some congruence rule, or possibly @@ -325,145 +566,138 @@ \end{warn} -\subsection{*The looper} -The looper is a tactic that is applied after simplification, in case the -solver failed to solve the simplified goal. If the looper succeeds, the -simplification process is started all over again. Each of the subgoals -generated by the looper is attacked in turn, in reverse order. A -typical looper is case splitting: the expansion of a conditional. Another -possibility is to apply an elimination rule on the assumptions. More -adventurous loopers could start an induction. The looper is set with -\ttindex{setloop}. Additional loopers, which are tried after the already set -looper, may be added with \ttindex{addloop}. +\subsection{*The looper}\label{sec:simp-looper} +\begin{ttbox} +setloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4} +addloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4} +addsplits : simpset * thm list -> simpset \hfill{\bf infix 4} +\end{ttbox} + +The looper is a tactic that is applied after simplification, in case +the solver failed to solve the simplified goal. If the looper +succeeds, the simplification process is started all over again. Each +of the subgoals generated by the looper is attacked in turn, in +reverse order. + +A typical looper is case splitting: the expansion of a conditional. +Another possibility is to apply an elimination rule on the +assumptions. More adventurous loopers could start an induction. + +\begin{ttdescription} + +\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the looper + of $ss$. + +\item[$ss$ \ttindexbold{addloop} $tacf$] adds $tacf$ as an additional + looper; it will be tried after the loopers which had already been + present in $ss$. + +\item[$ss$ \ttindexbold{addsplits} $thms$] adds + \texttt{(split_tac~$thms$)} as an additional looper. + +\end{ttdescription} + -\begin{figure} -\index{*simpset ML type} -\index{*empty_ss} -\index{*rep_ss} -\index{*prems_of_ss} -\index{*setloop} -\index{*addloop} -\index{*setSSolver} -\index{*addSSolver} -\index{*setSolver} -\index{*addSolver} -\index{*setsubgoaler} -\index{*setmksimps} -\index{*addsimps} -\index{*delsimps} -\index{*addeqcongs} -\index{*deleqcongs} -\index{*merge_ss} -\index{*simpset} -\index{*Addsimps} -\index{*Delsimps} -\index{*simp_tac} -\index{*asm_simp_tac} -\index{*full_simp_tac} -\index{*asm_full_simp_tac} -\index{*safe_asm_full_simp_tac} -\index{*Simp_tac} -\index{*Asm_simp_tac} -\index{*Full_simp_tac} -\index{*Asm_full_simp_tac} +\section{The simplification tactics}\label{simp-tactics} +\index{simplification!tactics}\index{tactics!simplification} +\begin{ttbox} +simp_tac : simpset -> int -> tactic +asm_simp_tac : simpset -> int -> tactic +full_simp_tac : simpset -> int -> tactic +asm_full_simp_tac : simpset -> int -> tactic +safe_asm_full_simp_tac : simpset -> int -> tactic +SIMPSET : (simpset -> tactic) -> tactic +SIMPSET' : (simpset -> 'a -> tactic) -> 'a -> tactic +\end{ttbox} -\begin{ttbox} -infix 4 setsubgoaler setloop addloop - setSSolver addSSolver setSolver addSolver - setmksimps addsimps delsimps addeqcongs deleqcongs; +These are the basic tactics that are underlying any actual +simplification work. The rewriting strategy is always strictly bottom +up, except for congruence rules, which are applied while descending +into a term. Conditions in conditional rewrite rules are solved +recursively before the rewrite rule is applied. -signature SIMPLIFIER = -sig - type simpset - val empty_ss: simpset - val rep_ss: simpset -> {\ttlbrace}simps: thm list, procs: string list, - congs: thm list, - subgoal_tac: simpset -> int -> tactic, - loop_tac: int -> tactic, - finish_tac: thm list -> int -> tactic, - unsafe_finish_tac: thm list -> int -> tactic{\ttrbrace} - val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset - val setloop: simpset * (int -> tactic) -> simpset - val addloop: simpset * (int -> tactic) -> simpset - val setSSolver: simpset * (thm list -> int -> tactic) -> simpset - val addSSolver: simpset * (thm list -> int -> tactic) -> simpset - val setSolver: simpset * (thm list -> int -> tactic) -> simpset - val addSolver: simpset * (thm list -> int -> tactic) -> simpset - val setmksimps: simpset * (thm -> thm list) -> simpset - val addsimps: simpset * thm list -> simpset - val delsimps: simpset * thm list -> simpset - val addeqcongs: simpset * thm list -> simpset - val deleqcongs: simpset * thm list -> simpset - val merge_ss: simpset * simpset -> simpset - val prems_of_ss: simpset -> thm list - val simpset: simpset ref - val Addsimps: thm list -> unit - val Delsimps: thm list -> unit - val simp_tac: simpset -> int -> tactic - val asm_simp_tac: simpset -> int -> tactic - val full_simp_tac: simpset -> int -> tactic - val asm_full_simp_tac: simpset -> int -> tactic - val safe_asm_full_simp_tac: simpset -> int -> tactic - val Simp_tac: int -> tactic - val Asm_simp_tac: int -> tactic - val Full_simp_tac: int -> tactic - val Asm_full_simp_tac: int -> tactic -end; -\end{ttbox} -\caption{The simplifier primitives} \label{SIMPLIFIER} -\end{figure} +\begin{ttdescription} + +\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, + \ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are + the basic simplification tactics that work exactly like their + namesakes in \S\ref{sec:simp-for-dummies}, except that they are + explicitly supplied with a simpset. + +\item[\ttindexbold{safe_asm_full_simp_tac}] is like + \texttt{asm_full_simp_tac}, but uses the safe solver as explained in + \S\ref{sec:simp-solver}. This tactic is mainly intended for + building special tools, e.g.\ for combining the simplifier with the + classical reasoner. It is rarely used directly. + +\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$] + are tacticals that make a tactic depend on the implicit current + simpset of the theory associated with the proof state they are + applied on. +\end{ttdescription} -\section{The simplification tactics} -\label{simp-tactics} -\index{simplification!tactics} -\index{tactics!simplification} +\medskip -The actual simplification work is performed by the following basic tactics: -\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, -\ttindexbold{full_simp_tac} and \ttindexbold{asm_full_simp_tac}. They work -exactly like their namesakes in \S\ref{sec:simp-for-dummies}, except that -they are explicitly supplied with a simpset. This is because the ones in -\S\ref{sec:simp-for-dummies} are defined in terms of the ones above, e.g. -\begin{ttbox} -fun Simp_tac i = simp_tac (!simpset) i; -\end{ttbox} -where \ttindex{!simpset} is the current simpset\index{simpset!current}. - -The rewriting strategy of all four tactics is strictly bottom up, except for -congruence rules, which are applied while descending into a term. Conditions -in conditional rewrite rules are solved recursively before the rewrite rule -is applied. - -The infix operation \ttindex{addsimps} adds rewrite rules to a -simpset, while \ttindex{delsimps} deletes them. They are used to -implement \ttindex{Addsimps} and \ttindex{Delsimps}, e.g. -\begin{ttbox} -fun Addsimps thms = (simpset := (!simpset addsimps thms)); -\end{ttbox} -and can also be used directly, even in the presence of a current simpset. For -example +Local modifications of simpsets within a proof are often much cleaner +by using above tactics in conjunction with explicit simpsets, rather +than their capitalized counterparts. For example \begin{ttbox} Addsimps \(thms\); by (Simp_tac \(i\)); Delsimps \(thms\); \end{ttbox} -can be compressed into +can be expressed more appropriately as \begin{ttbox} -by (simp_tac (!simpset addsimps \(thms\)) \(i\)); +by (simp_tac (simpset() addsimps \(thms\)) \(i\)); \end{ttbox} -The simpset associated with a particular theory can be retrieved via the name -of the theory using the function -\begin{ttbox} -simpset_of: string -> simpset -\end{ttbox}\index{*simpset_of} +\medskip + +Also note that functions depending implicitly on the current theory +context (like capital \texttt{Simp_tac} and the other commands of +\S\ref{sec:simp-for-dummies}) should be considered harmful outside of +actual proof scripts. In particular, ML programs like theory +definition packages or special tactics should refer to simpsets only +explicitly, via the above tactics used in conjunction with +\texttt{simpset_of} or the \texttt{SIMPSET} tacticals. + +\begin{warn} + There is a subtle difference between \texttt{(SIMPSET'~$tacf$)} and + \texttt{($tacf$~(simpset()))}. For example \texttt{(SIMPSET' + simp_tac)} would depend on the theory of the proof state it is + applied to, while \texttt{(simp_tac (simpset()))} implicitly refers + to the current theory context. Both are usually the same in proof + scripts, provided that goals are only stated within the current + theory. Robust programs would not count on that, of course. +\end{warn} + -To remind yourself of what is in a simpset, use the function \verb$rep_ss$ to -return its simplification and congruence rules. +\section{Forward simplification rules} +\index{simplification!forward rules} +\begin{ttbox}\index{*simplify}\index{*asm_simplify}\index{*full_simplify}\index{*asm_full_simplify} +simplify : simpset -> thm -> thm +asm_simplify : simpset -> thm -> thm +full_simplify : simpset -> thm -> thm +asm_full_simplify : simpset -> thm -> thm +\end{ttbox} + +These are forward rules, simplifying theorems in a similar way as the +corresponding simplification tactics do. The forward rules affect the whole -\section{Examples using the simplifier} + subgoals of a proof state. The +looper~/ solver process as described in \S\ref{sec:simp-looper} and +\S\ref{sec:simp-solver} does not apply here, though. + +\begin{warn} + Forward simplification should be used rarely in ordinary proof + scripts. It as mainly intended to provide an internal interface to + the simplifier for ML coded special utilities. +\end{warn} + + +\section{Examples of using the simplifier} \index{examples!of simplification} Assume we are working within {\tt FOL} (cf.\ \texttt{FOL/ex/Nat}) and that \begin{ttdescription} @@ -477,8 +711,8 @@ is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. \end{ttdescription} -We augment the implicit simpset of {\FOL} with the basic rewrite rules -for natural numbers: +We augment the implicit simpset inherited from \texttt{Nat} with the +basic rewrite rules for natural numbers: \begin{ttbox} Addsimps [add_0, add_Suc]; \end{ttbox} @@ -548,7 +782,7 @@ Switching tracing on illustrates how the simplifier solves the remaining subgoal: \begin{ttbox} -trace_simp := true; +set trace_simp; by (Asm_simp_tac 1); \ttbreak {\out Adding rewrite rule:} @@ -610,14 +844,9 @@ {\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} \end{ttbox} The remaining subgoal requires rewriting by the premise, so we add it -to the current simpset:\footnote{The previous simplifier required - congruence rules for function variables like~$f$ in order to - simplify their arguments. It was more general than the current - simplifier, but harder to use and slower. The present simplifier - can be given congruence rules to realize non-standard simplification - of a function's arguments, but this is seldom necessary.} +to the current simpset: \begin{ttbox} -by (asm_simp_tac (!simpset addsimps [prem]) 1); +by (asm_simp_tac (simpset() addsimps [prem]) 1); {\out Level 3} {\out f(i + j) = i + f(j)} {\out No subgoals!} @@ -627,8 +856,9 @@ \label{sec:reordering-asms} \index{assumptions!reordering} -As mentioned above, \ttindex{asm_full_simp_tac} may require the assumptions -to be permuted to be more effective. Given the subgoal +As mentioned in \S\ref{sec:simp-for-dummies-tacs}, +\ttindex{asm_full_simp_tac} may require the assumptions to be permuted +to be more effective. Given the subgoal \begin{ttbox} {\out 1. [| P(f(a)); Q; f(a) = t; R |] ==> S} \end{ttbox} @@ -654,12 +884,18 @@ {\out 1. [| Q; f(a) = t; R; P(f(a)) |] ==> S} \end{ttbox} -Note that reordering assumptions usually leads to brittle proofs and should -therefore be avoided. Future versions of \verb$asm_full_simp_tac$ may remove -the need for such manipulations. +\begin{warn} + Reordering assumptions usually leads to brittle proofs and should be + avoided. Future versions of \verb$asm_full_simp_tac$ may remove the + need for such manipulations. +\end{warn} + \section{Permutative rewrite rules} \index{rewrite rules!permutative|(} +\begin{ttbox} +settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4} +\end{ttbox} A rewrite rule is {\bf permutative} if the left-hand side and right-hand side are the same up to renaming of variables. The most common permutative @@ -667,24 +903,39 @@ (x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ for sets. Such rules are common enough to merit special attention. -Because ordinary rewriting loops given such rules, the simplifier employs a -special strategy, called {\bf ordered rewriting}\index{rewriting!ordered}. -There is a standard lexicographic ordering on terms. A permutative rewrite -rule is applied only if it decreases the given term with respect to this -ordering. For example, commutativity rewrites~$b+a$ to $a+b$, but then -stops because $a+b$ is strictly less than $b+a$. The Boyer-Moore theorem -prover~\cite{bm88book} also employs ordered rewriting. +Because ordinary rewriting loops given such rules, the simplifier +employs a special strategy, called {\bf ordered + rewriting}\index{rewriting!ordered}. There is a standard +lexicographic ordering on terms. This should be perfectly OK in most +cases, but can be changed for special applications. + +\begin{ttdescription} + +\item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as + term order in simpset $ss$. + +\end{ttdescription} + +\medskip -Permutative rewrite rules are added to simpsets just like other rewrite -rules; the simplifier recognizes their special status automatically. They -are most effective in the case of associative-commutative operators. -(Associativity by itself is not permutative.) When dealing with an -AC-operator~$f$, keep the following points in mind: +A permutative rewrite rule is applied only if it decreases the given +term with respect to this ordering. For example, commutativity +rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less +than $b+a$. The Boyer-Moore theorem prover~\cite{bm88book} also +employs ordered rewriting. + +Permutative rewrite rules are added to simpsets just like other +rewrite rules; the simplifier recognizes their special status +automatically. They are most effective in the case of +associative-commutative operators. (Associativity by itself is not +permutative.) When dealing with an AC-operator~$f$, keep the +following points in mind: \begin{itemize}\index{associative-commutative operators} -\item The associative law must always be oriented from left to right, namely - $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if used with - commutativity, leads to looping! Future versions of Isabelle may remove - this restriction. + +\item The associative law must always be oriented from left to right, + namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if + used with commutativity, leads to looping in conjunction with the + standard term order. \item To complete your set of rewrite rules, you must add not just associativity~(A) and commutativity~(C) but also a derived rule, {\bf @@ -699,17 +950,18 @@ such as boolean rings. \subsection{Example: sums of natural numbers} -This example is set in \HOL\ (see \texttt{HOL/ex/NatSum}). Theory -\thydx{Arith} contains natural numbers arithmetic. Its associated -simpset contains many arithmetic laws including distributivity -of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the -A, C and LC laws for~$+$ on type \texttt{nat}. Let us prove the -theorem + +This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}). +Theory \thydx{Arith} contains natural numbers arithmetic. Its +associated simpset contains many arithmetic laws including +distributivity of~$\times$ over~$+$, while {\tt add_ac} is a list +consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let +us prove the theorem \[ \sum@{i=1}^n i = n\times(n+1)/2. \] % A functional~{\tt sum} represents the summation operator under the interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We -extend {\tt Arith} using a theory file: +extend {\tt Arith} as follows: \begin{ttbox} NatSum = Arith + consts sum :: [nat=>nat, nat] => nat @@ -800,18 +1052,115 @@ \index{rewrite rules!permutative|)} +\section{*Coding simplification procedures} +\begin{ttbox} +mk_simproc: string -> cterm list -> + (Sign.sg -> thm list -> term -> thm option) -> simproc +\end{ttbox} + +\begin{ttdescription} +\item[\ttindexbold{mk_simproc}~$name$~$lhss$~$proc$] makes $proc$ a + simplification procedure for left-hand side patterns $lhss$. The + name just serves as a comment. The function $proc$ may be invoked + by the simplifier for redex positions matched by one of $lhss$ as + described below. +\end{ttdescription} + +Simplification procedures are applied in a two-stage process as +follows: The simplifier tries to match the current redex position +against any one of the $lhs$ patterns of any simplification procedure. +If this succeeds, it invokes the corresponding {\ML} function, passing +with the current signature, local assumptions and the (potential) +redex. The result may be either \texttt{None} (indicating failure) or +\texttt{Some~$thm$}. + +Any successful result is supposed to be a (possibly conditional) +rewrite rule $t \equiv u$ that is applicable to the current redex. +The rule will be applied just as any ordinary rewrite rule. It is +expected to be already in \emph{internal form}, though, bypassing the +automatic preprocessing of object-level equivalences. + +\medskip + +As an example of how to write your own simplification procedures, +consider eta-expansion of pair abstraction (see also +\texttt{HOL/Modelcheck/MCSyn} where this is used to provide external +model checker syntax). + +The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an +operator \texttt{split} together with some concrete syntax supporting +$\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a +tactic that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of +some pair type) to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule +is: +\begin{ttbox} +pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) +\end{ttbox} +Unfortunately, term rewriting using this rule directly would not +terminate! We now use the simplification procedure mechanism in order +to stop the simplifier from applying this rule over and over again, +making it rewrite only actual abstractions. The simplification +procedure \texttt{pair_eta_expand_proc} is defined as follows: +\begin{ttbox} +local + val lhss = + [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; + val rew = mk_meta_eq pair_eta_expand; \medskip + fun proc _ _ (Abs _) = Some rew + | proc _ _ _ = None; +in + val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; +end; +\end{ttbox} +This is an example of using \texttt{pair_eta_expand_proc}: +\begin{ttbox} +{\out 1. P (\%p::'a * 'a. fst p + snd p + z)} +by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1); +{\out 1. P (\%(x::'a,y::'a). x + y + z)} +\end{ttbox} + +\medskip + +In the above example the simplification procedure just did fine +grained control over rule application, beyond higher-order pattern +matching. Usually, procedures would do some more work, in particular +prove particular theorems depending on the current redex. + +For example, simplification procedures \ttindexbold{nat_cancel} of +\texttt{HOL/Arith} cancel common summands and constant factors out of +several relations of sums over natural numbers. + +Consider the following goal, which after cancelling $a$ on both sides +contains a factor of $2$. Simplifying with the simpset of +\texttt{Arith.thy} will do the cancellation automatically: +\begin{ttbox} +{\out 1. x + a + x < y + y + 2 + a + a + a + a + a} +by (Simp_tac 1); +{\out 1. x < Suc (a + (a + y))} +\end{ttbox} + +\medskip + +The {\ML} sources for these simplification procedures consist of a +generic part (files \texttt{cancel_sums.ML} and +\texttt{cancel_factor.ML} in \texttt{Provers/Arith}), and a +\texttt{HOL} specific part in \texttt{HOL/arith_data.ML}. + + \section{*Setting up the simplifier}\label{sec:setting-up-simp} \index{simplification!setting up} Setting up the simplifier for new logics is complicated. This section -describes how the simplifier is installed for intuitionistic first-order -logic; the code is largely taken from {\tt FOL/simpdata.ML}. +describes how the simplifier is installed for intuitionistic +first-order logic; the code is largely taken from {\tt + FOL/simpdata.ML} of the Isabelle sources. The simplifier and the case splitting tactic, which reside on separate -files, are not part of Pure Isabelle. They must be loaded explicitly: +files, are not part of Pure Isabelle. They must be loaded explicitly +by the object-logic as follows: \begin{ttbox} -use "../Provers/simplifier.ML"; -use "../Provers/splitter.ML"; +use "$ISABELLE_HOME/src/Provers/simplifier.ML"; +use "$ISABELLE_HOME/src/Provers/splitter.ML"; \end{ttbox} Simplification works by reducing various object-equalities to @@ -824,11 +1173,12 @@ \end{ttbox} Of course, you should only assert such rules if they are true for your particular logic. In Constructive Type Theory, equality is a ternary -relation of the form $a=b\in A$; the type~$A$ determines the meaning of the -equality essentially as a partial equivalence relation. The present -simplifier cannot be used. Rewriting in {\tt CTT} uses another simplifier, -which resides in the file {\tt typedsimp.ML} and is not documented. Even -this does not work for later variants of Constructive Type Theory that use +relation of the form $a=b\in A$; the type~$A$ determines the meaning +of the equality essentially as a partial equivalence relation. The +present simplifier cannot be used. Rewriting in {\tt CTT} uses +another simplifier, which resides in the file {\tt + Provers/typedsimp.ML} and is not documented. Even this does not +work for later variants of Constructive Type Theory that use intensional equality~\cite{nordstrom90}. @@ -842,13 +1192,13 @@ (writeln s; prove_goal IFOL.thy s (fn prems => [ (cut_facts_tac prems 1), - (Int.fast_tac 1) ])); + (IntPr.fast_tac 1) ])); \end{ttbox} The following rewrite rules about conjunction are a selection of those proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the standard simpset. \begin{ttbox} -val conj_rews = map int_prove_fun +val conj_simps = map int_prove_fun ["P & True <-> P", "True & P <-> P", "P & False <-> False", "False & P <-> False", "P & P <-> P", @@ -859,7 +1209,7 @@ blowup, they will not be included in the standard simpset. Instead they are merely bound to an \ML{} identifier, for user reference. \begin{ttbox} -val distrib_rews = map int_prove_fun +val distrib_simps = map int_prove_fun ["P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P", "(P | Q --> R) <-> (P --> R) & (Q --> R)"]; @@ -868,7 +1218,9 @@ \subsection{Functions for preprocessing the rewrite rules} \label{sec:setmksimps} -% +\begin{ttbox}\indexbold{*setmksimps} +setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4} +\end{ttbox} The next step is to define the function for preprocessing rewrite rules. This will be installed by calling {\tt setmksimps} below. Preprocessing occurs whenever rewrite rules are added, whether by user command or @@ -942,25 +1294,34 @@ \subsection{Making the initial simpset} -It is time to assemble these items. We open module {\tt Simplifier} to -gain access to its components. We define the infix operator -\ttindexbold{addcongs} to insert congruence rules; given a list of theorems, -it converts their conclusions into meta-equalities and passes them to -\ttindex{addeqcongs}. + +It is time to assemble these items. We open module {\tt Simplifier} +to gain direct access to its components. We define the infix operator +\ttindex{addcongs} to insert congruence rules; given a list of +theorems, it converts their conclusions into meta-equalities and +passes them to \ttindex{addeqcongs}. \begin{ttbox} open Simplifier; \ttbreak -infix addcongs; +infix 4 addcongs; fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection,iff_reflection]); \end{ttbox} -The list {\tt IFOL_rews} contains the default rewrite rules for first-order -logic. The first of these is the reflexive law expressed as the -equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is clearly useless. +Furthermore, we define the infix operator \ttindex{addsplits} +providing a convenient interface for adding split tactics. \begin{ttbox} -val IFOL_rews = - [refl RS P_iff_T] \at conj_rews \at disj_rews \at not_rews \at - imp_rews \at iff_rews \at quant_rews; +infix 4 addsplits; +fun ss addsplits splits = ss addloop (split_tac splits); +\end{ttbox} + +The list {\tt IFOL_simps} contains the default rewrite rules for +first-order logic. The first of these is the reflexive law expressed +as the equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is +clearly useless. +\begin{ttbox} +val IFOL_simps = + [refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at + imp_simps \at iff_simps \at quant_simps; \end{ttbox} The list {\tt triv_rls} contains trivial theorems for the solver. Any subgoal that is simplified to one of these will be removed. @@ -969,28 +1330,35 @@ val triv_rls = [TrueI,refl,iff_refl,notFalseI]; \end{ttbox} % -The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}. -It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt - mk_meta_eq}. It solves simplified subgoals using {\tt triv_rls} and -assumptions, and by detecting contradictions. -It uses \ttindex{asm_simp_tac} to tackle subgoals of -conditional rewrites. It takes {\tt IFOL_rews} as rewrite rules. -Other simpsets built from {\tt IFOL_ss} will inherit these items. -In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite -rules such as $\neg\neg P\bimp P$. +The basic simpset for intuitionistic \FOL{} is +\ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt + gen_all}, {\tt atomize} and {\tt mk_meta_eq}. It solves simplified +subgoals using {\tt triv_rls} and assumptions, and by detecting +contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of +conditional rewrites. + +Other simpsets built from {\tt FOL_basic_ss} will inherit these items. +In particular, \ttindexbold{IFOL_ss}, which introduces {\tt + IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later +extend {\tt IFOL_ss} with classical rewrite rules such as $\neg\neg +P\bimp P$. \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler} \index{*addsimps}\index{*addcongs} \begin{ttbox} -fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls \at prems), +fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls {\at} prems), atac, etac FalseE]; -fun safe_solver prems = FIRST'[match_tac (triv_rls \at prems), + +fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems), eq_assume_tac, ematch_tac [FalseE]]; -val IFOL_ss = empty_ss setsubgoaler asm_simp_tac - setSSolver safe_solver - setSolver unsafe_solver - setmksimps (map mk_meta_eq o atomize o gen_all) - addsimps IFOL_simps - addcongs [imp_cong]; + +val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac + addsimprocs [defALL_regroup,defEX_regroup] + setSSolver safe_solver + setSolver unsafe_solver + setmksimps (map mk_meta_eq o atomize o gen_all); + +val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} int_ex_simps {\at} int_all_simps) + addcongs [imp_cong]; \end{ttbox} This simpset takes {\tt imp_cong} as a congruence rule in order to use contextual information to simplify the conclusions of implications: @@ -1027,14 +1395,33 @@ \langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) \] Case splits should be allowed only when necessary; they are expensive -and hard to control. Here is a typical example of use, where {\tt - expand_if} is the first rule above: +and hard to control. Here is an example of use, where {\tt expand_if} +is the first rule above: \begin{ttbox} -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); +by (simp_tac (simpset() addloop (split_tac [expand_if])) 1); +\end{ttbox} +Users would usually prefer the following shortcut using +\ttindex{addsplits}: +\begin{ttbox} +by (simp_tac (simpset() addsplits [expand_if]) 1); \end{ttbox} +\subsection{Theory data for implicit simpsets} +\begin{ttbox}\indexbold{*simpset_thy_data} +simpset_thy_data: string * (object * (object -> object) * + (object * object -> object) * (Sign.sg -> object -> unit)) +\end{ttbox} + +Theory data for implicit simpsets has to be set up explicitly. The +simplifier already provides an appropriate data kind definition +record. This has to be installed into the base theory of any new +object-logic as \ttindexbold{thy_data} within the \texttt{ML} section. + +This is done at the end of \texttt{IFOL.thy} as follows: +\begin{ttbox} +ML val thy_data = [Simplifier.simpset_thy_data]; +\end{ttbox} + \index{simplification|)} - -