[isabelle-dev] Isabelle cs. 70300f1b6835

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Oct 21 16:42:25 CEST 2012

Hi Ondrej,

> But your observation gave me an idea that actually I should remove the
> explicit names for morphisms in Mapping.thy completely and then you
> wouldn't even notice there are any abstraction and representation
> functions behind the scene.

I would conclude that if abs and rep are completely opaque and do not
appear in user space (cf. find_theorems!), the duplication lookup == rep
is fine.

Concerning the transfer-or-not question, the mapping type is not really
an issue and I don't really mind loosing mapping_eq_iff etc.  However
there are types where transfer is not the only valid approach to conduct
proofs on, e.g. multisets, as far as I can forsee at the moment.  So it
would be too much rush to drop all those fundamental lemmas there.
Maybe future will bring more insight on this.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121021/677bf01f/attachment.sig>

More information about the isabelle-dev mailing list