author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44164  238c5ea1e2ce 
child 53379  74920496ab71 
permissions  rwrr 
24608  1 
(* Title: HOL/Induct/Common_Patterns.thy 
2 
Author: Makarius 

3 
*) 

4 

5 
header {* Common patterns of induction *} 

6 

7 
theory Common_Patterns 

8 
imports Main 

9 
begin 

10 

11 
text {* 

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. 

22 
*} 

23 

24 

25 
subsection {* Variations on statement structure *} 

26 

27 
subsubsection {* Local facts and parameters *} 

28 

29 
text {* 

30 
Augmenting a problem by additional facts and locally fixed variables 

31 
is a breadandbutter method in many applications. This is where 

32 
unwieldy objectlevel @{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. 

35 
*} 

36 

37 
lemma 

38 
fixes n :: nat 

39 
and x :: 'a 

40 
assumes "A n x" 

41 
shows "P n x" using `A n x` 

42 
proof (induct n arbitrary: x) 

43 
case 0 

44 
note prem = `A 0 x` 

45 
show "P 0 x" sorry 

46 
next 

47 
case (Suc n) 

48 
note hyp = `\<And>x. A n x \<Longrightarrow> P n x` 

49 
and prem = `A (Suc n) x` 

50 
show "P (Suc n) x" sorry 

51 
qed 

52 

53 

54 
subsubsection {* Local definitions *} 

55 

56 
text {* 

57 
Here the idea is to turn subexpressions 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. 

63 
*} 

64 

65 
lemma 

66 
fixes a :: "'a \<Rightarrow> nat" 

67 
assumes "A (a x)" 

68 
shows "P (a x)" using `A (a x)` 

69 
proof (induct n \<equiv> "a x" arbitrary: x) 

70 
case 0 

71 
note prem = `A (a x)` 

72 
and defn = `0 = a x` 

73 
show "P (a x)" sorry 

74 
next 

75 
case (Suc n) 

34915  76 
note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)` 
24608  77 
and prem = `A (a x)` 
78 
and defn = `Suc n = a x` 

79 
show "P (a x)" sorry 

80 
qed 

81 

82 
text {* 

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. 

86 
*} 

87 

88 

89 
subsubsection {* Simple simultaneous goals *} 

90 

91 
text {* 

92 
The most basic simultaneous induction operates on several goals 

93 
onebyone, where each case refers to induction hypotheses that are 

94 
duplicated according to the number of conclusions. 

95 
*} 

96 

97 
lemma 

98 
fixes n :: nat 

99 
shows "P n" and "Q n" 

100 
proof (induct n) 

101 
case 0 case 1 

102 
show "P 0" sorry 

103 
next 

104 
case 0 case 2 

105 
show "Q 0" sorry 

106 
next 

107 
case (Suc n) case 1 

108 
note hyps = `P n` `Q n` 

109 
show "P (Suc n)" sorry 

110 
next 

111 
case (Suc n) case 2 

112 
note hyps = `P n` `Q n` 

113 
show "Q (Suc n)" sorry 

114 
qed 

115 

116 
text {* 

117 
The split into subcases may be deferred as follows  this is 

118 
particularly relevant for goal statements with local premises. 

119 
*} 

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 

129 
note `A 0` 

130 
show "P 0" sorry 

131 
next 

132 
case 2 

133 
note `B 0` 

134 
show "Q 0" sorry 

135 
} 

136 
next 

137 
case (Suc n) 

138 
note `A n \<Longrightarrow> P n` 

139 
and `B n \<Longrightarrow> Q n` 

140 
{ 

141 
case 1 

142 
note `A (Suc n)` 

143 
show "P (Suc n)" sorry 

144 
next 

145 
case 2 

146 
note `B (Suc n)` 

147 
show "Q (Suc n)" sorry 

148 
} 

149 
qed 

150 

151 

152 
subsubsection {* Compound simultaneous goals *} 

153 

154 
text {* 

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. 

162 
*} 

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 

174 
note prem = `A 0 x` 

175 
show "P 0 x" sorry 

176 
} 

177 
{ 

178 
case 2 

179 
note prem = `B 0 y` 

180 
show "Q 0 y" sorry 

181 
} 

182 
next 

183 
case (Suc n) 

184 
note hyps = `\<And>x. A n x \<Longrightarrow> P n x` `\<And>y. B n y \<Longrightarrow> Q n y` 

185 
then have some_intermediate_result sorry 

186 
{ 

187 
case 1 

188 
note prem = `A (Suc n) x` 

189 
show "P (Suc n) x" sorry 

190 
} 

191 
{ 

192 
case 2 

193 
note prem = `B (Suc n) y` 

194 
show "Q (Suc n) y" sorry 

195 
} 

196 
qed 

197 

198 
text {* 

199 
Here @{text "induct"} provides again nested cases with numbered 

200 
subcases, 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. 

204 
*} 

205 

206 

207 
subsection {* Multiple rules *} 

208 

209 
text {* 

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 subproblems as 

218 
before! 

219 
*} 

220 

221 
datatype foo = Foo1 nat  Foo2 bar 

222 
and bar = Bar1 bool  Bar2 bazar 

223 
and bazar = Bazar foo 

224 

225 
text {* 

226 
The pack of induction rules for this datatype is: @{thm [display] 

227 
foo_bar_bazar.inducts [no_vars]} 

228 

229 
This corresponds to the following basic proof pattern: 

230 
*} 

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) 

241 
show "P (Foo1 n)" sorry 

242 
next 

243 
case (Foo2 bar) 

244 
note `Q bar` 

245 
show "P (Foo2 bar)" sorry 

246 
next 

247 
case (Bar1 b) 

248 
show "Q (Bar1 b)" sorry 

249 
next 

250 
case (Bar2 bazar) 

251 
note `R bazar` 

252 
show "Q (Bar2 bazar)" sorry 

253 
next 

254 
case (Bazar foo) 

255 
note `P foo` 

256 
show "R (Bazar foo)" sorry 

257 
qed 

258 

259 
text {* 

260 
This can be combined with the previous techniques for compound 

261 
statements, e.g.\ like this. 

262 
*} 

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 

282 
subsection {* Inductive predicates *} 

283 

284 
text {* 

285 
The most basic form of induction involving predicates (or sets) 

286 
essentially eliminates a given membership fact. 

287 
*} 

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 

299 
show "P 0" sorry 

300 
next 

301 
case (double n) 

302 
note `Even n` and `P n` 

303 
show "P (2 * n)" sorry 

304 
qed 

305 

306 
text {* 

307 
Alternatively, an initial rule statement may be proven as follows, 

308 
performing ``insitu'' elimination with explicit rule specification. 

309 
*} 

310 

311 
lemma "Even n \<Longrightarrow> P n" 

312 
proof (induct rule: Even.induct) 

313 
oops 

314 

315 
text {* 

316 
Simultaneous goals do not introduce anything new. 

317 
*} 

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 

327 
show "P1 0" sorry 

328 
next 

329 
case 2 

330 
show "P2 0" sorry 

331 
} 

332 
next 

333 
case (double n) 

334 
note `Even n` and `P1 n` and `P2 n` 

335 
{ 

336 
case 1 

337 
show "P1 (2 * n)" sorry 

338 
next 

339 
case 2 

340 
show "P2 (2 * n)" sorry 

341 
} 

342 
qed 

343 

344 
text {* 

345 
Working with mutual rules requires special care in composing the 

346 
statement as a twolevel conjunction, using lists of propositions 

347 
separated by @{text "and"}. For example: 

348 
*} 

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 

24609  365 
{ case 1 show "P1 0" sorry } 
366 
{ case 2 show "P2 0" sorry } 

367 
{ case 3 show "P3 0" sorry } 

24608  368 
next 
369 
case (succ_Evn n) 

24609  370 
note `Evn n` and `P1 n` `P2 n` `P3 n` 
371 
{ case 1 show "Q1 (Suc n)" sorry } 

372 
{ case 2 show "Q2 (Suc n)" sorry } 

24608  373 
next 
374 
case (succ_Odd n) 

24609  375 
note `Odd n` and `Q1 n` `Q2 n` 
376 
{ case 1 show "P1 (Suc n)" sorry } 

377 
{ case 2 show "P2 (Suc n)" sorry } 

378 
{ case 3 show "P3 (Suc n)" sorry } 

24608  379 
qed 
380 

44164
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

381 

238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

382 
text {* 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

383 
Cases and hypotheses in each case can be named explicitly. 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

384 
*} 
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 

238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

391 
text{* Underscores are replaced by the default name hyps: *} 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

392 

238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

393 
lemmas star_induct = star.induct[case_names base step[r _ IH]] 
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" 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

396 
proof(induct rule: star_induct) 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

397 
print_cases 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

398 
case base thus ?case . 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

399 
next 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

400 
case (step a b c) 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

401 
from step.prems have "star r b z" by(rule step.IH) 
238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

402 
from step.r this show ?case by(rule star.step) 
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 

238c5ea1e2ce
documented extended version of case_names attribute
nipkow
parents:
34915
diff
changeset

405 

24608  406 
end 