Re: [isabelle] Contracting Abbreviations of Locale Definitions

Hi Julian,

I also regularly suffer from these pretty-printing nightmares, but I vaguely remember a discussion with Clemens Ballarin on the subject. IIRC the problem is that it is not clear whether collapsing the abbreviations terminates in all cases. Clemens has never showed me an example where it actually happens, though.

Yet, I can still think of difficult situations as as the following:

locale foo =
  fixes f :: "'a => 'a => bool"
  and g :: "'a => 'a => 'a => bool"

definition (in foo) test where "test = f"

sublocale foo â f: foo "%x y. f y x" "%x y z. g y z x" .

This sublocale declaration makes the locale subgraph cyclic, However, the round-up algorithm realises that if you go six times through the circle, the composed parameter instantiations are alpha-beta-eta-equivalent to f and g again, so it stops. That means that the sublocale command adds five copies of foo to itself. Now consider the situation for the abbreviations. We have

  local.test == foo.test f

from the original definition. From the sublocale command, we would also get

  local.f.test == foo.test (%x y. f y x)
  local.f.f.test == foo.test f
  local.f.f.f.test == foo.test (%x y. f y x)
  local.f.f.f.f.test == foo.test f
  local.f.f.f.f.f.test == foo.test (%x y. f y x)

Obviously, they overlap. So which one should be used by the pretty-printer?


On 27/07/15 21:12, Julian Brunner wrote:
Dear all,

Isabelle will not contract the abbreviations introduced for locale
definitions when the locale is interpreted through a morphism other than
the identity. This behavior is described in the following threads:

The workaround that is proposed in these threads is to introduce additional
abbreviations after having interpreted the locale. In my formalization,
this would result in so much boilerplate as to make the whole appproach
using locales unusable. Now I'm wondering why this behavior was introduced
in the first place. Since there is no problem with expanding these
abbreviations, why would there be one with contracting them?

It seems like the reason for the abbreviations not being contracted is that
they use the "internal" print mode. Unfortunately, I was unable to find the
place where the print mode is set on these abbreviations in order to do
more experiments on this. So, before spending more time on this, I wanted
to ask what the original reasons for this behavor were and if it might be
possible to enable contraction of these abbreviations.

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