doc-src/Ref/simp.tex
changeset 104 d8205bb279a7
child 286 e7efbf03562b
equal deleted 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|)}