Email Gateway (Aug 18 2022 at 16:21): 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: Apr 19 2024 at 20:15 UTC