Re: [isabelle] cancel group.



Hi Viorel,

> 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;

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

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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