Theory Brackets

theory Brackets
  imports Dual_Spaces
begin

section{*Brackets*}

context vector_space
begin

text{*The following notation is not working properly:
  1. I do not know how to invert the order of the parameters, in such a a way that
  @{text "<x,f>"} denotes @{term "f x"};
  2. Even in the right order, where @{text "<f,x>"} denotes @{term "f x"},
  the notation @{text "<f,x>"} produces problems when trying to use it.*}

text{*A couple of notes on the following notation; it is done trying to mimic 
  the similar ideas in Halmos. First of all, we have chosen the symbols @{text "< _ >"}
  instead of @{text "[ _ ]"} since brackets would produce ambiguous inputs
  with lists, forcing us to write explicitly in a lot of scenarios the type
  of each of the components of the pair.*}
text{*Second, the \emph{input} annotation of \emph{abbreviation} makes the
  special syntax proposed to work only in the input mode, \emph{i.e.}, when we
  write something. Wihtout this annotation, the output would be also changed, 
  but that would affect to every function application in our setting, which
  is not our intention and apparently makes the pretty printer loop. For more details
  see \url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-August/msg00007.html}*}

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

term "<x, f> ⊕ <y, f>"

end

end