Re: [isabelle] finite sets and code generation



Hi Peter,

> For proof re-use reasons I use this idiom to fudge them into lists (in =
a definition context):
>=20
> xs_list =3D (SOME xs. set xs =3D { my finite set })
>=20
> The only substantial reason I have is that I can make use of the equiva=
lence relation partition operator '_ // _' on these sets.

If this is indeed the only reason, you should perhaps define an
alternative equivalence relation partition operator on lists and then
proof some lemmas which allow you to transfer theorems from the set to
the list representation (at least to some extent).

Sorry for being that vague, but we are still exploring how a systematic
transfer principle for such situations should look like.

Hope this helps,
	Florian

--=20

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

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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