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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
