Re: [isabelle] Ambiguity warning with _lessAll and _setless_All



On Tue, 2 Jan 2007, Peter Lammich wrote:

> 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) ?

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.