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