1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{simp}% |
3 \def\isabellecontext{simp}% |
|
4 \isamarkupfalse% |
4 % |
5 % |
5 \isamarkupsection{Simplification% |
6 \isamarkupsection{Simplification% |
6 } |
7 } |
|
8 \isamarkuptrue% |
7 % |
9 % |
8 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
9 \label{sec:simplification-II}\index{simplification|(} |
11 \label{sec:simplification-II}\index{simplification|(} |
10 This section describes features not covered until now. It also |
12 This section describes features not covered until now. It also |
11 outlines the simplification process itself, which can be helpful |
13 outlines the simplification process itself, which can be helpful |
12 when the simplifier does not do what you expect of it.% |
14 when the simplifier does not do what you expect of it.% |
13 \end{isamarkuptext}% |
15 \end{isamarkuptext}% |
|
16 \isamarkuptrue% |
14 % |
17 % |
15 \isamarkupsubsection{Advanced Features% |
18 \isamarkupsubsection{Advanced Features% |
16 } |
19 } |
|
20 \isamarkuptrue% |
17 % |
21 % |
18 \isamarkupsubsubsection{Congruence Rules% |
22 \isamarkupsubsubsection{Congruence Rules% |
19 } |
23 } |
|
24 \isamarkuptrue% |
20 % |
25 % |
21 \begin{isamarkuptext}% |
26 \begin{isamarkuptext}% |
22 \label{sec:simp-cong} |
27 \label{sec:simp-cong} |
23 While simplifying the conclusion $Q$ |
28 While simplifying the conclusion $Q$ |
24 of $P \Imp Q$, it is legal use the assumption $P$. |
29 of $P \Imp Q$, it is legal use the assumption $P$. |
76 \end{isabelle} |
81 \end{isabelle} |
77 \par\noindent |
82 \par\noindent |
78 is occasionally useful but is not a default rule; you have to declare it explicitly. |
83 is occasionally useful but is not a default rule; you have to declare it explicitly. |
79 \end{warn}% |
84 \end{warn}% |
80 \end{isamarkuptext}% |
85 \end{isamarkuptext}% |
|
86 \isamarkuptrue% |
81 % |
87 % |
82 \isamarkupsubsubsection{Permutative Rewrite Rules% |
88 \isamarkupsubsubsection{Permutative Rewrite Rules% |
83 } |
89 } |
|
90 \isamarkuptrue% |
84 % |
91 % |
85 \begin{isamarkuptext}% |
92 \begin{isamarkuptext}% |
86 \index{rewrite rules!permutative|bold}% |
93 \index{rewrite rules!permutative|bold}% |
87 An equation is a \textbf{permutative rewrite rule} if the left-hand |
94 An equation is a \textbf{permutative rewrite rule} if the left-hand |
88 side and right-hand side are the same up to renaming of variables. The most |
95 side and right-hand side are the same up to renaming of variables. The most |
119 |
126 |
120 Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely |
127 Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely |
121 necessary because the built-in arithmetic prover often succeeds without |
128 necessary because the built-in arithmetic prover often succeeds without |
122 such tricks.% |
129 such tricks.% |
123 \end{isamarkuptext}% |
130 \end{isamarkuptext}% |
|
131 \isamarkuptrue% |
124 % |
132 % |
125 \isamarkupsubsection{How the Simplifier Works% |
133 \isamarkupsubsection{How the Simplifier Works% |
126 } |
134 } |
|
135 \isamarkuptrue% |
127 % |
136 % |
128 \begin{isamarkuptext}% |
137 \begin{isamarkuptext}% |
129 \label{sec:SimpHow} |
138 \label{sec:SimpHow} |
130 Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified |
139 Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified |
131 first. A conditional equation is only applied if its condition can be |
140 first. A conditional equation is only applied if its condition can be |
132 proved, again by simplification. Below we explain some special features of |
141 proved, again by simplification. Below we explain some special features of |
133 the rewriting process.% |
142 the rewriting process.% |
134 \end{isamarkuptext}% |
143 \end{isamarkuptext}% |
|
144 \isamarkuptrue% |
135 % |
145 % |
136 \isamarkupsubsubsection{Higher-Order Patterns% |
146 \isamarkupsubsubsection{Higher-Order Patterns% |
137 } |
147 } |
|
148 \isamarkuptrue% |
138 % |
149 % |
139 \begin{isamarkuptext}% |
150 \begin{isamarkuptext}% |
140 \index{simplification rule|(} |
151 \index{simplification rule|(} |
141 So far we have pretended the simplifier can deal with arbitrary |
152 So far we have pretended the simplifier can deal with arbitrary |
142 rewrite rules. This is not quite true. For reasons of feasibility, |
153 rewrite rules. This is not quite true. For reasons of feasibility, |
170 introduced conditions may be hard to solve. |
181 introduced conditions may be hard to solve. |
171 |
182 |
172 There is no restriction on the form of the right-hand |
183 There is no restriction on the form of the right-hand |
173 sides. They may not contain extraneous term or type variables, though.% |
184 sides. They may not contain extraneous term or type variables, though.% |
174 \end{isamarkuptext}% |
185 \end{isamarkuptext}% |
|
186 \isamarkuptrue% |
175 % |
187 % |
176 \isamarkupsubsubsection{The Preprocessor% |
188 \isamarkupsubsubsection{The Preprocessor% |
177 } |
189 } |
|
190 \isamarkuptrue% |
178 % |
191 % |
179 \begin{isamarkuptext}% |
192 \begin{isamarkuptext}% |
180 \label{sec:simp-preprocessor} |
193 \label{sec:simp-preprocessor} |
181 When a theorem is declared a simplification rule, it need not be a |
194 When a theorem is declared a simplification rule, it need not be a |
182 conditional equation already. The simplifier will turn it into a set of |
195 conditional equation already. The simplifier will turn it into a set of |
201 \isa{p\ {\isasymLongrightarrow}\ t\ {\isacharequal}\ u},\quad \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ False},\quad \isa{s\ {\isacharequal}\ True}. |
214 \isa{p\ {\isasymLongrightarrow}\ t\ {\isacharequal}\ u},\quad \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ False},\quad \isa{s\ {\isacharequal}\ True}. |
202 \end{center} |
215 \end{center} |
203 \index{simplification rule|)} |
216 \index{simplification rule|)} |
204 \index{simplification|)}% |
217 \index{simplification|)}% |
205 \end{isamarkuptext}% |
218 \end{isamarkuptext}% |
|
219 \isamarkuptrue% |
|
220 \isamarkupfalse% |
206 \end{isabellebody}% |
221 \end{isabellebody}% |
207 %%% Local Variables: |
222 %%% Local Variables: |
208 %%% mode: latex |
223 %%% mode: latex |
209 %%% TeX-master: "root" |
224 %%% TeX-master: "root" |
210 %%% End: |
225 %%% End: |