wenzelm@6444

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

wenzelm@6444

2 
ID: $Id$

wenzelm@6444

3 
Author: Markus Wenzel, TU Muenchen

wenzelm@6444

4 

wenzelm@6444

5 
Basic propositional and quantifier reasoning.

wenzelm@6444

6 
*)

wenzelm@6444

7 

wenzelm@7748

8 
header {* Basic reasoning *};

wenzelm@7748

9 

wenzelm@6444

10 
theory BasicLogic = Main:;

wenzelm@6444

11 

wenzelm@7761

12 

wenzelm@7820

13 
subsection {* Pure backward reasoning *};

wenzelm@7740

14 

wenzelm@7820

15 
text {*

wenzelm@7820

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

wenzelm@7820

17 
look like, we consider the propositions $I$, $K$, and $S$. The

wenzelm@7820

18 
following (rather explicit) proofs should require little extra

wenzelm@7820

19 
explanations.

wenzelm@7820

20 
*};

wenzelm@7001

21 

wenzelm@6444

22 
lemma I: "A > A";

wenzelm@6444

23 
proof;

wenzelm@6444

24 
assume A;

wenzelm@7820

25 
show A; by assumption;

wenzelm@6444

26 
qed;

wenzelm@6444

27 

wenzelm@6444

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

wenzelm@6444

29 
proof;

wenzelm@6444

30 
assume A;

wenzelm@6444

31 
show "B > A";

wenzelm@6444

32 
proof;

wenzelm@7820

33 
show A; by assumption;

wenzelm@6444

34 
qed;

wenzelm@6444

35 
qed;

wenzelm@6444

36 

wenzelm@6444

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

wenzelm@6444

38 
proof;

wenzelm@6444

39 
assume "A > B > C";

wenzelm@6444

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

wenzelm@6444

41 
proof;

wenzelm@6444

42 
assume "A > B";

wenzelm@6444

43 
show "A > C";

wenzelm@6444

44 
proof;

wenzelm@6444

45 
assume A;

wenzelm@6444

46 
show C;

wenzelm@6444

47 
proof (rule mp);

wenzelm@6444

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

wenzelm@6444

49 
show B; by (rule mp);

wenzelm@6444

50 
qed;

wenzelm@6444

51 
qed;

wenzelm@6444

52 
qed;

wenzelm@6444

53 
qed;

wenzelm@6444

54 

wenzelm@7820

55 
text {*

wenzelm@7820

56 
Isar provides several ways to finetune the reasoning, avoiding

wenzelm@7820

57 
irrelevant detail. Several abbreviated language elements are

wenzelm@7820

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

wenzelm@7820

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

wenzelm@7761

60 

wenzelm@7820

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

wenzelm@7820

62 
*};

wenzelm@7820

63 

wenzelm@7820

64 
lemma "A > A";

wenzelm@7820

65 
proof;

wenzelm@7820

66 
assume A;

wenzelm@7820

67 
show A; .;

wenzelm@7820

68 
qed;

wenzelm@7820

69 

wenzelm@7820

70 
text {*

wenzelm@7820

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

wenzelm@7860

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

wenzelm@7860

73 
trivial operation. As usual in Isabelle, proof by assumption

wenzelm@7860

74 
involves full higherorder unification.}. Thus we may skip the

wenzelm@7860

75 
rather vacuous body of the above proof as well.

wenzelm@7820

76 
*};

wenzelm@7820

77 

wenzelm@7820

78 
lemma "A > A";

wenzelm@7820

79 
proof;

wenzelm@7820

80 
qed;

wenzelm@7820

81 

wenzelm@7820

82 
text {*

wenzelm@7820

83 
Note that the \isacommand{proof} command refers to the $\idt{rule}$

wenzelm@7820

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

wenzelm@7820

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

wenzelm@7820

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

wenzelm@7820

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

wenzelm@7820

88 
*};

wenzelm@7820

89 

wenzelm@7820

90 
lemma "A > A";

wenzelm@7820

91 
by rule;

wenzelm@7820

92 

wenzelm@7820

93 
text {*

wenzelm@7820

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

wenzelm@7820

95 
*};

wenzelm@7820

96 

wenzelm@7820

97 
lemma "A > A"; ..;

wenzelm@7820

98 

wenzelm@7820

99 
text {*

wenzelm@7820

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

wenzelm@7860

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

wenzelm@7860

102 
the rule is implication introduction.}

wenzelm@7820

103 
*};

wenzelm@7820

104 

wenzelm@7820

105 
text {*

wenzelm@7820

106 
Let us also reconsider $K$. It's statement is composed of iterated

wenzelm@7820

107 
connectives. Basic decomposition is by a single rule at a time,

wenzelm@7820

108 
which is why our first version above was by nesting two proofs.

wenzelm@7820

109 

wenzelm@7820

110 
The $\idt{intro}$ proof method repeatedly decomposes a goal's

wenzelm@7820

111 
conclusion.\footnote{The dual method is $\idt{elim}$, acting on a

wenzelm@7820

112 
goal's premises.}

wenzelm@7820

113 
*};

wenzelm@7820

114 

wenzelm@7820

115 
lemma "A > B > A";

wenzelm@7820

116 
proof intro;

wenzelm@7820

117 
assume A;

wenzelm@7820

118 
show A; .;

wenzelm@7820

119 
qed;

wenzelm@7820

120 

wenzelm@7820

121 
text {*

wenzelm@7820

122 
Again, the body may be collapsed.

wenzelm@7820

123 
*};

wenzelm@7820

124 

wenzelm@7820

125 
lemma "A > B > A";

wenzelm@7820

126 
by intro;

wenzelm@7820

127 

wenzelm@7820

128 
text {*

wenzelm@7820

129 
Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof

wenzelm@7820

130 
methods pick standard structural rules, in case no explicit arguments

wenzelm@7820

131 
are given. While implicit rules are usually just fine for single

wenzelm@7820

132 
rule application, this may go too far in iteration. Thus in

wenzelm@7820

133 
practice, $\idt{intro}$ and $\idt{elim}$ would be typically

wenzelm@7820

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

wenzelm@7860

135 
\isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip

wenzelm@7860

136 
implications and universal quantifiers.

wenzelm@7820

137 

wenzelm@7820

138 
Such welltuned iterated decomposition of certain structure is the

wenzelm@7860

139 
prime application of $\idt{intro}$ and $\idt{elim}$. In general,

wenzelm@7820

140 
terminal steps that solve a goal completely are typically performed

wenzelm@7860

141 
by actual automated proof methods (such as

wenzelm@7820

142 
\isacommand{by}~$\idt{blast}$).

wenzelm@7820

143 
*};

wenzelm@7820

144 

wenzelm@7820

145 

wenzelm@7820

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

wenzelm@7820

147 

wenzelm@7820

148 
text {*

wenzelm@7820

149 
Certainly, any proof may be performed in backwardstyle only. On the

wenzelm@7820

150 
other hand, small steps of reasoning are often more naturally

wenzelm@7820

151 
expressed in forwardstyle. Isar supports both backward and forward

wenzelm@7820

152 
reasoning as a firstclass concept. In order to demonstrate the

wenzelm@7820

153 
difference, we consider several proofs of $A \conj B \impl B \conj

wenzelm@7820

154 
A$.

wenzelm@7820

155 

wenzelm@7820

156 
The first version is purely backward.

wenzelm@7820

157 
*};

wenzelm@7001

158 

wenzelm@6444

159 
lemma "A & B > B & A";

wenzelm@6444

160 
proof;

wenzelm@6444

161 
assume "A & B";

wenzelm@6444

162 
show "B & A";

wenzelm@6444

163 
proof;

wenzelm@6444

164 
show B; by (rule conjunct2);

wenzelm@6444

165 
show A; by (rule conjunct1);

wenzelm@6444

166 
qed;

wenzelm@6444

167 
qed;

wenzelm@6444

168 

wenzelm@7820

169 
text {*

wenzelm@7820

170 
Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named

wenzelm@7820

171 
explicitly, since the goals did not provide any structural clue.

wenzelm@7820

172 
This may be avoided using \isacommand{from} to focus on $\idt{prems}$

wenzelm@7820

173 
(i.e.\ the $A \conj B$ assumption) as the current facts, enabling the

wenzelm@7820

174 
use of doubledot proofs. Note that \isacommand{from} already

wenzelm@7833

175 
does forwardchaining, involving the \name{conjE} rule.

wenzelm@7820

176 
*};

wenzelm@6444

177 

wenzelm@6444

178 
lemma "A & B > B & A";

wenzelm@6444

179 
proof;

wenzelm@7604

180 
assume "A & B";

wenzelm@7604

181 
show "B & A";

wenzelm@7604

182 
proof;

wenzelm@7604

183 
from prems; show B; ..;

wenzelm@7604

184 
from prems; show A; ..;

wenzelm@7604

185 
qed;

wenzelm@7604

186 
qed;

wenzelm@7604

187 

wenzelm@7820

188 
text {*

wenzelm@7820

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

wenzelm@7820

190 
Forwardchaining from the most recent facts is indicated by the

wenzelm@7820

191 
\isacommand{then} command. Thus the proof of $B \conj A$ from $A

wenzelm@7820

192 
\conj B$ actually becomes an elimination, rather than an

wenzelm@7820

193 
introduction. The resulting proof structure directly corresponds to

wenzelm@7820

194 
that of the $\name{conjE}$ rule, including the repeated goal

wenzelm@7820

195 
proposition that is abbreviated as $\var{thesis}$ below.

wenzelm@7820

196 
*};

wenzelm@7820

197 

wenzelm@7820

198 
lemma "A & B > B & A";

wenzelm@7820

199 
proof;

wenzelm@7820

200 
assume "A & B";

wenzelm@7820

201 
then; show "B & A";

wenzelm@7820

202 
proof  {* rule \name{conjE} of $A \conj B$ *};

wenzelm@7820

203 
assume A B;

wenzelm@7820

204 
show ?thesis; ..  {* rule \name{conjI} of $B \conj A$ *};

wenzelm@7820

205 
qed;

wenzelm@7820

206 
qed;

wenzelm@7820

207 

wenzelm@7820

208 
text {*

wenzelm@7820

209 
Subsequently, only the outermost decomposition step is left backward,

wenzelm@7820

210 
all the rest is forward.

wenzelm@7820

211 
*};

wenzelm@7820

212 

wenzelm@7604

213 
lemma "A & B > B & A";

wenzelm@7604

214 
proof;

wenzelm@6892

215 
assume ab: "A & B";

wenzelm@6892

216 
from ab; have a: A; ..;

wenzelm@6892

217 
from ab; have b: B; ..;

wenzelm@6892

218 
from b a; show "B & A"; ..;

wenzelm@6444

219 
qed;

wenzelm@6444

220 

wenzelm@7820

221 
text {*

wenzelm@7833

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

wenzelm@7820

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

wenzelm@7820

224 
do nothing, by referring to the ``'' proof method.

wenzelm@7820

225 
*};

wenzelm@7820

226 

wenzelm@7820

227 
lemma "A & B > B & A";

wenzelm@7820

228 
proof ;

wenzelm@7820

229 
{{;

wenzelm@7820

230 
assume ab: "A & B";

wenzelm@7820

231 
from ab; have a: A; ..;

wenzelm@7820

232 
from ab; have b: B; ..;

wenzelm@7820

233 
from b a; have "B & A"; ..;

wenzelm@7820

234 
}};

wenzelm@7820

235 
thus ?thesis; ..  {* rule \name{impI} *};

wenzelm@7820

236 
qed;

wenzelm@7820

237 

wenzelm@7820

238 
text {*

wenzelm@7820

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

wenzelm@7820

240 
from purely backward to purely forward reasoning. Apparently, in the

wenzelm@7820

241 
extreme ends we get slightly illstructured proofs, which also

wenzelm@7820

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

wenzelm@7820

243 
facts (forward).

wenzelm@7820

244 

wenzelm@7820

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

wenzelm@7820

246 
achieve just the \emph{right} balance of topdown backward

wenzelm@7820

247 
decomposition, and bottomup forward composition. In practice, there

wenzelm@7820

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

wenzelm@7820

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

wenzelm@7820

250 
etc., certain aspects such as rules~/ methods vs.\ facts have to be

wenzelm@7833

251 
emphasized in an appropriate way. This requires the proof writer to

wenzelm@7820

252 
develop good taste, and some practice, of course.

wenzelm@7820

253 
*};

wenzelm@7820

254 

wenzelm@7820

255 
text {*

wenzelm@7820

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

wenzelm@7820

257 
middle one, with conjunction introduction done after elimination.

wenzelm@7820

258 
This reads even more concisely using \isacommand{thus}, which

wenzelm@7820

259 
abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same

wenzelm@7820

260 
vein, \isacommand{hence} abbreviates

wenzelm@7820

261 
\isacommand{then}~\isacommand{have}.}

wenzelm@7820

262 
*};

wenzelm@7820

263 

wenzelm@7820

264 
lemma "A & B > B & A";

wenzelm@7820

265 
proof;

wenzelm@7820

266 
assume "A & B";

wenzelm@7820

267 
thus "B & A";

wenzelm@7820

268 
proof;

wenzelm@7820

269 
assume A B;

wenzelm@7820

270 
show ?thesis; ..;

wenzelm@7820

271 
qed;

wenzelm@7820

272 
qed;

wenzelm@7820

273 

wenzelm@7820

274 

wenzelm@6444

275 

wenzelm@7740

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

wenzelm@7001

277 

wenzelm@7820

278 
text {*

wenzelm@7820

279 
We rephrase some of the basic reasoning examples of

wenzelm@7833

280 
\cite{isabelleintro} (using HOL rather than FOL).

wenzelm@7820

281 
*};

wenzelm@7820

282 

wenzelm@7833

283 
subsubsection {* A propositional proof *};

wenzelm@7833

284 

wenzelm@7833

285 
text {*

wenzelm@7833

286 
We consider the proposition $P \disj P \impl P$. The proof below

wenzelm@7833

287 
involves forwardchaining from $P \disj P$, followed by an explicit

wenzelm@7833

288 
caseanalysis on the two \emph{identical} cases.

wenzelm@7833

289 
*};

wenzelm@6444

290 

wenzelm@6444

291 
lemma "P  P > P";

wenzelm@6444

292 
proof;

wenzelm@6444

293 
assume "P  P";

wenzelm@7833

294 
thus P;

wenzelm@7833

295 
proof  {*

wenzelm@7833

296 
rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}

wenzelm@7833

297 
*};

wenzelm@7833

298 
assume P; show P; .;

wenzelm@7833

299 
next;

wenzelm@7833

300 
assume P; show P; .;

wenzelm@7833

301 
qed;

wenzelm@7833

302 
qed;

wenzelm@7833

303 

wenzelm@7833

304 
text {*

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

308 

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

311 
assumptions. The corresponding proof text typically mimics this by

wenzelm@7833

312 
establishing results in appropriate contexts, separated by blocks.

wenzelm@7833

313 

wenzelm@7860

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

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

317 
new one. The resulting behavior is what one might expect from

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

321 
case.

wenzelm@7833

322 

wenzelm@7833

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

wenzelm@7833

324 
``cases'' actually coincide. Consequently the proof may be rephrased

wenzelm@7833

325 
as follows.

wenzelm@7833

326 
*};

wenzelm@7833

327 

wenzelm@7833

328 
lemma "P  P > P";

wenzelm@7833

329 
proof;

wenzelm@7833

330 
assume "P  P";

wenzelm@7833

331 
thus P;

wenzelm@6444

332 
proof;

wenzelm@6444

333 
assume P;

wenzelm@6444

334 
show P; .;

wenzelm@6444

335 
show P; .;

wenzelm@6444

336 
qed;

wenzelm@6444

337 
qed;

wenzelm@6444

338 

wenzelm@7833

339 
text {*

wenzelm@7833

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

wenzelm@7860

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

wenzelm@7860

342 
implicitly performed when concluding the single rule step of the

wenzelm@7860

343 
doubledot proof as follows.

wenzelm@7833

344 
*};

wenzelm@7833

345 

wenzelm@6444

346 
lemma "P  P > P";

wenzelm@6444

347 
proof;

wenzelm@6444

348 
assume "P  P";

wenzelm@7833

349 
thus P; ..;

wenzelm@6444

350 
qed;

wenzelm@6444

351 

wenzelm@6444

352 

wenzelm@7833

353 
subsubsection {* A quantifier proof *};

wenzelm@7833

354 

wenzelm@7833

355 
text {*

wenzelm@7833

356 
To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap

wenzelm@7833

357 
x)) \impl (\ex x P \ap x)$. Informally, this holds because any $a$

wenzelm@7833

358 
with $P \ap (f \ap a)$ may be taken as a witness for the second

wenzelm@7833

359 
existential statement.

wenzelm@6444

360 

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

366 
binds term abbreviations by higherorder pattern matching.

wenzelm@7833

367 
*};

wenzelm@7833

368 

wenzelm@7833

369 
lemma "(EX x. P (f x)) > (EX x. P x)";

wenzelm@6444

370 
proof;

wenzelm@7833

371 
assume "EX x. P (f x)";

wenzelm@7833

372 
thus "EX x. P x";

wenzelm@7833

373 
proof (rule exE)  {*

wenzelm@7833

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

wenzelm@7833

375 
*};

wenzelm@6444

376 
fix a;

wenzelm@7833

377 
assume "P (f a)" (is "P ?witness");

wenzelm@7480

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

wenzelm@6444

379 
qed;

wenzelm@6444

380 
qed;

wenzelm@6444

381 

wenzelm@7833

382 
text {*

wenzelm@7833

383 
While explicit rule instantiation may occasionally help to improve

wenzelm@7860

384 
the readability of certain aspects of reasoning, it is usually quite

wenzelm@7833

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

wenzelm@7833

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

wenzelm@7833

387 
instances (by higherorder unification). Thus we may as well prune

wenzelm@7833

388 
the text as follows.

wenzelm@7833

389 
*};

wenzelm@7833

390 

wenzelm@7833

391 
lemma "(EX x. P (f x)) > (EX x. P x)";

wenzelm@6444

392 
proof;

wenzelm@7833

393 
assume "EX x. P (f x)";

wenzelm@7833

394 
thus "EX x. P x";

wenzelm@6444

395 
proof;

wenzelm@6444

396 
fix a;

wenzelm@7833

397 
assume "P (f a)";

wenzelm@7480

398 
show ?thesis; ..;

wenzelm@6444

399 
qed;

wenzelm@6444

400 
qed;

wenzelm@6444

401 

wenzelm@6444

402 

wenzelm@7740

403 
subsubsection {* Deriving rules in Isabelle *};

wenzelm@7001

404 

wenzelm@7833

405 
text {*

wenzelm@7833

406 
We derive the conjunction elimination rule from the projections. The

wenzelm@7860

407 
proof is quite straightforward, since Isabelle/Isar supports

wenzelm@7860

408 
nonatomic goals and assumptions fully transparently.

wenzelm@7833

409 
*};

wenzelm@7001

410 

wenzelm@7001

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

wenzelm@7133

412 
proof ;

wenzelm@7833

413 
assume "A & B";

wenzelm@7001

414 
assume ab_c: "A ==> B ==> C";

wenzelm@7001

415 
show C;

wenzelm@7001

416 
proof (rule ab_c);

wenzelm@7833

417 
show A; by (rule conjunct1);

wenzelm@7833

418 
show B; by (rule conjunct2);

wenzelm@7001

419 
qed;

wenzelm@7001

420 
qed;

wenzelm@7001

421 

wenzelm@7860

422 
text {*

wenzelm@7860

423 
Note that classic Isabelle handles higher rules in a slightly

wenzelm@7860

424 
different way. The tactic script as given in \cite{isabelleintro}

wenzelm@7860

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

wenzelm@7860

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

wenzelm@7860

427 
conclusion. The proper result would then emerge by discharging of

wenzelm@7860

428 
the context at \texttt{qed} time.

wenzelm@7860

429 
*};

wenzelm@7860

430 

wenzelm@6444

431 
end;
