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.