Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] cancel group.

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

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,

Is there a reason for the following specification of not being part of
the Isabelle library?

context group_add
begin;
subclass cancel_semigroup_add;
proof
fix a b c :: 'a
assume "a + b = a + c"
then have "- a + a + b = - a + a + c"
unfolding add_assoc by simp
then show "b = c" by simp
next;
fix a b c :: 'a
assume "b + a = c + a"
then have "b + a + - a = c + a + - a" by simp;
then show "b = c" unfolding add_assoc; by simp;
qed;
end;

Best regards,

Viorel

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

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,

thanks for contributing this, until now this seems to have escaped
attention.

Cheers,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC