*To*: Freek Wiedijk <freek at cs.ru.nl>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] dest versus elim?*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Thu, 10 Mar 2016 13:30:20 +0100*In-reply-to*: <20160310115402.GA12555@wheezy.localdomain>*References*: <20160310115402.GA12555@wheezy.localdomain>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Dear Freek, for me, the difference is mostly in how a fact is stated. A basic example from natural deduction is conjunction elimination. In textbooks we often see two rules conj1: A & B ==> A conj2: A & B ==> B in Isabelle parlance those are "dest" (as in destructive) rules, since they loose information. If you apply such a rule (with drule) in an apply-script you can turn a provable subgoal into an unprovable one (since the fact that B holds disappeared). The corresponding "elim" rule (which I would really consider to be more general, as you suggested) is: conjE: A & B ==> (A ==> B ==> thesis) ==> thesis if you apply it with "erule" you just turn the single fact "A & B" into two facts "A" and "B" without (really) using information (since you could reconstruct "A & B" again with what you got). Moreover, the conclusion of "conjE" is so general that it will unify with the conclusion of any subgoal. So, whether "erule" succeeds or fails purely depends on whether some formula of the shape "?A & ?B" is among the premises of the subgoal. hope this helps, cheers chris On 03/10/2016 12:54 PM, Freek Wiedijk wrote: > Dear all, > > My apologies for a newbie question. > > I am trying to understand the relationship between "dest" > and "elim". From > > <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-March/msg00077.html> > > I got the impression that "elim" is a generalisation of > "dest". But in the Tutorial (reference from that message) > I read in 5.7 that "erule" unifies Q with the subgoal, > while "drule" does not. So that seems to imply that "erule" > might fail where "drule" does not? > > In the example files for Concrete Semantics, I see lemmas > (for example "SkipE") that are proved with "[elim]", but > where I think that you do not only want to use them when > their conclusion unifies with the goal? > > A pointer to a relevant book/manual is all I need. And if > this is too trivial, do not bother the list with this! > > Freek >

**References**:**[isabelle] dest versus elim?***From:*Freek Wiedijk

- Previous by Date: Re: [isabelle] dest versus elim?
- Next by Date: Re: [isabelle] dest versus elim?
- Previous by Thread: Re: [isabelle] dest versus elim?
- Next by Thread: Re: [isabelle] dest versus elim?
- Cl-isabelle-users March 2016 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