# Re: [isabelle] using mono predicate

Dear Viorel,
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
``sort constraints:
`
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
``interpretation).
`

`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.
``https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00132.html).
``You cannot have order morphisms as type class because they would involve
``multiple type variables, which Isabelle does not support.
`
Hope this helps,
Andreas
Viorel Preoteasa schrieb:

Hello,
I have the following theory fragment:
theory test imports Main
begin
class test = lattice
begin
theorem test:
"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.
Best regards,
Viorel Preoteasa

--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`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.*