25403
|
1 |
(*<*)theory Induction imports Main begin
|
|
2 |
fun itrev where
|
|
3 |
"itrev [] ys = ys" |
|
|
4 |
"itrev (x#xs) ys = itrev xs (x#ys)"
|
|
5 |
(*>*)
|
13999
|
6 |
|
|
7 |
section{*Case distinction and induction \label{sec:Induct}*}
|
|
8 |
|
|
9 |
text{* Computer science applications abound with inductively defined
|
|
10 |
structures, which is why we treat them in more detail. HOL already
|
|
11 |
comes with a datatype of lists with the two constructors @{text Nil}
|
|
12 |
and @{text Cons}. @{text Nil} is written @{term"[]"} and @{text"Cons x
|
|
13 |
xs"} is written @{term"x # xs"}. *}
|
|
14 |
|
|
15 |
subsection{*Case distinction\label{sec:CaseDistinction}*}
|
|
16 |
|
|
17 |
text{* We have already met the @{text cases} method for performing
|
|
18 |
binary case splits. Here is another example: *}
|
|
19 |
lemma "\<not> A \<or> A"
|
|
20 |
proof cases
|
|
21 |
assume "A" thus ?thesis ..
|
|
22 |
next
|
|
23 |
assume "\<not> A" thus ?thesis ..
|
|
24 |
qed
|
|
25 |
|
|
26 |
text{*\noindent The two cases must come in this order because @{text
|
|
27 |
cases} merely abbreviates @{text"(rule case_split_thm)"} where
|
|
28 |
@{thm[source] case_split_thm} is @{thm case_split_thm}. If we reverse
|
|
29 |
the order of the two cases in the proof, the first case would prove
|
|
30 |
@{prop"\<not> A \<Longrightarrow> \<not> A \<or> A"} which would solve the first premise of
|
|
31 |
@{thm[source] case_split_thm}, instantiating @{text ?P} with @{term "\<not>
|
|
32 |
A"}, thus making the second premise @{prop"\<not> \<not> A \<Longrightarrow> \<not> A \<or> A"}.
|
|
33 |
Therefore the order of subgoals is not always completely arbitrary.
|
|
34 |
|
|
35 |
The above proof is appropriate if @{term A} is textually small.
|
|
36 |
However, if @{term A} is large, we do not want to repeat it. This can
|
|
37 |
be avoided by the following idiom *}
|
|
38 |
|
|
39 |
lemma "\<not> A \<or> A"
|
|
40 |
proof (cases "A")
|
|
41 |
case True thus ?thesis ..
|
|
42 |
next
|
|
43 |
case False thus ?thesis ..
|
|
44 |
qed
|
|
45 |
|
|
46 |
text{*\noindent which is like the previous proof but instantiates
|
|
47 |
@{text ?P} right away with @{term A}. Thus we could prove the two
|
25412
|
48 |
cases in any order. The phrase \isakeyword{case}~@{text True}
|
|
49 |
abbreviates \isakeyword{assume}~@{text"True: A"} and analogously for
|
13999
|
50 |
@{text"False"} and @{prop"\<not>A"}.
|
|
51 |
|
|
52 |
The same game can be played with other datatypes, for example lists,
|
|
53 |
where @{term tl} is the tail of a list, and @{text length} returns a
|
|
54 |
natural number (remember: $0-1=0$):
|
|
55 |
*}
|
|
56 |
(*<*)declare length_tl[simp del](*>*)
|
|
57 |
lemma "length(tl xs) = length xs - 1"
|
|
58 |
proof (cases xs)
|
|
59 |
case Nil thus ?thesis by simp
|
|
60 |
next
|
|
61 |
case Cons thus ?thesis by simp
|
|
62 |
qed
|
25412
|
63 |
text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates
|
|
64 |
\isakeyword{assume}~@{text"Nil:"}~@{prop"xs = []"} and
|
|
65 |
\isakeyword{case}~@{text Cons} abbreviates \isakeyword{fix}~@{text"? ??"}
|
|
66 |
\isakeyword{assume}~@{text"Cons:"}~@{text"xs = ? # ??"},
|
13999
|
67 |
where @{text"?"} and @{text"??"}
|
|
68 |
stand for variable names that have been chosen by the system.
|
|
69 |
Therefore we cannot refer to them.
|
|
70 |
Luckily, this proof is simple enough we do not need to refer to them.
|
|
71 |
However, sometimes one may have to. Hence Isar offers a simple scheme for
|
|
72 |
naming those variables: replace the anonymous @{text Cons} by
|
25412
|
73 |
@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"}
|
|
74 |
\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}.
|
13999
|
75 |
In each \isakeyword{case} the assumption can be
|
|
76 |
referred to inside the proof by the name of the constructor. In
|
|
77 |
Section~\ref{sec:full-Ind} below we will come across an example
|
25403
|
78 |
of this.
|
13999
|
79 |
|
25403
|
80 |
\subsection{Structural induction}
|
13999
|
81 |
|
25403
|
82 |
We start with an inductive proof where both cases are proved automatically: *}
|
16522
|
83 |
lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)"
|
25427
|
84 |
by (induct n) simp_all
|
13999
|
85 |
|
15909
|
86 |
text{*\noindent The constraint @{text"::nat"} is needed because all of
|
|
87 |
the operations involved are overloaded.
|
25427
|
88 |
This proof also demonstrates that \isakeyword{by} can take two arguments,
|
|
89 |
one to start and one to finish the proof --- the latter is optional.
|
15909
|
90 |
|
|
91 |
If we want to expose more of the structure of the
|
13999
|
92 |
proof, we can use pattern matching to avoid having to repeat the goal
|
|
93 |
statement: *}
|
16522
|
94 |
lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" (is "?P n")
|
13999
|
95 |
proof (induct n)
|
|
96 |
show "?P 0" by simp
|
|
97 |
next
|
|
98 |
fix n assume "?P n"
|
|
99 |
thus "?P(Suc n)" by simp
|
|
100 |
qed
|
|
101 |
|
|
102 |
text{* \noindent We could refine this further to show more of the equational
|
|
103 |
proof. Instead we explore the same avenue as for case distinctions:
|
|
104 |
introducing context via the \isakeyword{case} command: *}
|
16522
|
105 |
lemma "2 * (\<Sum>i::nat \<le> n. i) = n*(n+1)"
|
13999
|
106 |
proof (induct n)
|
|
107 |
case 0 show ?case by simp
|
|
108 |
next
|
|
109 |
case Suc thus ?case by simp
|
|
110 |
qed
|
|
111 |
|
|
112 |
text{* \noindent The implicitly defined @{text ?case} refers to the
|
|
113 |
corresponding case to be proved, i.e.\ @{text"?P 0"} in the first case and
|
|
114 |
@{text"?P(Suc n)"} in the second case. Context \isakeyword{case}~@{text 0} is
|
|
115 |
empty whereas \isakeyword{case}~@{text Suc} assumes @{text"?P n"}. Again we
|
|
116 |
have the same problem as with case distinctions: we cannot refer to an anonymous @{term n}
|
|
117 |
in the induction step because it has not been introduced via \isakeyword{fix}
|
|
118 |
(in contrast to the previous proof). The solution is the one outlined for
|
|
119 |
@{text Cons} above: replace @{term Suc} by @{text"(Suc i)"}: *}
|
|
120 |
lemma fixes n::nat shows "n < n*n + 1"
|
|
121 |
proof (induct n)
|
|
122 |
case 0 show ?case by simp
|
|
123 |
next
|
|
124 |
case (Suc i) thus "Suc i < Suc i * Suc i + 1" by simp
|
|
125 |
qed
|
|
126 |
|
|
127 |
text{* \noindent Of course we could again have written
|
|
128 |
\isakeyword{thus}~@{text ?case} instead of giving the term explicitly
|
25403
|
129 |
but we wanted to use @{term i} somewhere.
|
|
130 |
|
|
131 |
\subsection{Generalization via @{text arbitrary}}
|
|
132 |
|
|
133 |
It is frequently necessary to generalize a claim before it becomes
|
|
134 |
provable by induction. The tutorial~\cite{LNCS2283} demonstrates this
|
|
135 |
with @{prop"itrev xs ys = rev xs @ ys"}, where @{text ys}
|
|
136 |
needs to be universally quantified before induction succeeds.\footnote{@{thm rev.simps(1)},\quad @{thm rev.simps(2)[no_vars]},\\ @{thm itrev.simps(1)[no_vars]},\quad @{thm itrev.simps(2)[no_vars]}} But
|
|
137 |
strictly speaking, this quantification step is already part of the
|
|
138 |
proof and the quantifiers should not clutter the original claim. This
|
|
139 |
is how the quantification step can be combined with induction: *}
|
|
140 |
lemma "itrev xs ys = rev xs @ ys"
|
25427
|
141 |
by (induct xs arbitrary: ys) simp_all
|
25403
|
142 |
text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars}
|
|
143 |
universally quantifies all \emph{vars} before the induction. Hence
|
|
144 |
they can be replaced by \emph{arbitrary} values in the proof.
|
13999
|
145 |
|
25403
|
146 |
The nice thing about generalization via @{text"arbitrary:"} is that in
|
|
147 |
the induction step the claim is available in unquantified form but
|
|
148 |
with the generalized variables replaced by @{text"?"}-variables, ready
|
|
149 |
for instantiation. In the above example the
|
|
150 |
induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}.
|
|
151 |
|
|
152 |
For the curious: @{text"arbitrary:"} introduces @{text"\<And>"}
|
|
153 |
behind the scenes.
|
|
154 |
|
|
155 |
\subsection{Inductive proofs of conditional formulae}
|
25412
|
156 |
\label{sec:full-Ind}
|
25403
|
157 |
|
|
158 |
Induction also copes well with formulae involving @{text"\<Longrightarrow>"}, for example
|
|
159 |
*}
|
|
160 |
|
|
161 |
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
|
25427
|
162 |
by (induct xs) simp_all
|
25403
|
163 |
|
|
164 |
text{*\noindent This is an improvement over that style the
|
|
165 |
tutorial~\cite{LNCS2283} advises, which requires @{text"\<longrightarrow>"}.
|
|
166 |
A further improvement is shown in the following proof:
|
|
167 |
*}
|
13999
|
168 |
|
25403
|
169 |
lemma "map f xs = map f ys \<Longrightarrow> length xs = length ys"
|
|
170 |
proof (induct ys arbitrary: xs)
|
|
171 |
case Nil thus ?case by simp
|
|
172 |
next
|
|
173 |
case (Cons y ys) note Asm = Cons
|
|
174 |
show ?case
|
|
175 |
proof (cases xs)
|
|
176 |
case Nil
|
|
177 |
hence False using Asm(2) by simp
|
|
178 |
thus ?thesis ..
|
|
179 |
next
|
|
180 |
case (Cons x xs')
|
25427
|
181 |
with Asm(2) have "map f xs' = map f ys" by simp
|
25403
|
182 |
from Asm(1)[OF this] `xs = x#xs'` show ?thesis by simp
|
|
183 |
qed
|
|
184 |
qed
|
|
185 |
|
|
186 |
text{*\noindent
|
|
187 |
The base case is trivial. In the step case Isar assumes
|
|
188 |
(under the name @{text Cons}) two propositions:
|
|
189 |
\begin{center}
|
|
190 |
\begin{tabular}{l}
|
|
191 |
@{text"map f ?xs = map f ys \<Longrightarrow> length ?xs = length ys"}\\
|
|
192 |
@{prop"map f xs = map f (y # ys)"}
|
|
193 |
\end{tabular}
|
|
194 |
\end{center}
|
|
195 |
The first is the induction hypothesis, the second, and this is new,
|
|
196 |
is the premise of the induction step. The actual goal at this point is merely
|
|
197 |
@{prop"length xs = length (y#ys)"}. The assumptions are given the new name
|
|
198 |
@{text Asm} to avoid a name clash further down. The proof procedes with a case distinction on @{text xs}. In the case @{prop"xs = []"}, the second of our two
|
|
199 |
assumptions (@{text"Asm(2)"}) implies the contradiction @{text"0 = Suc(\<dots>)"}.
|
|
200 |
In the case @{prop"xs = x#xs'"}, we first obtain
|
|
201 |
@{prop"map f xs' = map f ys"}, from which a forward step with the first assumption (@{text"Asm(1)[OF this]"}) yields @{prop"length xs' = length ys"}. Together
|
|
202 |
with @{prop"xs = x#xs"} this yields the goal
|
|
203 |
@{prop"length xs = length (y#ys)"}.
|
|
204 |
|
|
205 |
|
|
206 |
\subsection{Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}}
|
|
207 |
|
|
208 |
Let us now consider abstractly the situation where the goal to be proved
|
|
209 |
contains both @{text"\<And>"} and @{text"\<Longrightarrow>"}, say @{prop"\<And>x. P x \<Longrightarrow> Q x"}.
|
|
210 |
This means that in each case of the induction,
|
13999
|
211 |
@{text ?case} would be of the form @{prop"\<And>x. P' x \<Longrightarrow> Q' x"}. Thus the
|
|
212 |
first proof steps will be the canonical ones, fixing @{text x} and assuming
|
25403
|
213 |
@{prop"P' x"}. To avoid this tedium, induction performs the canonical steps
|
|
214 |
automatically: in each step case, the assumptions contain both the
|
|
215 |
usual induction hypothesis and @{prop"P' x"}, whereas @{text ?case} is only
|
|
216 |
@{prop"Q' x"}.
|
13999
|
217 |
|
25403
|
218 |
\subsection{Rule induction}
|
13999
|
219 |
|
25403
|
220 |
HOL also supports inductively defined sets. See \cite{LNCS2283}
|
13999
|
221 |
for details. As an example we define our own version of the reflexive
|
|
222 |
transitive closure of a relation --- HOL provides a predefined one as well.*}
|
23733
|
223 |
inductive_set
|
|
224 |
rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
|
|
225 |
for r :: "('a \<times> 'a)set"
|
|
226 |
where
|
|
227 |
refl: "(x,x) \<in> r*"
|
|
228 |
| step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
|
13999
|
229 |
|
|
230 |
text{* \noindent
|
|
231 |
First the constant is declared as a function on binary
|
|
232 |
relations (with concrete syntax @{term"r*"} instead of @{text"rtc
|
|
233 |
r"}), then the defining clauses are given. We will now prove that
|
|
234 |
@{term"r*"} is indeed transitive: *}
|
|
235 |
|
|
236 |
lemma assumes A: "(x,y) \<in> r*" shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*"
|
|
237 |
using A
|
|
238 |
proof induct
|
|
239 |
case refl thus ?case .
|
|
240 |
next
|
|
241 |
case step thus ?case by(blast intro: rtc.step)
|
|
242 |
qed
|
|
243 |
text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
|
|
244 |
\in R$ piped into the proof, here \isakeyword{using}~@{text A}. The
|
|
245 |
proof itself follows the inductive definition very
|
|
246 |
closely: there is one case for each rule, and it has the same name as
|
|
247 |
the rule, analogous to structural induction.
|
|
248 |
|
|
249 |
However, this proof is rather terse. Here is a more readable version:
|
|
250 |
*}
|
|
251 |
|
25403
|
252 |
lemma assumes "(x,y) \<in> r*" and "(y,z) \<in> r*" shows "(x,z) \<in> r*"
|
|
253 |
using assms
|
|
254 |
proof induct
|
|
255 |
fix x assume "(x,z) \<in> r*" -- {*@{text B}[@{text y} := @{text x}]*}
|
|
256 |
thus "(x,z) \<in> r*" .
|
|
257 |
next
|
|
258 |
fix x' x y
|
|
259 |
assume 1: "(x',x) \<in> r" and
|
|
260 |
IH: "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" and
|
|
261 |
B: "(y,z) \<in> r*"
|
|
262 |
from 1 IH[OF B] show "(x',z) \<in> r*" by(rule rtc.step)
|
13999
|
263 |
qed
|
25403
|
264 |
text{*\noindent
|
|
265 |
This time, merely for a change, we start the proof with by feeding both
|
|
266 |
assumptions into the inductive proof. Only the first assumption is
|
|
267 |
``consumed'' by the induction.
|
|
268 |
Since the second one is left over we don't just prove @{text ?thesis} but
|
|
269 |
@{text"(y,z) \<in> r* \<Longrightarrow> ?thesis"}, just as in the previous proof.
|
|
270 |
The base case is trivial. In the assumptions for the induction step we can
|
13999
|
271 |
see very clearly how things fit together and permit ourselves the
|
|
272 |
obvious forward step @{text"IH[OF B]"}.
|
|
273 |
|
25403
|
274 |
The notation \isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}
|
|
275 |
is also supported for inductive definitions. The \emph{constructor} is the
|
|
276 |
name of the rule and the \emph{vars} fix the free variables in the
|
13999
|
277 |
rule; the order of the \emph{vars} must correspond to the
|
25403
|
278 |
left-to-right order of the variables as they appear in the rule.
|
13999
|
279 |
For example, we could start the above detailed proof of the induction
|
25403
|
280 |
with \isakeyword{case}~\isa{(step x' x y)}. In that case we don't need
|
|
281 |
to spell out the assumptions but can refer to them by @{text"step(.)"},
|
|
282 |
although the resulting text will be quite cryptic.
|
13999
|
283 |
|
25403
|
284 |
\subsection{More induction}
|
13999
|
285 |
|
25403
|
286 |
We close the section by demonstrating how arbitrary induction
|
13999
|
287 |
rules are applied. As a simple example we have chosen recursion
|
|
288 |
induction, i.e.\ induction based on a recursive function
|
|
289 |
definition. However, most of what we show works for induction in
|
|
290 |
general.
|
|
291 |
|
|
292 |
The example is an unusual definition of rotation: *}
|
|
293 |
|
25403
|
294 |
fun rot :: "'a list \<Rightarrow> 'a list" where
|
|
295 |
"rot [] = []" |
|
|
296 |
"rot [x] = [x]" |
|
13999
|
297 |
"rot (x#y#zs) = y # rot(x#zs)"
|
|
298 |
text{*\noindent This yields, among other things, the induction rule
|
|
299 |
@{thm[source]rot.induct}: @{thm[display]rot.induct[no_vars]}
|
25403
|
300 |
The following proof relies on a default naming scheme for cases: they are
|
13999
|
301 |
called 1, 2, etc, unless they have been named explicitly. The latter happens
|
25403
|
302 |
only with datatypes and inductively defined sets, but (usually)
|
|
303 |
not with recursive functions. *}
|
13999
|
304 |
|
|
305 |
lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
|
|
306 |
proof (induct xs rule: rot.induct)
|
|
307 |
case 1 thus ?case by simp
|
|
308 |
next
|
|
309 |
case 2 show ?case by simp
|
|
310 |
next
|
|
311 |
case (3 a b cs)
|
|
312 |
have "rot (a # b # cs) = b # rot(a # cs)" by simp
|
|
313 |
also have "\<dots> = b # tl(a # cs) @ [hd(a # cs)]" by(simp add:3)
|
|
314 |
also have "\<dots> = tl (a # b # cs) @ [hd (a # b # cs)]" by simp
|
|
315 |
finally show ?case .
|
|
316 |
qed
|
|
317 |
|
|
318 |
text{*\noindent
|
|
319 |
The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01}
|
|
320 |
for how to reason with chains of equations) to demonstrate that the
|
25403
|
321 |
\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)} notation also
|
13999
|
322 |
works for arbitrary induction theorems with numbered cases. The order
|
|
323 |
of the \emph{vars} corresponds to the order of the
|
|
324 |
@{text"\<And>"}-quantified variables in each case of the induction
|
25403
|
325 |
theorem. For induction theorems produced by \isakeyword{fun} it is
|
13999
|
326 |
the order in which the variables appear on the left-hand side of the
|
|
327 |
equation.
|
|
328 |
|
|
329 |
The proof is so simple that it can be condensed to
|
|
330 |
*}
|
|
331 |
|
|
332 |
(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
|
25412
|
333 |
by (induct xs rule: rot.induct) simp_all
|
13999
|
334 |
|
|
335 |
(*<*)end(*>*)
|
25403
|
336 |
(*
|
|
337 |
lemma assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
|
|
338 |
shows "P(n::nat)"
|
|
339 |
proof (rule A)
|
|
340 |
show "\<And>m. m < n \<Longrightarrow> P m"
|
|
341 |
proof (induct n)
|
|
342 |
case 0 thus ?case by simp
|
|
343 |
next
|
|
344 |
case (Suc n) -- {*\isakeyword{fix} @{term m} \isakeyword{assume} @{text Suc}: @{text[source]"?m < n \<Longrightarrow> P ?m"} @{prop[source]"m < Suc n"}*}
|
|
345 |
show ?case -- {*@{term ?case}*}
|
|
346 |
proof cases
|
|
347 |
assume eq: "m = n"
|
|
348 |
from Suc and A have "P n" by blast
|
|
349 |
with eq show "P m" by simp
|
|
350 |
next
|
|
351 |
assume "m \<noteq> n"
|
|
352 |
with Suc have "m < n" by arith
|
|
353 |
thus "P m" by(rule Suc)
|
|
354 |
qed
|
|
355 |
qed
|
|
356 |
qed
|
|
357 |
*) |