author | wenzelm |
Mon, 02 Nov 2015 13:58:19 +0100 | |
changeset 61541 | 846c72206207 |
parent 58882 | 6e2010ab8bd9 |
child 61542 | b3eb789616c3 |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Basic_Logic.thy |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
Basic propositional and quantifier reasoning. |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
5 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
|
58882 | 7 |
section \<open>Basic logical reasoning\<close> |
7748 | 8 |
|
31758 | 9 |
theory Basic_Logic |
10 |
imports Main |
|
11 |
begin |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
12 |
|
7761 | 13 |
|
58614 | 14 |
subsection \<open>Pure backward reasoning\<close> |
7740 | 15 |
|
61541 | 16 |
text \<open>In order to get a first idea of how Isabelle/Isar proof documents may |
17 |
look like, we consider the propositions \<open>I\<close>, \<open>K\<close>, and \<open>S\<close>. The following |
|
18 |
(rather explicit) proofs should require little extra explanations.\<close> |
|
7001 | 19 |
|
55640 | 20 |
lemma I: "A \<longrightarrow> A" |
10007 | 21 |
proof |
22 |
assume A |
|
23393 | 23 |
show A by fact |
10007 | 24 |
qed |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
25 |
|
55640 | 26 |
lemma K: "A \<longrightarrow> B \<longrightarrow> A" |
10007 | 27 |
proof |
28 |
assume A |
|
55640 | 29 |
show "B \<longrightarrow> A" |
10007 | 30 |
proof |
23393 | 31 |
show A by fact |
10007 | 32 |
qed |
33 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
34 |
|
55640 | 35 |
lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C" |
10007 | 36 |
proof |
55640 | 37 |
assume "A \<longrightarrow> B \<longrightarrow> C" |
38 |
show "(A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C" |
|
10007 | 39 |
proof |
55640 | 40 |
assume "A \<longrightarrow> B" |
41 |
show "A \<longrightarrow> C" |
|
10007 | 42 |
proof |
43 |
assume A |
|
44 |
show C |
|
45 |
proof (rule mp) |
|
55640 | 46 |
show "B \<longrightarrow> C" by (rule mp) fact+ |
23393 | 47 |
show B by (rule mp) fact+ |
10007 | 48 |
qed |
49 |
qed |
|
50 |
qed |
|
51 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
52 |
|
61541 | 53 |
text \<open>Isar provides several ways to fine-tune the reasoning, avoiding |
54 |
excessive detail. Several abbreviated language elements are available, |
|
55 |
enabling the writer to express proofs in a more concise way, even without |
|
56 |
referring to any automated proof tools yet. |
|
7761 | 57 |
|
61541 | 58 |
First of all, proof by assumption may be abbreviated as a single dot.\<close> |
7820 | 59 |
|
55640 | 60 |
lemma "A \<longrightarrow> A" |
10007 | 61 |
proof |
62 |
assume A |
|
23393 | 63 |
show A by fact+ |
10007 | 64 |
qed |
7820 | 65 |
|
61541 | 66 |
text \<open>In fact, concluding any (sub-)proof already involves solving any |
67 |
remaining goals by assumption\footnote{This is not a completely trivial |
|
68 |
operation, as proof by assumption may involve full higher-order |
|
69 |
unification.}. Thus we may skip the rather vacuous body of the above proof |
|
70 |
as well.\<close> |
|
7820 | 71 |
|
55640 | 72 |
lemma "A \<longrightarrow> A" |
10007 | 73 |
proof |
74 |
qed |
|
7820 | 75 |
|
61541 | 76 |
text \<open>Note that the \isacommand{proof} command refers to the \<open>rule\<close> method |
77 |
(without arguments) by default. Thus it implicitly applies a single rule, |
|
78 |
as determined from the syntactic form of the statements involved. The |
|
79 |
\isacommand{by} command abbreviates any proof with empty body, so the |
|
80 |
proof may be further pruned.\<close> |
|
7820 | 81 |
|
55640 | 82 |
lemma "A \<longrightarrow> A" |
10007 | 83 |
by rule |
7820 | 84 |
|
58614 | 85 |
text \<open>Proof by a single rule may be abbreviated as double-dot.\<close> |
7820 | 86 |
|
55640 | 87 |
lemma "A \<longrightarrow> A" .. |
7820 | 88 |
|
61541 | 89 |
text \<open>Thus we have arrived at an adequate representation of the proof of a |
90 |
tautology that holds by a single standard rule.\footnote{Apparently, the |
|
91 |
rule here is implication introduction.} |
|
7820 | 92 |
|
61541 | 93 |
\<^medskip> |
94 |
Let us also reconsider \<open>K\<close>. Its statement is composed of iterated |
|
95 |
connectives. Basic decomposition is by a single rule at a time, which is |
|
96 |
why our first version above was by nesting two proofs. |
|
7820 | 97 |
|
61541 | 98 |
The \<open>intro\<close> proof method repeatedly decomposes a goal's |
99 |
conclusion.\footnote{The dual method is \<open>elim\<close>, acting on a goal's |
|
100 |
premises.}\<close> |
|
7820 | 101 |
|
55640 | 102 |
lemma "A \<longrightarrow> B \<longrightarrow> A" |
12387 | 103 |
proof (intro impI) |
10007 | 104 |
assume A |
23393 | 105 |
show A by fact |
10007 | 106 |
qed |
7820 | 107 |
|
58614 | 108 |
text \<open>Again, the body may be collapsed.\<close> |
7820 | 109 |
|
55640 | 110 |
lemma "A \<longrightarrow> B \<longrightarrow> A" |
12387 | 111 |
by (intro impI) |
7820 | 112 |
|
61541 | 113 |
text \<open>Just like \<open>rule\<close>, the \<open>intro\<close> and \<open>elim\<close> proof methods pick standard |
114 |
structural rules, in case no explicit arguments are given. While implicit |
|
115 |
rules are usually just fine for single rule application, this may go too |
|
116 |
far with iteration. Thus in practice, \<open>intro\<close> and \<open>elim\<close> would be |
|
117 |
typically restricted to certain structures by giving a few rules only, |
|
118 |
e.g.\ \isacommand{proof}~\<open>(intro impI allI)\<close> to strip implications and |
|
119 |
universal quantifiers. |
|
7820 | 120 |
|
61541 | 121 |
Such well-tuned iterated decomposition of certain structures is the prime |
122 |
application of \<open>intro\<close> and \<open>elim\<close>. In contrast, terminal steps that solve |
|
123 |
a goal completely are usually performed by actual automated proof methods |
|
124 |
(such as \isacommand{by}~\<open>blast\<close>.\<close> |
|
7820 | 125 |
|
126 |
||
58614 | 127 |
subsection \<open>Variations of backward vs.\ forward reasoning\<close> |
7820 | 128 |
|
61541 | 129 |
text \<open>Certainly, any proof may be performed in backward-style only. On the |
130 |
other hand, small steps of reasoning are often more naturally expressed in |
|
131 |
forward-style. Isar supports both backward and forward reasoning as a |
|
132 |
first-class concept. In order to demonstrate the difference, we consider |
|
133 |
several proofs of \<open>A \<and> B \<longrightarrow> B \<and> A\<close>. |
|
7820 | 134 |
|
58614 | 135 |
The first version is purely backward.\<close> |
7001 | 136 |
|
55640 | 137 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
10007 | 138 |
proof |
55640 | 139 |
assume "A \<and> B" |
140 |
show "B \<and> A" |
|
10007 | 141 |
proof |
23393 | 142 |
show B by (rule conjunct2) fact |
143 |
show A by (rule conjunct1) fact |
|
10007 | 144 |
qed |
145 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
146 |
|
61541 | 147 |
text \<open>Above, the projection rules \<open>conjunct1\<close> / \<open>conjunct2\<close> had to be named |
148 |
explicitly, since the goals \<open>B\<close> and \<open>A\<close> did not provide any structural |
|
149 |
clue. This may be avoided using \isacommand{from} to focus on the \<open>A \<and> B\<close> |
|
150 |
assumption as the current facts, enabling the use of double-dot proofs. |
|
151 |
Note that \isacommand{from} already does forward-chaining, involving the |
|
152 |
\<open>conjE\<close> rule here.\<close> |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
153 |
|
55640 | 154 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
10007 | 155 |
proof |
55640 | 156 |
assume "A \<and> B" |
157 |
show "B \<and> A" |
|
10007 | 158 |
proof |
58614 | 159 |
from \<open>A \<and> B\<close> show B .. |
160 |
from \<open>A \<and> B\<close> show A .. |
|
10007 | 161 |
qed |
162 |
qed |
|
7604 | 163 |
|
61541 | 164 |
text \<open>In the next version, we move the forward step one level upwards. |
165 |
Forward-chaining from the most recent facts is indicated by the |
|
166 |
\isacommand{then} command. Thus the proof of \<open>B \<and> A\<close> from \<open>A \<and> B\<close> actually |
|
167 |
becomes an elimination, rather than an introduction. The resulting proof |
|
168 |
structure directly corresponds to that of the \<open>conjE\<close> rule, including the |
|
169 |
repeated goal proposition that is abbreviated as \<open>?thesis\<close> below.\<close> |
|
7820 | 170 |
|
55640 | 171 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
10007 | 172 |
proof |
55640 | 173 |
assume "A \<and> B" |
174 |
then show "B \<and> A" |
|
61541 | 175 |
proof -- \<open>rule \<open>conjE\<close> of \<open>A \<and> B\<close>\<close> |
23373 | 176 |
assume B A |
61541 | 177 |
then show ?thesis .. -- \<open>rule \<open>conjI\<close> of \<open>B \<and> A\<close>\<close> |
10007 | 178 |
qed |
179 |
qed |
|
7820 | 180 |
|
61541 | 181 |
text \<open>In the subsequent version we flatten the structure of the main body by |
182 |
doing forward reasoning all the time. Only the outermost decomposition |
|
183 |
step is left as backward.\<close> |
|
7820 | 184 |
|
55640 | 185 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
10007 | 186 |
proof |
55640 | 187 |
assume "A \<and> B" |
58614 | 188 |
from \<open>A \<and> B\<close> have A .. |
189 |
from \<open>A \<and> B\<close> have B .. |
|
190 |
from \<open>B\<close> \<open>A\<close> show "B \<and> A" .. |
|
10007 | 191 |
qed |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
192 |
|
61541 | 193 |
text \<open>We can still push forward-reasoning a bit further, even at the risk of |
194 |
getting ridiculous. Note that we force the initial proof step to do |
|
195 |
nothing here, by referring to the \<open>-\<close> proof method.\<close> |
|
7820 | 196 |
|
55640 | 197 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
10007 | 198 |
proof - |
199 |
{ |
|
55640 | 200 |
assume "A \<and> B" |
58614 | 201 |
from \<open>A \<and> B\<close> have A .. |
202 |
from \<open>A \<and> B\<close> have B .. |
|
203 |
from \<open>B\<close> \<open>A\<close> have "B \<and> A" .. |
|
10007 | 204 |
} |
61541 | 205 |
then show ?thesis .. -- \<open>rule \<open>impI\<close>\<close> |
10007 | 206 |
qed |
7820 | 207 |
|
61541 | 208 |
text \<open> |
209 |
\<^medskip> |
|
210 |
With these examples we have shifted through a whole range from purely |
|
211 |
backward to purely forward reasoning. Apparently, in the extreme ends we |
|
212 |
get slightly ill-structured proofs, which also require much explicit |
|
213 |
naming of either rules (backward) or local facts (forward). |
|
7820 | 214 |
|
61541 | 215 |
The general lesson learned here is that good proof style would achieve |
216 |
just the \<^emph>\<open>right\<close> balance of top-down backward decomposition, and |
|
217 |
bottom-up forward composition. In general, there is no single best way to |
|
218 |
arrange some pieces of formal reasoning, of course. Depending on the |
|
219 |
actual applications, the intended audience etc., rules (and methods) on |
|
220 |
the one hand vs.\ facts on the other hand have to be emphasized in an |
|
221 |
appropriate way. This requires the proof writer to develop good taste, and |
|
222 |
some practice, of course. |
|
7820 | 223 |
|
61541 | 224 |
\<^medskip> |
225 |
For our example the most appropriate way of reasoning is probably the |
|
226 |
middle one, with conjunction introduction done after elimination.\<close> |
|
7820 | 227 |
|
55640 | 228 |
lemma "A \<and> B \<longrightarrow> B \<and> A" |
10007 | 229 |
proof |
55640 | 230 |
assume "A \<and> B" |
231 |
then show "B \<and> A" |
|
10007 | 232 |
proof |
23373 | 233 |
assume B A |
234 |
then show ?thesis .. |
|
10007 | 235 |
qed |
236 |
qed |
|
7820 | 237 |
|
238 |
||
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
239 |
|
58614 | 240 |
subsection \<open>A few examples from ``Introduction to Isabelle''\<close> |
7001 | 241 |
|
61541 | 242 |
text \<open>We rephrase some of the basic reasoning examples of @{cite |
243 |
"isabelle-intro"}, using HOL rather than FOL.\<close> |
|
37671 | 244 |
|
7820 | 245 |
|
58614 | 246 |
subsubsection \<open>A propositional proof\<close> |
7833 | 247 |
|
61541 | 248 |
text \<open>We consider the proposition \<open>P \<or> P \<longrightarrow> P\<close>. The proof below involves |
249 |
forward-chaining from \<open>P \<or> P\<close>, followed by an explicit case-analysis on |
|
250 |
the two \<^emph>\<open>identical\<close> cases.\<close> |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
251 |
|
55640 | 252 |
lemma "P \<or> P \<longrightarrow> P" |
10007 | 253 |
proof |
55640 | 254 |
assume "P \<or> P" |
23373 | 255 |
then show P |
58614 | 256 |
proof -- \<open> |
61541 | 257 |
rule \<open>disjE\<close>: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$} |
58614 | 258 |
\<close> |
23393 | 259 |
assume P show P by fact |
10007 | 260 |
next |
23393 | 261 |
assume P show P by fact |
10007 | 262 |
qed |
263 |
qed |
|
7833 | 264 |
|
61541 | 265 |
text \<open>Case splits are \<^emph>\<open>not\<close> hardwired into the Isar language as a |
266 |
special feature. The \isacommand{next} command used to separate the cases |
|
267 |
above is just a short form of managing block structure. |
|
7833 | 268 |
|
61541 | 269 |
\<^medskip> |
270 |
In general, applying proof methods may split up a goal into separate |
|
271 |
``cases'', i.e.\ new subgoals with individual local assumptions. The |
|
272 |
corresponding proof text typically mimics this by establishing results in |
|
273 |
appropriate contexts, separated by blocks. |
|
7833 | 274 |
|
18193 | 275 |
In order to avoid too much explicit parentheses, the Isar system |
276 |
implicitly opens an additional block for any new goal, the |
|
61541 | 277 |
\isacommand{next} statement then closes one block level, opening a new |
278 |
one. The resulting behaviour is what one would expect from separating |
|
279 |
cases, only that it is more flexible. E.g.\ an induction base case (which |
|
280 |
does not introduce local assumptions) would \<^emph>\<open>not\<close> require |
|
281 |
\isacommand{next} to separate the subsequent step case. |
|
7833 | 282 |
|
61541 | 283 |
\<^medskip> |
284 |
In our example the situation is even simpler, since the two cases actually |
|
285 |
coincide. Consequently the proof may be rephrased as follows.\<close> |
|
7833 | 286 |
|
55656 | 287 |
lemma "P \<or> P \<longrightarrow> P" |
10007 | 288 |
proof |
55640 | 289 |
assume "P \<or> P" |
23373 | 290 |
then show P |
10007 | 291 |
proof |
292 |
assume P |
|
23393 | 293 |
show P by fact |
294 |
show P by fact |
|
10007 | 295 |
qed |
296 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
297 |
|
58614 | 298 |
text \<open>Again, the rather vacuous body of the proof may be collapsed. |
37671 | 299 |
Thus the case analysis degenerates into two assumption steps, which |
300 |
are implicitly performed when concluding the single rule step of the |
|
58614 | 301 |
double-dot proof as follows.\<close> |
7833 | 302 |
|
55656 | 303 |
lemma "P \<or> P \<longrightarrow> P" |
10007 | 304 |
proof |
55640 | 305 |
assume "P \<or> P" |
23373 | 306 |
then show P .. |
10007 | 307 |
qed |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
308 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
309 |
|
58614 | 310 |
subsubsection \<open>A quantifier proof\<close> |
7833 | 311 |
|
61541 | 312 |
text \<open>To illustrate quantifier reasoning, let us prove |
313 |
\<open>(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)\<close>. Informally, this holds because any \<open>a\<close> with |
|
314 |
\<open>P (f a)\<close> may be taken as a witness for the second existential statement. |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
315 |
|
61541 | 316 |
The first proof is rather verbose, exhibiting quite a lot of (redundant) |
317 |
detail. It gives explicit rules, even with some instantiation. |
|
318 |
Furthermore, we encounter two new language elements: the \isacommand{fix} |
|
319 |
command augments the context by some new ``arbitrary, but fixed'' element; |
|
320 |
the \isacommand{is} annotation binds term abbreviations by higher-order |
|
321 |
pattern matching.\<close> |
|
7833 | 322 |
|
55640 | 323 |
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" |
10007 | 324 |
proof |
55640 | 325 |
assume "\<exists>x. P (f x)" |
326 |
then show "\<exists>y. P y" |
|
61541 | 327 |
proof (rule exE) -- |
328 |
\<open>rule \<open>exE\<close>: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}\<close> |
|
10007 | 329 |
fix a |
330 |
assume "P (f a)" (is "P ?witness") |
|
23373 | 331 |
then show ?thesis by (rule exI [of P ?witness]) |
10007 | 332 |
qed |
333 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
334 |
|
61541 | 335 |
text \<open>While explicit rule instantiation may occasionally improve readability |
336 |
of certain aspects of reasoning, it is usually quite redundant. Above, the |
|
337 |
basic proof outline gives already enough structural clues for the system |
|
338 |
to infer both the rules and their instances (by higher-order unification). |
|
339 |
Thus we may as well prune the text as follows.\<close> |
|
7833 | 340 |
|
55640 | 341 |
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" |
10007 | 342 |
proof |
55640 | 343 |
assume "\<exists>x. P (f x)" |
344 |
then show "\<exists>y. P y" |
|
10007 | 345 |
proof |
346 |
fix a |
|
347 |
assume "P (f a)" |
|
23373 | 348 |
then show ?thesis .. |
10007 | 349 |
qed |
350 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
351 |
|
61541 | 352 |
text \<open>Explicit \<open>\<exists>\<close>-elimination as seen above can become quite cumbersome in |
353 |
practice. The derived Isar language element ``\isakeyword{obtain}'' |
|
354 |
provides a more handsome way to do generalized existence reasoning.\<close> |
|
9477 | 355 |
|
55640 | 356 |
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" |
10007 | 357 |
proof |
55640 | 358 |
assume "\<exists>x. P (f x)" |
10636 | 359 |
then obtain a where "P (f a)" .. |
55640 | 360 |
then show "\<exists>y. P y" .. |
10007 | 361 |
qed |
9477 | 362 |
|
61541 | 363 |
text \<open>Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and |
364 |
\isakeyword{assume} together with a soundness proof of the elimination |
|
365 |
involved. Thus it behaves similar to any other forward proof element. Also |
|
366 |
note that due to the nature of general existence reasoning involved here, |
|
367 |
any result exported from the context of an \isakeyword{obtain} statement |
|
368 |
may \<^emph>\<open>not\<close> refer to the parameters introduced there.\<close> |
|
9477 | 369 |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
370 |
|
58614 | 371 |
subsubsection \<open>Deriving rules in Isabelle\<close> |
7001 | 372 |
|
61541 | 373 |
text \<open>We derive the conjunction elimination rule from the corresponding |
374 |
projections. The proof is quite straight-forward, since Isabelle/Isar |
|
375 |
supports non-atomic goals and assumptions fully transparently.\<close> |
|
7001 | 376 |
|
55640 | 377 |
theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C" |
10007 | 378 |
proof - |
55640 | 379 |
assume "A \<and> B" |
380 |
assume r: "A \<Longrightarrow> B \<Longrightarrow> C" |
|
10007 | 381 |
show C |
382 |
proof (rule r) |
|
23393 | 383 |
show A by (rule conjunct1) fact |
384 |
show B by (rule conjunct2) fact |
|
10007 | 385 |
qed |
386 |
qed |
|
7001 | 387 |
|
10007 | 388 |
end |