Hi Florian, All, 2011/11/29 Florian Haftmann <[email protected]>: > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
