Re: [isabelle] Strange behavior of binders in locales

On 17/08/17 17:36, Diego Marmsoler wrote:
> Letâs say I have the following definition within locale A:
> definition myBinder :: "('a â bool) â bool" (binder "Ab" 10)
>   where "myBinder P â True"
> Now lets say I have another locale B which is based on A and for which I want to change the syntax of myBinder.
> Therefore I add the following in B:
> notation myBinder (binder "Bb" 10)
> now I get the following error message: âMore than one parse translation for "\<^const>MyTheory.A.myBinder_binderâ
> Does someone know how to change the syntax of a binder within a locale?
> (By the way it works well for any other mixfix notation)

The binder notation consists of some special tricks on top of syntax
translations.  The example above shows that local changes of binder
syntax has never been used before. Such corner cases may or may not work
and it is apriori unclear if that is strange or normal. Isabelle is so
complex that it is possible to fall off the "inhabitable area" occasionally.

Anyway, a quick test shows that it is possible to remove the old binder
explicitly with 'no_notation' and then add the new one, e.g. like this:


definition test:: "('a â bool) â bool"
  where "test P â True"

notation test (binder "+" 10)

no_notation test (binder "+" 10)
notation test (binder "-" 10)


A few more notes:

  * Definitions in Isabelle/HOL are usually expressed with the equality
of HOL (=), not the one of Pure (â). The latter is used internally for
foundational purposes, although some users have the habit to abuse it
for HOL definitions, because they like the syntactic priority better.
Note that for expressions of type bool, it is also possible to use the
notation â which has lower syntactic priority (but for binders
parentheses are required nonetheless).

  * Camel case is normally not used in Isabelle sources: there is a
general quest for readability of specifications and proofs and


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