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.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
