Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Ambiguity warning with _lessAll and _setless_All

Email Gateway (Aug 18 2022 at 10:03):

From: Peter Lammich <peter.lammich@uni-muenster.de>
I get the following warning in Isabelle 2005:

Ambiguous input "ALL y<(x::nat). P x"

produces 2 parse trees.

("Trueprop" ("_lessAll" y ("_constrain" x nat) ("_applC" P x)))

("Trueprop" ("_setlessAll" y ("_constrain" x nat) ("_applC" P x)))

Fortunately, only one parse tree is type correct.

You may still want to disambiguate your grammar or your input.

Should I simply ignore it, or is there a way to turn it off (While still
using the ALL y<x Syntax) ?

Greetings and thanks in advance
Peter

Email Gateway (Aug 18 2022 at 10:05):

From: Makarius <makarius@sketis.net>
You may ignore this as long as you only get warnings, but no errors.
Alternatively, the following declarations will disambiguate the grammer in
this respect:

no_syntax
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)

no_syntax (HOL)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)

syntax (output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)

syntax (HOL output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)

Makarius

Last updated: May 03 2024 at 04:19 UTC