[isabelle-dev] Name for derived quotient_def theorem
bulwahn at in.tum.de
Wed Mar 28 09:22:14 CEST 2012
Thank you for your suggestions. We will take them into account.
On 03/28/2012 07:26 AM, Florian Haftmann wrote:
> the name given to the derived theorem is unsatisfactory. Since it is
> not a »code-only« theorem, it should not carry the »code« within. If it
> would be a »code-only« theorem, the convention is to suffix with
> »_code«, not »_code_eqn«.
> Also, for derived theorems proved by packages it is much more common to
> use qualification suffixes (e.g. ».simp«, ».intro«) rather than plumbing
> underscores (cf. module binding.ML). Btw. this also applies to the
> respectfulness theorem: ».rsp« would be better than »_rsp«.
This is explained by looking at the history: The typedef package
introduces names with underscores, quotient_type and quotient_def
inherit this from typedef.
Here a list of names we were thinking of while discussing:
In the end, we decided for the one you can see (although I am personally
still in favor of abs_equation or similar).
I think ".simp" is rather strange, because it is really not simplifying
anything, but rather unfolding the definition in some special way.
More information about the isabelle-dev