Email Gateway (Aug 18 2022 at 19:04): Email Gateway (Aug 18 2022 at 19:04):From: Makarius <makarius@sketis.net>
"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.
Makarius
Email Gateway (Aug 18 2022 at 19:14):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
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:
syntax
"MyNotation" :: "args => 'a" ("{|(_)|}")
translations
"{|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!
Stephan
Last updated: Nov 21 2024 at 12:39 UTC