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

Hi Viorel,

you can always use the [symmetric] attribute:

  assumes "fst a = a1" "snd a = a2"
  shows "a = (a1, a2)"
  using assms[symmetric]
  by simp

There are of course other methods to work with pair splitting. You could
add the rules:

  (A, B) = X <-> fst X = A /\ snd X = B
  X = (A, B) <-> fst X = A /\ snd X = B

But of course these rules are very dangerous! The simplifier can't
rewrite X after applying these rules.


Am Donnerstag, den 11.11.2010, 12:21 +0200 schrieb Viorel Preoteasa:
> 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?
> Best regards,
> Viorel

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