Re: [isabelle] Syntaxdefinition in Locales



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

Am 14.09.2011 18:45, schrieb René Neumann:
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é


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
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 MHonArc.