doc-src/Ref/simp.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 1100 74921c7613e7
child 11181 d04f57b91166
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     1 %%%THIS DOCUMENTS THE OBSOLETE SIMPLIFIER!!!!
     2 \chapter{Simplification} \label{simp-chap}
     3 \index{simplification|(}
     4 Object-level 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 place-holders 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 if-then-else\/} 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
    25 Fig.\ts\ref{SIMP}.  
    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 auto-tactic}, 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{simp-tactics}.
    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{simp-simpsets}
   110 Simpsets are values of the abstract type \ttindexbold{simpset}.  They are
   111 manipulated by the following functions:
   112 \index{simplification sets|bold}
   113 \begin{ttdescription}
   114 \item[\ttindexbold{empty_ss}] 
   115 is the empty simpset.  It has no congruence or rewrite rules and its
   116 auto-tactic always fails.
   117 
   118 \item[$ss$ \ttindexbold{addcongs} $thms$] 
   119 is the simpset~$ss$ plus the congruence rules~$thms$.
   120 
   121 \item[$ss$ \ttindexbold{delcongs} $thms$] 
   122 is the simpset~$ss$ minus the congruence rules~$thms$.
   123 
   124 \item[$ss$ \ttindexbold{addrews} $thms$] 
   125 is the simpset~$ss$ plus the rewrite rules~$thms$.
   126 
   127 \item[$ss$ \ttindexbold{delrews} $thms$] 
   128 is the simpset~$ss$ minus the rewrite rules~$thms$.
   129 
   130 \item[$ss$ \ttindexbold{setauto} $tacf$] 
   131 is the simpset~$ss$ with $tacf$ for its auto-tactic.
   132 
   133 \item[\ttindexbold{print_ss} $ss$] 
   134 prints all the congruence and rewrite rules in the simpset~$ss$.
   135 \end{ttdescription}
   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{SimpFun-input}.  
   147 
   148 The auto-tactic 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 auto-tactic is {\tt ares_tac [TrueI]}, which attempts proof by
   154 assumption and resolution with the theorem $True$.  In explicitly typed
   155 logics, the auto-tactic can be used to solve simple type checking
   156 obligations.  Some applications demand a sophisticated auto-tactic 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 auto-tactic is permitted to instantiate unknowns.
   163 \end{warn}
   164 
   165 
   166 \section{The simplification tactics} \label{simp-tactics}
   167 \index{simplification!tactics|bold}
   168 \index{tactics!simplification|bold}
   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{ttdescription}
   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 auto-tactic
   178 (\S\ref{simp-simpsets}).
   179   
   180 \item[\ttindexbold{ASM_SIMP_TAC}] 
   181 is like \verb$SIMP_TAC$, but also uses assumptions as additional
   182 rewrite rules.
   183 \end{ttdescription}
   184 Many logics have conditional operators like {\it if-then-else}.  If the
   185 simplifier has been set up with such case splits (see~\ttindex{case_splits}
   186 in \S\ref{SimpFun-input}), there are tactics which automatically alternate
   187 between simplification and case splitting:
   188 \begin{ttdescription}
   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 pre-conditions 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{ttdescription}
   210 Finally there are two useful functions for generating congruence
   211 rules for constants and free variables:
   212 \begin{ttdescription}
   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{ttdescription}
   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{SimpFun-input} 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{ttdescription}
   244 \item[Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,
   245 \item[add_0] is the rewrite rule $0+n = n$,
   246 \item[add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,
   247 \item[induct] is the induction rule
   248 $\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.
   249 \item[FOL_ss] is a basic simpset for {\tt FOL}.
   250 \end{ttdescription}
   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{SimpFun-input}
   357 \index{simplification!setting up|bold}
   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 non-symmetric
   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{ttdescription}
   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 right-hand 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{ttdescription}
   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|)}