[isabelle] Dealing with Cases



Hey all:

I am now at the point where I need to start understanding a bit more 
about cases and how to work with case statements.  In particular, I have 
read about this thing called split, and it sort of makes senses, but I 
have not been able to use it very well.  In some specific cases I have 
been able to use the cases method quite well. Here is a simple one that 
kind of has me stumped though, how do I show this?

(case X of Blah x y => f x y)
= f (case X of Blah x y => x) (case X of Blah x y => y)

I guess that I am not sure how cases work under the hood, so I am not 
sure how I would go about handling this, as splitting twice does not seem 
to quite work the way that I want. 

-- 
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.






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