Re: [isabelle] Syntaxdefinition in Locales
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
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,
Am 14.09.2011 18:45, schrieb René Neumann:
I have the following setting (in Isabelle2011):
definition foo where
"foo a b G = id"
locale spam =
fixes G :: "'a"
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"
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
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and