[isabelle] Type variables, locale import and notation



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"
> begin
>   definition bar :: "'a â 'a â bool" (infix "â" 50) where
>   "x â y = (â(l  :: 'b). foo x l y â pred l)"
> end
> 
> 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
> begin
>   term bar (* "op â"  :: "'a â 'a â bool" *)
>   term "op â" (* "op â" :: "'a â 'a â bool" *)
> end

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
> begin
>   term bar (* "Îtype. spec.bar ex" :: "'a itself â nat â nat â bool", where "'a :: b" *)
>   term "op â" (* Inner lexical error. Failed to parse term *)
> end

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"
> begin
>   term bar (* "s.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)
> end

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,
Ferdinand

-- 
Ferdinand Vesely
PhD Candidate
Department of Computer Science, Swansea University
http://cs.swan.ac.uk/~csfvesely/




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