author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 37671  fa53d267dab3 
child 55640  abc140f21caa 
permissions  rwrr 
33026  1 
(* Title: HOL/Isar_Examples/Basic_Logic.thy 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

2 
Author: Markus Wenzel, TU Muenchen 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

3 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

4 
Basic propositional and quantifier reasoning. 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

5 
*) 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

6 

10007  7 
header {* Basic logical reasoning *} 
7748  8 

31758  9 
theory Basic_Logic 
10 
imports Main 

11 
begin 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

12 

7761  13 

10007  14 
subsection {* Pure backward reasoning *} 
7740  15 

37671  16 
text {* In order to get a first idea of how Isabelle/Isar proof 
17 
documents may look like, we consider the propositions @{text I}, 

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

19 
should require little extra explanations. *} 

7001  20 

10007  21 
lemma I: "A > A" 
22 
proof 

23 
assume A 

23393  24 
show A by fact 
10007  25 
qed 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

26 

10007  27 
lemma K: "A > B > A" 
28 
proof 

29 
assume A 

30 
show "B > A" 

31 
proof 

23393  32 
show A by fact 
10007  33 
qed 
34 
qed 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

35 

10007  36 
lemma S: "(A > B > C) > (A > B) > A > C" 
37 
proof 

38 
assume "A > B > C" 

39 
show "(A > B) > A > C" 

40 
proof 

41 
assume "A > B" 

42 
show "A > C" 

43 
proof 

44 
assume A 

45 
show C 

46 
proof (rule mp) 

23393  47 
show "B > C" by (rule mp) fact+ 
48 
show B by (rule mp) fact+ 

10007  49 
qed 
50 
qed 

51 
qed 

52 
qed 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

53 

37671  54 
text {* Isar provides several ways to finetune the reasoning, 
55 
avoiding excessive detail. Several abbreviated language elements 

56 
are available, enabling the writer to express proofs in a more 

57 
concise way, even without referring to any automated proof tools 

58 
yet. 

7761  59 

18193  60 
First of all, proof by assumption may be abbreviated as a single 
37671  61 
dot. *} 
7820  62 

10007  63 
lemma "A > A" 
64 
proof 

65 
assume A 

23393  66 
show A by fact+ 
10007  67 
qed 
7820  68 

37671  69 
text {* In fact, concluding any (sub)proof already involves solving 
70 
any remaining goals by assumption\footnote{This is not a completely 

18193  71 
trivial operation, as proof by assumption may involve full 
72 
higherorder unification.}. Thus we may skip the rather vacuous 

37671  73 
body of the above proof as well. *} 
7820  74 

10007  75 
lemma "A > A" 
76 
proof 

77 
qed 

7820  78 

37671  79 
text {* Note that the \isacommand{proof} command refers to the @{text 
80 
rule} method (without arguments) by default. Thus it implicitly 

81 
applies a single rule, as determined from the syntactic form of the 

82 
statements involved. The \isacommand{by} command abbreviates any 

83 
proof with empty body, so the proof may be further pruned. *} 

7820  84 

10007  85 
lemma "A > A" 
86 
by rule 

7820  87 

37671  88 
text {* Proof by a single rule may be abbreviated as doubledot. *} 
7820  89 

10007  90 
lemma "A > A" .. 
7820  91 

37671  92 
text {* Thus we have arrived at an adequate representation of the 
93 
proof of a tautology that holds by a single standard 

94 
rule.\footnote{Apparently, the rule here is implication 

95 
introduction.} *} 

7820  96 

37671  97 
text {* Let us also reconsider @{text K}. Its statement is composed 
98 
of iterated connectives. Basic decomposition is by a single rule at 

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

18193  100 
proofs. 
7820  101 

18193  102 
The @{text intro} proof method repeatedly decomposes a goal's 
103 
conclusion.\footnote{The dual method is @{text elim}, acting on a 

37671  104 
goal's premises.} *} 
7820  105 

10007  106 
lemma "A > B > A" 
12387  107 
proof (intro impI) 
10007  108 
assume A 
23393  109 
show A by fact 
10007  110 
qed 
7820  111 

37671  112 
text {* Again, the body may be collapsed. *} 
7820  113 

10007  114 
lemma "A > B > A" 
12387  115 
by (intro impI) 
7820  116 

37671  117 
text {* Just like @{text rule}, the @{text intro} and @{text elim} 
118 
proof methods pick standard structural rules, in case no explicit 

18193  119 
arguments are given. While implicit rules are usually just fine for 
120 
single rule application, this may go too far with iteration. Thus 

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

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

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

124 
and universal quantifiers. 

7820  125 

18193  126 
Such welltuned iterated decomposition of certain structures is the 
127 
prime application of @{text intro} and @{text elim}. In contrast, 

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

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

37671  130 
blast}. *} 
7820  131 

132 

10007  133 
subsection {* Variations of backward vs.\ forward reasoning *} 
7820  134 

37671  135 
text {* Certainly, any proof may be performed in backwardstyle only. 
136 
On the other hand, small steps of reasoning are often more naturally 

18193  137 
expressed in forwardstyle. Isar supports both backward and forward 
138 
reasoning as a firstclass concept. In order to demonstrate the 

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

7820  140 

37671  141 
The first version is purely backward. *} 
7001  142 

10007  143 
lemma "A & B > B & A" 
144 
proof 

145 
assume "A & B" 

146 
show "B & A" 

147 
proof 

23393  148 
show B by (rule conjunct2) fact 
149 
show A by (rule conjunct1) fact 

10007  150 
qed 
151 
qed 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

152 

37671  153 
text {* Above, the @{text "conjunct_1/2"} projection rules had to be 
154 
named explicitly, since the goals @{text B} and @{text A} did not 

155 
provide any structural clue. This may be avoided using 

156 
\isacommand{from} to focus on the @{text "A \<and> B"} assumption as the 

157 
current facts, enabling the use of doubledot proofs. Note that 

158 
\isacommand{from} already does forwardchaining, involving the 

159 
@{text conjE} rule here. *} 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

160 

10007  161 
lemma "A & B > B & A" 
162 
proof 

163 
assume "A & B" 

164 
show "B & A" 

165 
proof 

23373  166 
from `A & B` show B .. 
167 
from `A & B` show A .. 

10007  168 
qed 
169 
qed 

7604  170 

37671  171 
text {* In the next version, we move the forward step one level 
172 
upwards. Forwardchaining from the most recent facts is indicated 

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

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

18193  175 
introduction. The resulting proof structure directly corresponds to 
176 
that of the @{text conjE} rule, including the repeated goal 

37671  177 
proposition that is abbreviated as @{text ?thesis} below. *} 
7820  178 

10007  179 
lemma "A & B > B & A" 
180 
proof 

181 
assume "A & B" 

182 
then show "B & A" 

18193  183 
proof  {* rule @{text conjE} of @{text "A \<and> B"} *} 
23373  184 
assume B A 
185 
then show ?thesis ..  {* rule @{text conjI} of @{text "B \<and> A"} *} 

10007  186 
qed 
187 
qed 

7820  188 

37671  189 
text {* In the subsequent version we flatten the structure of the main 
190 
body by doing forward reasoning all the time. Only the outermost 

191 
decomposition step is left as backward. *} 

7820  192 

10007  193 
lemma "A & B > B & A" 
194 
proof 

23373  195 
assume "A & B" 
196 
from `A & B` have A .. 

197 
from `A & B` have B .. 

198 
from `B` `A` show "B & A" .. 

10007  199 
qed 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

200 

37671  201 
text {* We can still push forwardreasoning a bit further, even at the 
202 
risk of getting ridiculous. Note that we force the initial proof 

203 
step to do nothing here, by referring to the ``'' proof method. *} 

7820  204 

10007  205 
lemma "A & B > B & A" 
206 
proof  

207 
{ 

23373  208 
assume "A & B" 
209 
from `A & B` have A .. 

210 
from `A & B` have B .. 

211 
from `B` `A` have "B & A" .. 

10007  212 
} 
37671  213 
then show ?thesis ..  {* rule @{text impI} *} 
10007  214 
qed 
7820  215 

37671  216 
text {* \medskip With these examples we have shifted through a whole 
217 
range from purely backward to purely forward reasoning. Apparently, 

218 
in the extreme ends we get slightly illstructured proofs, which 

219 
also require much explicit naming of either rules (backward) or 

220 
local facts (forward). 

7820  221 

18193  222 
The general lesson learned here is that good proof style would 
223 
achieve just the \emph{right} balance of topdown backward 

224 
decomposition, and bottomup forward composition. In general, there 

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

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

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

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

37671  229 
proof writer to develop good taste, and some practice, of course. *} 
7820  230 

37671  231 
text {* For our example the most appropriate way of reasoning is 
232 
probably the middle one, with conjunction introduction done after 

233 
elimination. *} 

7820  234 

10007  235 
lemma "A & B > B & A" 
236 
proof 

237 
assume "A & B" 

23373  238 
then show "B & A" 
10007  239 
proof 
23373  240 
assume B A 
241 
then show ?thesis .. 

10007  242 
qed 
243 
qed 

7820  244 

245 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

246 

10007  247 
subsection {* A few examples from ``Introduction to Isabelle'' *} 
7001  248 

37671  249 
text {* We rephrase some of the basic reasoning examples of 
250 
\cite{isabelleintro}, using HOL rather than FOL. *} 

251 

7820  252 

10007  253 
subsubsection {* A propositional proof *} 
7833  254 

37671  255 
text {* We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof 
256 
below involves forwardchaining from @{text "P \<or> P"}, followed by an 

257 
explicit caseanalysis on the two \emph{identical} cases. *} 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

258 

10007  259 
lemma "P  P > P" 
260 
proof 

261 
assume "P  P" 

23373  262 
then show P 
7833  263 
proof  {* 
18193  264 
rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$} 
10007  265 
*} 
23393  266 
assume P show P by fact 
10007  267 
next 
23393  268 
assume P show P by fact 
10007  269 
qed 
270 
qed 

7833  271 

37671  272 
text {* Case splits are \emph{not} hardwired into the Isar language as 
273 
a special feature. The \isacommand{next} command used to separate 

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

7833  275 

18193  276 
\medskip In general, applying proof methods may split up a goal into 
277 
separate ``cases'', i.e.\ new subgoals with individual local 

278 
assumptions. The corresponding proof text typically mimics this by 

279 
establishing results in appropriate contexts, separated by blocks. 

7833  280 

18193  281 
In order to avoid too much explicit parentheses, the Isar system 
282 
implicitly opens an additional block for any new goal, the 

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

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

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

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

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

288 
case. 

7833  289 

18193  290 
\medskip In our example the situation is even simpler, since the two 
291 
cases actually coincide. Consequently the proof may be rephrased as 

37671  292 
follows. *} 
7833  293 

10007  294 
lemma "P  P > P" 
295 
proof 

296 
assume "P  P" 

23373  297 
then show P 
10007  298 
proof 
299 
assume P 

23393  300 
show P by fact 
301 
show P by fact 

10007  302 
qed 
303 
qed 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

304 

37671  305 
text {* Again, the rather vacuous body of the proof may be collapsed. 
306 
Thus the case analysis degenerates into two assumption steps, which 

307 
are implicitly performed when concluding the single rule step of the 

308 
doubledot proof as follows. *} 

7833  309 

10007  310 
lemma "P  P > P" 
311 
proof 

312 
assume "P  P" 

23373  313 
then show P .. 
10007  314 
qed 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

315 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

316 

10007  317 
subsubsection {* A quantifier proof *} 
7833  318 

37671  319 
text {* To illustrate quantifier reasoning, let us prove @{text 
320 
"(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any 

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

322 
second existential statement. 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

323 

18193  324 
The first proof is rather verbose, exhibiting quite a lot of 
325 
(redundant) detail. It gives explicit rules, even with some 

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

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

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

37671  329 
binds term abbreviations by higherorder pattern matching. *} 
7833  330 

10636  331 
lemma "(EX x. P (f x)) > (EX y. P y)" 
10007  332 
proof 
333 
assume "EX x. P (f x)" 

23373  334 
then show "EX y. P y" 
7833  335 
proof (rule exE)  {* 
37671  336 
rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$} 
10007  337 
*} 
338 
fix a 

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

23373  340 
then show ?thesis by (rule exI [of P ?witness]) 
10007  341 
qed 
342 
qed 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

343 

37671  344 
text {* While explicit rule instantiation may occasionally improve 
18193  345 
readability of certain aspects of reasoning, it is usually quite 
346 
redundant. Above, the basic proof outline gives already enough 

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

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

37671  349 
the text as follows. *} 
7833  350 

10636  351 
lemma "(EX x. P (f x)) > (EX y. P y)" 
10007  352 
proof 
353 
assume "EX x. P (f x)" 

23373  354 
then show "EX y. P y" 
10007  355 
proof 
356 
fix a 

357 
assume "P (f a)" 

23373  358 
then show ?thesis .. 
10007  359 
qed 
360 
qed 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

361 

37671  362 
text {* Explicit @{text \<exists>}elimination as seen above can become quite 
18193  363 
cumbersome in practice. The derived Isar language element 
364 
``\isakeyword{obtain}'' provides a more handsome way to do 

37671  365 
generalized existence reasoning. *} 
9477  366 

10636  367 
lemma "(EX x. P (f x)) > (EX y. P y)" 
10007  368 
proof 
369 
assume "EX x. P (f x)" 

10636  370 
then obtain a where "P (f a)" .. 
23373  371 
then show "EX y. P y" .. 
10007  372 
qed 
9477  373 

37671  374 
text {* Technically, \isakeyword{obtain} is similar to 
375 
\isakeyword{fix} and \isakeyword{assume} together with a soundness 

376 
proof of the elimination involved. Thus it behaves similar to any 

377 
other forward proof element. Also note that due to the nature of 

378 
general existence reasoning involved here, any result exported from 

379 
the context of an \isakeyword{obtain} statement may \emph{not} refer 

380 
to the parameters introduced there. *} 

9477  381 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

382 

10007  383 
subsubsection {* Deriving rules in Isabelle *} 
7001  384 

37671  385 
text {* We derive the conjunction elimination rule from the 
386 
corresponding projections. The proof is quite straightforward, 

387 
since Isabelle/Isar supports nonatomic goals and assumptions fully 

388 
transparently. *} 

7001  389 

10007  390 
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C" 
391 
proof  

392 
assume "A & B" 

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

394 
show C 

395 
proof (rule r) 

23393  396 
show A by (rule conjunct1) fact 
397 
show B by (rule conjunct2) fact 

10007  398 
qed 
399 
qed 

7001  400 

10007  401 
end 