[isabelle-dev] Abbreviations + Monad_Syntax introduce "unit itself" additional type variable

Peter Lammich lammich at in.tum.de
Thu Sep 19 12:21:05 CEST 2013

Referring to Isabelle_2013 AND Isabelle_12_Sep_2013:

In the following example, using an abbreviation that contains
monad-syntax introduces a superfluous additional itself-parameter, that,
however, is immediately instantiated to "unit itself". Note that, when
replacing abbreviation by definition, everything works as expected.

It looks like (see also my previous post) that monad-syntax has some
severe issues with abbreviations, that I would really like to see fixed
in the next release, as they render unusable many of my tools.


theory Scratch

abbreviation "abbr1 == Some () >>= (%_. Some False)"

abbreviation "abbr2 == do {
    Some ();
    Some False

(* ### Additional type variable(s) in specification of "abbr2": 'a *)

term "(abbr1, abbr2)"

"(Some () >>= (%_::unit. Some False),
  %TYPE::unit itself. Some () >>= (%_::unit. Some False))"
  :: "bool option * (unit itself => bool option)"

definition "abbr3 == do {
    Some ();
    Some False

(* No additional type parameter *)

More information about the isabelle-dev mailing list