Re: [isabelle] dest versus elim?



The terminology comes from natural deduction.

- intro is for introduction rules, which are used in back-chaining style to reduce a goal to subgoals

But elimination rules in natural reduction come in two forms. The most general form (e.g. disjE or exE in Isabelle) allows any formula as the conclusion, and is analogous to a sequent calculus rule that operates only on the left side. But there is also a special form (e.g. conjunct1, mp) that doesnât fit this pattern, but performs forward reasoning. I have called these destruction rules, but this nomenclature is totally non-standard.

- elim is for proper elimination rules
- dest is for destruction rules, and performs forward reasoning in your assumptions 

Larry

> On 10 Mar 2016, at 11:54, Freek Wiedijk <freek at cs.ru.nl> 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.