avoid clash of Advanced/simp.thy vs. Misc/simp.thy;
--- a/doc-src/TutorialI/Advanced/ROOT.ML Wed Jul 25 22:30:18 2012 +0200
+++ b/doc-src/TutorialI/Advanced/ROOT.ML Wed Jul 25 23:02:50 2012 +0200
@@ -1,2 +1,2 @@
use "../settings.ML";
-use_thy "simp";
+use_thy "simp2";
--- a/doc-src/TutorialI/Advanced/advanced.tex Wed Jul 25 22:30:18 2012 +0200
+++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Jul 25 23:02:50 2012 +0200
@@ -5,7 +5,7 @@
yet and which are worth learning. The sections of this chapter are
independent of each other and can be read in any order.
-\input{Advanced/document/simp.tex}
+\input{Advanced/document/simp2.tex}
\section{Advanced Induction Techniques}
\label{sec:advanced-ind}
--- a/doc-src/TutorialI/Advanced/document/simp.tex Wed Jul 25 22:30:18 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{simp}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Simplification%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:simplification-II}\index{simplification|(}
-This section describes features not covered until now. It also
-outlines the simplification process itself, which can be helpful
-when the simplifier does not do what you expect of it.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Advanced Features%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Congruence Rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:simp-cong}
-While simplifying the conclusion $Q$
-of $P \Imp Q$, it is legal to use the assumption $P$.
-For $\Imp$ this policy is hardwired, but
-contextual information can also be made available for other
-operators. For example, \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} when simplifying \isa{xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}. The generation of contextual information during simplification is
-controlled by so-called \bfindex{congruence rules}. This is the one for
-\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}:
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-It should be read as follows:
-In order to simplify \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q} to \isa{P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}},
-simplify \isa{P} to \isa{P{\isaliteral{27}{\isacharprime}}}
-and assume \isa{P{\isaliteral{27}{\isacharprime}}} when simplifying \isa{Q} to \isa{Q{\isaliteral{27}{\isacharprime}}}.
-
-Here are some more examples. The congruence rules for bounded
-quantifiers supply contextual information about the bound variable:
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\ {\isaliteral{3D}{\isacharequal}}\ Q\ x{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
-\isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}B{\isaliteral{2E}{\isachardot}}\ Q\ x{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-One congruence rule for conditional expressions supplies contextual
-information for simplifying the \isa{then} and \isa{else} cases:
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{3B}{\isacharsemicolon}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{3D}{\isacharequal}}\ u{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ v{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
-\isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ u\ else\ v{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-An alternative congruence rule for conditional expressions
-actually \emph{prevents} simplification of some arguments:
-\begin{isabelle}%
-\ \ \ \ \ b\ {\isaliteral{3D}{\isacharequal}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-Only the first argument is simplified; the others remain unchanged.
-This makes simplification much faster and is faithful to the evaluation
-strategy in programming languages, which is why this is the default
-congruence rule for \isa{if}. Analogous rules control the evaluation of
-\isa{case} expressions.
-
-You can declare your own congruence rules with the attribute \attrdx{cong},
-either globally, in the usual manner,
-\begin{quote}
-\isacommand{declare} \textit{theorem-name} \isa{{\isaliteral{5B}{\isacharbrackleft}}cong{\isaliteral{5D}{\isacharbrackright}}}
-\end{quote}
-or locally in a \isa{simp} call by adding the modifier
-\begin{quote}
-\isa{cong{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}
-\end{quote}
-The effect is reversed by \isa{cong\ del} instead of \isa{cong}.
-
-\begin{warn}
-The congruence rule \isa{conj{\isaliteral{5F}{\isacharunderscore}}cong}
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-\par\noindent
-is occasionally useful but is not a default rule; you have to declare it explicitly.
-\end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Permutative Rewrite Rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{rewrite rules!permutative|bold}%
-An equation is a \textbf{permutative rewrite rule} if the left-hand
-side and right-hand side are the same up to renaming of variables. The most
-common permutative rule is commutativity: \isa{x\ {\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x}. Other examples
-include \isa{x\ {\isaliteral{2D}{\isacharminus}}\ y\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{2D}{\isacharminus}}\ y} in arithmetic and \isa{insert\ x\ {\isaliteral{28}{\isacharparenleft}}insert\ y\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ y\ {\isaliteral{28}{\isacharparenleft}}insert\ x\ A{\isaliteral{29}{\isacharparenright}}} for sets. Such rules are problematic because
-once they apply, they can be used forever. The simplifier is aware of this
-danger and treats permutative rules by means of a special strategy, called
-\bfindex{ordered rewriting}: a permutative rewrite
-rule is only applied if the term becomes smaller with respect to a fixed
-lexicographic ordering on terms. For example, commutativity rewrites
-\isa{b\ {\isaliteral{2B}{\isacharplus}}\ a} to \isa{a\ {\isaliteral{2B}{\isacharplus}}\ b}, but then stops because \isa{a\ {\isaliteral{2B}{\isacharplus}}\ b} is strictly
-smaller than \isa{b\ {\isaliteral{2B}{\isacharplus}}\ a}. Permutative rewrite rules can be turned into
-simplification rules in the usual manner via the \isa{simp} attribute; the
-simplifier recognizes their special status automatically.
-
-Permutative rewrite rules are most effective in the case of
-associative-commutative functions. (Associativity by itself is not
-permutative.) When dealing with an AC-function~$f$, keep the
-following points in mind:
-\begin{itemize}\index{associative-commutative function}
-
-\item The associative law must always be oriented from left to right,
- namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
- used with commutativity, can lead to nontermination.
-
-\item To complete your set of rewrite rules, you must add not just
- associativity~(A) and commutativity~(C) but also a derived rule, {\bf
- left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
-\end{itemize}
-Ordered rewriting with the combination of A, C, and LC sorts a term
-lexicographically:
-\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
- f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
-
-Note that ordered rewriting for \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}} on numbers is rarely
-necessary because the built-in arithmetic prover often succeeds without
-such tricks.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{How the Simplifier Works%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:SimpHow}
-Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
-first. A conditional equation is only applied if its condition can be
-proved, again by simplification. Below we explain some special features of
-the rewriting process.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Higher-Order Patterns%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{simplification rule|(}
-So far we have pretended the simplifier can deal with arbitrary
-rewrite rules. This is not quite true. For reasons of feasibility,
-the simplifier expects the
-left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
-This restricts where
-unknowns may occur. Higher-order patterns are terms in $\beta$-normal
-form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
-Each occurrence of an unknown is of the form
-$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
-variables. Thus all ordinary rewrite rules, where all unknowns are
-of base type, for example \isa{{\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c{\isaliteral{29}{\isacharparenright}}}, are acceptable: if an unknown is
-of base type, it cannot have any arguments. Additionally, the rule
-\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is also acceptable, in
-both directions: all arguments of the unknowns \isa{{\isaliteral{3F}{\isacharquery}}P} and
-\isa{{\isaliteral{3F}{\isacharquery}}Q} are distinct bound variables.
-
-If the left-hand side is not a higher-order pattern, all is not lost.
-The simplifier will still try to apply the rule provided it
-matches directly: without much $\lambda$-calculus hocus
-pocus. For example, \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True} rewrites
-\isa{g\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ g} to \isa{True}, but will fail to match
-\isa{g{\isaliteral{28}{\isacharparenleft}}h\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ g{\isaliteral{28}{\isacharparenleft}}h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}. However, you can
-eliminate the offending subterms --- those that are not patterns ---
-by adding new variables and conditions.
-In our example, we eliminate \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x} and obtain
- \isa{{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True}, which is fine
-as a conditional rewrite rule since conditions can be arbitrary
-terms. However, this trick is not a panacea because the newly
-introduced conditions may be hard to solve.
-
-There is no restriction on the form of the right-hand
-sides. They may not contain extraneous term or type variables, though.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The Preprocessor%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:simp-preprocessor}
-When a theorem is declared a simplification rule, it need not be a
-conditional equation already. The simplifier will turn it into a set of
-conditional equations automatically. For example, \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x} becomes the two separate
-simplification rules \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x} and \isa{h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x}. In
-general, the input theorem is converted as follows:
-\begin{eqnarray}
-\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
-P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
-P \land Q &\mapsto& P,\ Q \nonumber\\
-\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
-\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
-\isa{if}\ P\ \isa{then}\ Q\ \isa{else}\ R &\mapsto&
- P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
-\end{eqnarray}
-Once this conversion process is finished, all remaining non-equations
-$P$ are turned into trivial equations $P =\isa{True}$.
-For example, the formula
-\begin{center}\isa{{\isaliteral{28}{\isacharparenleft}}p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ r{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ s}\end{center}
-is converted into the three rules
-\begin{center}
-\isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u},\quad \isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ False},\quad \isa{s\ {\isaliteral{3D}{\isacharequal}}\ True}.
-\end{center}
-\index{simplification rule|)}
-\index{simplification|)}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Advanced/document/simp2.tex Wed Jul 25 23:02:50 2012 +0200
@@ -0,0 +1,249 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{simp{\isadigit{2}}}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Simplification%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:simplification-II}\index{simplification|(}
+This section describes features not covered until now. It also
+outlines the simplification process itself, which can be helpful
+when the simplifier does not do what you expect of it.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Advanced Features%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Congruence Rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:simp-cong}
+While simplifying the conclusion $Q$
+of $P \Imp Q$, it is legal to use the assumption $P$.
+For $\Imp$ this policy is hardwired, but
+contextual information can also be made available for other
+operators. For example, \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} when simplifying \isa{xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}. The generation of contextual information during simplification is
+controlled by so-called \bfindex{congruence rules}. This is the one for
+\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}:
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+It should be read as follows:
+In order to simplify \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q} to \isa{P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}},
+simplify \isa{P} to \isa{P{\isaliteral{27}{\isacharprime}}}
+and assume \isa{P{\isaliteral{27}{\isacharprime}}} when simplifying \isa{Q} to \isa{Q{\isaliteral{27}{\isacharprime}}}.
+
+Here are some more examples. The congruence rules for bounded
+quantifiers supply contextual information about the bound variable:
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\ {\isaliteral{3D}{\isacharequal}}\ Q\ x{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}B{\isaliteral{2E}{\isachardot}}\ Q\ x{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+One congruence rule for conditional expressions supplies contextual
+information for simplifying the \isa{then} and \isa{else} cases:
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{3B}{\isacharsemicolon}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{3D}{\isacharequal}}\ u{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ v{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ u\ else\ v{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+An alternative congruence rule for conditional expressions
+actually \emph{prevents} simplification of some arguments:
+\begin{isabelle}%
+\ \ \ \ \ b\ {\isaliteral{3D}{\isacharequal}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+Only the first argument is simplified; the others remain unchanged.
+This makes simplification much faster and is faithful to the evaluation
+strategy in programming languages, which is why this is the default
+congruence rule for \isa{if}. Analogous rules control the evaluation of
+\isa{case} expressions.
+
+You can declare your own congruence rules with the attribute \attrdx{cong},
+either globally, in the usual manner,
+\begin{quote}
+\isacommand{declare} \textit{theorem-name} \isa{{\isaliteral{5B}{\isacharbrackleft}}cong{\isaliteral{5D}{\isacharbrackright}}}
+\end{quote}
+or locally in a \isa{simp} call by adding the modifier
+\begin{quote}
+\isa{cong{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}
+\end{quote}
+The effect is reversed by \isa{cong\ del} instead of \isa{cong}.
+
+\begin{warn}
+The congruence rule \isa{conj{\isaliteral{5F}{\isacharunderscore}}cong}
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\par\noindent
+is occasionally useful but is not a default rule; you have to declare it explicitly.
+\end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Permutative Rewrite Rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{rewrite rules!permutative|bold}%
+An equation is a \textbf{permutative rewrite rule} if the left-hand
+side and right-hand side are the same up to renaming of variables. The most
+common permutative rule is commutativity: \isa{x\ {\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x}. Other examples
+include \isa{x\ {\isaliteral{2D}{\isacharminus}}\ y\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{2D}{\isacharminus}}\ y} in arithmetic and \isa{insert\ x\ {\isaliteral{28}{\isacharparenleft}}insert\ y\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ y\ {\isaliteral{28}{\isacharparenleft}}insert\ x\ A{\isaliteral{29}{\isacharparenright}}} for sets. Such rules are problematic because
+once they apply, they can be used forever. The simplifier is aware of this
+danger and treats permutative rules by means of a special strategy, called
+\bfindex{ordered rewriting}: a permutative rewrite
+rule is only applied if the term becomes smaller with respect to a fixed
+lexicographic ordering on terms. For example, commutativity rewrites
+\isa{b\ {\isaliteral{2B}{\isacharplus}}\ a} to \isa{a\ {\isaliteral{2B}{\isacharplus}}\ b}, but then stops because \isa{a\ {\isaliteral{2B}{\isacharplus}}\ b} is strictly
+smaller than \isa{b\ {\isaliteral{2B}{\isacharplus}}\ a}. Permutative rewrite rules can be turned into
+simplification rules in the usual manner via the \isa{simp} attribute; the
+simplifier recognizes their special status automatically.
+
+Permutative rewrite rules are most effective in the case of
+associative-commutative functions. (Associativity by itself is not
+permutative.) When dealing with an AC-function~$f$, keep the
+following points in mind:
+\begin{itemize}\index{associative-commutative function}
+
+\item The associative law must always be oriented from left to right,
+ namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
+ used with commutativity, can lead to nontermination.
+
+\item To complete your set of rewrite rules, you must add not just
+ associativity~(A) and commutativity~(C) but also a derived rule, {\bf
+ left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
+\end{itemize}
+Ordered rewriting with the combination of A, C, and LC sorts a term
+lexicographically:
+\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
+ f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
+
+Note that ordered rewriting for \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}} on numbers is rarely
+necessary because the built-in arithmetic prover often succeeds without
+such tricks.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{How the Simplifier Works%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:SimpHow}
+Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
+first. A conditional equation is only applied if its condition can be
+proved, again by simplification. Below we explain some special features of
+the rewriting process.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Higher-Order Patterns%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{simplification rule|(}
+So far we have pretended the simplifier can deal with arbitrary
+rewrite rules. This is not quite true. For reasons of feasibility,
+the simplifier expects the
+left-hand side of each rule to be a so-called \emph{higher-order
+pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
+This restricts where
+unknowns may occur. Higher-order patterns are terms in $\beta$-normal
+form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
+Each occurrence of an unknown is of the form
+$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
+variables. Thus all ordinary rewrite rules, where all unknowns are
+of base type, for example \isa{{\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c{\isaliteral{29}{\isacharparenright}}}, are acceptable: if an unknown is
+of base type, it cannot have any arguments. Additionally, the rule
+\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is also acceptable, in
+both directions: all arguments of the unknowns \isa{{\isaliteral{3F}{\isacharquery}}P} and
+\isa{{\isaliteral{3F}{\isacharquery}}Q} are distinct bound variables.
+
+If the left-hand side is not a higher-order pattern, all is not lost.
+The simplifier will still try to apply the rule provided it
+matches directly: without much $\lambda$-calculus hocus
+pocus. For example, \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True} rewrites
+\isa{g\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ g} to \isa{True}, but will fail to match
+\isa{g{\isaliteral{28}{\isacharparenleft}}h\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ g{\isaliteral{28}{\isacharparenleft}}h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}. However, you can
+eliminate the offending subterms --- those that are not patterns ---
+by adding new variables and conditions.
+In our example, we eliminate \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x} and obtain
+ \isa{{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True}, which is fine
+as a conditional rewrite rule since conditions can be arbitrary
+terms. However, this trick is not a panacea because the newly
+introduced conditions may be hard to solve.
+
+There is no restriction on the form of the right-hand
+sides. They may not contain extraneous term or type variables, though.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The Preprocessor%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:simp-preprocessor}
+When a theorem is declared a simplification rule, it need not be a
+conditional equation already. The simplifier will turn it into a set of
+conditional equations automatically. For example, \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x} becomes the two separate
+simplification rules \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x} and \isa{h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x}. In
+general, the input theorem is converted as follows:
+\begin{eqnarray}
+\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
+P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
+P \land Q &\mapsto& P,\ Q \nonumber\\
+\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
+\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
+\isa{if}\ P\ \isa{then}\ Q\ \isa{else}\ R &\mapsto&
+ P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
+\end{eqnarray}
+Once this conversion process is finished, all remaining non-equations
+$P$ are turned into trivial equations $P =\isa{True}$.
+For example, the formula
+\begin{center}\isa{{\isaliteral{28}{\isacharparenleft}}p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ r{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ s}\end{center}
+is converted into the three rules
+\begin{center}
+\isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u},\quad \isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ False},\quad \isa{s\ {\isaliteral{3D}{\isacharequal}}\ True}.
+\end{center}
+\index{simplification rule|)}
+\index{simplification|)}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/TutorialI/Advanced/simp.thy Wed Jul 25 22:30:18 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-(*<*)
-theory simp imports Main begin
-(*>*)
-
-section{*Simplification*}
-
-text{*\label{sec:simplification-II}\index{simplification|(}
-This section describes features not covered until now. It also
-outlines the simplification process itself, which can be helpful
-when the simplifier does not do what you expect of it.
-*}
-
-subsection{*Advanced Features*}
-
-subsubsection{*Congruence Rules*}
-
-text{*\label{sec:simp-cong}
-While simplifying the conclusion $Q$
-of $P \Imp Q$, it is legal to use the assumption $P$.
-For $\Imp$ this policy is hardwired, but
-contextual information can also be made available for other
-operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
-True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
-xs"}. The generation of contextual information during simplification is
-controlled by so-called \bfindex{congruence rules}. This is the one for
-@{text"\<longrightarrow>"}:
-@{thm[display]imp_cong[no_vars]}
-It should be read as follows:
-In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
-simplify @{prop P} to @{prop P'}
-and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
-
-Here are some more examples. The congruence rules for bounded
-quantifiers supply contextual information about the bound variable:
-@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
-One congruence rule for conditional expressions supplies contextual
-information for simplifying the @{text then} and @{text else} cases:
-@{thm[display]if_cong[no_vars]}
-An alternative congruence rule for conditional expressions
-actually \emph{prevents} simplification of some arguments:
-@{thm[display]if_weak_cong[no_vars]}
-Only the first argument is simplified; the others remain unchanged.
-This makes simplification much faster and is faithful to the evaluation
-strategy in programming languages, which is why this is the default
-congruence rule for @{text "if"}. Analogous rules control the evaluation of
-@{text case} expressions.
-
-You can declare your own congruence rules with the attribute \attrdx{cong},
-either globally, in the usual manner,
-\begin{quote}
-\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
-\end{quote}
-or locally in a @{text"simp"} call by adding the modifier
-\begin{quote}
-@{text"cong:"} \textit{list of theorem names}
-\end{quote}
-The effect is reversed by @{text"cong del"} instead of @{text cong}.
-
-\begin{warn}
-The congruence rule @{thm[source]conj_cong}
-@{thm[display]conj_cong[no_vars]}
-\par\noindent
-is occasionally useful but is not a default rule; you have to declare it explicitly.
-\end{warn}
-*}
-
-subsubsection{*Permutative Rewrite Rules*}
-
-text{*
-\index{rewrite rules!permutative|bold}%
-An equation is a \textbf{permutative rewrite rule} if the left-hand
-side and right-hand side are the same up to renaming of variables. The most
-common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples
-include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
-y A) = insert y (insert x A)"} for sets. Such rules are problematic because
-once they apply, they can be used forever. The simplifier is aware of this
-danger and treats permutative rules by means of a special strategy, called
-\bfindex{ordered rewriting}: a permutative rewrite
-rule is only applied if the term becomes smaller with respect to a fixed
-lexicographic ordering on terms. For example, commutativity rewrites
-@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
-smaller than @{term"b+a"}. Permutative rewrite rules can be turned into
-simplification rules in the usual manner via the @{text simp} attribute; the
-simplifier recognizes their special status automatically.
-
-Permutative rewrite rules are most effective in the case of
-associative-commutative functions. (Associativity by itself is not
-permutative.) When dealing with an AC-function~$f$, keep the
-following points in mind:
-\begin{itemize}\index{associative-commutative function}
-
-\item The associative law must always be oriented from left to right,
- namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
- used with commutativity, can lead to nontermination.
-
-\item To complete your set of rewrite rules, you must add not just
- associativity~(A) and commutativity~(C) but also a derived rule, {\bf
- left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
-\end{itemize}
-Ordered rewriting with the combination of A, C, and LC sorts a term
-lexicographically:
-\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
- f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
-
-Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
-necessary because the built-in arithmetic prover often succeeds without
-such tricks.
-*}
-
-subsection{*How the Simplifier Works*}
-
-text{*\label{sec:SimpHow}
-Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
-first. A conditional equation is only applied if its condition can be
-proved, again by simplification. Below we explain some special features of
-the rewriting process.
-*}
-
-subsubsection{*Higher-Order Patterns*}
-
-text{*\index{simplification rule|(}
-So far we have pretended the simplifier can deal with arbitrary
-rewrite rules. This is not quite true. For reasons of feasibility,
-the simplifier expects the
-left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
-This restricts where
-unknowns may occur. Higher-order patterns are terms in $\beta$-normal
-form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
-Each occurrence of an unknown is of the form
-$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
-variables. Thus all ordinary rewrite rules, where all unknowns are
-of base type, for example @{thm add_assoc}, are acceptable: if an unknown is
-of base type, it cannot have any arguments. Additionally, the rule
-@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in
-both directions: all arguments of the unknowns @{text"?P"} and
-@{text"?Q"} are distinct bound variables.
-
-If the left-hand side is not a higher-order pattern, all is not lost.
-The simplifier will still try to apply the rule provided it
-matches directly: without much $\lambda$-calculus hocus
-pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
-@{term"g a \<in> range g"} to @{const True}, but will fail to match
-@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can
-eliminate the offending subterms --- those that are not patterns ---
-by adding new variables and conditions.
-In our example, we eliminate @{text"?f ?x"} and obtain
- @{text"?y =
-?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine
-as a conditional rewrite rule since conditions can be arbitrary
-terms. However, this trick is not a panacea because the newly
-introduced conditions may be hard to solve.
-
-There is no restriction on the form of the right-hand
-sides. They may not contain extraneous term or type variables, though.
-*}
-
-subsubsection{*The Preprocessor*}
-
-text{*\label{sec:simp-preprocessor}
-When a theorem is declared a simplification rule, it need not be a
-conditional equation already. The simplifier will turn it into a set of
-conditional equations automatically. For example, @{prop"f x =
-g x & h x = k x"} becomes the two separate
-simplification rules @{prop"f x = g x"} and @{prop"h x = k x"}. In
-general, the input theorem is converted as follows:
-\begin{eqnarray}
-\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
-P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
-P \land Q &\mapsto& P,\ Q \nonumber\\
-\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
-\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
-@{text "if"}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
- P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
-\end{eqnarray}
-Once this conversion process is finished, all remaining non-equations
-$P$ are turned into trivial equations $P =\isa{True}$.
-For example, the formula
-\begin{center}@{prop"(p \<longrightarrow> t=u \<and> ~r) \<and> s"}\end{center}
-is converted into the three rules
-\begin{center}
-@{prop"p \<Longrightarrow> t = u"},\quad @{prop"p \<Longrightarrow> r = False"},\quad @{prop"s = True"}.
-\end{center}
-\index{simplification rule|)}
-\index{simplification|)}
-*}
-(*<*)
-end
-(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Advanced/simp2.thy Wed Jul 25 23:02:50 2012 +0200
@@ -0,0 +1,189 @@
+(*<*)
+theory simp2 imports Main begin
+(*>*)
+
+section{*Simplification*}
+
+text{*\label{sec:simplification-II}\index{simplification|(}
+This section describes features not covered until now. It also
+outlines the simplification process itself, which can be helpful
+when the simplifier does not do what you expect of it.
+*}
+
+subsection{*Advanced Features*}
+
+subsubsection{*Congruence Rules*}
+
+text{*\label{sec:simp-cong}
+While simplifying the conclusion $Q$
+of $P \Imp Q$, it is legal to use the assumption $P$.
+For $\Imp$ this policy is hardwired, but
+contextual information can also be made available for other
+operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
+True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
+xs"}. The generation of contextual information during simplification is
+controlled by so-called \bfindex{congruence rules}. This is the one for
+@{text"\<longrightarrow>"}:
+@{thm[display]imp_cong[no_vars]}
+It should be read as follows:
+In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
+simplify @{prop P} to @{prop P'}
+and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
+
+Here are some more examples. The congruence rules for bounded
+quantifiers supply contextual information about the bound variable:
+@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
+One congruence rule for conditional expressions supplies contextual
+information for simplifying the @{text then} and @{text else} cases:
+@{thm[display]if_cong[no_vars]}
+An alternative congruence rule for conditional expressions
+actually \emph{prevents} simplification of some arguments:
+@{thm[display]if_weak_cong[no_vars]}
+Only the first argument is simplified; the others remain unchanged.
+This makes simplification much faster and is faithful to the evaluation
+strategy in programming languages, which is why this is the default
+congruence rule for @{text "if"}. Analogous rules control the evaluation of
+@{text case} expressions.
+
+You can declare your own congruence rules with the attribute \attrdx{cong},
+either globally, in the usual manner,
+\begin{quote}
+\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
+\end{quote}
+or locally in a @{text"simp"} call by adding the modifier
+\begin{quote}
+@{text"cong:"} \textit{list of theorem names}
+\end{quote}
+The effect is reversed by @{text"cong del"} instead of @{text cong}.
+
+\begin{warn}
+The congruence rule @{thm[source]conj_cong}
+@{thm[display]conj_cong[no_vars]}
+\par\noindent
+is occasionally useful but is not a default rule; you have to declare it explicitly.
+\end{warn}
+*}
+
+subsubsection{*Permutative Rewrite Rules*}
+
+text{*
+\index{rewrite rules!permutative|bold}%
+An equation is a \textbf{permutative rewrite rule} if the left-hand
+side and right-hand side are the same up to renaming of variables. The most
+common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples
+include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
+y A) = insert y (insert x A)"} for sets. Such rules are problematic because
+once they apply, they can be used forever. The simplifier is aware of this
+danger and treats permutative rules by means of a special strategy, called
+\bfindex{ordered rewriting}: a permutative rewrite
+rule is only applied if the term becomes smaller with respect to a fixed
+lexicographic ordering on terms. For example, commutativity rewrites
+@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
+smaller than @{term"b+a"}. Permutative rewrite rules can be turned into
+simplification rules in the usual manner via the @{text simp} attribute; the
+simplifier recognizes their special status automatically.
+
+Permutative rewrite rules are most effective in the case of
+associative-commutative functions. (Associativity by itself is not
+permutative.) When dealing with an AC-function~$f$, keep the
+following points in mind:
+\begin{itemize}\index{associative-commutative function}
+
+\item The associative law must always be oriented from left to right,
+ namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
+ used with commutativity, can lead to nontermination.
+
+\item To complete your set of rewrite rules, you must add not just
+ associativity~(A) and commutativity~(C) but also a derived rule, {\bf
+ left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
+\end{itemize}
+Ordered rewriting with the combination of A, C, and LC sorts a term
+lexicographically:
+\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
+ f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
+
+Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
+necessary because the built-in arithmetic prover often succeeds without
+such tricks.
+*}
+
+subsection{*How the Simplifier Works*}
+
+text{*\label{sec:SimpHow}
+Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
+first. A conditional equation is only applied if its condition can be
+proved, again by simplification. Below we explain some special features of
+the rewriting process.
+*}
+
+subsubsection{*Higher-Order Patterns*}
+
+text{*\index{simplification rule|(}
+So far we have pretended the simplifier can deal with arbitrary
+rewrite rules. This is not quite true. For reasons of feasibility,
+the simplifier expects the
+left-hand side of each rule to be a so-called \emph{higher-order
+pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
+This restricts where
+unknowns may occur. Higher-order patterns are terms in $\beta$-normal
+form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
+Each occurrence of an unknown is of the form
+$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
+variables. Thus all ordinary rewrite rules, where all unknowns are
+of base type, for example @{thm add_assoc}, are acceptable: if an unknown is
+of base type, it cannot have any arguments. Additionally, the rule
+@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in
+both directions: all arguments of the unknowns @{text"?P"} and
+@{text"?Q"} are distinct bound variables.
+
+If the left-hand side is not a higher-order pattern, all is not lost.
+The simplifier will still try to apply the rule provided it
+matches directly: without much $\lambda$-calculus hocus
+pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
+@{term"g a \<in> range g"} to @{const True}, but will fail to match
+@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can
+eliminate the offending subterms --- those that are not patterns ---
+by adding new variables and conditions.
+In our example, we eliminate @{text"?f ?x"} and obtain
+ @{text"?y =
+?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine
+as a conditional rewrite rule since conditions can be arbitrary
+terms. However, this trick is not a panacea because the newly
+introduced conditions may be hard to solve.
+
+There is no restriction on the form of the right-hand
+sides. They may not contain extraneous term or type variables, though.
+*}
+
+subsubsection{*The Preprocessor*}
+
+text{*\label{sec:simp-preprocessor}
+When a theorem is declared a simplification rule, it need not be a
+conditional equation already. The simplifier will turn it into a set of
+conditional equations automatically. For example, @{prop"f x =
+g x & h x = k x"} becomes the two separate
+simplification rules @{prop"f x = g x"} and @{prop"h x = k x"}. In
+general, the input theorem is converted as follows:
+\begin{eqnarray}
+\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
+P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
+P \land Q &\mapsto& P,\ Q \nonumber\\
+\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
+\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
+@{text "if"}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
+ P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
+\end{eqnarray}
+Once this conversion process is finished, all remaining non-equations
+$P$ are turned into trivial equations $P =\isa{True}$.
+For example, the formula
+\begin{center}@{prop"(p \<longrightarrow> t=u \<and> ~r) \<and> s"}\end{center}
+is converted into the three rules
+\begin{center}
+@{prop"p \<Longrightarrow> t = u"},\quad @{prop"p \<Longrightarrow> r = False"},\quad @{prop"s = True"}.
+\end{center}
+\index{simplification rule|)}
+\index{simplification|)}
+*}
+(*<*)
+end
+(*>*)
--- a/doc-src/TutorialI/IsaMakefile Wed Jul 25 22:30:18 2012 +0200
+++ b/doc-src/TutorialI/IsaMakefile Wed Jul 25 23:02:50 2012 +0200
@@ -121,7 +121,7 @@
HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
-$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
+$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp2.thy Advanced/ROOT.ML
$(USEDIR) Advanced
@rm -f Advanced/document/isabelle.sty
@rm -f Advanced/document/isabellesym.sty