Re: [isabelle] rewriting with assumptions from right to left



Viorel Preoteasa schrieb:
> Hello,
> 
> I have the following lemma:
> 
> lemma "fst a = a1 ==> snd a = a2 ==> a = (a1, a2)";
> 
> This will be automatically proved by using the assumptions from
> right to left.
> 
> Is there a way of simplifying using the assumptions from right
> to left?

We are getting a bit specialized here, aren't we?
Sledgehammering this goal yields

by (metis surjective_pairing).

Tobias

> Best regards,
> 
> Viorel





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