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