66 Isar implements the following principle: \begin{quote}\em Command |
66 Isar implements the following principle: \begin{quote}\em Command |
67 \isakeyword{proof} automatically tries to select an introduction rule |
67 \isakeyword{proof} automatically tries to select an introduction rule |
68 based on the goal and a predefined list of rules. \end{quote} Here |
68 based on the goal and a predefined list of rules. \end{quote} Here |
69 \isa{impI} is applied automatically:% |
69 \isa{impI} is applied automatically:% |
70 \end{isamarkuptext}% |
70 \end{isamarkuptext}% |
71 \isamarkupfalse% |
71 \isamarkuptrue% |
72 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline |
72 \isacommand{lemma}\isamarkupfalse% |
73 % |
73 \ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A{\isachardoublequoteclose}\isanewline |
74 \isadelimproof |
74 % |
75 % |
75 \isadelimproof |
76 \endisadelimproof |
76 % |
77 % |
77 \endisadelimproof |
78 \isatagproof |
78 % |
79 \isamarkupfalse% |
79 \isatagproof |
80 \isacommand{proof}\isanewline |
80 \isacommand{proof}\isamarkupfalse% |
81 \ \ \isamarkupfalse% |
81 \isanewline |
82 \isacommand{assume}\ a{\isacharcolon}\ A\isanewline |
82 \ \ \isacommand{assume}\isamarkupfalse% |
83 \ \ \isamarkupfalse% |
83 \ a{\isacharcolon}\ A\isanewline |
84 \isacommand{show}\ A\ \isamarkupfalse% |
84 \ \ \isacommand{show}\isamarkupfalse% |
85 \isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline |
85 \ A\ \isacommand{by}\isamarkupfalse% |
86 \isamarkupfalse% |
86 {\isacharparenleft}rule\ a{\isacharparenright}\isanewline |
87 \isacommand{qed}% |
87 \isacommand{qed}\isamarkupfalse% |
88 \endisatagproof |
88 % |
89 {\isafoldproof}% |
89 \endisatagproof |
90 % |
90 {\isafoldproof}% |
91 \isadelimproof |
91 % |
92 % |
92 \isadelimproof |
93 \endisadelimproof |
93 % |
94 \isamarkuptrue% |
94 \endisadelimproof |
95 % |
95 % |
96 \begin{isamarkuptext}% |
96 \begin{isamarkuptext}% |
97 \noindent Single-identifier formulae such as \isa{A} need not |
97 \noindent Single-identifier formulae such as \isa{A} need not |
98 be enclosed in double quotes. However, we will continue to do so for |
98 be enclosed in double quotes. However, we will continue to do so for |
99 uniformity. |
99 uniformity. |
100 |
100 |
101 Trivial proofs, in particular those by assumption, should be trivial |
101 Trivial proofs, in particular those by assumption, should be trivial |
102 to perform. Proof ``.'' does just that (and a bit more). Thus |
102 to perform. Proof ``.'' does just that (and a bit more). Thus |
103 naming of assumptions is often superfluous:% |
103 naming of assumptions is often superfluous:% |
104 \end{isamarkuptext}% |
104 \end{isamarkuptext}% |
105 \isamarkupfalse% |
105 \isamarkuptrue% |
106 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline |
106 \isacommand{lemma}\isamarkupfalse% |
107 % |
107 \ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A{\isachardoublequoteclose}\isanewline |
108 \isadelimproof |
108 % |
109 % |
109 \isadelimproof |
110 \endisadelimproof |
110 % |
111 % |
111 \endisadelimproof |
112 \isatagproof |
112 % |
113 \isamarkupfalse% |
113 \isatagproof |
114 \isacommand{proof}\isanewline |
114 \isacommand{proof}\isamarkupfalse% |
115 \ \ \isamarkupfalse% |
115 \isanewline |
116 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline |
116 \ \ \isacommand{assume}\isamarkupfalse% |
117 \ \ \isamarkupfalse% |
117 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline |
118 \isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% |
118 \ \ \isacommand{show}\isamarkupfalse% |
119 \isacommand{{\isachardot}}\isanewline |
119 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% |
120 \isamarkupfalse% |
120 \isanewline |
121 \isacommand{qed}% |
121 \isacommand{qed}\isamarkupfalse% |
122 \endisatagproof |
122 % |
123 {\isafoldproof}% |
123 \endisatagproof |
124 % |
124 {\isafoldproof}% |
125 \isadelimproof |
125 % |
126 % |
126 \isadelimproof |
127 \endisadelimproof |
127 % |
128 \isamarkuptrue% |
128 \endisadelimproof |
129 % |
129 % |
130 \begin{isamarkuptext}% |
130 \begin{isamarkuptext}% |
131 To hide proofs by assumption further, \isakeyword{by}\isa{{\isacharparenleft}method{\isacharparenright}} |
131 To hide proofs by assumption further, \isakeyword{by}\isa{{\isacharparenleft}method{\isacharparenright}} |
132 first applies \isa{method} and then tries to solve all remaining subgoals |
132 first applies \isa{method} and then tries to solve all remaining subgoals |
133 by assumption:% |
133 by assumption:% |
134 \end{isamarkuptext}% |
134 \end{isamarkuptext}% |
135 \isamarkupfalse% |
135 \isamarkuptrue% |
136 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline |
136 \isacommand{lemma}\isamarkupfalse% |
137 % |
137 \ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
138 \isadelimproof |
138 % |
139 % |
139 \isadelimproof |
140 \endisadelimproof |
140 % |
141 % |
141 \endisadelimproof |
142 \isatagproof |
142 % |
143 \isamarkupfalse% |
143 \isatagproof |
144 \isacommand{proof}\isanewline |
144 \isacommand{proof}\isamarkupfalse% |
145 \ \ \isamarkupfalse% |
145 \isanewline |
146 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline |
146 \ \ \isacommand{assume}\isamarkupfalse% |
147 \ \ \isamarkupfalse% |
147 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline |
148 \isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% |
148 \ \ \isacommand{show}\isamarkupfalse% |
149 \isacommand{by}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
149 \ {\isachardoublequoteopen}A\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
150 \isamarkupfalse% |
150 {\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
151 \isacommand{qed}% |
151 \isacommand{qed}\isamarkupfalse% |
152 \endisatagproof |
152 % |
153 {\isafoldproof}% |
153 \endisatagproof |
154 % |
154 {\isafoldproof}% |
155 \isadelimproof |
155 % |
156 % |
156 \isadelimproof |
157 \endisadelimproof |
157 % |
158 \isamarkuptrue% |
158 \endisadelimproof |
159 % |
159 % |
160 \begin{isamarkuptext}% |
160 \begin{isamarkuptext}% |
161 \noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. |
161 \noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. |
162 A drawback of implicit proofs by assumption is that it |
162 A drawback of implicit proofs by assumption is that it |
163 is no longer obvious where an assumption is used. |
163 is no longer obvious where an assumption is used. |
164 |
164 |
165 Proofs of the form \isakeyword{by}\isa{{\isacharparenleft}rule}~\emph{name}\isa{{\isacharparenright}} |
165 Proofs of the form \isakeyword{by}\isa{{\isacharparenleft}rule}~\emph{name}\isa{{\isacharparenright}} |
166 can be abbreviated to ``..'' if \emph{name} refers to one of the |
166 can be abbreviated to ``..'' if \emph{name} refers to one of the |
167 predefined introduction rules (or elimination rules, see below):% |
167 predefined introduction rules (or elimination rules, see below):% |
168 \end{isamarkuptext}% |
168 \end{isamarkuptext}% |
169 \isamarkupfalse% |
169 \isamarkuptrue% |
170 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline |
170 \isacommand{lemma}\isamarkupfalse% |
171 % |
171 \ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
172 \isadelimproof |
172 % |
173 % |
173 \isadelimproof |
174 \endisadelimproof |
174 % |
175 % |
175 \endisadelimproof |
176 \isatagproof |
176 % |
177 \isamarkupfalse% |
177 \isatagproof |
178 \isacommand{proof}\isanewline |
178 \isacommand{proof}\isamarkupfalse% |
179 \ \ \isamarkupfalse% |
179 \isanewline |
180 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline |
180 \ \ \isacommand{assume}\isamarkupfalse% |
181 \ \ \isamarkupfalse% |
181 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline |
182 \isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% |
182 \ \ \isacommand{show}\isamarkupfalse% |
183 \isacommand{{\isachardot}{\isachardot}}\isanewline |
183 \ {\isachardoublequoteopen}A\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
184 \isamarkupfalse% |
184 \isanewline |
185 \isacommand{qed}% |
185 \isacommand{qed}\isamarkupfalse% |
186 \endisatagproof |
186 % |
187 {\isafoldproof}% |
187 \endisatagproof |
188 % |
188 {\isafoldproof}% |
189 \isadelimproof |
189 % |
190 % |
190 \isadelimproof |
191 \endisadelimproof |
191 % |
192 \isamarkuptrue% |
192 \endisadelimproof |
193 % |
193 % |
194 \begin{isamarkuptext}% |
194 \begin{isamarkuptext}% |
195 \noindent |
195 \noindent |
196 This is what happens: first the matching introduction rule \isa{conjI} |
196 This is what happens: first the matching introduction rule \isa{conjI} |
197 is applied (first ``.''), then the two subgoals are solved by assumption |
197 is applied (first ``.''), then the two subgoals are solved by assumption |
209 \ \ \ \ \ {\isasymlbrakk}{\isacharquery}P\ {\isasymand}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R% |
209 \ \ \ \ \ {\isasymlbrakk}{\isacharquery}P\ {\isasymand}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R% |
210 \end{isabelle} In the following proof it is applied |
210 \end{isabelle} In the following proof it is applied |
211 by hand, after its first (\emph{major}) premise has been eliminated via |
211 by hand, after its first (\emph{major}) premise has been eliminated via |
212 \isa{{\isacharbrackleft}OF\ AB{\isacharbrackright}}:% |
212 \isa{{\isacharbrackleft}OF\ AB{\isacharbrackright}}:% |
213 \end{isamarkuptext}% |
213 \end{isamarkuptext}% |
214 \isamarkupfalse% |
214 \isamarkuptrue% |
215 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
215 \isacommand{lemma}\isamarkupfalse% |
216 % |
216 \ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
217 \isadelimproof |
217 % |
218 % |
218 \isadelimproof |
219 \endisadelimproof |
219 % |
220 % |
220 \endisadelimproof |
221 \isatagproof |
221 % |
222 \isamarkupfalse% |
222 \isatagproof |
223 \isacommand{proof}\isanewline |
223 \isacommand{proof}\isamarkupfalse% |
224 \ \ \isamarkupfalse% |
224 \isanewline |
225 \isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline |
225 \ \ \isacommand{assume}\isamarkupfalse% |
226 \ \ \isamarkupfalse% |
226 \ AB{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline |
227 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
227 \ \ \isacommand{show}\isamarkupfalse% |
228 \ \ \isamarkupfalse% |
228 \ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
229 \isacommand{proof}\ {\isacharparenleft}rule\ conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}{\isacharparenright}\ \ % |
229 \ \ \isacommand{proof}\isamarkupfalse% |
|
230 \ {\isacharparenleft}rule\ conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}{\isacharparenright}\ \ % |
230 \isamarkupcmt{\isa{conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}}: \isa{{\isacharparenleft}{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R}% |
231 \isamarkupcmt{\isa{conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}}: \isa{{\isacharparenleft}{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R}% |
231 } |
232 } |
232 \isanewline |
233 \isanewline |
233 \ \ \ \ \isamarkupfalse% |
234 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
234 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline |
235 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\isanewline |
235 \ \ \ \ \isamarkupfalse% |
236 \ \ \ \ \isacommand{show}\isamarkupfalse% |
236 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
237 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
237 \isacommand{{\isachardot}{\isachardot}}\isanewline |
238 \isanewline |
238 \ \ \isamarkupfalse% |
239 \ \ \isacommand{qed}\isamarkupfalse% |
239 \isacommand{qed}\isanewline |
240 \isanewline |
240 \isamarkupfalse% |
241 \isacommand{qed}\isamarkupfalse% |
241 \isacommand{qed}% |
242 % |
242 \endisatagproof |
243 \endisatagproof |
243 {\isafoldproof}% |
244 {\isafoldproof}% |
244 % |
245 % |
245 \isadelimproof |
246 \isadelimproof |
246 % |
247 % |
247 \endisadelimproof |
248 \endisadelimproof |
248 \isamarkuptrue% |
|
249 % |
249 % |
250 \begin{isamarkuptext}% |
250 \begin{isamarkuptext}% |
251 \noindent Note that the term \isa{{\isacharquery}thesis} always stands for the |
251 \noindent Note that the term \isa{{\isacharquery}thesis} always stands for the |
252 ``current goal'', i.e.\ the enclosing \isakeyword{show} (or |
252 ``current goal'', i.e.\ the enclosing \isakeyword{show} (or |
253 \isakeyword{have}) statement. |
253 \isakeyword{have}) statement. |
266 how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof}, |
266 how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof}, |
267 an elimination rule (from a predefined list) is applied |
267 an elimination rule (from a predefined list) is applied |
268 whose first premise is solved by the \emph{fact}. Thus the proof above |
268 whose first premise is solved by the \emph{fact}. Thus the proof above |
269 is equivalent to the following one:% |
269 is equivalent to the following one:% |
270 \end{isamarkuptext}% |
270 \end{isamarkuptext}% |
271 \isamarkupfalse% |
271 \isamarkuptrue% |
272 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
272 \isacommand{lemma}\isamarkupfalse% |
273 % |
273 \ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
274 \isadelimproof |
274 % |
275 % |
275 \isadelimproof |
276 \endisadelimproof |
276 % |
277 % |
277 \endisadelimproof |
278 \isatagproof |
278 % |
279 \isamarkupfalse% |
279 \isatagproof |
280 \isacommand{proof}\isanewline |
280 \isacommand{proof}\isamarkupfalse% |
281 \ \ \isamarkupfalse% |
281 \isanewline |
282 \isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline |
282 \ \ \isacommand{assume}\isamarkupfalse% |
283 \ \ \isamarkupfalse% |
283 \ AB{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline |
284 \isacommand{from}\ AB\ \isamarkupfalse% |
284 \ \ \isacommand{from}\isamarkupfalse% |
285 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
285 \ AB\ \isacommand{show}\isamarkupfalse% |
286 \ \ \isamarkupfalse% |
286 \ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
287 \isacommand{proof}\isanewline |
287 \ \ \isacommand{proof}\isamarkupfalse% |
288 \ \ \ \ \isamarkupfalse% |
288 \isanewline |
289 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline |
289 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
290 \ \ \ \ \isamarkupfalse% |
290 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\isanewline |
291 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
291 \ \ \ \ \isacommand{show}\isamarkupfalse% |
292 \isacommand{{\isachardot}{\isachardot}}\isanewline |
292 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
293 \ \ \isamarkupfalse% |
293 \isanewline |
294 \isacommand{qed}\isanewline |
294 \ \ \isacommand{qed}\isamarkupfalse% |
295 \isamarkupfalse% |
295 \isanewline |
296 \isacommand{qed}% |
296 \isacommand{qed}\isamarkupfalse% |
297 \endisatagproof |
297 % |
298 {\isafoldproof}% |
298 \endisatagproof |
299 % |
299 {\isafoldproof}% |
300 \isadelimproof |
300 % |
301 % |
301 \isadelimproof |
302 \endisadelimproof |
302 % |
303 \isamarkuptrue% |
303 \endisadelimproof |
304 % |
304 % |
305 \begin{isamarkuptext}% |
305 \begin{isamarkuptext}% |
306 Now we come to a second important principle: |
306 Now we come to a second important principle: |
307 \begin{quote}\em |
307 \begin{quote}\em |
308 Try to arrange the sequence of propositions in a UNIX-like pipe, |
308 Try to arrange the sequence of propositions in a UNIX-like pipe, |
309 such that the proof of each proposition builds on the previous proposition. |
309 such that the proof of each proposition builds on the previous proposition. |
310 \end{quote} |
310 \end{quote} |
311 The previous proposition can be referred to via the fact \isa{this}. |
311 The previous proposition can be referred to via the fact \isa{this}. |
312 This greatly reduces the need for explicit naming of propositions:% |
312 This greatly reduces the need for explicit naming of propositions:% |
313 \end{isamarkuptext}% |
313 \end{isamarkuptext}% |
314 \isamarkupfalse% |
314 \isamarkuptrue% |
315 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
315 \isacommand{lemma}\isamarkupfalse% |
316 % |
316 \ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
317 \isadelimproof |
317 % |
318 % |
318 \isadelimproof |
319 \endisadelimproof |
319 % |
320 % |
320 \endisadelimproof |
321 \isatagproof |
321 % |
322 \isamarkupfalse% |
322 \isatagproof |
323 \isacommand{proof}\isanewline |
323 \isacommand{proof}\isamarkupfalse% |
324 \ \ \isamarkupfalse% |
324 \isanewline |
325 \isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline |
325 \ \ \isacommand{assume}\isamarkupfalse% |
326 \ \ \isamarkupfalse% |
326 \ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline |
327 \isacommand{from}\ this\ \isamarkupfalse% |
327 \ \ \isacommand{from}\isamarkupfalse% |
328 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
328 \ this\ \isacommand{show}\isamarkupfalse% |
329 \ \ \isamarkupfalse% |
329 \ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
330 \isacommand{proof}\isanewline |
330 \ \ \isacommand{proof}\isamarkupfalse% |
331 \ \ \ \ \isamarkupfalse% |
331 \isanewline |
332 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline |
332 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
333 \ \ \ \ \isamarkupfalse% |
333 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\isanewline |
334 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
334 \ \ \ \ \isacommand{show}\isamarkupfalse% |
335 \isacommand{{\isachardot}{\isachardot}}\isanewline |
335 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
336 \ \ \isamarkupfalse% |
336 \isanewline |
337 \isacommand{qed}\isanewline |
337 \ \ \isacommand{qed}\isamarkupfalse% |
338 \isamarkupfalse% |
338 \isanewline |
339 \isacommand{qed}% |
339 \isacommand{qed}\isamarkupfalse% |
340 \endisatagproof |
340 % |
341 {\isafoldproof}% |
341 \endisatagproof |
342 % |
342 {\isafoldproof}% |
343 \isadelimproof |
343 % |
344 % |
344 \isadelimproof |
345 \endisadelimproof |
345 % |
346 \isamarkuptrue% |
346 \endisadelimproof |
347 % |
347 % |
348 \begin{isamarkuptext}% |
348 \begin{isamarkuptext}% |
349 \noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations: |
349 \noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations: |
350 \begin{center} |
350 \begin{center} |
351 \begin{tabular}{r@ {\quad=\quad}l} |
351 \begin{tabular}{r@ {\quad=\quad}l} |
354 \end{tabular} |
354 \end{tabular} |
355 \end{center} |
355 \end{center} |
356 |
356 |
357 Here is an alternative proof that operates purely by forward reasoning:% |
357 Here is an alternative proof that operates purely by forward reasoning:% |
358 \end{isamarkuptext}% |
358 \end{isamarkuptext}% |
359 \isamarkupfalse% |
359 \isamarkuptrue% |
360 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
360 \isacommand{lemma}\isamarkupfalse% |
361 % |
361 \ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
362 \isadelimproof |
362 % |
363 % |
363 \isadelimproof |
364 \endisadelimproof |
364 % |
365 % |
365 \endisadelimproof |
366 \isatagproof |
366 % |
367 \isamarkupfalse% |
367 \isatagproof |
368 \isacommand{proof}\isanewline |
368 \isacommand{proof}\isamarkupfalse% |
369 \ \ \isamarkupfalse% |
369 \isanewline |
370 \isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline |
370 \ \ \isacommand{assume}\isamarkupfalse% |
371 \ \ \isamarkupfalse% |
371 \ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline |
372 \isacommand{from}\ ab\ \isamarkupfalse% |
372 \ \ \isacommand{from}\isamarkupfalse% |
373 \isacommand{have}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% |
373 \ ab\ \isacommand{have}\isamarkupfalse% |
374 \isacommand{{\isachardot}{\isachardot}}\isanewline |
374 \ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
375 \ \ \isamarkupfalse% |
375 \isanewline |
376 \isacommand{from}\ ab\ \isamarkupfalse% |
376 \ \ \isacommand{from}\isamarkupfalse% |
377 \isacommand{have}\ b{\isacharcolon}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse% |
377 \ ab\ \isacommand{have}\isamarkupfalse% |
378 \isacommand{{\isachardot}{\isachardot}}\isanewline |
378 \ b{\isacharcolon}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
379 \ \ \isamarkupfalse% |
379 \isanewline |
380 \isacommand{from}\ b\ a\ \isamarkupfalse% |
380 \ \ \isacommand{from}\isamarkupfalse% |
381 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% |
381 \ b\ a\ \isacommand{show}\isamarkupfalse% |
382 \isacommand{{\isachardot}{\isachardot}}\isanewline |
382 \ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
383 \isamarkupfalse% |
383 \isanewline |
384 \isacommand{qed}% |
384 \isacommand{qed}\isamarkupfalse% |
385 \endisatagproof |
385 % |
386 {\isafoldproof}% |
386 \endisatagproof |
387 % |
387 {\isafoldproof}% |
388 \isadelimproof |
388 % |
389 % |
389 \isadelimproof |
390 \endisadelimproof |
390 % |
391 \isamarkuptrue% |
391 \endisadelimproof |
392 % |
392 % |
393 \begin{isamarkuptext}% |
393 \begin{isamarkuptext}% |
394 \noindent It is worth examining this text in detail because it |
394 \noindent It is worth examining this text in detail because it |
395 exhibits a number of new concepts. For a start, it is the first time |
395 exhibits a number of new concepts. For a start, it is the first time |
396 we have proved intermediate propositions (\isakeyword{have}) on the |
396 we have proved intermediate propositions (\isakeyword{have}) on the |
434 In the previous proof of \isa{A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A} we needed to feed |
434 In the previous proof of \isa{A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A} we needed to feed |
435 more than one fact into a proof step, a frequent situation. Then the |
435 more than one fact into a proof step, a frequent situation. Then the |
436 UNIX-pipe model appears to break down and we need to name the different |
436 UNIX-pipe model appears to break down and we need to name the different |
437 facts to refer to them. But this can be avoided:% |
437 facts to refer to them. But this can be avoided:% |
438 \end{isamarkuptext}% |
438 \end{isamarkuptext}% |
439 \isamarkupfalse% |
439 \isamarkuptrue% |
440 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
440 \isacommand{lemma}\isamarkupfalse% |
441 % |
441 \ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
442 \isadelimproof |
442 % |
443 % |
443 \isadelimproof |
444 \endisadelimproof |
444 % |
445 % |
445 \endisadelimproof |
446 \isatagproof |
446 % |
447 \isamarkupfalse% |
447 \isatagproof |
448 \isacommand{proof}\isanewline |
448 \isacommand{proof}\isamarkupfalse% |
449 \ \ \isamarkupfalse% |
449 \isanewline |
450 \isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline |
450 \ \ \isacommand{assume}\isamarkupfalse% |
451 \ \ \isamarkupfalse% |
451 \ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline |
452 \isacommand{from}\ ab\ \isamarkupfalse% |
452 \ \ \isacommand{from}\isamarkupfalse% |
453 \isacommand{have}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse% |
453 \ ab\ \isacommand{have}\isamarkupfalse% |
454 \isacommand{{\isachardot}{\isachardot}}\isanewline |
454 \ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
455 \ \ \isamarkupfalse% |
455 \isanewline |
456 \isacommand{moreover}\isanewline |
456 \ \ \isacommand{moreover}\isamarkupfalse% |
457 \ \ \isamarkupfalse% |
457 \isanewline |
458 \isacommand{from}\ ab\ \isamarkupfalse% |
458 \ \ \isacommand{from}\isamarkupfalse% |
459 \isacommand{have}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% |
459 \ ab\ \isacommand{have}\isamarkupfalse% |
460 \isacommand{{\isachardot}{\isachardot}}\isanewline |
460 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
461 \ \ \isamarkupfalse% |
461 \isanewline |
462 \isacommand{ultimately}\ \isamarkupfalse% |
462 \ \ \isacommand{ultimately}\isamarkupfalse% |
463 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% |
463 \ \isacommand{show}\isamarkupfalse% |
464 \isacommand{{\isachardot}{\isachardot}}\isanewline |
464 \ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
465 \isamarkupfalse% |
465 \isanewline |
466 \isacommand{qed}% |
466 \isacommand{qed}\isamarkupfalse% |
467 \endisatagproof |
467 % |
468 {\isafoldproof}% |
468 \endisatagproof |
469 % |
469 {\isafoldproof}% |
470 \isadelimproof |
470 % |
471 % |
471 \isadelimproof |
472 \endisadelimproof |
472 % |
473 \isamarkuptrue% |
473 \endisadelimproof |
474 % |
474 % |
475 \begin{isamarkuptext}% |
475 \begin{isamarkuptext}% |
476 \noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with |
476 \noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with |
477 \isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands |
477 \isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands |
478 for \isakeyword{from}~\isa{A{\isadigit{1}}}~\dots~\isa{An}. This avoids having to |
478 for \isakeyword{from}~\isa{A{\isadigit{1}}}~\dots~\isa{An}. This avoids having to |
484 Although we have only seen a few introduction and elimination rules so |
484 Although we have only seen a few introduction and elimination rules so |
485 far, Isar's predefined rules include all the usual natural deduction |
485 far, Isar's predefined rules include all the usual natural deduction |
486 rules. We conclude our exposition of propositional logic with an extended |
486 rules. We conclude our exposition of propositional logic with an extended |
487 example --- which rules are used implicitly where?% |
487 example --- which rules are used implicitly where?% |
488 \end{isamarkuptext}% |
488 \end{isamarkuptext}% |
489 \isamarkupfalse% |
489 \isamarkuptrue% |
490 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline |
490 \isacommand{lemma}\isamarkupfalse% |
491 % |
491 \ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\isanewline |
492 \isadelimproof |
492 % |
493 % |
493 \isadelimproof |
494 \endisadelimproof |
494 % |
495 % |
495 \endisadelimproof |
496 \isatagproof |
496 % |
497 \isamarkupfalse% |
497 \isatagproof |
498 \isacommand{proof}\isanewline |
498 \isacommand{proof}\isamarkupfalse% |
499 \ \ \isamarkupfalse% |
499 \isanewline |
500 \isacommand{assume}\ n{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline |
500 \ \ \isacommand{assume}\isamarkupfalse% |
501 \ \ \isamarkupfalse% |
501 \ n{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline |
502 \isacommand{show}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline |
502 \ \ \isacommand{show}\isamarkupfalse% |
503 \ \ \isamarkupfalse% |
503 \ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\isanewline |
504 \isacommand{proof}\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline |
504 \ \ \isacommand{proof}\isamarkupfalse% |
505 \ \ \ \ \isamarkupfalse% |
505 \ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline |
506 \isacommand{assume}\ nn{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isanewline |
506 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
507 \ \ \ \ \isamarkupfalse% |
507 \ nn{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline |
508 \isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline |
508 \ \ \ \ \isacommand{have}\isamarkupfalse% |
509 \ \ \ \ \isamarkupfalse% |
509 \ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\isanewline |
510 \isacommand{proof}\isanewline |
510 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
511 \ \ \ \ \ \ \isamarkupfalse% |
511 \isanewline |
512 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline |
512 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
513 \ \ \ \ \ \ \isamarkupfalse% |
513 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline |
514 \isacommand{have}\ {\isachardoublequote}{\isasymnot}\ B{\isachardoublequote}\isanewline |
514 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse% |
515 \ \ \ \ \ \ \isamarkupfalse% |
515 \ {\isachardoublequoteopen}{\isasymnot}\ B{\isachardoublequoteclose}\isanewline |
516 \isacommand{proof}\isanewline |
516 \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% |
517 \ \ \ \ \ \ \ \ \isamarkupfalse% |
517 \isanewline |
518 \isacommand{assume}\ {\isachardoublequote}B{\isachardoublequote}\isanewline |
518 \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
519 \ \ \ \ \ \ \ \ \isamarkupfalse% |
519 \ {\isachardoublequoteopen}B{\isachardoublequoteclose}\isanewline |
520 \isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse% |
520 \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse% |
521 \isacommand{{\isachardot}{\isachardot}}\isanewline |
521 \ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
522 \ \ \ \ \ \ \ \ \isamarkupfalse% |
522 \isanewline |
523 \isacommand{with}\ n\ \isamarkupfalse% |
523 \ \ \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
524 \isacommand{show}\ False\ \isamarkupfalse% |
524 \ n\ \isacommand{show}\isamarkupfalse% |
525 \isacommand{{\isachardot}{\isachardot}}\isanewline |
525 \ False\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
526 \ \ \ \ \ \ \isamarkupfalse% |
526 \isanewline |
527 \isacommand{qed}\isanewline |
527 \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% |
528 \ \ \ \ \ \ \isamarkupfalse% |
528 \isanewline |
529 \isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse% |
529 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% |
530 \isacommand{{\isachardot}{\isachardot}}\isanewline |
530 \ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
531 \ \ \ \ \ \ \isamarkupfalse% |
531 \isanewline |
532 \isacommand{with}\ nn\ \isamarkupfalse% |
532 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
533 \isacommand{show}\ False\ \isamarkupfalse% |
533 \ nn\ \isacommand{show}\isamarkupfalse% |
534 \isacommand{{\isachardot}{\isachardot}}\isanewline |
534 \ False\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
535 \ \ \ \ \isamarkupfalse% |
535 \isanewline |
536 \isacommand{qed}\isanewline |
536 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
537 \ \ \ \ \isamarkupfalse% |
537 \isanewline |
538 \isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse% |
538 \ \ \ \ \isacommand{hence}\isamarkupfalse% |
539 \isacommand{{\isachardot}{\isachardot}}\isanewline |
539 \ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
540 \ \ \ \ \isamarkupfalse% |
540 \isanewline |
541 \isacommand{with}\ nn\ \isamarkupfalse% |
541 \ \ \ \ \isacommand{with}\isamarkupfalse% |
542 \isacommand{show}\ False\ \isamarkupfalse% |
542 \ nn\ \isacommand{show}\isamarkupfalse% |
543 \isacommand{{\isachardot}{\isachardot}}\isanewline |
543 \ False\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
544 \ \ \isamarkupfalse% |
544 \isanewline |
545 \isacommand{qed}\isanewline |
545 \ \ \isacommand{qed}\isamarkupfalse% |
546 \isamarkupfalse% |
546 \isanewline |
547 \isacommand{qed}% |
547 \isacommand{qed}\isamarkupfalse% |
548 \endisatagproof |
548 % |
549 {\isafoldproof}% |
549 \endisatagproof |
550 % |
550 {\isafoldproof}% |
551 \isadelimproof |
551 % |
552 % |
552 \isadelimproof |
553 \endisadelimproof |
553 % |
554 \isamarkuptrue% |
554 \endisadelimproof |
555 % |
555 % |
556 \begin{isamarkuptext}% |
556 \begin{isamarkuptext}% |
557 \noindent |
557 \noindent |
558 Rule \isa{ccontr} (``classical contradiction'') is |
558 Rule \isa{ccontr} (``classical contradiction'') is |
559 \isa{{\isacharparenleft}{\isasymnot}\ P\ {\isasymLongrightarrow}\ False{\isacharparenright}\ {\isasymLongrightarrow}\ P}. |
559 \isa{{\isacharparenleft}{\isasymnot}\ P\ {\isasymLongrightarrow}\ False{\isacharparenright}\ {\isasymLongrightarrow}\ P}. |
576 % |
576 % |
577 \begin{isamarkuptext}% |
577 \begin{isamarkuptext}% |
578 So far our examples have been a bit unnatural: normally we want to |
578 So far our examples have been a bit unnatural: normally we want to |
579 prove rules expressed with \isa{{\isasymLongrightarrow}}, not \isa{{\isasymlongrightarrow}}. Here is an example:% |
579 prove rules expressed with \isa{{\isasymLongrightarrow}}, not \isa{{\isasymlongrightarrow}}. Here is an example:% |
580 \end{isamarkuptext}% |
580 \end{isamarkuptext}% |
581 \isamarkupfalse% |
581 \isamarkuptrue% |
582 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline |
582 \isacommand{lemma}\isamarkupfalse% |
583 % |
583 \ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline |
584 \isadelimproof |
584 % |
585 % |
585 \isadelimproof |
586 \endisadelimproof |
586 % |
587 % |
587 \endisadelimproof |
588 \isatagproof |
588 % |
589 \isamarkupfalse% |
589 \isatagproof |
590 \isacommand{proof}\isanewline |
590 \isacommand{proof}\isamarkupfalse% |
591 \ \ \isamarkupfalse% |
591 \isanewline |
592 \isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse% |
592 \ \ \isacommand{assume}\isamarkupfalse% |
593 \isacommand{thus}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse% |
593 \ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse% |
594 \isacommand{{\isachardot}{\isachardot}}\isanewline |
594 \ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
595 \isamarkupfalse% |
595 \isanewline |
596 \isacommand{next}\isanewline |
596 \isacommand{next}\isamarkupfalse% |
597 \ \ \isamarkupfalse% |
597 \isanewline |
598 \isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse% |
598 \ \ \isacommand{assume}\isamarkupfalse% |
599 \isacommand{thus}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% |
599 \ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse% |
600 \isacommand{{\isachardot}{\isachardot}}\isanewline |
600 \ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
601 \isamarkupfalse% |
601 \isanewline |
602 \isacommand{qed}% |
602 \isacommand{qed}\isamarkupfalse% |
603 \endisatagproof |
603 % |
604 {\isafoldproof}% |
604 \endisatagproof |
605 % |
605 {\isafoldproof}% |
606 \isadelimproof |
606 % |
607 % |
607 \isadelimproof |
608 \endisadelimproof |
608 % |
609 \isamarkuptrue% |
609 \endisadelimproof |
610 % |
610 % |
611 \begin{isamarkuptext}% |
611 \begin{isamarkuptext}% |
612 \noindent The \isakeyword{proof} always works on the conclusion, |
612 \noindent The \isakeyword{proof} always works on the conclusion, |
613 \isa{B\ {\isasymand}\ A} in our case, thus selecting $\land$-introduction. Hence |
613 \isa{B\ {\isasymand}\ A} in our case, thus selecting $\land$-introduction. Hence |
614 we must show \isa{B} and \isa{A}; both are proved by |
614 we must show \isa{B} and \isa{A}; both are proved by |
631 |
631 |
632 This is all very well as long as formulae are small. Let us now look at some |
632 This is all very well as long as formulae are small. Let us now look at some |
633 devices to avoid repeating (possibly large) formulae. A very general method |
633 devices to avoid repeating (possibly large) formulae. A very general method |
634 is pattern matching:% |
634 is pattern matching:% |
635 \end{isamarkuptext}% |
635 \end{isamarkuptext}% |
636 \isamarkupfalse% |
636 \isamarkuptrue% |
637 \isacommand{lemma}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\isanewline |
637 \isacommand{lemma}\isamarkupfalse% |
638 \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline |
638 \ {\isachardoublequoteopen}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequoteclose}\isanewline |
639 % |
639 \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequoteclose}{\isacharparenright}\isanewline |
640 \isadelimproof |
640 % |
641 % |
641 \isadelimproof |
642 \endisadelimproof |
642 % |
643 % |
643 \endisadelimproof |
644 \isatagproof |
644 % |
645 \isamarkupfalse% |
645 \isatagproof |
646 \isacommand{proof}\isanewline |
646 \isacommand{proof}\isamarkupfalse% |
647 \ \ \isamarkupfalse% |
647 \isanewline |
648 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse% |
648 \ \ \isacommand{assume}\isamarkupfalse% |
649 \isacommand{thus}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse% |
649 \ {\isachardoublequoteopen}{\isacharquery}AB{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse% |
650 \isacommand{{\isachardot}{\isachardot}}\isanewline |
650 \ {\isachardoublequoteopen}{\isacharquery}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
651 \isamarkupfalse% |
651 \isanewline |
652 \isacommand{next}\isanewline |
652 \isacommand{next}\isamarkupfalse% |
653 \ \ \isamarkupfalse% |
653 \isanewline |
654 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse% |
654 \ \ \isacommand{assume}\isamarkupfalse% |
655 \isacommand{thus}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse% |
655 \ {\isachardoublequoteopen}{\isacharquery}AB{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse% |
656 \isacommand{{\isachardot}{\isachardot}}\isanewline |
656 \ {\isachardoublequoteopen}{\isacharquery}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
657 \isamarkupfalse% |
657 \isanewline |
658 \isacommand{qed}% |
658 \isacommand{qed}\isamarkupfalse% |
659 \endisatagproof |
659 % |
660 {\isafoldproof}% |
660 \endisatagproof |
661 % |
661 {\isafoldproof}% |
662 \isadelimproof |
662 % |
663 % |
663 \isadelimproof |
664 \endisadelimproof |
664 % |
665 \isamarkuptrue% |
665 \endisadelimproof |
666 % |
666 % |
667 \begin{isamarkuptext}% |
667 \begin{isamarkuptext}% |
668 \noindent Any formula may be followed by |
668 \noindent Any formula may be followed by |
669 \isa{{\isacharparenleft}}\isakeyword{is}~\emph{pattern}\isa{{\isacharparenright}} which causes the pattern |
669 \isa{{\isacharparenleft}}\isakeyword{is}~\emph{pattern}\isa{{\isacharparenright}} which causes the pattern |
670 to be matched against the formula, instantiating the \isa{{\isacharquery}}-variables in |
670 to be matched against the formula, instantiating the \isa{{\isacharquery}}-variables in |
673 |
673 |
674 We can simplify things even more by stating the theorem by means of the |
674 We can simplify things even more by stating the theorem by means of the |
675 \isakeyword{assumes} and \isakeyword{shows} elements which allow direct |
675 \isakeyword{assumes} and \isakeyword{shows} elements which allow direct |
676 naming of assumptions:% |
676 naming of assumptions:% |
677 \end{isamarkuptext}% |
677 \end{isamarkuptext}% |
678 \isamarkupfalse% |
678 \isamarkuptrue% |
679 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline |
679 \isacommand{lemma}\isamarkupfalse% |
680 \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline |
680 \ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequoteopen}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequoteclose}\isanewline |
681 % |
681 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequoteclose}{\isacharparenright}\isanewline |
682 \isadelimproof |
682 % |
683 % |
683 \isadelimproof |
684 \endisadelimproof |
684 % |
685 % |
685 \endisadelimproof |
686 \isatagproof |
686 % |
687 \isamarkupfalse% |
687 \isatagproof |
688 \isacommand{proof}\isanewline |
688 \isacommand{proof}\isamarkupfalse% |
689 \ \ \isamarkupfalse% |
689 \isanewline |
690 \isacommand{from}\ AB\ \isamarkupfalse% |
690 \ \ \isacommand{from}\isamarkupfalse% |
691 \isacommand{show}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse% |
691 \ AB\ \isacommand{show}\isamarkupfalse% |
692 \isacommand{{\isachardot}{\isachardot}}\isanewline |
692 \ {\isachardoublequoteopen}{\isacharquery}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
693 \isamarkupfalse% |
693 \isanewline |
694 \isacommand{next}\isanewline |
694 \isacommand{next}\isamarkupfalse% |
695 \ \ \isamarkupfalse% |
695 \isanewline |
696 \isacommand{from}\ AB\ \isamarkupfalse% |
696 \ \ \isacommand{from}\isamarkupfalse% |
697 \isacommand{show}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse% |
697 \ AB\ \isacommand{show}\isamarkupfalse% |
698 \isacommand{{\isachardot}{\isachardot}}\isanewline |
698 \ {\isachardoublequoteopen}{\isacharquery}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
699 \isamarkupfalse% |
699 \isanewline |
700 \isacommand{qed}% |
700 \isacommand{qed}\isamarkupfalse% |
701 \endisatagproof |
701 % |
702 {\isafoldproof}% |
702 \endisatagproof |
703 % |
703 {\isafoldproof}% |
704 \isadelimproof |
704 % |
705 % |
705 \isadelimproof |
706 \endisadelimproof |
706 % |
707 \isamarkuptrue% |
707 \endisadelimproof |
708 % |
708 % |
709 \begin{isamarkuptext}% |
709 \begin{isamarkuptext}% |
710 \noindent Note the difference between \isa{{\isacharquery}AB}, a term, and |
710 \noindent Note the difference between \isa{{\isacharquery}AB}, a term, and |
711 \isa{AB}, a fact. |
711 \isa{AB}, a fact. |
712 |
712 |
713 Finally we want to start the proof with $\land$-elimination so we |
713 Finally we want to start the proof with $\land$-elimination so we |
714 don't have to perform it twice, as above. Here is a slick way to |
714 don't have to perform it twice, as above. Here is a slick way to |
715 achieve this:% |
715 achieve this:% |
716 \end{isamarkuptext}% |
716 \end{isamarkuptext}% |
717 \isamarkupfalse% |
717 \isamarkuptrue% |
718 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline |
718 \isacommand{lemma}\isamarkupfalse% |
719 \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline |
719 \ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequoteopen}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequoteclose}\isanewline |
720 % |
720 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequoteclose}{\isacharparenright}\isanewline |
721 \isadelimproof |
721 % |
722 % |
722 \isadelimproof |
723 \endisadelimproof |
723 % |
724 % |
724 \endisadelimproof |
725 \isatagproof |
725 % |
726 \isamarkupfalse% |
726 \isatagproof |
727 \isacommand{using}\ AB\isanewline |
727 \isacommand{using}\isamarkupfalse% |
728 \isamarkupfalse% |
728 \ AB\isanewline |
729 \isacommand{proof}\isanewline |
729 \isacommand{proof}\isamarkupfalse% |
730 \ \ \isamarkupfalse% |
730 \isanewline |
731 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse% |
731 \ \ \isacommand{assume}\isamarkupfalse% |
732 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
732 \ {\isachardoublequoteopen}{\isacharquery}A{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}B{\isachardoublequoteclose}\ \isacommand{show}\isamarkupfalse% |
733 \isacommand{{\isachardot}{\isachardot}}\isanewline |
733 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
734 \isamarkupfalse% |
734 \isanewline |
735 \isacommand{qed}% |
735 \isacommand{qed}\isamarkupfalse% |
736 \endisatagproof |
736 % |
737 {\isafoldproof}% |
737 \endisatagproof |
738 % |
738 {\isafoldproof}% |
739 \isadelimproof |
739 % |
740 % |
740 \isadelimproof |
741 \endisadelimproof |
741 % |
742 \isamarkuptrue% |
742 \endisadelimproof |
743 % |
743 % |
744 \begin{isamarkuptext}% |
744 \begin{isamarkuptext}% |
745 \noindent Command \isakeyword{using} can appear before a proof |
745 \noindent Command \isakeyword{using} can appear before a proof |
746 and adds further facts to those piped into the proof. Here \isa{AB} |
746 and adds further facts to those piped into the proof. Here \isa{AB} |
747 is the only such fact and it triggers $\land$-elimination. Another |
747 is the only such fact and it triggers $\land$-elimination. Another |
756 Sometimes it is necessary to suppress the implicit application of rules in a |
756 Sometimes it is necessary to suppress the implicit application of rules in a |
757 \isakeyword{proof}. For example \isakeyword{show}~\isa{A\ {\isasymor}\ B} would |
757 \isakeyword{proof}. For example \isakeyword{show}~\isa{A\ {\isasymor}\ B} would |
758 trigger $\lor$-introduction, requiring us to prove \isa{A}. A simple |
758 trigger $\lor$-introduction, requiring us to prove \isa{A}. A simple |
759 ``\isa{{\isacharminus}}'' prevents this \emph{faux pas}:% |
759 ``\isa{{\isacharminus}}'' prevents this \emph{faux pas}:% |
760 \end{isamarkuptext}% |
760 \end{isamarkuptext}% |
761 \isamarkupfalse% |
761 \isamarkuptrue% |
762 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}B\ {\isasymor}\ A{\isachardoublequote}\isanewline |
762 \isacommand{lemma}\isamarkupfalse% |
763 % |
763 \ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline |
764 \isadelimproof |
764 % |
765 % |
765 \isadelimproof |
766 \endisadelimproof |
766 % |
767 % |
767 \endisadelimproof |
768 \isatagproof |
768 % |
769 \isamarkupfalse% |
769 \isatagproof |
770 \isacommand{proof}\ {\isacharminus}\isanewline |
770 \isacommand{proof}\isamarkupfalse% |
771 \ \ \isamarkupfalse% |
771 \ {\isacharminus}\isanewline |
772 \isacommand{from}\ AB\ \isamarkupfalse% |
772 \ \ \isacommand{from}\isamarkupfalse% |
773 \isacommand{show}\ {\isacharquery}thesis\isanewline |
773 \ AB\ \isacommand{show}\isamarkupfalse% |
774 \ \ \isamarkupfalse% |
774 \ {\isacharquery}thesis\isanewline |
775 \isacommand{proof}\isanewline |
775 \ \ \isacommand{proof}\isamarkupfalse% |
776 \ \ \ \ \isamarkupfalse% |
776 \isanewline |
777 \isacommand{assume}\ A\ \isamarkupfalse% |
777 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
778 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
778 \ A\ \isacommand{show}\isamarkupfalse% |
779 \isacommand{{\isachardot}{\isachardot}}\isanewline |
779 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
780 \ \ \isamarkupfalse% |
780 \isanewline |
781 \isacommand{next}\isanewline |
781 \ \ \isacommand{next}\isamarkupfalse% |
782 \ \ \ \ \isamarkupfalse% |
782 \isanewline |
783 \isacommand{assume}\ B\ \isamarkupfalse% |
783 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
784 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
784 \ B\ \isacommand{show}\isamarkupfalse% |
785 \isacommand{{\isachardot}{\isachardot}}\isanewline |
785 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
786 \ \ \isamarkupfalse% |
786 \isanewline |
787 \isacommand{qed}\isanewline |
787 \ \ \isacommand{qed}\isamarkupfalse% |
788 \isamarkupfalse% |
788 \isanewline |
789 \isacommand{qed}% |
789 \isacommand{qed}\isamarkupfalse% |
790 \endisatagproof |
790 % |
791 {\isafoldproof}% |
791 \endisatagproof |
792 % |
792 {\isafoldproof}% |
793 \isadelimproof |
793 % |
794 % |
794 \isadelimproof |
795 \endisadelimproof |
795 % |
796 \isamarkuptrue% |
796 \endisadelimproof |
797 % |
797 % |
798 \isamarkupsubsection{Predicate calculus% |
798 \isamarkupsubsection{Predicate calculus% |
799 } |
799 } |
800 \isamarkuptrue% |
800 \isamarkuptrue% |
801 % |
801 % |
805 (the universal quantifier at the |
805 (the universal quantifier at the |
806 meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to |
806 meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to |
807 \isa{{\isasymLongrightarrow}}. Here is a sample proof, annotated with the rules that are |
807 \isa{{\isasymLongrightarrow}}. Here is a sample proof, annotated with the rules that are |
808 applied implicitly:% |
808 applied implicitly:% |
809 \end{isamarkuptext}% |
809 \end{isamarkuptext}% |
810 \isamarkupfalse% |
810 \isamarkuptrue% |
811 \isacommand{lemma}\ \isakeyword{assumes}\ P{\isacharcolon}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline |
811 \isacommand{lemma}\isamarkupfalse% |
812 % |
812 \ \isakeyword{assumes}\ P{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline |
813 \isadelimproof |
813 % |
814 % |
814 \isadelimproof |
815 \endisadelimproof |
815 % |
816 % |
816 \endisadelimproof |
817 \isatagproof |
817 % |
818 \isamarkupfalse% |
818 \isatagproof |
819 \isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ % |
819 \isacommand{proof}\isamarkupfalse% |
|
820 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ % |
820 \isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}% |
821 \isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}% |
821 } |
822 } |
822 \isanewline |
823 \isanewline |
823 \ \ \isamarkupfalse% |
824 \ \ \isacommand{fix}\isamarkupfalse% |
824 \isacommand{fix}\ a\isanewline |
825 \ a\isanewline |
825 \ \ \isamarkupfalse% |
826 \ \ \isacommand{from}\isamarkupfalse% |
826 \isacommand{from}\ P\ \isamarkupfalse% |
827 \ P\ \isacommand{show}\isamarkupfalse% |
827 \isacommand{show}\ {\isachardoublequote}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
828 \ {\isachardoublequoteopen}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
828 \isacommand{{\isachardot}{\isachardot}}\ \ % |
829 \ \ % |
829 \isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}% |
830 \isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}% |
830 } |
831 } |
831 \isanewline |
832 \isanewline |
832 \isamarkupfalse% |
833 \isacommand{qed}\isamarkupfalse% |
833 \isacommand{qed}% |
834 % |
834 \endisatagproof |
835 \endisatagproof |
835 {\isafoldproof}% |
836 {\isafoldproof}% |
836 % |
837 % |
837 \isadelimproof |
838 \isadelimproof |
838 % |
839 % |
839 \endisadelimproof |
840 \endisadelimproof |
840 \isamarkuptrue% |
|
841 % |
841 % |
842 \begin{isamarkuptext}% |
842 \begin{isamarkuptext}% |
843 \noindent Note that in the proof we have chosen to call the bound |
843 \noindent Note that in the proof we have chosen to call the bound |
844 variable \isa{a} instead of \isa{x} merely to show that the choice of |
844 variable \isa{a} instead of \isa{x} merely to show that the choice of |
845 local names is irrelevant. |
845 local names is irrelevant. |
846 |
846 |
847 Next we look at \isa{{\isasymexists}} which is a bit more tricky.% |
847 Next we look at \isa{{\isasymexists}} which is a bit more tricky.% |
848 \end{isamarkuptext}% |
848 \end{isamarkuptext}% |
849 \isamarkupfalse% |
849 \isamarkuptrue% |
850 \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline |
850 \isacommand{lemma}\isamarkupfalse% |
851 % |
851 \ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequoteclose}\isanewline |
852 \isadelimproof |
852 % |
853 % |
853 \isadelimproof |
854 \endisadelimproof |
854 % |
855 % |
855 \endisadelimproof |
856 \isatagproof |
856 % |
857 \isamarkupfalse% |
857 \isatagproof |
858 \isacommand{proof}\ {\isacharminus}\isanewline |
858 \isacommand{proof}\isamarkupfalse% |
859 \ \ \isamarkupfalse% |
859 \ {\isacharminus}\isanewline |
860 \isacommand{from}\ Pf\ \isamarkupfalse% |
860 \ \ \isacommand{from}\isamarkupfalse% |
861 \isacommand{show}\ {\isacharquery}thesis\isanewline |
861 \ Pf\ \isacommand{show}\isamarkupfalse% |
862 \ \ \isamarkupfalse% |
862 \ {\isacharquery}thesis\isanewline |
863 \isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ % |
863 \ \ \isacommand{proof}\isamarkupfalse% |
|
864 \ \ \ \ \ \ \ \ \ \ \ \ \ \ % |
864 \isamarkupcmt{\isa{exE}: \isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}% |
865 \isamarkupcmt{\isa{exE}: \isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}% |
865 } |
866 } |
866 \isanewline |
867 \isanewline |
867 \ \ \ \ \isamarkupfalse% |
868 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
868 \isacommand{fix}\ x\isanewline |
869 \ x\isanewline |
869 \ \ \ \ \isamarkupfalse% |
870 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
870 \isacommand{assume}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline |
871 \ {\isachardoublequoteopen}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline |
871 \ \ \ \ \isamarkupfalse% |
872 \ \ \ \ \isacommand{show}\isamarkupfalse% |
872 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
873 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
873 \isacommand{{\isachardot}{\isachardot}}\ \ % |
874 \ \ % |
874 \isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}% |
875 \isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}% |
875 } |
876 } |
876 \isanewline |
877 \isanewline |
877 \ \ \isamarkupfalse% |
878 \ \ \isacommand{qed}\isamarkupfalse% |
878 \isacommand{qed}\isanewline |
879 \isanewline |
879 \isamarkupfalse% |
880 \isacommand{qed}\isamarkupfalse% |
880 \isacommand{qed}% |
881 % |
881 \endisatagproof |
882 \endisatagproof |
882 {\isafoldproof}% |
883 {\isafoldproof}% |
883 % |
884 % |
884 \isadelimproof |
885 \isadelimproof |
885 % |
886 % |
886 \endisadelimproof |
887 \endisadelimproof |
887 \isamarkuptrue% |
|
888 % |
888 % |
889 \begin{isamarkuptext}% |
889 \begin{isamarkuptext}% |
890 \noindent Explicit $\exists$-elimination as seen above can become |
890 \noindent Explicit $\exists$-elimination as seen above can become |
891 cumbersome in practice. The derived Isar language element |
891 cumbersome in practice. The derived Isar language element |
892 \isakeyword{obtain} provides a more appealing form of generalised |
892 \isakeyword{obtain} provides a more appealing form of generalised |
893 existence reasoning:% |
893 existence reasoning:% |
894 \end{isamarkuptext}% |
894 \end{isamarkuptext}% |
895 \isamarkupfalse% |
895 \isamarkuptrue% |
896 \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline |
896 \isacommand{lemma}\isamarkupfalse% |
897 % |
897 \ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequoteclose}\isanewline |
898 \isadelimproof |
898 % |
899 % |
899 \isadelimproof |
900 \endisadelimproof |
900 % |
901 % |
901 \endisadelimproof |
902 \isatagproof |
902 % |
903 \isamarkupfalse% |
903 \isatagproof |
904 \isacommand{proof}\ {\isacharminus}\isanewline |
904 \isacommand{proof}\isamarkupfalse% |
905 \ \ \isamarkupfalse% |
905 \ {\isacharminus}\isanewline |
906 \isacommand{from}\ Pf\ \isamarkupfalse% |
906 \ \ \isacommand{from}\isamarkupfalse% |
907 \isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
907 \ Pf\ \isacommand{obtain}\isamarkupfalse% |
908 \isacommand{{\isachardot}{\isachardot}}\isanewline |
908 \ x\ \isakeyword{where}\ {\isachardoublequoteopen}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
909 \ \ \isamarkupfalse% |
909 \isanewline |
910 \isacommand{thus}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\ \isamarkupfalse% |
910 \ \ \isacommand{thus}\isamarkupfalse% |
911 \isacommand{{\isachardot}{\isachardot}}\isanewline |
911 \ {\isachardoublequoteopen}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
912 \isamarkupfalse% |
912 \isanewline |
913 \isacommand{qed}% |
913 \isacommand{qed}\isamarkupfalse% |
914 \endisatagproof |
914 % |
915 {\isafoldproof}% |
915 \endisatagproof |
916 % |
916 {\isafoldproof}% |
917 \isadelimproof |
917 % |
918 % |
918 \isadelimproof |
919 \endisadelimproof |
919 % |
920 \isamarkuptrue% |
920 \endisadelimproof |
921 % |
921 % |
922 \begin{isamarkuptext}% |
922 \begin{isamarkuptext}% |
923 \noindent Note how the proof text follows the usual mathematical style |
923 \noindent Note how the proof text follows the usual mathematical style |
924 of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$ |
924 of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$ |
925 as a new local variable. Technically, \isakeyword{obtain} is similar to |
925 as a new local variable. Technically, \isakeyword{obtain} is similar to |
927 the elimination involved. |
927 the elimination involved. |
928 |
928 |
929 Here is a proof of a well known tautology. |
929 Here is a proof of a well known tautology. |
930 Which rule is used where?% |
930 Which rule is used where?% |
931 \end{isamarkuptext}% |
931 \end{isamarkuptext}% |
932 \isamarkupfalse% |
932 \isamarkuptrue% |
933 \isacommand{lemma}\ \isakeyword{assumes}\ ex{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\isanewline |
933 \isacommand{lemma}\isamarkupfalse% |
934 % |
934 \ \isakeyword{assumes}\ ex{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\isanewline |
935 \isadelimproof |
935 % |
936 % |
936 \isadelimproof |
937 \endisadelimproof |
937 % |
938 % |
938 \endisadelimproof |
939 \isatagproof |
939 % |
940 \isamarkupfalse% |
940 \isatagproof |
941 \isacommand{proof}\isanewline |
941 \isacommand{proof}\isamarkupfalse% |
942 \ \ \isamarkupfalse% |
942 \isanewline |
943 \isacommand{fix}\ y\isanewline |
943 \ \ \isacommand{fix}\isamarkupfalse% |
944 \ \ \isamarkupfalse% |
944 \ y\isanewline |
945 \isacommand{from}\ ex\ \isamarkupfalse% |
945 \ \ \isacommand{from}\isamarkupfalse% |
946 \isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse% |
946 \ ex\ \isacommand{obtain}\isamarkupfalse% |
947 \isacommand{{\isachardot}{\isachardot}}\isanewline |
947 \ x\ \isakeyword{where}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
948 \ \ \isamarkupfalse% |
948 \isanewline |
949 \isacommand{hence}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isamarkupfalse% |
949 \ \ \isacommand{hence}\isamarkupfalse% |
950 \isacommand{{\isachardot}{\isachardot}}\isanewline |
950 \ {\isachardoublequoteopen}P\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
951 \ \ \isamarkupfalse% |
951 \isanewline |
952 \isacommand{thus}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse% |
952 \ \ \isacommand{thus}\isamarkupfalse% |
953 \isacommand{{\isachardot}{\isachardot}}\isanewline |
953 \ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
954 \isamarkupfalse% |
954 \isanewline |
955 \isacommand{qed}% |
955 \isacommand{qed}\isamarkupfalse% |
956 \endisatagproof |
956 % |
957 {\isafoldproof}% |
957 \endisatagproof |
958 % |
958 {\isafoldproof}% |
959 \isadelimproof |
959 % |
960 % |
960 \isadelimproof |
961 \endisadelimproof |
961 % |
962 \isamarkuptrue% |
962 \endisadelimproof |
963 % |
963 % |
964 \isamarkupsubsection{Making bigger steps% |
964 \isamarkupsubsection{Making bigger steps% |
965 } |
965 } |
966 \isamarkuptrue% |
966 \isamarkuptrue% |
967 % |
967 % |
969 So far we have confined ourselves to single step proofs. Of course |
969 So far we have confined ourselves to single step proofs. Of course |
970 powerful automatic methods can be used just as well. Here is an example, |
970 powerful automatic methods can be used just as well. Here is an example, |
971 Cantor's theorem that there is no surjective function from a set to its |
971 Cantor's theorem that there is no surjective function from a set to its |
972 powerset:% |
972 powerset:% |
973 \end{isamarkuptext}% |
973 \end{isamarkuptext}% |
974 \isamarkupfalse% |
974 \isamarkuptrue% |
975 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline |
975 \isacommand{theorem}\isamarkupfalse% |
976 % |
976 \ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequoteclose}\isanewline |
977 \isadelimproof |
977 % |
978 % |
978 \isadelimproof |
979 \endisadelimproof |
979 % |
980 % |
980 \endisadelimproof |
981 \isatagproof |
981 % |
982 \isamarkupfalse% |
982 \isatagproof |
983 \isacommand{proof}\isanewline |
983 \isacommand{proof}\isamarkupfalse% |
984 \ \ \isamarkupfalse% |
984 \isanewline |
985 \isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline |
985 \ \ \isacommand{let}\isamarkupfalse% |
986 \ \ \isamarkupfalse% |
986 \ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
987 \isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline |
987 \ \ \isacommand{show}\isamarkupfalse% |
988 \ \ \isamarkupfalse% |
988 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}\isanewline |
989 \isacommand{proof}\isanewline |
989 \ \ \isacommand{proof}\isamarkupfalse% |
990 \ \ \ \ \isamarkupfalse% |
990 \isanewline |
991 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline |
991 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
992 \ \ \ \ \isamarkupfalse% |
992 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline |
993 \isacommand{then}\ \isamarkupfalse% |
993 \ \ \ \ \isacommand{then}\isamarkupfalse% |
994 \isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse% |
994 \ \isacommand{obtain}\isamarkupfalse% |
995 \isacommand{{\isachardot}{\isachardot}}\isanewline |
995 \ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
996 \ \ \ \ \isamarkupfalse% |
996 \isanewline |
997 \isacommand{show}\ False\isanewline |
997 \ \ \ \ \isacommand{show}\isamarkupfalse% |
998 \ \ \ \ \isamarkupfalse% |
998 \ False\isanewline |
999 \isacommand{proof}\ cases\isanewline |
999 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
1000 \ \ \ \ \ \ \isamarkupfalse% |
1000 \ cases\isanewline |
1001 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline |
1001 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
1002 \ \ \ \ \ \ \isamarkupfalse% |
1002 \ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline |
1003 \isacommand{with}\ fy\ \isamarkupfalse% |
1003 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
1004 \isacommand{show}\ False\ \isamarkupfalse% |
1004 \ fy\ \isacommand{show}\isamarkupfalse% |
1005 \isacommand{by}\ blast\isanewline |
1005 \ False\ \isacommand{by}\isamarkupfalse% |
1006 \ \ \ \ \isamarkupfalse% |
1006 \ blast\isanewline |
1007 \isacommand{next}\isanewline |
1007 \ \ \ \ \isacommand{next}\isamarkupfalse% |
1008 \ \ \ \ \ \ \isamarkupfalse% |
1008 \isanewline |
1009 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline |
1009 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
1010 \ \ \ \ \ \ \isamarkupfalse% |
1010 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline |
1011 \isacommand{with}\ fy\ \isamarkupfalse% |
1011 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
1012 \isacommand{show}\ False\ \isamarkupfalse% |
1012 \ fy\ \isacommand{show}\isamarkupfalse% |
1013 \isacommand{by}\ blast\isanewline |
1013 \ False\ \isacommand{by}\isamarkupfalse% |
1014 \ \ \ \ \isamarkupfalse% |
1014 \ blast\isanewline |
1015 \isacommand{qed}\isanewline |
1015 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
1016 \ \ \isamarkupfalse% |
1016 \isanewline |
1017 \isacommand{qed}\isanewline |
1017 \ \ \isacommand{qed}\isamarkupfalse% |
1018 \isamarkupfalse% |
1018 \isanewline |
1019 \isacommand{qed}% |
1019 \isacommand{qed}\isamarkupfalse% |
1020 \endisatagproof |
1020 % |
1021 {\isafoldproof}% |
1021 \endisatagproof |
1022 % |
1022 {\isafoldproof}% |
1023 \isadelimproof |
1023 % |
1024 % |
1024 \isadelimproof |
1025 \endisadelimproof |
1025 % |
1026 \isamarkuptrue% |
1026 \endisadelimproof |
1027 % |
1027 % |
1028 \begin{isamarkuptext}% |
1028 \begin{isamarkuptext}% |
1029 \noindent |
1029 \noindent |
1030 For a start, the example demonstrates two new constructs: |
1030 For a start, the example demonstrates two new constructs: |
1031 \begin{itemize} |
1031 \begin{itemize} |
1042 Method \isa{blast} is used because the contradiction does not follow easily |
1042 Method \isa{blast} is used because the contradiction does not follow easily |
1043 by just a single rule. If you find the proof too cryptic for human |
1043 by just a single rule. If you find the proof too cryptic for human |
1044 consumption, here is a more detailed version; the beginning up to |
1044 consumption, here is a more detailed version; the beginning up to |
1045 \isakeyword{obtain} stays unchanged.% |
1045 \isakeyword{obtain} stays unchanged.% |
1046 \end{isamarkuptext}% |
1046 \end{isamarkuptext}% |
1047 \isamarkupfalse% |
1047 \isamarkuptrue% |
1048 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline |
1048 \isacommand{theorem}\isamarkupfalse% |
1049 % |
1049 \ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequoteclose}\isanewline |
1050 \isadelimproof |
1050 % |
1051 % |
1051 \isadelimproof |
1052 \endisadelimproof |
1052 % |
1053 % |
1053 \endisadelimproof |
1054 \isatagproof |
1054 % |
1055 \isamarkupfalse% |
1055 \isatagproof |
1056 \isacommand{proof}\isanewline |
1056 \isacommand{proof}\isamarkupfalse% |
1057 \ \ \isamarkupfalse% |
1057 \isanewline |
1058 \isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline |
1058 \ \ \isacommand{let}\isamarkupfalse% |
1059 \ \ \isamarkupfalse% |
1059 \ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
1060 \isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline |
1060 \ \ \isacommand{show}\isamarkupfalse% |
1061 \ \ \isamarkupfalse% |
1061 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}\isanewline |
1062 \isacommand{proof}\isanewline |
1062 \ \ \isacommand{proof}\isamarkupfalse% |
1063 \ \ \ \ \isamarkupfalse% |
1063 \isanewline |
1064 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline |
1064 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
1065 \ \ \ \ \isamarkupfalse% |
1065 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline |
1066 \isacommand{then}\ \isamarkupfalse% |
1066 \ \ \ \ \isacommand{then}\isamarkupfalse% |
1067 \isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse% |
1067 \ \isacommand{obtain}\isamarkupfalse% |
1068 \isacommand{{\isachardot}{\isachardot}}\isanewline |
1068 \ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
1069 \ \ \ \ \isamarkupfalse% |
1069 \isanewline |
1070 \isacommand{show}\ False\isanewline |
1070 \ \ \ \ \isacommand{show}\isamarkupfalse% |
1071 \ \ \ \ \isamarkupfalse% |
1071 \ False\isanewline |
1072 \isacommand{proof}\ cases\isanewline |
1072 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
1073 \ \ \ \ \ \ \isamarkupfalse% |
1073 \ cases\isanewline |
1074 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline |
1074 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
1075 \ \ \ \ \ \ \isamarkupfalse% |
1075 \ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline |
1076 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse% |
1076 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% |
1077 \isacommand{by}\ simp\isanewline |
1077 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ f\ y{\isachardoublequoteclose}\ \ \ \isacommand{by}\isamarkupfalse% |
1078 \ \ \ \ \ \ \isamarkupfalse% |
1078 \ simp\isanewline |
1079 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse% |
1079 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% |
1080 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline |
1080 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse% |
1081 \ \ \ \ \ \ \isamarkupfalse% |
1081 {\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline |
1082 \isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse% |
1082 \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse% |
1083 \isacommand{by}\ contradiction\isanewline |
1083 \ False\ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
1084 \ \ \ \ \isamarkupfalse% |
1084 \ contradiction\isanewline |
1085 \isacommand{next}\isanewline |
1085 \ \ \ \ \isacommand{next}\isamarkupfalse% |
1086 \ \ \ \ \ \ \isamarkupfalse% |
1086 \isanewline |
1087 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline |
1087 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
1088 \ \ \ \ \ \ \isamarkupfalse% |
1088 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline |
1089 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse% |
1089 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% |
1090 \isacommand{by}\ simp\isanewline |
1090 \ {\isachardoublequoteopen}y\ {\isasymin}\ f\ y{\isachardoublequoteclose}\ \ \ \isacommand{by}\isamarkupfalse% |
1091 \ \ \ \ \ \ \isamarkupfalse% |
1091 \ simp\isanewline |
1092 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse% |
1092 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% |
1093 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline |
1093 \ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse% |
1094 \ \ \ \ \ \ \isamarkupfalse% |
1094 {\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline |
1095 \isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse% |
1095 \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse% |
1096 \isacommand{by}\ contradiction\isanewline |
1096 \ False\ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
1097 \ \ \ \ \isamarkupfalse% |
1097 \ contradiction\isanewline |
1098 \isacommand{qed}\isanewline |
1098 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
1099 \ \ \isamarkupfalse% |
1099 \isanewline |
1100 \isacommand{qed}\isanewline |
1100 \ \ \isacommand{qed}\isamarkupfalse% |
1101 \isamarkupfalse% |
1101 \isanewline |
1102 \isacommand{qed}% |
1102 \isacommand{qed}\isamarkupfalse% |
1103 \endisatagproof |
1103 % |
1104 {\isafoldproof}% |
1104 \endisatagproof |
1105 % |
1105 {\isafoldproof}% |
1106 \isadelimproof |
1106 % |
1107 % |
1107 \isadelimproof |
1108 \endisadelimproof |
1108 % |
1109 \isamarkuptrue% |
1109 \endisadelimproof |
1110 % |
1110 % |
1111 \begin{isamarkuptext}% |
1111 \begin{isamarkuptext}% |
1112 \noindent Method \isa{contradiction} succeeds if both $P$ and |
1112 \noindent Method \isa{contradiction} succeeds if both $P$ and |
1113 $\neg P$ are among the assumptions and the facts fed into that step, in any order. |
1113 $\neg P$ are among the assumptions and the facts fed into that step, in any order. |
1114 |
1114 |
1115 As it happens, Cantor's theorem can be proved automatically by best-first |
1115 As it happens, Cantor's theorem can be proved automatically by best-first |
1116 search. Depth-first search would diverge, but best-first search successfully |
1116 search. Depth-first search would diverge, but best-first search successfully |
1117 navigates through the large search space:% |
1117 navigates through the large search space:% |
1118 \end{isamarkuptext}% |
1118 \end{isamarkuptext}% |
1119 \isamarkupfalse% |
1119 \isamarkuptrue% |
1120 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline |
1120 \isacommand{theorem}\isamarkupfalse% |
1121 % |
1121 \ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequoteclose}\isanewline |
1122 \isadelimproof |
1122 % |
1123 % |
1123 \isadelimproof |
1124 \endisadelimproof |
1124 % |
1125 % |
1125 \endisadelimproof |
1126 \isatagproof |
1126 % |
1127 \isamarkupfalse% |
1127 \isatagproof |
1128 \isacommand{by}\ best% |
1128 \isacommand{by}\isamarkupfalse% |
1129 \endisatagproof |
1129 \ best% |
1130 {\isafoldproof}% |
1130 \endisatagproof |
1131 % |
1131 {\isafoldproof}% |
1132 \isadelimproof |
1132 % |
1133 % |
1133 \isadelimproof |
1134 \endisadelimproof |
1134 % |
1135 \isamarkuptrue% |
1135 \endisadelimproof |
1136 % |
1136 % |
1137 \isamarkupsubsection{Raw proof blocks% |
1137 \isamarkupsubsection{Raw proof blocks% |
1138 } |
1138 } |
1139 \isamarkuptrue% |
1139 \isamarkuptrue% |
1140 % |
1140 % |
1142 Although we have shown how to employ powerful automatic methods like |
1142 Although we have shown how to employ powerful automatic methods like |
1143 \isa{blast} to achieve bigger proof steps, there may still be the |
1143 \isa{blast} to achieve bigger proof steps, there may still be the |
1144 tendency to use the default introduction and elimination rules to |
1144 tendency to use the default introduction and elimination rules to |
1145 decompose goals and facts. This can lead to very tedious proofs:% |
1145 decompose goals and facts. This can lead to very tedious proofs:% |
1146 \end{isamarkuptext}% |
1146 \end{isamarkuptext}% |
|
1147 \isamarkuptrue% |
1147 % |
1148 % |
1148 \isadelimML |
1149 \isadelimML |
1149 % |
1150 % |
1150 \endisadelimML |
1151 \endisadelimML |
1151 % |
1152 % |
1152 \isatagML |
1153 \isatagML |
|
1154 \isamarkupfalse% |
1153 % |
1155 % |
1154 \endisatagML |
1156 \endisatagML |
1155 {\isafoldML}% |
1157 {\isafoldML}% |
1156 % |
1158 % |
1157 \isadelimML |
1159 \isadelimML |
1158 % |
1160 % |
1159 \endisadelimML |
1161 \endisadelimML |
1160 \isamarkupfalse% |
1162 \isacommand{lemma}\isamarkupfalse% |
1161 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline |
1163 \ {\isachardoublequoteopen}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1162 % |
1164 % |
1163 \isadelimproof |
1165 \isadelimproof |
1164 % |
1166 % |
1165 \endisadelimproof |
1167 \endisadelimproof |
1166 % |
1168 % |
1167 \isatagproof |
1169 \isatagproof |
1168 \isamarkupfalse% |
1170 \isacommand{proof}\isamarkupfalse% |
1169 \isacommand{proof}\isanewline |
1171 \isanewline |
1170 \ \ \isamarkupfalse% |
1172 \ \ \isacommand{fix}\isamarkupfalse% |
1171 \isacommand{fix}\ x\ \isamarkupfalse% |
1173 \ x\ \isacommand{show}\isamarkupfalse% |
1172 \isacommand{show}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline |
1174 \ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1173 \ \ \isamarkupfalse% |
1175 \ \ \isacommand{proof}\isamarkupfalse% |
1174 \isacommand{proof}\isanewline |
1176 \isanewline |
1175 \ \ \ \ \isamarkupfalse% |
1177 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
1176 \isacommand{fix}\ y\ \isamarkupfalse% |
1178 \ y\ \isacommand{show}\isamarkupfalse% |
1177 \isacommand{show}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline |
1179 \ {\isachardoublequoteopen}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1178 \ \ \ \ \isamarkupfalse% |
1180 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
1179 \isacommand{proof}\isanewline |
1181 \isanewline |
1180 \ \ \ \ \ \ \isamarkupfalse% |
1182 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
1181 \isacommand{assume}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequote}\isanewline |
1183 \ {\isachardoublequoteopen}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequoteclose}\isanewline |
1182 \ \ \ \ \ \ \isamarkupfalse% |
1184 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% |
1183 \isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse% |
1185 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% |
1184 \isacommand{sorry}\isanewline |
1186 \isanewline |
1185 \ \ \ \ \isamarkupfalse% |
1187 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
1186 \isacommand{qed}\isanewline |
1188 \isanewline |
1187 \ \ \isamarkupfalse% |
1189 \ \ \isacommand{qed}\isamarkupfalse% |
1188 \isacommand{qed}\isanewline |
1190 \isanewline |
1189 \isamarkupfalse% |
1191 \isacommand{qed}\isamarkupfalse% |
1190 \isacommand{qed}% |
1192 % |
1191 \endisatagproof |
1193 \endisatagproof |
1192 {\isafoldproof}% |
1194 {\isafoldproof}% |
1193 % |
1195 % |
1194 \isadelimproof |
1196 \isadelimproof |
1195 % |
1197 % |
1196 \endisadelimproof |
1198 \endisadelimproof |
1197 \isamarkuptrue% |
|
1198 % |
1199 % |
1199 \begin{isamarkuptext}% |
1200 \begin{isamarkuptext}% |
1200 \noindent Since we are only interested in the decomposition and not the |
1201 \noindent Since we are only interested in the decomposition and not the |
1201 actual proof, the latter has been replaced by |
1202 actual proof, the latter has been replaced by |
1202 \isakeyword{sorry}. Command \isakeyword{sorry} proves anything but is |
1203 \isakeyword{sorry}. Command \isakeyword{sorry} proves anything but is |
1203 only allowed in quick and dirty mode, the default interactive mode. It |
1204 only allowed in quick and dirty mode, the default interactive mode. It |
1204 is very convenient for top down proof development. |
1205 is very convenient for top down proof development. |
1205 |
1206 |
1206 Luckily we can avoid this step by step decomposition very easily:% |
1207 Luckily we can avoid this step by step decomposition very easily:% |
1207 \end{isamarkuptext}% |
1208 \end{isamarkuptext}% |
1208 \isamarkupfalse% |
1209 \isamarkuptrue% |
1209 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline |
1210 \isacommand{lemma}\isamarkupfalse% |
1210 % |
1211 \ {\isachardoublequoteopen}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1211 \isadelimproof |
1212 % |
1212 % |
1213 \isadelimproof |
1213 \endisadelimproof |
1214 % |
1214 % |
1215 \endisadelimproof |
1215 \isatagproof |
1216 % |
1216 \isamarkupfalse% |
1217 \isatagproof |
1217 \isacommand{proof}\ {\isacharminus}\isanewline |
1218 \isacommand{proof}\isamarkupfalse% |
1218 \ \ \isamarkupfalse% |
1219 \ {\isacharminus}\isanewline |
1219 \isacommand{have}\ {\isachardoublequote}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline |
1220 \ \ \isacommand{have}\isamarkupfalse% |
1220 \ \ \isamarkupfalse% |
1221 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1221 \isacommand{proof}\ {\isacharminus}\isanewline |
1222 \ \ \isacommand{proof}\isamarkupfalse% |
1222 \ \ \ \ \isamarkupfalse% |
1223 \ {\isacharminus}\isanewline |
1223 \isacommand{fix}\ x\ y\ \isamarkupfalse% |
1224 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
1224 \isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline |
1225 \ x\ y\ \isacommand{assume}\isamarkupfalse% |
1225 \ \ \ \ \isamarkupfalse% |
1226 \ {\isachardoublequoteopen}A\ x\ y{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ x\ y{\isachardoublequoteclose}\isanewline |
1226 \isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse% |
1227 \ \ \ \ \isacommand{show}\isamarkupfalse% |
1227 \isacommand{sorry}\isanewline |
1228 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% |
1228 \ \ \isamarkupfalse% |
1229 \isanewline |
1229 \isacommand{qed}\isanewline |
1230 \ \ \isacommand{qed}\isamarkupfalse% |
1230 \ \ \isamarkupfalse% |
1231 \isanewline |
1231 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
1232 \ \ \isacommand{thus}\isamarkupfalse% |
1232 \isacommand{by}\ blast\isanewline |
1233 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
1233 \isamarkupfalse% |
1234 \ blast\isanewline |
1234 \isacommand{qed}% |
1235 \isacommand{qed}\isamarkupfalse% |
1235 \endisatagproof |
1236 % |
1236 {\isafoldproof}% |
1237 \endisatagproof |
1237 % |
1238 {\isafoldproof}% |
1238 \isadelimproof |
1239 % |
1239 % |
1240 \isadelimproof |
1240 \endisadelimproof |
1241 % |
1241 \isamarkuptrue% |
1242 \endisadelimproof |
1242 % |
1243 % |
1243 \begin{isamarkuptext}% |
1244 \begin{isamarkuptext}% |
1244 \noindent |
1245 \noindent |
1245 This can be simplified further by \emph{raw proof blocks}, i.e.\ |
1246 This can be simplified further by \emph{raw proof blocks}, i.e.\ |
1246 proofs enclosed in braces:% |
1247 proofs enclosed in braces:% |
1247 \end{isamarkuptext}% |
1248 \end{isamarkuptext}% |
1248 \isamarkupfalse% |
1249 \isamarkuptrue% |
1249 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline |
1250 \isacommand{lemma}\isamarkupfalse% |
1250 % |
1251 \ {\isachardoublequoteopen}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1251 \isadelimproof |
1252 % |
1252 % |
1253 \isadelimproof |
1253 \endisadelimproof |
1254 % |
1254 % |
1255 \endisadelimproof |
1255 \isatagproof |
1256 % |
1256 \isamarkupfalse% |
1257 \isatagproof |
1257 \isacommand{proof}\ {\isacharminus}\isanewline |
1258 \isacommand{proof}\isamarkupfalse% |
1258 \ \ \isamarkupfalse% |
1259 \ {\isacharminus}\isanewline |
1259 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse% |
1260 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse% |
1260 \isacommand{fix}\ x\ y\ \isamarkupfalse% |
1261 \ \isacommand{fix}\isamarkupfalse% |
1261 \isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline |
1262 \ x\ y\ \isacommand{assume}\isamarkupfalse% |
1262 \ \ \ \ \isamarkupfalse% |
1263 \ {\isachardoublequoteopen}A\ x\ y{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ x\ y{\isachardoublequoteclose}\isanewline |
1263 \isacommand{have}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse% |
1264 \ \ \ \ \isacommand{have}\isamarkupfalse% |
1264 \isacommand{sorry}\ \isamarkupfalse% |
1265 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% |
1265 \isacommand{{\isacharbraceright}}\isanewline |
1266 \ \isacommand{{\isacharbraceright}}\isamarkupfalse% |
1266 \ \ \isamarkupfalse% |
1267 \isanewline |
1267 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
1268 \ \ \isacommand{thus}\isamarkupfalse% |
1268 \isacommand{by}\ blast\isanewline |
1269 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
1269 \isamarkupfalse% |
1270 \ blast\isanewline |
1270 \isacommand{qed}% |
1271 \isacommand{qed}\isamarkupfalse% |
1271 \endisatagproof |
1272 % |
1272 {\isafoldproof}% |
1273 \endisatagproof |
1273 % |
1274 {\isafoldproof}% |
1274 \isadelimproof |
1275 % |
1275 % |
1276 \isadelimproof |
1276 \endisadelimproof |
1277 % |
1277 \isamarkuptrue% |
1278 \endisadelimproof |
1278 % |
1279 % |
1279 \begin{isamarkuptext}% |
1280 \begin{isamarkuptext}% |
1280 \noindent The result of the raw proof block is the same theorem |
1281 \noindent The result of the raw proof block is the same theorem |
1281 as above, namely \isa{{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}A\ x\ y{\isacharsemicolon}\ B\ x\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y}. Raw |
1282 as above, namely \isa{{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}A\ x\ y{\isacharsemicolon}\ B\ x\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y}. Raw |
1282 proof blocks are like ordinary proofs except that they do not prove |
1283 proof blocks are like ordinary proofs except that they do not prove |
1304 goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that |
1305 goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that |
1305 the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and |
1306 the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and |
1306 that each case $P_i$ implies the goal. Taken together, this proves the |
1307 that each case $P_i$ implies the goal. Taken together, this proves the |
1307 goal. The corresponding Isar proof pattern (for $n = 3$) is very handy:% |
1308 goal. The corresponding Isar proof pattern (for $n = 3$) is very handy:% |
1308 \end{isamarkuptext}% |
1309 \end{isamarkuptext}% |
|
1310 \isamarkuptrue% |
1309 % |
1311 % |
1310 \renewcommand{\isamarkupcmt}[1]{#1} |
1312 \renewcommand{\isamarkupcmt}[1]{#1} |
1311 % |
|
1312 \isadelimproof |
|
1313 % |
|
1314 \endisadelimproof |
|
1315 % |
|
1316 \isatagproof |
|
1317 \isamarkupfalse% |
1313 \isamarkupfalse% |
1318 \isacommand{proof}\ {\isacharminus}\isanewline |
1314 % |
1319 \ \ \isamarkupfalse% |
1315 \isadelimproof |
1320 \isacommand{have}\ {\isachardoublequote}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequote}\ \ % |
1316 % |
|
1317 \endisadelimproof |
|
1318 % |
|
1319 \isatagproof |
|
1320 \isacommand{proof}\isamarkupfalse% |
|
1321 \ {\isacharminus}\isanewline |
|
1322 \ \ \isacommand{have}\isamarkupfalse% |
|
1323 \ {\isachardoublequoteopen}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequoteclose}\ \isamarkupfalse% |
|
1324 \ % |
1321 \isamarkupcmt{\dots% |
1325 \isamarkupcmt{\dots% |
1322 } |
1326 } |
1323 \isanewline |
1327 \isanewline |
1324 \ \ \isamarkupfalse% |
1328 \ \ \isacommand{moreover}\isamarkupfalse% |
1325 \isacommand{moreover}\isanewline |
1329 \isanewline |
1326 \ \ \isamarkupfalse% |
1330 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse% |
1327 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse% |
1331 \ \isacommand{assume}\isamarkupfalse% |
1328 \isacommand{assume}\ P\isactrlisub {\isadigit{1}}\isanewline |
1332 \ P\isactrlisub {\isadigit{1}}\isanewline |
1329 \ \ \ \ % |
1333 \ \ \ \ % |
1330 \isamarkupcmt{\dots% |
1334 \isamarkupcmt{\dots% |
1331 } |
1335 } |
1332 \isanewline |
1336 \isanewline |
1333 \ \ \ \ \isamarkupfalse% |
1337 \ \ \ \ \isacommand{have}\isamarkupfalse% |
1334 \isacommand{have}\ {\isacharquery}thesis\ \ % |
1338 \ {\isacharquery}thesis\ \isamarkupfalse% |
|
1339 \ % |
1335 \isamarkupcmt{\dots% |
1340 \isamarkupcmt{\dots% |
1336 } |
1341 } |
1337 \ \isamarkupfalse% |
1342 \ \isacommand{{\isacharbraceright}}\isamarkupfalse% |
1338 \isacommand{{\isacharbraceright}}\isanewline |
1343 \isanewline |
1339 \ \ \isamarkupfalse% |
1344 \ \ \isacommand{moreover}\isamarkupfalse% |
1340 \isacommand{moreover}\isanewline |
1345 \isanewline |
1341 \ \ \isamarkupfalse% |
1346 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse% |
1342 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse% |
1347 \ \isacommand{assume}\isamarkupfalse% |
1343 \isacommand{assume}\ P\isactrlisub {\isadigit{2}}\isanewline |
1348 \ P\isactrlisub {\isadigit{2}}\isanewline |
1344 \ \ \ \ % |
1349 \ \ \ \ % |
1345 \isamarkupcmt{\dots% |
1350 \isamarkupcmt{\dots% |
1346 } |
1351 } |
1347 \isanewline |
1352 \isanewline |
1348 \ \ \ \ \isamarkupfalse% |
1353 \ \ \ \ \isacommand{have}\isamarkupfalse% |
1349 \isacommand{have}\ {\isacharquery}thesis\ \ % |
1354 \ {\isacharquery}thesis\ \isamarkupfalse% |
|
1355 \ % |
1350 \isamarkupcmt{\dots% |
1356 \isamarkupcmt{\dots% |
1351 } |
1357 } |
1352 \ \isamarkupfalse% |
1358 \ \isacommand{{\isacharbraceright}}\isamarkupfalse% |
1353 \isacommand{{\isacharbraceright}}\isanewline |
1359 \isanewline |
1354 \ \ \isamarkupfalse% |
1360 \ \ \isacommand{moreover}\isamarkupfalse% |
1355 \isacommand{moreover}\isanewline |
1361 \isanewline |
1356 \ \ \isamarkupfalse% |
1362 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse% |
1357 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse% |
1363 \ \isacommand{assume}\isamarkupfalse% |
1358 \isacommand{assume}\ P\isactrlisub {\isadigit{3}}\isanewline |
1364 \ P\isactrlisub {\isadigit{3}}\isanewline |
1359 \ \ \ \ % |
1365 \ \ \ \ % |
1360 \isamarkupcmt{\dots% |
1366 \isamarkupcmt{\dots% |
1361 } |
1367 } |
1362 \isanewline |
1368 \isanewline |
1363 \ \ \ \ \isamarkupfalse% |
1369 \ \ \ \ \isacommand{have}\isamarkupfalse% |
1364 \isacommand{have}\ {\isacharquery}thesis\ \ % |
1370 \ {\isacharquery}thesis\ \isamarkupfalse% |
|
1371 \ % |
1365 \isamarkupcmt{\dots% |
1372 \isamarkupcmt{\dots% |
1366 } |
1373 } |
1367 \ \isamarkupfalse% |
1374 \ \isacommand{{\isacharbraceright}}\isamarkupfalse% |
1368 \isacommand{{\isacharbraceright}}\isanewline |
1375 \isanewline |
1369 \ \ \isamarkupfalse% |
1376 \ \ \isacommand{ultimately}\isamarkupfalse% |
1370 \isacommand{ultimately}\ \isamarkupfalse% |
1377 \ \isacommand{show}\isamarkupfalse% |
1371 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
1378 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
1372 \isacommand{by}\ blast\isanewline |
1379 \ blast\isanewline |
1373 \isamarkupfalse% |
1380 \isacommand{qed}\isamarkupfalse% |
1374 \isacommand{qed}% |
1381 % |
1375 \endisatagproof |
1382 \endisatagproof |
1376 {\isafoldproof}% |
1383 {\isafoldproof}% |
1377 % |
1384 % |
1378 \isadelimproof |
1385 \isadelimproof |
1379 % |
1386 % |
1380 \endisadelimproof |
1387 \endisadelimproof |
1381 % |
1388 % |
1382 \renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
1389 \renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
1383 \isamarkuptrue% |
|
1384 % |
1390 % |
1385 \isamarkupsubsection{Further refinements% |
1391 \isamarkupsubsection{Further refinements% |
1386 } |
1392 } |
1387 \isamarkuptrue% |
1393 \isamarkuptrue% |
1388 % |
1394 % |
1434 Sometimes it is necessary to decorate a proposition with type |
1440 Sometimes it is necessary to decorate a proposition with type |
1435 constraints, as in Cantor's theorem above. These type constraints tend |
1441 constraints, as in Cantor's theorem above. These type constraints tend |
1436 to make the theorem less readable. The situation can be improved a |
1442 to make the theorem less readable. The situation can be improved a |
1437 little by combining the type constraint with an outer \isa{{\isasymAnd}}:% |
1443 little by combining the type constraint with an outer \isa{{\isasymAnd}}:% |
1438 \end{isamarkuptext}% |
1444 \end{isamarkuptext}% |
|
1445 \isamarkuptrue% |
|
1446 \isacommand{theorem}\isamarkupfalse% |
|
1447 \ {\isachardoublequoteopen}{\isasymAnd}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardot}\ {\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}% |
|
1448 \isadelimproof |
|
1449 % |
|
1450 \endisadelimproof |
|
1451 % |
|
1452 \isatagproof |
1439 \isamarkupfalse% |
1453 \isamarkupfalse% |
1440 \isacommand{theorem}\ {\isachardoublequote}{\isasymAnd}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardot}\ {\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequote}% |
1454 % |
1441 \isadelimproof |
1455 \endisatagproof |
1442 % |
1456 {\isafoldproof}% |
1443 \endisadelimproof |
1457 % |
1444 % |
1458 \isadelimproof |
1445 \isatagproof |
1459 % |
1446 % |
1460 \endisadelimproof |
1447 \endisatagproof |
|
1448 {\isafoldproof}% |
|
1449 % |
|
1450 \isadelimproof |
|
1451 % |
|
1452 \endisadelimproof |
|
1453 \isamarkuptrue% |
|
1454 % |
1461 % |
1455 \begin{isamarkuptext}% |
1462 \begin{isamarkuptext}% |
1456 \noindent However, now \isa{f} is bound and we need a |
1463 \noindent However, now \isa{f} is bound and we need a |
1457 \isakeyword{fix}~\isa{f} in the proof before we can refer to \isa{f}. |
1464 \isakeyword{fix}~\isa{f} in the proof before we can refer to \isa{f}. |
1458 This is avoided by \isakeyword{fixes}:% |
1465 This is avoided by \isakeyword{fixes}:% |
1459 \end{isamarkuptext}% |
1466 \end{isamarkuptext}% |
|
1467 \isamarkuptrue% |
|
1468 \isacommand{theorem}\isamarkupfalse% |
|
1469 \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}% |
|
1470 \isadelimproof |
|
1471 % |
|
1472 \endisadelimproof |
|
1473 % |
|
1474 \isatagproof |
1460 \isamarkupfalse% |
1475 \isamarkupfalse% |
1461 \isacommand{theorem}\ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequote}% |
1476 % |
1462 \isadelimproof |
1477 \endisatagproof |
1463 % |
1478 {\isafoldproof}% |
1464 \endisadelimproof |
1479 % |
1465 % |
1480 \isadelimproof |
1466 \isatagproof |
1481 % |
1467 % |
1482 \endisadelimproof |
1468 \endisatagproof |
|
1469 {\isafoldproof}% |
|
1470 % |
|
1471 \isadelimproof |
|
1472 % |
|
1473 \endisadelimproof |
|
1474 \isamarkuptrue% |
|
1475 % |
1483 % |
1476 \begin{isamarkuptext}% |
1484 \begin{isamarkuptext}% |
1477 \noindent |
1485 \noindent |
1478 Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:% |
1486 Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:% |
1479 \end{isamarkuptext}% |
1487 \end{isamarkuptext}% |
1480 \isamarkupfalse% |
1488 \isamarkuptrue% |
1481 \isacommand{lemma}\ comm{\isacharunderscore}mono{\isacharcolon}\isanewline |
1489 \isacommand{lemma}\isamarkupfalse% |
1482 \ \ \isakeyword{fixes}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\isanewline |
1490 \ comm{\isacharunderscore}mono{\isacharcolon}\isanewline |
1483 \ \ \ \ \ \ \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharplus}{\isacharplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
1491 \ \ \isakeyword{fixes}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isachargreater}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\isanewline |
1484 \ \ \isakeyword{assumes}\ comm{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}x\ y{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isacharplus}{\isacharplus}\ y\ {\isacharequal}\ y\ {\isacharplus}{\isacharplus}\ x{\isachardoublequote}\ \isakeyword{and}\isanewline |
1492 \ \ \ \ \ \ \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharplus}{\isacharplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
1485 \ \ \ \ \ \ \ \ \ \ mono{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ x\ {\isacharplus}{\isacharplus}\ z\ {\isachargreater}\ y\ {\isacharplus}{\isacharplus}\ z{\isachardoublequote}\isanewline |
1493 \ \ \isakeyword{assumes}\ comm{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isacharplus}{\isacharplus}\ y\ {\isacharequal}\ y\ {\isacharplus}{\isacharplus}\ x{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
1486 \ \ \isakeyword{shows}\ {\isachardoublequote}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequote}\isanewline |
1494 \ \ \ \ \ \ \ \ \ \ mono{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ x\ {\isacharplus}{\isacharplus}\ z\ {\isachargreater}\ y\ {\isacharplus}{\isacharplus}\ z{\isachardoublequoteclose}\isanewline |
1487 % |
1495 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequoteclose}\isanewline |
1488 \isadelimproof |
1496 % |
1489 % |
1497 \isadelimproof |
1490 \endisadelimproof |
1498 % |
1491 % |
1499 \endisadelimproof |
1492 \isatagproof |
1500 % |
1493 \isamarkupfalse% |
1501 \isatagproof |
1494 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}% |
1502 \isacommand{by}\isamarkupfalse% |
1495 \endisatagproof |
1503 {\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}% |
1496 {\isafoldproof}% |
1504 \endisatagproof |
1497 % |
1505 {\isafoldproof}% |
1498 \isadelimproof |
1506 % |
1499 % |
1507 \isadelimproof |
1500 \endisadelimproof |
1508 % |
1501 \isamarkuptrue% |
1509 \endisadelimproof |
1502 % |
1510 % |
1503 \begin{isamarkuptext}% |
1511 \begin{isamarkuptext}% |
1504 \noindent The concrete syntax is dropped at the end of the proof and the |
1512 \noindent The concrete syntax is dropped at the end of the proof and the |
1505 theorem becomes \begin{isabelle}% |
1513 theorem becomes \begin{isabelle}% |
1506 {\isasymlbrakk}{\isasymAnd}x\ y{\isachardot}\ {\isacharquery}f\ x\ y\ {\isacharequal}\ {\isacharquery}f\ y\ x{\isacharsemicolon}\isanewline |
1514 {\isasymlbrakk}{\isasymAnd}x\ y{\isachardot}\ {\isacharquery}f\ x\ y\ {\isacharequal}\ {\isacharquery}f\ y\ x{\isacharsemicolon}\isanewline |
1517 % |
1525 % |
1518 \begin{isamarkuptext}% |
1526 \begin{isamarkuptext}% |
1519 The \isakeyword{obtain} construct can introduce multiple |
1527 The \isakeyword{obtain} construct can introduce multiple |
1520 witnesses and propositions as in the following proof fragment:% |
1528 witnesses and propositions as in the following proof fragment:% |
1521 \end{isamarkuptext}% |
1529 \end{isamarkuptext}% |
1522 \isamarkupfalse% |
1530 \isamarkuptrue% |
1523 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}R{\isachardoublequote}\isanewline |
1531 \isacommand{lemma}\isamarkupfalse% |
1524 % |
1532 \ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}R{\isachardoublequoteclose}\isanewline |
1525 \isadelimproof |
1533 % |
1526 % |
1534 \isadelimproof |
1527 \endisadelimproof |
1535 % |
1528 % |
1536 \endisadelimproof |
1529 \isatagproof |
1537 % |
1530 \isamarkupfalse% |
1538 \isatagproof |
1531 \isacommand{proof}\ {\isacharminus}\isanewline |
1539 \isacommand{proof}\isamarkupfalse% |
1532 \ \ \isamarkupfalse% |
1540 \ {\isacharminus}\isanewline |
1533 \isacommand{from}\ A\ \isamarkupfalse% |
1541 \ \ \isacommand{from}\isamarkupfalse% |
1534 \isacommand{obtain}\ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequote}Q\ x\ y{\isachardoublequote}\ \ \isamarkupfalse% |
1542 \ A\ \isacommand{obtain}\isamarkupfalse% |
1535 \isacommand{by}\ blast% |
1543 \ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequoteopen}P\ x\ y{\isachardoublequoteclose}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequoteopen}Q\ x\ y{\isachardoublequoteclose}\ \ \isacommand{by}\isamarkupfalse% |
1536 \endisatagproof |
1544 \ blast\isamarkupfalse% |
1537 {\isafoldproof}% |
1545 % |
1538 % |
1546 \endisatagproof |
1539 \isadelimproof |
1547 {\isafoldproof}% |
1540 % |
1548 % |
1541 \endisadelimproof |
1549 \isadelimproof |
1542 \isamarkuptrue% |
1550 % |
|
1551 \endisadelimproof |
1543 % |
1552 % |
1544 \begin{isamarkuptext}% |
1553 \begin{isamarkuptext}% |
1545 Remember also that one does not even need to start with a formula |
1554 Remember also that one does not even need to start with a formula |
1546 containing \isa{{\isasymexists}} as we saw in the proof of Cantor's theorem.% |
1555 containing \isa{{\isasymexists}} as we saw in the proof of Cantor's theorem.% |
1547 \end{isamarkuptext}% |
1556 \end{isamarkuptext}% |
1554 \begin{isamarkuptext}% |
1563 \begin{isamarkuptext}% |
1555 Finally, whole ``scripts'' (tactic-based proofs in the style of |
1564 Finally, whole ``scripts'' (tactic-based proofs in the style of |
1556 \cite{LNCS2283}) may appear in the leaves of the proof tree, although this is |
1565 \cite{LNCS2283}) may appear in the leaves of the proof tree, although this is |
1557 best avoided. Here is a contrived example:% |
1566 best avoided. Here is a contrived example:% |
1558 \end{isamarkuptext}% |
1567 \end{isamarkuptext}% |
1559 \isamarkupfalse% |
1568 \isamarkuptrue% |
1560 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline |
1569 \isacommand{lemma}\isamarkupfalse% |
1561 % |
1570 \ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\isanewline |
1562 \isadelimproof |
1571 % |
1563 % |
1572 \isadelimproof |
1564 \endisadelimproof |
1573 % |
1565 % |
1574 \endisadelimproof |
1566 \isatagproof |
1575 % |
1567 \isamarkupfalse% |
1576 \isatagproof |
1568 \isacommand{proof}\isanewline |
1577 \isacommand{proof}\isamarkupfalse% |
1569 \ \ \isamarkupfalse% |
1578 \isanewline |
1570 \isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline |
1579 \ \ \isacommand{assume}\isamarkupfalse% |
1571 \ \ \isamarkupfalse% |
1580 \ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline |
1572 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline |
1581 \ \ \isacommand{show}\isamarkupfalse% |
1573 \ \ \ \ \isamarkupfalse% |
1582 \ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\isanewline |
1574 \isacommand{apply}{\isacharparenleft}rule\ impI{\isacharparenright}\isanewline |
1583 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
1575 \ \ \ \ \isamarkupfalse% |
1584 {\isacharparenleft}rule\ impI{\isacharparenright}\isanewline |
1576 \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline |
1585 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
1577 \ \ \ \ \isamarkupfalse% |
1586 {\isacharparenleft}erule\ impE{\isacharparenright}\isanewline |
1578 \isacommand{apply}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline |
1587 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
1579 \ \ \ \ \isamarkupfalse% |
1588 {\isacharparenleft}rule\ a{\isacharparenright}\isanewline |
1580 \isacommand{apply}\ assumption\isanewline |
1589 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
1581 \ \ \ \ \isamarkupfalse% |
1590 \ assumption\isanewline |
1582 \isacommand{done}\isanewline |
1591 \ \ \ \ \isacommand{done}\isamarkupfalse% |
1583 \isamarkupfalse% |
1592 \isanewline |
1584 \isacommand{qed}% |
1593 \isacommand{qed}\isamarkupfalse% |
1585 \endisatagproof |
1594 % |
1586 {\isafoldproof}% |
1595 \endisatagproof |
1587 % |
1596 {\isafoldproof}% |
1588 \isadelimproof |
1597 % |
1589 % |
1598 \isadelimproof |
1590 \endisadelimproof |
1599 % |
1591 \isamarkuptrue% |
1600 \endisadelimproof |
1592 % |
1601 % |
1593 \begin{isamarkuptext}% |
1602 \begin{isamarkuptext}% |
1594 \noindent You may need to resort to this technique if an |
1603 \noindent You may need to resort to this technique if an |
1595 automatic step fails to prove the desired proposition. |
1604 automatic step fails to prove the desired proposition. |
1596 |
1605 |
1597 When converting a proof from tactic-style into Isar you can proceed |
1606 When converting a proof from tactic-style into Isar you can proceed |
1598 in a top-down manner: parts of the proof can be left in script form |
1607 in a top-down manner: parts of the proof can be left in script form |
1599 while the outer structure is already expressed in Isar.% |
1608 while the outer structure is already expressed in Isar.% |
1600 \end{isamarkuptext}% |
1609 \end{isamarkuptext}% |
|
1610 \isamarkuptrue% |
1601 % |
1611 % |
1602 \isadelimtheory |
1612 \isadelimtheory |
1603 % |
1613 % |
1604 \endisadelimtheory |
1614 \endisadelimtheory |
1605 % |
1615 % |
1606 \isatagtheory |
1616 \isatagtheory |
|
1617 \isamarkupfalse% |
1607 % |
1618 % |
1608 \endisatagtheory |
1619 \endisatagtheory |
1609 {\isafoldtheory}% |
1620 {\isafoldtheory}% |
1610 % |
1621 % |
1611 \isadelimtheory |
1622 \isadelimtheory |