summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/BasicLogic.thy

author | wenzelm |

Wed Nov 16 19:34:19 2005 +0100 (2005-11-16) | |

changeset 18193 | 54419506df9e |

parent 16417 | 9bc16273c2d4 |

child 23373 | ead82c82da9e |

permissions | -rw-r--r-- |

tuned document;

1 (* Title: HOL/Isar_examples/BasicLogic.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

5 Basic propositional and quantifier reasoning.

6 *)

8 header {* Basic logical reasoning *}

10 theory BasicLogic imports Main begin

13 subsection {* Pure backward reasoning *}

15 text {*

16 In order to get a first idea of how Isabelle/Isar proof documents

17 may look like, we consider the propositions @{text I}, @{text K},

18 and @{text S}. The following (rather explicit) proofs should

19 require little extra explanations.

20 *}

22 lemma I: "A --> A"

23 proof

24 assume A

25 show A by assumption

26 qed

28 lemma K: "A --> B --> A"

29 proof

30 assume A

31 show "B --> A"

32 proof

33 show A by assumption

34 qed

35 qed

37 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"

38 proof

39 assume "A --> B --> C"

40 show "(A --> B) --> A --> C"

41 proof

42 assume "A --> B"

43 show "A --> C"

44 proof

45 assume A

46 show C

47 proof (rule mp)

48 show "B --> C" by (rule mp)

49 show B by (rule mp)

50 qed

51 qed

52 qed

53 qed

55 text {*

56 Isar provides several ways to fine-tune the reasoning, avoiding

57 excessive detail. Several abbreviated language elements are

58 available, enabling the writer to express proofs in a more concise

59 way, even without referring to any automated proof tools yet.

61 First of all, proof by assumption may be abbreviated as a single

62 dot.

63 *}

65 lemma "A --> A"

66 proof

67 assume A

68 show A .

69 qed

71 text {*

72 In fact, concluding any (sub-)proof already involves solving any

73 remaining goals by assumption\footnote{This is not a completely

74 trivial operation, as proof by assumption may involve full

75 higher-order unification.}. Thus we may skip the rather vacuous

76 body of the above proof as well.

77 *}

79 lemma "A --> A"

80 proof

81 qed

83 text {*

84 Note that the \isacommand{proof} command refers to the @{text rule}

85 method (without arguments) by default. Thus it implicitly applies a

86 single rule, as determined from the syntactic form of the statements

87 involved. The \isacommand{by} command abbreviates any proof with

88 empty body, so the proof may be further pruned.

89 *}

91 lemma "A --> A"

92 by rule

94 text {*

95 Proof by a single rule may be abbreviated as double-dot.

96 *}

98 lemma "A --> A" ..

100 text {*

101 Thus we have arrived at an adequate representation of the proof of a

102 tautology that holds by a single standard rule.\footnote{Apparently,

103 the rule here is implication introduction.}

104 *}

106 text {*

107 Let us also reconsider @{text K}. Its statement is composed of

108 iterated connectives. Basic decomposition is by a single rule at a

109 time, which is why our first version above was by nesting two

110 proofs.

112 The @{text intro} proof method repeatedly decomposes a goal's

113 conclusion.\footnote{The dual method is @{text elim}, acting on a

114 goal's premises.}

115 *}

117 lemma "A --> B --> A"

118 proof (intro impI)

119 assume A

120 show A .

121 qed

123 text {*

124 Again, the body may be collapsed.

125 *}

127 lemma "A --> B --> A"

128 by (intro impI)

130 text {*

131 Just like @{text rule}, the @{text intro} and @{text elim} proof

132 methods pick standard structural rules, in case no explicit

133 arguments are given. While implicit rules are usually just fine for

134 single rule application, this may go too far with iteration. Thus

135 in practice, @{text intro} and @{text elim} would be typically

136 restricted to certain structures by giving a few rules only, e.g.\

137 \isacommand{proof}~@{text "(intro impI allI)"} to strip implications

138 and universal quantifiers.

140 Such well-tuned iterated decomposition of certain structures is the

141 prime application of @{text intro} and @{text elim}. In contrast,

142 terminal steps that solve a goal completely are usually performed by

143 actual automated proof methods (such as \isacommand{by}~@{text

144 blast}.

145 *}

148 subsection {* Variations of backward vs.\ forward reasoning *}

150 text {*

151 Certainly, any proof may be performed in backward-style only. On

152 the other hand, small steps of reasoning are often more naturally

153 expressed in forward-style. Isar supports both backward and forward

154 reasoning as a first-class concept. In order to demonstrate the

155 difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.

157 The first version is purely backward.

158 *}

160 lemma "A & B --> B & A"

161 proof

162 assume "A & B"

163 show "B & A"

164 proof

165 show B by (rule conjunct2)

166 show A by (rule conjunct1)

167 qed

168 qed

170 text {*

171 Above, the @{text "conjunct_1/2"} projection rules had to be named

172 explicitly, since the goals @{text B} and @{text A} did not provide

173 any structural clue. This may be avoided using \isacommand{from} to

174 focus on @{text prems} (i.e.\ the @{text "A \<and> B"} assumption) as the

175 current facts, enabling the use of double-dot proofs. Note that

176 \isacommand{from} already does forward-chaining, involving the

177 \name{conjE} rule here.

178 *}

180 lemma "A & B --> B & A"

181 proof

182 assume "A & B"

183 show "B & A"

184 proof

185 from prems show B ..

186 from prems show A ..

187 qed

188 qed

190 text {*

191 In the next version, we move the forward step one level upwards.

192 Forward-chaining from the most recent facts is indicated by the

193 \isacommand{then} command. Thus the proof of @{text "B \<and> A"} from

194 @{text "A \<and> B"} actually becomes an elimination, rather than an

195 introduction. The resulting proof structure directly corresponds to

196 that of the @{text conjE} rule, including the repeated goal

197 proposition that is abbreviated as @{text ?thesis} below.

198 *}

200 lemma "A & B --> B & A"

201 proof

202 assume "A & B"

203 then show "B & A"

204 proof -- {* rule @{text conjE} of @{text "A \<and> B"} *}

205 assume A B

206 show ?thesis .. -- {* rule @{text conjI} of @{text "B \<and> A"} *}

207 qed

208 qed

210 text {*

211 In the subsequent version we flatten the structure of the main body

212 by doing forward reasoning all the time. Only the outermost

213 decomposition step is left as backward.

214 *}

216 lemma "A & B --> B & A"

217 proof

218 assume ab: "A & B"

219 from ab have a: A ..

220 from ab have b: B ..

221 from b a show "B & A" ..

222 qed

224 text {*

225 We can still push forward-reasoning a bit further, even at the risk

226 of getting ridiculous. Note that we force the initial proof step to

227 do nothing here, by referring to the ``-'' proof method.

228 *}

230 lemma "A & B --> B & A"

231 proof -

232 {

233 assume ab: "A & B"

234 from ab have a: A ..

235 from ab have b: B ..

236 from b a have "B & A" ..

237 }

238 thus ?thesis .. -- {* rule \name{impI} *}

239 qed

241 text {*

242 \medskip With these examples we have shifted through a whole range

243 from purely backward to purely forward reasoning. Apparently, in

244 the extreme ends we get slightly ill-structured proofs, which also

245 require much explicit naming of either rules (backward) or local

246 facts (forward).

248 The general lesson learned here is that good proof style would

249 achieve just the \emph{right} balance of top-down backward

250 decomposition, and bottom-up forward composition. In general, there

251 is no single best way to arrange some pieces of formal reasoning, of

252 course. Depending on the actual applications, the intended audience

253 etc., rules (and methods) on the one hand vs.\ facts on the other

254 hand have to be emphasized in an appropriate way. This requires the

255 proof writer to develop good taste, and some practice, of course.

256 *}

258 text {*

259 For our example the most appropriate way of reasoning is probably

260 the middle one, with conjunction introduction done after

261 elimination. This reads even more concisely using

262 \isacommand{thus}, which abbreviates

263 \isacommand{then}~\isacommand{show}.\footnote{In the same vein,

264 \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.}

265 *}

267 lemma "A & B --> B & A"

268 proof

269 assume "A & B"

270 thus "B & A"

271 proof

272 assume A B

273 show ?thesis ..

274 qed

275 qed

279 subsection {* A few examples from ``Introduction to Isabelle'' *}

281 text {*

282 We rephrase some of the basic reasoning examples of

283 \cite{isabelle-intro}, using HOL rather than FOL.

284 *}

286 subsubsection {* A propositional proof *}

288 text {*

289 We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof below

290 involves forward-chaining from @{text "P \<or> P"}, followed by an

291 explicit case-analysis on the two \emph{identical} cases.

292 *}

294 lemma "P | P --> P"

295 proof

296 assume "P | P"

297 thus P

298 proof -- {*

299 rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}

300 *}

301 assume P show P .

302 next

303 assume P show P .

304 qed

305 qed

307 text {*

308 Case splits are \emph{not} hardwired into the Isar language as a

309 special feature. The \isacommand{next} command used to separate the

310 cases above is just a short form of managing block structure.

312 \medskip In general, applying proof methods may split up a goal into

313 separate ``cases'', i.e.\ new subgoals with individual local

314 assumptions. The corresponding proof text typically mimics this by

315 establishing results in appropriate contexts, separated by blocks.

317 In order to avoid too much explicit parentheses, the Isar system

318 implicitly opens an additional block for any new goal, the

319 \isacommand{next} statement then closes one block level, opening a

320 new one. The resulting behavior is what one would expect from

321 separating cases, only that it is more flexible. E.g.\ an induction

322 base case (which does not introduce local assumptions) would

323 \emph{not} require \isacommand{next} to separate the subsequent step

324 case.

326 \medskip In our example the situation is even simpler, since the two

327 cases actually coincide. Consequently the proof may be rephrased as

328 follows.

329 *}

331 lemma "P | P --> P"

332 proof

333 assume "P | P"

334 thus P

335 proof

336 assume P

337 show P .

338 show P .

339 qed

340 qed

342 text {*

343 Again, the rather vacuous body of the proof may be collapsed. Thus

344 the case analysis degenerates into two assumption steps, which are

345 implicitly performed when concluding the single rule step of the

346 double-dot proof as follows.

347 *}

349 lemma "P | P --> P"

350 proof

351 assume "P | P"

352 thus P ..

353 qed

356 subsubsection {* A quantifier proof *}

358 text {*

359 To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f

360 x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any @{text a}

361 with @{text "P (f a)"} may be taken as a witness for the second

362 existential statement.

364 The first proof is rather verbose, exhibiting quite a lot of

365 (redundant) detail. It gives explicit rules, even with some

366 instantiation. Furthermore, we encounter two new language elements:

367 the \isacommand{fix} command augments the context by some new

368 ``arbitrary, but fixed'' element; the \isacommand{is} annotation

369 binds term abbreviations by higher-order pattern matching.

370 *}

372 lemma "(EX x. P (f x)) --> (EX y. P y)"

373 proof

374 assume "EX x. P (f x)"

375 thus "EX y. P y"

376 proof (rule exE) -- {*

377 rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}

378 *}

379 fix a

380 assume "P (f a)" (is "P ?witness")

381 show ?thesis by (rule exI [of P ?witness])

382 qed

383 qed

385 text {*

386 While explicit rule instantiation may occasionally improve

387 readability of certain aspects of reasoning, it is usually quite

388 redundant. Above, the basic proof outline gives already enough

389 structural clues for the system to infer both the rules and their

390 instances (by higher-order unification). Thus we may as well prune

391 the text as follows.

392 *}

394 lemma "(EX x. P (f x)) --> (EX y. P y)"

395 proof

396 assume "EX x. P (f x)"

397 thus "EX y. P y"

398 proof

399 fix a

400 assume "P (f a)"

401 show ?thesis ..

402 qed

403 qed

405 text {*

406 Explicit @{text \<exists>}-elimination as seen above can become quite

407 cumbersome in practice. The derived Isar language element

408 ``\isakeyword{obtain}'' provides a more handsome way to do

409 generalized existence reasoning.

410 *}

412 lemma "(EX x. P (f x)) --> (EX y. P y)"

413 proof

414 assume "EX x. P (f x)"

415 then obtain a where "P (f a)" ..

416 thus "EX y. P y" ..

417 qed

419 text {*

420 Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and

421 \isakeyword{assume} together with a soundness proof of the

422 elimination involved. Thus it behaves similar to any other forward

423 proof element. Also note that due to the nature of general

424 existence reasoning involved here, any result exported from the

425 context of an \isakeyword{obtain} statement may \emph{not} refer to

426 the parameters introduced there.

427 *}

431 subsubsection {* Deriving rules in Isabelle *}

433 text {*

434 We derive the conjunction elimination rule from the corresponding

435 projections. The proof is quite straight-forward, since

436 Isabelle/Isar supports non-atomic goals and assumptions fully

437 transparently.

438 *}

440 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"

441 proof -

442 assume "A & B"

443 assume r: "A ==> B ==> C"

444 show C

445 proof (rule r)

446 show A by (rule conjunct1)

447 show B by (rule conjunct2)

448 qed

449 qed

451 text {*

452 Note that classic Isabelle handles higher rules in a slightly

453 different way. The tactic script as given in \cite{isabelle-intro}

454 for the same example of \name{conjE} depends on the primitive

455 \texttt{goal} command to decompose the rule into premises and

456 conclusion. The actual result would then emerge by discharging of

457 the context at \texttt{qed} time.

458 *}

460 end