[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 29 11:48:06 CET 2015
thanks for undertaking this.
I will have a look at this and give feedback.
Am 27.10.2015 um 18:59 schrieb Clemens Ballarin:
> Related to the below discussion on isabelle-users, I have now refined the patch I had circulated then. Here is the NEWS entry:
> * More gentle suppression of syntax along locale morphisms while
> printing terms. Previously 'abbreviation' and 'notation' declarations
> would be suppressed for morphisms (except term identity). Now merely
> 'notation' is suppressed. This can be of great help when working with
> complex locale hierarchies, because proof states are displayed much
> more succinctly. It also means that only notation needs to be
> redeclared if desired, as illustrated by this example:
> locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)
> definition derived (infixl "\<odot>" 65) where ...
> locale morphism =
> left!: struct composition + right!: struct composition'
> for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
> notation right.derived ("\<odot>''")
> The full patch is attached. Interestingly, it is fully compatible also with the AFP. Since I'm not particularly familiar with generic_target.ML I'm posting it here for feedback. My intention is to push this in the near future.
> On 28 July, 2015 12:12 CEST, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>> Hi Julian,
>> First of all, I would be very happy if you could solve this problem of missing
>> contractions. Clemens has never showed me an example where folding of abbreviations would
>> lead to non-termination. And I do not know precisely how abbreviations and locales are
>> implemented, so it is hard for me to decide whether something would lead to a problem.
>> Nevertheless, here is another example:
>> locale l = fixes f :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a"
>> definition (in l) foo where "foo ≡ f (%x. x)"
>> interpretation l "id" where "l.foo id == id (%x. x)" sorry
>> If the interpretation installs abbreviations which respect the rewrite morphism, then the
>> abbreviation reads as "id (%x. x) == id (%x. x)" which clearly loops. If it does not, then
>> "id (%x. x)" is always printed as "foo". This might not be optimal, as the right-hand
>> sides can be arbitrary general terms that should remain the way they are.
>> On 28/07/15 11:33, Julian Brunner wrote:
>>> 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"
>>> definition test where "test = f"
>>> sublocale f!: foo f "% x y z. g y z x" by this
>>> 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
>>> <mailto: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?
>>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev