Re: [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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev