Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Local_Theory.map_naming in locales

view this post on Zulip Email Gateway (Aug 19 2022 at 17:12):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 17:14):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

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

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.

Having a look at Local_Theory.map_naming this is quite obvious

fun map_naming f =
map_top (fn (naming, operations, after_close, brittle, target) =>
(f naming, operations, after_close, brittle, target));

I.e. only the topmost context in the stack of local theories is affected.

It is unclear to me what can be done in our current infrastructure to
achieve the desired effect. I will spend some time to understand this
occasionally.

Florian

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

signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 17:16):

From: Makarius <makarius@sketis.net>
So far, the "naming" of a local_theory only refers to the background
theory for foundation. There is still no provision for more name space
control, but it is one of the important things in the pipeline for a very
long time. Over many years, there were just important ingredients missing
to move forward, e.g. unnamed context begin ... end blocks. There were
also rather lame reasons like the inability to write "private definition
..." or "private theorem ..." with TTY/Proof General still around.

There is a whole complex around name space policies, but I don't recall
all details on the spot. Here are some aspects to rekindle a discussion
of what could be done eventually.

* Some concrete syntax for bindings and namings (e.g. in context
headers) to add name space qualification (with and without "mandatory"
flag).

* Likewise some syntax for certain flags, e.g. "concealed", "private",
"hidden".

* Reform of existing theories to eliminate all uses of "hide", "hide
(open)", "map_naming" etc.

* Session-qualified theory names.

* Restoration of old tools that only cope with full names like
"Theory.foo" or "Theory.local.foo" -- paradoxically, such "old" tools
are sometimes only a few years old.

Makarius

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

From: Makarius <makarius@sketis.net>
This thread about Isabelle name space policies is continued on
isabelle-dev, just in the nick of time before the hot phase of the
Isabelle2015 process starts.

The "lame reasons" due to TTY/Proof General no longer exist ...

Makarius

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

From: Makarius <makarius@sketis.net>
On Thu, 12 Feb 2015, Andreas Lochbihler wrote:

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

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?

When making some name space reforms for Isabelle2015, I also looked at
this case, but did not see a way to do it properly.

Extra qualification of name bindings is possible in Isabelle/ML via
Binding.qualified, but there is no Isar syntax for it. Naming prefixes in
the name space are used by the system in other situations. Above the open
question is what happens with the naming under interpretation.

Moreover, many tools break down when they see more name prefixes than
expected. This is a problem of these tools, but the usual reason why the
system cannot move forward right now.

Further reforms are in the pipeline (for approx. 10 years) and will get
through eventually.

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.

Can you point to the concrete definitions for this?

Makarius

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

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,

Thanks for keeping this on the radar.

On 07/05/15 11:54, Makarius wrote:

Extra qualification of name bindings is possible in Isabelle/ML via Binding.qualified, but
there is no Isar syntax for it. Naming prefixes in the name space are used by the system
in other situations. Above the open question is what happens with the naming under
interpretation.

Moreover, many tools break down when they see more name prefixes than expected. This is a
problem of these tools, but the usual reason why the system cannot move forward right now.
In my use case, I am not adding more levels of prefixes than would be there anyway,
because I just want to emulate the effect of any other command.

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.

Can you point to the concrete definitions for this?
I stumbled over this limitation of inductive_set in JinjaThreads. In Isabelle2011-1, I
used an inductive to actually define an inductive set, because 'a set and 'a => bool were
the same at that time:
http://sourceforge.net/p/afp/afp-2011-1/ci/default/tree/thys/JinjaThreads/MM/JMM_Spec.thy#l113

When the two types were separated again, I converted the inductive into a function and
manually derived all the necessary theorems, as can be seen in
http://sourceforge.net/p/afp/afp-2014/ci/default/tree/thys/JinjaThreads/MM/JMM_Spec.thy#l111

Of course, it would be great if the names were action_loc_aux.intros instead of
action_loc_aux_intros etc.

I do not have a public real example in a locale, but I have attached a stripped-down
version. By the way, it would be great if parameters for inductive(_set) that are always
the same could be declared with for even if they are not the first ones (such as the x in
the attached example).

Best,
Andreas
Scratch.thy

Last updated: Apr 25 2024 at 20:15 UTC