*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]*From*: Holger Blasum <hbl at sysgo.com>*Date*: Thu, 20 Dec 2012 21:55:49 +0100*Cc*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <471B2DE1-DDC9-4526-8248-AFA898FB5B29@cam.ac.uk>*References*: <471B2DE1-DDC9-4526-8248-AFA898FB5B29@cam.ac.uk>*User-agent*: Mutt/1.5.21 (2010-09-15)

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, -- Holger

**Follow-Ups**:

**References**:**[isabelle] intro rule for &&&***From:*John Wickerson

- Previous by Date: Re: [isabelle] Simplifier: Ignoring duplicate rewrite rule should be modulo alpha-equivalence
- Next by Date: Re: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]
- Previous by Thread: Re: [isabelle] intro rule for &&&
- Next by Thread: Re: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]
- Cl-isabelle-users December 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list