# HG changeset patch # User wenzelm # Date 1343250170 -7200 # Node ID af1dabad14c0c3c7f0434b15d683d7019bbf1a77 # Parent d9e43ea3a045be5f59b8479ee204bc32f4d68827 avoid clash of Advanced/simp.thy vs. Misc/simp.thy; diff -r d9e43ea3a045 -r af1dabad14c0 doc-src/TutorialI/Advanced/ROOT.ML --- 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"; diff -r d9e43ea3a045 -r af1dabad14c0 doc-src/TutorialI/Advanced/advanced.tex --- 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} diff -r d9e43ea3a045 -r af1dabad14c0 doc-src/TutorialI/Advanced/document/simp.tex --- 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: diff -r d9e43ea3a045 -r af1dabad14c0 doc-src/TutorialI/Advanced/document/simp2.tex --- /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: diff -r d9e43ea3a045 -r af1dabad14c0 doc-src/TutorialI/Advanced/simp.thy --- 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"\"}: -@{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"(\x. ?P x \ ?Q x) = ((\x. ?P x) \ (\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 \ range ?f) = True"} rewrites -@{term"g a \ range g"} to @{const True}, but will fail to match -@{text"g(h b) \ range(\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 \ (?y \ 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 \ t=u \ ~r) \ s"}\end{center} -is converted into the three rules -\begin{center} -@{prop"p \ t = u"},\quad @{prop"p \ r = False"},\quad @{prop"s = True"}. -\end{center} -\index{simplification rule|)} -\index{simplification|)} -*} -(*<*) -end -(*>*) diff -r d9e43ea3a045 -r af1dabad14c0 doc-src/TutorialI/Advanced/simp2.thy --- /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"\"}: +@{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"(\x. ?P x \ ?Q x) = ((\x. ?P x) \ (\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 \ range ?f) = True"} rewrites +@{term"g a \ range g"} to @{const True}, but will fail to match +@{text"g(h b) \ range(\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 \ (?y \ 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 \ t=u \ ~r) \ s"}\end{center} +is converted into the three rules +\begin{center} +@{prop"p \ t = u"},\quad @{prop"p \ r = False"},\quad @{prop"s = True"}. +\end{center} +\index{simplification rule|)} +\index{simplification|)} +*} +(*<*) +end +(*>*) diff -r d9e43ea3a045 -r af1dabad14c0 doc-src/TutorialI/IsaMakefile --- 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