Re: [isabelle] Syntax, translations inside a locale

On Fri, 24 Feb 2012, Stephan van Staden wrote:

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?

"Simple" and "properly" are in conflict here. Raw syntax + translations is a global macro mechanism that does not quite fit into the concept of local theory declarations, and their implicit transformation by morphisms that descrive how to move between different contexts.

Since raw syntax is totally unchecked, you can make an improper solution by some kind of dynamic scoping: produce global syntax that captures certain fixed variables as they occur in a locale, but probably somewhere else. (Local fixes with mixfix annotations are marked as "\<^fixed>xxx" in the syntax layer.)

Another way is to use "indexed syntax" as can be seen in some theories in src/HOL/Algebra (search for \<index> symbols). It would require some additional tinkering to make such context dependent notation work with free-form syntax, not just plain mixfix annotations.

A fully proper solution should be also possible, but requires further thought. I am trying myself for years to make record and datatype definitions ready for local theory contexts, together with their specific syntax. It will happen at some point in the future ...

BTW, syntax constants as "MyNotation" above are usually called like "_my_notation". The initial "_" prevents accidental overlap with non-syntax things, while still allowing plain prefix application syntax in translations patterns (independently of the concrete notation). In general, contemporary Isabelle sources are camel-case free.


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