[isabelle] Abbreviations with adhoc-overloaded constants



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




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