[isabelle] Difference between lemma attribute and declare



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.

theory Scratch
  imports Main
begin

attribute_setup test = \<open>
  Thm.declaration_attribute (fn thm => fn context =>(@{print} (Thm.has_name_hint thm); context))
  |> Scan.succeed
  \<close>

lemma t[test]: "True"
  by (fact TrueI)
(* Prints
true
true
true
true
*)

declare t[test]
(* Prints
true
false
true
false
false
*)

end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.