Email Gateway (Aug 19 2022 at 09:35): Email Gateway (Aug 19 2022 at 09:35):From: Holger Blasum <hbl@sysgo.com>
Dear John,
... which is insoluble. I think the "apply rule" step is using the conjE rule. Which rule should I apply in order to obtain the preferred proof state below? I briefly tried conjunctionI but that doesn't seem quite to fit.
Looking at this for curiosity (we all agree that production proofs are
not usually down at this low-level) this appears strange to me indeed.
By "apply(insert conjE)" one can inspect what's inside a rule and that
for conjE gives me: "!!P Q R. P & Q ==> (P ==> Q ==> R) ==> R"
Conversely, straightforward conjunction elimination rules (conjunctionD1,
conjunctionD2) happily exists on the metalogical level "!! A B. PROP A &&&
PROP B ==> PROP A)", using it is simple:
lemma assumes "A &&& B" shows "A" "B"
using assms
apply(rule conjunctionD1)
using assms
apply(rule conjunctionD2)
done
As remedy, we can simply prove axioms conjD1 and conjD2:
lemma conjD1: "!!A B. A & B ==> A" by simp
lemma conjD2: "!!A B. A & B ==> B" by simp
And then what I assume you wanted to do (it's not exactly
your question, so the email subject was changed, maybe sb else works
out answering exactly that question) becomes:
lemma assumes "A & B" shows "A" "B"
using assms
apply(rule conjD1)
using assms
apply(rule conjD2)
done
Also checked with some treatments of Natural Deduction (examples:
Van Dalen, Logic and Structure 1997 p. 36, Prawitz, Natural
Deduction 1965 p. 20, Gentzen 1934, p. 186) that conjunction
elimination is presented in the style of conjD1 and conjD2 and not
Isabelle's conjE (of course, disjunction elimination is a different beast).
Is there any deeper reason "conjE" appears overly complicated and/or
"conjD1" and "conjD2" are not aboard?
best,
Email Gateway (Aug 19 2022 at 09:35):From: Tobias Nipkow <nipkow@in.tum.de>
Am 20/12/2012 21:55, schrieb Holger Blasum:
lemma conjD1: "!!A B. A & B ==> A" by simp
lemma conjD2: "!!A B. A & B ==> B" by simp
...
Is there any deeper reason "conjE" appears overly complicated
Because you used it with rule, not erule. It makes perfect sense in apply scripts.
and/or "conjD1" and "conjD2" are not aboard?
They are, and Proof General actually tells you so when you state conjD1:
Auto solve_direct: The current goal can be solved directly with
HOL.conjE: [|?P & ?Q; [|?P; ?Q|] ==> ?R|] ==> ?R
HOL.conjunct1: ?P & ?Q ==> ?P
Regards
Tobias
Email Gateway (Aug 19 2022 at 09:35):From: Makarius <makarius@sketis.net>
After some further acquaintance with the truely natural Natural Deduction
of Isabelle/Pure and Isabelle/Isar you will consider conjD1/conjD2 as much
less natural than they seem; and they are not elimination rules at all.
It might also help to ask the 'print_statement' command to print rules for
you in structured Isar form.
Thus neither conjE nor disjE look like beasts anymore.
Makarius
Last updated: Apr 16 2024 at 12:28 UTC