*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Contracting Abbreviations of Locale Definitions*From*: Julian Brunner <julianbrunner at gmail.com>*Date*: Tue, 28 Jul 2015 09:33:48 +0000*In-reply-to*: <55B726DD.5010406@inf.ethz.ch>*References*: <CAE5E_attrbdE-N8+XjiSme6uD9FZdeBaLSFqDg3+FVpVi2=8yw@mail.gmail.com> <55B726DD.5010406@inf.ethz.ch>

Hi Andreas, Good call on the overlapping abbreviations, I did not consider this case. However, the conflict already arises with the current implementation. Consider the following: locale foo = fixes f :: "'a => 'a => bool" fixes g :: "'a => 'a => 'a => bool" begin definition test where "test = f" sublocale f!: foo f "% x y z. g y z x" by this end This generates the following abbreviations (they end up in the Consts record in this order): f.test == foo.test f f.f.test == foo.test f test == foo.test f Since 'test' only depends on the parameter f, which is interpreted under the identity morphism (eta contraction seems to matter here, so this does not happen with your original example), all of these abbreviations are set up to be contracted before printing. In fact, 'test' is printed as 'f.test' (presumably due to the order of the abbreviations in the Consts record). Given that these contraction conflicts are already a problem as it is, I do not think that it would make things significantly worse to allow contraction of abbreviations introduced via other morphisms (barring other problems like the one you discussed with Clemens Ballarin). On Tue, Jul 28, 2015 at 8:53 AM Andreas Lochbihler < andreas.lochbihler at inf.ethz.ch> wrote: > 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? > > Andreas > > > 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: > > > > > https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-September/msg00040.html > > > https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-January/msg00029.html > > > > 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. > > >

**Follow-Ups**:**Re: [isabelle] Contracting Abbreviations of Locale Definitions***From:*Andreas Lochbihler

**References**:**[isabelle] Contracting Abbreviations of Locale Definitions***From:*Julian Brunner

**Re: [isabelle] Contracting Abbreviations of Locale Definitions***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] apply x apply y vs. by x y
- Next by Date: Re: [isabelle] Implementing the higher-order logic Q0 within the Isabelle proof assistant software
- Previous by Thread: Re: [isabelle] Contracting Abbreviations of Locale Definitions
- Next by Thread: Re: [isabelle] Contracting Abbreviations of Locale Definitions
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list