111 |
111 |
112 In case of a subterm of the form \isa{split\ f\ p} this is easy: the split |
112 In case of a subterm of the form \isa{split\ f\ p} this is easy: the split |
113 rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:% |
113 rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:% |
114 \index{*split (method)}% |
114 \index{*split (method)}% |
115 \end{isamarkuptext}% |
115 \end{isamarkuptext}% |
116 \isamarkupfalse% |
116 \isamarkuptrue% |
117 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline |
117 \isacommand{lemma}\isamarkupfalse% |
118 % |
118 \ {\isachardoublequoteopen}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequoteclose}\isanewline |
119 \isadelimproof |
119 % |
120 % |
120 \isadelimproof |
121 \endisadelimproof |
121 % |
122 % |
122 \endisadelimproof |
123 \isatagproof |
123 % |
124 \isamarkupfalse% |
124 \isatagproof |
125 \isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}\isamarkuptrue% |
125 \isacommand{apply}\isamarkupfalse% |
126 % |
126 {\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}% |
127 \begin{isamarkuptxt}% |
127 \begin{isamarkuptxt}% |
128 \begin{isabelle}% |
128 \begin{isabelle}% |
129 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p% |
129 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p% |
130 \end{isabelle} |
130 \end{isabelle} |
131 This subgoal is easily proved by simplification. Thus we could have combined |
131 This subgoal is easily proved by simplification. Thus we could have combined |
132 simplification and splitting in one command that proves the goal outright:% |
132 simplification and splitting in one command that proves the goal outright:% |
133 \end{isamarkuptxt}% |
133 \end{isamarkuptxt}% |
134 % |
134 \isamarkuptrue% |
135 \endisatagproof |
135 \isamarkupfalse% |
136 {\isafoldproof}% |
136 % |
137 % |
137 \endisatagproof |
138 \isadelimproof |
138 {\isafoldproof}% |
139 % |
139 % |
140 \endisadelimproof |
140 \isadelimproof |
141 % |
141 % |
142 \isadelimproof |
142 \endisadelimproof |
143 % |
143 \isamarkupfalse% |
144 \endisadelimproof |
144 % |
145 % |
145 \isadelimproof |
146 \isatagproof |
146 % |
147 \isamarkupfalse% |
147 \endisadelimproof |
148 \isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}% |
148 % |
149 \endisatagproof |
149 \isatagproof |
150 {\isafoldproof}% |
150 \isacommand{by}\isamarkupfalse% |
151 % |
151 {\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}% |
152 \isadelimproof |
152 \endisatagproof |
153 % |
153 {\isafoldproof}% |
154 \endisadelimproof |
154 % |
155 \isamarkuptrue% |
155 \isadelimproof |
|
156 % |
|
157 \endisadelimproof |
156 % |
158 % |
157 \begin{isamarkuptext}% |
159 \begin{isamarkuptext}% |
158 Let us look at a second example:% |
160 Let us look at a second example:% |
159 \end{isamarkuptext}% |
161 \end{isamarkuptext}% |
160 \isamarkupfalse% |
162 \isamarkuptrue% |
161 \isacommand{lemma}\ {\isachardoublequote}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
163 \isacommand{lemma}\isamarkupfalse% |
162 % |
164 \ {\isachardoublequoteopen}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
163 \isadelimproof |
165 % |
164 % |
166 \isadelimproof |
165 \endisadelimproof |
167 % |
166 % |
168 \endisadelimproof |
167 \isatagproof |
169 % |
168 \isamarkupfalse% |
170 \isatagproof |
169 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isamarkuptrue% |
171 \isacommand{apply}\isamarkupfalse% |
170 % |
172 {\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
171 \begin{isamarkuptxt}% |
173 \begin{isamarkuptxt}% |
172 \begin{isabelle}% |
174 \begin{isabelle}% |
173 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p% |
175 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p% |
174 \end{isabelle} |
176 \end{isabelle} |
175 A paired \isa{let} reduces to a paired $\lambda$-abstraction, which |
177 A paired \isa{let} reduces to a paired $\lambda$-abstraction, which |
176 can be split as above. The same is true for paired set comprehension:% |
178 can be split as above. The same is true for paired set comprehension:% |
177 \end{isamarkuptxt}% |
179 \end{isamarkuptxt}% |
178 % |
180 \isamarkuptrue% |
179 \endisatagproof |
181 \isamarkupfalse% |
180 {\isafoldproof}% |
182 % |
181 % |
183 \endisatagproof |
182 \isadelimproof |
184 {\isafoldproof}% |
183 % |
185 % |
184 \endisadelimproof |
186 \isadelimproof |
185 \isamarkupfalse% |
187 % |
186 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline |
188 \endisadelimproof |
187 % |
189 \isacommand{lemma}\isamarkupfalse% |
188 \isadelimproof |
190 \ {\isachardoublequoteopen}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequoteclose}\isanewline |
189 % |
191 % |
190 \endisadelimproof |
192 \isadelimproof |
191 % |
193 % |
192 \isatagproof |
194 \endisadelimproof |
193 \isamarkupfalse% |
195 % |
194 \isacommand{apply}\ simp\isamarkuptrue% |
196 \isatagproof |
195 % |
197 \isacommand{apply}\isamarkupfalse% |
|
198 \ simp% |
196 \begin{isamarkuptxt}% |
199 \begin{isamarkuptxt}% |
197 \begin{isabelle}% |
200 \begin{isabelle}% |
198 \ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% |
201 \ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% |
199 \end{isabelle} |
202 \end{isabelle} |
200 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split} |
203 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split} |
201 as above. If you are worried about the strange form of the premise: |
204 as above. If you are worried about the strange form of the premise: |
202 \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}. |
205 \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}. |
203 The same proof procedure works for% |
206 The same proof procedure works for% |
204 \end{isamarkuptxt}% |
207 \end{isamarkuptxt}% |
205 % |
208 \isamarkuptrue% |
206 \endisatagproof |
209 \isamarkupfalse% |
207 {\isafoldproof}% |
210 % |
208 % |
211 \endisatagproof |
209 \isadelimproof |
212 {\isafoldproof}% |
210 % |
213 % |
211 \endisadelimproof |
214 \isadelimproof |
212 \isamarkupfalse% |
215 % |
213 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}% |
216 \endisadelimproof |
214 \isadelimproof |
217 \isacommand{lemma}\isamarkupfalse% |
215 % |
218 \ {\isachardoublequoteopen}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequoteclose}% |
216 \endisadelimproof |
219 \isadelimproof |
217 % |
220 % |
218 \isatagproof |
221 \endisadelimproof |
219 \isamarkuptrue% |
222 % |
|
223 \isatagproof |
220 % |
224 % |
221 \begin{isamarkuptxt}% |
225 \begin{isamarkuptxt}% |
222 \noindent |
226 \noindent |
223 except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because |
227 except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because |
224 \isa{split} occurs in the assumptions. |
228 \isa{split} occurs in the assumptions. |
225 |
229 |
226 However, splitting \isa{split} is not always a solution, as no \isa{split} |
230 However, splitting \isa{split} is not always a solution, as no \isa{split} |
227 may be present in the goal. Consider the following function:% |
231 may be present in the goal. Consider the following function:% |
228 \end{isamarkuptxt}% |
232 \end{isamarkuptxt}% |
229 % |
233 \isamarkuptrue% |
230 \endisatagproof |
234 \isamarkupfalse% |
231 {\isafoldproof}% |
235 % |
232 % |
236 \endisatagproof |
233 \isadelimproof |
237 {\isafoldproof}% |
234 % |
238 % |
235 \endisadelimproof |
239 \isadelimproof |
236 \isamarkupfalse% |
240 % |
237 \isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline |
241 \endisadelimproof |
238 \isamarkupfalse% |
242 \isacommand{consts}\isamarkupfalse% |
239 \isacommand{primrec}\isanewline |
243 \ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline |
240 \ \ {\isachardoublequote}swap\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
244 \isacommand{primrec}\isamarkupfalse% |
241 % |
245 \isanewline |
|
246 \ \ {\isachardoublequoteopen}swap\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardoublequoteclose}% |
242 \begin{isamarkuptext}% |
247 \begin{isamarkuptext}% |
243 \noindent |
248 \noindent |
244 Note that the above \isacommand{primrec} definition is admissible |
249 Note that the above \isacommand{primrec} definition is admissible |
245 because \isa{{\isasymtimes}} is a datatype. When we now try to prove% |
250 because \isa{{\isasymtimes}} is a datatype. When we now try to prove% |
246 \end{isamarkuptext}% |
251 \end{isamarkuptext}% |
247 \isamarkupfalse% |
252 \isamarkuptrue% |
248 \isacommand{lemma}\ {\isachardoublequote}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequote}% |
253 \isacommand{lemma}\isamarkupfalse% |
249 \isadelimproof |
254 \ {\isachardoublequoteopen}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequoteclose}% |
250 % |
255 \isadelimproof |
251 \endisadelimproof |
256 % |
252 % |
257 \endisadelimproof |
253 \isatagproof |
258 % |
254 \isamarkuptrue% |
259 \isatagproof |
255 % |
260 % |
256 \begin{isamarkuptxt}% |
261 \begin{isamarkuptxt}% |
257 \noindent |
262 \noindent |
258 simplification will do nothing, because the defining equation for \isa{Pairs{\isachardot}swap} |
263 simplification will do nothing, because the defining equation for \isa{Pairs{\isachardot}swap} |
259 expects a pair. Again, we need to turn \isa{p} into a pair first, but this |
264 expects a pair. Again, we need to turn \isa{p} into a pair first, but this |
260 time there is no \isa{split} in sight. In this case the only thing we can do |
265 time there is no \isa{split} in sight. In this case the only thing we can do |
261 is to split the term by hand:% |
266 is to split the term by hand:% |
262 \end{isamarkuptxt}% |
267 \end{isamarkuptxt}% |
263 \isamarkupfalse% |
268 \isamarkuptrue% |
264 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ p{\isacharparenright}\isamarkuptrue% |
269 \isacommand{apply}\isamarkupfalse% |
265 % |
270 {\isacharparenleft}case{\isacharunderscore}tac\ p{\isacharparenright}% |
266 \begin{isamarkuptxt}% |
271 \begin{isamarkuptxt}% |
267 \noindent |
272 \noindent |
268 \begin{isabelle}% |
273 \begin{isabelle}% |
269 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ p{\isacharparenright}\ {\isacharequal}\ p% |
274 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ p{\isacharparenright}\ {\isacharequal}\ p% |
270 \end{isabelle} |
275 \end{isabelle} |
277 |
282 |
278 In case the term to be split is a quantified variable, there are more options. |
283 In case the term to be split is a quantified variable, there are more options. |
279 You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal |
284 You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal |
280 with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:% |
285 with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:% |
281 \end{isamarkuptxt}% |
286 \end{isamarkuptxt}% |
282 % |
287 \isamarkuptrue% |
283 \endisatagproof |
288 \isamarkupfalse% |
284 {\isafoldproof}% |
289 % |
285 % |
290 \endisatagproof |
286 \isadelimproof |
291 {\isafoldproof}% |
287 % |
292 % |
288 \endisadelimproof |
293 \isadelimproof |
289 \isamarkupfalse% |
294 % |
290 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline |
295 \endisadelimproof |
291 % |
296 \isacommand{lemma}\isamarkupfalse% |
292 \isadelimproof |
297 \ {\isachardoublequoteopen}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequoteclose}\isanewline |
293 % |
298 % |
294 \endisadelimproof |
299 \isadelimproof |
295 % |
300 % |
296 \isatagproof |
301 \endisadelimproof |
297 \isamarkupfalse% |
302 % |
298 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkuptrue% |
303 \isatagproof |
299 % |
304 \isacommand{apply}\isamarkupfalse% |
|
305 {\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}% |
300 \begin{isamarkuptxt}% |
306 \begin{isamarkuptxt}% |
301 \noindent |
307 \noindent |
302 \begin{isabelle}% |
308 \begin{isabelle}% |
303 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline |
309 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline |
304 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\isanewline |
310 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\isanewline |
305 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}% |
311 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}% |
306 \end{isabelle}% |
312 \end{isabelle}% |
307 \end{isamarkuptxt}% |
313 \end{isamarkuptxt}% |
308 \isamarkupfalse% |
314 \isamarkuptrue% |
309 \isacommand{apply}\ simp\isanewline |
315 \isacommand{apply}\isamarkupfalse% |
310 \isamarkupfalse% |
316 \ simp\isanewline |
311 \isacommand{done}% |
317 \isacommand{done}\isamarkupfalse% |
312 \endisatagproof |
318 % |
313 {\isafoldproof}% |
319 \endisatagproof |
314 % |
320 {\isafoldproof}% |
315 \isadelimproof |
321 % |
316 % |
322 \isadelimproof |
317 \endisadelimproof |
323 % |
318 \isamarkuptrue% |
324 \endisadelimproof |
319 % |
325 % |
320 \begin{isamarkuptext}% |
326 \begin{isamarkuptext}% |
321 \noindent |
327 \noindent |
322 Note that we have intentionally included only \isa{split{\isacharunderscore}paired{\isacharunderscore}all} |
328 Note that we have intentionally included only \isa{split{\isacharunderscore}paired{\isacharunderscore}all} |
323 in the first simplification step, and then we simplify again. |
329 in the first simplification step, and then we simplify again. |
326 \isa{split{\isacharunderscore}paired{\isacharunderscore}all} may interfere with other functions |
332 \isa{split{\isacharunderscore}paired{\isacharunderscore}all} may interfere with other functions |
327 of the simplifier. |
333 of the simplifier. |
328 The following command could fail (here it does not) |
334 The following command could fail (here it does not) |
329 where two separate \isa{simp} applications succeed.% |
335 where two separate \isa{simp} applications succeed.% |
330 \end{isamarkuptext}% |
336 \end{isamarkuptext}% |
331 % |
337 \isamarkuptrue% |
332 \isadelimproof |
338 \isamarkupfalse% |
333 % |
339 % |
334 \endisadelimproof |
340 \isadelimproof |
335 % |
341 % |
336 \isatagproof |
342 \endisadelimproof |
337 \isamarkupfalse% |
343 % |
338 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}% |
344 \isatagproof |
339 \endisatagproof |
345 \isacommand{apply}\isamarkupfalse% |
340 {\isafoldproof}% |
346 {\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
341 % |
347 % |
342 \isadelimproof |
348 \endisatagproof |
343 % |
349 {\isafoldproof}% |
344 \endisadelimproof |
350 % |
345 \isamarkuptrue% |
351 \isadelimproof |
|
352 % |
|
353 \endisadelimproof |
346 % |
354 % |
347 \begin{isamarkuptext}% |
355 \begin{isamarkuptext}% |
348 \noindent |
356 \noindent |
349 Finally, the simplifier automatically splits all \isa{{\isasymforall}} and |
357 Finally, the simplifier automatically splits all \isa{{\isasymforall}} and |
350 \isa{{\isasymexists}}-quantified variables:% |
358 \isa{{\isasymexists}}-quantified variables:% |
351 \end{isamarkuptext}% |
359 \end{isamarkuptext}% |
352 \isamarkupfalse% |
360 \isamarkuptrue% |
353 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequote}\isanewline |
361 \isacommand{lemma}\isamarkupfalse% |
354 % |
362 \ {\isachardoublequoteopen}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequoteclose}\isanewline |
355 \isadelimproof |
363 % |
356 % |
364 \isadelimproof |
357 \endisadelimproof |
365 % |
358 % |
366 \endisadelimproof |
359 \isatagproof |
367 % |
360 \isamarkupfalse% |
368 \isatagproof |
361 \isacommand{by}\ simp% |
369 \isacommand{by}\isamarkupfalse% |
362 \endisatagproof |
370 \ simp% |
363 {\isafoldproof}% |
371 \endisatagproof |
364 % |
372 {\isafoldproof}% |
365 \isadelimproof |
373 % |
366 % |
374 \isadelimproof |
367 \endisadelimproof |
375 % |
368 \isamarkuptrue% |
376 \endisadelimproof |
369 % |
377 % |
370 \begin{isamarkuptext}% |
378 \begin{isamarkuptext}% |
371 \noindent |
379 \noindent |
372 To turn off this automatic splitting, just disable the |
380 To turn off this automatic splitting, just disable the |
373 responsible simplification rules: |
381 responsible simplification rules: |