Re: [isabelle] using mono predicate
this is how the type error arises:
In the context order, mono has the type "'a :: type => 'b :: order => bool",
which is specified in the definition of mono in theory Orderings. The sort
constraint order on 'b is necessary such that the order operation are availabe
on the image type.
In your theorem test, you are in the locale context test, which is a sublocale
of order, i.e. mono has the polymorphic type "'a :: type => ?'b :: order =>
bool" where ?'b is free and 'a is bound.
The function f has type "'a :: type => 'a", i.e., mono's type must be
specialized such that ?'b becomes 'a. However, 'a is not known to be of sort
order, so this gives the type error.
I know of three approaches to your problem:
1. State and prove your theorem test outside the context test, but with explicit
class test = lattice
theorem test: "f x = (x::'a :: test) ==> mono f ==> f x = x"
Alternatively, you can use the sort constraint "order" instead of "test".
This approach is suitable if
- you analogously move all theorems that rely on theorem test out of the context
test and add sort constraints where necessary, and
- you never need to interpret the locale for class test in a context where 'a is
instantiated to a type which is not in class test (via the commands sublocale or
2. Change the definition of class test such that 'a has the sort constraint
order. The conditions are similar to 1., but now, everything in context test
includes the sort constraint.
3. Give up on type classes and do everything in locales. Then, you will have to
define mono yourself in a locale for order morphisms and setup proof automation
by yourself. The locale tutorial contains such an example with order
homomorphisms. If you base your order morphism locale on the locale "order" that
lives behind the type class "order", you get some automation from the type class
"order" for free, but not everything (cf.
You cannot have order morphisms as type class because they would involve
multiple type variables, which Isabelle does not support.
Hope this helps,
Viorel Preoteasa schrieb:
I have the following theory fragment:
theory test imports Main
class test = lattice
"f x = (x::'a) ==> mono f ==> f x = x"
When processing the theorem test I get the following error:
*** Type unification failed: Variable 'a::type not of sort order
The predicate mono is defined in class order and class lattice
extends the class order.
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 023
Telefon: +49 721 608-48352
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