[isabelle] A special notation for function application

Dear all,

I was trying to introduce some additional notation for linear
functionals in vector spaces; the idea is to use:

"[x, f]" as an alternative notation for "f x", where "f" is a linear
functional (let's say, type "'a => 'b") and "x" is an element of type
"'a" (note that the arguments f and x are interchanged in the proposed

I would like that all notation available for "f x" would still work
for the new notation "[x, f]", in such a way that

[x, f] \oplus [y, f]

would be equivalent to (without unfolding any particular definition):

f x \oplus f y

Is it possible to reach these behavior? How? Maybe brackets are
already a bit overloaded in terms of notation (lists, propositions...)
so a notation based for instance in "<x, f >" would be also

I tried the following approach (which does not interchange arguments)

  app :: "('b => 'a) => 'b => 'a" ("<(_),(_)>" 90)
  where "<f, x> == f x"

but then when I write, for instance, "term <f, x>" the system does not
seem to find the correct type of the expression.

Thanks for any hint,


Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

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