Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Globally disabling record syntax?

Email Gateway (Nov 07 2023 at 17:09):

From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,

For a project we are systematically using the datatype_record package in
HOL-Library as opposed to the standard record type. Unfortunately, when
using datatype_record we suffer ambiguity everywhere when trying to use
record syntax owing to the use of the same functional record update syntax
for both record packages. Is there an easy way to globally disable the
syntax in Record.thy throughout a project to avoid this?

HOL-Library.Datatype_Records.thy contains a no_syntax declaration that
seems to try to do this, however in practice this doesn't seem to work.

Thanks,
Dominic

Email Gateway (Nov 08 2023 at 11:05):

From: Thomas Sewell <tals4@cam.ac.uk>
I haven't investigated whether this applies to record syntax, but this general advice might be relevant.

Does the no_syntax declaration work the Datatype_Records theory itself, or in any other theory that only includes that one? If so, the difficulty might be with theory merges.

Many things are a little awkward to disable in Isabelle because of the way theory/context merges work. The various datasets are combined into something like a union. So, if a problematic simp rule is added to the simpset in library theory A, and explicitly removed in theory B, a later theory C which imports both B and other parts of the library will tend to have the problematic rule appear again, because it will be present in the combined simpset if it was present in any of the simpsets to be merged, i.e. if there's any theory inclusion path from A->C which doesn't go via the deletion in B.

It's possible you can make the notation deletion work by ensuring that all the library inclusions in your development go through a small number of include theories, and that they explicitly do the necessary deletions.

One could imagine a system that tried to respect explicit deletions downstream, but this would require a more complex datastructure. Usually what's simpler is to try to avoid ever needing deletions. Have you considered using update notation that is similar but uses a different bit of syntax to the builtin datatype one?

Best regards,
Thomas.

Email Gateway (Nov 08 2023 at 13:10):

From: Makarius <makarius@sketis.net>
We have that already: declarations wrt. local contexts, e.g. 'locale' or 'bundle'.

This does not work for raw 'syntax' or 'no_syntax', because it is too low-level.

Makarius

Email Gateway (Nov 08 2023 at 13:21):

From: Makarius <makarius@sketis.net>
Actually, these commands are already "localized" since Isabelle2021-1
(December 2021). See NEWS:

• Commands 'syntax' and 'no_syntax' now work in a local theory context,
  but in contrast to 'notation' and 'no_notation' there is no proper way
  to refer to local entities. Note that local syntax works well with
  'bundle', e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory
  Main of Isabelle/HOL.

(This is merely a side-alley of this thread.)

Makarius

Email Gateway (Nov 08 2023 at 14:02):

From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Thanks for the replies.

The no_syntax command appears in Datatype_Records.thy in HOL-Library.
We surmised that this was related to different theories importing the HOL
library and the Datatype_Records.thy ftheory and therefore causing a
clash between the syntax and no_syntax commands. Unfortunately it will
be hard to rearrange our theory files to try to address this that way, I
think. If there's currently no easy way to handle this other than that
approach then I think we will consider introducing our own custom syntax or
continue living with the syntax ambiguity which isn't a major problem.

Thanks,
Dominic

Last updated: Apr 28 2024 at 20:16 UTC