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