[isabelle] Syntax, translations inside a locale

Dear all,

I'm working in a locale where I have an associative and commutative operator + with unit 0. I want an alternative notation for it - an operator, say {|_|}, with arbitrary (but finite) arity.

Without Isabelle I would write:

{| n1, n2, ..., nk |}   =def   n1 + n2 + ... + nk

Then I want to prove/use theorems such as {|n1, n2|} + n3 = {|n1, n2, n3|}, etc.

In Isabelle, I've tried to write:

  "MyNotation" :: "args => 'a"  ("{|(_)|}")
  "{|x, xs|}" == "x + {|xs|}"
  "{| |}" == "0"

However, it gives the error: 'Illegal application of command "syntax" in local theory mode'.

Is there a simple way to do it properly in a locale? Thanks in advance for help and pointers!


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