
lcp@104: %%%THIS DOCUMENTS THE OBSOLETE SIMPLIFIER!!!!
lcp@104: \chapter{Simplification} \label{simp-chap}
lcp@104: \index{simplification|(}
lcp@104: Object-level rewriting is not primitive in Isabelle.  For efficiency,
lcp@104: perhaps it ought to be.  On the other hand, it is difficult to conceive of
lcp@104: a general mechanism that could accommodate the diversity of rewriting found
lcp@104: in different logics.  Hence rewriting in Isabelle works via resolution,
lcp@104: using unknowns as place-holders for simplified terms.  This chapter
lcp@104: describes a generic simplification package, the functor~\ttindex{SimpFun},
lcp@104: which expects the basic laws of equational logic and returns a suite of
lcp@104: simplification tactics.  The code lives in
lcp@104: \verb$Provers/simp.ML$.
lcp@104: 
lcp@104: This rewriting package is not as general as one might hope (using it for {\tt
lcp@104: HOL} is not quite as convenient as it could be; rewriting modulo equations is
lcp@104: not supported~\ldots) but works well for many logics.  It performs
lcp@104: conditional and unconditional rewriting and handles multiple reduction
lcp@104: relations and local assumptions.  It also has a facility for automatic case
lcp@104: splits by expanding conditionals like {\it if-then-else\/} during rewriting.
lcp@104: 
lcp@104: For many of Isabelle's logics ({\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt HOL})
lcp@104: the simplifier has been set up already. Hence we start by describing the
lcp@104: functions provided by the simplifier --- those functions exported by
lcp@104: \ttindex{SimpFun} through its result signature \ttindex{SIMP} shown in
lcp@286: Fig.\ts\ref{SIMP}.  
lcp@104: 
lcp@104: 
lcp@104: \section{Simplification sets}
lcp@104: \index{simplification sets}
lcp@104: The simplification tactics are controlled by {\bf simpsets}, which consist of
lcp@104: three things:
lcp@104: \begin{enumerate}
lcp@104: \item {\bf Rewrite rules}, which are theorems like 
lcp@104: $\Var{m} + succ(\Var{n}) = succ(\Var{m} + \Var{n})$.  {\bf Conditional}
lcp@104: rewrites such as $m<n \Imp m/n = 0$ are permitted.
lcp@104: \index{rewrite rules}
lcp@104: 
lcp@104: \item {\bf Congruence rules}, which typically have the form
lcp@104: \index{congruence rules}
lcp@104: \[ \List{\Var{x@1} = \Var{y@1}; \ldots; \Var{x@n} = \Var{y@n}} \Imp
lcp@104:    f(\Var{x@1},\ldots,\Var{x@n}) = f(\Var{y@1},\ldots,\Var{y@n}).
lcp@104: \]
lcp@104: 
lcp@104: \item The {\bf auto-tactic}, which attempts to solve the simplified
lcp@104: subgoal, say by recognizing it as a tautology.
lcp@104: \end{enumerate}
lcp@104: 
lcp@104: \subsection{Congruence rules}
lcp@104: Congruence rules enable the rewriter to simplify subterms.  Without a
lcp@104: congruence rule for the function~$g$, no argument of~$g$ can be rewritten.
lcp@104: Congruence rules can be generalized in the following ways:
lcp@104: 
lcp@104: {\bf Additional assumptions} are allowed:
lcp@104: \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
lcp@104:    \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2})
lcp@104: \]
lcp@104: This rule assumes $Q@1$, and any rewrite rules it contains, while
lcp@1100: simplifying~$P@2$.  Such `local' assumptions are effective for rewriting
lcp@104: formulae such as $x=0\imp y+x=y$.
lcp@104: 
lcp@104: {\bf Additional quantifiers} are allowed, typically for binding operators:
lcp@104: \[ \List{\Forall z. \Var{P}(z) \bimp \Var{Q}(z)} \Imp
lcp@104:    \forall x.\Var{P}(x) \bimp \forall x.\Var{Q}(x)
lcp@104: \]
lcp@104: 
lcp@104: {\bf Different equalities} can be mixed.  The following example
lcp@104: enables the transition from formula rewriting to term rewriting:
lcp@104: \[ \List{\Var{x@1}=\Var{y@1};\Var{x@2}=\Var{y@2}} \Imp
lcp@104:    (\Var{x@1}=\Var{x@2}) \bimp (\Var{y@1}=\Var{y@2})
lcp@104: \]
lcp@104: \begin{warn}
lcp@104: It is not necessary to assert a separate congruence rule for each constant,
lcp@104: provided your logic contains suitable substitution rules. The function {\tt
lcp@104: mk_congs} derives congruence rules from substitution
lcp@104: rules~\S\ref{simp-tactics}.
lcp@104: \end{warn}
lcp@104: 
lcp@104: 
lcp@104: \begin{figure}
lcp@104: \indexbold{*SIMP}
lcp@104: \begin{ttbox}
lcp@104: infix 4 addrews addcongs delrews delcongs setauto;
lcp@104: signature SIMP =
lcp@104: sig
lcp@104:   type simpset
lcp@104:   val empty_ss  : simpset
lcp@104:   val addcongs  : simpset * thm list -> simpset
lcp@104:   val addrews   : simpset * thm list -> simpset
lcp@104:   val delcongs  : simpset * thm list -> simpset
lcp@104:   val delrews   : simpset * thm list -> simpset
lcp@104:   val print_ss  : simpset -> unit
lcp@104:   val setauto   : simpset * (int -> tactic) -> simpset
lcp@104:   val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
lcp@104:   val ASM_SIMP_TAC      : simpset -> int -> tactic
lcp@104:   val CASE_TAC          : simpset -> int -> tactic
lcp@104:   val SIMP_CASE2_TAC    : simpset -> int -> tactic
lcp@104:   val SIMP_THM          : simpset -> thm -> thm
lcp@104:   val SIMP_TAC          : simpset -> int -> tactic
lcp@104:   val SIMP_CASE_TAC     : simpset -> int -> tactic
lcp@104:   val mk_congs          : theory -> string list -> thm list
lcp@104:   val mk_typed_congs    : theory -> (string*string) list -> thm list
lcp@104:   val tracing   : bool ref
lcp@104: end;
lcp@104: \end{ttbox}
lcp@104: \caption{The signature {\tt SIMP}} \label{SIMP}
lcp@104: \end{figure}
lcp@104: 
lcp@104: 
lcp@104: \subsection{The abstract type {\tt simpset}}\label{simp-simpsets}
lcp@104: Simpsets are values of the abstract type \ttindexbold{simpset}.  They are
lcp@104: manipulated by the following functions:
lcp@104: \index{simplification sets|bold}
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{empty_ss}] 
lcp@104: is the empty simpset.  It has no congruence or rewrite rules and its
lcp@104: auto-tactic always fails.
lcp@104: 
lcp@323: \item[$ss$ \ttindexbold{addcongs} $thms$] 
lcp@104: is the simpset~$ss$ plus the congruence rules~$thms$.
lcp@104: 
lcp@323: \item[$ss$ \ttindexbold{delcongs} $thms$] 
lcp@104: is the simpset~$ss$ minus the congruence rules~$thms$.
lcp@104: 
lcp@323: \item[$ss$ \ttindexbold{addrews} $thms$] 
lcp@104: is the simpset~$ss$ plus the rewrite rules~$thms$.
lcp@104: 
lcp@323: \item[$ss$ \ttindexbold{delrews} $thms$] 
lcp@104: is the simpset~$ss$ minus the rewrite rules~$thms$.
lcp@104: 
lcp@323: \item[$ss$ \ttindexbold{setauto} $tacf$] 
lcp@104: is the simpset~$ss$ with $tacf$ for its auto-tactic.
lcp@104: 
lcp@104: \item[\ttindexbold{print_ss} $ss$] 
lcp@104: prints all the congruence and rewrite rules in the simpset~$ss$.
lcp@323: \end{ttdescription}
lcp@104: Adding a rule to a simpset already containing it, or deleting one
lcp@104: from a simpset not containing it, generates a warning message.
lcp@104: 
lcp@104: In principle, any theorem can be used as a rewrite rule.  Before adding a
lcp@104: theorem to a simpset, {\tt addrews} preprocesses the theorem to extract the
lcp@104: maximum amount of rewriting from it.  Thus it need not have the form $s=t$.
lcp@104: In {\tt FOL} for example, an atomic formula $P$ is transformed into the
lcp@104: rewrite rule $P \bimp True$.  This preprocessing is not fixed but logic
lcp@104: dependent.  The existing logics like {\tt FOL} are fairly clever in this
lcp@104: respect.  For a more precise description see {\tt mk_rew_rules} in
lcp@104: \S\ref{SimpFun-input}.  
lcp@104: 
lcp@104: The auto-tactic is applied after simplification to solve a goal.  This may
lcp@104: be the overall goal or some subgoal that arose during conditional
lcp@104: rewriting.  Calling ${\tt auto_tac}~i$ must either solve exactly
lcp@104: subgoal~$i$ or fail.  If it succeeds without reducing the number of
lcp@104: subgoals by one, havoc and strange exceptions may result.
lcp@104: A typical auto-tactic is {\tt ares_tac [TrueI]}, which attempts proof by
lcp@104: assumption and resolution with the theorem $True$.  In explicitly typed
lcp@104: logics, the auto-tactic can be used to solve simple type checking
lcp@104: obligations.  Some applications demand a sophisticated auto-tactic such as
lcp@104: {\tt fast_tac}, but this could make simplification slow.
lcp@104:   
lcp@104: \begin{warn}
lcp@104: Rewriting never instantiates unknowns in subgoals.  (It uses
lcp@104: \ttindex{match_tac} rather than \ttindex{resolve_tac}.)  However, the
lcp@104: auto-tactic is permitted to instantiate unknowns.
lcp@104: \end{warn}
lcp@104: 
lcp@104: 
lcp@104: \section{The simplification tactics} \label{simp-tactics}
lcp@104: \index{simplification!tactics|bold}
lcp@104: \index{tactics!simplification|bold}
lcp@104: The actual simplification work is performed by the following tactics.  The
lcp@104: rewriting strategy is strictly bottom up.  Conditions in conditional rewrite
lcp@104: rules are solved recursively before the rewrite rule is applied.
lcp@104: 
lcp@104: There are two basic simplification tactics:
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{SIMP_TAC} $ss$ $i$] 
lcp@104: simplifies subgoal~$i$ using the rules in~$ss$.  It may solve the
lcp@104: subgoal completely if it has become trivial, using the auto-tactic
lcp@104: (\S\ref{simp-simpsets}).
lcp@104:   
lcp@104: \item[\ttindexbold{ASM_SIMP_TAC}] 
lcp@104: is like \verb$SIMP_TAC$, but also uses assumptions as additional
lcp@104: rewrite rules.
lcp@323: \end{ttdescription}
lcp@104: Many logics have conditional operators like {\it if-then-else}.  If the
lcp@104: simplifier has been set up with such case splits (see~\ttindex{case_splits}
lcp@104: in \S\ref{SimpFun-input}), there are tactics which automatically alternate
lcp@104: between simplification and case splitting:
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{SIMP_CASE_TAC}] 
lcp@104: is like {\tt SIMP_TAC} but also performs automatic case splits.
lcp@104: More precisely, after each simplification phase the tactic tries to apply a
lcp@104: theorem in \ttindex{case_splits}.  If this succeeds, the tactic calls
lcp@104: itself recursively on the result.
lcp@104: 
lcp@104: \item[\ttindexbold{ASM_SIMP_CASE_TAC}] 
lcp@104: is like {\tt SIMP_CASE_TAC}, but also uses assumptions for
lcp@104: rewriting.
lcp@104: 
lcp@104: \item[\ttindexbold{SIMP_CASE2_TAC}] 
lcp@104: is like {\tt SIMP_CASE_TAC}, but also tries to solve the
lcp@104: pre-conditions of conditional simplification rules by repeated case splits.
lcp@104: 
lcp@104: \item[\ttindexbold{CASE_TAC}] 
lcp@104: tries to break up a goal using a rule in
lcp@104: \ttindex{case_splits}.
lcp@104: 
lcp@104: \item[\ttindexbold{SIMP_THM}] 
lcp@104: simplifies a theorem using assumptions and case splitting.
lcp@323: \end{ttdescription}
lcp@104: Finally there are two useful functions for generating congruence
lcp@104: rules for constants and free variables:
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{mk_congs} $thy$ $cs$] 
lcp@104: computes a list of congruence rules, one for each constant in $cs$.
lcp@104: Remember that the name of an infix constant
lcp@104: \verb$+$ is \verb$op +$.
lcp@104: 
lcp@104: \item[\ttindexbold{mk_typed_congs}] 
lcp@104: computes congruence rules for explicitly typed free variables and
lcp@104: constants.  Its second argument is a list of name and type pairs.  Names
lcp@104: can be either free variables like {\tt P}, or constants like \verb$op =$.
lcp@104: For example in {\tt FOL}, the pair
lcp@104: \verb$("f","'a => 'a")$ generates the rule \verb$?x = ?y ==> f(?x) = f(?y)$.
lcp@104: Such congruence rules are necessary for goals with free variables whose
lcp@104: arguments need to be rewritten.
lcp@323: \end{ttdescription}
lcp@104: Both functions work correctly only if {\tt SimpFun} has been supplied with the
lcp@104: necessary substitution rules.  The details are discussed in
lcp@104: \S\ref{SimpFun-input} under {\tt subst_thms}.
lcp@104: \begin{warn}
lcp@104: Using the simplifier effectively may take a bit of experimentation. In
lcp@104: particular it may often happen that simplification stops short of what you
lcp@104: expected or runs forever. To diagnose these problems, the simplifier can be
lcp@104: traced. The reference variable \ttindexbold{tracing} controls the output of
lcp@104: tracing information.
lcp@104: \index{tracing!of simplification}
lcp@104: \end{warn}
lcp@104: 
lcp@104: 
lcp@104: \section{Example: using the simplifier}
lcp@104: \index{simplification!example}
lcp@104: Assume we are working within {\tt FOL} and that
lcp@323: \begin{ttdescription}
lcp@323: \item[Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,
lcp@323: \item[add_0] is the rewrite rule $0+n = n$,
lcp@323: \item[add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,
lcp@323: \item[induct] is the induction rule
lcp@104: $\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.
lcp@323: \item[FOL_ss] is a basic simpset for {\tt FOL}.
lcp@323: \end{ttdescription}
lcp@104: We generate congruence rules for $Suc$ and for the infix operator~$+$:
lcp@104: \begin{ttbox}
lcp@104: val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
lcp@104: prths nat_congs;
lcp@104: {\out ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)}
lcp@104: {\out [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb}
lcp@104: \end{ttbox}
lcp@104: We create a simpset for natural numbers by extending~{\tt FOL_ss}:
lcp@104: \begin{ttbox}
lcp@104: val add_ss = FOL_ss  addcongs nat_congs  
lcp@104:                      addrews  [add_0, add_Suc];
lcp@104: \end{ttbox}
lcp@104: Proofs by induction typically involve simplification:\footnote
lcp@104: {These examples reside on the file {\tt FOL/ex/nat.ML}.} 
lcp@104: \begin{ttbox}
lcp@104: goal Nat.thy "m+0 = m";
lcp@104: {\out Level 0}
lcp@104: {\out m + 0 = m}
lcp@104: {\out  1. m + 0 = m}
lcp@104: \ttbreak
lcp@104: by (res_inst_tac [("n","m")] induct 1);
lcp@104: {\out Level 1}
lcp@104: {\out m + 0 = m}
lcp@104: {\out  1. 0 + 0 = 0}
lcp@104: {\out  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
lcp@104: \end{ttbox}
lcp@104: Simplification solves the first subgoal:
lcp@104: \begin{ttbox}
lcp@104: by (SIMP_TAC add_ss 1);
lcp@104: {\out Level 2}
lcp@104: {\out m + 0 = m}
lcp@104: {\out  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
lcp@104: \end{ttbox}
lcp@104: The remaining subgoal requires \ttindex{ASM_SIMP_TAC} in order to use the
lcp@104: induction hypothesis as a rewrite rule:
lcp@104: \begin{ttbox}
lcp@104: by (ASM_SIMP_TAC add_ss 1);
lcp@104: {\out Level 3}
lcp@104: {\out m + 0 = m}
lcp@104: {\out No subgoals!}
lcp@104: \end{ttbox}
lcp@104: The next proof is similar.
lcp@104: \begin{ttbox}
lcp@104: goal Nat.thy "m+Suc(n) = Suc(m+n)";
lcp@104: {\out Level 0}
lcp@104: {\out m + Suc(n) = Suc(m + n)}
lcp@104: {\out  1. m + Suc(n) = Suc(m + n)}
lcp@104: \ttbreak
lcp@104: by (res_inst_tac [("n","m")] induct 1);
lcp@104: {\out Level 1}
lcp@104: {\out m + Suc(n) = Suc(m + n)}
lcp@104: {\out  1. 0 + Suc(n) = Suc(0 + n)}
lcp@104: {\out  2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}
lcp@104: \end{ttbox}
lcp@104: Using the tactical \ttindex{ALLGOALS}, a single command simplifies all the
lcp@104: subgoals:
lcp@104: \begin{ttbox}
lcp@104: by (ALLGOALS (ASM_SIMP_TAC add_ss));
lcp@104: {\out Level 2}
lcp@104: {\out m + Suc(n) = Suc(m + n)}
lcp@104: {\out No subgoals!}
lcp@104: \end{ttbox}
lcp@104: Some goals contain free function variables.  The simplifier must have
lcp@104: congruence rules for those function variables, or it will be unable to
lcp@104: simplify their arguments:
lcp@104: \begin{ttbox}
lcp@104: val f_congs = mk_typed_congs Nat.thy [("f","nat => nat")];
lcp@104: val f_ss = add_ss addcongs f_congs;
lcp@104: prths f_congs;
lcp@104: {\out ?Xa = ?Ya ==> f(?Xa) = f(?Ya)}
lcp@104: \end{ttbox}
lcp@104: Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
lcp@104: the law $f(Suc(n)) = Suc(f(n))$:
lcp@104: \begin{ttbox}
lcp@104: val [prem] = goal Nat.thy
lcp@104:     "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
lcp@104: {\out Level 0}
lcp@104: {\out f(i + j) = i + f(j)}
lcp@104: {\out  1. f(i + j) = i + f(j)}
lcp@104: \ttbreak
lcp@104: by (res_inst_tac [("n","i")] induct 1);
lcp@104: {\out Level 1}
lcp@104: {\out f(i + j) = i + f(j)}
lcp@104: {\out  1. f(0 + j) = 0 + f(j)}
lcp@104: {\out  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
lcp@104: \end{ttbox}
lcp@104: We simplify each subgoal in turn.  The first one is trivial:
lcp@104: \begin{ttbox}
lcp@104: by (SIMP_TAC f_ss 1);
lcp@104: {\out Level 2}
lcp@104: {\out f(i + j) = i + f(j)}
lcp@104: {\out  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
lcp@104: \end{ttbox}
lcp@104: The remaining subgoal requires rewriting by the premise, shown
lcp@104: below, so we add it to {\tt f_ss}:
lcp@104: \begin{ttbox}
lcp@104: prth prem;
lcp@104: {\out f(Suc(?n)) = Suc(f(?n))  [!!n. f(Suc(n)) = Suc(f(n))]}
lcp@104: by (ASM_SIMP_TAC (f_ss addrews [prem]) 1);
lcp@104: {\out Level 3}
lcp@104: {\out f(i + j) = i + f(j)}
lcp@104: {\out No subgoals!}
lcp@104: \end{ttbox}
lcp@104: 
lcp@104: 
lcp@104: \section{Setting up the simplifier} \label{SimpFun-input}
lcp@104: \index{simplification!setting up|bold}
lcp@104: To set up a simplifier for a new logic, the \ML\ functor
lcp@104: \ttindex{SimpFun} needs to be supplied with theorems to justify
lcp@104: rewriting.  A rewrite relation must be reflexive and transitive; symmetry
lcp@104: is not necessary.  Hence the package is also applicable to non-symmetric
lcp@104: relations such as occur in operational semantics.  In the sequel, $\gg$
lcp@104: denotes some {\bf reduction relation}: a binary relation to be used for
lcp@104: rewriting.  Several reduction relations can be used at once.  In {\tt FOL},
lcp@104: both $=$ (on terms) and $\bimp$ (on formulae) can be used for rewriting.
lcp@104: 
lcp@104: The argument to {\tt SimpFun} is a structure with signature
lcp@104: \ttindexbold{SIMP_DATA}:
lcp@104: \begin{ttbox}
lcp@104: signature SIMP_DATA =
lcp@104: sig
lcp@104:   val case_splits  : (thm * string) list
lcp@104:   val dest_red     : term -> term * term * term
lcp@104:   val mk_rew_rules : thm -> thm list
lcp@104:   val norm_thms    : (thm*thm) list
lcp@104:   val red1         : thm
lcp@104:   val red2         : thm 
lcp@104:   val refl_thms    : thm list
lcp@104:   val subst_thms   : thm list 
lcp@104:   val trans_thms   : thm list
lcp@104: end;
lcp@104: \end{ttbox}
lcp@104: The components of {\tt SIMP_DATA} need to be instantiated as follows.  Many
lcp@104: of these components are lists, and can be empty.
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{refl_thms}] 
lcp@104: supplies reflexivity theorems of the form $\Var{x} \gg
lcp@104: \Var{x}$.  They must not have additional premises as, for example,
lcp@104: $\Var{x}\in\Var{A} \Imp \Var{x} = \Var{x}\in\Var{A}$ in type theory.
lcp@104: 
lcp@104: \item[\ttindexbold{trans_thms}] 
lcp@104: supplies transitivity theorems of the form
lcp@104: $\List{\Var{x}\gg\Var{y}; \Var{y}\gg\Var{z}} \Imp {\Var{x}\gg\Var{z}}$.
lcp@104: 
lcp@104: \item[\ttindexbold{red1}] 
lcp@104: is a theorem of the form $\List{\Var{P}\gg\Var{Q};
lcp@104: \Var{P}} \Imp \Var{Q}$, where $\gg$ is a relation between formulae, such as
lcp@104: $\bimp$ in {\tt FOL}.
lcp@104: 
lcp@104: \item[\ttindexbold{red2}] 
lcp@104: is a theorem of the form $\List{\Var{P}\gg\Var{Q};
lcp@104: \Var{Q}} \Imp \Var{P}$, where $\gg$ is a relation between formulae, such as
lcp@104: $\bimp$ in {\tt FOL}.
lcp@104: 
lcp@104: \item[\ttindexbold{mk_rew_rules}] 
lcp@104: is a function that extracts rewrite rules from theorems.  A rewrite rule is
lcp@104: a theorem of the form $\List{\ldots}\Imp s \gg t$.  In its simplest form,
lcp@104: {\tt mk_rew_rules} maps a theorem $t$ to the singleton list $[t]$.  More
lcp@104: sophisticated versions may do things like
lcp@104: \[
lcp@104: \begin{array}{l@{}r@{\quad\mapsto\quad}l}
lcp@104: \mbox{create formula rewrites:}& P & [P \bimp True] \\[.5ex]
oheimb@11181: \mbox{remove negations:}& \neg P & [P \bimp False] \\[.5ex]
lcp@104: \mbox{create conditional rewrites:}& P\imp s\gg t & [P\Imp s\gg t] \\[.5ex]
lcp@104: \mbox{break up conjunctions:}& 
lcp@104:         (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]
lcp@104: \end{array}
lcp@104: \]
lcp@104: The more theorems are turned into rewrite rules, the better.  The function
lcp@104: is used in two places:
lcp@104: \begin{itemize}
lcp@104: \item 
lcp@104: $ss$~\ttindex{addrews}~$thms$ applies {\tt mk_rew_rules} to each element of
lcp@104: $thms$ before adding it to $ss$.
lcp@104: \item 
lcp@104: simplification with assumptions (as in \ttindex{ASM_SIMP_TAC}) uses
lcp@104: {\tt mk_rew_rules} to turn assumptions into rewrite rules.
lcp@104: \end{itemize}
lcp@104: 
lcp@104: \item[\ttindexbold{case_splits}] 
lcp@104: supplies expansion rules for case splits.  The simplifier is designed
lcp@104: for rules roughly of the kind
lcp@104: \[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
oheimb@11181: \conj (\neg\Var{Q} \imp \Var{P}(\Var{y})) 
lcp@104: \] 
lcp@104: but is insensitive to the form of the right-hand side.  Other examples
lcp@104: include product types, where $split ::
lcp@104: (\alpha\To\beta\To\gamma)\To\alpha*\beta\To\gamma$:
lcp@104: \[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
lcp@104: {<}a,b{>} \imp \Var{P}(\Var{f}(a,b))) 
lcp@104: \] 
lcp@104: Each theorem in the list is paired with the name of the constant being
lcp@104: eliminated, {\tt"if"} and {\tt"split"} in the examples above.
lcp@104: 
lcp@104: \item[\ttindexbold{norm_thms}] 
lcp@104: supports an optimization.  It should be a list of pairs of rules of the
lcp@104: form $\Var{x} \gg norm(\Var{x})$ and $norm(\Var{x}) \gg \Var{x}$.  These
lcp@104: introduce and eliminate {\tt norm}, an arbitrary function that should be
lcp@104: used nowhere else.  This function serves to tag subterms that are in normal
lcp@104: form.  Such rules can speed up rewriting significantly!
lcp@104: 
lcp@104: \item[\ttindexbold{subst_thms}] 
lcp@104: supplies substitution rules of the form
lcp@104: \[ \List{\Var{x} \gg \Var{y}; \Var{P}(\Var{x})} \Imp \Var{P}(\Var{y}) \]
lcp@104: They are used to derive congruence rules via \ttindex{mk_congs} and
lcp@104: \ttindex{mk_typed_congs}.  If $f :: [\tau@1,\cdots,\tau@n]\To\tau$ is a
lcp@104: constant or free variable, the computation of a congruence rule
lcp@104: \[\List{\Var{x@1} \gg@1 \Var{y@1}; \ldots; \Var{x@n} \gg@n \Var{y@n}}
lcp@104: \Imp f(\Var{x@1},\ldots,\Var{x@n}) \gg f(\Var{y@1},\ldots,\Var{y@n}) \]
lcp@104: requires a reflexivity theorem for some reduction ${\gg} ::
lcp@104: \alpha\To\alpha\To\sigma$ such that $\tau$ is an instance of $\alpha$.  If a
lcp@104: suitable reflexivity law is missing, no congruence rule for $f$ can be
lcp@104: generated.   Otherwise an $n$-ary congruence rule of the form shown above is
lcp@104: derived, subject to the availability of suitable substitution laws for each
lcp@104: argument position.  
lcp@104: 
lcp@104: A substitution law is suitable for argument $i$ if it
lcp@104: uses a reduction ${\gg@i} :: \alpha@i\To\alpha@i\To\sigma@i$ such that
lcp@104: $\tau@i$ is an instance of $\alpha@i$.  If a suitable substitution law for
lcp@104: argument $i$ is missing, the $i^{th}$ premise of the above congruence rule
lcp@104: cannot be generated and hence argument $i$ cannot be rewritten.  In the
lcp@104: worst case, if there are no suitable substitution laws at all, the derived
lcp@104: congruence simply degenerates into a reflexivity law.
lcp@104: 
lcp@104: \item[\ttindexbold{dest_red}] 
lcp@104: takes reductions apart.  Given a term $t$ representing the judgement
lcp@104: \mbox{$a \gg b$}, \verb$dest_red$~$t$ should return a triple $(c,ta,tb)$
lcp@104: where $ta$ and $tb$ represent $a$ and $b$, and $c$ is a term of the form
lcp@104: \verb$Const(_,_)$, the reduction constant $\gg$.  
lcp@104: 
lcp@104: Suppose the logic has a coercion function like $Trueprop::o\To prop$, as do
lcp@104: {\tt FOL} and~{\tt HOL}\@.  If $\gg$ is a binary operator (not necessarily
lcp@104: infix), the following definition does the job:
lcp@104: \begin{verbatim}
lcp@104:    fun dest_red( _ $ (c $ ta $ tb) ) = (c,ta,tb);
lcp@104: \end{verbatim}
lcp@104: The wildcard pattern {\tt_} matches the coercion function.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
lcp@104: \section{A sample instantiation}
wenzelm@9695: Here is the instantiation of {\tt SIMP_DATA} for FOL.  The code for {\tt
wenzelm@9695:   mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
lcp@104: \begin{ttbox}
lcp@104: structure FOL_SimpData : SIMP_DATA =
lcp@104:   struct
lcp@104:   val refl_thms      = [ \(\Var{x}=\Var{x}\), \(\Var{P}\bimp\Var{P}\) ]
lcp@104:   val trans_thms     = [ \(\List{\Var{x}=\Var{y};\Var{y}=\Var{z}}\Imp\Var{x}=\Var{z}\),
lcp@104:                          \(\List{\Var{P}\bimp\Var{Q};\Var{Q}\bimp\Var{R}}\Imp\Var{P}\bimp\Var{R}\) ]
lcp@104:   val red1           = \(\List{\Var{P}\bimp\Var{Q}; \Var{P}} \Imp \Var{Q}\)
lcp@104:   val red2           = \(\List{\Var{P}\bimp\Var{Q}; \Var{Q}} \Imp \Var{P}\)
lcp@104:   val mk_rew_rules   = ...
lcp@104:   val case_splits    = [ \(\Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp\)
oheimb@11181:                            \((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))\) ]
lcp@104:   val norm_thms      = [ (\(\Var{x}=norm(\Var{x})\),\(norm(\Var{x})=\Var{x}\)),
lcp@104:                         (\(\Var{P}\bimp{}NORM(\Var{P}\)), \(NORM(\Var{P})\bimp\Var{P}\)) ]
lcp@104:   val subst_thms     = [ \(\List{\Var{x}=\Var{y}; \Var{P}(\Var{x})}\Imp\Var{P}(\Var{y})\) ]
lcp@104:   val dest_red       = fn (_ $ (opn $ lhs $ rhs)) => (opn,lhs,rhs)
lcp@104:   end;
lcp@104: \end{ttbox}
lcp@104: 
lcp@104: \index{simplification|)}




