florian.haftmann at informatik.tu-muenchen.de
Mon Jul 4 21:13:37 CEST 2016
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev