avoid clash of Advanced/simp.thy vs. Misc/simp.thy;
1.1 --- a/doc-src/TutorialI/Advanced/ROOT.ML Wed Jul 25 22:30:18 2012 +0200
1.2 +++ b/doc-src/TutorialI/Advanced/ROOT.ML Wed Jul 25 23:02:50 2012 +0200
1.3 @@ -1,2 +1,2 @@
1.4 use "../settings.ML";
1.5 -use_thy "simp";
1.6 +use_thy "simp2";
2.1 --- a/doc-src/TutorialI/Advanced/advanced.tex Wed Jul 25 22:30:18 2012 +0200
2.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Jul 25 23:02:50 2012 +0200
2.3 @@ -5,7 +5,7 @@
2.4 yet and which are worth learning. The sections of this chapter are
2.5 independent of each other and can be read in any order.
2.6
2.7 -\input{Advanced/document/simp.tex}
2.8 +\input{Advanced/document/simp2.tex}
2.9
2.10 \section{Advanced Induction Techniques}
2.11 \label{sec:advanced-ind}
3.1 --- a/doc-src/TutorialI/Advanced/document/simp.tex Wed Jul 25 22:30:18 2012 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,249 +0,0 @@
3.4 -%
3.5 -\begin{isabellebody}%
3.6 -\def\isabellecontext{simp}%
3.7 -%
3.8 -\isadelimtheory
3.9 -%
3.10 -\endisadelimtheory
3.11 -%
3.12 -\isatagtheory
3.13 -%
3.14 -\endisatagtheory
3.15 -{\isafoldtheory}%
3.16 -%
3.17 -\isadelimtheory
3.18 -%
3.19 -\endisadelimtheory
3.20 -%
3.21 -\isamarkupsection{Simplification%
3.22 -}
3.23 -\isamarkuptrue%
3.24 -%
3.25 -\begin{isamarkuptext}%
3.26 -\label{sec:simplification-II}\index{simplification|(}
3.27 -This section describes features not covered until now. It also
3.28 -outlines the simplification process itself, which can be helpful
3.29 -when the simplifier does not do what you expect of it.%
3.30 -\end{isamarkuptext}%
3.31 -\isamarkuptrue%
3.32 -%
3.33 -\isamarkupsubsection{Advanced Features%
3.34 -}
3.35 -\isamarkuptrue%
3.36 -%
3.37 -\isamarkupsubsubsection{Congruence Rules%
3.38 -}
3.39 -\isamarkuptrue%
3.40 -%
3.41 -\begin{isamarkuptext}%
3.42 -\label{sec:simp-cong}
3.43 -While simplifying the conclusion $Q$
3.44 -of $P \Imp Q$, it is legal to use the assumption $P$.
3.45 -For $\Imp$ this policy is hardwired, but
3.46 -contextual information can also be made available for other
3.47 -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
3.48 -controlled by so-called \bfindex{congruence rules}. This is the one for
3.49 -\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}:
3.50 -\begin{isabelle}%
3.51 -\ \ \ \ \ {\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}}%
3.52 -\end{isabelle}
3.53 -It should be read as follows:
3.54 -In order to simplify \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q} to \isa{P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}},
3.55 -simplify \isa{P} to \isa{P{\isaliteral{27}{\isacharprime}}}
3.56 -and assume \isa{P{\isaliteral{27}{\isacharprime}}} when simplifying \isa{Q} to \isa{Q{\isaliteral{27}{\isacharprime}}}.
3.57 -
3.58 -Here are some more examples. The congruence rules for bounded
3.59 -quantifiers supply contextual information about the bound variable:
3.60 -\begin{isabelle}%
3.61 -\ \ \ \ \ {\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
3.62 -\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}}%
3.63 -\end{isabelle}
3.64 -One congruence rule for conditional expressions supplies contextual
3.65 -information for simplifying the \isa{then} and \isa{else} cases:
3.66 -\begin{isabelle}%
3.67 -\ \ \ \ \ {\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
3.68 -\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}}%
3.69 -\end{isabelle}
3.70 -An alternative congruence rule for conditional expressions
3.71 -actually \emph{prevents} simplification of some arguments:
3.72 -\begin{isabelle}%
3.73 -\ \ \ \ \ 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}}%
3.74 -\end{isabelle}
3.75 -Only the first argument is simplified; the others remain unchanged.
3.76 -This makes simplification much faster and is faithful to the evaluation
3.77 -strategy in programming languages, which is why this is the default
3.78 -congruence rule for \isa{if}. Analogous rules control the evaluation of
3.79 -\isa{case} expressions.
3.80 -
3.81 -You can declare your own congruence rules with the attribute \attrdx{cong},
3.82 -either globally, in the usual manner,
3.83 -\begin{quote}
3.84 -\isacommand{declare} \textit{theorem-name} \isa{{\isaliteral{5B}{\isacharbrackleft}}cong{\isaliteral{5D}{\isacharbrackright}}}
3.85 -\end{quote}
3.86 -or locally in a \isa{simp} call by adding the modifier
3.87 -\begin{quote}
3.88 -\isa{cong{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}
3.89 -\end{quote}
3.90 -The effect is reversed by \isa{cong\ del} instead of \isa{cong}.
3.91 -
3.92 -\begin{warn}
3.93 -The congruence rule \isa{conj{\isaliteral{5F}{\isacharunderscore}}cong}
3.94 -\begin{isabelle}%
3.95 -\ \ \ \ \ {\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}}%
3.96 -\end{isabelle}
3.97 -\par\noindent
3.98 -is occasionally useful but is not a default rule; you have to declare it explicitly.
3.99 -\end{warn}%
3.100 -\end{isamarkuptext}%
3.101 -\isamarkuptrue%
3.102 -%
3.103 -\isamarkupsubsubsection{Permutative Rewrite Rules%
3.104 -}
3.105 -\isamarkuptrue%
3.106 -%
3.107 -\begin{isamarkuptext}%
3.108 -\index{rewrite rules!permutative|bold}%
3.109 -An equation is a \textbf{permutative rewrite rule} if the left-hand
3.110 -side and right-hand side are the same up to renaming of variables. The most
3.111 -common permutative rule is commutativity: \isa{x\ {\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x}. Other examples
3.112 -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
3.113 -once they apply, they can be used forever. The simplifier is aware of this
3.114 -danger and treats permutative rules by means of a special strategy, called
3.115 -\bfindex{ordered rewriting}: a permutative rewrite
3.116 -rule is only applied if the term becomes smaller with respect to a fixed
3.117 -lexicographic ordering on terms. For example, commutativity rewrites
3.118 -\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
3.119 -smaller than \isa{b\ {\isaliteral{2B}{\isacharplus}}\ a}. Permutative rewrite rules can be turned into
3.120 -simplification rules in the usual manner via the \isa{simp} attribute; the
3.121 -simplifier recognizes their special status automatically.
3.122 -
3.123 -Permutative rewrite rules are most effective in the case of
3.124 -associative-commutative functions. (Associativity by itself is not
3.125 -permutative.) When dealing with an AC-function~$f$, keep the
3.126 -following points in mind:
3.127 -\begin{itemize}\index{associative-commutative function}
3.128 -
3.129 -\item The associative law must always be oriented from left to right,
3.130 - namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
3.131 - used with commutativity, can lead to nontermination.
3.132 -
3.133 -\item To complete your set of rewrite rules, you must add not just
3.134 - associativity~(A) and commutativity~(C) but also a derived rule, {\bf
3.135 - left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
3.136 -\end{itemize}
3.137 -Ordered rewriting with the combination of A, C, and LC sorts a term
3.138 -lexicographically:
3.139 -\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
3.140 - 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)) \]
3.141 -
3.142 -Note that ordered rewriting for \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}} on numbers is rarely
3.143 -necessary because the built-in arithmetic prover often succeeds without
3.144 -such tricks.%
3.145 -\end{isamarkuptext}%
3.146 -\isamarkuptrue%
3.147 -%
3.148 -\isamarkupsubsection{How the Simplifier Works%
3.149 -}
3.150 -\isamarkuptrue%
3.151 -%
3.152 -\begin{isamarkuptext}%
3.153 -\label{sec:SimpHow}
3.154 -Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
3.155 -first. A conditional equation is only applied if its condition can be
3.156 -proved, again by simplification. Below we explain some special features of
3.157 -the rewriting process.%
3.158 -\end{isamarkuptext}%
3.159 -\isamarkuptrue%
3.160 -%
3.161 -\isamarkupsubsubsection{Higher-Order Patterns%
3.162 -}
3.163 -\isamarkuptrue%
3.164 -%
3.165 -\begin{isamarkuptext}%
3.166 -\index{simplification rule|(}
3.167 -So far we have pretended the simplifier can deal with arbitrary
3.168 -rewrite rules. This is not quite true. For reasons of feasibility,
3.169 -the simplifier expects the
3.170 -left-hand side of each rule to be a so-called \emph{higher-order
3.171 -pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
3.172 -This restricts where
3.173 -unknowns may occur. Higher-order patterns are terms in $\beta$-normal
3.174 -form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
3.175 -Each occurrence of an unknown is of the form
3.176 -$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
3.177 -variables. Thus all ordinary rewrite rules, where all unknowns are
3.178 -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
3.179 -of base type, it cannot have any arguments. Additionally, the rule
3.180 -\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
3.181 -both directions: all arguments of the unknowns \isa{{\isaliteral{3F}{\isacharquery}}P} and
3.182 -\isa{{\isaliteral{3F}{\isacharquery}}Q} are distinct bound variables.
3.183 -
3.184 -If the left-hand side is not a higher-order pattern, all is not lost.
3.185 -The simplifier will still try to apply the rule provided it
3.186 -matches directly: without much $\lambda$-calculus hocus
3.187 -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
3.188 -\isa{g\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ g} to \isa{True}, but will fail to match
3.189 -\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
3.190 -eliminate the offending subterms --- those that are not patterns ---
3.191 -by adding new variables and conditions.
3.192 -In our example, we eliminate \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x} and obtain
3.193 - \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
3.194 -as a conditional rewrite rule since conditions can be arbitrary
3.195 -terms. However, this trick is not a panacea because the newly
3.196 -introduced conditions may be hard to solve.
3.197 -
3.198 -There is no restriction on the form of the right-hand
3.199 -sides. They may not contain extraneous term or type variables, though.%
3.200 -\end{isamarkuptext}%
3.201 -\isamarkuptrue%
3.202 -%
3.203 -\isamarkupsubsubsection{The Preprocessor%
3.204 -}
3.205 -\isamarkuptrue%
3.206 -%
3.207 -\begin{isamarkuptext}%
3.208 -\label{sec:simp-preprocessor}
3.209 -When a theorem is declared a simplification rule, it need not be a
3.210 -conditional equation already. The simplifier will turn it into a set of
3.211 -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
3.212 -simplification rules \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x} and \isa{h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x}. In
3.213 -general, the input theorem is converted as follows:
3.214 -\begin{eqnarray}
3.215 -\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
3.216 -P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
3.217 -P \land Q &\mapsto& P,\ Q \nonumber\\
3.218 -\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
3.219 -\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
3.220 -\isa{if}\ P\ \isa{then}\ Q\ \isa{else}\ R &\mapsto&
3.221 - P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
3.222 -\end{eqnarray}
3.223 -Once this conversion process is finished, all remaining non-equations
3.224 -$P$ are turned into trivial equations $P =\isa{True}$.
3.225 -For example, the formula
3.226 -\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}
3.227 -is converted into the three rules
3.228 -\begin{center}
3.229 -\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}.
3.230 -\end{center}
3.231 -\index{simplification rule|)}
3.232 -\index{simplification|)}%
3.233 -\end{isamarkuptext}%
3.234 -\isamarkuptrue%
3.235 -%
3.236 -\isadelimtheory
3.237 -%
3.238 -\endisadelimtheory
3.239 -%
3.240 -\isatagtheory
3.241 -%
3.242 -\endisatagtheory
3.243 -{\isafoldtheory}%
3.244 -%
3.245 -\isadelimtheory
3.246 -%
3.247 -\endisadelimtheory
3.248 -\end{isabellebody}%
3.249 -%%% Local Variables:
3.250 -%%% mode: latex
3.251 -%%% TeX-master: "root"
3.252 -%%% End:
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/TutorialI/Advanced/document/simp2.tex Wed Jul 25 23:02:50 2012 +0200
4.3 @@ -0,0 +1,249 @@
4.4 +%
4.5 +\begin{isabellebody}%
4.6 +\def\isabellecontext{simp{\isadigit{2}}}%
4.7 +%
4.8 +\isadelimtheory
4.9 +%
4.10 +\endisadelimtheory
4.11 +%
4.12 +\isatagtheory
4.13 +%
4.14 +\endisatagtheory
4.15 +{\isafoldtheory}%
4.16 +%
4.17 +\isadelimtheory
4.18 +%
4.19 +\endisadelimtheory
4.20 +%
4.21 +\isamarkupsection{Simplification%
4.22 +}
4.23 +\isamarkuptrue%
4.24 +%
4.25 +\begin{isamarkuptext}%
4.26 +\label{sec:simplification-II}\index{simplification|(}
4.27 +This section describes features not covered until now. It also
4.28 +outlines the simplification process itself, which can be helpful
4.29 +when the simplifier does not do what you expect of it.%
4.30 +\end{isamarkuptext}%
4.31 +\isamarkuptrue%
4.32 +%
4.33 +\isamarkupsubsection{Advanced Features%
4.34 +}
4.35 +\isamarkuptrue%
4.36 +%
4.37 +\isamarkupsubsubsection{Congruence Rules%
4.38 +}
4.39 +\isamarkuptrue%
4.40 +%
4.41 +\begin{isamarkuptext}%
4.42 +\label{sec:simp-cong}
4.43 +While simplifying the conclusion $Q$
4.44 +of $P \Imp Q$, it is legal to use the assumption $P$.
4.45 +For $\Imp$ this policy is hardwired, but
4.46 +contextual information can also be made available for other
4.47 +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
4.48 +controlled by so-called \bfindex{congruence rules}. This is the one for
4.49 +\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}:
4.50 +\begin{isabelle}%
4.51 +\ \ \ \ \ {\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}}%
4.52 +\end{isabelle}
4.53 +It should be read as follows:
4.54 +In order to simplify \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q} to \isa{P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}},
4.55 +simplify \isa{P} to \isa{P{\isaliteral{27}{\isacharprime}}}
4.56 +and assume \isa{P{\isaliteral{27}{\isacharprime}}} when simplifying \isa{Q} to \isa{Q{\isaliteral{27}{\isacharprime}}}.
4.57 +
4.58 +Here are some more examples. The congruence rules for bounded
4.59 +quantifiers supply contextual information about the bound variable:
4.60 +\begin{isabelle}%
4.61 +\ \ \ \ \ {\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
4.62 +\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}}%
4.63 +\end{isabelle}
4.64 +One congruence rule for conditional expressions supplies contextual
4.65 +information for simplifying the \isa{then} and \isa{else} cases:
4.66 +\begin{isabelle}%
4.67 +\ \ \ \ \ {\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
4.68 +\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}}%
4.69 +\end{isabelle}
4.70 +An alternative congruence rule for conditional expressions
4.71 +actually \emph{prevents} simplification of some arguments:
4.72 +\begin{isabelle}%
4.73 +\ \ \ \ \ 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}}%
4.74 +\end{isabelle}
4.75 +Only the first argument is simplified; the others remain unchanged.
4.76 +This makes simplification much faster and is faithful to the evaluation
4.77 +strategy in programming languages, which is why this is the default
4.78 +congruence rule for \isa{if}. Analogous rules control the evaluation of
4.79 +\isa{case} expressions.
4.80 +
4.81 +You can declare your own congruence rules with the attribute \attrdx{cong},
4.82 +either globally, in the usual manner,
4.83 +\begin{quote}
4.84 +\isacommand{declare} \textit{theorem-name} \isa{{\isaliteral{5B}{\isacharbrackleft}}cong{\isaliteral{5D}{\isacharbrackright}}}
4.85 +\end{quote}
4.86 +or locally in a \isa{simp} call by adding the modifier
4.87 +\begin{quote}
4.88 +\isa{cong{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}
4.89 +\end{quote}
4.90 +The effect is reversed by \isa{cong\ del} instead of \isa{cong}.
4.91 +
4.92 +\begin{warn}
4.93 +The congruence rule \isa{conj{\isaliteral{5F}{\isacharunderscore}}cong}
4.94 +\begin{isabelle}%
4.95 +\ \ \ \ \ {\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}}%
4.96 +\end{isabelle}
4.97 +\par\noindent
4.98 +is occasionally useful but is not a default rule; you have to declare it explicitly.
4.99 +\end{warn}%
4.100 +\end{isamarkuptext}%
4.101 +\isamarkuptrue%
4.102 +%
4.103 +\isamarkupsubsubsection{Permutative Rewrite Rules%
4.104 +}
4.105 +\isamarkuptrue%
4.106 +%
4.107 +\begin{isamarkuptext}%
4.108 +\index{rewrite rules!permutative|bold}%
4.109 +An equation is a \textbf{permutative rewrite rule} if the left-hand
4.110 +side and right-hand side are the same up to renaming of variables. The most
4.111 +common permutative rule is commutativity: \isa{x\ {\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x}. Other examples
4.112 +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
4.113 +once they apply, they can be used forever. The simplifier is aware of this
4.114 +danger and treats permutative rules by means of a special strategy, called
4.115 +\bfindex{ordered rewriting}: a permutative rewrite
4.116 +rule is only applied if the term becomes smaller with respect to a fixed
4.117 +lexicographic ordering on terms. For example, commutativity rewrites
4.118 +\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
4.119 +smaller than \isa{b\ {\isaliteral{2B}{\isacharplus}}\ a}. Permutative rewrite rules can be turned into
4.120 +simplification rules in the usual manner via the \isa{simp} attribute; the
4.121 +simplifier recognizes their special status automatically.
4.122 +
4.123 +Permutative rewrite rules are most effective in the case of
4.124 +associative-commutative functions. (Associativity by itself is not
4.125 +permutative.) When dealing with an AC-function~$f$, keep the
4.126 +following points in mind:
4.127 +\begin{itemize}\index{associative-commutative function}
4.128 +
4.129 +\item The associative law must always be oriented from left to right,
4.130 + namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
4.131 + used with commutativity, can lead to nontermination.
4.132 +
4.133 +\item To complete your set of rewrite rules, you must add not just
4.134 + associativity~(A) and commutativity~(C) but also a derived rule, {\bf
4.135 + left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
4.136 +\end{itemize}
4.137 +Ordered rewriting with the combination of A, C, and LC sorts a term
4.138 +lexicographically:
4.139 +\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
4.140 + 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)) \]
4.141 +
4.142 +Note that ordered rewriting for \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}} on numbers is rarely
4.143 +necessary because the built-in arithmetic prover often succeeds without
4.144 +such tricks.%
4.145 +\end{isamarkuptext}%
4.146 +\isamarkuptrue%
4.147 +%
4.148 +\isamarkupsubsection{How the Simplifier Works%
4.149 +}
4.150 +\isamarkuptrue%
4.151 +%
4.152 +\begin{isamarkuptext}%
4.153 +\label{sec:SimpHow}
4.154 +Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
4.155 +first. A conditional equation is only applied if its condition can be
4.156 +proved, again by simplification. Below we explain some special features of
4.157 +the rewriting process.%
4.158 +\end{isamarkuptext}%
4.159 +\isamarkuptrue%
4.160 +%
4.161 +\isamarkupsubsubsection{Higher-Order Patterns%
4.162 +}
4.163 +\isamarkuptrue%
4.164 +%
4.165 +\begin{isamarkuptext}%
4.166 +\index{simplification rule|(}
4.167 +So far we have pretended the simplifier can deal with arbitrary
4.168 +rewrite rules. This is not quite true. For reasons of feasibility,
4.169 +the simplifier expects the
4.170 +left-hand side of each rule to be a so-called \emph{higher-order
4.171 +pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
4.172 +This restricts where
4.173 +unknowns may occur. Higher-order patterns are terms in $\beta$-normal
4.174 +form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
4.175 +Each occurrence of an unknown is of the form
4.176 +$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
4.177 +variables. Thus all ordinary rewrite rules, where all unknowns are
4.178 +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
4.179 +of base type, it cannot have any arguments. Additionally, the rule
4.180 +\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
4.181 +both directions: all arguments of the unknowns \isa{{\isaliteral{3F}{\isacharquery}}P} and
4.182 +\isa{{\isaliteral{3F}{\isacharquery}}Q} are distinct bound variables.
4.183 +
4.184 +If the left-hand side is not a higher-order pattern, all is not lost.
4.185 +The simplifier will still try to apply the rule provided it
4.186 +matches directly: without much $\lambda$-calculus hocus
4.187 +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
4.188 +\isa{g\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ g} to \isa{True}, but will fail to match
4.189 +\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
4.190 +eliminate the offending subterms --- those that are not patterns ---
4.191 +by adding new variables and conditions.
4.192 +In our example, we eliminate \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x} and obtain
4.193 + \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
4.194 +as a conditional rewrite rule since conditions can be arbitrary
4.195 +terms. However, this trick is not a panacea because the newly
4.196 +introduced conditions may be hard to solve.
4.197 +
4.198 +There is no restriction on the form of the right-hand
4.199 +sides. They may not contain extraneous term or type variables, though.%
4.200 +\end{isamarkuptext}%
4.201 +\isamarkuptrue%
4.202 +%
4.203 +\isamarkupsubsubsection{The Preprocessor%
4.204 +}
4.205 +\isamarkuptrue%
4.206 +%
4.207 +\begin{isamarkuptext}%
4.208 +\label{sec:simp-preprocessor}
4.209 +When a theorem is declared a simplification rule, it need not be a
4.210 +conditional equation already. The simplifier will turn it into a set of
4.211 +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
4.212 +simplification rules \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x} and \isa{h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x}. In
4.213 +general, the input theorem is converted as follows:
4.214 +\begin{eqnarray}
4.215 +\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
4.216 +P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
4.217 +P \land Q &\mapsto& P,\ Q \nonumber\\
4.218 +\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
4.219 +\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
4.220 +\isa{if}\ P\ \isa{then}\ Q\ \isa{else}\ R &\mapsto&
4.221 + P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
4.222 +\end{eqnarray}
4.223 +Once this conversion process is finished, all remaining non-equations
4.224 +$P$ are turned into trivial equations $P =\isa{True}$.
4.225 +For example, the formula
4.226 +\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}
4.227 +is converted into the three rules
4.228 +\begin{center}
4.229 +\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}.
4.230 +\end{center}
4.231 +\index{simplification rule|)}
4.232 +\index{simplification|)}%
4.233 +\end{isamarkuptext}%
4.234 +\isamarkuptrue%
4.235 +%
4.236 +\isadelimtheory
4.237 +%
4.238 +\endisadelimtheory
4.239 +%
4.240 +\isatagtheory
4.241 +%
4.242 +\endisatagtheory
4.243 +{\isafoldtheory}%
4.244 +%
4.245 +\isadelimtheory
4.246 +%
4.247 +\endisadelimtheory
4.248 +\end{isabellebody}%
4.249 +%%% Local Variables:
4.250 +%%% mode: latex
4.251 +%%% TeX-master: "root"
4.252 +%%% End:
5.1 --- a/doc-src/TutorialI/Advanced/simp.thy Wed Jul 25 22:30:18 2012 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,189 +0,0 @@
5.4 -(*<*)
5.5 -theory simp imports Main begin
5.6 -(*>*)
5.7 -
5.8 -section{*Simplification*}
5.9 -
5.10 -text{*\label{sec:simplification-II}\index{simplification|(}
5.11 -This section describes features not covered until now. It also
5.12 -outlines the simplification process itself, which can be helpful
5.13 -when the simplifier does not do what you expect of it.
5.14 -*}
5.15 -
5.16 -subsection{*Advanced Features*}
5.17 -
5.18 -subsubsection{*Congruence Rules*}
5.19 -
5.20 -text{*\label{sec:simp-cong}
5.21 -While simplifying the conclusion $Q$
5.22 -of $P \Imp Q$, it is legal to use the assumption $P$.
5.23 -For $\Imp$ this policy is hardwired, but
5.24 -contextual information can also be made available for other
5.25 -operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
5.26 -True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
5.27 -xs"}. The generation of contextual information during simplification is
5.28 -controlled by so-called \bfindex{congruence rules}. This is the one for
5.29 -@{text"\<longrightarrow>"}:
5.30 -@{thm[display]imp_cong[no_vars]}
5.31 -It should be read as follows:
5.32 -In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
5.33 -simplify @{prop P} to @{prop P'}
5.34 -and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
5.35 -
5.36 -Here are some more examples. The congruence rules for bounded
5.37 -quantifiers supply contextual information about the bound variable:
5.38 -@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
5.39 -One congruence rule for conditional expressions supplies contextual
5.40 -information for simplifying the @{text then} and @{text else} cases:
5.41 -@{thm[display]if_cong[no_vars]}
5.42 -An alternative congruence rule for conditional expressions
5.43 -actually \emph{prevents} simplification of some arguments:
5.44 -@{thm[display]if_weak_cong[no_vars]}
5.45 -Only the first argument is simplified; the others remain unchanged.
5.46 -This makes simplification much faster and is faithful to the evaluation
5.47 -strategy in programming languages, which is why this is the default
5.48 -congruence rule for @{text "if"}. Analogous rules control the evaluation of
5.49 -@{text case} expressions.
5.50 -
5.51 -You can declare your own congruence rules with the attribute \attrdx{cong},
5.52 -either globally, in the usual manner,
5.53 -\begin{quote}
5.54 -\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
5.55 -\end{quote}
5.56 -or locally in a @{text"simp"} call by adding the modifier
5.57 -\begin{quote}
5.58 -@{text"cong:"} \textit{list of theorem names}
5.59 -\end{quote}
5.60 -The effect is reversed by @{text"cong del"} instead of @{text cong}.
5.61 -
5.62 -\begin{warn}
5.63 -The congruence rule @{thm[source]conj_cong}
5.64 -@{thm[display]conj_cong[no_vars]}
5.65 -\par\noindent
5.66 -is occasionally useful but is not a default rule; you have to declare it explicitly.
5.67 -\end{warn}
5.68 -*}
5.69 -
5.70 -subsubsection{*Permutative Rewrite Rules*}
5.71 -
5.72 -text{*
5.73 -\index{rewrite rules!permutative|bold}%
5.74 -An equation is a \textbf{permutative rewrite rule} if the left-hand
5.75 -side and right-hand side are the same up to renaming of variables. The most
5.76 -common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples
5.77 -include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
5.78 -y A) = insert y (insert x A)"} for sets. Such rules are problematic because
5.79 -once they apply, they can be used forever. The simplifier is aware of this
5.80 -danger and treats permutative rules by means of a special strategy, called
5.81 -\bfindex{ordered rewriting}: a permutative rewrite
5.82 -rule is only applied if the term becomes smaller with respect to a fixed
5.83 -lexicographic ordering on terms. For example, commutativity rewrites
5.84 -@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
5.85 -smaller than @{term"b+a"}. Permutative rewrite rules can be turned into
5.86 -simplification rules in the usual manner via the @{text simp} attribute; the
5.87 -simplifier recognizes their special status automatically.
5.88 -
5.89 -Permutative rewrite rules are most effective in the case of
5.90 -associative-commutative functions. (Associativity by itself is not
5.91 -permutative.) When dealing with an AC-function~$f$, keep the
5.92 -following points in mind:
5.93 -\begin{itemize}\index{associative-commutative function}
5.94 -
5.95 -\item The associative law must always be oriented from left to right,
5.96 - namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
5.97 - used with commutativity, can lead to nontermination.
5.98 -
5.99 -\item To complete your set of rewrite rules, you must add not just
5.100 - associativity~(A) and commutativity~(C) but also a derived rule, {\bf
5.101 - left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
5.102 -\end{itemize}
5.103 -Ordered rewriting with the combination of A, C, and LC sorts a term
5.104 -lexicographically:
5.105 -\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
5.106 - 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)) \]
5.107 -
5.108 -Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
5.109 -necessary because the built-in arithmetic prover often succeeds without
5.110 -such tricks.
5.111 -*}
5.112 -
5.113 -subsection{*How the Simplifier Works*}
5.114 -
5.115 -text{*\label{sec:SimpHow}
5.116 -Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
5.117 -first. A conditional equation is only applied if its condition can be
5.118 -proved, again by simplification. Below we explain some special features of
5.119 -the rewriting process.
5.120 -*}
5.121 -
5.122 -subsubsection{*Higher-Order Patterns*}
5.123 -
5.124 -text{*\index{simplification rule|(}
5.125 -So far we have pretended the simplifier can deal with arbitrary
5.126 -rewrite rules. This is not quite true. For reasons of feasibility,
5.127 -the simplifier expects the
5.128 -left-hand side of each rule to be a so-called \emph{higher-order
5.129 -pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
5.130 -This restricts where
5.131 -unknowns may occur. Higher-order patterns are terms in $\beta$-normal
5.132 -form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
5.133 -Each occurrence of an unknown is of the form
5.134 -$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
5.135 -variables. Thus all ordinary rewrite rules, where all unknowns are
5.136 -of base type, for example @{thm add_assoc}, are acceptable: if an unknown is
5.137 -of base type, it cannot have any arguments. Additionally, the rule
5.138 -@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in
5.139 -both directions: all arguments of the unknowns @{text"?P"} and
5.140 -@{text"?Q"} are distinct bound variables.
5.141 -
5.142 -If the left-hand side is not a higher-order pattern, all is not lost.
5.143 -The simplifier will still try to apply the rule provided it
5.144 -matches directly: without much $\lambda$-calculus hocus
5.145 -pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
5.146 -@{term"g a \<in> range g"} to @{const True}, but will fail to match
5.147 -@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can
5.148 -eliminate the offending subterms --- those that are not patterns ---
5.149 -by adding new variables and conditions.
5.150 -In our example, we eliminate @{text"?f ?x"} and obtain
5.151 - @{text"?y =
5.152 -?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine
5.153 -as a conditional rewrite rule since conditions can be arbitrary
5.154 -terms. However, this trick is not a panacea because the newly
5.155 -introduced conditions may be hard to solve.
5.156 -
5.157 -There is no restriction on the form of the right-hand
5.158 -sides. They may not contain extraneous term or type variables, though.
5.159 -*}
5.160 -
5.161 -subsubsection{*The Preprocessor*}
5.162 -
5.163 -text{*\label{sec:simp-preprocessor}
5.164 -When a theorem is declared a simplification rule, it need not be a
5.165 -conditional equation already. The simplifier will turn it into a set of
5.166 -conditional equations automatically. For example, @{prop"f x =
5.167 -g x & h x = k x"} becomes the two separate
5.168 -simplification rules @{prop"f x = g x"} and @{prop"h x = k x"}. In
5.169 -general, the input theorem is converted as follows:
5.170 -\begin{eqnarray}
5.171 -\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
5.172 -P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
5.173 -P \land Q &\mapsto& P,\ Q \nonumber\\
5.174 -\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
5.175 -\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
5.176 -@{text "if"}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
5.177 - P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
5.178 -\end{eqnarray}
5.179 -Once this conversion process is finished, all remaining non-equations
5.180 -$P$ are turned into trivial equations $P =\isa{True}$.
5.181 -For example, the formula
5.182 -\begin{center}@{prop"(p \<longrightarrow> t=u \<and> ~r) \<and> s"}\end{center}
5.183 -is converted into the three rules
5.184 -\begin{center}
5.185 -@{prop"p \<Longrightarrow> t = u"},\quad @{prop"p \<Longrightarrow> r = False"},\quad @{prop"s = True"}.
5.186 -\end{center}
5.187 -\index{simplification rule|)}
5.188 -\index{simplification|)}
5.189 -*}
5.190 -(*<*)
5.191 -end
5.192 -(*>*)
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/TutorialI/Advanced/simp2.thy Wed Jul 25 23:02:50 2012 +0200
6.3 @@ -0,0 +1,189 @@
6.4 +(*<*)
6.5 +theory simp2 imports Main begin
6.6 +(*>*)
6.7 +
6.8 +section{*Simplification*}
6.9 +
6.10 +text{*\label{sec:simplification-II}\index{simplification|(}
6.11 +This section describes features not covered until now. It also
6.12 +outlines the simplification process itself, which can be helpful
6.13 +when the simplifier does not do what you expect of it.
6.14 +*}
6.15 +
6.16 +subsection{*Advanced Features*}
6.17 +
6.18 +subsubsection{*Congruence Rules*}
6.19 +
6.20 +text{*\label{sec:simp-cong}
6.21 +While simplifying the conclusion $Q$
6.22 +of $P \Imp Q$, it is legal to use the assumption $P$.
6.23 +For $\Imp$ this policy is hardwired, but
6.24 +contextual information can also be made available for other
6.25 +operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
6.26 +True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
6.27 +xs"}. The generation of contextual information during simplification is
6.28 +controlled by so-called \bfindex{congruence rules}. This is the one for
6.29 +@{text"\<longrightarrow>"}:
6.30 +@{thm[display]imp_cong[no_vars]}
6.31 +It should be read as follows:
6.32 +In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
6.33 +simplify @{prop P} to @{prop P'}
6.34 +and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
6.35 +
6.36 +Here are some more examples. The congruence rules for bounded
6.37 +quantifiers supply contextual information about the bound variable:
6.38 +@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
6.39 +One congruence rule for conditional expressions supplies contextual
6.40 +information for simplifying the @{text then} and @{text else} cases:
6.41 +@{thm[display]if_cong[no_vars]}
6.42 +An alternative congruence rule for conditional expressions
6.43 +actually \emph{prevents} simplification of some arguments:
6.44 +@{thm[display]if_weak_cong[no_vars]}
6.45 +Only the first argument is simplified; the others remain unchanged.
6.46 +This makes simplification much faster and is faithful to the evaluation
6.47 +strategy in programming languages, which is why this is the default
6.48 +congruence rule for @{text "if"}. Analogous rules control the evaluation of
6.49 +@{text case} expressions.
6.50 +
6.51 +You can declare your own congruence rules with the attribute \attrdx{cong},
6.52 +either globally, in the usual manner,
6.53 +\begin{quote}
6.54 +\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
6.55 +\end{quote}
6.56 +or locally in a @{text"simp"} call by adding the modifier
6.57 +\begin{quote}
6.58 +@{text"cong:"} \textit{list of theorem names}
6.59 +\end{quote}
6.60 +The effect is reversed by @{text"cong del"} instead of @{text cong}.
6.61 +
6.62 +\begin{warn}
6.63 +The congruence rule @{thm[source]conj_cong}
6.64 +@{thm[display]conj_cong[no_vars]}
6.65 +\par\noindent
6.66 +is occasionally useful but is not a default rule; you have to declare it explicitly.
6.67 +\end{warn}
6.68 +*}
6.69 +
6.70 +subsubsection{*Permutative Rewrite Rules*}
6.71 +
6.72 +text{*
6.73 +\index{rewrite rules!permutative|bold}%
6.74 +An equation is a \textbf{permutative rewrite rule} if the left-hand
6.75 +side and right-hand side are the same up to renaming of variables. The most
6.76 +common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples
6.77 +include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
6.78 +y A) = insert y (insert x A)"} for sets. Such rules are problematic because
6.79 +once they apply, they can be used forever. The simplifier is aware of this
6.80 +danger and treats permutative rules by means of a special strategy, called
6.81 +\bfindex{ordered rewriting}: a permutative rewrite
6.82 +rule is only applied if the term becomes smaller with respect to a fixed
6.83 +lexicographic ordering on terms. For example, commutativity rewrites
6.84 +@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
6.85 +smaller than @{term"b+a"}. Permutative rewrite rules can be turned into
6.86 +simplification rules in the usual manner via the @{text simp} attribute; the
6.87 +simplifier recognizes their special status automatically.
6.88 +
6.89 +Permutative rewrite rules are most effective in the case of
6.90 +associative-commutative functions. (Associativity by itself is not
6.91 +permutative.) When dealing with an AC-function~$f$, keep the
6.92 +following points in mind:
6.93 +\begin{itemize}\index{associative-commutative function}
6.94 +
6.95 +\item The associative law must always be oriented from left to right,
6.96 + namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
6.97 + used with commutativity, can lead to nontermination.
6.98 +
6.99 +\item To complete your set of rewrite rules, you must add not just
6.100 + associativity~(A) and commutativity~(C) but also a derived rule, {\bf
6.101 + left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
6.102 +\end{itemize}
6.103 +Ordered rewriting with the combination of A, C, and LC sorts a term
6.104 +lexicographically:
6.105 +\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
6.106 + 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)) \]
6.107 +
6.108 +Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
6.109 +necessary because the built-in arithmetic prover often succeeds without
6.110 +such tricks.
6.111 +*}
6.112 +
6.113 +subsection{*How the Simplifier Works*}
6.114 +
6.115 +text{*\label{sec:SimpHow}
6.116 +Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
6.117 +first. A conditional equation is only applied if its condition can be
6.118 +proved, again by simplification. Below we explain some special features of
6.119 +the rewriting process.
6.120 +*}
6.121 +
6.122 +subsubsection{*Higher-Order Patterns*}
6.123 +
6.124 +text{*\index{simplification rule|(}
6.125 +So far we have pretended the simplifier can deal with arbitrary
6.126 +rewrite rules. This is not quite true. For reasons of feasibility,
6.127 +the simplifier expects the
6.128 +left-hand side of each rule to be a so-called \emph{higher-order
6.129 +pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
6.130 +This restricts where
6.131 +unknowns may occur. Higher-order patterns are terms in $\beta$-normal
6.132 +form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
6.133 +Each occurrence of an unknown is of the form
6.134 +$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
6.135 +variables. Thus all ordinary rewrite rules, where all unknowns are
6.136 +of base type, for example @{thm add_assoc}, are acceptable: if an unknown is
6.137 +of base type, it cannot have any arguments. Additionally, the rule
6.138 +@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in
6.139 +both directions: all arguments of the unknowns @{text"?P"} and
6.140 +@{text"?Q"} are distinct bound variables.
6.141 +
6.142 +If the left-hand side is not a higher-order pattern, all is not lost.
6.143 +The simplifier will still try to apply the rule provided it
6.144 +matches directly: without much $\lambda$-calculus hocus
6.145 +pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
6.146 +@{term"g a \<in> range g"} to @{const True}, but will fail to match
6.147 +@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can
6.148 +eliminate the offending subterms --- those that are not patterns ---
6.149 +by adding new variables and conditions.
6.150 +In our example, we eliminate @{text"?f ?x"} and obtain
6.151 + @{text"?y =
6.152 +?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine
6.153 +as a conditional rewrite rule since conditions can be arbitrary
6.154 +terms. However, this trick is not a panacea because the newly
6.155 +introduced conditions may be hard to solve.
6.156 +
6.157 +There is no restriction on the form of the right-hand
6.158 +sides. They may not contain extraneous term or type variables, though.
6.159 +*}
6.160 +
6.161 +subsubsection{*The Preprocessor*}
6.162 +
6.163 +text{*\label{sec:simp-preprocessor}
6.164 +When a theorem is declared a simplification rule, it need not be a
6.165 +conditional equation already. The simplifier will turn it into a set of
6.166 +conditional equations automatically. For example, @{prop"f x =
6.167 +g x & h x = k x"} becomes the two separate
6.168 +simplification rules @{prop"f x = g x"} and @{prop"h x = k x"}. In
6.169 +general, the input theorem is converted as follows:
6.170 +\begin{eqnarray}
6.171 +\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
6.172 +P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
6.173 +P \land Q &\mapsto& P,\ Q \nonumber\\
6.174 +\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
6.175 +\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
6.176 +@{text "if"}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
6.177 + P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
6.178 +\end{eqnarray}
6.179 +Once this conversion process is finished, all remaining non-equations
6.180 +$P$ are turned into trivial equations $P =\isa{True}$.
6.181 +For example, the formula
6.182 +\begin{center}@{prop"(p \<longrightarrow> t=u \<and> ~r) \<and> s"}\end{center}
6.183 +is converted into the three rules
6.184 +\begin{center}
6.185 +@{prop"p \<Longrightarrow> t = u"},\quad @{prop"p \<Longrightarrow> r = False"},\quad @{prop"s = True"}.
6.186 +\end{center}
6.187 +\index{simplification rule|)}
6.188 +\index{simplification|)}
6.189 +*}
6.190 +(*<*)
6.191 +end
6.192 +(*>*)
7.1 --- a/doc-src/TutorialI/IsaMakefile Wed Jul 25 22:30:18 2012 +0200
7.2 +++ b/doc-src/TutorialI/IsaMakefile Wed Jul 25 23:02:50 2012 +0200
7.3 @@ -121,7 +121,7 @@
7.4
7.5 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
7.6
7.7 -$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
7.8 +$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp2.thy Advanced/ROOT.ML
7.9 $(USEDIR) Advanced
7.10 @rm -f Advanced/document/isabelle.sty
7.11 @rm -f Advanced/document/isabellesym.sty