author | paulson |
Wed, 10 Jan 2001 12:43:51 +0100 | |
changeset 10854 | d1ff1ff5c5ad |
parent 10848 | 7b3ee4695fe6 |
child 10887 | 7fb42b97413a |
permissions | -rw-r--r-- |
10792 | 1 |
% $Id$ |
10295 | 2 |
\chapter{The Rules of the Game} |
3 |
\label{chap:rules} |
|
4 |
||
5 |
Until now, we have proved everything using only induction and simplification. |
|
6 |
Substantial proofs require more elaborate forms of inference. This chapter |
|
7 |
outlines the concepts and techniques that underlie reasoning in Isabelle. The examples |
|
8 |
are mainly drawn from predicate logic. The first examples in this |
|
9 |
chapter will consist of detailed, low-level proof steps. Later, we shall |
|
10 |
see how to automate such reasoning using the methods \isa{blast}, |
|
11 |
\isa{auto} and others. |
|
12 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
13 |
\section{Natural Deduction} |
10295 | 14 |
|
15 |
In Isabelle, proofs are constructed using inference rules. The |
|
16 |
most familiar inference rule is probably \emph{modus ponens}: |
|
17 |
\[ \infer{Q}{P\imp Q & P} \] |
|
18 |
This rule says that from $P\imp Q$ and $P$ |
|
19 |
we may infer~$Q$. |
|
20 |
||
21 |
%Early logical formalisms had this |
|
22 |
%rule and at most one or two others, along with many complicated |
|
23 |
%axioms. Any desired theorem could be obtained by applying \emph{modus |
|
24 |
%ponens} or other rules to the axioms, but proofs were |
|
25 |
%hard to find. For example, a standard inference system has |
|
26 |
%these two axioms (amongst others): |
|
27 |
%\begin{gather*} |
|
28 |
% P\imp(Q\imp P) \tag{K}\\ |
|
29 |
% (P\imp(Q\imp R))\imp ((P\imp Q)\imp(P\imp R)) \tag{S} |
|
30 |
%\end{gather*} |
|
31 |
%Try proving the trivial fact $P\imp P$ using these axioms and \emph{modus |
|
32 |
%ponens}! |
|
33 |
||
34 |
\textbf{Natural deduction} is an attempt to formalize logic in a way |
|
35 |
that mirrors human reasoning patterns. |
|
36 |
% |
|
37 |
%Instead of having a few |
|
38 |
%inference rules and many axioms, it has many inference rules |
|
39 |
%and few axioms. |
|
40 |
% |
|
41 |
For each logical symbol (say, $\conj$), there |
|
42 |
are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules. |
|
43 |
The introduction rules allow us to infer this symbol (say, to |
|
44 |
infer conjunctions). The elimination rules allow us to deduce |
|
45 |
consequences from this symbol. Ideally each rule should mention |
|
46 |
one symbol only. For predicate logic this can be |
|
47 |
done, but when users define their own concepts they typically |
|
48 |
have to refer to other symbols as well. It is best not be dogmatic. |
|
49 |
||
50 |
Natural deduction generally deserves its name. It is easy to use. Each |
|
51 |
proof step consists of identifying the outermost symbol of a formula and |
|
52 |
applying the corresponding rule. It creates new subgoals in |
|
53 |
an obvious way from parts of the chosen formula. Expanding the |
|
54 |
definitions of constants can blow up the goal enormously. Deriving natural |
|
55 |
deduction rules for such constants lets us reason in terms of their key |
|
56 |
properties, which might otherwise be obscured by the technicalities of its |
|
57 |
definition. Natural deduction rules also lend themselves to automation. |
|
58 |
Isabelle's |
|
59 |
\textbf{classical reasoner} accepts any suitable collection of natural deduction |
|
60 |
rules and uses them to search for proofs automatically. Isabelle is designed around |
|
61 |
natural deduction and many of its tools use the terminology of introduction and |
|
62 |
elimination rules. |
|
63 |
||
64 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
65 |
\section{Introduction Rules} |
10295 | 66 |
|
67 |
An \textbf{introduction} rule tells us when we can infer a formula |
|
68 |
containing a specific logical symbol. For example, the conjunction |
|
69 |
introduction rule says that if we have $P$ and if we have $Q$ then |
|
70 |
we have $P\conj Q$. In a mathematics text, it is typically shown |
|
71 |
like this: |
|
72 |
\[ \infer{P\conj Q}{P & Q} \] |
|
73 |
The rule introduces the conjunction |
|
74 |
symbol~($\conj$) in its conclusion. Of course, in Isabelle proofs we |
|
75 |
mainly reason backwards. When we apply this rule, the subgoal already has |
|
76 |
the form of a conjunction; the proof step makes this conjunction symbol |
|
77 |
disappear. |
|
78 |
||
79 |
In Isabelle notation, the rule looks like this: |
|
80 |
\begin{isabelle} |
|
81 |
\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI} |
|
82 |
\end{isabelle} |
|
83 |
Carefully examine the syntax. The premises appear to the |
|
84 |
left of the arrow and the conclusion to the right. The premises (if |
|
85 |
more than one) are grouped using the fat brackets. The question marks |
|
86 |
indicate \textbf{schematic variables} (also called \textbf{unknowns}): they may |
|
87 |
be replaced by arbitrary formulas. If we use the rule backwards, Isabelle |
|
88 |
tries to unify the current subgoal with the conclusion of the rule, which |
|
89 |
has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below, |
|
90 |
\S\ref{sec:unification}.) If successful, |
|
91 |
it yields new subgoals given by the formulas assigned to |
|
92 |
\isa{?P} and \isa{?Q}. |
|
93 |
||
94 |
The following trivial proof illustrates this point. |
|
95 |
\begin{isabelle} |
|
10596 | 96 |
\isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\ |
10295 | 97 |
Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ |
10301 | 98 |
(Q\ \isasymand\ P)"\isanewline |
10295 | 99 |
\isacommand{apply}\ (rule\ conjI)\isanewline |
100 |
\ \isacommand{apply}\ assumption\isanewline |
|
101 |
\isacommand{apply}\ (rule\ conjI)\isanewline |
|
102 |
\ \isacommand{apply}\ assumption\isanewline |
|
103 |
\isacommand{apply}\ assumption |
|
104 |
\end{isabelle} |
|
105 |
At the start, Isabelle presents |
|
106 |
us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved, |
|
107 |
\isa{P\ \isasymand\ |
|
108 |
(Q\ \isasymand\ P)}. We are working backwards, so when we |
|
109 |
apply conjunction introduction, the rule removes the outermost occurrence |
|
110 |
of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply |
|
10596 | 111 |
the proof method \isa{rule} --- here with {\isa{conjI}}, the conjunction |
10295 | 112 |
introduction rule. |
113 |
\begin{isabelle} |
|
10596 | 114 |
%\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\ |
10295 | 115 |
%\isasymand\ P\isanewline |
10596 | 116 |
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline |
117 |
\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P |
|
10295 | 118 |
\end{isabelle} |
119 |
Isabelle leaves two new subgoals: the two halves of the original conjunction. |
|
120 |
The first is simply \isa{P}, which is trivial, since \isa{P} is among |
|
10596 | 121 |
the assumptions. We can apply the \isa{assumption} |
10295 | 122 |
method, which proves a subgoal by finding a matching assumption. |
123 |
\begin{isabelle} |
|
10596 | 124 |
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ |
10295 | 125 |
Q\ \isasymand\ P |
126 |
\end{isabelle} |
|
127 |
We are left with the subgoal of proving |
|
128 |
\isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply |
|
129 |
\isa{rule conjI} again. |
|
130 |
\begin{isabelle} |
|
10596 | 131 |
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline |
132 |
\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P |
|
10295 | 133 |
\end{isabelle} |
134 |
We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved |
|
10596 | 135 |
using the \isa{assumption} method. |
10295 | 136 |
|
137 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
138 |
\section{Elimination Rules} |
10295 | 139 |
|
140 |
\textbf{Elimination} rules work in the opposite direction from introduction |
|
141 |
rules. In the case of conjunction, there are two such rules. |
|
142 |
From $P\conj Q$ we infer $P$. also, from $P\conj Q$ |
|
143 |
we infer $Q$: |
|
144 |
\[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \] |
|
145 |
||
146 |
Now consider disjunction. There are two introduction rules, which resemble inverted forms of the |
|
147 |
conjunction elimination rules: |
|
148 |
\[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \] |
|
149 |
||
150 |
What is the disjunction elimination rule? The situation is rather different from |
|
151 |
conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we |
|
152 |
cannot conclude that $Q$ is true; there are no direct |
|
153 |
elimination rules of the sort that we have seen for conjunction. Instead, |
|
154 |
there is an elimination rule that works indirectly. If we are trying to prove |
|
155 |
something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider |
|
156 |
two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is |
|
157 |
true and prove $R$ a second time. Here we see a fundamental concept used in natural |
|
158 |
deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under |
|
159 |
different assumptions. The assumptions are local to these subproofs and are visible |
|
160 |
nowhere else. |
|
161 |
||
162 |
In a logic text, the disjunction elimination rule might be shown |
|
163 |
like this: |
|
164 |
\[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \] |
|
165 |
The assumptions $[P]$ and $[Q]$ are bracketed |
|
166 |
to emphasize that they are local to their subproofs. In Isabelle |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
167 |
notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the |
10295 | 168 |
same purpose: |
169 |
\begin{isabelle} |
|
170 |
\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE} |
|
171 |
\end{isabelle} |
|
172 |
When we use this sort of elimination rule backwards, it produces |
|
173 |
a case split. (We have this before, in proofs by induction.) The following proof |
|
174 |
illustrates the use of disjunction elimination. |
|
175 |
\begin{isabelle} |
|
10301 | 176 |
\isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ |
10295 | 177 |
\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline |
178 |
\isacommand{apply}\ (erule\ disjE)\isanewline |
|
179 |
\ \isacommand{apply}\ (rule\ disjI2)\isanewline |
|
180 |
\ \isacommand{apply}\ assumption\isanewline |
|
181 |
\isacommand{apply}\ (rule\ disjI1)\isanewline |
|
182 |
\isacommand{apply}\ assumption |
|
183 |
\end{isabelle} |
|
184 |
We assume \isa{P\ \isasymor\ Q} and |
|
185 |
must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction |
|
186 |
elimination rule, \isa{disjE}. The method {\isa{erule}} applies an |
|
187 |
elimination rule to the assumptions, searching for one that matches the |
|
188 |
rule's first premise. Deleting that assumption, it |
|
189 |
return the subgoals for the remaining premises. Most of the |
|
190 |
time, this is the best way to use elimination rules; only rarely is there |
|
191 |
any point in keeping the assumption. |
|
192 |
||
193 |
\begin{isabelle} |
|
194 |
%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline |
|
195 |
\ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline |
|
196 |
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P |
|
197 |
\end{isabelle} |
|
198 |
Here it leaves us with two subgoals. The first assumes \isa{P} and the |
|
199 |
second assumes \isa{Q}. Tackling the first subgoal, we need to |
|
200 |
show \isa{Q\ \isasymor\ P}\@. The second introduction rule (\isa{disjI2}) |
|
201 |
can reduce this to \isa{P}, which matches the assumption. So, we apply the |
|
10596 | 202 |
\isa{rule} method with \isa{disjI2} \ldots |
10295 | 203 |
\begin{isabelle} |
204 |
\ 1.\ P\ \isasymLongrightarrow\ P\isanewline |
|
205 |
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P |
|
206 |
\end{isabelle} |
|
10596 | 207 |
\ldots and finish off with the \isa{assumption} |
10295 | 208 |
method. We are left with the other subgoal, which |
209 |
assumes \isa{Q}. |
|
210 |
\begin{isabelle} |
|
211 |
\ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P |
|
212 |
\end{isabelle} |
|
213 |
Its proof is similar, using the introduction |
|
214 |
rule \isa{disjI1}. |
|
215 |
||
216 |
The result of this proof is a new inference rule \isa{disj_swap}, which is neither |
|
217 |
an introduction nor an elimination rule, but which might |
|
218 |
be useful. We can use it to replace any goal of the form $Q\disj P$ |
|
219 |
by a one of the form $P\disj Q$. |
|
220 |
||
221 |
||
222 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
223 |
\section{Destruction Rules: Some Examples} |
10295 | 224 |
|
225 |
Now let us examine the analogous proof for conjunction. |
|
226 |
\begin{isabelle} |
|
10301 | 227 |
\isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline |
10295 | 228 |
\isacommand{apply}\ (rule\ conjI)\isanewline |
229 |
\ \isacommand{apply}\ (drule\ conjunct2)\isanewline |
|
230 |
\ \isacommand{apply}\ assumption\isanewline |
|
231 |
\isacommand{apply}\ (drule\ conjunct1)\isanewline |
|
232 |
\isacommand{apply}\ assumption |
|
233 |
\end{isabelle} |
|
234 |
Recall that the conjunction elimination rules --- whose Isabelle names are |
|
235 |
\isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half |
|
236 |
of a conjunction. Rules of this sort (where the conclusion is a subformula of a |
|
237 |
premise) are called \textbf{destruction} rules, by analogy with the destructor |
|
10301 | 238 |
functions of functional programming.% |
10295 | 239 |
\footnote{This Isabelle terminology has no counterpart in standard logic texts, |
240 |
although the distinction between the two forms of elimination rule is well known. |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
241 |
Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
242 |
[for $\disj$ and $\exists$] are very |
10295 | 243 |
bad. What is catastrophic about them is the parasitic presence of a formula [$R$] |
244 |
which has no structural link with the formula which is eliminated.''} |
|
245 |
||
246 |
The first proof step applies conjunction introduction, leaving |
|
247 |
two subgoals: |
|
248 |
\begin{isabelle} |
|
249 |
%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline |
|
250 |
\ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline |
|
251 |
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P |
|
252 |
\end{isabelle} |
|
253 |
||
254 |
To invoke the elimination rule, we apply a new method, \isa{drule}. |
|
255 |
Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if |
|
256 |
you prefer). Applying the |
|
257 |
second conjunction rule using \isa{drule} replaces the assumption |
|
258 |
\isa{P\ \isasymand\ Q} by \isa{Q}. |
|
259 |
\begin{isabelle} |
|
260 |
\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline |
|
261 |
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P |
|
262 |
\end{isabelle} |
|
263 |
The resulting subgoal can be proved by applying \isa{assumption}. |
|
264 |
The other subgoal is similarly proved, using the \isa{conjunct1} rule and the |
|
265 |
\isa{assumption} method. |
|
266 |
||
267 |
Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to |
|
268 |
you. Isabelle does not attempt to work out whether a rule |
|
269 |
is an introduction rule or an elimination rule. The |
|
270 |
method determines how the rule will be interpreted. Many rules |
|
271 |
can be used in more than one way. For example, \isa{disj_swap} can |
|
272 |
be applied to assumptions as well as to goals; it replaces any |
|
273 |
assumption of the form |
|
274 |
$P\disj Q$ by a one of the form $Q\disj P$. |
|
275 |
||
276 |
Destruction rules are simpler in form than indirect rules such as \isa{disjE}, |
|
277 |
but they can be inconvenient. Each of the conjunction rules discards half |
|
278 |
of the formula, when usually we want to take both parts of the conjunction as new |
|
279 |
assumptions. The easiest way to do so is by using an |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
280 |
alternative conjunction elimination rule that resembles \isa{disjE}\@. It is |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
281 |
seldom, if ever, seen in logic books. In Isabelle syntax it looks like this: |
10295 | 282 |
\begin{isabelle} |
283 |
\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE} |
|
284 |
\end{isabelle} |
|
285 |
||
286 |
\begin{exercise} |
|
287 |
Use the rule {\isa{conjE}} to shorten the proof above. |
|
288 |
\end{exercise} |
|
289 |
||
290 |
||
291 |
\section{Implication} |
|
292 |
||
293 |
At the start of this chapter, we saw the rule \textit{modus ponens}. It is, in fact, |
|
294 |
a destruction rule. The matching introduction rule looks like this |
|
295 |
in Isabelle: |
|
296 |
\begin{isabelle} |
|
297 |
(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\ |
|
298 |
\isasymlongrightarrow\ ?Q\rulename{impI} |
|
299 |
\end{isabelle} |
|
300 |
And this is \textit{modus ponens}: |
|
301 |
\begin{isabelle} |
|
302 |
\isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\ |
|
303 |
\isasymLongrightarrow\ ?Q |
|
304 |
\rulename{mp} |
|
305 |
\end{isabelle} |
|
306 |
||
307 |
Here is a proof using the rules for implication. This |
|
308 |
lemma performs a sort of uncurrying, replacing the two antecedents |
|
309 |
of a nested implication by a conjunction. |
|
310 |
\begin{isabelle} |
|
311 |
\isacommand{lemma}\ imp_uncurry:\ |
|
10301 | 312 |
"P\ \isasymlongrightarrow\ (Q\ |
10295 | 313 |
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ |
314 |
\isasymand\ Q\ \isasymlongrightarrow\ |
|
315 |
R"\isanewline |
|
316 |
\isacommand{apply}\ (rule\ impI)\isanewline |
|
317 |
\isacommand{apply}\ (erule\ conjE)\isanewline |
|
318 |
\isacommand{apply}\ (drule\ mp)\isanewline |
|
319 |
\ \isacommand{apply}\ assumption\isanewline |
|
320 |
\isacommand{apply}\ (drule\ mp)\isanewline |
|
321 |
\ \ \isacommand{apply}\ assumption\isanewline |
|
322 |
\ \isacommand{apply}\ assumption |
|
323 |
\end{isabelle} |
|
324 |
First, we state the lemma and apply implication introduction (\isa{rule impI}), |
|
325 |
which moves the conjunction to the assumptions. |
|
326 |
\begin{isabelle} |
|
327 |
%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\ |
|
328 |
%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline |
|
10596 | 329 |
\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R |
10295 | 330 |
\end{isabelle} |
331 |
Next, we apply conjunction elimination (\isa{erule conjE}), which splits this |
|
332 |
conjunction into two parts. |
|
333 |
\begin{isabelle} |
|
10596 | 334 |
\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\ |
10295 | 335 |
Q\isasymrbrakk\ \isasymLongrightarrow\ R |
336 |
\end{isabelle} |
|
337 |
Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\ |
|
338 |
\isasymlongrightarrow\ R)}, where the parentheses have been inserted for |
|
339 |
clarity. The nested implication requires two applications of |
|
340 |
\textit{modus ponens}: \isa{drule mp}. The first use yields the |
|
341 |
implication \isa{Q\ |
|
342 |
\isasymlongrightarrow\ R}, but first we must prove the extra subgoal |
|
343 |
\isa{P}, which we do by assumption. |
|
344 |
\begin{isabelle} |
|
10596 | 345 |
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline |
346 |
\ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R |
|
10295 | 347 |
\end{isabelle} |
348 |
Repeating these steps for \isa{Q\ |
|
349 |
\isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}. |
|
350 |
\begin{isabelle} |
|
10596 | 351 |
\ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ |
10295 | 352 |
\isasymLongrightarrow\ R |
353 |
\end{isabelle} |
|
354 |
||
355 |
The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow} |
|
356 |
both stand for implication, but they differ in many respects. Isabelle |
|
357 |
uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is |
|
358 |
built-in and Isabelle's inference mechanisms treat it specially. On the |
|
359 |
other hand, \isa{\isasymlongrightarrow} is just one of the many connectives |
|
360 |
available in higher-order logic. We reason about it using inference rules |
|
361 |
such as \isa{impI} and \isa{mp}, just as we reason about the other |
|
362 |
connectives. You will have to use \isa{\isasymlongrightarrow} in any |
|
363 |
context that requires a formula of higher-order logic. Use |
|
364 |
\isa{\isasymLongrightarrow} to separate a theorem's preconditions from its |
|
365 |
conclusion. |
|
366 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
367 |
\medskip |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
368 |
\indexbold{by} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
369 |
The \isacommand{by} command is useful for proofs like these that use |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
370 |
\isa{assumption} heavily. It executes an |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
371 |
\isacommand{apply} command, then tries to prove all remaining subgoals using |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
372 |
\isa{assumption}. Since (if successful) it ends the proof, it also replaces the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
373 |
\isacommand{done} symbol. For example, the proof above can be shortened: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
374 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
375 |
\isacommand{lemma}\ imp_uncurry:\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
376 |
"P\ \isasymlongrightarrow\ (Q\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
377 |
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
378 |
\isasymand\ Q\ \isasymlongrightarrow\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
379 |
R"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
380 |
\isacommand{apply}\ (rule\ impI)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
381 |
\isacommand{apply}\ (erule\ conjE)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
382 |
\isacommand{apply}\ (drule\ mp)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
383 |
\ \isacommand{apply}\ assumption\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
384 |
\isacommand{by}\ (drule\ mp) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
385 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
386 |
We could use \isacommand{by} to replace the final \isacommand{apply} and |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
387 |
\isacommand{done} in any proof, but typically we use it |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
388 |
to eliminate calls to \isa{assumption}. It is also a nice way of expressing a |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
389 |
one-line proof. |
10295 | 390 |
|
391 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
392 |
\section{Unification and Substitution}\label{sec:unification} |
10295 | 393 |
|
394 |
As we have seen, Isabelle rules involve variables that begin with a |
|
395 |
question mark. These are called \textbf{schematic} variables and act as |
|
396 |
placeholders for terms. \textbf{Unification} refers to the process of |
|
397 |
making two terms identical, possibly by replacing their variables by |
|
398 |
terms. The simplest case is when the two terms are already the same. Next |
|
399 |
simplest is when the variables in only one of the term |
|
400 |
are replaced; this is called \textbf{pattern-matching}. The |
|
10596 | 401 |
\isa{rule} method typically matches the rule's conclusion |
10295 | 402 |
against the current subgoal. In the most complex case, variables in both |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
403 |
terms are replaced; the \isa{rule} method can do this if the goal |
10295 | 404 |
itself contains schematic variables. Other occurrences of the variables in |
405 |
the rule or proof state are updated at the same time. |
|
406 |
||
407 |
Schematic variables in goals are sometimes called \textbf{unknowns}. They |
|
408 |
are useful because they let us proceed with a proof even when we do not |
|
409 |
know what certain terms should be --- as when the goal is $\exists x.\,P$. |
|
410 |
They can be filled in later, often automatically. |
|
411 |
||
412 |
Unification is well known to Prolog programmers. Isabelle uses \textbf{higher-order} |
|
413 |
unification, which is unification in the |
|
414 |
typed $\lambda$-calculus. The general case is |
|
415 |
undecidable, but for our purposes, the differences from ordinary |
|
416 |
unification are straightforward. It handles bound variables |
|
417 |
correctly, avoiding capture. The two terms \isa{{\isasymlambda}x.\ ?P} and |
|
418 |
\isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by |
|
419 |
\isa{t x} is forbidden because the free occurrence of~\isa{x} would become |
|
420 |
bound. The two terms |
|
421 |
\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are |
|
422 |
trivially unifiable because they differ only by a bound variable renaming. |
|
423 |
||
424 |
Higher-order unification sometimes must invent |
|
425 |
$\lambda$-terms to replace function variables, |
|
426 |
which can lead to a combinatorial explosion. However, Isabelle proofs tend |
|
427 |
to involve easy cases where there are few possibilities for the |
|
428 |
$\lambda$-term being constructed. In the easiest case, the |
|
429 |
function variable is applied only to bound variables, |
|
430 |
as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and |
|
431 |
\isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace |
|
432 |
\isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most |
|
433 |
one unifier, like ordinary unification. A harder case is |
|
434 |
unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h}, |
|
435 |
namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}. |
|
436 |
Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is |
|
437 |
exponential in the number of occurrences of~\isa{a} in the second term. |
|
438 |
||
439 |
Isabelle also uses function variables to express \textbf{substitution}. |
|
440 |
A typical substitution rule allows us to replace one term by |
|
441 |
another if we know that two terms are equal. |
|
442 |
\[ \infer{P[t/x]}{s=t & P[s/x]} \] |
|
443 |
The conclusion uses a notation for substitution: $P[t/x]$ is the result of |
|
444 |
replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
445 |
designated by~$x$. For example, it can |
10295 | 446 |
derive symmetry of equality from reflexivity. Using $x=s$ for~$P$ |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
447 |
replaces just the first $s$ in $s=s$ by~$t$: |
10295 | 448 |
\[ \infer{t=s}{s=t & \infer{s=s}{}} \] |
449 |
||
450 |
The Isabelle version of the substitution rule looks like this: |
|
451 |
\begin{isabelle} |
|
452 |
\isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\ |
|
453 |
?t |
|
454 |
\rulename{ssubst} |
|
455 |
\end{isabelle} |
|
456 |
Crucially, \isa{?P} is a function |
|
457 |
variable: it can be replaced by a $\lambda$-expression |
|
458 |
involving one bound variable whose occurrences identify the places |
|
459 |
in which $s$ will be replaced by~$t$. The proof above requires |
|
460 |
\isa{{\isasymlambda}x.~x=s}. |
|
461 |
||
462 |
The \isa{simp} method replaces equals by equals, but using the substitution |
|
463 |
rule gives us more control. Consider this proof: |
|
464 |
\begin{isabelle} |
|
465 |
\isacommand{lemma}\ |
|
10596 | 466 |
"\isasymlbrakk \ x\ =\ f\ x;\ odd(f\ x)\ \isasymrbrakk\ \isasymLongrightarrow\ |
467 |
odd\ x"\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
468 |
\isacommand{by}\ (erule\ ssubst) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
469 |
\end{isabelle} |
10295 | 470 |
% |
471 |
The simplifier might loop, replacing \isa{x} by \isa{f x} and then by |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
472 |
\isa{f(f x)} and so forth. (Here \isa{simp} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
473 |
can see the danger and would re-orient the equality, but in more complicated |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
474 |
cases it can be fooled.) When we apply substitution, Isabelle replaces every |
10295 | 475 |
\isa{x} in the subgoal by \isa{f x} just once: it cannot loop. The |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
476 |
resulting subgoal is trivial by assumption, so the \isacommand{by} command |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
477 |
proves it implicitly. |
10295 | 478 |
|
479 |
We are using the \isa{erule} method it in a novel way. Hitherto, |
|
480 |
the conclusion of the rule was just a variable such as~\isa{?R}, but it may |
|
481 |
be any term. The conclusion is unified with the subgoal just as |
|
482 |
it would be with the \isa{rule} method. At the same time \isa{erule} looks |
|
483 |
for an assumption that matches the rule's first premise, as usual. With |
|
484 |
\isa{ssubst} the effect is to find, use and delete an equality |
|
485 |
assumption. |
|
486 |
||
487 |
||
488 |
Higher-order unification can be tricky, as this example indicates: |
|
489 |
\begin{isabelle} |
|
10596 | 490 |
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ |
10295 | 491 |
f\ x;\ triple\ (f\ x)\ |
492 |
(f\ x)\ x\ \isasymrbrakk\ |
|
493 |
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline |
|
494 |
\isacommand{apply}\ (erule\ ssubst)\isanewline |
|
495 |
\isacommand{back}\isanewline |
|
496 |
\isacommand{back}\isanewline |
|
497 |
\isacommand{back}\isanewline |
|
498 |
\isacommand{back}\isanewline |
|
499 |
\isacommand{apply}\ assumption\isanewline |
|
500 |
\isacommand{done} |
|
501 |
\end{isabelle} |
|
502 |
% |
|
503 |
By default, Isabelle tries to substitute for all the |
|
504 |
occurrences. Applying \isa{erule\ ssubst} yields this subgoal: |
|
505 |
\begin{isabelle} |
|
506 |
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x) |
|
507 |
\end{isabelle} |
|
508 |
The substitution should have been done in the first two occurrences |
|
509 |
of~\isa{x} only. Isabelle has gone too far. The \isa{back} |
|
510 |
method allows us to reject this possibility and get a new one: |
|
511 |
\begin{isabelle} |
|
512 |
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x) |
|
513 |
\end{isabelle} |
|
514 |
% |
|
515 |
Now Isabelle has left the first occurrence of~\isa{x} alone. That is |
|
516 |
promising but it is not the desired combination. So we use \isa{back} |
|
517 |
again: |
|
518 |
\begin{isabelle} |
|
519 |
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x) |
|
520 |
\end{isabelle} |
|
521 |
% |
|
522 |
This also is wrong, so we use \isa{back} again: |
|
523 |
\begin{isabelle} |
|
524 |
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x) |
|
525 |
\end{isabelle} |
|
526 |
% |
|
527 |
And this one is wrong too. Looking carefully at the series |
|
528 |
of alternatives, we see a binary countdown with reversed bits: 111, |
|
529 |
011, 101, 001. Invoke \isa{back} again: |
|
530 |
\begin{isabelle} |
|
531 |
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x% |
|
532 |
\end{isabelle} |
|
533 |
At last, we have the right combination! This goal follows by assumption. |
|
534 |
||
535 |
Never use {\isa{back}} in the final version of a proof. |
|
536 |
It should only be used for exploration. One way to get rid of {\isa{back}} |
|
537 |
to combine two methods in a single \textbf{apply} command. Isabelle |
|
538 |
applies the first method and then the second. If the second method |
|
539 |
fails then Isabelle automatically backtracks. This process continues until |
|
540 |
the first method produces an output that the second method can |
|
541 |
use. We get a one-line proof of our example: |
|
542 |
\begin{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
543 |
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ |
10295 | 544 |
\isasymrbrakk\ |
545 |
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline |
|
546 |
\isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline |
|
547 |
\isacommand{done} |
|
548 |
\end{isabelle} |
|
549 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
550 |
\noindent |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
551 |
The \isacommand{by} command works too, since it backtracks when |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
552 |
proving subgoals by assumption: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
553 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
554 |
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
555 |
\isasymrbrakk\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
556 |
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
557 |
\isacommand{by}\ (erule\ ssubst) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
558 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
559 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
560 |
|
10295 | 561 |
The most general way to get rid of the {\isa{back}} command is |
10596 | 562 |
to instantiate variables in the rule. The method \isa{rule_tac} is |
10295 | 563 |
similar to \isa{rule}, but it |
564 |
makes some of the rule's variables denote specified terms. |
|
10596 | 565 |
Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
566 |
\isa{erule_tac} since above we used \isa{erule}. |
10295 | 567 |
\begin{isabelle} |
10596 | 568 |
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
569 |
\isacommand{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
570 |
\isakeyword{in}\ ssubst) |
10295 | 571 |
\end{isabelle} |
572 |
% |
|
573 |
To specify a desired substitution |
|
574 |
requires instantiating the variable \isa{?P} with a $\lambda$-expression. |
|
575 |
The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\ |
|
576 |
u\ x} indicate that the first two arguments have to be substituted, leaving |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
577 |
the third unchanged. With this instantiation, backtracking is neither necessary |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
578 |
nor possible. |
10295 | 579 |
|
10596 | 580 |
An alternative to \isa{rule_tac} is to use \isa{rule} with the |
581 |
\isa{of} directive, described in \S\ref{sec:forward} below. An |
|
582 |
advantage of \isa{rule_tac} is that the instantiations may refer to |
|
10295 | 583 |
variables bound in the current subgoal. |
584 |
||
585 |
||
586 |
\section{Negation} |
|
587 |
||
588 |
Negation causes surprising complexity in proofs. Its natural |
|
589 |
deduction rules are straightforward, but additional rules seem |
|
590 |
necessary in order to handle negated assumptions gracefully. |
|
591 |
||
592 |
Negation introduction deduces $\neg P$ if assuming $P$ leads to a |
|
593 |
contradiction. Negation elimination deduces any formula in the |
|
594 |
presence of $\neg P$ together with~$P$: |
|
595 |
\begin{isabelle} |
|
596 |
(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P% |
|
597 |
\rulename{notI}\isanewline |
|
598 |
\isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R% |
|
599 |
\rulename{notE} |
|
600 |
\end{isabelle} |
|
601 |
% |
|
602 |
Classical logic allows us to assume $\neg P$ |
|
603 |
when attempting to prove~$P$: |
|
604 |
\begin{isabelle} |
|
605 |
(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P% |
|
606 |
\rulename{classical} |
|
607 |
\end{isabelle} |
|
608 |
% |
|
609 |
Three further rules are variations on the theme of contrapositive. |
|
610 |
They differ in the placement of the negation symbols: |
|
611 |
\begin{isabelle} |
|
612 |
\isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% |
|
613 |
\rulename{contrapos_pp}\isanewline |
|
614 |
\isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% |
|
615 |
\rulename{contrapos_np}\isanewline |
|
616 |
\isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P% |
|
617 |
\rulename{contrapos_nn} |
|
618 |
\end{isabelle} |
|
619 |
% |
|
620 |
These rules are typically applied using the {\isa{erule}} method, where |
|
621 |
their effect is to form a contrapositive from an |
|
622 |
assumption and the goal's conclusion. |
|
623 |
||
624 |
The most important of these is \isa{contrapos_np}. It is useful |
|
625 |
for applying introduction rules to negated assumptions. For instance, |
|
626 |
the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we |
|
627 |
might want to use conjunction introduction on it. |
|
628 |
Before we can do so, we must move that assumption so that it |
|
629 |
becomes the conclusion. The following proof demonstrates this |
|
630 |
technique: |
|
631 |
\begin{isabelle} |
|
632 |
\isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\ |
|
633 |
\isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\ |
|
634 |
R"\isanewline |
|
635 |
\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\ |
|
636 |
contrapos_np)\isanewline |
|
637 |
\isacommand{apply}\ intro\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
638 |
\isacommand{by}\ (erule\ notE) |
10295 | 639 |
\end{isabelle} |
640 |
% |
|
641 |
There are two negated assumptions and we need to exchange the conclusion with the |
|
642 |
second one. The method \isa{erule contrapos_np} would select the first assumption, |
|
643 |
which we do not want. So we specify the desired assumption explicitly, using |
|
644 |
\isa{erule_tac}. This is the resulting subgoal: |
|
645 |
\begin{isabelle} |
|
646 |
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ |
|
647 |
R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q% |
|
648 |
\end{isabelle} |
|
649 |
The former conclusion, namely \isa{R}, now appears negated among the assumptions, |
|
650 |
while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new |
|
651 |
conclusion. |
|
652 |
||
653 |
We can now apply introduction rules. We use the {\isa{intro}} method, which |
|
654 |
repeatedly applies built-in introduction rules. Here its effect is equivalent |
|
10596 | 655 |
to \isa{rule impI}. |
656 |
\begin{isabelle} |
|
10295 | 657 |
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\ |
658 |
R\isasymrbrakk\ \isasymLongrightarrow\ Q% |
|
659 |
\end{isabelle} |
|
660 |
We can see a contradiction in the form of assumptions \isa{\isasymnot\ R} |
|
661 |
and~\isa{R}, which suggests using negation elimination. If applied on its own, |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
662 |
\isa{notE} will select the first negated assumption, which is useless. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
663 |
Instead, we invoke the rule using the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
664 |
\isa{by} command. |
10295 | 665 |
Now when Isabelle selects the first assumption, it tries to prove \isa{P\ |
666 |
\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the |
|
667 |
assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption. That |
|
668 |
concludes the proof. |
|
669 |
||
670 |
\medskip |
|
671 |
||
672 |
Here is another example. |
|
673 |
\begin{isabelle} |
|
674 |
\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\ |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
675 |
\isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
676 |
\isacommand{apply}\ intro\isanewline |
10295 | 677 |
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline |
678 |
\ \isacommand{apply}\ assumption |
|
679 |
\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
680 |
\isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI) |
10295 | 681 |
\end{isabelle} |
682 |
% |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
683 |
The first proof step applies the {\isa{intro}} method, which repeatedly uses |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
684 |
built-in introduction rules. Here it creates the negative assumption |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
685 |
\hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}. That comes from \isa{disjCI}, a |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
686 |
disjunction introduction rule that combines the effects of |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
687 |
\isa{disjI1} and \isa{disjI2}. |
10295 | 688 |
\begin{isabelle} |
689 |
\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\ |
|
690 |
R)\isasymrbrakk\ \isasymLongrightarrow\ P% |
|
691 |
\end{isabelle} |
|
692 |
Next we apply the {\isa{elim}} method, which repeatedly applies |
|
693 |
elimination rules; here, the elimination rules given |
|
694 |
in the command. One of the subgoals is trivial, leaving us with one other: |
|
695 |
\begin{isabelle} |
|
696 |
\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P% |
|
697 |
\end{isabelle} |
|
698 |
% |
|
699 |
Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The |
|
700 |
combination |
|
701 |
\begin{isabelle} |
|
702 |
\ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI) |
|
703 |
\end{isabelle} |
|
704 |
is robust: the \isa{conjI} forces the \isa{erule} to select a |
|
10301 | 705 |
conjunction. The two subgoals are the ones we would expect from applying |
10295 | 706 |
conjunction introduction to |
707 |
\isa{Q\ |
|
708 |
\isasymand\ R}: |
|
709 |
\begin{isabelle} |
|
10596 | 710 |
\ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ |
10295 | 711 |
Q\isanewline |
10596 | 712 |
\ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R% |
10295 | 713 |
\end{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
714 |
They are proved by assumption, which is implicit in the \isacommand{by} command. |
10295 | 715 |
|
716 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
717 |
\section{Quantifiers} |
10295 | 718 |
|
719 |
Quantifiers require formalizing syntactic substitution and the notion of \textbf{arbitrary |
|
720 |
value}. Consider the universal quantifier. In a logic book, its |
|
721 |
introduction rule looks like this: |
|
722 |
\[ \infer{\forall x.\,P}{P} \] |
|
723 |
Typically, a proviso written in English says that $x$ must not |
|
724 |
occur in the assumptions. This proviso guarantees that $x$ can be regarded as |
|
725 |
arbitrary, since it has not been assumed to satisfy any special conditions. |
|
726 |
Isabelle's underlying formalism, called the |
|
727 |
\textbf{meta-logic}, eliminates the need for English. It provides its own universal |
|
728 |
quantifier (\isasymAnd) to express the notion of an arbitrary value. We have |
|
729 |
already seen another symbol of the meta-logic, namely |
|
730 |
\isa\isasymLongrightarrow, which expresses inference rules and the treatment of |
|
731 |
assumptions. The only other symbol in the meta-logic is \isa\isasymequiv, which |
|
732 |
can be used to define constants. |
|
733 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
734 |
\subsection{The Universal Introduction Rule} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
735 |
|
10295 | 736 |
Returning to the universal quantifier, we find that having a similar quantifier |
737 |
as part of the meta-logic makes the introduction rule trivial to express: |
|
738 |
\begin{isabelle} |
|
10596 | 739 |
(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI} |
10295 | 740 |
\end{isabelle} |
741 |
||
742 |
||
743 |
The following trivial proof demonstrates how the universal introduction |
|
744 |
rule works. |
|
745 |
\begin{isabelle} |
|
746 |
\isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline |
|
747 |
\isacommand{apply}\ (rule\ allI)\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
748 |
\isacommand{by}\ (rule\ impI) |
10295 | 749 |
\end{isabelle} |
750 |
The first step invokes the rule by applying the method \isa{rule allI}. |
|
751 |
\begin{isabelle} |
|
752 |
%{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline |
|
10596 | 753 |
\ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x |
10295 | 754 |
\end{isabelle} |
755 |
Note that the resulting proof state has a bound variable, |
|
756 |
namely~\bigisa{x}. The rule has replaced the universal quantifier of |
|
757 |
higher-order logic by Isabelle's meta-level quantifier. Our goal is to |
|
758 |
prove |
|
759 |
\isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is |
|
760 |
an implication, so we apply the corresponding introduction rule (\isa{impI}). |
|
761 |
\begin{isabelle} |
|
10596 | 762 |
\ 1.\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow\ P\ x |
10295 | 763 |
\end{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
764 |
This last subgoal is implicitly proved by assumption. |
10295 | 765 |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
766 |
\subsection{The Universal Elimination Rule} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
767 |
|
10295 | 768 |
Now consider universal elimination. In a logic text, |
769 |
the rule looks like this: |
|
770 |
\[ \infer{P[t/x]}{\forall x.\,P} \] |
|
771 |
The conclusion is $P$ with $t$ substituted for the variable~$x$. |
|
772 |
Isabelle expresses substitution using a function variable: |
|
773 |
\begin{isabelle} |
|
774 |
{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec} |
|
775 |
\end{isabelle} |
|
776 |
This destruction rule takes a |
|
777 |
universally quantified formula and removes the quantifier, replacing |
|
778 |
the bound variable \bigisa{x} by the schematic variable \bigisa{?x}. Recall that a |
|
779 |
schematic variable starts with a question mark and acts as a |
|
780 |
placeholder: it can be replaced by any term. |
|
781 |
||
782 |
To see how this works, let us derive a rule about reducing |
|
783 |
the scope of a universal quantifier. In mathematical notation we write |
|
784 |
\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \] |
|
785 |
with the proviso `$x$ not free in~$P$.' Isabelle's treatment of |
|
786 |
substitution makes the proviso unnecessary. The conclusion is expressed as |
|
787 |
\isa{P\ |
|
788 |
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the |
|
789 |
variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
790 |
bound variable capture. Here is the Isabelle proof in full: |
10295 | 791 |
\begin{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
792 |
\isacommand{lemma}\ "(\isasymforall x.\ P\ \isasymlongrightarrow \ Q\ x)\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
793 |
\isasymLongrightarrow \ P\ \isasymlongrightarrow \ (\isasymforall x.\ Q\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
794 |
x)"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
795 |
\isacommand{apply}\ (rule\ impI,\ rule\ allI)\isanewline |
10295 | 796 |
\isacommand{apply}\ (drule\ spec)\isanewline |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
797 |
\isacommand{by}\ (drule\ mp) |
10295 | 798 |
\end{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
799 |
First we apply implies introduction (\isa{impI}), |
10295 | 800 |
which moves the \isa{P} from the conclusion to the assumptions. Then |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
801 |
we apply universal introduction (\isa{allI}). |
10295 | 802 |
\begin{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
803 |
\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
804 |
x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x |
10295 | 805 |
\end{isabelle} |
806 |
As before, it replaces the HOL |
|
807 |
quantifier by a meta-level quantifier, producing a subgoal that |
|
808 |
binds the variable~\bigisa{x}. The leading bound variables |
|
809 |
(here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\ |
|
810 |
\isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the |
|
811 |
conclusion, here \isa{Q\ x}. At each proof step, the subgoals inherit the |
|
812 |
previous context, though some context elements may be added or deleted. |
|
813 |
Applying \isa{erule} deletes an assumption, while many natural deduction |
|
814 |
rules add bound variables or assumptions. |
|
815 |
||
816 |
Now, to reason from the universally quantified |
|
817 |
assumption, we apply the elimination rule using the {\isa{drule}} |
|
818 |
method. This rule is called \isa{spec} because it specializes a universal formula |
|
819 |
to a particular term. |
|
820 |
\begin{isabelle} |
|
10596 | 821 |
\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\ |
822 |
x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x |
|
10295 | 823 |
\end{isabelle} |
824 |
Observe how the context has changed. The quantified formula is gone, |
|
825 |
replaced by a new assumption derived from its body. Informally, we have |
|
826 |
removed the quantifier. The quantified variable |
|
827 |
has been replaced by the curious term |
|
828 |
\bigisa{?x2~x}; it acts as a placeholder that may be replaced |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
829 |
by any term that can be built from~\bigisa{x}. (Formally, \bigisa{?x2} is an |
10295 | 830 |
unknown of function type, applied to the argument~\bigisa{x}.) This new assumption is |
831 |
an implication, so we can use \emph{modus ponens} on it. As before, it requires |
|
832 |
proving the antecedent (in this case \isa{P}) and leaves us with the consequent. |
|
833 |
\begin{isabelle} |
|
10596 | 834 |
\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\ |
10295 | 835 |
\isasymLongrightarrow\ Q\ x |
836 |
\end{isabelle} |
|
837 |
The consequent is \isa{Q} applied to that placeholder. It may be replaced by any |
|
838 |
term built from~\bigisa{x}, and here |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
839 |
it should simply be~\bigisa{x}. The \isa{assumption} method, implicit in the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
840 |
\isacommand{by} command, proves this subgoal. The assumption need not |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
841 |
be identical to the conclusion, provided the two formulas are unifiable. |
10295 | 842 |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
843 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
844 |
\subsection{Re-using an Assumption: the {\tt\slshape frule} Method} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
845 |
|
10295 | 846 |
Note that \isa{drule spec} removes the universal quantifier and --- as |
847 |
usual with elimination rules --- discards the original formula. Sometimes, a |
|
848 |
universal formula has to be kept so that it can be used again. Then we use a new |
|
849 |
method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
850 |
the selected assumption. The \isa{f} is for \emph{forward}. |
10295 | 851 |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
852 |
In this example, going from \isa{P\ a} to \isa{P(h(h~a))} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
853 |
requires two uses of the quantified assumption, one for each~\isa{h} being |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
854 |
affixed to the term~\isa{a}. |
10295 | 855 |
\begin{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
856 |
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x); |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
857 |
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))"\isanewline |
10295 | 858 |
\isacommand{apply}\ (frule\ spec)\isanewline |
859 |
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline |
|
860 |
\isacommand{apply}\ (drule\ spec)\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
861 |
\isacommand{by}\ (drule\ mp) |
10295 | 862 |
\end{isabelle} |
863 |
% |
|
864 |
Applying \isa{frule\ spec} leaves this subgoal: |
|
865 |
\begin{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
866 |
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (h\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) |
10295 | 867 |
\end{isabelle} |
868 |
It is just what \isa{drule} would have left except that the quantified |
|
869 |
assumption is still present. The next step is to apply \isa{mp} to the |
|
870 |
implication and the assumption \isa{P\ a}, which leaves this subgoal: |
|
871 |
\begin{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
872 |
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) |
10295 | 873 |
\end{isabelle} |
874 |
% |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
875 |
We have created the assumption \isa{P(h\ a)}, which is progress. To finish the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
876 |
proof, we apply \isa{spec} one last time, using \isa{drule}. |
10854 | 877 |
|
878 |
\medskip |
|
879 |
\emph{A final remark}. Applying \isa{spec} by the command |
|
10295 | 880 |
\begin{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
881 |
\isacommand{apply}\ (drule\ mp,\ assumption) |
10295 | 882 |
\end{isabelle} |
10854 | 883 |
would not work a second time: it would add a second copy of \isa{P(h~a)} instead |
884 |
of the desired assumption, \isa{P(h(h~a))}. The \isacommand{by} |
|
885 |
command forces Isabelle to backtrack until it finds the correct one. |
|
886 |
Alternatively, we could have used the \isacommand{apply} command and bundled the |
|
887 |
\isa{drule mp} with \emph{two} calls of \isa{assumption}. |
|
10295 | 888 |
|
889 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
890 |
\subsection{The Existential Quantifier} |
10295 | 891 |
|
892 |
The concepts just presented also apply to the existential quantifier, |
|
893 |
whose introduction rule looks like this in Isabelle: |
|
894 |
\begin{isabelle} |
|
895 |
?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI} |
|
896 |
\end{isabelle} |
|
897 |
If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x. |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
898 |
P(x)$ is also true. It is a dual of the universal elimination rule, and |
10295 | 899 |
logic texts present it using the same notation for substitution. The existential |
900 |
elimination rule looks like this |
|
901 |
in a logic text: |
|
902 |
\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \] |
|
903 |
% |
|
904 |
It looks like this in Isabelle: |
|
905 |
\begin{isabelle} |
|
10596 | 906 |
\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE} |
10295 | 907 |
\end{isabelle} |
908 |
% |
|
909 |
Given an existentially quantified theorem and some |
|
910 |
formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with |
|
911 |
the universal introduction rule, the textbook version imposes a proviso on the |
|
912 |
quantified variable, which Isabelle expresses using its meta-logic. Note that it is |
|
913 |
enough to have a universal quantifier in the meta-logic; we do not need an existential |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
914 |
quantifier to be built in as well. |
10295 | 915 |
|
916 |
||
917 |
\begin{exercise} |
|
918 |
Prove the lemma |
|
919 |
\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \] |
|
920 |
\emph{Hint}: the proof is similar |
|
921 |
to the one just above for the universal quantifier. |
|
922 |
\end{exercise} |
|
923 |
||
924 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
925 |
\section{Hilbert's $\epsilon$-Operator} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
926 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
927 |
Isabelle/HOL provides Hilbert's |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
928 |
$\epsilon$-operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
929 |
true, provided such a value exists. Using this operator, we can express an |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
930 |
existential destruction rule: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
931 |
\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \] |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
932 |
This rule is seldom used, for it can cause exponential blow-up. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
933 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
934 |
\subsection{Definite Descriptions} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
935 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
936 |
In ASCII, we write \isa{SOME} for $\epsilon$. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
937 |
\REMARK{the internal constant is \isa{Eps}} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
938 |
The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
939 |
description}: when \isa{P} is satisfied by a unique value,~\isa{a}. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
940 |
We reason using this rule: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
941 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
942 |
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
943 |
\isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
944 |
\rulename{some_equality} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
945 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
946 |
For instance, we can define the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
947 |
cardinality of a finite set~$A$ to be that |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
948 |
$n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$. We can then |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
949 |
prove that the cardinality of the empty set is zero (since $n=0$ satisfies the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
950 |
description) and proceed to prove other facts. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
951 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
952 |
Here is an example. HOL defines \isa{inv},\indexbold{*inv (constant)} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
953 |
which expresses inverses of functions, as a definite |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
954 |
description: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
955 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
956 |
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
957 |
\rulename{inv_def} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
958 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
959 |
The inverse of \isa{f}, when applied to \isa{y}, returns some {x} such that |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
960 |
\isa{f~x~=~y}. For example, we can prove \isa{inv~Suc} really is the inverse |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
961 |
of the \isa{Suc} function |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
962 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
963 |
\isacommand{lemma}\ "inv\ Suc\ (Suc\ x)\ =\ x"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
964 |
\isacommand{by}\ (simp\ add:\ inv_def) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
965 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
966 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
967 |
\noindent |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
968 |
The proof is a one-liner: the subgoal simplifies to a degenerate application of |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
969 |
\isa{SOME}, which is then erased. The definition says nothing about what |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
970 |
\isa{inv~Suc} returns when applied to zero. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
971 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
972 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
973 |
A more challenging example illustrates how Isabelle/HOL defines the least-number |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
974 |
operator, which denotes the least \isa{x} satisfying~\isa{P}: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
975 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
976 |
(LEAST\ x.\ P\ x)\ \isasymequiv \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
977 |
P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
978 |
\rulename{Least_def} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
979 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
980 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
981 |
Let us prove the counterpart of \isa{some_equality} for this operator. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
982 |
The first step merely unfolds the definition: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
983 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
984 |
\isacommand{theorem}\ Least_equality:\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
985 |
\ \ \ \ \ "\isasymlbrakk \ P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\ \isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
986 |
\isacommand{apply}\ (simp\ add:\ Least_def)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
987 |
%\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
988 |
%\isasymle \ x\isasymrbrakk \isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
989 |
%\ \ \ \ \isasymLongrightarrow \ (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
990 |
\isacommand{apply}\ (rule\ some_equality)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
991 |
\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
992 |
\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
993 |
\isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ P\ k\ \isasymand \ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
994 |
(\isasymforall y.\ P\ y\ \isasymlongrightarrow \ k\ \isasymle \ y)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
995 |
\ 2.\ \isasymAnd x.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x;\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)\isasymrbrakk \isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
996 |
\ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
997 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
998 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
999 |
As always with \isa{some_equality}, we must show existence and |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1000 |
uniqueness of the claimed solution,~\isa{k}. Existence, the first |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1001 |
subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1002 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1003 |
\isasymlbrakk x\ \isasymle \ y;\ y\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ x\ =\ y% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1004 |
\rulename{order_antisym} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1005 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1006 |
The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}. One call |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1007 |
to \isa{auto} does it all: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1008 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1009 |
\isacommand{by}\ (auto\ intro:\ order_antisym) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1010 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1011 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1012 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1013 |
\subsection{Indefinite Descriptions} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1014 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1015 |
Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1016 |
description}, when it makes an arbitrary selection from the values |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1017 |
satisfying~\isa{P}\@. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1018 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1019 |
P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1020 |
\rulename{someI}\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1021 |
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1022 |
x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1023 |
\rulename{someI2} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1024 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1025 |
Rule \isa{someI} is basic (if anything satisfies \isa{P} then so does |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1026 |
\hbox{\isa{SOME\ x.\ P\ x}}). Rule \isa{someI2} is easier to apply in a backward |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1027 |
proof. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1028 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1029 |
\medskip |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1030 |
For example, let us prove the Axiom of Choice: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1031 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1032 |
\isacommand{theorem}\ axiom_of_choice: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1033 |
\ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1034 |
\isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1035 |
\isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1036 |
\ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1037 |
\isasymLongrightarrow \ P\ x\ (?f\ x) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1038 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1039 |
% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1040 |
We have applied the introduction rules; now it is time to apply the elimination |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1041 |
rules. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1042 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1043 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1044 |
\isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1045 |
\ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1046 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1047 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1048 |
\noindent |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1049 |
The rule \isa{someI} automatically instantiates |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1050 |
\isa{f} to \hbox{\isa{\isasymlambda x.\ SOME y.\ P\ x\ y}}, which is the choice |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1051 |
function. It also instantiates \isa{?x2\ x} to \isa{x}. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1052 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1053 |
\isacommand{by}\ (rule\ someI)\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1054 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1055 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1056 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1057 |
\section{Some Proofs That Fail} |
10295 | 1058 |
|
1059 |
Most of the examples in this tutorial involve proving theorems. But not every |
|
1060 |
conjecture is true, and it can be instructive to see how |
|
1061 |
proofs fail. Here we attempt to prove a distributive law involving |
|
1062 |
the existential quantifier and conjunction. |
|
1063 |
\begin{isabelle} |
|
1064 |
\isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x"\isanewline |
|
1065 |
\isacommand{apply}\ (erule\ conjE)\isanewline |
|
1066 |
\isacommand{apply}\ (erule\ exE)\isanewline |
|
1067 |
\isacommand{apply}\ (erule\ exE)\isanewline |
|
1068 |
\isacommand{apply}\ (rule\ exI)\isanewline |
|
1069 |
\isacommand{apply}\ (rule\ conjI)\isanewline |
|
1070 |
\ \isacommand{apply}\ assumption\isanewline |
|
1071 |
\isacommand{oops} |
|
1072 |
\end{isabelle} |
|
1073 |
The first steps are routine. We apply conjunction elimination (\isa{erule |
|
1074 |
conjE}) to split the assumption in two, leaving two existentially quantified |
|
1075 |
assumptions. Applying existential elimination (\isa{erule exE}) removes one of |
|
1076 |
the quantifiers. |
|
1077 |
\begin{isabelle} |
|
1078 |
%({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ |
|
1079 |
%\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline |
|
10596 | 1080 |
\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x |
10295 | 1081 |
\end{isabelle} |
1082 |
% |
|
1083 |
When we remove the other quantifier, we get a different bound |
|
1084 |
variable in the subgoal. (The name \isa{xa} is generated automatically.) |
|
1085 |
\begin{isabelle} |
|
10596 | 1086 |
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ |
10295 | 1087 |
\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x |
1088 |
\end{isabelle} |
|
1089 |
The proviso of the existential elimination rule has forced the variables to |
|
1090 |
differ: we can hardly expect two arbitrary values to be equal! There is |
|
1091 |
no way to prove this subgoal. Removing the |
|
1092 |
conclusion's existential quantifier yields two |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1093 |
identical placeholders, which can become any term involving the variables \isa{x} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1094 |
and~\isa{xa}. We need one to become \isa{x} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1095 |
and the other to become~\isa{xa}, but Isabelle requires all instances of a |
10295 | 1096 |
placeholder to be identical. |
1097 |
\begin{isabelle} |
|
10596 | 1098 |
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ |
10295 | 1099 |
\isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline |
10596 | 1100 |
\ 2.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa) |
10295 | 1101 |
\end{isabelle} |
1102 |
We can prove either subgoal |
|
1103 |
using the \isa{assumption} method. If we prove the first one, the placeholder |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1104 |
changes into~\isa{x}. |
10295 | 1105 |
\begin{isabelle} |
10596 | 1106 |
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ |
10295 | 1107 |
\isasymLongrightarrow\ Q\ x |
1108 |
\end{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1109 |
We are left with a subgoal that cannot be proved. Applying the \isa{assumption} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1110 |
method results in an error message: |
10295 | 1111 |
\begin{isabelle} |
1112 |
*** empty result sequence -- proof command failed |
|
1113 |
\end{isabelle} |
|
1114 |
We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command. |
|
1115 |
||
1116 |
\medskip |
|
1117 |
||
1118 |
Here is another abortive proof, illustrating the interaction between |
|
1119 |
bound variables and unknowns. |
|
1120 |
If $R$ is a reflexive relation, |
|
1121 |
is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when |
|
1122 |
we attempt to prove it. |
|
1123 |
\begin{isabelle} |
|
1124 |
\isacommand{lemma}\ "{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ |
|
1125 |
{\isasymexists}x.\ {\isasymforall}y.\ R\ x\ y"\isanewline |
|
1126 |
\isacommand{apply}\ (rule\ exI)\isanewline |
|
1127 |
\isacommand{apply}\ (rule\ allI)\isanewline |
|
1128 |
\isacommand{apply}\ (drule\ spec)\isanewline |
|
1129 |
\isacommand{oops} |
|
1130 |
\end{isabelle} |
|
1131 |
First, |
|
1132 |
we remove the existential quantifier. The new proof state has |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1133 |
an unknown, namely~\isa{?x}. |
10295 | 1134 |
\begin{isabelle} |
1135 |
%{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\ |
|
1136 |
%{\isasymforall}y.\ R\ x\ y\isanewline |
|
1137 |
\ 1.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymforall}y.\ R\ ?x\ y |
|
1138 |
\end{isabelle} |
|
1139 |
Next, we remove the universal quantifier |
|
1140 |
from the conclusion, putting the bound variable~\isa{y} into the subgoal. |
|
1141 |
\begin{isabelle} |
|
10596 | 1142 |
\ 1.\ \isasymAnd y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y |
10295 | 1143 |
\end{isabelle} |
1144 |
Finally, we try to apply our reflexivity assumption. We obtain a |
|
1145 |
new assumption whose identical placeholders may be replaced by |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1146 |
any term involving~\isa{y}. |
10295 | 1147 |
\begin{isabelle} |
10596 | 1148 |
\ 1.\ \isasymAnd y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y |
10295 | 1149 |
\end{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1150 |
This subgoal can only be proved by putting \isa{y} for all the placeholders, |
10295 | 1151 |
making the assumption and conclusion become \isa{R\ y\ y}. |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1152 |
But Isabelle refuses to substitute \isa{y}, a bound variable, for |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1153 |
\isa{?x}; that would be a bound variable capture. The proof fails. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1154 |
Note that Isabelle can replace \isa{?z2~y} by \isa{y}; this involves |
10295 | 1155 |
instantiating |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1156 |
\isa{?z2} to the identity function. |
10295 | 1157 |
|
1158 |
This example is typical of how Isabelle enforces sound quantifier reasoning. |
|
1159 |
||
1160 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1161 |
\section{Proving Theorems Using the {\tt\slshape blast} Method} |
10295 | 1162 |
|
1163 |
It is hard to prove substantial theorems using the methods |
|
1164 |
described above. A proof may be dozens or hundreds of steps long. You |
|
1165 |
may need to search among different ways of proving certain |
|
1166 |
subgoals. Often a choice that proves one subgoal renders another |
|
1167 |
impossible to prove. There are further complications that we have not |
|
1168 |
discussed, concerning negation and disjunction. Isabelle's |
|
1169 |
\textbf{classical reasoner} is a family of tools that perform such |
|
1170 |
proofs automatically. The most important of these is the |
|
10596 | 1171 |
\isa{blast} method. |
10295 | 1172 |
|
1173 |
In this section, we shall first see how to use the classical |
|
1174 |
reasoner in its default mode and then how to insert additional |
|
1175 |
rules, enabling it to work in new problem domains. |
|
1176 |
||
1177 |
We begin with examples from pure predicate logic. The following |
|
1178 |
example is known as Andrew's challenge. Peter Andrews designed |
|
1179 |
it to be hard to prove by automatic means.% |
|
1180 |
\footnote{Pelletier~\cite{pelletier86} describes it and many other |
|
1181 |
problems for automatic theorem provers.} |
|
1182 |
The nested biconditionals cause an exponential explosion: the formal |
|
10596 | 1183 |
proof is enormous. However, the \isa{blast} method proves it in |
10295 | 1184 |
a fraction of a second. |
1185 |
\begin{isabelle} |
|
1186 |
\isacommand{lemma}\ |
|
1187 |
"(({\isasymexists}x.\ |
|
1188 |
{\isasymforall}y.\ |
|
10301 | 1189 |
p(x){=}p(y))\ |
10295 | 1190 |
=\ |
1191 |
(({\isasymexists}x.\ |
|
10301 | 1192 |
q(x))=({\isasymforall}y.\ |
1193 |
p(y))))\ |
|
10295 | 1194 |
\ \ =\ \ \ \ \isanewline |
1195 |
\ \ \ \ \ \ \ \ |
|
1196 |
(({\isasymexists}x.\ |
|
1197 |
{\isasymforall}y.\ |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1198 |
q(x){=}q(y))\ =\ (({\isasymexists}x.\ p(x))=({\isasymforall}y.\ q(y))))"\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1199 |
\isacommand{by}\ blast |
10295 | 1200 |
\end{isabelle} |
1201 |
The next example is a logic problem composed by Lewis Carroll. |
|
10596 | 1202 |
The \isa{blast} method finds it trivial. Moreover, it turns out |
10295 | 1203 |
that not all of the assumptions are necessary. We can easily |
1204 |
experiment with variations of this formula and see which ones |
|
1205 |
can be proved. |
|
1206 |
\begin{isabelle} |
|
1207 |
\isacommand{lemma}\ |
|
1208 |
"({\isasymforall}x.\ |
|
1209 |
honest(x)\ \isasymand\ |
|
1210 |
industrious(x)\ \isasymlongrightarrow\ |
|
10301 | 1211 |
healthy(x))\ |
10295 | 1212 |
\isasymand\ \ \isanewline |
1213 |
\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\ |
|
1214 |
grocer(x)\ \isasymand\ |
|
10301 | 1215 |
healthy(x))\ |
10295 | 1216 |
\isasymand\ \isanewline |
1217 |
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ |
|
1218 |
industrious(x)\ \isasymand\ |
|
1219 |
grocer(x)\ \isasymlongrightarrow\ |
|
10301 | 1220 |
honest(x))\ |
10295 | 1221 |
\isasymand\ \isanewline |
1222 |
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ |
|
1223 |
cyclist(x)\ \isasymlongrightarrow\ |
|
10301 | 1224 |
industrious(x))\ |
10295 | 1225 |
\isasymand\ \isanewline |
1226 |
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ |
|
1227 |
{\isasymnot}healthy(x)\ \isasymand\ |
|
1228 |
cyclist(x)\ \isasymlongrightarrow\ |
|
10301 | 1229 |
{\isasymnot}honest(x))\ |
10295 | 1230 |
\ \isanewline |
1231 |
\ \ \ \ \ \ \ \ \isasymlongrightarrow\ |
|
1232 |
({\isasymforall}x.\ |
|
1233 |
grocer(x)\ \isasymlongrightarrow\ |
|
10301 | 1234 |
{\isasymnot}cyclist(x))"\isanewline |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1235 |
\isacommand{by}\ blast |
10295 | 1236 |
\end{isabelle} |
10596 | 1237 |
The \isa{blast} method is also effective for set theory, which is |
10295 | 1238 |
described in the next chapter. This formula below may look horrible, but |
1239 |
the \isa{blast} method proves it easily. |
|
1240 |
\begin{isabelle} |
|
10301 | 1241 |
\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline |
1242 |
\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1243 |
\isacommand{by}\ blast |
10295 | 1244 |
\end{isabelle} |
1245 |
||
1246 |
Few subgoals are couched purely in predicate logic and set theory. |
|
1247 |
We can extend the scope of the classical reasoner by giving it new rules. |
|
1248 |
Extending it effectively requires understanding the notions of |
|
1249 |
introduction, elimination and destruction rules. Moreover, there is a |
|
1250 |
distinction between safe and unsafe rules. A \textbf{safe} rule is one |
|
1251 |
that can be applied backwards without losing information; an |
|
1252 |
\textbf{unsafe} rule loses information, perhaps transforming the subgoal |
|
1253 |
into one that cannot be proved. The safe/unsafe |
|
1254 |
distinction affects the proof search: if a proof attempt fails, the |
|
1255 |
classical reasoner backtracks to the most recent unsafe rule application |
|
1256 |
and makes another choice. |
|
1257 |
||
1258 |
An important special case avoids all these complications. A logical |
|
1259 |
equivalence, which in higher-order logic is an equality between |
|
1260 |
formulas, can be given to the classical |
|
10596 | 1261 |
reasoner and simplifier by using the attribute \isa{iff}. You |
10295 | 1262 |
should do so if the right hand side of the equivalence is |
1263 |
simpler than the left-hand side. |
|
1264 |
||
1265 |
For example, here is a simple fact about list concatenation. |
|
1266 |
The result of appending two lists is empty if and only if both |
|
1267 |
of the lists are themselves empty. Obviously, applying this equivalence |
|
1268 |
will result in a simpler goal. When stating this lemma, we include |
|
10596 | 1269 |
the \isa{iff} attribute. Once we have proved the lemma, Isabelle |
10295 | 1270 |
will make it known to the classical reasoner (and to the simplifier). |
1271 |
\begin{isabelle} |
|
1272 |
\isacommand{lemma}\ |
|
10854 | 1273 |
[iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\ |
1274 |
(xs=[]\ \isacharampersand\ ys=[])"\isanewline |
|
1275 |
\isacommand{apply}\ (induct_tac\ xs)\isanewline |
|
1276 |
\isacommand{apply}\ (simp_all)\isanewline |
|
10295 | 1277 |
\isacommand{done} |
1278 |
\end{isabelle} |
|
1279 |
% |
|
1280 |
This fact about multiplication is also appropriate for |
|
10854 | 1281 |
the \isa{iff} attribute:\REMARK{the ?s are ugly here but we need |
1282 |
them again when talking about \isa{of}; we need a consistent style} |
|
10295 | 1283 |
\begin{isabelle} |
10596 | 1284 |
(\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0) |
10295 | 1285 |
\end{isabelle} |
1286 |
A product is zero if and only if one of the factors is zero. The |
|
1287 |
reasoning involves a logical \textsc{or}. Proving new rules for |
|
1288 |
disjunctive reasoning is hard, but translating to an actual disjunction |
|
1289 |
works: the classical reasoner handles disjunction properly. |
|
1290 |
||
10596 | 1291 |
In more detail, this is how the \isa{iff} attribute works. It converts |
10295 | 1292 |
the equivalence $P=Q$ to a pair of rules: the introduction |
1293 |
rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the |
|
1294 |
classical reasoner as safe rules, ensuring that all occurrences of $P$ in |
|
1295 |
a subgoal are replaced by~$Q$. The simplifier performs the same |
|
1296 |
replacement, since \isa{iff} gives $P=Q$ to the |
|
1297 |
simplifier. But classical reasoning is different from |
|
1298 |
simplification. Simplification is deterministic: it applies rewrite rules |
|
1299 |
repeatedly, as long as possible, in order to \emph{transform} a goal. Classical |
|
1300 |
reasoning uses search and backtracking in order to \emph{prove} a goal. |
|
1301 |
||
1302 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1303 |
\section{Proving the Correctness of Euclid's Algorithm} |
10295 | 1304 |
\label{sec:proving-euclid} |
1305 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1306 |
A brief development will illustrate the advanced use of |
10854 | 1307 |
\isa{blast}. We shall also see \isa{case_tac} used to perform a Boolean |
1308 |
case split. |
|
1309 |
||
1310 |
In \S\ref{sec:recdef-simplification}, we declared the |
|
10596 | 1311 |
recursive function \isa{gcd}: |
10295 | 1312 |
\begin{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1313 |
\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline |
10301 | 1314 |
\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\ |
10596 | 1315 |
::nat*nat\ \isasymRightarrow\ nat)"\isanewline |
10301 | 1316 |
\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" |
10295 | 1317 |
\end{isabelle} |
1318 |
Let us prove that it computes the greatest common |
|
1319 |
divisor of its two arguments. |
|
1320 |
The theorem is expressed in terms of the familiar |
|
1321 |
\textbf{divides} relation from number theory: |
|
1322 |
\begin{isabelle} |
|
10596 | 1323 |
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k |
10295 | 1324 |
\rulename{dvd_def} |
1325 |
\end{isabelle} |
|
1326 |
% |
|
1327 |
A simple induction proves the theorem. Here \isa{gcd.induct} refers to the |
|
1328 |
induction rule returned by \isa{recdef}. The proof relies on the simplification |
|
1329 |
rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the |
|
1330 |
definition of \isa{gcd} can cause looping. |
|
1331 |
\begin{isabelle} |
|
10301 | 1332 |
\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ n)"\isanewline |
1333 |
\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline |
|
1334 |
\isacommand{apply}\ (case_tac\ "n=0")\isanewline |
|
10295 | 1335 |
\isacommand{apply}\ (simp_all)\isanewline |
1336 |
\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline |
|
1337 |
\isacommand{done}% |
|
1338 |
\end{isabelle} |
|
1339 |
Notice that the induction formula |
|
1340 |
is a conjunction. This is necessary: in the inductive step, each |
|
1341 |
half of the conjunction establishes the other. The first three proof steps |
|
1342 |
are applying induction, performing a case analysis on \isa{n}, |
|
10854 | 1343 |
and simplifying. Let us pass over these quickly --- we shall discuss |
1344 |
\isa{case_tac} below --- and consider the use of \isa{blast}. We have reached the |
|
1345 |
following subgoal: |
|
10295 | 1346 |
\begin{isabelle} |
1347 |
%gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline |
|
10596 | 1348 |
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline |
1349 |
\ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk\isanewline |
|
10546 | 1350 |
\ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m |
10295 | 1351 |
\end{isabelle} |
1352 |
% |
|
1353 |
One of the assumptions, the induction hypothesis, is a conjunction. |
|
1354 |
The two divides relationships it asserts are enough to prove |
|
1355 |
the conclusion, for we have the following theorem at our disposal: |
|
1356 |
\begin{isabelle} |
|
1357 |
\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m% |
|
1358 |
\rulename{dvd_mod_imp_dvd} |
|
1359 |
\end{isabelle} |
|
1360 |
% |
|
1361 |
This theorem can be applied in various ways. As an introduction rule, it |
|
1362 |
would cause backward chaining from the conclusion (namely |
|
10854 | 1363 |
\isa{?k~dvd~?m}) to the two premises, which |
10295 | 1364 |
also involve the divides relation. This process does not look promising |
1365 |
and could easily loop. More sensible is to apply the rule in the forward |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1366 |
direction; each step would eliminate an occurrence of the \isa{mod} symbol, so the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1367 |
process must terminate. |
10295 | 1368 |
|
1369 |
So the final proof step applies the \isa{blast} method. |
|
1370 |
Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells \isa{blast} |
|
1371 |
to use it as destruction rule: in the forward direction. |
|
1372 |
||
1373 |
\medskip |
|
1374 |
We have proved a conjunction. Now, let us give names to each of the |
|
1375 |
two halves: |
|
1376 |
\begin{isabelle} |
|
1377 |
\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline |
|
1378 |
\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]% |
|
1379 |
\end{isabelle} |
|
1380 |
||
1381 |
Several things are happening here. The keyword \isacommand{lemmas} |
|
1382 |
tells Isabelle to transform a theorem in some way and to |
|
1383 |
give a name to the resulting theorem. Attributes can be given, |
|
1384 |
here \isa{iff}, which supplies the new theorems to the classical reasoner |
|
10854 | 1385 |
and the simplifier. The directive \isa{THEN}, described in |
1386 |
\S\ref{sec:forward} below, supplies the lemma |
|
10295 | 1387 |
\isa{gcd_dvd_both} to the |
10854 | 1388 |
destruction rule \isa{conjunct1}. The effect is to extract the first part: |
10295 | 1389 |
\begin{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1390 |
\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?m1 |
10295 | 1391 |
\end{isabelle} |
1392 |
The variable names \isa{?m1} and \isa{?n1} arise because |
|
1393 |
Isabelle renames schematic variables to prevent |
|
1394 |
clashes. The second \isacommand{lemmas} declaration yields |
|
1395 |
\begin{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1396 |
\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?n1 |
10295 | 1397 |
\end{isabelle} |
1398 |
||
10854 | 1399 |
\medskip |
10596 | 1400 |
To complete the verification of the \isa{gcd} function, we must |
10295 | 1401 |
prove that it returns the greatest of all the common divisors |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1402 |
of its arguments. The proof is by induction, case analysis and simplification. |
10295 | 1403 |
\begin{isabelle} |
1404 |
\isacommand{lemma}\ gcd_greatest\ |
|
10301 | 1405 |
[rule_format]:\isanewline |
10792 | 1406 |
\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\ |
1407 |
k\ dvd\ gcd(m,n)"\isanewline |
|
10854 | 1408 |
\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline |
10301 | 1409 |
\isacommand{apply}\ (case_tac\ "n=0")\isanewline |
10295 | 1410 |
\isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline |
1411 |
\isacommand{done} |
|
1412 |
\end{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1413 |
|
10854 | 1414 |
The case analysis is performed by \isa{case_tac~"n=0"}: the operand has type |
1415 |
\isa{bool}. Until now, we have used \isa{case_tac} only with datatypes, and since |
|
1416 |
\isa{nat} is a datatype, we could have written |
|
1417 |
\isa{case_tac~"n"} with a similar effect. However, the definition of \isa{gcd} |
|
1418 |
makes a Boolean decision: |
|
1419 |
\begin{isabelle} |
|
1420 |
\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" |
|
1421 |
\end{isabelle} |
|
1422 |
Proofs about a function frequently follow the function's definition, so we perform |
|
1423 |
case analysis over the same formula. |
|
1424 |
||
1425 |
\begingroup\samepage |
|
1426 |
\begin{isabelle} |
|
1427 |
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline |
|
1428 |
\ \ \ \ \ \ \ \ \ \ \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline |
|
1429 |
\ \ \ \ \ \ \ \ \ \ \ \ \ n\ =\ 0\isasymrbrakk \isanewline |
|
1430 |
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n) |
|
1431 |
\pagebreak[0]\isanewline |
|
1432 |
\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline |
|
1433 |
\ \ \ \ \ \ \ \ \ \ \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline |
|
1434 |
\ \ \ \ \ \ \ \ \ \ \ \ \ n\ \isasymnoteq \ 0\isasymrbrakk \isanewline |
|
1435 |
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n) |
|
1436 |
\end{isabelle} |
|
1437 |
\endgroup |
|
1438 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1439 |
\begin{warn} |
10295 | 1440 |
Note that the theorem has been expressed using HOL implication, |
1441 |
\isa{\isasymlongrightarrow}, because the induction affects the two |
|
1442 |
preconditions. The directive \isa{rule_format} tells Isabelle to replace |
|
1443 |
each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1444 |
storing the theorem we have proved. This directive can also remove outer |
10295 | 1445 |
universal quantifiers, converting a theorem into the usual format for |
10854 | 1446 |
inference rules. (See \S\ref{sec:forward}.) |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1447 |
\end{warn} |
10295 | 1448 |
|
1449 |
The facts proved above can be summarized as a single logical |
|
1450 |
equivalence. This step gives us a chance to see another application |
|
1451 |
of \isa{blast}, and it is worth doing for sound logical reasons. |
|
1452 |
\begin{isabelle} |
|
10301 | 1453 |
\isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline |
10792 | 1454 |
\ \ \ \ \ \ \ \ \ "(k\ dvd\ gcd(m,n))\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ |
1455 |
n)"\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1456 |
\isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans) |
10295 | 1457 |
\end{isabelle} |
10596 | 1458 |
This theorem concisely expresses the correctness of the \isa{gcd} |
10295 | 1459 |
function. |
10596 | 1460 |
We state it with the \isa{iff} attribute so that |
1461 |
Isabelle can use it to remove some occurrences of \isa{gcd}. |
|
10295 | 1462 |
The theorem has a one-line |
10596 | 1463 |
proof using \isa{blast} supplied with four introduction |
10295 | 1464 |
rules: note the {\isa{intro}} attribute. The exclamation mark |
1465 |
({\isa{intro}}{\isa{!}})\ signifies safe rules, which are |
|
1466 |
applied aggressively. Rules given without the exclamation mark |
|
1467 |
are applied reluctantly and their uses can be undone if |
|
1468 |
the search backtracks. Here the unsafe rule expresses transitivity |
|
1469 |
of the divides relation: |
|
1470 |
\begin{isabelle} |
|
1471 |
\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p% |
|
1472 |
\rulename{dvd_trans} |
|
1473 |
\end{isabelle} |
|
1474 |
Applying \isa{dvd_trans} as |
|
1475 |
an introduction rule entails a risk of looping, for it multiplies |
|
1476 |
occurrences of the divides symbol. However, this proof relies |
|
1477 |
on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply |
|
1478 |
aggressively because it yields simpler subgoals. The proof implicitly |
|
1479 |
uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were |
|
1480 |
declared using \isa{iff}. |
|
1481 |
||
1482 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1483 |
\section{Other Classical Reasoning Methods} |
10295 | 1484 |
|
10596 | 1485 |
The \isa{blast} method is our main workhorse for proving theorems |
10295 | 1486 |
automatically. Other components of the classical reasoner interact |
1487 |
with the simplifier. Still others perform classical reasoning |
|
1488 |
to a limited extent, giving the user fine control over the proof. |
|
1489 |
||
1490 |
Of the latter methods, the most useful is {\isa{clarify}}. It performs |
|
1491 |
all obvious reasoning steps without splitting the goal into multiple |
|
1492 |
parts. It does not apply rules that could render the |
|
1493 |
goal unprovable (so-called unsafe rules). By performing the obvious |
|
1494 |
steps, {\isa{clarify}} lays bare the difficult parts of the problem, |
|
1495 |
where human intervention is necessary. |
|
1496 |
||
1497 |
For example, the following conjecture is false: |
|
1498 |
\begin{isabelle} |
|
1499 |
\isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\ |
|
1500 |
({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\ |
|
1501 |
\isasymand\ Q\ x)"\isanewline |
|
1502 |
\isacommand{apply}\ clarify |
|
1503 |
\end{isabelle} |
|
10596 | 1504 |
The \isa{blast} method would simply fail, but {\isa{clarify}} presents |
10295 | 1505 |
a subgoal that helps us see why we cannot continue the proof. |
1506 |
\begin{isabelle} |
|
10596 | 1507 |
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\ |
10295 | 1508 |
xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x |
1509 |
\end{isabelle} |
|
1510 |
The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x} |
|
1511 |
refer to distinct bound variables. To reach this state, \isa{clarify} applied |
|
1512 |
the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall} |
|
1513 |
and the elimination rule for ~\isa{\isasymand}. It did not apply the introduction |
|
1514 |
rule for \isa{\isasymand} because of its policy never to split goals. |
|
1515 |
||
1516 |
Also available is {\isa{clarsimp}}, a method that interleaves {\isa{clarify}} |
|
1517 |
and {\isa{simp}}. Also there is \isa{safe}, which like \isa{clarify} performs |
|
1518 |
obvious steps and even applies those that split goals. |
|
1519 |
||
10546 | 1520 |
The \isa{force} method applies the classical reasoner and simplifier |
10295 | 1521 |
to one goal. |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1522 |
%% \REMARK{example needed of \isa{force}?} |
10295 | 1523 |
Unless it can prove the goal, it fails. Contrast |
10546 | 1524 |
that with the \isa{auto} method, which also combines classical reasoning |
10295 | 1525 |
with simplification. The latter's purpose is to prove all the |
1526 |
easy subgoals and parts of subgoals. Unfortunately, it can produce |
|
1527 |
large numbers of new subgoals; also, since it proves some subgoals |
|
1528 |
and splits others, it obscures the structure of the proof tree. |
|
10546 | 1529 |
The \isa{force} method does not have these drawbacks. Another |
1530 |
difference: \isa{force} tries harder than {\isa{auto}} to prove |
|
10295 | 1531 |
its goal, so it can take much longer to terminate. |
1532 |
||
1533 |
Older components of the classical reasoner have largely been |
|
10596 | 1534 |
superseded by \isa{blast}, but they still have niche applications. |
1535 |
Most important among these are \isa{fast} and \isa{best}. While \isa{blast} |
|
10295 | 1536 |
searches for proofs using a built-in first-order reasoner, these |
1537 |
earlier methods search for proofs using standard Isabelle inference. |
|
1538 |
That makes them slower but enables them to work correctly in the |
|
1539 |
presence of the more unusual features of Isabelle rules, such |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1540 |
as type classes and function unknowns. For example, recall the introduction rule |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1541 |
for Hilbert's epsilon-operator: |
10295 | 1542 |
\begin{isabelle} |
10546 | 1543 |
?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x) |
10295 | 1544 |
\rulename{someI} |
1545 |
\end{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1546 |
% |
10295 | 1547 |
The repeated occurrence of the variable \isa{?P} makes this rule tricky |
1548 |
to apply. Consider this contrived example: |
|
1549 |
\begin{isabelle} |
|
10596 | 1550 |
\isacommand{lemma}\ "\isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\isanewline |
10295 | 1551 |
\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\ |
1552 |
\isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline |
|
1553 |
\isacommand{apply}\ (rule\ someI) |
|
1554 |
\end{isabelle} |
|
1555 |
% |
|
1556 |
We can apply rule \isa{someI} explicitly. It yields the |
|
1557 |
following subgoal: |
|
1558 |
\begin{isabelle} |
|
10596 | 1559 |
\ 1.\ \isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\ |
10295 | 1560 |
\isasymand\ Q\ ?x% |
1561 |
\end{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1562 |
The proof from this point is trivial. Could we have |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1563 |
proved the theorem with a single command? Not using \isa{blast}: it |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1564 |
cannot perform the higher-order unification needed here. The |
10596 | 1565 |
\isa{fast} method succeeds: |
10295 | 1566 |
\begin{isabelle} |
1567 |
\isacommand{apply}\ (fast\ intro!:\ someI) |
|
1568 |
\end{isabelle} |
|
1569 |
||
10596 | 1570 |
The \isa{best} method is similar to \isa{fast} but it uses a |
10295 | 1571 |
best-first search instead of depth-first search. Accordingly, |
1572 |
it is slower but is less susceptible to divergence. Transitivity |
|
10596 | 1573 |
rules usually cause \isa{fast} to loop where often \isa{best} |
10295 | 1574 |
can manage. |
1575 |
||
1576 |
Here is a summary of the classical reasoning methods: |
|
1577 |
\begin{itemize} |
|
1578 |
\item \isa{blast} works automatically and is the fastest |
|
1579 |
\item \isa{clarify} and \isa{clarsimp} perform obvious steps without splitting the |
|
1580 |
goal; \isa{safe} even splits goals |
|
1581 |
\item \isa{force} uses classical reasoning and simplification to prove a goal; |
|
1582 |
\isa{auto} is similar but leaves what it cannot prove |
|
1583 |
\item \isa{fast} and \isa{best} are legacy methods that work well with rules involving |
|
1584 |
unusual features |
|
1585 |
\end{itemize} |
|
1586 |
A table illustrates the relationships among four of these methods. |
|
1587 |
\begin{center} |
|
1588 |
\begin{tabular}{r|l|l|} |
|
1589 |
& no split & split \\ \hline |
|
1590 |
no simp & \isa{clarify} & \isa{safe} \\ \hline |
|
1591 |
simp & \isa{clarsimp} & \isa{auto} \\ \hline |
|
1592 |
\end{tabular} |
|
1593 |
\end{center} |
|
1594 |
||
1595 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1596 |
\section{Directives for Forward Proof}\label{sec:forward} |
10295 | 1597 |
|
1598 |
Forward proof means deriving new facts from old ones. It is the |
|
1599 |
most fundamental type of proof. Backward proof, by working from goals to |
|
1600 |
subgoals, can help us find a difficult proof. But it is |
|
1601 |
not always the best way of presenting the proof so found. Forward |
|
10301 | 1602 |
proof is particularly good for reasoning from the general |
10295 | 1603 |
to the specific. For example, consider the following distributive law for |
1604 |
the |
|
1605 |
\isa{gcd} function: |
|
1606 |
\[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\] |
|
1607 |
||
1608 |
Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$) |
|
1609 |
\[ k = \gcd(k,k\times n)\] |
|
1610 |
We have derived a new fact about \isa{gcd}; if re-oriented, it might be |
|
1611 |
useful for simplification. After re-orienting it and putting $n=1$, we |
|
1612 |
derive another useful law: |
|
1613 |
\[ \gcd(k,k)=k \] |
|
1614 |
Substituting values for variables --- instantiation --- is a forward step. |
|
1615 |
Re-orientation works by applying the symmetry of equality to |
|
1616 |
an equation, so it too is a forward step. |
|
1617 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1618 |
\subsection{The {\tt\slshape of} and {\tt\slshape THEN} Directives} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1619 |
|
10295 | 1620 |
Now let us reproduce our examples in Isabelle. Here is the distributive |
1621 |
law: |
|
1622 |
\begin{isabelle}% |
|
10596 | 1623 |
?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n) |
10295 | 1624 |
\rulename{gcd_mult_distrib2} |
1625 |
\end{isabelle}% |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1626 |
The first step is to replace \isa{?m} by~1 in this law. The \isa{of} directive |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1627 |
refers to variables not by name but by their order of occurrence in the theorem. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1628 |
In this case, the variables are \isa{?k}, \isa{?m} and~\isa{?n}. So, the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1629 |
expression |
10295 | 1630 |
\hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m} |
1631 |
by~\isa{1}. |
|
1632 |
\begin{isabelle} |
|
1633 |
\isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1] |
|
1634 |
\end{isabelle} |
|
1635 |
% |
|
1636 |
The command |
|
1637 |
\isa{thm gcd_mult_0} |
|
1638 |
displays the resulting theorem: |
|
1639 |
\begin{isabelle} |
|
10596 | 1640 |
\ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n) |
10295 | 1641 |
\end{isabelle} |
1642 |
Something is odd: {\isa{k}} is an ordinary variable, while {\isa{?n}} |
|
1643 |
is schematic. We did not specify an instantiation |
|
1644 |
for {\isa{?n}}. In its present form, the theorem does not allow |
|
1645 |
substitution for {\isa{k}}. One solution is to avoid giving an instantiation for |
|
1646 |
\isa{?k}: instead of a term we can put an underscore~(\isa{_}). For example, |
|
1647 |
\begin{isabelle} |
|
1648 |
\ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1] |
|
1649 |
\end{isabelle} |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1650 |
replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1651 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1652 |
The next step is to put |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1653 |
the theorem \isa{gcd_mult_0} into a simplified form, performing the steps |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1654 |
$\gcd(1,n)=1$ and $k\times1=k$. The \isa{simplified}\indexbold{simplified} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1655 |
attribute takes a theorem |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1656 |
and returns the result of simplifying it, with respect to the default |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1657 |
simplification rules: |
10295 | 1658 |
\begin{isabelle} |
1659 |
\isacommand{lemmas}\ |
|
1660 |
gcd_mult_1\ =\ gcd_mult_0\ |
|
1661 |
[simplified]% |
|
1662 |
\end{isabelle} |
|
1663 |
% |
|
1664 |
Again, we display the resulting theorem: |
|
1665 |
\begin{isabelle} |
|
10596 | 1666 |
\ \ \ \ \ k\ =\ gcd\ (k,\ k\ *\ ?n) |
10295 | 1667 |
\end{isabelle} |
1668 |
% |
|
1669 |
To re-orient the equation requires the symmetry rule: |
|
1670 |
\begin{isabelle} |
|
1671 |
?s\ =\ ?t\ |
|
1672 |
\isasymLongrightarrow\ ?t\ =\ |
|
1673 |
?s% |
|
1674 |
\rulename{sym} |
|
1675 |
\end{isabelle} |
|
1676 |
The following declaration gives our equation to \isa{sym}: |
|
1677 |
\begin{isabelle} |
|
1678 |
\ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\ |
|
1679 |
[THEN\ sym] |
|
1680 |
\end{isabelle} |
|
1681 |
% |
|
1682 |
Here is the result: |
|
1683 |
\begin{isabelle} |
|
10596 | 1684 |
\ \ \ \ \ gcd\ (k,\ k\ *\ ?n)\ =\ k% |
10295 | 1685 |
\end{isabelle} |
1686 |
\isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1687 |
resulting conclusion. The effect is to exchange the |
10596 | 1688 |
two operands of the equality. Typically \isa{THEN} is used with destruction |
10295 | 1689 |
rules. Above we have used |
1690 |
\isa{THEN~conjunct1} to extract the first part of the theorem |
|
1691 |
\isa{gcd_dvd_both}. Also useful is \isa{THEN~spec}, which removes the quantifier |
|
1692 |
from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp}, which converts the |
|
1693 |
implication $P\imp Q$ into the rule $\vcenter{\infer{Q}{P}}$. |
|
1694 |
Similar to \isa{mp} are the following two rules, which extract |
|
1695 |
the two directions of reasoning about a boolean equivalence: |
|
1696 |
\begin{isabelle} |
|
10596 | 1697 |
\isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% |
10295 | 1698 |
\rulename{iffD1}% |
1699 |
\isanewline |
|
10596 | 1700 |
\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% |
10295 | 1701 |
\rulename{iffD2} |
1702 |
\end{isabelle} |
|
1703 |
% |
|
1704 |
Normally we would never name the intermediate theorems |
|
1705 |
such as \isa{gcd_mult_0} and |
|
1706 |
\isa{gcd_mult_1} but would combine |
|
1707 |
the three forward steps: |
|
1708 |
\begin{isabelle} |
|
1709 |
\isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]% |
|
1710 |
\end{isabelle} |
|
1711 |
The directives, or attributes, are processed from left to right. This |
|
1712 |
declaration of \isa{gcd_mult} is equivalent to the |
|
1713 |
previous one. |
|
1714 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1715 |
Such declarations can make the proof script hard to read. Better |
10295 | 1716 |
is to state the new lemma explicitly and to prove it using a single |
1717 |
\isa{rule} method whose operand is expressed using forward reasoning: |
|
1718 |
\begin{isabelle} |
|
1719 |
\isacommand{lemma}\ gcd_mult\ |
|
10301 | 1720 |
[simp]:\ |
10596 | 1721 |
"gcd(k,\ k*n)\ =\ k"\isanewline |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1722 |
\isacommand{by}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]) |
10295 | 1723 |
\end{isabelle} |
1724 |
Compared with the previous proof of \isa{gcd_mult}, this |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1725 |
version shows the reader what has been proved. Also, the result will be processed |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1726 |
in the normal way. In particular, Isabelle generalizes over all variables: the |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1727 |
resulting theorem will have {\isa{?k}} instead of {\isa{k}}. |
10295 | 1728 |
|
1729 |
At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here |
|
1730 |
is the Isabelle version: |
|
1731 |
\begin{isabelle} |
|
10301 | 1732 |
\isacommand{lemma}\ gcd_self\ [simp]:\ "gcd(k,k)\ =\ k"\isanewline |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1733 |
\isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified]) |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1734 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1735 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1736 |
\medskip |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1737 |
The \isa{rule_format}\indexbold{rule_format} directive replaces a common usage |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1738 |
of \isa{THEN}\@. It is needed in proofs by induction when the induction formula must be |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1739 |
expressed using |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1740 |
\isa{\isasymlongrightarrow} and \isa{\isasymforall}. For example, in |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1741 |
Sect.\ts\ref{sec:proving-euclid} above we were able to write just this: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1742 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1743 |
\isacommand{lemma}\ gcd_greatest\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1744 |
[rule_format]:\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1745 |
\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1746 |
k\ dvd\ gcd(m,n)" |
10295 | 1747 |
\end{isabelle} |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1748 |
% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1749 |
It replaces a clumsy use of \isa{THEN}: |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1750 |
\begin{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1751 |
\isacommand{lemma}\ gcd_greatest\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1752 |
[THEN mp, THEN mp]:\isanewline |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1753 |
\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\ |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1754 |
k\ dvd\ gcd(m,n)" |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1755 |
\end{isabelle} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1756 |
% |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1757 |
Through \isa{rule_format} we can replace any number of applications of \isa{THEN} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1758 |
with the rules \isa{mp} and \isa{spec}, eliminating the outermost occurrences of |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1759 |
\isa{\isasymlongrightarrow} and \isa{\isasymforall}. |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1760 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1761 |
|
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1762 |
\subsection{The {\tt\slshape OF} Directive} |
10295 | 1763 |
|
1764 |
Recall that \isa{of} generates an instance of a rule by specifying |
|
1765 |
values for its variables. Analogous is \isa{OF}, which generates an |
|
1766 |
instance of a rule by specifying facts for its premises. Let us try |
|
1767 |
it with this rule: |
|
1768 |
\begin{isabelle} |
|
10596 | 1769 |
\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\ |
10295 | 1770 |
\isasymLongrightarrow\ ?k\ dvd\ ?m |
1771 |
\rulename{relprime_dvd_mult} |
|
1772 |
\end{isabelle} |
|
1773 |
First, we |
|
1774 |
prove an instance of its first premise: |
|
1775 |
\begin{isabelle} |
|
1776 |
\isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1777 |
\isacommand{by}\ (simp\ add:\ gcd.simps) |
10295 | 1778 |
\end{isabelle} |
1779 |
We have evaluated an application of the \isa{gcd} function by |
|
1780 |
simplification. Expression evaluation is not guaranteed to terminate, and |
|
1781 |
certainly is not efficient; Isabelle performs arithmetic operations by |
|
1782 |
rewriting symbolic bit strings. Here, however, the simplification takes |
|
10596 | 1783 |
less than one second. We can specify this new lemma to \isa{OF}, |
10295 | 1784 |
generating an instance of \isa{relprime_dvd_mult}. The expression |
1785 |
\begin{isabelle} |
|
1786 |
\ \ \ \ \ relprime_dvd_mult [OF relprime_20_81] |
|
1787 |
\end{isabelle} |
|
1788 |
yields the theorem |
|
1789 |
\begin{isabelle} |
|
10596 | 1790 |
\ \ \ \ \ \#20\ dvd\ (?m\ *\ \#81)\ \isasymLongrightarrow\ \#20\ dvd\ ?m% |
10295 | 1791 |
\end{isabelle} |
1792 |
% |
|
10596 | 1793 |
\isa{OF} takes any number of operands. Consider |
10295 | 1794 |
the following facts about the divides relation: |
1795 |
\begin{isabelle} |
|
1796 |
\isasymlbrakk?k\ dvd\ ?m;\ |
|
1797 |
?k\ dvd\ ?n\isasymrbrakk\ |
|
1798 |
\isasymLongrightarrow\ ?k\ dvd\ |
|
10596 | 1799 |
(?m\ +\ ?n) |
10295 | 1800 |
\rulename{dvd_add}\isanewline |
1801 |
?m\ dvd\ ?m% |
|
1802 |
\rulename{dvd_refl} |
|
1803 |
\end{isabelle} |
|
1804 |
Let us supply \isa{dvd_refl} for each of the premises of \isa{dvd_add}: |
|
1805 |
\begin{isabelle} |
|
1806 |
\ \ \ \ \ dvd_add [OF dvd_refl dvd_refl] |
|
1807 |
\end{isabelle} |
|
1808 |
Here is the theorem that we have expressed: |
|
1809 |
\begin{isabelle} |
|
10596 | 1810 |
\ \ \ \ \ ?k\ dvd\ (?k\ +\ ?k) |
10295 | 1811 |
\end{isabelle} |
1812 |
As with \isa{of}, we can use the \isa{_} symbol to leave some positions |
|
1813 |
unspecified: |
|
1814 |
\begin{isabelle} |
|
1815 |
\ \ \ \ \ dvd_add [OF _ dvd_refl] |
|
1816 |
\end{isabelle} |
|
1817 |
The result is |
|
1818 |
\begin{isabelle} |
|
10596 | 1819 |
\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k) |
10295 | 1820 |
\end{isabelle} |
1821 |
||
10596 | 1822 |
You may have noticed that \isa{THEN} and \isa{OF} are based on |
10295 | 1823 |
the same idea, namely to combine two rules. They differ in the |
1824 |
order of the combination and thus in their effect. We use \isa{THEN} |
|
1825 |
typically with a destruction rule to extract a subformula of the current |
|
1826 |
theorem. We use \isa{OF} with a list of facts to generate an instance of |
|
1827 |
the current theorem. |
|
1828 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1829 |
Here is a summary of some primitives for forward reasoning: |
10295 | 1830 |
\begin{itemize} |
10596 | 1831 |
\item \isa{of} instantiates the variables of a rule to a list of terms |
1832 |
\item \isa{OF} applies a rule to a list of theorems |
|
1833 |
\item \isa{THEN} gives a theorem to a named rule and returns the |
|
10295 | 1834 |
conclusion |
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1835 |
\item \isa{rule_format} puts a theorem into standard form |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1836 |
by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall} |
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1837 |
\item \isa{simplified} applies the simplifier to a theorem |
10295 | 1838 |
\end{itemize} |
1839 |
||
1840 |
||
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1841 |
\section{Methods for Forward Proof} |
10295 | 1842 |
|
1843 |
We have seen that forward proof works well within a backward |
|
1844 |
proof. Also in that spirit is the \isa{insert} method, which inserts a |
|
1845 |
given theorem as a new assumption of the current subgoal. This already |
|
1846 |
is a forward step; moreover, we may (as always when using a theorem) apply |
|
10596 | 1847 |
\isa{of}, \isa{THEN} and other directives. The new assumption can then |
10295 | 1848 |
be used to help prove the subgoal. |
1849 |
||
1850 |
For example, consider this theorem about the divides relation. |
|
1851 |
Only the first proof step is given; it inserts the distributive law for |
|
1852 |
\isa{gcd}. We specify its variables as shown. |
|
1853 |
\begin{isabelle} |
|
1854 |
\isacommand{lemma}\ |
|
1855 |
relprime_dvd_mult:\isanewline |
|
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset
|
1856 |
\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ (m*n)\ |
10596 | 1857 |
\isasymrbrakk\ |
10295 | 1858 |
\isasymLongrightarrow\ k\ dvd\ |
1859 |
m"\isanewline |
|
1860 |
\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\ |
|
1861 |
n]) |
|
1862 |
\end{isabelle} |
|
1863 |
In the resulting subgoal, note how the equation has been |
|
1864 |
inserted: |
|
1865 |
\begin{isabelle} |
|
10596 | 1866 |
\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ |
1867 |
dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\ |
|
10295 | 1868 |
m\isanewline |
10596 | 1869 |
\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline |
1870 |
\ \ \ \ \ m\ *\ gcd\ |
|
10295 | 1871 |
(k,\ n)\ |
10596 | 1872 |
=\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline |
10295 | 1873 |
\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m |
1874 |
\end{isabelle} |
|
1875 |
The next proof step, \isa{\isacommand{apply}(simp)}, |
|
1876 |
utilizes the assumption \isa{gcd(k,n)\ =\ |
|
1877 |
1}. Here is the result: |
|
1878 |
\begin{isabelle} |
|
10596 | 1879 |
\isasymlbrakk gcd\ (k,\ |
10295 | 1880 |
n)\ =\ 1;\ k\ |
10596 | 1881 |
dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\ |
10295 | 1882 |
m\isanewline |
10596 | 1883 |
\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline |
1884 |
\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline |
|
10295 | 1885 |
\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m |
1886 |
\end{isabelle} |
|
1887 |
Simplification has yielded an equation for \isa{m} that will be used to |
|
1888 |
complete the proof. |
|
1889 |
||
1890 |
\medskip |
|
10399 | 1891 |
Here is another proof using \isa{insert}. \REMARK{Effect with unknowns?} |
10295 | 1892 |
Division and remainder obey a well-known law: |
1893 |
\begin{isabelle} |
|
10596 | 1894 |
(?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m |
10295 | 1895 |
\rulename{mod_div_equality} |
1896 |
\end{isabelle} |
|
1897 |
||
1898 |
We refer to this law explicitly in the following proof: |
|
1899 |
\begin{isabelle} |
|
1900 |
\isacommand{lemma}\ div_mult_self_is_m:\ \isanewline |
|
10596 | 1901 |
\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\ |
1902 |
(m::nat)"\isanewline |
|
1903 |
\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline |
|
10295 | 1904 |
\isacommand{apply}\ (simp)\isanewline |
1905 |
\isacommand{done} |
|
1906 |
\end{isabelle} |
|
1907 |
The first step inserts the law, specifying \isa{m*n} and |
|
10301 | 1908 |
\isa{n} for its variables. Notice that non-trivial expressions must be |
10295 | 1909 |
enclosed in quotation marks. Here is the resulting |
1910 |
subgoal, with its new assumption: |
|
1911 |
\begin{isabelle} |
|
1912 |
%0\ \isacharless\ n\ \isasymLongrightarrow\ (m\ |
|
10596 | 1913 |
%*\ n)\ div\ n\ =\ m\isanewline |
10295 | 1914 |
\ 1.\ \isasymlbrakk0\ \isacharless\ |
10596 | 1915 |
n;\ \ (m\ *\ n)\ div\ n\ *\ n\ +\ (m\ *\ n)\ mod\ n\ |
1916 |
=\ m\ *\ n\isasymrbrakk\isanewline |
|
1917 |
\ \ \ \ \isasymLongrightarrow\ (m\ *\ n)\ div\ n\ |
|
10295 | 1918 |
=\ m |
1919 |
\end{isabelle} |
|
10596 | 1920 |
Simplification reduces \isa{(m\ *\ n)\ mod\ n} to zero. |
10295 | 1921 |
Then it cancels the factor~\isa{n} on both |
1922 |
sides of the equation, proving the theorem. |
|
1923 |
||
1924 |
\medskip |
|
10596 | 1925 |
A similar method is {\isa{subgoal_tac}}. Instead of inserting |
10295 | 1926 |
a theorem as an assumption, it inserts an arbitrary formula. |
1927 |
This formula must be proved later as a separate subgoal. The |
|
1928 |
idea is to claim that the formula holds on the basis of the current |
|
1929 |
assumptions, to use this claim to complete the proof, and finally |
|
1930 |
to justify the claim. It is a valuable means of giving the proof |
|
1931 |
some structure. The explicit formula will be more readable than |
|
1932 |
proof commands that yield that formula indirectly. |
|
1933 |
||
1934 |
Look at the following example. |
|
1935 |
\begin{isabelle} |
|
1936 |
\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ \#37;\ \#66\ <\ \#2*z;\ z*z\ |
|
1937 |
\isasymnoteq\ \#1225;\ Q(\#34);\ Q(\#36)\isasymrbrakk\isanewline |
|
1938 |
\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline |
|
1939 |
\isacommand{apply}\ (subgoal_tac\ "z\ =\ \#34\ \isasymor\ z\ =\ |
|
1940 |
\#36")\isanewline |
|
1941 |
\isacommand{apply}\ blast\isanewline |
|
1942 |
\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ \#35")\isanewline |
|
1943 |
\isacommand{apply}\ arith\isanewline |
|
1944 |
\isacommand{apply}\ force\isanewline |
|
1945 |
\isacommand{done} |
|
1946 |
\end{isabelle} |
|
1947 |
Let us prove it informally. The first assumption tells us |
|
1948 |
that \isa{z} is no greater than 36. The second tells us that \isa{z} |
|
1949 |
is at least 34. The third assumption tells us that \isa{z} cannot be 35, since |
|
1950 |
$35\times35=1225$. So \isa{z} is either 34 or 36, and since \isa{Q} holds for |
|
1951 |
both of those values, we have the conclusion. |
|
1952 |
||
1953 |
The Isabelle proof closely follows this reasoning. The first |
|
1954 |
step is to claim that \isa{z} is either 34 or 36. The resulting proof |
|
1955 |
state gives us two subgoals: |
|
1956 |
\begin{isabelle} |
|
10596 | 1957 |
%\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ |
10295 | 1958 |
%Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline |
10596 | 1959 |
\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline |
10295 | 1960 |
\ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline |
1961 |
\ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline |
|
10596 | 1962 |
\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline |
10295 | 1963 |
\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36 |
1964 |
\end{isabelle} |
|
1965 |
||
1966 |
The first subgoal is trivial, but for the second Isabelle needs help to eliminate |
|
1967 |
the case |
|
10596 | 1968 |
\isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two |
10295 | 1969 |
subgoals: |
1970 |
\begin{isabelle} |
|
10596 | 1971 |
\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ |
10295 | 1972 |
\#1225;\ Q\ \#34;\ Q\ \#36;\isanewline |
1973 |
\ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline |
|
1974 |
\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline |
|
10596 | 1975 |
\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline |
10295 | 1976 |
\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35 |
1977 |
\end{isabelle} |
|
1978 |
||
1979 |
Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic: |
|
10546 | 1980 |
the method {\isa{arith}}. For the second subgoal we apply the method \isa{force}, |
10295 | 1981 |
which proceeds by assuming that \isa{z}=35 and arriving at a contradiction. |
1982 |
||
1983 |
||
1984 |
\medskip |
|
1985 |
Summary of these methods: |
|
1986 |
\begin{itemize} |
|
1987 |
\item {\isa{insert}} adds a theorem as a new assumption |
|
1988 |
\item {\isa{subgoal_tac}} adds a formula as a new assumption and leaves the |
|
1989 |
subgoal of proving that formula |
|
1990 |
\end{itemize} |