[isabelle] Unexpected printing of nested PROP functions · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected printing of nested PROP functions

Email Gateway (Aug 13 2025 at 09:58):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Dear list,

I am using Isabelle2025 and want to report an unexpected behaviour of
the printing of terms containing nested prop functions (form
Isabelle/Pure).

A minimal example is "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop)
PROP x)", which is printed as "PROP f PROP g PROP x", which can be
misinterpreted as "f g x".

Some possible outputs that are less prone to misinterpretation:

"PROP f PROP (g PROP x)"
"PROP f (g x)"
"PROP f PROP (g x)"
Note that all these cases can already correctly be used as input.

Below, you can find a corresponding theory file.

Best wishes,

Kevin

theory Scratch
   imports Pure
begin

term "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop) PROP x)"
(*
This prints "PROP f PROP g PROP x", which can be misinterpreted as "f g x".
*)

end

Email Gateway (Aug 14 2025 at 10:38):

From: Tobias Nipkow <nipkow@in.tum.de>
Kevin,

I think I am to blame for PROP and the grammar may indeed be suboptimal. I'll
take a look soon.

Tobias

On 13/08/2025 11:50, Kevin Kappelmann wrote:

Dear list,

I am using Isabelle2025 and want to report an unexpected behaviour of the
printing of terms containing nested prop functions (form Isabelle/Pure).

A minimal example is "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop) PROP x)",
which is printed as "PROP f PROP g PROP x", which can be misinterpreted as "f g x".

Some possible outputs that are less prone to misinterpretation:
1. "PROP f PROP (g PROP x)"
2. "PROP f (g x)"
3. "PROP f PROP (g x)"
Note that all these cases can already correctly be used as input.

Below, you can find a corresponding theory file.

Best wishes,

Kevin

```isabelle
theory Scratch
imports Pure
begin

term "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop) PROP x)"
(*
This prints "PROP f PROP g PROP x", which can be misinterpreted as "f g x".
*)

end
```

smime.p7s

Email Gateway (Aug 14 2025 at 10:40):

From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Kevin, as I guess you know, Isabelle maintains a separation between the object-logic and the meta-logic by relying on an embedding from the former to the latter, which is hidden from users for the sake of readability. The drawback is that a rule such as P ==> P becomes ambiguous as to whether P has (assuming Isabelle/HOL) type bool or type prop. Therefore, the notation “PROP term" is provided to suppress the default embedding and ensure that in “PROP P" the variable has type prop. So I'm not even sure why you need three PROPs in f(g x); I would expect “PROP f (g x)".

Things have changed massively in the past 30 years or so, and I see that the syntax is now defined as follows:

("_aprop", typ "aprop ⇒ prop",
Mixfix.mixfix "(‹open_block notation=‹prefix PROP››PROP _)"),

Maybe something can be tweaked in Pure/pure_thy.ML.

Larry

On 13 Aug 2025, at 10:50, Kevin Kappelmann <kevin.kappelmann@tum.de> wrote:

Dear list,

I am using Isabelle2025 and want to report an unexpected behaviour of the printing of terms containing nested prop functions (form Isabelle/Pure).

A minimal example is "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop) PROP x)", which is printed as "PROP f PROP g PROP x", which can be misinterpreted as "f g x".

Some possible outputs that are less prone to misinterpretation:
1. "PROP f PROP (g PROP x)"
2. "PROP f (g x)"
3. "PROP f PROP (g x)"
Note that all these cases can already correctly be used as input.

Below, you can find a corresponding theory file.

Best wishes,

Kevin

```isabelle
theory Scratch
imports Pure
begin

term "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop) PROP x)"
(*
This prints "PROP f PROP g PROP x", which can be misinterpreted as "f g x".
*)

end
```

Email Gateway (Aug 15 2025 at 11:35):

From: Makarius <makarius@sketis.net>
On 14/08/2025 12:40, Lawrence Paulson wrote:

Things have changed massively in the past 30 years or so, and I see that the syntax is now defined as follows:

("_aprop", typ "aprop ⇒ prop",
Mixfix.mixfix "(‹open_block notation=‹prefix PROP››PROP _)"),

Maybe something can be tweaked in Pure/pure_thy.ML.

Indeed, things have changed a lot in the past decades. I am responsible for
almost everything there, and I won't accept arbitrary patches.

I am presently busy elsewhere to look myself. The motivation of the example is
rather weak.

Makarius

Email Gateway (Aug 15 2025 at 11:48):

From: Makarius <makarius@sketis.net>
On 13/08/2025 11:50, Kevin Kappelmann wrote:

I am using Isabelle2025 and want to report an unexpected behaviour of the
printing of terms containing nested prop functions (form Isabelle/Pure).

```isabelle
theory Scratch
imports Pure
begin

term "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop) PROP x)"
(*
This prints "PROP f PROP g PROP x", which can be misinterpreted as "f g x".
*)

end
```

Side remark: PIDE markup in Isabelle2025 effectively highlights subexpressions
of inner syntax in input and output (although it is technically about mixfix
syntax blocks instead of actual lambda-term expressions).

So using the normal C-mouse hovering in Isabelle/jEdit (not Isabelle/VSCode),
you will see the structure of the term.

Moreover, output does not require the C modifier for mouse hovering, so casual
users will quickly see, what they did not explicitly ask for.

Here is my version of the example:

theory Scratch
imports Pure
begin

notepad
begin
fix f :: "prop ⇒ prop"
and g :: "prop ⇒ prop"
and x :: "prop"
term "PROP f PROP g PROP x"
end

end

Despite the ambiguity of the syntax, the Prover IDE makes clear what the
structure of the underlying term application really is.

(The deeper reason why PROP syntax for the special "aprop" category has many
odd side-conditions is that this hardly ever occurs in regular applications.
An when it does occur, there are more oddities to be expected from the logical
side.)

Makarius

Email Gateway (Aug 15 2025 at 13:12):

From: Manuel Eberl <manuel@pruvisto.org>
Side note: there is some other syntax that is also a bit odd. For
example, if you have a function applied to "CARD('a)", that gets
rendered as "f CARD('a)". So the CARD basically looks like a function,
but it isn't. And it binds more strongly than a function application, in
some sense.

Not a huge issue or anything, but definitely confusing. But at least
nowadays, the CARD syntax is ctrl+clickable, so someone who is not
familiar with it can quickly find out what it means.

Manuel

On 15/08/2025 13:48, Makarius wrote:

On 13/08/2025 11:50, Kevin Kappelmann wrote:

I am using Isabelle2025 and want to report an unexpected behaviour of
the printing of terms containing nested prop functions (form
Isabelle/Pure).

```isabelle
theory Scratch
imports Pure
begin

term "PROP (f :: prop ⇒ prop) PROP ((g :: prop ⇒ prop) PROP x)"
(*
This prints "PROP f PROP g PROP x", which can be misinterpreted as "f
g x".
*)

end
```

Side remark: PIDE markup in Isabelle2025 effectively highlights
subexpressions of inner syntax in input and output (although it is
technically about mixfix syntax blocks instead of actual lambda-term
expressions).

So using the normal C-mouse hovering in Isabelle/jEdit (not
Isabelle/VSCode), you will see the structure of the term.

Moreover, output does not require the C modifier for mouse hovering,
so casual users will quickly see, what they did not explicitly ask for.

Here is my version of the example:

theory Scratch
imports Pure
begin

notepad
begin
fix f :: "prop ⇒ prop"
and g :: "prop ⇒ prop"
and x :: "prop"
term "PROP f PROP g PROP x"
end

end

Despite the ambiguity of the syntax, the Prover IDE makes clear what
the structure of the underlying term application really is.

(The deeper reason why PROP syntax for the special "aprop" category
has many odd side-conditions is that this hardly ever occurs in
regular applications. An when it does occur, there are more oddities
to be expected from the logical side.)

Makarius

Email Gateway (Aug 15 2025 at 21:36):

From: Makarius <makarius@sketis.net>
On 15/08/2025 15:09, Manuel Eberl wrote:

Side note: there is some other syntax that is also a bit odd. For example, if
you have a function applied to "CARD('a)", that gets rendered as "f CARD('a)".
So the CARD basically looks like a function, but it isn't. And it binds more
strongly than a function application, in some sense.

This kind of "quasi-first-order application" stems from a time before
Isabelle/HOL, as we know it today. See all other object-logics to get a sense
of the original Isabelle framework.

I have my own list of things that could be improved at some indefinite point
in the future.

Now that we have so much markup, we could eventually come up with
Isabelle/Scala tools to do inner-syntax updates systematically --- no crappy "AI".

Makarius

Last updated: Aug 20 2025 at 20:23 UTC