Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Local_Theory.map_background_naming does not sh...


view this post on Zulip Email Gateway (Aug 22 2022 at 09:56):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts on name spaces,

As described in another thread
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-May/msg00084.html
I am working around the restriction that we cannot have instantiated arguments to
inductive_set definitions. I try to imitate what the wrapper for inductive_set does using
the attribute to_set and Local_Theory.map_background_naming to get the qualified theorem
names.

As discussed in the thread mentioned above, Local_Theory.map_background_naming does not
work inside locales. I now discovered that it does not shadow existing theorem names,
either, when I use it inside another unnamed context. The shadowing only takes place after
all contexts have been left. In the example below, I would have expected the second "thm
list.simps" to refer to the new theorem, but it does not.

theory Scratch imports Main begin

thm list.simps (* refers to List.list.simps *)
context begin
context begin
local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "list") *}
lemma simps: "True" ..
end
thm list.simps (* refers to List.list.simps, expected is Scratch.list.simps *)
end
thm list.simps (* refers to Scratch.list.simps *)

end

I guess this is another limitation of the current name space situation that might
eventually improve. For the time being, is there a better way to acheive what I want -
with less surprises?

Andreas


Last updated: Mar 28 2024 at 16:17 UTC