author | boehmes |
Tue, 07 Dec 2010 15:44:38 +0100 | |
changeset 41064 | 0c447a17770a |
parent 32834 | a4e0b8d88f28 |
permissions | -rw-r--r-- |
17914 | 1 |
(*<*)theory Logic imports Main begin(*>*) |
13999 | 2 |
|
3 |
section{*Logic \label{sec:Logic}*} |
|
4 |
||
5 |
subsection{*Propositional logic*} |
|
6 |
||
7 |
subsubsection{*Introduction rules*} |
|
8 |
||
9 |
text{* We start with a really trivial toy proof to introduce the basic |
|
10 |
features of structured proofs. *} |
|
11 |
lemma "A \<longrightarrow> A" |
|
12 |
proof (rule impI) |
|
13 |
assume a: "A" |
|
14 |
show "A" by(rule a) |
|
15 |
qed |
|
16 |
text{*\noindent |
|
17 |
The operational reading: the \isakeyword{assume}-\isakeyword{show} |
|
18 |
block proves @{prop"A \<Longrightarrow> A"} (@{term a} is a degenerate rule (no |
|
19 |
assumptions) that proves @{term A} outright), which rule |
|
20 |
@{thm[source]impI} (@{thm impI}) turns into the desired @{prop"A \<longrightarrow> |
|
21 |
A"}. However, this text is much too detailed for comfort. Therefore |
|
22 |
Isar implements the following principle: \begin{quote}\em Command |
|
23 |
\isakeyword{proof} automatically tries to select an introduction rule |
|
24 |
based on the goal and a predefined list of rules. \end{quote} Here |
|
25 |
@{thm[source]impI} is applied automatically: *} |
|
26 |
||
27 |
lemma "A \<longrightarrow> A" |
|
28 |
proof |
|
29 |
assume a: A |
|
30 |
show A by(rule a) |
|
31 |
qed |
|
32 |
||
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
29298
diff
changeset
|
33 |
text{*\noindent As you see above, single-identifier formulae such as @{term A} |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
29298
diff
changeset
|
34 |
need not be enclosed in double quotes. However, we will continue to do so for |
13999 | 35 |
uniformity. |
36 |
||
29298 | 37 |
Instead of applying fact @{text a} via the @{text rule} method, we can |
38 |
also push it directly onto our goal. The proof is then immediate, |
|
39 |
which is formally written as ``.'' in Isar: *} |
|
13999 | 40 |
lemma "A \<longrightarrow> A" |
41 |
proof |
|
29298 | 42 |
assume a: "A" |
43 |
from a show "A" . |
|
13999 | 44 |
qed |
45 |
||
29298 | 46 |
text{* We can also push several facts towards a goal, and put another |
47 |
rule in between to establish some result that is one step further |
|
48 |
removed. We illustrate this by introducing a trivial conjunction: *} |
|
13999 | 49 |
lemma "A \<longrightarrow> A \<and> A" |
50 |
proof |
|
29298 | 51 |
assume a: "A" |
52 |
from a and a show "A \<and> A" by(rule conjI) |
|
13999 | 53 |
qed |
54 |
text{*\noindent Rule @{thm[source]conjI} is of course @{thm conjI}. |
|
55 |
||
56 |
Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} |
|
29298 | 57 |
can be abbreviated to ``..'' if \emph{name} refers to one of the |
13999 | 58 |
predefined introduction rules (or elimination rules, see below): *} |
59 |
||
60 |
lemma "A \<longrightarrow> A \<and> A" |
|
61 |
proof |
|
29298 | 62 |
assume a: "A" |
63 |
from a and a show "A \<and> A" .. |
|
13999 | 64 |
qed |
65 |
text{*\noindent |
|
66 |
This is what happens: first the matching introduction rule @{thm[source]conjI} |
|
29298 | 67 |
is applied (first ``.''), the remaining problem is solved immediately (second ``.''). *} |
13999 | 68 |
|
69 |
subsubsection{*Elimination rules*} |
|
70 |
||
71 |
text{*A typical elimination rule is @{thm[source]conjE}, $\land$-elimination: |
|
72 |
@{thm[display,indent=5]conjE} In the following proof it is applied |
|
73 |
by hand, after its first (\emph{major}) premise has been eliminated via |
|
29298 | 74 |
@{text"[OF ab]"}: *} |
13999 | 75 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
76 |
proof |
|
29298 | 77 |
assume ab: "A \<and> B" |
13999 | 78 |
show "B \<and> A" |
29298 | 79 |
proof (rule conjE[OF ab]) -- {*@{text"conjE[OF ab]"}: @{thm conjE[OF ab]} *} |
80 |
assume a: "A" and b: "B" |
|
81 |
from b and a show ?thesis .. |
|
13999 | 82 |
qed |
83 |
qed |
|
84 |
text{*\noindent Note that the term @{text"?thesis"} always stands for the |
|
85 |
``current goal'', i.e.\ the enclosing \isakeyword{show} (or |
|
86 |
\isakeyword{have}) statement. |
|
87 |
||
88 |
This is too much proof text. Elimination rules should be selected |
|
89 |
automatically based on their major premise, the formula or rather connective |
|
90 |
to be eliminated. In Isar they are triggered by facts being fed |
|
91 |
\emph{into} a proof. Syntax: |
|
92 |
\begin{center} |
|
93 |
\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof} |
|
94 |
\end{center} |
|
95 |
where \emph{fact} stands for the name of a previously proved |
|
96 |
proposition, e.g.\ an assumption, an intermediate result or some global |
|
97 |
theorem, which may also be modified with @{text OF} etc. |
|
98 |
The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it |
|
99 |
how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof}, |
|
100 |
an elimination rule (from a predefined list) is applied |
|
101 |
whose first premise is solved by the \emph{fact}. Thus the proof above |
|
102 |
is equivalent to the following one: *} |
|
103 |
||
104 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
105 |
proof |
|
29298 | 106 |
assume ab: "A \<and> B" |
107 |
from ab show "B \<and> A" |
|
13999 | 108 |
proof |
29298 | 109 |
assume a: "A" and b: "B" |
110 |
from b and a show ?thesis .. |
|
13999 | 111 |
qed |
112 |
qed |
|
113 |
||
114 |
text{* Now we come to a second important principle: |
|
115 |
\begin{quote}\em |
|
116 |
Try to arrange the sequence of propositions in a UNIX-like pipe, |
|
117 |
such that the proof of each proposition builds on the previous proposition. |
|
118 |
\end{quote} |
|
119 |
The previous proposition can be referred to via the fact @{text this}. |
|
29298 | 120 |
This greatly reduces the need for explicit naming of propositions. We also |
121 |
rearrange the additional inner assumptions into proper order for immediate use: |
|
13999 | 122 |
*} |
123 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
124 |
proof |
|
125 |
assume "A \<and> B" |
|
126 |
from this show "B \<and> A" |
|
127 |
proof |
|
29298 | 128 |
assume "B" "A" |
129 |
from this show ?thesis .. |
|
13999 | 130 |
qed |
131 |
qed |
|
132 |
||
133 |
text{*\noindent Because of the frequency of \isakeyword{from}~@{text |
|
134 |
this}, Isar provides two abbreviations: |
|
135 |
\begin{center} |
|
136 |
\begin{tabular}{r@ {\quad=\quad}l} |
|
137 |
\isakeyword{then} & \isakeyword{from} @{text this} \\ |
|
138 |
\isakeyword{thus} & \isakeyword{then} \isakeyword{show} |
|
139 |
\end{tabular} |
|
140 |
\end{center} |
|
141 |
||
142 |
Here is an alternative proof that operates purely by forward reasoning: *} |
|
143 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
144 |
proof |
|
145 |
assume ab: "A \<and> B" |
|
146 |
from ab have a: "A" .. |
|
147 |
from ab have b: "B" .. |
|
148 |
from b a show "B \<and> A" .. |
|
149 |
qed |
|
150 |
||
151 |
text{*\noindent It is worth examining this text in detail because it |
|
152 |
exhibits a number of new concepts. For a start, it is the first time |
|
153 |
we have proved intermediate propositions (\isakeyword{have}) on the |
|
154 |
way to the final \isakeyword{show}. This is the norm in nontrivial |
|
155 |
proofs where one cannot bridge the gap between the assumptions and the |
|
156 |
conclusion in one step. To understand how the proof works we need to |
|
25412 | 157 |
explain more Isar details: |
158 |
\begin{itemize} |
|
159 |
\item |
|
13999 | 160 |
Method @{text rule} can be given a list of rules, in which case |
161 |
@{text"(rule"}~\textit{rules}@{text")"} applies the first matching |
|
25412 | 162 |
rule in the list \textit{rules}. |
163 |
\item Command \isakeyword{from} can be |
|
13999 | 164 |
followed by any number of facts. Given \isakeyword{from}~@{text |
165 |
f}$_1$~\dots~@{text f}$_n$, the proof step |
|
166 |
@{text"(rule"}~\textit{rules}@{text")"} following a \isakeyword{have} |
|
167 |
or \isakeyword{show} searches \textit{rules} for a rule whose first |
|
168 |
$n$ premises can be proved by @{text f}$_1$~\dots~@{text f}$_n$ in the |
|
25412 | 169 |
given order. |
170 |
\item ``..'' is short for |
|
171 |
@{text"by(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnote{or |
|
172 |
merely @{text"(rule"}~\textit{intro-rules}@{text")"} if there are no facts |
|
173 |
fed into the proof}, where \textit{elim-rules} and \textit{intro-rules} |
|
174 |
are the predefined elimination and introduction rule. Thus |
|
175 |
elimination rules are tried first (if there are incoming facts). |
|
176 |
\end{itemize} |
|
177 |
Hence in the above proof both \isakeyword{have}s are proved via |
|
13999 | 178 |
@{thm[source]conjE} triggered by \isakeyword{from}~@{text ab} whereas |
179 |
in the \isakeyword{show} step no elimination rule is applicable and |
|
180 |
the proof succeeds with @{thm[source]conjI}. The latter would fail had |
|
181 |
we written \isakeyword{from}~@{text"a b"} instead of |
|
182 |
\isakeyword{from}~@{text"b a"}. |
|
183 |
||
25412 | 184 |
A plain \isakeyword{proof} with no argument is short for |
185 |
\isakeyword{proof}~@{text"(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnotemark[1]. |
|
186 |
This means that the matching rule is selected by the incoming facts and the goal exactly as just explained. |
|
13999 | 187 |
|
25412 | 188 |
Although we have only seen a few introduction and elimination rules so |
13999 | 189 |
far, Isar's predefined rules include all the usual natural deduction |
190 |
rules. We conclude our exposition of propositional logic with an extended |
|
191 |
example --- which rules are used implicitly where? *} |
|
192 |
lemma "\<not> (A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B" |
|
193 |
proof |
|
194 |
assume n: "\<not> (A \<and> B)" |
|
195 |
show "\<not> A \<or> \<not> B" |
|
196 |
proof (rule ccontr) |
|
197 |
assume nn: "\<not> (\<not> A \<or> \<not> B)" |
|
198 |
have "\<not> A" |
|
199 |
proof |
|
29298 | 200 |
assume a: "A" |
13999 | 201 |
have "\<not> B" |
202 |
proof |
|
29298 | 203 |
assume b: "B" |
204 |
from a and b have "A \<and> B" .. |
|
13999 | 205 |
with n show False .. |
206 |
qed |
|
207 |
hence "\<not> A \<or> \<not> B" .. |
|
208 |
with nn show False .. |
|
209 |
qed |
|
210 |
hence "\<not> A \<or> \<not> B" .. |
|
211 |
with nn show False .. |
|
212 |
qed |
|
213 |
qed |
|
214 |
text{*\noindent |
|
215 |
Rule @{thm[source]ccontr} (``classical contradiction'') is |
|
216 |
@{thm ccontr[no_vars]}. |
|
217 |
Apart from demonstrating the strangeness of classical |
|
218 |
arguments by contradiction, this example also introduces two new |
|
219 |
abbreviations: |
|
220 |
\begin{center} |
|
221 |
\begin{tabular}{l@ {\quad=\quad}l} |
|
222 |
\isakeyword{hence} & \isakeyword{then} \isakeyword{have} \\ |
|
223 |
\isakeyword{with}~\emph{facts} & |
|
224 |
\isakeyword{from}~\emph{facts} @{text this} |
|
225 |
\end{tabular} |
|
226 |
\end{center} |
|
227 |
*} |
|
228 |
||
19840 | 229 |
|
13999 | 230 |
subsection{*Avoiding duplication*} |
231 |
||
232 |
text{* So far our examples have been a bit unnatural: normally we want to |
|
233 |
prove rules expressed with @{text"\<Longrightarrow>"}, not @{text"\<longrightarrow>"}. Here is an example: |
|
234 |
*} |
|
235 |
lemma "A \<and> B \<Longrightarrow> B \<and> A" |
|
236 |
proof |
|
237 |
assume "A \<and> B" thus "B" .. |
|
238 |
next |
|
239 |
assume "A \<and> B" thus "A" .. |
|
240 |
qed |
|
241 |
text{*\noindent The \isakeyword{proof} always works on the conclusion, |
|
242 |
@{prop"B \<and> A"} in our case, thus selecting $\land$-introduction. Hence |
|
243 |
we must show @{prop B} and @{prop A}; both are proved by |
|
244 |
$\land$-elimination and the proofs are separated by \isakeyword{next}: |
|
245 |
\begin{description} |
|
246 |
\item[\isakeyword{next}] deals with multiple subgoals. For example, |
|
247 |
when showing @{term"A \<and> B"} we need to show both @{term A} and @{term |
|
248 |
B}. Each subgoal is proved separately, in \emph{any} order. The |
|
249 |
individual proofs are separated by \isakeyword{next}. \footnote{Each |
|
250 |
\isakeyword{show} must prove one of the pending subgoals. If a |
|
251 |
\isakeyword{show} matches multiple subgoals, e.g.\ if the subgoals |
|
252 |
contain ?-variables, the first one is proved. Thus the order in which |
|
253 |
the subgoals are proved can matter --- see |
|
254 |
\S\ref{sec:CaseDistinction} for an example.} |
|
255 |
||
256 |
Strictly speaking \isakeyword{next} is only required if the subgoals |
|
257 |
are proved in different assumption contexts which need to be |
|
258 |
separated, which is not the case above. For clarity we |
|
259 |
have employed \isakeyword{next} anyway and will continue to do so. |
|
260 |
\end{description} |
|
261 |
||
262 |
This is all very well as long as formulae are small. Let us now look at some |
|
263 |
devices to avoid repeating (possibly large) formulae. A very general method |
|
264 |
is pattern matching: *} |
|
265 |
||
266 |
lemma "large_A \<and> large_B \<Longrightarrow> large_B \<and> large_A" |
|
267 |
(is "?AB \<Longrightarrow> ?B \<and> ?A") |
|
268 |
proof |
|
269 |
assume "?AB" thus "?B" .. |
|
270 |
next |
|
271 |
assume "?AB" thus "?A" .. |
|
272 |
qed |
|
273 |
text{*\noindent Any formula may be followed by |
|
274 |
@{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern |
|
275 |
to be matched against the formula, instantiating the @{text"?"}-variables in |
|
276 |
the pattern. Subsequent uses of these variables in other terms causes |
|
277 |
them to be replaced by the terms they stand for. |
|
278 |
||
279 |
We can simplify things even more by stating the theorem by means of the |
|
280 |
\isakeyword{assumes} and \isakeyword{shows} elements which allow direct |
|
281 |
naming of assumptions: *} |
|
282 |
||
29298 | 283 |
lemma assumes ab: "large_A \<and> large_B" |
13999 | 284 |
shows "large_B \<and> large_A" (is "?B \<and> ?A") |
285 |
proof |
|
29298 | 286 |
from ab show "?B" .. |
13999 | 287 |
next |
29298 | 288 |
from ab show "?A" .. |
13999 | 289 |
qed |
290 |
text{*\noindent Note the difference between @{text ?AB}, a term, and |
|
29298 | 291 |
@{text ab}, a fact. |
13999 | 292 |
|
293 |
Finally we want to start the proof with $\land$-elimination so we |
|
294 |
don't have to perform it twice, as above. Here is a slick way to |
|
295 |
achieve this: *} |
|
296 |
||
29298 | 297 |
lemma assumes ab: "large_A \<and> large_B" |
13999 | 298 |
shows "large_B \<and> large_A" (is "?B \<and> ?A") |
29298 | 299 |
using ab |
13999 | 300 |
proof |
29298 | 301 |
assume "?B" "?A" thus ?thesis .. |
13999 | 302 |
qed |
303 |
text{*\noindent Command \isakeyword{using} can appear before a proof |
|
29298 | 304 |
and adds further facts to those piped into the proof. Here @{text ab} |
13999 | 305 |
is the only such fact and it triggers $\land$-elimination. Another |
306 |
frequent idiom is as follows: |
|
307 |
\begin{center} |
|
308 |
\isakeyword{from} \emph{major-facts}~ |
|
309 |
\isakeyword{show} \emph{proposition}~ |
|
310 |
\isakeyword{using} \emph{minor-facts}~ |
|
311 |
\emph{proof} |
|
312 |
\end{center} |
|
313 |
||
314 |
Sometimes it is necessary to suppress the implicit application of rules in a |
|
27171 | 315 |
\isakeyword{proof}. For example \isakeyword{show(s)}~@{prop[source]"P \<or> Q"} |
316 |
would trigger $\lor$-introduction, requiring us to prove @{prop P}, which may |
|
317 |
not be what we had in mind. |
|
318 |
A simple ``@{text"-"}'' prevents this \emph{faux pas}: *} |
|
13999 | 319 |
|
29298 | 320 |
lemma assumes ab: "A \<or> B" shows "B \<or> A" |
13999 | 321 |
proof - |
29298 | 322 |
from ab show ?thesis |
13999 | 323 |
proof |
29298 | 324 |
assume A thus ?thesis .. |
13999 | 325 |
next |
29298 | 326 |
assume B thus ?thesis .. |
13999 | 327 |
qed |
328 |
qed |
|
25412 | 329 |
text{*\noindent Alternatively one can feed @{prop"A \<or> B"} directly |
330 |
into the proof, thus triggering the elimination rule: *} |
|
29298 | 331 |
lemma assumes ab: "A \<or> B" shows "B \<or> A" |
332 |
using ab |
|
25412 | 333 |
proof |
29298 | 334 |
assume A thus ?thesis .. |
25412 | 335 |
next |
29298 | 336 |
assume B thus ?thesis .. |
25412 | 337 |
qed |
338 |
text{* \noindent Remember that eliminations have priority over |
|
339 |
introductions. |
|
13999 | 340 |
|
25412 | 341 |
\subsection{Avoiding names} |
342 |
||
343 |
Too many names can easily clutter a proof. We already learned |
|
19840 | 344 |
about @{text this} as a means of avoiding explicit names. Another |
345 |
handy device is to refer to a fact not by name but by contents: for |
|
346 |
example, writing @{text "`A \<or> B`"} (enclosing the formula in back quotes) |
|
347 |
refers to the fact @{text"A \<or> B"} |
|
348 |
without the need to name it. Here is a simple example, a revised version |
|
349 |
of the previous proof *} |
|
350 |
||
351 |
lemma assumes "A \<or> B" shows "B \<or> A" |
|
25412 | 352 |
using `A \<or> B` |
19840 | 353 |
(*<*)oops(*>*) |
354 |
text{*\noindent which continues as before. |
|
355 |
||
356 |
Clearly, this device of quoting facts by contents is only advisable |
|
357 |
for small formulae. In such cases it is superior to naming because the |
|
358 |
reader immediately sees what the fact is without needing to search for |
|
25412 | 359 |
it in the preceding proof text. |
360 |
||
361 |
The assumptions of a lemma can also be referred to via their |
|
362 |
predefined name @{text assms}. Hence the @{text"`A \<or> B`"} in the |
|
363 |
previous proof can also be replaced by @{text assms}. Note that @{text |
|
364 |
assms} refers to the list of \emph{all} assumptions. To pick out a |
|
365 |
specific one, say the second, write @{text"assms(2)"}. |
|
366 |
||
367 |
This indexing notation $name(.)$ works for any $name$ that stands for |
|
368 |
a list of facts, for example $f$@{text".simps"}, the equations of the |
|
369 |
recursively defined function $f$. You may also select sublists by writing |
|
370 |
$name(2-3)$. |
|
13999 | 371 |
|
25412 | 372 |
Above we recommended the UNIX-pipe model (i.e. @{text this}) to avoid |
373 |
the need to name propositions. But frequently we needed to feed more |
|
374 |
than one previously derived fact into a proof step. Then the UNIX-pipe |
|
375 |
model appears to break down and we need to name the different facts to |
|
376 |
refer to them. But this can be avoided: *} |
|
377 |
lemma assumes "A \<and> B" shows "B \<and> A" |
|
378 |
proof - |
|
379 |
from `A \<and> B` have "B" .. |
|
380 |
moreover |
|
381 |
from `A \<and> B` have "A" .. |
|
382 |
ultimately show "B \<and> A" .. |
|
383 |
qed |
|
384 |
text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term |
|
385 |
An} into a sequence by separating their proofs with |
|
386 |
\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands |
|
387 |
for \isakeyword{from}~@{term A1}~\dots~@{term An}. This avoids having to |
|
388 |
introduce names for all of the sequence elements. |
|
13999 | 389 |
|
25412 | 390 |
|
391 |
\subsection{Predicate calculus} |
|
392 |
||
393 |
Command \isakeyword{fix} introduces new local variables into a |
|
13999 | 394 |
proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to @{text"\<And>"} |
395 |
(the universal quantifier at the |
|
396 |
meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to |
|
397 |
@{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are |
|
398 |
applied implicitly: *} |
|
399 |
lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P(f x)" |
|
400 |
proof --"@{thm[source]allI}: @{thm allI}" |
|
401 |
fix a |
|
402 |
from P show "P(f a)" .. --"@{thm[source]allE}: @{thm allE}" |
|
403 |
qed |
|
404 |
text{*\noindent Note that in the proof we have chosen to call the bound |
|
405 |
variable @{term a} instead of @{term x} merely to show that the choice of |
|
406 |
local names is irrelevant. |
|
407 |
||
408 |
Next we look at @{text"\<exists>"} which is a bit more tricky. |
|
409 |
*} |
|
410 |
||
411 |
lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y" |
|
412 |
proof - |
|
413 |
from Pf show ?thesis |
|
414 |
proof -- "@{thm[source]exE}: @{thm exE}" |
|
415 |
fix x |
|
416 |
assume "P(f x)" |
|
29298 | 417 |
thus ?thesis .. -- "@{thm[source]exI}: @{thm exI}" |
13999 | 418 |
qed |
419 |
qed |
|
420 |
text{*\noindent Explicit $\exists$-elimination as seen above can become |
|
421 |
cumbersome in practice. The derived Isar language element |
|
422 |
\isakeyword{obtain} provides a more appealing form of generalised |
|
423 |
existence reasoning: *} |
|
424 |
||
425 |
lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y" |
|
426 |
proof - |
|
427 |
from Pf obtain x where "P(f x)" .. |
|
428 |
thus "\<exists>y. P y" .. |
|
429 |
qed |
|
430 |
text{*\noindent Note how the proof text follows the usual mathematical style |
|
431 |
of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$ |
|
432 |
as a new local variable. Technically, \isakeyword{obtain} is similar to |
|
433 |
\isakeyword{fix} and \isakeyword{assume} together with a soundness proof of |
|
434 |
the elimination involved. |
|
435 |
||
436 |
Here is a proof of a well known tautology. |
|
437 |
Which rule is used where? *} |
|
438 |
||
439 |
lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y" |
|
440 |
proof |
|
441 |
fix y |
|
442 |
from ex obtain x where "\<forall>y. P x y" .. |
|
443 |
hence "P x y" .. |
|
444 |
thus "\<exists>x. P x y" .. |
|
445 |
qed |
|
446 |
||
447 |
subsection{*Making bigger steps*} |
|
448 |
||
449 |
text{* So far we have confined ourselves to single step proofs. Of course |
|
450 |
powerful automatic methods can be used just as well. Here is an example, |
|
451 |
Cantor's theorem that there is no surjective function from a set to its |
|
452 |
powerset: *} |
|
453 |
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
|
454 |
proof |
|
455 |
let ?S = "{x. x \<notin> f x}" |
|
456 |
show "?S \<notin> range f" |
|
457 |
proof |
|
458 |
assume "?S \<in> range f" |
|
19840 | 459 |
then obtain y where "?S = f y" .. |
13999 | 460 |
show False |
461 |
proof cases |
|
462 |
assume "y \<in> ?S" |
|
19840 | 463 |
with `?S = f y` show False by blast |
13999 | 464 |
next |
465 |
assume "y \<notin> ?S" |
|
19840 | 466 |
with `?S = f y` show False by blast |
13999 | 467 |
qed |
468 |
qed |
|
469 |
qed |
|
470 |
text{*\noindent |
|
471 |
For a start, the example demonstrates two new constructs: |
|
472 |
\begin{itemize} |
|
473 |
\item \isakeyword{let} introduces an abbreviation for a term, in our case |
|
474 |
the witness for the claim. |
|
475 |
\item Proof by @{text"cases"} starts a proof by cases. Note that it remains |
|
476 |
implicit what the two cases are: it is merely expected that the two subproofs |
|
477 |
prove @{text"P \<Longrightarrow> ?thesis"} and @{text"\<not>P \<Longrightarrow> ?thesis"} (in that order) |
|
478 |
for some @{term P}. |
|
479 |
\end{itemize} |
|
480 |
If you wonder how to \isakeyword{obtain} @{term y}: |
|
481 |
via the predefined elimination rule @{thm rangeE[no_vars]}. |
|
482 |
||
483 |
Method @{text blast} is used because the contradiction does not follow easily |
|
484 |
by just a single rule. If you find the proof too cryptic for human |
|
485 |
consumption, here is a more detailed version; the beginning up to |
|
486 |
\isakeyword{obtain} stays unchanged. *} |
|
487 |
||
488 |
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
|
489 |
proof |
|
490 |
let ?S = "{x. x \<notin> f x}" |
|
491 |
show "?S \<notin> range f" |
|
492 |
proof |
|
493 |
assume "?S \<in> range f" |
|
19840 | 494 |
then obtain y where "?S = f y" .. |
13999 | 495 |
show False |
496 |
proof cases |
|
497 |
assume "y \<in> ?S" |
|
498 |
hence "y \<notin> f y" by simp |
|
19840 | 499 |
hence "y \<notin> ?S" by(simp add: `?S = f y`) |
29298 | 500 |
with `y \<in> ?S` show False by contradiction |
13999 | 501 |
next |
502 |
assume "y \<notin> ?S" |
|
503 |
hence "y \<in> f y" by simp |
|
19840 | 504 |
hence "y \<in> ?S" by(simp add: `?S = f y`) |
29298 | 505 |
with `y \<notin> ?S` show False by contradiction |
13999 | 506 |
qed |
507 |
qed |
|
508 |
qed |
|
509 |
text{*\noindent Method @{text contradiction} succeeds if both $P$ and |
|
510 |
$\neg P$ are among the assumptions and the facts fed into that step, in any order. |
|
511 |
||
512 |
As it happens, Cantor's theorem can be proved automatically by best-first |
|
513 |
search. Depth-first search would diverge, but best-first search successfully |
|
514 |
navigates through the large search space: |
|
515 |
*} |
|
516 |
||
517 |
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
|
518 |
by best |
|
519 |
(* Of course this only works in the context of HOL's carefully |
|
520 |
constructed introduction and elimination rules for set theory.*) |
|
521 |
||
522 |
subsection{*Raw proof blocks*} |
|
523 |
||
524 |
text{* Although we have shown how to employ powerful automatic methods like |
|
525 |
@{text blast} to achieve bigger proof steps, there may still be the |
|
526 |
tendency to use the default introduction and elimination rules to |
|
527 |
decompose goals and facts. This can lead to very tedious proofs: |
|
528 |
*} |
|
529 |
lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y" |
|
530 |
proof |
|
531 |
fix x show "\<forall>y. A x y \<and> B x y \<longrightarrow> C x y" |
|
532 |
proof |
|
533 |
fix y show "A x y \<and> B x y \<longrightarrow> C x y" |
|
534 |
proof |
|
535 |
assume "A x y \<and> B x y" |
|
536 |
show "C x y" sorry |
|
537 |
qed |
|
538 |
qed |
|
539 |
qed |
|
540 |
text{*\noindent Since we are only interested in the decomposition and not the |
|
541 |
actual proof, the latter has been replaced by |
|
542 |
\isakeyword{sorry}. Command \isakeyword{sorry} proves anything but is |
|
543 |
only allowed in quick and dirty mode, the default interactive mode. It |
|
544 |
is very convenient for top down proof development. |
|
545 |
||
546 |
Luckily we can avoid this step by step decomposition very easily: *} |
|
547 |
||
548 |
lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y" |
|
549 |
proof - |
|
550 |
have "\<And>x y. \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> C x y" |
|
551 |
proof - |
|
552 |
fix x y assume "A x y" "B x y" |
|
553 |
show "C x y" sorry |
|
554 |
qed |
|
555 |
thus ?thesis by blast |
|
556 |
qed |
|
557 |
||
558 |
text{*\noindent |
|
559 |
This can be simplified further by \emph{raw proof blocks}, i.e.\ |
|
560 |
proofs enclosed in braces: *} |
|
561 |
||
562 |
lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y" |
|
563 |
proof - |
|
564 |
{ fix x y assume "A x y" "B x y" |
|
565 |
have "C x y" sorry } |
|
566 |
thus ?thesis by blast |
|
567 |
qed |
|
568 |
||
569 |
text{*\noindent The result of the raw proof block is the same theorem |
|
570 |
as above, namely @{prop"\<And>x y. \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> C x y"}. Raw |
|
571 |
proof blocks are like ordinary proofs except that they do not prove |
|
572 |
some explicitly stated property but that the property emerges directly |
|
573 |
out of the \isakeyword{fixe}s, \isakeyword{assume}s and |
|
574 |
\isakeyword{have} in the block. Thus they again serve to avoid |
|
575 |
duplication. Note that the conclusion of a raw proof block is stated with |
|
576 |
\isakeyword{have} rather than \isakeyword{show} because it is not the |
|
577 |
conclusion of some pending goal but some independent claim. |
|
578 |
||
579 |
The general idea demonstrated in this subsection is very |
|
25427 | 580 |
important in Isar and distinguishes it from \isa{apply}-style proofs: |
13999 | 581 |
\begin{quote}\em |
582 |
Do not manipulate the proof state into a particular form by applying |
|
25427 | 583 |
proof methods but state the desired form explicitly and let the proof |
584 |
methods verify that from this form the original goal follows. |
|
13999 | 585 |
\end{quote} |
14617 | 586 |
This yields more readable and also more robust proofs. |
587 |
||
588 |
\subsubsection{General case distinctions} |
|
589 |
||
590 |
As an important application of raw proof blocks we show how to deal |
|
591 |
with general case distinctions --- more specific kinds are treated in |
|
592 |
\S\ref{sec:CaseDistinction}. Imagine that you would like to prove some |
|
593 |
goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that |
|
594 |
the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and |
|
595 |
that each case $P_i$ implies the goal. Taken together, this proves the |
|
596 |
goal. The corresponding Isar proof pattern (for $n = 3$) is very handy: |
|
597 |
*} |
|
598 |
text_raw{*\renewcommand{\isamarkupcmt}[1]{#1}*} |
|
599 |
(*<*)lemma "XXX"(*>*) |
|
600 |
proof - |
|
601 |
have "P\<^isub>1 \<or> P\<^isub>2 \<or> P\<^isub>3" (*<*)sorry(*>*) -- {*\dots*} |
|
602 |
moreover |
|
603 |
{ assume P\<^isub>1 |
|
604 |
-- {*\dots*} |
|
605 |
have ?thesis (*<*)sorry(*>*) -- {*\dots*} } |
|
606 |
moreover |
|
607 |
{ assume P\<^isub>2 |
|
608 |
-- {*\dots*} |
|
609 |
have ?thesis (*<*)sorry(*>*) -- {*\dots*} } |
|
610 |
moreover |
|
611 |
{ assume P\<^isub>3 |
|
612 |
-- {*\dots*} |
|
613 |
have ?thesis (*<*)sorry(*>*) -- {*\dots*} } |
|
614 |
ultimately show ?thesis by blast |
|
615 |
qed |
|
616 |
text_raw{*\renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}*} |
|
617 |
||
13999 | 618 |
|
619 |
subsection{*Further refinements*} |
|
620 |
||
621 |
text{* This subsection discusses some further tricks that can make |
|
622 |
life easier although they are not essential. *} |
|
623 |
||
624 |
subsubsection{*\isakeyword{and}*} |
|
625 |
||
626 |
text{* Propositions (following \isakeyword{assume} etc) may but need not be |
|
627 |
separated by \isakeyword{and}. This is not just for readability |
|
628 |
(\isakeyword{from} \isa{A} \isakeyword{and} \isa{B} looks nicer than |
|
629 |
\isakeyword{from} \isa{A} \isa{B}) but for structuring lists of propositions |
|
630 |
into possibly named blocks. In |
|
631 |
\begin{center} |
|
632 |
\isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$ |
|
633 |
\isakeyword{and} $A_4$ |
|
634 |
\end{center} |
|
635 |
label \isa{A} refers to the list of propositions $A_1$ $A_2$ and |
|
636 |
label \isa{B} to $A_3$. *} |
|
637 |
||
638 |
subsubsection{*\isakeyword{note}*} |
|
639 |
text{* If you want to remember intermediate fact(s) that cannot be |
|
640 |
named directly, use \isakeyword{note}. For example the result of raw |
|
641 |
proof block can be named by following it with |
|
642 |
\isakeyword{note}~@{text"some_name = this"}. As a side effect, |
|
643 |
@{text this} is set to the list of facts on the right-hand side. You |
|
644 |
can also say @{text"note some_fact"}, which simply sets @{text this}, |
|
645 |
i.e.\ recalls @{text"some_fact"}, e.g.\ in a \isakeyword{moreover} sequence. *} |
|
646 |
||
647 |
||
648 |
subsubsection{*\isakeyword{fixes}*} |
|
649 |
||
650 |
text{* Sometimes it is necessary to decorate a proposition with type |
|
651 |
constraints, as in Cantor's theorem above. These type constraints tend |
|
652 |
to make the theorem less readable. The situation can be improved a |
|
653 |
little by combining the type constraint with an outer @{text"\<And>"}: *} |
|
654 |
||
655 |
theorem "\<And>f :: 'a \<Rightarrow> 'a set. \<exists>S. S \<notin> range f" |
|
656 |
(*<*)oops(*>*) |
|
657 |
text{*\noindent However, now @{term f} is bound and we need a |
|
658 |
\isakeyword{fix}~\isa{f} in the proof before we can refer to @{term f}. |
|
659 |
This is avoided by \isakeyword{fixes}: *} |
|
660 |
||
661 |
theorem fixes f :: "'a \<Rightarrow> 'a set" shows "\<exists>S. S \<notin> range f" |
|
662 |
(*<*)oops(*>*) |
|
663 |
text{* \noindent |
|
664 |
Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:*} |
|
665 |
||
666 |
lemma comm_mono: |
|
667 |
fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix ">" 60) and |
|
668 |
f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "++" 70) |
|
669 |
assumes comm: "\<And>x y::'a. x ++ y = y ++ x" and |
|
670 |
mono: "\<And>x y z::'a. x > y \<Longrightarrow> x ++ z > y ++ z" |
|
671 |
shows "x > y \<Longrightarrow> z ++ x > z ++ y" |
|
672 |
by(simp add: comm mono) |
|
673 |
||
674 |
text{*\noindent The concrete syntax is dropped at the end of the proof and the |
|
675 |
theorem becomes @{thm[display,margin=60]comm_mono} |
|
676 |
\tweakskip *} |
|
677 |
||
678 |
subsubsection{*\isakeyword{obtain}*} |
|
679 |
||
680 |
text{* The \isakeyword{obtain} construct can introduce multiple |
|
681 |
witnesses and propositions as in the following proof fragment:*} |
|
682 |
||
683 |
lemma assumes A: "\<exists>x y. P x y \<and> Q x y" shows "R" |
|
684 |
proof - |
|
685 |
from A obtain x y where P: "P x y" and Q: "Q x y" by blast |
|
686 |
(*<*)oops(*>*) |
|
687 |
text{* Remember also that one does not even need to start with a formula |
|
688 |
containing @{text"\<exists>"} as we saw in the proof of Cantor's theorem. |
|
689 |
*} |
|
690 |
||
691 |
subsubsection{*Combining proof styles*} |
|
692 |
||
25427 | 693 |
text{* Finally, whole \isa{apply}-scripts may appear in the leaves of the |
694 |
proof tree, although this is best avoided. Here is a contrived example: *} |
|
13999 | 695 |
|
696 |
lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B" |
|
697 |
proof |
|
698 |
assume a: "A" |
|
699 |
show "(A \<longrightarrow>B) \<longrightarrow> B" |
|
700 |
apply(rule impI) |
|
701 |
apply(erule impE) |
|
702 |
apply(rule a) |
|
703 |
apply assumption |
|
704 |
done |
|
705 |
qed |
|
706 |
||
707 |
text{*\noindent You may need to resort to this technique if an |
|
708 |
automatic step fails to prove the desired proposition. |
|
709 |
||
25427 | 710 |
When converting a proof from \isa{apply}-style into Isar you can proceed |
13999 | 711 |
in a top-down manner: parts of the proof can be left in script form |
712 |
while the outer structure is already expressed in Isar. *} |
|
713 |
||
714 |
(*<*)end(*>*) |