[isabelle-dev] Quotient example with partiality?

[Cezary Kaliszyk]

Hi Florian, All,

2011/11/29 Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> I'm asking myself the question how one would define rational numbers
> using the quotient package.  The key issue is that the equivalence
> relation here is partial, ruling out denominators of value zero.  In the
> Isabelle reference manual I can find »partial:« in a syntax diagram but
> not any concrete example in the distribution.

When developing the quotient package we included the infrastructure
for defining quotient types with partial equivalence relations, however
since one of the main uses was supposed to be nominal (where its
always reflexive) we did not test the partial functionality too much.

The idea of using the quotient package with partial equivalence relations
is that two changes need to be done:

First if the user specifies 'partial:' in the quotient_type definition,
the obligation to prove changes from 'equivp' to 'part_equivp'. Which
is simpler,
but then less lifting can be done automatically (to be more precise, some
of the theorems that allow for automatic regularization do hold only for
reflexive equivalence relations).

Second, when lifting theorems, the theorems on the raw level can talk
about elements being in the domain (the reflexive part of the partial
equivalence relation). This is achieved by quantifying the variables with
bounded quantifiers that respect the partial equivalence relation. These
should then be lifted to quantifiers over the lifted type.

Having said this, we did not develop any examples where the relation would
be a real partial equivalence, we only tried to use 'partial' with reflexive
equivalence relations.

I will try to draft an example partial quotient and get back to you.

As for the second question, yes quotients do more than typedef so I am
also confused as to the reasons for mixing the two. It would be nice to
get it fully localized but still the meaning of typedef that restricts a type
fixed in a locale is quite unclear. Or has this been cleared in the meantime?

Regards,

Cezary