Re: [isabelle] rewriting with assumptions from right to left
you can always use the [symmetric] attribute:
assumes "fst a = a1" "snd a = a2"
shows "a = (a1, a2)"
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:
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and