Re: [isabelle] dest versus elim?



Hi,

chapter 5 of the tutorial (rules of the game) is exactly the right thing
to read (the whole chapter), in particluar 5.2..5.4 may answer your
questions.

Best,
  Peter


On Do, 2016-03-10 at 12:54 +0100, 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.