Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Difference between lemma attribute and declare

Email Gateway (Nov 16 2021 at 12:16):

From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Dear list,

I have encountered some behavior that I didn't expect when using
attributes. Say we have an attribute test. If we use lemma t[test], then
the function that implements the attribute is called four times. If we
use declare t[test], the function is called five times.

Furthermore, I am working on some existing code that uses the name hint
of theorems (i.e. Thm.get_name_hint). I suspect that the code relies on
them in an undisciplined way but I don't want to change the whole thing
right now. Now, if we use lemma t[test], the name hint always exists.
For declare t[test], on the other hand, the theorem that is passed to
the attribute function only has a name hint 2/5 times.

My questions:

• What is the reason that the attribute function is called multiple times?
• What is the reason that the name hint does not always exist when using
  declare and is there a workaround?

Cheers,

Lukas

P.S: See the attached theory file for an example.
Scratch.thy

Last updated: Jan 04 2025 at 20:18 UTC