[isabelle] Local_Theory.map_naming in locales



Dear experts on name spaces and local theories,

I use Local_Theory.map_naming in an unnamed context to add a mandatory prefix to some theorems. For example,

context begin
local_setup â Local_Theory.map_naming (Name_Space.mandatory_path "foo") â
lemma bar: "bar â True" ..
end

Then, I get the theorem foo.bar, but not bar. I picked this pattern up from http://isabelle.in.tum.de/repos/isabelle/file/8f4a332500e4/src/HOL/Product_Type.thy#l1017

Unfortunately, this does not seem to work when I am inside a locale.

locale test = assumes *: True begin
context begin
local_setup â Local_Theory.map_naming (Name_Space.mandatory_path "foo") â
lemma bar: "bar â True" ..
end

Now, the theorem names "bar", "local.bar", and "test.foo.bar" are available. I would have expected "foo.bar", "local.foo.bar", and "test.foo.bar", but the first two do not exist.

Moreover, when I later interpret test, the foo prefix does not show up either. What is the recommended way to install such mandatory prefixes? What am I doing wrong here?

Background: Why do I need this? The command inductive_set does not allow instantiations in the parameters. Therefore, I first define my set foo as a predicate foop with inductive and then manually perform the translation to sets as would be done with inductive_set. To get the same names (foo.intros, foo.cases, ...), I open an unnamed context, add the mandatory prefix foo to the name space with map_naming and transfer the theorems for foop using [pred_to_set]. This works fine at the theory level.

Best,
Andreas




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