[isabelle-dev] Name for derived quotient_def theorem

[Lukas Bulwahn]

Hi Florian,


Thank you for your suggestions. We will take them into account.

On 03/28/2012 07:26 AM, Florian Haftmann wrote:
> http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53
> 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:

- abstract_eq
- abs_equation
- abs_def
- code_cert
- code_certificate

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.


Lukas