Re: [isabelle] Type variables, locale import and notation

Dear Ferdinand,

Any notation is dropped when you instantiate the parameters of a locale beyond renaming. The reason is that in general the number of arguments changes, so the notation does not make much sense any more. You can always reintroduce the notations using the command `notation` as follows:

  context s3 begin
  notation bar (infix "â" 50)

The reason for the type token 'b itself for bar is as follows: In HOL, all type variables in the definition of a constant must appear in the type of the constant. Otherwise, inconsistencies could be introduced. In Isabelle, abbreviations must also obey this rule. Now, the locale constant bar gets translated to a foundational constant with the locale parameters as additional ones. This can be seen when pretty-printing bar in s3: you get " ex". Now, ex contains the type variable 'b, which does not show up in the fixed parameters of the locale (in fact s2 does not fix any parameters at all). Therefore, Isabelle introduces the type token for


On 24/04/16 01:51, Ferdinand Vesely wrote:
Dear List,

I have a problem with using (infix) notation inside a locale in
combination with type variables. In summary, I'm trying to introduce a
binary abbreviation of a ternary predicate, where the type of the
omitted parameter is a type variable (restricted by a sort). On the
top-level, such a binary abbreviation is generalised to three
parameters again by introducing a "type parameter" (e.g., "'a itself").
I've figured out that by using locales I can fix the (abstract) type
locally and use the binary predicate inside the locale as I've
intended. However, this does not play well when I also want to use
infix notation for the abbreviation in a specialised locale (= import
with instantiated parameter). Here is a contrived example of my
problem. First the basic definitions:

class a = fixes pred :: "'a â bool"

locale s =
   fixes foo :: "'a â ('b :: a) â 'a â bool"
   definition bar :: "'a â 'a â bool" (infix "â" 50) where
   "x â y = (â(l  :: 'b). foo x l y â pred l)"

class b = a +
   assumes b_pred: "âl. pred l"

definition ex :: "nat â ('b :: b) â nat â bool" where
"ex x l y = (y = x + 1 â pred l)"

Now if I create a new locale where I only import locale s above, the
types are as expected:

locale s1 = s
   term bar (* "op â"  :: "'a â 'a â bool" *)
   term "op â" (* "op â" :: "'a â 'a â bool" *)

But if I want to specialise the locale with the above definition of 'ex,
the type parameter is re-introduced even inside the locale and the infix
notation does not work anymore (Isabelle does not warn about this). I'm
not sure why the parameter is introduced inside the locale. Why is this
the case? Shouldn't the types of the corresponding parameters of 'foo'
and 'ex' be unified?

locale s2 = s where foo = ex
   term bar (* "Îtype. ex" :: "'a itself â nat â nat â bool", where "'a :: b" *)
   term "op â" (* Inner lexical error. Failed to parse term *)

Anyway, I've found out that if I add a new locale parameter with the
same sort constraint on the type as in the type of 'ex', the additional
"itself parameter" is not introduced. However, the infix notation still
does not work.

locale s3 = s where foo = "ex :: nat â ('b :: b) â nat â bool" +
   fixes t :: "('b :: b) itself"
   term bar (* " ex" :: "nat â nat â bool" *)
   term "op â" (* Inner lexical error. Failed to parse term *)

   lemma "1 â 2" (* Inner lexical error. Failed to parse term *)

   lemma "bar 1 2" (* OK *)
   by (simp add: bar_def ex_def b_pred)

   lemma "Âbar 2 1" (* OK *)
   by (simp add: bar_def ex_def)

Why is the infix notation for bar silently dropped in locale s3? Is
there any way around this, i.e., using the infix notation introduced
in locale s?

My other question is if there is a better way to introduce such an
abbreviation without implicitly adding the extra "type parameter" and
to keep the infix notation.

Kind regards,

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