After a long discussion during a lunch break we decided to use
".rep_eq". I will also change "_rsp" to ".rsp". What about "_def"?
Should I change it to ".def" as well? "_def" seems to be a
inconsistency, I guess because of historical reasons. Should new
packages use ".def" instead of "_def"?
Ondrej
On 03/28/2012 09:29 AM, Tobias Nipkow wrote:
Yes, "simps" should not be used for special purpose rules.
Tobias
Am 28/03/2012 09:22, schrieb 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
