Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Abbreviations with adhoc-overloaded constants

Email Gateway (Aug 22 2022 at 10:45):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,

I am struggling with abbreviations that involve constants which have been registered with
adhoc_overloading. My problem is that I cannot get Isabelle's pretty-printer to fold the
abbreviations again.

Below is the minimal example (for Isabelle2015).

consts foo :: "'a ⇒ 'a"
consts foo_nat :: "nat ⇒ nat"
adhoc_overloading foo foo_nat

abbreviation bar :: "nat ⇒ nat" where "bar == id foo_nat" (* use unoverloaded constant *)
term bar (* prints "id foo" *)

abbreviation bar' :: "nat ⇒ nat" where "bar' == id foo" (* use overloaded constant *)
term bar' (* prints "id foo" *)

How can I make Isabelle's pretty printer contract the right-hand sides of bar or bar' (all
this should work also inside a locale).

Some background context on my use case. I have a locale l for abstracting over a
monomorphic monad in some definition d. Later, I instantiate the monad operations in
different ways using locale import or interpretation. Unfortunately, I get huge terms
mentioning the global version l.d applied to all the instantiated locale parameters rather
than just <my chosen prefix>.d.

Thanks in advance for any hints,
Andreas

Email Gateway (Aug 22 2022 at 11:04):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

this seems yet another instance of the fact that abbreviations, class
operations and adhoc-overloading in its current implementation do not
interact smoothly. It requires substantial reforms here to get these
more robust.

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 11:04):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,

On 06/08/15 11:16, Florian Haftmann wrote:

Hi Andreas,

Am 31.07.2015 um 12:16 schrieb Andreas Lochbihler:

Dear all,

I am struggling with abbreviations that involve constants which have
been registered with adhoc_overloading. My problem is that I cannot get
Isabelle's pretty-printer to fold the abbreviations again.

Below is the minimal example (for Isabelle2015).

consts foo :: "'a ⇒ 'a"
consts foo_nat :: "nat ⇒ nat"
adhoc_overloading foo foo_nat

abbreviation bar :: "nat ⇒ nat" where "bar == id foo_nat" (* use
unoverloaded constant *)
term bar (* prints "id foo" *)

abbreviation bar' :: "nat ⇒ nat" where "bar' == id foo" (* use
overloaded constant *)
term bar' (* prints "id foo" *)

How can I make Isabelle's pretty printer contract the right-hand sides
of bar or bar' (all this should work also inside a locale).

this seems yet another instance of the fact that abbreviations, class
operations and adhoc-overloading in its current implementation do not
interact smoothly.
You are probably right. If I disable adhoc-overloading for the uncheck phase using
[[show_variants]], the abbreviations are contracted again.

It requires substantial reforms here to get these more robust.
So for the time being, I have to decide between nice monad syntax and folded abbreviations.

Best,
Andreas

Last updated: Apr 20 2024 at 12:26 UTC