*To*: cl-isabelle-users at lists.cam.ac.uk, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] problem with class and sulocale declarations*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Wed, 08 Sep 2010 11:50:19 +0300*In-reply-to*: <4C873BA2.6030603@informatik.tu-muenchen.de>*References*: <4C873677.6010001@abo.fi> <4C873BA2.6030603@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2

Hi Florian, I think that I have narrowed down the problem: class sup_a = fixes sup_a :: "'a => 'a => 'a" (infixl "\<squnion>1" 65) class inf_a = fixes inf_a :: "'a => 'a => 'a" (infixl "\<sqinter>1" 65) class test = ord + times + one + sup_a + inf_a + assumes a[simp]: "a = 1" and b[simp]:"a = b" and [simp]: "a \<le> b" and [simp]: "\<not> a < b" begin end;

apply unfold_locales; by simp_all; class bounded = zero + test In this theory I get the same error for "class bounded = zero + test" I have two more unrelated questions for this example: 1. Why squnion and sqinter symbols are not defined in separate classes as most of the other symbols? This would make there reuse simpler.

assumption a should replace any element with 1. Best regards, Viorel On 9/8/2010 10:30 AM, Florian Haftmann wrote:

Hi Viorel,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 has indeed already been detected and will disappear in the next Isabelle release. For the moment an explicit type annotation should help: class bounded_some_algebra = zero + some_algebra + assumes zero_smallest: "(0::'a)<= a" Sorry for the inconvenience, Florian

**Follow-Ups**:**Re: [isabelle] problem with class and sulocale declarations***From:*Florian Haftmann

**References**:**[isabelle] problem with class and sulocale declarations***From:*Viorel Preoteasa

**Re: [isabelle] problem with class and sulocale declarations***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Congruence rule for Let
- Next by Date: Re: [isabelle] adm and fixrec’s induct rules
- Previous by Thread: Re: [isabelle] problem with class and sulocale declarations
- Next by Thread: Re: [isabelle] problem with class and sulocale declarations
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list