Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Private abbreviations scope extends over their...

Email Gateway (Aug 22 2022 at 18:54):

From: Peter Lammich <lammich@in.tum.de>
Hi List,

consider the following snippet

context begin
  private abbreviation "HD2 l ≡ hd (tl l)"
end

term "hd (tl l)"

(* Output:
"??.Scratch.HD2 l" :: "'a"
*)

I would have expected the abbreviation to be only folded inside the
context, b/c it is private ... however, the abbreviation is also folded
outside the context, to some strange ??.-constant.

Is their any way to make abbreviations actually local to a context? Or
does "private" with abbreviations simply make no sense?

Email Gateway (Aug 22 2022 at 18:54):

From: Makarius <makarius@sketis.net>
On 10/01/2019 11:08, Peter Lammich wrote:

Hi List,

consider the following snippet

context begin
  private abbreviation "HD2 l ≡ hd (tl l)"
end

term "hd (tl l)"

(* Output:
"??.Scratch.HD2 l" :: "'a"
*)

I would have expected the abbreviation to be only folded inside the
context, b/c it is private ... however, the abbreviation is also folded
outside the context, to some strange ??.-constant.

Here is the relevant paragraph from the isar-ref manual:

➧ ⬚‹private› or ⬚‹qualified› may be given as modifiers before any local
theory command. This restricts name space accesses to the local scope, as
determined by the enclosing ⬚‹context begin … end› block. Outside its
scope,
a ⬚‹private› name is inaccessible, and a ⬚‹qualified› name is only
accessible with some qualification.

It is all about name space accesses: the other aspects of a
specification element are unaffected. So the behaviour from above is to
be expected.

Is their any way to make abbreviations actually local to a context?

There might be some tricks, but I can't say anything on the spot.

Or
does "private" with abbreviations simply make no sense?

It might make sense in some situations of name space management, notably
with "abbreviation (input)".

Makarius

Email Gateway (Aug 22 2022 at 18:55):

From: Lars Hupel <hupel@in.tum.de>
Hi Peter,

I would have expected the abbreviation to be only folded inside the
context, b/c it is private ... however, the abbreviation is also folded
outside the context, to some strange ??.-constant.

this is working as designed. "private" and "qualified" affect the naming
discipline, not the visibility of other logical content. If you have a
private definition, it will still be part of the theory after you exit
the context, but its name is hidden.

I'm not even sure if there's an Isar command to "undo" abbreviations
(contrary to notation).

Is their any way to make abbreviations actually local to a context? Or
does "private" with abbreviations simply make no sense?

Do you want to reuse other things from the context elsewhere? In that
case, consider "experiment". This will open a context based on an
anonymous locale* that can't be interpreted once you exit it.

Alternatively, you could use a plain locale.

Cheers
Lars

• a locale with a random name

Email Gateway (Aug 22 2022 at 18:55):

From: Peter Lammich <lammich@in.tum.de>
Thanks for the quick responses.

In my use-case, 
  private abbreviation (input) 
was the way to go, as I merely used the abbreviation to allow more
concise writing of a bunch of lemmas and definitions.

Last updated: Apr 19 2024 at 08:19 UTC