*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Problem with Pairs*From*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Date*: Thu, 31 Jul 2008 10:07:44 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <48916C7D.90802@uni-muenster.de>*References*: <489035FB.5050005@uibk.ac.at> <48916C7D.90802@uni-muenster.de>*User-agent*: Thunderbird 2.0.0.14 (X11/20080501)

Thanks for your reply,

lemma "(let (_,_,s) = f n in P s) = P (snd (snd (f n)))" unfolding Let_def split_def .. I don't know which (if any) of the two ways is preferable. christian Peter Lammich wrote:

A manual case split does the job. lemma "(let (_,_,s) = f n in P s) = P (snd (snd (f n)))" by (cases "f n") auto No idea whether there's an automatic way. -- Peter Christian Sternagel wrote:Hi there, I have problems using pattern-matching with pairs. The thing is that I'm not able to prove equivalence between an expression (let (_,_,s) = f n in P s) and P (snd (snd (f n))) Are there any general advices (except, don't use pairing =)). cheers christian

**References**:**[isabelle] Problem with Pairs***From:*Christian Sternagel

**Re: [isabelle] Problem with Pairs***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Problem with Pairs
- Next by Date: [isabelle] 1 year fellowship for a doctoral researcher on program analysis
- Previous by Thread: Re: [isabelle] Problem with Pairs
- Next by Thread: Re: [isabelle] Problem with Pairs
- Cl-isabelle-users July 2008 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