Email Gateway (Aug 18 2022 at 18:23): Email Gateway (Aug 18 2022 at 18:23):From: René Neumann <lists@necoro.eu>
Dear list-members,
I have the following setting (in Isabelle2011):
definition foo where
"foo a b G = id"
locale spam =
fixes G :: "'a"
begin
abbreviation f ("_ \<rightarrow>\<star> _" [100,100] 40)
where "f a b == foo a b G"
abbreviation test ("_ \<star> _" [100,100] 40)
where "test a b == a > b"
end
locale eggs =
...
sublocale eggs <= spam "some_rather_complex_instantiation"
My problem now is, that my new syntax of f is available in the locale
spam, but not in eggs (after the sublocale proof), while the
abbreviation itself is.
To make things even more tricky: The new syntax defined for 'test' works
just fine in spam and in eggs. It seems like any definition containing G
just kills the syntax interpretation in sublocales.
Is this a bug, a feature or something that is wrong to try in the first
place? My reason is, that I wanted to hide the
'some_rather_complex_instantiation' throughout eggs and its sublocales
whenever I work with foo. (I know, that I could just use the plain
abbreviation without the syntax, but well ... :))
(Btw: Using 'definition' instead of 'abbreviation' does not change
anything).
Thanks,
René
Email Gateway (Aug 18 2022 at 18:23):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear René,
this is a "feature" of the locale mechanism that is documented in the locale
tutorial, see Section 6, immediately before Section 6.1 starts, and has been
mentioned in
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-February/msg00058.html
Syntax declarations are disabled when inherited through a non-identical morphism
as in your case. Test works because it only involves locale parameters that are
at most renamed -- in fact, it does not involve any parameter.
As you will notice, not only input syntax is lost, but also the pretty printer
no longer collapses the abbreviation:
term "f" prints as "%a b. foo a b some_rather_complex_instantiation"
However, you can easily reinstall the syntax translation for f as follows, but
this will not give you the print translation.
notation (in eggs) f ("_ \<rightarrow>\<star> _" [100,100] 40)
If you also want to print "a \<rightarrow>\<star> b" instead of "foo a b
some_rather_complex_instantiation", you have to manually install a translation.
You can achieve this most easily by introducing another abbreviation:
abbreviation (in eggs)
"f'" ("_ \<rightarrow>\<star> _" [100,100] 40)
where "f' a b == foo a b some_rather_complex_instantiation"
Hope this helps,
Andreas
Last updated: Apr 19 2024 at 08:19 UTC