[isabelle-dev] Name for derived quotient_def theorem

[Ondřej Kunčar]

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