Email Gateway (Aug 22 2022 at 09:56): 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: Nov 21 2024 at 12:39 UTC