Re: [isabelle] locale import
ord is a type class in the first place, not a pure locale. Hence, mixfix syntax
works a little differently, which interferes with parsing of the assumptions. If
ord was a standard locale that declares < and <= as notation, your declaration
> locale poset = ord +
> fixes A :: "'a set"
> assumes lt_le_not_le: "[|x : A; y : A|] ==> x < y <-> x <= y & ~ (y <= x)"
> and refl: "x : A ==> x <= x"
> and trans: "[|x : A; y : A; z : A; x <= y; y <= z|] ==> x <= z"
Trying to process this declaration in Isabelle2011-1, I get an error message
saying that 'a was not of class ord. This already give some hint about the
problem. Syntax declarations in type class contexts do not arrive at the locale,
the following post mentions this:
Hence, Isabelle does not parse the occurrences of < and <= as the locale
parameters. Instead, it interprets them as the overloaded "constants" less and
less_eq. Consequently, A's type is not related to less' and less_eq's.
Experts on classes and locales (Florian, Clemens) might tell you why syntax is
I don't know any satisfactory workaround. Of course, you could force the type
variables to agree by repeating less and less_eq with type signatures in a for
clause, but that would erase all notation. Equivalently, you could refrain from
mixfix syntax and literally use less and less_eq in the assumptions. Then,
Isabelle unifies the type variables. But syntax is still not available inside
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and