|
1 |
|
2 header {* Example: First-Order Logic *} |
|
3 |
|
4 theory %visible First_Order_Logic |
|
5 imports Base (* FIXME Pure!? *) |
|
6 begin |
|
7 |
|
8 text {* |
|
9 \noindent In order to commence a new object-logic within |
|
10 Isabelle/Pure we introduce abstract syntactic categories @{text "i"} |
|
11 for individuals and @{text "o"} for object-propositions. The latter |
|
12 is embedded into the language of Pure propositions by means of a |
|
13 separate judgment. |
|
14 *} |
|
15 |
|
16 typedecl i |
|
17 typedecl o |
|
18 |
|
19 judgment |
|
20 Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
|
21 |
|
22 text {* |
|
23 \noindent Note that the object-logic judgement is implicit in the |
|
24 syntax: writing @{prop A} produces @{term "Trueprop A"} internally. |
|
25 From the Pure perspective this means ``@{prop A} is derivable in the |
|
26 object-logic''. |
|
27 *} |
|
28 |
|
29 |
|
30 subsection {* Equational reasoning \label{sec:framework-ex-equal} *} |
|
31 |
|
32 text {* |
|
33 Equality is axiomatized as a binary predicate on individuals, with |
|
34 reflexivity as introduction, and substitution as elimination |
|
35 principle. Note that the latter is particularly convenient in a |
|
36 framework like Isabelle, because syntactic congruences are |
|
37 implicitly produced by unification of @{term "B x"} against |
|
38 expressions containing occurrences of @{term x}. |
|
39 *} |
|
40 |
|
41 axiomatization |
|
42 equal :: "i \<Rightarrow> i \<Rightarrow> o" (infix "=" 50) |
|
43 where |
|
44 refl [intro]: "x = x" and |
|
45 subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y" |
|
46 |
|
47 text {* |
|
48 \noindent Substitution is very powerful, but also hard to control in |
|
49 full generality. We derive some common symmetry~/ transitivity |
|
50 schemes of @{term equal} as particular consequences. |
|
51 *} |
|
52 |
|
53 theorem sym [sym]: |
|
54 assumes "x = y" |
|
55 shows "y = x" |
|
56 proof - |
|
57 have "x = x" .. |
|
58 with `x = y` show "y = x" .. |
|
59 qed |
|
60 |
|
61 theorem forw_subst [trans]: |
|
62 assumes "y = x" and "B x" |
|
63 shows "B y" |
|
64 proof - |
|
65 from `y = x` have "x = y" .. |
|
66 from this and `B x` show "B y" .. |
|
67 qed |
|
68 |
|
69 theorem back_subst [trans]: |
|
70 assumes "B x" and "x = y" |
|
71 shows "B y" |
|
72 proof - |
|
73 from `x = y` and `B x` |
|
74 show "B y" .. |
|
75 qed |
|
76 |
|
77 theorem trans [trans]: |
|
78 assumes "x = y" and "y = z" |
|
79 shows "x = z" |
|
80 proof - |
|
81 from `y = z` and `x = y` |
|
82 show "x = z" .. |
|
83 qed |
|
84 |
|
85 |
|
86 subsection {* Basic group theory *} |
|
87 |
|
88 text {* |
|
89 As an example for equational reasoning we consider some bits of |
|
90 group theory. The subsequent locale definition postulates group |
|
91 operations and axioms; we also derive some consequences of this |
|
92 specification. |
|
93 *} |
|
94 |
|
95 locale group = |
|
96 fixes prod :: "i \<Rightarrow> i \<Rightarrow> i" (infix "\<circ>" 70) |
|
97 and inv :: "i \<Rightarrow> i" ("(_\<inverse>)" [1000] 999) |
|
98 and unit :: i ("1") |
|
99 assumes assoc: "(x \<circ> y) \<circ> z = x \<circ> (y \<circ> z)" |
|
100 and left_unit: "1 \<circ> x = x" |
|
101 and left_inv: "x\<inverse> \<circ> x = 1" |
|
102 begin |
|
103 |
|
104 theorem right_inv: "x \<circ> x\<inverse> = 1" |
|
105 proof - |
|
106 have "x \<circ> x\<inverse> = 1 \<circ> (x \<circ> x\<inverse>)" by (rule left_unit [symmetric]) |
|
107 also have "\<dots> = (1 \<circ> x) \<circ> x\<inverse>" by (rule assoc [symmetric]) |
|
108 also have "1 = (x\<inverse>)\<inverse> \<circ> x\<inverse>" by (rule left_inv [symmetric]) |
|
109 also have "\<dots> \<circ> x = (x\<inverse>)\<inverse> \<circ> (x\<inverse> \<circ> x)" by (rule assoc) |
|
110 also have "x\<inverse> \<circ> x = 1" by (rule left_inv) |
|
111 also have "((x\<inverse>)\<inverse> \<circ> \<dots>) \<circ> x\<inverse> = (x\<inverse>)\<inverse> \<circ> (1 \<circ> x\<inverse>)" by (rule assoc) |
|
112 also have "1 \<circ> x\<inverse> = x\<inverse>" by (rule left_unit) |
|
113 also have "(x\<inverse>)\<inverse> \<circ> \<dots> = 1" by (rule left_inv) |
|
114 finally show "x \<circ> x\<inverse> = 1" . |
|
115 qed |
|
116 |
|
117 theorem right_unit: "x \<circ> 1 = x" |
|
118 proof - |
|
119 have "1 = x\<inverse> \<circ> x" by (rule left_inv [symmetric]) |
|
120 also have "x \<circ> \<dots> = (x \<circ> x\<inverse>) \<circ> x" by (rule assoc [symmetric]) |
|
121 also have "x \<circ> x\<inverse> = 1" by (rule right_inv) |
|
122 also have "\<dots> \<circ> x = x" by (rule left_unit) |
|
123 finally show "x \<circ> 1 = x" . |
|
124 qed |
|
125 |
|
126 text {* |
|
127 \noindent Reasoning from basic axioms is often tedious. Our proofs |
|
128 work by producing various instances of the given rules (potentially |
|
129 the symmetric form) using the pattern ``@{command have}~@{text |
|
130 eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of |
|
131 results via @{command also}/@{command finally}. These steps may |
|
132 involve any of the transitivity rules declared in |
|
133 \secref{sec:framework-ex-equal}, namely @{thm trans} in combining |
|
134 the first two results in @{thm right_inv} and in the final steps of |
|
135 both proofs, @{thm forw_subst} in the first combination of @{thm |
|
136 right_unit}, and @{thm back_subst} in all other calculational steps. |
|
137 |
|
138 Occasional substitutions in calculations are adequate, but should |
|
139 not be over-emphasized. The other extreme is to compose a chain by |
|
140 plain transitivity only, with replacements occurring always in |
|
141 topmost position. For example: |
|
142 *} |
|
143 |
|
144 (*<*) |
|
145 theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
|
146 proof - |
|
147 assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)" |
|
148 (*>*) |
|
149 have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv .. |
|
150 also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc .. |
|
151 also have "\<dots> = 1 \<circ> x" unfolding right_inv .. |
|
152 also have "\<dots> = x" unfolding left_unit .. |
|
153 finally have "x \<circ> 1 = x" . |
|
154 (*<*) |
|
155 qed |
|
156 (*>*) |
|
157 |
|
158 text {* |
|
159 \noindent Here we have re-used the built-in mechanism for unfolding |
|
160 definitions in order to normalize each equational problem. A more |
|
161 realistic object-logic would include proper setup for the Simplifier |
|
162 (\secref{sec:simplifier}), the main automated tool for equational |
|
163 reasoning in Isabelle. Then ``@{command unfolding}~@{thm |
|
164 left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text |
|
165 "(simp only: left_inv)"}'' etc. |
|
166 *} |
|
167 |
|
168 end |
|
169 |
|
170 |
|
171 subsection {* Propositional logic \label{sec:framework-ex-prop} *} |
|
172 |
|
173 text {* |
|
174 We axiomatize basic connectives of propositional logic: implication, |
|
175 disjunction, and conjunction. The associated rules are modeled |
|
176 after Gentzen's system of Natural Deduction \cite{Gentzen:1935}. |
|
177 *} |
|
178 |
|
179 axiomatization |
|
180 imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) where |
|
181 impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and |
|
182 impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B" |
|
183 |
|
184 axiomatization |
|
185 disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where |
|
186 disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B" and |
|
187 disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B" and |
|
188 disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" |
|
189 |
|
190 axiomatization |
|
191 conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) where |
|
192 conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and |
|
193 conjD\<^sub>1: "A \<and> B \<Longrightarrow> A" and |
|
194 conjD\<^sub>2: "A \<and> B \<Longrightarrow> B" |
|
195 |
|
196 text {* |
|
197 \noindent The conjunctive destructions have the disadvantage that |
|
198 decomposing @{prop "A \<and> B"} involves an immediate decision which |
|
199 component should be projected. The more convenient simultaneous |
|
200 elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as |
|
201 follows: |
|
202 *} |
|
203 |
|
204 theorem conjE [elim]: |
|
205 assumes "A \<and> B" |
|
206 obtains A and B |
|
207 proof |
|
208 from `A \<and> B` show A by (rule conjD\<^sub>1) |
|
209 from `A \<and> B` show B by (rule conjD\<^sub>2) |
|
210 qed |
|
211 |
|
212 text {* |
|
213 \noindent Here is an example of swapping conjuncts with a single |
|
214 intermediate elimination step: |
|
215 *} |
|
216 |
|
217 (*<*) |
|
218 lemma "\<And>A. PROP A \<Longrightarrow> PROP A" |
|
219 proof - |
|
220 (*>*) |
|
221 assume "A \<and> B" |
|
222 then obtain B and A .. |
|
223 then have "B \<and> A" .. |
|
224 (*<*) |
|
225 qed |
|
226 (*>*) |
|
227 |
|
228 text {* |
|
229 \noindent Note that the analogous elimination rule for disjunction |
|
230 ``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with |
|
231 the original axiomatization of @{thm disjE}. |
|
232 |
|
233 \medskip We continue propositional logic by introducing absurdity |
|
234 with its characteristic elimination. Plain truth may then be |
|
235 defined as a proposition that is trivially true. |
|
236 *} |
|
237 |
|
238 axiomatization |
|
239 false :: o ("\<bottom>") where |
|
240 falseE [elim]: "\<bottom> \<Longrightarrow> A" |
|
241 |
|
242 definition |
|
243 true :: o ("\<top>") where |
|
244 "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
|
245 |
|
246 theorem trueI [intro]: \<top> |
|
247 unfolding true_def .. |
|
248 |
|
249 text {* |
|
250 \medskip\noindent Now negation represents an implication towards |
|
251 absurdity: |
|
252 *} |
|
253 |
|
254 definition |
|
255 not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where |
|
256 "\<not> A \<equiv> A \<longrightarrow> \<bottom>" |
|
257 |
|
258 theorem notI [intro]: |
|
259 assumes "A \<Longrightarrow> \<bottom>" |
|
260 shows "\<not> A" |
|
261 unfolding not_def |
|
262 proof |
|
263 assume A |
|
264 then show \<bottom> by (rule `A \<Longrightarrow> \<bottom>`) |
|
265 qed |
|
266 |
|
267 theorem notE [elim]: |
|
268 assumes "\<not> A" and A |
|
269 shows B |
|
270 proof - |
|
271 from `\<not> A` have "A \<longrightarrow> \<bottom>" unfolding not_def . |
|
272 from `A \<longrightarrow> \<bottom>` and `A` have \<bottom> .. |
|
273 then show B .. |
|
274 qed |
|
275 |
|
276 |
|
277 subsection {* Classical logic *} |
|
278 |
|
279 text {* |
|
280 Subsequently we state the principle of classical contradiction as a |
|
281 local assumption. Thus we refrain from forcing the object-logic |
|
282 into the classical perspective. Within that context, we may derive |
|
283 well-known consequences of the classical principle. |
|
284 *} |
|
285 |
|
286 locale classical = |
|
287 assumes classical: "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C" |
|
288 begin |
|
289 |
|
290 theorem double_negation: |
|
291 assumes "\<not> \<not> C" |
|
292 shows C |
|
293 proof (rule classical) |
|
294 assume "\<not> C" |
|
295 with `\<not> \<not> C` show C .. |
|
296 qed |
|
297 |
|
298 theorem tertium_non_datur: "C \<or> \<not> C" |
|
299 proof (rule double_negation) |
|
300 show "\<not> \<not> (C \<or> \<not> C)" |
|
301 proof |
|
302 assume "\<not> (C \<or> \<not> C)" |
|
303 have "\<not> C" |
|
304 proof |
|
305 assume C then have "C \<or> \<not> C" .. |
|
306 with `\<not> (C \<or> \<not> C)` show \<bottom> .. |
|
307 qed |
|
308 then have "C \<or> \<not> C" .. |
|
309 with `\<not> (C \<or> \<not> C)` show \<bottom> .. |
|
310 qed |
|
311 qed |
|
312 |
|
313 text {* |
|
314 \noindent These examples illustrate both classical reasoning and |
|
315 non-trivial propositional proofs in general. All three rules |
|
316 characterize classical logic independently, but the original rule is |
|
317 already the most convenient to use, because it leaves the conclusion |
|
318 unchanged. Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our |
|
319 format for eliminations, despite the additional twist that the |
|
320 context refers to the main conclusion. So we may write @{thm |
|
321 classical} as the Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''. |
|
322 This also explains nicely how classical reasoning really works: |
|
323 whatever the main @{text thesis} might be, we may always assume its |
|
324 negation! |
|
325 *} |
|
326 |
|
327 end |
|
328 |
|
329 |
|
330 subsection {* Quantifiers \label{sec:framework-ex-quant} *} |
|
331 |
|
332 text {* |
|
333 Representing quantifiers is easy, thanks to the higher-order nature |
|
334 of the underlying framework. According to the well-known technique |
|
335 introduced by Church \cite{church40}, quantifiers are operators on |
|
336 predicates, which are syntactically represented as @{text "\<lambda>"}-terms |
|
337 of type @{typ "i \<Rightarrow> o"}. Binder notation turns @{text "All (\<lambda>x. B |
|
338 x)"} into @{text "\<forall>x. B x"} etc. |
|
339 *} |
|
340 |
|
341 axiomatization |
|
342 All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) where |
|
343 allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x" and |
|
344 allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a" |
|
345 |
|
346 axiomatization |
|
347 Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where |
|
348 exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)" and |
|
349 exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C" |
|
350 |
|
351 text {* |
|
352 \noindent The statement of @{thm exE} corresponds to ``@{text |
|
353 "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}'' in Isar. In the |
|
354 subsequent example we illustrate quantifier reasoning involving all |
|
355 four rules: |
|
356 *} |
|
357 |
|
358 theorem |
|
359 assumes "\<exists>x. \<forall>y. R x y" |
|
360 shows "\<forall>y. \<exists>x. R x y" |
|
361 proof -- {* @{text "\<forall>"} introduction *} |
|
362 obtain x where "\<forall>y. R x y" using `\<exists>x. \<forall>y. R x y` .. -- {* @{text "\<exists>"} elimination *} |
|
363 fix y have "R x y" using `\<forall>y. R x y` .. -- {* @{text "\<forall>"} destruction *} |
|
364 then show "\<exists>x. R x y" .. -- {* @{text "\<exists>"} introduction *} |
|
365 qed |
|
366 |
|
367 |
|
368 subsection {* Canonical reasoning patterns *} |
|
369 |
|
370 text {* |
|
371 The main rules of first-order predicate logic from |
|
372 \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant} |
|
373 can now be summarized as follows, using the native Isar statement |
|
374 format of \secref{sec:framework-stmt}. |
|
375 |
|
376 \medskip |
|
377 \begin{tabular}{l} |
|
378 @{text "impI: \<ASSUMES> A \<Longrightarrow> B \<SHOWS> A \<longrightarrow> B"} \\ |
|
379 @{text "impD: \<ASSUMES> A \<longrightarrow> B \<AND> A \<SHOWS> B"} \\[1ex] |
|
380 |
|
381 @{text "disjI\<^sub>1: \<ASSUMES> A \<SHOWS> A \<or> B"} \\ |
|
382 @{text "disjI\<^sub>2: \<ASSUMES> B \<SHOWS> A \<or> B"} \\ |
|
383 @{text "disjE: \<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"} \\[1ex] |
|
384 |
|
385 @{text "conjI: \<ASSUMES> A \<AND> B \<SHOWS> A \<and> B"} \\ |
|
386 @{text "conjE: \<ASSUMES> A \<and> B \<OBTAINS> A \<AND> B"} \\[1ex] |
|
387 |
|
388 @{text "falseE: \<ASSUMES> \<bottom> \<SHOWS> A"} \\ |
|
389 @{text "trueI: \<SHOWS> \<top>"} \\[1ex] |
|
390 |
|
391 @{text "notI: \<ASSUMES> A \<Longrightarrow> \<bottom> \<SHOWS> \<not> A"} \\ |
|
392 @{text "notE: \<ASSUMES> \<not> A \<AND> A \<SHOWS> B"} \\[1ex] |
|
393 |
|
394 @{text "allI: \<ASSUMES> \<And>x. B x \<SHOWS> \<forall>x. B x"} \\ |
|
395 @{text "allE: \<ASSUMES> \<forall>x. B x \<SHOWS> B a"} \\[1ex] |
|
396 |
|
397 @{text "exI: \<ASSUMES> B a \<SHOWS> \<exists>x. B x"} \\ |
|
398 @{text "exE: \<ASSUMES> \<exists>x. B x \<OBTAINS> a \<WHERE> B a"} |
|
399 \end{tabular} |
|
400 \medskip |
|
401 |
|
402 \noindent This essentially provides a declarative reading of Pure |
|
403 rules as Isar reasoning patterns: the rule statements tells how a |
|
404 canonical proof outline shall look like. Since the above rules have |
|
405 already been declared as @{attribute (Pure) intro}, @{attribute |
|
406 (Pure) elim}, @{attribute (Pure) dest} --- each according to its |
|
407 particular shape --- we can immediately write Isar proof texts as |
|
408 follows: |
|
409 *} |
|
410 |
|
411 (*<*) |
|
412 theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
|
413 proof - |
|
414 (*>*) |
|
415 |
|
416 txt_raw {*\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
417 |
|
418 have "A \<longrightarrow> B" |
|
419 proof |
|
420 assume A |
|
421 show B sorry %noproof |
|
422 qed |
|
423 |
|
424 txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
425 |
|
426 have "A \<longrightarrow> B" and A sorry %noproof |
|
427 then have B .. |
|
428 |
|
429 txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
430 |
|
431 have A sorry %noproof |
|
432 then have "A \<or> B" .. |
|
433 |
|
434 have B sorry %noproof |
|
435 then have "A \<or> B" .. |
|
436 |
|
437 txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
438 |
|
439 have "A \<or> B" sorry %noproof |
|
440 then have C |
|
441 proof |
|
442 assume A |
|
443 then show C sorry %noproof |
|
444 next |
|
445 assume B |
|
446 then show C sorry %noproof |
|
447 qed |
|
448 |
|
449 txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
450 |
|
451 have A and B sorry %noproof |
|
452 then have "A \<and> B" .. |
|
453 |
|
454 txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
455 |
|
456 have "A \<and> B" sorry %noproof |
|
457 then obtain A and B .. |
|
458 |
|
459 txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
460 |
|
461 have "\<bottom>" sorry %noproof |
|
462 then have A .. |
|
463 |
|
464 txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
465 |
|
466 have "\<top>" .. |
|
467 |
|
468 txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
469 |
|
470 have "\<not> A" |
|
471 proof |
|
472 assume A |
|
473 then show "\<bottom>" sorry %noproof |
|
474 qed |
|
475 |
|
476 txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
477 |
|
478 have "\<not> A" and A sorry %noproof |
|
479 then have B .. |
|
480 |
|
481 txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
482 |
|
483 have "\<forall>x. B x" |
|
484 proof |
|
485 fix x |
|
486 show "B x" sorry %noproof |
|
487 qed |
|
488 |
|
489 txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
490 |
|
491 have "\<forall>x. B x" sorry %noproof |
|
492 then have "B a" .. |
|
493 |
|
494 txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
495 |
|
496 have "\<exists>x. B x" |
|
497 proof |
|
498 show "B a" sorry %noproof |
|
499 qed |
|
500 |
|
501 txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*) |
|
502 |
|
503 have "\<exists>x. B x" sorry %noproof |
|
504 then obtain a where "B a" .. |
|
505 |
|
506 txt_raw {*\end{minipage}*} |
|
507 |
|
508 (*<*) |
|
509 qed |
|
510 (*>*) |
|
511 |
|
512 text {* |
|
513 \bigskip\noindent Of course, these proofs are merely examples. As |
|
514 sketched in \secref{sec:framework-subproof}, there is a fair amount |
|
515 of flexibility in expressing Pure deductions in Isar. Here the user |
|
516 is asked to express himself adequately, aiming at proof texts of |
|
517 literary quality. |
|
518 *} |
|
519 |
|
520 end %visible |