[isabelle-dev] Bijections

[Florian Haftmann]

Hi all,
	
in 1a474286f315 I have introduced a locale for (total) bijections,
allowing to obtain typical facts like ‹inv f ∘ f = id› by interpretation.

The motivation was that most of these facts have not ‹bij› but ‹inj› or
‹surj› as premise, which makes proof complicated due to two lifting
steps, especially if you need the same facts over and over.

Of course there could also be a locale for partial bijections, and also
a whole hierarchy spanning injections etc., but this would result in a
lot of duplication.

The idea to turn all those predicates into locales sounds too radical
for me, since lifting arguments referring to terms like ‹bij (f ∘ g)›
are tedious to express within the module system. But maybe others with
more experience than me in that area have already made some thoughts
about that matter.
	
Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160704/de8b5d68/attachment.asc>