Re: [isabelle] New type class definitions and the underlying type classes



Hi Jesus,

> More generally, is there a difference between the two following type
> class definitions? Is there a "better" or a "more appropriate" way to
proceed?

> class A = bar +
>    fixes foo :: "'a::type"
>
> class B =
>    fixes foo :: "'a::bar"

Definitely.  For class A, you get at the back a locale A importing from
another locale bar, with a corresponding type class A which is a
subclass of another type class bar.

For class B, you get at the back a locale B which does not import any
other locale, with a corresponding type class B which *is* a subclass of
another type class bar.

For class A, you can prove additional locale dependencies *plus*
corresponding subclass relations by means of subclass.

For class B, you can only prove additional subclass relations by means
of instance … \<subseteq> …, in lack of a corresponding locale for the
potential superclass.

I would suggest to go the path with classes of shape A unless there are
good reasons not to do so.

Cheers,
	Florian

-- 

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.