[isabelle] Local_Theory.map_background_naming does not shadow names



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




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