%%%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|)}