--- a/doc-src/Ref/simplifier.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/simplifier.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,4 +1,4 @@
-%% $Id$
+
\chapter{Simplification}
\label{chap:simplification}
\index{simplification|(}
@@ -810,173 +810,6 @@
\end{warn}
-\section{Examples of using the Simplifier}
-\index{examples!of simplification} Assume we are working within {\tt
- FOL} (see the file \texttt{FOL/ex/Nat}) and that
-\begin{ttdescription}
-\item[Nat.thy]
- is a theory including the constants $0$, $Suc$ and $+$,
-\item[add_0]
- is the rewrite rule $0+\Var{n} = \Var{n}$,
-\item[add_Suc]
- is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$,
-\item[induct]
- is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp
- \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$.
-\end{ttdescription}
-We augment the implicit simpset inherited from \texttt{Nat} with the
-basic rewrite rules for addition of natural numbers:
-\begin{ttbox}
-Addsimps [add_0, add_Suc];
-\end{ttbox}
-
-\subsection{A trivial example}
-Proofs by induction typically involve simplification. Here is a proof
-that~0 is a right identity:
-\begin{ttbox}
-Goal "m+0 = m";
-{\out Level 0}
-{\out m + 0 = m}
-{\out 1. m + 0 = m}
-\end{ttbox}
-The first step is to perform induction on the variable~$m$. This returns a
-base case and inductive step as two subgoals:
-\begin{ttbox}
-by (res_inst_tac [("n","m")] induct 1);
-{\out Level 1}
-{\out m + 0 = m}
-{\out 1. 0 + 0 = 0}
-{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
-\end{ttbox}
-Simplification solves the first subgoal trivially:
-\begin{ttbox}
-by (Simp_tac 1);
-{\out Level 2}
-{\out m + 0 = m}
-{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
-\end{ttbox}
-The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the
-induction hypothesis as a rewrite rule:
-\begin{ttbox}
-by (Asm_simp_tac 1);
-{\out Level 3}
-{\out m + 0 = m}
-{\out No subgoals!}
-\end{ttbox}
-
-\subsection{An example of tracing}
-\index{tracing!of simplification|(}\index{*trace_simp}
-
-Let us prove a similar result involving more complex terms. We prove
-that addition is commutative.
-\begin{ttbox}
-Goal "m+Suc(n) = Suc(m+n)";
-{\out Level 0}
-{\out m + Suc(n) = Suc(m + n)}
-{\out 1. m + Suc(n) = Suc(m + n)}
-\end{ttbox}
-Performing induction on~$m$ yields two subgoals:
-\begin{ttbox}
-by (res_inst_tac [("n","m")] induct 1);
-{\out Level 1}
-{\out m + Suc(n) = Suc(m + n)}
-{\out 1. 0 + Suc(n) = Suc(0 + n)}
-{\out 2. !!x. x + Suc(n) = Suc(x + n) ==>}
-{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}
-\end{ttbox}
-Simplification solves the first subgoal, this time rewriting two
-occurrences of~0:
-\begin{ttbox}
-by (Simp_tac 1);
-{\out Level 2}
-{\out m + Suc(n) = Suc(m + n)}
-{\out 1. !!x. x + Suc(n) = Suc(x + n) ==>}
-{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}
-\end{ttbox}
-Switching tracing on illustrates how the simplifier solves the remaining
-subgoal:
-\begin{ttbox}
-set trace_simp;
-by (Asm_simp_tac 1);
-\ttbreak
-{\out Adding rewrite rule:}
-{\out .x + Suc n == Suc (.x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out ?m + Suc ?n == Suc (?m + ?n)}
-{\out Rewriting:}
-{\out Suc .x + Suc n == Suc (Suc .x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out Suc ?m + ?n == Suc (?m + ?n)}
-{\out Rewriting:}
-{\out Suc .x + n == Suc (.x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out Suc ?m + ?n == Suc (?m + ?n)}
-{\out Rewriting:}
-{\out Suc .x + n == Suc (.x + n)}
-\ttbreak
-{\out Applying instance of rewrite rule:}
-{\out ?x = ?x == True}
-{\out Rewriting:}
-{\out Suc (Suc (.x + n)) = Suc (Suc (.x + n)) == True}
-\ttbreak
-{\out Level 3}
-{\out m + Suc(n) = Suc(m + n)}
-{\out No subgoals!}
-\end{ttbox}
-Many variations are possible. At Level~1 (in either example) we could have
-solved both subgoals at once using the tactical \ttindex{ALLGOALS}:
-\begin{ttbox}
-by (ALLGOALS Asm_simp_tac);
-{\out Level 2}
-{\out m + Suc(n) = Suc(m + n)}
-{\out No subgoals!}
-\end{ttbox}
-\index{tracing!of simplification|)}
-
-
-\subsection{Free variables and simplification}
-
-Here is a conjecture to be proved for an arbitrary function~$f$
-satisfying the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$:
-\begin{ttbox}
-val [prem] = Goal
- "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-{\out Level 0}
-{\out f(i + j) = i + f(j)}
-{\out 1. f(i + j) = i + f(j)}
-\ttbreak
-{\out val prem = "f(Suc(?n)) = Suc(f(?n))}
-{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
-\end{ttbox}
-In the theorem~\texttt{prem}, note that $f$ is a free variable while
-$\Var{n}$ is a schematic variable.
-\begin{ttbox}
-by (res_inst_tac [("n","i")] induct 1);
-{\out Level 1}
-{\out f(i + j) = i + f(j)}
-{\out 1. f(0 + j) = 0 + f(j)}
-{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
-\end{ttbox}
-We simplify each subgoal in turn. The first one is trivial:
-\begin{ttbox}
-by (Simp_tac 1);
-{\out Level 2}
-{\out f(i + j) = i + f(j)}
-{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
-\end{ttbox}
-The remaining subgoal requires rewriting by the premise, so we add it
-to the current simpset:
-\begin{ttbox}
-by (asm_simp_tac (simpset() addsimps [prem]) 1);
-{\out Level 3}
-{\out f(i + j) = i + f(j)}
-{\out No subgoals!}
-\end{ttbox}
-
-
\section{Permutative rewrite rules}
\index{rewrite rules!permutative|(}