Re: [isabelle] dest versus elim?



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
> 




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