Re: [isabelle] Problem with Pairs



Thanks for your reply,

in the meantime I found out (thnx to Alexander Krauss) that the following also does work

 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









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