[isabelle-dev] Name for derived quotient_def theorem

[Tobias Nipkow]

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