[isabelle-dev] Bijections

[Johannes Hölzl]

Very nice!

One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?

 - Johannes

Am Montag, den 04.07.2016, 21:13 +0200 schrieb 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