[isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]

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)

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)

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?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.