author | wenzelm |
Sun, 14 Feb 2016 19:44:59 +0100 | |
changeset 62315 | ccb42dbf4aa1 |
parent 60530 | 44f9873d6f6f |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
24608 | 1 |
(* Title: HOL/Induct/Common_Patterns.thy |
2 |
Author: Makarius |
|
3 |
*) |
|
4 |
||
60530 | 5 |
section \<open>Common patterns of induction\<close> |
24608 | 6 |
|
7 |
theory Common_Patterns |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
60530 | 11 |
text \<open> |
24608 | 12 |
The subsequent Isar proof schemes illustrate common proof patterns |
13 |
supported by the generic @{text "induct"} method. |
|
14 |
||
15 |
To demonstrate variations on statement (goal) structure we refer to |
|
16 |
the induction rule of Peano natural numbers: @{thm nat.induct |
|
17 |
[no_vars]}, which is the simplest case of datatype induction. We |
|
18 |
shall also see more complex (mutual) datatype inductions involving |
|
19 |
several rules. Working with inductive predicates is similar, but |
|
20 |
involves explicit facts about membership, instead of implicit |
|
21 |
syntactic typing. |
|
60530 | 22 |
\<close> |
24608 | 23 |
|
24 |
||
60530 | 25 |
subsection \<open>Variations on statement structure\<close> |
24608 | 26 |
|
60530 | 27 |
subsubsection \<open>Local facts and parameters\<close> |
24608 | 28 |
|
60530 | 29 |
text \<open> |
24608 | 30 |
Augmenting a problem by additional facts and locally fixed variables |
31 |
is a bread-and-butter method in many applications. This is where |
|
32 |
unwieldy object-level @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in |
|
33 |
the past. The @{text "induct"} method works with primary means of |
|
34 |
the proof language instead. |
|
60530 | 35 |
\<close> |
24608 | 36 |
|
37 |
lemma |
|
38 |
fixes n :: nat |
|
39 |
and x :: 'a |
|
40 |
assumes "A n x" |
|
60530 | 41 |
shows "P n x" using \<open>A n x\<close> |
24608 | 42 |
proof (induct n arbitrary: x) |
43 |
case 0 |
|
60530 | 44 |
note prem = \<open>A 0 x\<close> |
62315 | 45 |
show "P 0 x" \<proof> |
24608 | 46 |
next |
47 |
case (Suc n) |
|
60530 | 48 |
note hyp = \<open>\<And>x. A n x \<Longrightarrow> P n x\<close> |
49 |
and prem = \<open>A (Suc n) x\<close> |
|
62315 | 50 |
show "P (Suc n) x" \<proof> |
24608 | 51 |
qed |
52 |
||
53 |
||
60530 | 54 |
subsubsection \<open>Local definitions\<close> |
24608 | 55 |
|
60530 | 56 |
text \<open> |
24608 | 57 |
Here the idea is to turn sub-expressions of the problem into a |
58 |
defined induction variable. This is often accompanied with fixing |
|
59 |
of auxiliary parameters in the original expression, otherwise the |
|
60 |
induction step would refer invariably to particular entities. This |
|
61 |
combination essentially expresses a partially abstracted |
|
62 |
representation of inductive expressions. |
|
60530 | 63 |
\<close> |
24608 | 64 |
|
65 |
lemma |
|
66 |
fixes a :: "'a \<Rightarrow> nat" |
|
67 |
assumes "A (a x)" |
|
60530 | 68 |
shows "P (a x)" using \<open>A (a x)\<close> |
24608 | 69 |
proof (induct n \<equiv> "a x" arbitrary: x) |
70 |
case 0 |
|
60530 | 71 |
note prem = \<open>A (a x)\<close> |
72 |
and defn = \<open>0 = a x\<close> |
|
62315 | 73 |
show "P (a x)" \<proof> |
24608 | 74 |
next |
75 |
case (Suc n) |
|
60530 | 76 |
note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close> |
77 |
and prem = \<open>A (a x)\<close> |
|
78 |
and defn = \<open>Suc n = a x\<close> |
|
62315 | 79 |
show "P (a x)" \<proof> |
24608 | 80 |
qed |
81 |
||
60530 | 82 |
text \<open> |
24608 | 83 |
Observe how the local definition @{text "n = a x"} recurs in the |
84 |
inductive cases as @{text "0 = a x"} and @{text "Suc n = a x"}, |
|
85 |
according to underlying induction rule. |
|
60530 | 86 |
\<close> |
24608 | 87 |
|
88 |
||
60530 | 89 |
subsubsection \<open>Simple simultaneous goals\<close> |
24608 | 90 |
|
60530 | 91 |
text \<open> |
24608 | 92 |
The most basic simultaneous induction operates on several goals |
93 |
one-by-one, where each case refers to induction hypotheses that are |
|
94 |
duplicated according to the number of conclusions. |
|
60530 | 95 |
\<close> |
24608 | 96 |
|
97 |
lemma |
|
98 |
fixes n :: nat |
|
99 |
shows "P n" and "Q n" |
|
100 |
proof (induct n) |
|
101 |
case 0 case 1 |
|
62315 | 102 |
show "P 0" \<proof> |
24608 | 103 |
next |
104 |
case 0 case 2 |
|
62315 | 105 |
show "Q 0" \<proof> |
24608 | 106 |
next |
107 |
case (Suc n) case 1 |
|
60530 | 108 |
note hyps = \<open>P n\<close> \<open>Q n\<close> |
62315 | 109 |
show "P (Suc n)" \<proof> |
24608 | 110 |
next |
111 |
case (Suc n) case 2 |
|
60530 | 112 |
note hyps = \<open>P n\<close> \<open>Q n\<close> |
62315 | 113 |
show "Q (Suc n)" \<proof> |
24608 | 114 |
qed |
115 |
||
60530 | 116 |
text \<open> |
24608 | 117 |
The split into subcases may be deferred as follows -- this is |
118 |
particularly relevant for goal statements with local premises. |
|
60530 | 119 |
\<close> |
24608 | 120 |
|
121 |
lemma |
|
122 |
fixes n :: nat |
|
123 |
shows "A n \<Longrightarrow> P n" |
|
124 |
and "B n \<Longrightarrow> Q n" |
|
125 |
proof (induct n) |
|
126 |
case 0 |
|
127 |
{ |
|
128 |
case 1 |
|
60530 | 129 |
note \<open>A 0\<close> |
62315 | 130 |
show "P 0" \<proof> |
24608 | 131 |
next |
132 |
case 2 |
|
60530 | 133 |
note \<open>B 0\<close> |
62315 | 134 |
show "Q 0" \<proof> |
24608 | 135 |
} |
136 |
next |
|
137 |
case (Suc n) |
|
60530 | 138 |
note \<open>A n \<Longrightarrow> P n\<close> |
139 |
and \<open>B n \<Longrightarrow> Q n\<close> |
|
24608 | 140 |
{ |
141 |
case 1 |
|
60530 | 142 |
note \<open>A (Suc n)\<close> |
62315 | 143 |
show "P (Suc n)" \<proof> |
24608 | 144 |
next |
145 |
case 2 |
|
60530 | 146 |
note \<open>B (Suc n)\<close> |
62315 | 147 |
show "Q (Suc n)" \<proof> |
24608 | 148 |
} |
149 |
qed |
|
150 |
||
151 |
||
60530 | 152 |
subsubsection \<open>Compound simultaneous goals\<close> |
24608 | 153 |
|
60530 | 154 |
text \<open> |
24608 | 155 |
The following pattern illustrates the slightly more complex |
156 |
situation of simultaneous goals with individual local assumptions. |
|
157 |
In compound simultaneous statements like this, local assumptions |
|
158 |
need to be included into each goal, using @{text "\<Longrightarrow>"} of the Pure |
|
159 |
framework. In contrast, local parameters do not require separate |
|
160 |
@{text "\<And>"} prefixes here, but may be moved into the common context |
|
161 |
of the whole statement. |
|
60530 | 162 |
\<close> |
24608 | 163 |
|
164 |
lemma |
|
165 |
fixes n :: nat |
|
166 |
and x :: 'a |
|
167 |
and y :: 'b |
|
168 |
shows "A n x \<Longrightarrow> P n x" |
|
169 |
and "B n y \<Longrightarrow> Q n y" |
|
170 |
proof (induct n arbitrary: x y) |
|
171 |
case 0 |
|
172 |
{ |
|
173 |
case 1 |
|
60530 | 174 |
note prem = \<open>A 0 x\<close> |
62315 | 175 |
show "P 0 x" \<proof> |
24608 | 176 |
} |
177 |
{ |
|
178 |
case 2 |
|
60530 | 179 |
note prem = \<open>B 0 y\<close> |
62315 | 180 |
show "Q 0 y" \<proof> |
24608 | 181 |
} |
182 |
next |
|
183 |
case (Suc n) |
|
60530 | 184 |
note hyps = \<open>\<And>x. A n x \<Longrightarrow> P n x\<close> \<open>\<And>y. B n y \<Longrightarrow> Q n y\<close> |
62315 | 185 |
then have some_intermediate_result \<proof> |
24608 | 186 |
{ |
187 |
case 1 |
|
60530 | 188 |
note prem = \<open>A (Suc n) x\<close> |
62315 | 189 |
show "P (Suc n) x" \<proof> |
24608 | 190 |
} |
191 |
{ |
|
192 |
case 2 |
|
60530 | 193 |
note prem = \<open>B (Suc n) y\<close> |
62315 | 194 |
show "Q (Suc n) y" \<proof> |
24608 | 195 |
} |
196 |
qed |
|
197 |
||
60530 | 198 |
text \<open> |
24608 | 199 |
Here @{text "induct"} provides again nested cases with numbered |
200 |
sub-cases, which allows to share common parts of the body context. |
|
201 |
In typical applications, there could be a long intermediate proof of |
|
202 |
general consequences of the induction hypotheses, before finishing |
|
203 |
each conclusion separately. |
|
60530 | 204 |
\<close> |
24608 | 205 |
|
206 |
||
60530 | 207 |
subsection \<open>Multiple rules\<close> |
24608 | 208 |
|
60530 | 209 |
text \<open> |
24608 | 210 |
Multiple induction rules emerge from mutual definitions of |
211 |
datatypes, inductive predicates, functions etc. The @{text |
|
212 |
"induct"} method accepts replicated arguments (with @{text "and"} |
|
213 |
separator), corresponding to each projection of the induction |
|
214 |
principle. |
|
215 |
||
216 |
The goal statement essentially follows the same arrangement, |
|
217 |
although it might be subdivided into simultaneous sub-problems as |
|
218 |
before! |
|
60530 | 219 |
\<close> |
24608 | 220 |
|
58310 | 221 |
datatype foo = Foo1 nat | Foo2 bar |
24608 | 222 |
and bar = Bar1 bool | Bar2 bazar |
223 |
and bazar = Bazar foo |
|
224 |
||
60530 | 225 |
text \<open> |
24608 | 226 |
The pack of induction rules for this datatype is: @{thm [display] |
58270 | 227 |
foo.induct [no_vars] bar.induct [no_vars] bazar.induct [no_vars]} |
24608 | 228 |
|
229 |
This corresponds to the following basic proof pattern: |
|
60530 | 230 |
\<close> |
24608 | 231 |
|
232 |
lemma |
|
233 |
fixes foo :: foo |
|
234 |
and bar :: bar |
|
235 |
and bazar :: bazar |
|
236 |
shows "P foo" |
|
237 |
and "Q bar" |
|
238 |
and "R bazar" |
|
239 |
proof (induct foo and bar and bazar) |
|
240 |
case (Foo1 n) |
|
62315 | 241 |
show "P (Foo1 n)" \<proof> |
24608 | 242 |
next |
243 |
case (Foo2 bar) |
|
60530 | 244 |
note \<open>Q bar\<close> |
62315 | 245 |
show "P (Foo2 bar)" \<proof> |
24608 | 246 |
next |
247 |
case (Bar1 b) |
|
62315 | 248 |
show "Q (Bar1 b)" \<proof> |
24608 | 249 |
next |
250 |
case (Bar2 bazar) |
|
60530 | 251 |
note \<open>R bazar\<close> |
62315 | 252 |
show "Q (Bar2 bazar)" \<proof> |
24608 | 253 |
next |
254 |
case (Bazar foo) |
|
60530 | 255 |
note \<open>P foo\<close> |
62315 | 256 |
show "R (Bazar foo)" \<proof> |
24608 | 257 |
qed |
258 |
||
60530 | 259 |
text \<open> |
24608 | 260 |
This can be combined with the previous techniques for compound |
261 |
statements, e.g.\ like this. |
|
60530 | 262 |
\<close> |
24608 | 263 |
|
264 |
lemma |
|
265 |
fixes x :: 'a and y :: 'b and z :: 'c |
|
266 |
and foo :: foo |
|
267 |
and bar :: bar |
|
268 |
and bazar :: bazar |
|
269 |
shows |
|
270 |
"A x foo \<Longrightarrow> P x foo" |
|
271 |
and |
|
272 |
"B1 y bar \<Longrightarrow> Q1 y bar" |
|
273 |
"B2 y bar \<Longrightarrow> Q2 y bar" |
|
274 |
and |
|
275 |
"C1 z bazar \<Longrightarrow> R1 z bazar" |
|
276 |
"C2 z bazar \<Longrightarrow> R2 z bazar" |
|
277 |
"C3 z bazar \<Longrightarrow> R3 z bazar" |
|
278 |
proof (induct foo and bar and bazar arbitrary: x and y and z) |
|
279 |
oops |
|
280 |
||
281 |
||
60530 | 282 |
subsection \<open>Inductive predicates\<close> |
24608 | 283 |
|
60530 | 284 |
text \<open> |
24608 | 285 |
The most basic form of induction involving predicates (or sets) |
286 |
essentially eliminates a given membership fact. |
|
60530 | 287 |
\<close> |
24608 | 288 |
|
289 |
inductive Even :: "nat \<Rightarrow> bool" where |
|
290 |
zero: "Even 0" |
|
291 |
| double: "Even n \<Longrightarrow> Even (2 * n)" |
|
292 |
||
293 |
lemma |
|
294 |
assumes "Even n" |
|
295 |
shows "P n" |
|
296 |
using assms |
|
297 |
proof induct |
|
298 |
case zero |
|
62315 | 299 |
show "P 0" \<proof> |
24608 | 300 |
next |
301 |
case (double n) |
|
60530 | 302 |
note \<open>Even n\<close> and \<open>P n\<close> |
62315 | 303 |
show "P (2 * n)" \<proof> |
24608 | 304 |
qed |
305 |
||
60530 | 306 |
text \<open> |
24608 | 307 |
Alternatively, an initial rule statement may be proven as follows, |
308 |
performing ``in-situ'' elimination with explicit rule specification. |
|
60530 | 309 |
\<close> |
24608 | 310 |
|
311 |
lemma "Even n \<Longrightarrow> P n" |
|
312 |
proof (induct rule: Even.induct) |
|
313 |
oops |
|
314 |
||
60530 | 315 |
text \<open> |
24608 | 316 |
Simultaneous goals do not introduce anything new. |
60530 | 317 |
\<close> |
24608 | 318 |
|
319 |
lemma |
|
320 |
assumes "Even n" |
|
321 |
shows "P1 n" and "P2 n" |
|
322 |
using assms |
|
323 |
proof induct |
|
324 |
case zero |
|
325 |
{ |
|
326 |
case 1 |
|
62315 | 327 |
show "P1 0" \<proof> |
24608 | 328 |
next |
329 |
case 2 |
|
62315 | 330 |
show "P2 0" \<proof> |
24608 | 331 |
} |
332 |
next |
|
333 |
case (double n) |
|
60530 | 334 |
note \<open>Even n\<close> and \<open>P1 n\<close> and \<open>P2 n\<close> |
24608 | 335 |
{ |
336 |
case 1 |
|
62315 | 337 |
show "P1 (2 * n)" \<proof> |
24608 | 338 |
next |
339 |
case 2 |
|
62315 | 340 |
show "P2 (2 * n)" \<proof> |
24608 | 341 |
} |
342 |
qed |
|
343 |
||
60530 | 344 |
text \<open> |
24608 | 345 |
Working with mutual rules requires special care in composing the |
346 |
statement as a two-level conjunction, using lists of propositions |
|
347 |
separated by @{text "and"}. For example: |
|
60530 | 348 |
\<close> |
24608 | 349 |
|
350 |
inductive Evn :: "nat \<Rightarrow> bool" and Odd :: "nat \<Rightarrow> bool" |
|
351 |
where |
|
352 |
zero: "Evn 0" |
|
353 |
| succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)" |
|
354 |
| succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)" |
|
355 |
||
24609 | 356 |
lemma |
357 |
"Evn n \<Longrightarrow> P1 n" |
|
358 |
"Evn n \<Longrightarrow> P2 n" |
|
359 |
"Evn n \<Longrightarrow> P3 n" |
|
360 |
and |
|
361 |
"Odd n \<Longrightarrow> Q1 n" |
|
362 |
"Odd n \<Longrightarrow> Q2 n" |
|
24608 | 363 |
proof (induct rule: Evn_Odd.inducts) |
364 |
case zero |
|
62315 | 365 |
{ case 1 show "P1 0" \<proof> } |
366 |
{ case 2 show "P2 0" \<proof> } |
|
367 |
{ case 3 show "P3 0" \<proof> } |
|
24608 | 368 |
next |
369 |
case (succ_Evn n) |
|
60530 | 370 |
note \<open>Evn n\<close> and \<open>P1 n\<close> \<open>P2 n\<close> \<open>P3 n\<close> |
62315 | 371 |
{ case 1 show "Q1 (Suc n)" \<proof> } |
372 |
{ case 2 show "Q2 (Suc n)" \<proof> } |
|
24608 | 373 |
next |
374 |
case (succ_Odd n) |
|
60530 | 375 |
note \<open>Odd n\<close> and \<open>Q1 n\<close> \<open>Q2 n\<close> |
62315 | 376 |
{ case 1 show "P1 (Suc n)" \<proof> } |
377 |
{ case 2 show "P2 (Suc n)" \<proof> } |
|
378 |
{ case 3 show "P3 (Suc n)" \<proof> } |
|
24608 | 379 |
qed |
380 |
||
44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
381 |
|
60530 | 382 |
text \<open> |
44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
383 |
Cases and hypotheses in each case can be named explicitly. |
60530 | 384 |
\<close> |
44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
385 |
|
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
386 |
inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r |
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
387 |
where |
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
388 |
refl: "star r x x" |
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
389 |
| step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
390 |
|
60530 | 391 |
text \<open>Underscores are replaced by the default name hyps:\<close> |
44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
392 |
|
53379 | 393 |
lemmas star_induct = star.induct [case_names base step[r _ IH]] |
44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
394 |
|
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
395 |
lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
53379 | 396 |
proof (induct rule: star_induct) print_cases |
397 |
case base |
|
398 |
then show ?case . |
|
44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
399 |
next |
53379 | 400 |
case (step a b c) print_facts |
401 |
from step.prems have "star r b z" by (rule step.IH) |
|
402 |
with step.r show ?case by (rule star.step) |
|
44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
403 |
qed |
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset
|
404 |
|
24608 | 405 |
end |