Re: [isabelle] locale import

Hi Christian,

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 would work.

> 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 not imported.

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 the context.

Best regards,

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
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 MHonArc.