43 This makes simplification much faster and is faithful to the evaluation |
43 This makes simplification much faster and is faithful to the evaluation |
44 strategy in programming languages, which is why this is the default |
44 strategy in programming languages, which is why this is the default |
45 congruence rule for @{text if}. Analogous rules control the evaluaton of |
45 congruence rule for @{text if}. Analogous rules control the evaluaton of |
46 @{text case} expressions. |
46 @{text case} expressions. |
47 |
47 |
48 You can delare your own congruence rules with the attribute @{text cong}, |
48 You can declare your own congruence rules with the attribute @{text cong}, |
49 either globally, in the usual manner, |
49 either globally, in the usual manner, |
50 \begin{quote} |
50 \begin{quote} |
51 \isacommand{declare} \textit{theorem-name} @{text"[cong]"} |
51 \isacommand{declare} \textit{theorem-name} @{text"[cong]"} |
52 \end{quote} |
52 \end{quote} |
53 or locally in a @{text"simp"} call by adding the modifier |
53 or locally in a @{text"simp"} call by adding the modifier |
103 lexicographically: |
104 lexicographically: |
104 \[\def\maps#1{~\stackrel{#1}{\leadsto}~} |
105 \[\def\maps#1{~\stackrel{#1}{\leadsto}~} |
105 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)) \] |
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)) \] |
106 |
107 |
107 Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely |
108 Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely |
108 necessary because the builtin arithmetic capabilities often take care of |
109 necessary because the built-in arithmetic prover often succeeds without |
109 this. |
110 such hints. |
110 *} |
111 *} |
111 |
112 |
112 subsection{*How it works*} |
113 subsection{*How It Works*} |
113 |
114 |
114 text{*\label{sec:SimpHow} |
115 text{*\label{sec:SimpHow} |
115 Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified |
116 Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified |
116 first) and a conditional equation is only applied if its condition could be |
117 first) and a conditional equation is only applied if its condition could be |
117 proved (again by simplification). Below we explain some special features of the rewriting process. |
118 proved (again by simplification). Below we explain some special features of the rewriting process. |
118 *} |
119 *} |
119 |
120 |
120 subsubsection{*Higher-order patterns*} |
121 subsubsection{*Higher-Order Patterns*} |
121 |
122 |
122 text{*\index{simplification rule|(} |
123 text{*\index{simplification rule|(} |
123 So far we have pretended the simplifier can deal with arbitrary |
124 So far we have pretended the simplifier can deal with arbitrary |
124 rewrite rules. This is not quite true. Due to efficiency (and |
125 rewrite rules. This is not quite true. Due to efficiency (and |
125 potentially also computability) reasons, the simplifier expects the |
126 potentially also computability) reasons, the simplifier expects the |
137 both directions: all arguments of the unknowns @{text"?P"} and |
138 both directions: all arguments of the unknowns @{text"?P"} and |
138 @{text"?Q"} are distinct bound variables. |
139 @{text"?Q"} are distinct bound variables. |
139 |
140 |
140 If the left-hand side is not a higher-order pattern, not all is lost |
141 If the left-hand side is not a higher-order pattern, not all is lost |
141 and the simplifier will still try to apply the rule, but only if it |
142 and the simplifier will still try to apply the rule, but only if it |
142 matches ``directly'', i.e.\ without much $\lambda$-calculus hocus |
143 matches \emph{directly}, i.e.\ without much $\lambda$-calculus hocus |
143 pocus. For example, @{text"?f ?x \<in> range ?f = True"} rewrites |
144 pocus. For example, @{text"?f ?x \<in> range ?f = True"} rewrites |
144 @{term"g a \<in> range g"} to @{term True}, but will fail to match |
145 @{term"g a \<in> range g"} to @{term True}, but will fail to match |
145 @{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can |
146 @{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can |
146 replace the offending subterms (in our case @{text"?f ?x"}, which |
147 replace the offending subterms (in our case @{text"?f ?x"}, which |
147 is not a pattern) by adding new variables and conditions: @{text"?y = |
148 is not a pattern) by adding new variables and conditions: @{text"?y = |
148 ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is fine |
149 ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is fine |
149 as a conditional rewrite rule since conditions can be arbitrary |
150 as a conditional rewrite rule since conditions can be arbitrary |
150 terms. However, this trick is not a panacea because the newly |
151 terms. However, this trick is not a panacea because the newly |
151 introduced conditions may be hard to prove, which has to take place |
152 introduced conditions may be hard to prove, as they must be |
152 before the rule can actually be applied. |
153 before the rule can actually be applied. |
153 |
154 |
154 There is basically no restriction on the form of the right-hand |
155 There is no restriction on the form of the right-hand |
155 sides. They may not contain extraneous term or type variables, though. |
156 sides. They may not contain extraneous term or type variables, though. |
156 *} |
157 *} |
157 |
158 |
158 subsubsection{*The preprocessor*} |
159 subsubsection{*The Preprocessor*} |
159 |
160 |
160 text{*\label{sec:simp-preprocessor} |
161 text{*\label{sec:simp-preprocessor} |
161 When some theorem is declared a simplification rule, it need not be a |
162 When a theorem is declared a simplification rule, it need not be a |
162 conditional equation already. The simplifier will turn it into a set of |
163 conditional equation already. The simplifier will turn it into a set of |
163 conditional equations automatically. For example, given @{prop"f x = |
164 conditional equations automatically. For example, @{prop"f x = |
164 g x & h x = k x"} the simplifier will turn this into the two separate |
165 g x & h x = k x"} becomes the two separate |
165 simplifiction rules @{prop"f x = g x"} and @{prop"h x = k x"}. In |
166 simplification rules @{prop"f x = g x"} and @{prop"h x = k x"}. In |
166 general, the input theorem is converted as follows: |
167 general, the input theorem is converted as follows: |
167 \begin{eqnarray} |
168 \begin{eqnarray} |
168 \neg P &\mapsto& P = False \nonumber\\ |
169 \neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\ |
169 P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\ |
170 P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\ |
170 P \land Q &\mapsto& P,\ Q \nonumber\\ |
171 P \land Q &\mapsto& P,\ Q \nonumber\\ |
171 \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\ |
172 \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\ |
172 \forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\ |
173 \forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\ |
173 @{text if}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto& |
174 @{text if}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto& |
174 P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber |
175 P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber |
175 \end{eqnarray} |
176 \end{eqnarray} |
176 Once this conversion process is finished, all remaining non-equations |
177 Once this conversion process is finished, all remaining non-equations |
177 $P$ are turned into trivial equations $P = True$. |
178 $P$ are turned into trivial equations $P =\isa{True}$. |
178 For example, the formula \begin{center}@{prop"(p \<longrightarrow> q \<and> r) \<and> s"}\end{center} |
179 For example, the formula |
|
180 \begin{center}@{prop"(p \<longrightarrow> t=u \<and> ~r) \<and> s"}\end{center} |
179 is converted into the three rules |
181 is converted into the three rules |
180 \begin{center} |
182 \begin{center} |
181 @{prop"p \<Longrightarrow> q = True"},\quad @{prop"p \<Longrightarrow> r = True"},\quad @{prop"s = True"}. |
183 @{prop"p \<Longrightarrow> t = u"},\quad @{prop"p \<Longrightarrow> r = False"},\quad @{prop"s = True"}. |
182 \end{center} |
184 \end{center} |
183 \index{simplification rule|)} |
185 \index{simplification rule|)} |
184 \index{simplification|)} |
186 \index{simplification|)} |
185 *} |
187 *} |
186 (*<*) |
188 (*<*) |