[isabelle-dev] Name for derived quotient_def theorem

Tobias Nipkow nipkow at in.tum.de
Wed Mar 28 09:29:23 CEST 2012

Yes, "simps" should not be used for special purpose rules.


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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list