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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
