summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Ref/simp.tex

author | obua |

Fri, 16 Sep 2005 21:02:15 +0200 | |

changeset 17440 | df77edc4f5d0 |

parent 11181 | d04f57b91166 |

permissions | -rw-r--r-- |

fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions

%%%THIS DOCUMENTS THE OBSOLETE SIMPLIFIER!!!! \chapter{Simplification} \label{simp-chap} \index{simplification|(} Object-level rewriting is not primitive in Isabelle. For efficiency, perhaps it ought to be. On the other hand, it is difficult to conceive of a general mechanism that could accommodate the diversity of rewriting found in different logics. Hence rewriting in Isabelle works via resolution, using unknowns as place-holders for simplified terms. This chapter describes a generic simplification package, the functor~\ttindex{SimpFun}, which expects the basic laws of equational logic and returns a suite of simplification tactics. The code lives in \verb$Provers/simp.ML$. This rewriting package is not as general as one might hope (using it for {\tt HOL} is not quite as convenient as it could be; rewriting modulo equations is not supported~\ldots) but works well for many logics. It performs conditional and unconditional rewriting and handles multiple reduction relations and local assumptions. It also has a facility for automatic case splits by expanding conditionals like {\it if-then-else\/} during rewriting. For many of Isabelle's logics ({\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt HOL}) the simplifier has been set up already. Hence we start by describing the functions provided by the simplifier --- those functions exported by \ttindex{SimpFun} through its result signature \ttindex{SIMP} shown in Fig.\ts\ref{SIMP}. \section{Simplification sets} \index{simplification sets} The simplification tactics are controlled by {\bf simpsets}, which consist of three things: \begin{enumerate} \item {\bf Rewrite rules}, which are theorems like $\Var{m} + succ(\Var{n}) = succ(\Var{m} + \Var{n})$. {\bf Conditional} rewrites such as $m<n \Imp m/n = 0$ are permitted. \index{rewrite rules} \item {\bf Congruence rules}, which typically have the form \index{congruence rules} \[ \List{\Var{x@1} = \Var{y@1}; \ldots; \Var{x@n} = \Var{y@n}} \Imp f(\Var{x@1},\ldots,\Var{x@n}) = f(\Var{y@1},\ldots,\Var{y@n}). \] \item The {\bf auto-tactic}, which attempts to solve the simplified subgoal, say by recognizing it as a tautology. \end{enumerate} \subsection{Congruence rules} Congruence rules enable the rewriter to simplify subterms. Without a congruence rule for the function~$g$, no argument of~$g$ can be rewritten. Congruence rules can be generalized in the following ways: {\bf Additional assumptions} are allowed: \[ \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}) \] This rule assumes $Q@1$, and any rewrite rules it contains, while simplifying~$P@2$. Such `local' assumptions are effective for rewriting formulae such as $x=0\imp y+x=y$. {\bf Additional quantifiers} are allowed, typically for binding operators: \[ \List{\Forall z. \Var{P}(z) \bimp \Var{Q}(z)} \Imp \forall x.\Var{P}(x) \bimp \forall x.\Var{Q}(x) \] {\bf Different equalities} can be mixed. The following example enables the transition from formula rewriting to term rewriting: \[ \List{\Var{x@1}=\Var{y@1};\Var{x@2}=\Var{y@2}} \Imp (\Var{x@1}=\Var{x@2}) \bimp (\Var{y@1}=\Var{y@2}) \] \begin{warn} It is not necessary to assert a separate congruence rule for each constant, provided your logic contains suitable substitution rules. The function {\tt mk_congs} derives congruence rules from substitution rules~\S\ref{simp-tactics}. \end{warn} \begin{figure} \indexbold{*SIMP} \begin{ttbox} infix 4 addrews addcongs delrews delcongs setauto; signature SIMP = sig type simpset val empty_ss : simpset val addcongs : simpset * thm list -> simpset val addrews : simpset * thm list -> simpset val delcongs : simpset * thm list -> simpset val delrews : simpset * thm list -> simpset val print_ss : simpset -> unit val setauto : simpset * (int -> tactic) -> simpset val ASM_SIMP_CASE_TAC : simpset -> int -> tactic val ASM_SIMP_TAC : simpset -> int -> tactic val CASE_TAC : simpset -> int -> tactic val SIMP_CASE2_TAC : simpset -> int -> tactic val SIMP_THM : simpset -> thm -> thm val SIMP_TAC : simpset -> int -> tactic val SIMP_CASE_TAC : simpset -> int -> tactic val mk_congs : theory -> string list -> thm list val mk_typed_congs : theory -> (string*string) list -> thm list val tracing : bool ref end; \end{ttbox} \caption{The signature {\tt SIMP}} \label{SIMP} \end{figure} \subsection{The abstract type {\tt simpset}}\label{simp-simpsets} Simpsets are values of the abstract type \ttindexbold{simpset}. They are manipulated by the following functions: \index{simplification sets|bold} \begin{ttdescription} \item[\ttindexbold{empty_ss}] is the empty simpset. It has no congruence or rewrite rules and its auto-tactic always fails. \item[$ss$ \ttindexbold{addcongs} $thms$] is the simpset~$ss$ plus the congruence rules~$thms$. \item[$ss$ \ttindexbold{delcongs} $thms$] is the simpset~$ss$ minus the congruence rules~$thms$. \item[$ss$ \ttindexbold{addrews} $thms$] is the simpset~$ss$ plus the rewrite rules~$thms$. \item[$ss$ \ttindexbold{delrews} $thms$] is the simpset~$ss$ minus the rewrite rules~$thms$. \item[$ss$ \ttindexbold{setauto} $tacf$] is the simpset~$ss$ with $tacf$ for its auto-tactic. \item[\ttindexbold{print_ss} $ss$] prints all the congruence and rewrite rules in the simpset~$ss$. \end{ttdescription} Adding a rule to a simpset already containing it, or deleting one from a simpset not containing it, generates a warning message. In principle, any theorem can be used as a rewrite rule. Before adding a theorem to a simpset, {\tt addrews} preprocesses the theorem to extract the maximum amount of rewriting from it. Thus it need not have the form $s=t$. In {\tt FOL} for example, an atomic formula $P$ is transformed into the rewrite rule $P \bimp True$. This preprocessing is not fixed but logic dependent. The existing logics like {\tt FOL} are fairly clever in this respect. For a more precise description see {\tt mk_rew_rules} in \S\ref{SimpFun-input}. The auto-tactic is applied after simplification to solve a goal. This may be the overall goal or some subgoal that arose during conditional rewriting. Calling ${\tt auto_tac}~i$ must either solve exactly subgoal~$i$ or fail. If it succeeds without reducing the number of subgoals by one, havoc and strange exceptions may result. A typical auto-tactic is {\tt ares_tac [TrueI]}, which attempts proof by assumption and resolution with the theorem $True$. In explicitly typed logics, the auto-tactic can be used to solve simple type checking obligations. Some applications demand a sophisticated auto-tactic such as {\tt fast_tac}, but this could make simplification slow. \begin{warn} Rewriting never instantiates unknowns in subgoals. (It uses \ttindex{match_tac} rather than \ttindex{resolve_tac}.) However, the auto-tactic is permitted to instantiate unknowns. \end{warn} \section{The simplification tactics} \label{simp-tactics} \index{simplification!tactics|bold} \index{tactics!simplification|bold} The actual simplification work is performed by the following tactics. The rewriting strategy is strictly bottom up. Conditions in conditional rewrite rules are solved recursively before the rewrite rule is applied. There are two basic simplification tactics: \begin{ttdescription} \item[\ttindexbold{SIMP_TAC} $ss$ $i$] simplifies subgoal~$i$ using the rules in~$ss$. It may solve the subgoal completely if it has become trivial, using the auto-tactic (\S\ref{simp-simpsets}). \item[\ttindexbold{ASM_SIMP_TAC}] is like \verb$SIMP_TAC$, but also uses assumptions as additional rewrite rules. \end{ttdescription} Many logics have conditional operators like {\it if-then-else}. If the simplifier has been set up with such case splits (see~\ttindex{case_splits} in \S\ref{SimpFun-input}), there are tactics which automatically alternate between simplification and case splitting: \begin{ttdescription} \item[\ttindexbold{SIMP_CASE_TAC}] is like {\tt SIMP_TAC} but also performs automatic case splits. More precisely, after each simplification phase the tactic tries to apply a theorem in \ttindex{case_splits}. If this succeeds, the tactic calls itself recursively on the result. \item[\ttindexbold{ASM_SIMP_CASE_TAC}] is like {\tt SIMP_CASE_TAC}, but also uses assumptions for rewriting. \item[\ttindexbold{SIMP_CASE2_TAC}] is like {\tt SIMP_CASE_TAC}, but also tries to solve the pre-conditions of conditional simplification rules by repeated case splits. \item[\ttindexbold{CASE_TAC}] tries to break up a goal using a rule in \ttindex{case_splits}. \item[\ttindexbold{SIMP_THM}] simplifies a theorem using assumptions and case splitting. \end{ttdescription} Finally there are two useful functions for generating congruence rules for constants and free variables: \begin{ttdescription} \item[\ttindexbold{mk_congs} $thy$ $cs$] computes a list of congruence rules, one for each constant in $cs$. Remember that the name of an infix constant \verb$+$ is \verb$op +$. \item[\ttindexbold{mk_typed_congs}] computes congruence rules for explicitly typed free variables and constants. Its second argument is a list of name and type pairs. Names can be either free variables like {\tt P}, or constants like \verb$op =$. For example in {\tt FOL}, the pair \verb$("f","'a => 'a")$ generates the rule \verb$?x = ?y ==> f(?x) = f(?y)$. Such congruence rules are necessary for goals with free variables whose arguments need to be rewritten. \end{ttdescription} Both functions work correctly only if {\tt SimpFun} has been supplied with the necessary substitution rules. The details are discussed in \S\ref{SimpFun-input} under {\tt subst_thms}. \begin{warn} Using the simplifier effectively may take a bit of experimentation. In particular it may often happen that simplification stops short of what you expected or runs forever. To diagnose these problems, the simplifier can be traced. The reference variable \ttindexbold{tracing} controls the output of tracing information. \index{tracing!of simplification} \end{warn} \section{Example: using the simplifier} \index{simplification!example} Assume we are working within {\tt FOL} and that \begin{ttdescription} \item[Nat.thy] is a theory including the constants $0$, $Suc$ and $+$, \item[add_0] is the rewrite rule $0+n = n$, \item[add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$, \item[induct] is the induction rule $\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$. \item[FOL_ss] is a basic simpset for {\tt FOL}. \end{ttdescription} We generate congruence rules for $Suc$ and for the infix operator~$+$: \begin{ttbox} val nat_congs = mk_congs Nat.thy ["Suc", "op +"]; prths nat_congs; {\out ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)} {\out [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb} \end{ttbox} We create a simpset for natural numbers by extending~{\tt FOL_ss}: \begin{ttbox} val add_ss = FOL_ss addcongs nat_congs addrews [add_0, add_Suc]; \end{ttbox} Proofs by induction typically involve simplification:\footnote {These examples reside on the file {\tt FOL/ex/nat.ML}.} \begin{ttbox} goal Nat.thy "m+0 = m"; {\out Level 0} {\out m + 0 = m} {\out 1. m + 0 = m} \ttbreak by (res_inst_tac [("n","m")] induct 1); {\out Level 1} {\out m + 0 = m} {\out 1. 0 + 0 = 0} {\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} \end{ttbox} Simplification solves the first subgoal: \begin{ttbox} by (SIMP_TAC add_ss 1); {\out Level 2} {\out m + 0 = m} {\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} \end{ttbox} The remaining subgoal requires \ttindex{ASM_SIMP_TAC} in order to use the induction hypothesis as a rewrite rule: \begin{ttbox} by (ASM_SIMP_TAC add_ss 1); {\out Level 3} {\out m + 0 = m} {\out No subgoals!} \end{ttbox} The next proof is similar. \begin{ttbox} goal Nat.thy "m+Suc(n) = Suc(m+n)"; {\out Level 0} {\out m + Suc(n) = Suc(m + n)} {\out 1. m + Suc(n) = Suc(m + n)} \ttbreak by (res_inst_tac [("n","m")] induct 1); {\out Level 1} {\out m + Suc(n) = Suc(m + n)} {\out 1. 0 + Suc(n) = Suc(0 + n)} {\out 2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)} \end{ttbox} Using the tactical \ttindex{ALLGOALS}, a single command simplifies all the subgoals: \begin{ttbox} by (ALLGOALS (ASM_SIMP_TAC add_ss)); {\out Level 2} {\out m + Suc(n) = Suc(m + n)} {\out No subgoals!} \end{ttbox} Some goals contain free function variables. The simplifier must have congruence rules for those function variables, or it will be unable to simplify their arguments: \begin{ttbox} val f_congs = mk_typed_congs Nat.thy [("f","nat => nat")]; val f_ss = add_ss addcongs f_congs; prths f_congs; {\out ?Xa = ?Ya ==> f(?Xa) = f(?Ya)} \end{ttbox} Here is a conjecture to be proved for an arbitrary function~$f$ satisfying the law $f(Suc(n)) = Suc(f(n))$: \begin{ttbox} val [prem] = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; {\out Level 0} {\out f(i + j) = i + f(j)} {\out 1. f(i + j) = i + f(j)} \ttbreak by (res_inst_tac [("n","i")] induct 1); {\out Level 1} {\out f(i + j) = i + f(j)} {\out 1. f(0 + j) = 0 + f(j)} {\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} \end{ttbox} We simplify each subgoal in turn. The first one is trivial: \begin{ttbox} by (SIMP_TAC f_ss 1); {\out Level 2} {\out f(i + j) = i + f(j)} {\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, shown below, so we add it to {\tt f_ss}: \begin{ttbox} prth prem; {\out f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))]} by (ASM_SIMP_TAC (f_ss addrews [prem]) 1); {\out Level 3} {\out f(i + j) = i + f(j)} {\out No subgoals!} \end{ttbox} \section{Setting up the simplifier} \label{SimpFun-input} \index{simplification!setting up|bold} To set up a simplifier for a new logic, the \ML\ functor \ttindex{SimpFun} needs to be supplied with theorems to justify rewriting. A rewrite relation must be reflexive and transitive; symmetry is not necessary. Hence the package is also applicable to non-symmetric relations such as occur in operational semantics. In the sequel, $\gg$ denotes some {\bf reduction relation}: a binary relation to be used for rewriting. Several reduction relations can be used at once. In {\tt FOL}, both $=$ (on terms) and $\bimp$ (on formulae) can be used for rewriting. The argument to {\tt SimpFun} is a structure with signature \ttindexbold{SIMP_DATA}: \begin{ttbox} signature SIMP_DATA = sig val case_splits : (thm * string) list val dest_red : term -> term * term * term val mk_rew_rules : thm -> thm list val norm_thms : (thm*thm) list val red1 : thm val red2 : thm val refl_thms : thm list val subst_thms : thm list val trans_thms : thm list end; \end{ttbox} The components of {\tt SIMP_DATA} need to be instantiated as follows. Many of these components are lists, and can be empty. \begin{ttdescription} \item[\ttindexbold{refl_thms}] supplies reflexivity theorems of the form $\Var{x} \gg \Var{x}$. They must not have additional premises as, for example, $\Var{x}\in\Var{A} \Imp \Var{x} = \Var{x}\in\Var{A}$ in type theory. \item[\ttindexbold{trans_thms}] supplies transitivity theorems of the form $\List{\Var{x}\gg\Var{y}; \Var{y}\gg\Var{z}} \Imp {\Var{x}\gg\Var{z}}$. \item[\ttindexbold{red1}] is a theorem of the form $\List{\Var{P}\gg\Var{Q}; \Var{P}} \Imp \Var{Q}$, where $\gg$ is a relation between formulae, such as $\bimp$ in {\tt FOL}. \item[\ttindexbold{red2}] is a theorem of the form $\List{\Var{P}\gg\Var{Q}; \Var{Q}} \Imp \Var{P}$, where $\gg$ is a relation between formulae, such as $\bimp$ in {\tt FOL}. \item[\ttindexbold{mk_rew_rules}] is a function that extracts rewrite rules from theorems. A rewrite rule is a theorem of the form $\List{\ldots}\Imp s \gg t$. In its simplest form, {\tt mk_rew_rules} maps a theorem $t$ to the singleton list $[t]$. More sophisticated versions may do things like \[ \begin{array}{l@{}r@{\quad\mapsto\quad}l} \mbox{create formula rewrites:}& P & [P \bimp True] \\[.5ex] \mbox{remove negations:}& \neg P & [P \bimp False] \\[.5ex] \mbox{create conditional rewrites:}& P\imp s\gg t & [P\Imp s\gg t] \\[.5ex] \mbox{break up conjunctions:}& (s@1 \gg@1 t@1) \conj (s@2 \gg@2 t@2) & [s@1 \gg@1 t@1, s@2 \gg@2 t@2] \end{array} \] The more theorems are turned into rewrite rules, the better. The function is used in two places: \begin{itemize} \item $ss$~\ttindex{addrews}~$thms$ applies {\tt mk_rew_rules} to each element of $thms$ before adding it to $ss$. \item simplification with assumptions (as in \ttindex{ASM_SIMP_TAC}) uses {\tt mk_rew_rules} to turn assumptions into rewrite rules. \end{itemize} \item[\ttindexbold{case_splits}] supplies expansion rules for case splits. The simplifier is designed for rules roughly of the kind \[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x})) \conj (\neg\Var{Q} \imp \Var{P}(\Var{y})) \] but is insensitive to the form of the right-hand side. Other examples include product types, where $split :: (\alpha\To\beta\To\gamma)\To\alpha*\beta\To\gamma$: \[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = {<}a,b{>} \imp \Var{P}(\Var{f}(a,b))) \] Each theorem in the list is paired with the name of the constant being eliminated, {\tt"if"} and {\tt"split"} in the examples above. \item[\ttindexbold{norm_thms}] supports an optimization. It should be a list of pairs of rules of the form $\Var{x} \gg norm(\Var{x})$ and $norm(\Var{x}) \gg \Var{x}$. These introduce and eliminate {\tt norm}, an arbitrary function that should be used nowhere else. This function serves to tag subterms that are in normal form. Such rules can speed up rewriting significantly! \item[\ttindexbold{subst_thms}] supplies substitution rules of the form \[ \List{\Var{x} \gg \Var{y}; \Var{P}(\Var{x})} \Imp \Var{P}(\Var{y}) \] They are used to derive congruence rules via \ttindex{mk_congs} and \ttindex{mk_typed_congs}. If $f :: [\tau@1,\cdots,\tau@n]\To\tau$ is a constant or free variable, the computation of a congruence rule \[\List{\Var{x@1} \gg@1 \Var{y@1}; \ldots; \Var{x@n} \gg@n \Var{y@n}} \Imp f(\Var{x@1},\ldots,\Var{x@n}) \gg f(\Var{y@1},\ldots,\Var{y@n}) \] requires a reflexivity theorem for some reduction ${\gg} :: \alpha\To\alpha\To\sigma$ such that $\tau$ is an instance of $\alpha$. If a suitable reflexivity law is missing, no congruence rule for $f$ can be generated. Otherwise an $n$-ary congruence rule of the form shown above is derived, subject to the availability of suitable substitution laws for each argument position. A substitution law is suitable for argument $i$ if it uses a reduction ${\gg@i} :: \alpha@i\To\alpha@i\To\sigma@i$ such that $\tau@i$ is an instance of $\alpha@i$. If a suitable substitution law for argument $i$ is missing, the $i^{th}$ premise of the above congruence rule cannot be generated and hence argument $i$ cannot be rewritten. In the worst case, if there are no suitable substitution laws at all, the derived congruence simply degenerates into a reflexivity law. \item[\ttindexbold{dest_red}] takes reductions apart. Given a term $t$ representing the judgement \mbox{$a \gg b$}, \verb$dest_red$~$t$ should return a triple $(c,ta,tb)$ where $ta$ and $tb$ represent $a$ and $b$, and $c$ is a term of the form \verb$Const(_,_)$, the reduction constant $\gg$. Suppose the logic has a coercion function like $Trueprop::o\To prop$, as do {\tt FOL} and~{\tt HOL}\@. If $\gg$ is a binary operator (not necessarily infix), the following definition does the job: \begin{verbatim} fun dest_red( _ $ (c $ ta $ tb) ) = (c,ta,tb); \end{verbatim} The wildcard pattern {\tt_} matches the coercion function. \end{ttdescription} \section{A sample instantiation} Here is the instantiation of {\tt SIMP_DATA} for FOL. The code for {\tt mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}. \begin{ttbox} structure FOL_SimpData : SIMP_DATA = struct val refl_thms = [ \(\Var{x}=\Var{x}\), \(\Var{P}\bimp\Var{P}\) ] val trans_thms = [ \(\List{\Var{x}=\Var{y};\Var{y}=\Var{z}}\Imp\Var{x}=\Var{z}\), \(\List{\Var{P}\bimp\Var{Q};\Var{Q}\bimp\Var{R}}\Imp\Var{P}\bimp\Var{R}\) ] val red1 = \(\List{\Var{P}\bimp\Var{Q}; \Var{P}} \Imp \Var{Q}\) val red2 = \(\List{\Var{P}\bimp\Var{Q}; \Var{Q}} \Imp \Var{P}\) val mk_rew_rules = ... val case_splits = [ \(\Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp\) \((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))\) ] val norm_thms = [ (\(\Var{x}=norm(\Var{x})\),\(norm(\Var{x})=\Var{x}\)), (\(\Var{P}\bimp{}NORM(\Var{P}\)), \(NORM(\Var{P})\bimp\Var{P}\)) ] val subst_thms = [ \(\List{\Var{x}=\Var{y}; \Var{P}(\Var{x})}\Imp\Var{P}(\Var{y})\) ] val dest_red = fn (_ $ (opn $ lhs $ rhs)) => (opn,lhs,rhs) end; \end{ttbox} \index{simplification|)}