Email Gateway (Aug 18 2022 at 17:38): Email Gateway (Aug 18 2022 at 17:38):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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
Email Gateway (Aug 18 2022 at 17:38):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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:
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).
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.
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:
Email Gateway (Aug 18 2022 at 17:38):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello Viorel,
there is no direct way to enforce this. The easiest is to add a trivial
assumption which introduces the sort constraint, for example:
class test = lattices +
assumes "(a :: 'a :: order) = a"
The class command also accepts the constrains element that locales support, but
this seems to be without effect.
Andreas
Viorel Preoteasa schrieb:
Last updated: Nov 21 2024 at 12:39 UTC