doc-src/Ref/simp.tex
 changeset 104 d8205bb279a7 child 286 e7efbf03562b
equal inserted replaced
103:30bd42401ab2 104:d8205bb279a7

     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 Figure~\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{description}

   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[\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 auto-tactic.

   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{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{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 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{description}

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