# [isabelle] problem with class and sulocale declarations

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] problem with class and sulocale declarations
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Wed, 08 Sep 2010 10:08:39 +0300
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2

Hello,
I have many algebraic structures developed as classes. At some point
I want a new class with additional constant zero.
class bounded_some_algebra = zero + some_algebra +
assumes zero_smallest: "0 <= a"
However, when I introduce this declaration I get the error:
*** Type unification failed
***
*** Cannot meet type constraint:
***
*** Term: times::'b => 'b => 'b :: 'b => 'b => 'b
*** Type: 'a => 'a => 'a
***
*** At command "class".
This problem occur after the sublocale declaration:

`sublocale some_algebra < lattice1!:some_lattice_b "1" "op *" "op l->"
``"op <=" "op <" "op r->" "op \<squnion>1"
`
Here both some_lattice_b and some_algebra are subclasses of a common class.

`If I introduce the class bounded_some_algebra before the sublocale, then
``it works,
`except that I get a similar problem later when using bounded_some_algebra.

`I tried to make a smaller example to show the problem, but I could not
``reproduce
`it.
Best regards,
Viorel Preoteasa

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*