Re: [isabelle] problem with class and sulocale declarations



 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;

sublocale test < testlattice!: lattice "op \<le>" "op <" "op \<sqinter>1" "op \<squnion>1";
  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.

2. Why the proof for the above sublocale fails if I remove assumption b from test?
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







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