[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 29 11:48:06 CET 2015
Hi Clemens,
thanks for undertaking this.
I will have a look at this and give feedback.
Cheers,
Florian
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)
> begin
> definition derived (infixl "\<odot>" 65) where ...
> end
>
> locale morphism =
> left!: struct composition + right!: struct composition'
> for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
> begin
> notation right.derived ("\<odot>''")
> end
>
> 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.
>
> Clemens
>
>
> 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.
>>
>> Andreas
>>
>> 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"
>>> 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
>>> <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?
>>>
>>> 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.
>>> >
>>>
>>
>
>
>
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151029/72919ba8/attachment.sig>
More information about the isabelle-dev
mailing list