Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 16:25):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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

Email Gateway (Aug 18 2022 at 16:26):

From: Simon Meier <simon.y.meier@gmail.com>
Hi Viorel,

this is not precisely the answer you are looking for, but the following
proof script should also do the trick of proving the lemma:

by (cases a) auto

best regards,
Simon

Email Gateway (Aug 18 2022 at 16:26):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Email Gateway (Aug 18 2022 at 16:26):

From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Viorel,

you can always use the [symmetric] attribute:

lemma
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.

Greetings,
Johannes

Last updated: Apr 19 2024 at 20:15 UTC