[isabelle] cancel group.



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





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