104

1 
%%%THIS DOCUMENTS THE OBSOLETE SIMPLIFIER!!!!


2 
\chapter{Simplification} \label{simpchap}


3 
\index{simplification(}


4 
Objectlevel rewriting is not primitive in Isabelle. For efficiency,


5 
perhaps it ought to be. On the other hand, it is difficult to conceive of


6 
a general mechanism that could accommodate the diversity of rewriting found


7 
in different logics. Hence rewriting in Isabelle works via resolution,


8 
using unknowns as placeholders for simplified terms. This chapter


9 
describes a generic simplification package, the functor~\ttindex{SimpFun},


10 
which expects the basic laws of equational logic and returns a suite of


11 
simplification tactics. The code lives in


12 
\verb$Provers/simp.ML$.


13 


14 
This rewriting package is not as general as one might hope (using it for {\tt


15 
HOL} is not quite as convenient as it could be; rewriting modulo equations is


16 
not supported~\ldots) but works well for many logics. It performs


17 
conditional and unconditional rewriting and handles multiple reduction


18 
relations and local assumptions. It also has a facility for automatic case


19 
splits by expanding conditionals like {\it ifthenelse\/} during rewriting.


20 


21 
For many of Isabelle's logics ({\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt HOL})


22 
the simplifier has been set up already. Hence we start by describing the


23 
functions provided by the simplifier  those functions exported by


24 
\ttindex{SimpFun} through its result signature \ttindex{SIMP} shown in

286

25 
Fig.\ts\ref{SIMP}.

104

26 


27 


28 
\section{Simplification sets}


29 
\index{simplification sets}


30 
The simplification tactics are controlled by {\bf simpsets}, which consist of


31 
three things:


32 
\begin{enumerate}


33 
\item {\bf Rewrite rules}, which are theorems like


34 
$\Var{m} + succ(\Var{n}) = succ(\Var{m} + \Var{n})$. {\bf Conditional}


35 
rewrites such as $m<n \Imp m/n = 0$ are permitted.


36 
\index{rewrite rules}


37 


38 
\item {\bf Congruence rules}, which typically have the form


39 
\index{congruence rules}


40 
\[ \List{\Var{x@1} = \Var{y@1}; \ldots; \Var{x@n} = \Var{y@n}} \Imp


41 
f(\Var{x@1},\ldots,\Var{x@n}) = f(\Var{y@1},\ldots,\Var{y@n}).


42 
\]


43 


44 
\item The {\bf autotactic}, which attempts to solve the simplified


45 
subgoal, say by recognizing it as a tautology.


46 
\end{enumerate}


47 


48 
\subsection{Congruence rules}


49 
Congruence rules enable the rewriter to simplify subterms. Without a


50 
congruence rule for the function~$g$, no argument of~$g$ can be rewritten.


51 
Congruence rules can be generalized in the following ways:


52 


53 
{\bf Additional assumptions} are allowed:


54 
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}


55 
\Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2})


56 
\]


57 
This rule assumes $Q@1$, and any rewrite rules it contains, while


58 
simplifying~$P@2$. Such ``local'' assumptions are effective for rewriting


59 
formulae such as $x=0\imp y+x=y$.


60 


61 
{\bf Additional quantifiers} are allowed, typically for binding operators:


62 
\[ \List{\Forall z. \Var{P}(z) \bimp \Var{Q}(z)} \Imp


63 
\forall x.\Var{P}(x) \bimp \forall x.\Var{Q}(x)


64 
\]


65 


66 
{\bf Different equalities} can be mixed. The following example


67 
enables the transition from formula rewriting to term rewriting:


68 
\[ \List{\Var{x@1}=\Var{y@1};\Var{x@2}=\Var{y@2}} \Imp


69 
(\Var{x@1}=\Var{x@2}) \bimp (\Var{y@1}=\Var{y@2})


70 
\]


71 
\begin{warn}


72 
It is not necessary to assert a separate congruence rule for each constant,


73 
provided your logic contains suitable substitution rules. The function {\tt


74 
mk_congs} derives congruence rules from substitution


75 
rules~\S\ref{simptactics}.


76 
\end{warn}


77 


78 


79 
\begin{figure}


80 
\indexbold{*SIMP}


81 
\begin{ttbox}


82 
infix 4 addrews addcongs delrews delcongs setauto;


83 
signature SIMP =


84 
sig


85 
type simpset


86 
val empty_ss : simpset


87 
val addcongs : simpset * thm list > simpset


88 
val addrews : simpset * thm list > simpset


89 
val delcongs : simpset * thm list > simpset


90 
val delrews : simpset * thm list > simpset


91 
val print_ss : simpset > unit


92 
val setauto : simpset * (int > tactic) > simpset


93 
val ASM_SIMP_CASE_TAC : simpset > int > tactic


94 
val ASM_SIMP_TAC : simpset > int > tactic


95 
val CASE_TAC : simpset > int > tactic


96 
val SIMP_CASE2_TAC : simpset > int > tactic


97 
val SIMP_THM : simpset > thm > thm


98 
val SIMP_TAC : simpset > int > tactic


99 
val SIMP_CASE_TAC : simpset > int > tactic


100 
val mk_congs : theory > string list > thm list


101 
val mk_typed_congs : theory > (string*string) list > thm list


102 
val tracing : bool ref


103 
end;


104 
\end{ttbox}


105 
\caption{The signature {\tt SIMP}} \label{SIMP}


106 
\end{figure}


107 


108 


109 
\subsection{The abstract type {\tt simpset}}\label{simpsimpsets}


110 
Simpsets are values of the abstract type \ttindexbold{simpset}. They are


111 
manipulated by the following functions:


112 
\index{simplification setsbold}


113 
\begin{description}


114 
\item[\ttindexbold{empty_ss}]


115 
is the empty simpset. It has no congruence or rewrite rules and its


116 
autotactic always fails.


117 


118 
\item[\tt $ss$ \ttindexbold{addcongs} $thms$]


119 
is the simpset~$ss$ plus the congruence rules~$thms$.


120 


121 
\item[\tt $ss$ \ttindexbold{delcongs} $thms$]


122 
is the simpset~$ss$ minus the congruence rules~$thms$.


123 


124 
\item[\tt $ss$ \ttindexbold{addrews} $thms$]


125 
is the simpset~$ss$ plus the rewrite rules~$thms$.


126 


127 
\item[\tt $ss$ \ttindexbold{delrews} $thms$]


128 
is the simpset~$ss$ minus the rewrite rules~$thms$.


129 


130 
\item[\tt $ss$ \ttindexbold{setauto} $tacf$]


131 
is the simpset~$ss$ with $tacf$ for its autotactic.


132 


133 
\item[\ttindexbold{print_ss} $ss$]


134 
prints all the congruence and rewrite rules in the simpset~$ss$.


135 
\end{description}


136 
Adding a rule to a simpset already containing it, or deleting one


137 
from a simpset not containing it, generates a warning message.


138 


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


141 
maximum amount of rewriting from it. Thus it need not have the form $s=t$.


142 
In {\tt FOL} for example, an atomic formula $P$ is transformed into the


143 
rewrite rule $P \bimp True$. This preprocessing is not fixed but logic


144 
dependent. The existing logics like {\tt FOL} are fairly clever in this


145 
respect. For a more precise description see {\tt mk_rew_rules} in


146 
\S\ref{SimpFuninput}.


147 


148 
The autotactic is applied after simplification to solve a goal. This may


149 
be the overall goal or some subgoal that arose during conditional


150 
rewriting. Calling ${\tt auto_tac}~i$ must either solve exactly


151 
subgoal~$i$ or fail. If it succeeds without reducing the number of


152 
subgoals by one, havoc and strange exceptions may result.


153 
A typical autotactic is {\tt ares_tac [TrueI]}, which attempts proof by


154 
assumption and resolution with the theorem $True$. In explicitly typed


155 
logics, the autotactic can be used to solve simple type checking


156 
obligations. Some applications demand a sophisticated autotactic such as


157 
{\tt fast_tac}, but this could make simplification slow.


158 


159 
\begin{warn}


160 
Rewriting never instantiates unknowns in subgoals. (It uses


161 
\ttindex{match_tac} rather than \ttindex{resolve_tac}.) However, the


162 
autotactic is permitted to instantiate unknowns.


163 
\end{warn}


164 


165 


166 
\section{The simplification tactics} \label{simptactics}


167 
\index{simplification!tacticsbold}


168 
\index{tactics!simplificationbold}


169 
The actual simplification work is performed by the following tactics. The


170 
rewriting strategy is strictly bottom up. Conditions in conditional rewrite


171 
rules are solved recursively before the rewrite rule is applied.


172 


173 
There are two basic simplification tactics:


174 
\begin{description}


175 
\item[\ttindexbold{SIMP_TAC} $ss$ $i$]


176 
simplifies subgoal~$i$ using the rules in~$ss$. It may solve the


177 
subgoal completely if it has become trivial, using the autotactic


178 
(\S\ref{simpsimpsets}).


179 


180 
\item[\ttindexbold{ASM_SIMP_TAC}]


181 
is like \verb$SIMP_TAC$, but also uses assumptions as additional


182 
rewrite rules.


183 
\end{description}


184 
Many logics have conditional operators like {\it ifthenelse}. If the


185 
simplifier has been set up with such case splits (see~\ttindex{case_splits}


186 
in \S\ref{SimpFuninput}), there are tactics which automatically alternate


187 
between simplification and case splitting:


188 
\begin{description}


189 
\item[\ttindexbold{SIMP_CASE_TAC}]


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


192 
theorem in \ttindex{case_splits}. If this succeeds, the tactic calls


193 
itself recursively on the result.


194 


195 
\item[\ttindexbold{ASM_SIMP_CASE_TAC}]


196 
is like {\tt SIMP_CASE_TAC}, but also uses assumptions for


197 
rewriting.


198 


199 
\item[\ttindexbold{SIMP_CASE2_TAC}]


200 
is like {\tt SIMP_CASE_TAC}, but also tries to solve the


201 
preconditions of conditional simplification rules by repeated case splits.


202 


203 
\item[\ttindexbold{CASE_TAC}]


204 
tries to break up a goal using a rule in


205 
\ttindex{case_splits}.


206 


207 
\item[\ttindexbold{SIMP_THM}]


208 
simplifies a theorem using assumptions and case splitting.


209 
\end{description}


210 
Finally there are two useful functions for generating congruence


211 
rules for constants and free variables:


212 
\begin{description}


213 
\item[\ttindexbold{mk_congs} $thy$ $cs$]


214 
computes a list of congruence rules, one for each constant in $cs$.


215 
Remember that the name of an infix constant


216 
\verb$+$ is \verb$op +$.


217 


218 
\item[\ttindexbold{mk_typed_congs}]


219 
computes congruence rules for explicitly typed free variables and


220 
constants. Its second argument is a list of name and type pairs. Names


221 
can be either free variables like {\tt P}, or constants like \verb$op =$.


222 
For example in {\tt FOL}, the pair


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


225 
arguments need to be rewritten.


226 
\end{description}


227 
Both functions work correctly only if {\tt SimpFun} has been supplied with the


228 
necessary substitution rules. The details are discussed in


229 
\S\ref{SimpFuninput} under {\tt subst_thms}.


230 
\begin{warn}


231 
Using the simplifier effectively may take a bit of experimentation. In


232 
particular it may often happen that simplification stops short of what you


233 
expected or runs forever. To diagnose these problems, the simplifier can be


234 
traced. The reference variable \ttindexbold{tracing} controls the output of


235 
tracing information.


236 
\index{tracing!of simplification}


237 
\end{warn}


238 


239 


240 
\section{Example: using the simplifier}


241 
\index{simplification!example}


242 
Assume we are working within {\tt FOL} and that


243 
\begin{description}


244 
\item[\tt Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,


245 
\item[\tt add_0] is the rewrite rule $0+n = n$,


246 
\item[\tt add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,


247 
\item[\tt induct] is the induction rule


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}.


250 
\end{description}


251 
We generate congruence rules for $Suc$ and for the infix operator~$+$:


252 
\begin{ttbox}


253 
val nat_congs = mk_congs Nat.thy ["Suc", "op +"];


254 
prths nat_congs;


255 
{\out ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)}


256 
{\out [ ?Xa = ?Ya; ?Xb = ?Yb ] ==> ?Xa + ?Xb = ?Ya + ?Yb}


257 
\end{ttbox}


258 
We create a simpset for natural numbers by extending~{\tt FOL_ss}:


259 
\begin{ttbox}


260 
val add_ss = FOL_ss addcongs nat_congs


261 
addrews [add_0, add_Suc];


262 
\end{ttbox}


263 
Proofs by induction typically involve simplification:\footnote


264 
{These examples reside on the file {\tt FOL/ex/nat.ML}.}


265 
\begin{ttbox}


266 
goal Nat.thy "m+0 = m";


267 
{\out Level 0}


268 
{\out m + 0 = m}


269 
{\out 1. m + 0 = m}


270 
\ttbreak


271 
by (res_inst_tac [("n","m")] induct 1);


272 
{\out Level 1}


273 
{\out m + 0 = m}


274 
{\out 1. 0 + 0 = 0}


275 
{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}


276 
\end{ttbox}


277 
Simplification solves the first subgoal:


278 
\begin{ttbox}


279 
by (SIMP_TAC add_ss 1);


280 
{\out Level 2}


281 
{\out m + 0 = m}


282 
{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}


283 
\end{ttbox}


284 
The remaining subgoal requires \ttindex{ASM_SIMP_TAC} in order to use the


285 
induction hypothesis as a rewrite rule:


286 
\begin{ttbox}


287 
by (ASM_SIMP_TAC add_ss 1);


288 
{\out Level 3}


289 
{\out m + 0 = m}


290 
{\out No subgoals!}


291 
\end{ttbox}


292 
The next proof is similar.


293 
\begin{ttbox}


294 
goal Nat.thy "m+Suc(n) = Suc(m+n)";


295 
{\out Level 0}


296 
{\out m + Suc(n) = Suc(m + n)}


297 
{\out 1. m + Suc(n) = Suc(m + n)}


298 
\ttbreak


299 
by (res_inst_tac [("n","m")] induct 1);


300 
{\out Level 1}


301 
{\out m + Suc(n) = Suc(m + n)}


302 
{\out 1. 0 + Suc(n) = Suc(0 + n)}


303 
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}


304 
\end{ttbox}


305 
Using the tactical \ttindex{ALLGOALS}, a single command simplifies all the


306 
subgoals:


307 
\begin{ttbox}


308 
by (ALLGOALS (ASM_SIMP_TAC add_ss));


309 
{\out Level 2}


310 
{\out m + Suc(n) = Suc(m + n)}


311 
{\out No subgoals!}


312 
\end{ttbox}


313 
Some goals contain free function variables. The simplifier must have


314 
congruence rules for those function variables, or it will be unable to


315 
simplify their arguments:


316 
\begin{ttbox}


317 
val f_congs = mk_typed_congs Nat.thy [("f","nat => nat")];


318 
val f_ss = add_ss addcongs f_congs;


319 
prths f_congs;


320 
{\out ?Xa = ?Ya ==> f(?Xa) = f(?Ya)}


321 
\end{ttbox}


322 
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying


323 
the law $f(Suc(n)) = Suc(f(n))$:


324 
\begin{ttbox}


325 
val [prem] = goal Nat.thy


326 
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";


327 
{\out Level 0}


328 
{\out f(i + j) = i + f(j)}


329 
{\out 1. f(i + j) = i + f(j)}


330 
\ttbreak


331 
by (res_inst_tac [("n","i")] induct 1);


332 
{\out Level 1}


333 
{\out f(i + j) = i + f(j)}


334 
{\out 1. f(0 + j) = 0 + f(j)}


335 
{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}


336 
\end{ttbox}


337 
We simplify each subgoal in turn. The first one is trivial:


338 
\begin{ttbox}


339 
by (SIMP_TAC f_ss 1);


340 
{\out Level 2}


341 
{\out f(i + j) = i + f(j)}


342 
{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}


343 
\end{ttbox}


344 
The remaining subgoal requires rewriting by the premise, shown


345 
below, so we add it to {\tt f_ss}:


346 
\begin{ttbox}


347 
prth prem;


348 
{\out f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))]}


349 
by (ASM_SIMP_TAC (f_ss addrews [prem]) 1);


350 
{\out Level 3}


351 
{\out f(i + j) = i + f(j)}


352 
{\out No subgoals!}


353 
\end{ttbox}


354 


355 


356 
\section{Setting up the simplifier} \label{SimpFuninput}


357 
\index{simplification!setting upbold}


358 
To set up a simplifier for a new logic, the \ML\ functor


359 
\ttindex{SimpFun} needs to be supplied with theorems to justify


360 
rewriting. A rewrite relation must be reflexive and transitive; symmetry


361 
is not necessary. Hence the package is also applicable to nonsymmetric


362 
relations such as occur in operational semantics. In the sequel, $\gg$


363 
denotes some {\bf reduction relation}: a binary relation to be used for


364 
rewriting. Several reduction relations can be used at once. In {\tt FOL},


365 
both $=$ (on terms) and $\bimp$ (on formulae) can be used for rewriting.


366 


367 
The argument to {\tt SimpFun} is a structure with signature


368 
\ttindexbold{SIMP_DATA}:


369 
\begin{ttbox}


370 
signature SIMP_DATA =


371 
sig


372 
val case_splits : (thm * string) list


373 
val dest_red : term > term * term * term


374 
val mk_rew_rules : thm > thm list


375 
val norm_thms : (thm*thm) list


376 
val red1 : thm


377 
val red2 : thm


378 
val refl_thms : thm list


379 
val subst_thms : thm list


380 
val trans_thms : thm list


381 
end;


382 
\end{ttbox}


383 
The components of {\tt SIMP_DATA} need to be instantiated as follows. Many


384 
of these components are lists, and can be empty.


385 
\begin{description}


386 
\item[\ttindexbold{refl_thms}]


387 
supplies reflexivity theorems of the form $\Var{x} \gg


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.


390 


391 
\item[\ttindexbold{trans_thms}]


392 
supplies transitivity theorems of the form


393 
$\List{\Var{x}\gg\Var{y}; \Var{y}\gg\Var{z}} \Imp {\Var{x}\gg\Var{z}}$.


394 


395 
\item[\ttindexbold{red1}]


396 
is a theorem of the form $\List{\Var{P}\gg\Var{Q};


397 
\Var{P}} \Imp \Var{Q}$, where $\gg$ is a relation between formulae, such as


398 
$\bimp$ in {\tt FOL}.


399 


400 
\item[\ttindexbold{red2}]


401 
is a theorem of the form $\List{\Var{P}\gg\Var{Q};


402 
\Var{Q}} \Imp \Var{P}$, where $\gg$ is a relation between formulae, such as


403 
$\bimp$ in {\tt FOL}.


404 


405 
\item[\ttindexbold{mk_rew_rules}]


406 
is a function that extracts rewrite rules from theorems. A rewrite rule is


407 
a theorem of the form $\List{\ldots}\Imp s \gg t$. In its simplest form,


408 
{\tt mk_rew_rules} maps a theorem $t$ to the singleton list $[t]$. More


409 
sophisticated versions may do things like


410 
\[


411 
\begin{array}{l@{}r@{\quad\mapsto\quad}l}


412 
\mbox{create formula rewrites:}& P & [P \bimp True] \\[.5ex]


413 
\mbox{remove negations:}& \lnot P & [P \bimp False] \\[.5ex]


414 
\mbox{create conditional rewrites:}& P\imp s\gg t & [P\Imp s\gg t] \\[.5ex]


415 
\mbox{break up conjunctions:}&


416 
(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]


417 
\end{array}


418 
\]


419 
The more theorems are turned into rewrite rules, the better. The function


420 
is used in two places:


421 
\begin{itemize}


422 
\item


423 
$ss$~\ttindex{addrews}~$thms$ applies {\tt mk_rew_rules} to each element of


424 
$thms$ before adding it to $ss$.


425 
\item


426 
simplification with assumptions (as in \ttindex{ASM_SIMP_TAC}) uses


427 
{\tt mk_rew_rules} to turn assumptions into rewrite rules.


428 
\end{itemize}


429 


430 
\item[\ttindexbold{case_splits}]


431 
supplies expansion rules for case splits. The simplifier is designed


432 
for rules roughly of the kind


433 
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))


434 
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))


435 
\]


436 
but is insensitive to the form of the righthand side. Other examples


437 
include product types, where $split ::


438 
(\alpha\To\beta\To\gamma)\To\alpha*\beta\To\gamma$:


439 
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =


440 
{<}a,b{>} \imp \Var{P}(\Var{f}(a,b)))


441 
\]


442 
Each theorem in the list is paired with the name of the constant being


443 
eliminated, {\tt"if"} and {\tt"split"} in the examples above.


444 


445 
\item[\ttindexbold{norm_thms}]


446 
supports an optimization. It should be a list of pairs of rules of the


447 
form $\Var{x} \gg norm(\Var{x})$ and $norm(\Var{x}) \gg \Var{x}$. These


448 
introduce and eliminate {\tt norm}, an arbitrary function that should be


449 
used nowhere else. This function serves to tag subterms that are in normal


450 
form. Such rules can speed up rewriting significantly!


451 


452 
\item[\ttindexbold{subst_thms}]


453 
supplies substitution rules of the form


454 
\[ \List{\Var{x} \gg \Var{y}; \Var{P}(\Var{x})} \Imp \Var{P}(\Var{y}) \]


455 
They are used to derive congruence rules via \ttindex{mk_congs} and


456 
\ttindex{mk_typed_congs}. If $f :: [\tau@1,\cdots,\tau@n]\To\tau$ is a


457 
constant or free variable, the computation of a congruence rule


458 
\[\List{\Var{x@1} \gg@1 \Var{y@1}; \ldots; \Var{x@n} \gg@n \Var{y@n}}


459 
\Imp f(\Var{x@1},\ldots,\Var{x@n}) \gg f(\Var{y@1},\ldots,\Var{y@n}) \]


460 
requires a reflexivity theorem for some reduction ${\gg} ::


461 
\alpha\To\alpha\To\sigma$ such that $\tau$ is an instance of $\alpha$. If a


462 
suitable reflexivity law is missing, no congruence rule for $f$ can be


463 
generated. Otherwise an $n$ary congruence rule of the form shown above is


464 
derived, subject to the availability of suitable substitution laws for each


465 
argument position.


466 


467 
A substitution law is suitable for argument $i$ if it


468 
uses a reduction ${\gg@i} :: \alpha@i\To\alpha@i\To\sigma@i$ such that


469 
$\tau@i$ is an instance of $\alpha@i$. If a suitable substitution law for


470 
argument $i$ is missing, the $i^{th}$ premise of the above congruence rule


471 
cannot be generated and hence argument $i$ cannot be rewritten. In the


472 
worst case, if there are no suitable substitution laws at all, the derived


473 
congruence simply degenerates into a reflexivity law.


474 


475 
\item[\ttindexbold{dest_red}]


476 
takes reductions apart. Given a term $t$ representing the judgement


477 
\mbox{$a \gg b$}, \verb$dest_red$~$t$ should return a triple $(c,ta,tb)$


478 
where $ta$ and $tb$ represent $a$ and $b$, and $c$ is a term of the form


479 
\verb$Const(_,_)$, the reduction constant $\gg$.


480 


481 
Suppose the logic has a coercion function like $Trueprop::o\To prop$, as do


482 
{\tt FOL} and~{\tt HOL}\@. If $\gg$ is a binary operator (not necessarily


483 
infix), the following definition does the job:


484 
\begin{verbatim}


485 
fun dest_red( _ $ (c $ ta $ tb) ) = (c,ta,tb);


486 
\end{verbatim}


487 
The wildcard pattern {\tt_} matches the coercion function.


488 
\end{description}


489 


490 


491 
\section{A sample instantiation}


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}.


494 
\begin{ttbox}


495 
structure FOL_SimpData : SIMP_DATA =


496 
struct


497 
val refl_thms = [ \(\Var{x}=\Var{x}\), \(\Var{P}\bimp\Var{P}\) ]


498 
val trans_thms = [ \(\List{\Var{x}=\Var{y};\Var{y}=\Var{z}}\Imp\Var{x}=\Var{z}\),


499 
\(\List{\Var{P}\bimp\Var{Q};\Var{Q}\bimp\Var{R}}\Imp\Var{P}\bimp\Var{R}\) ]


500 
val red1 = \(\List{\Var{P}\bimp\Var{Q}; \Var{P}} \Imp \Var{Q}\)


501 
val red2 = \(\List{\Var{P}\bimp\Var{Q}; \Var{Q}} \Imp \Var{P}\)


502 
val mk_rew_rules = ...


503 
val case_splits = [ \(\Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp\)


504 
\((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))\) ]


505 
val norm_thms = [ (\(\Var{x}=norm(\Var{x})\),\(norm(\Var{x})=\Var{x}\)),


506 
(\(\Var{P}\bimp{}NORM(\Var{P}\)), \(NORM(\Var{P})\bimp\Var{P}\)) ]


507 
val subst_thms = [ \(\List{\Var{x}=\Var{y}; \Var{P}(\Var{x})}\Imp\Var{P}(\Var{y})\) ]


508 
val dest_red = fn (_ $ (opn $ lhs $ rhs)) => (opn,lhs,rhs)


509 
end;


510 
\end{ttbox}


511 


512 
\index{simplification)}
