Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] problem with class and sulocale declarations

view this post on Zulip Email Gateway (Aug 18 2022 at 16:02):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 16:02):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,

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
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:02):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hi Florian,

Your suggested solution is the first thing that I tried myself, however
it did not help.
The problem occurs also for:

class bounded_some_algebra = zero + some_algebra

without assumptions.

Best regards,

Viorel

view this post on Zulip Email Gateway (Aug 18 2022 at 16:02):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 16:02):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,

sorry for that problem. Its technical source is rather obscure (c.f.
http://isabelle.in.tum.de/repos/isabelle/rev/95a41e6ef5a8). Until the
next Isabelle release however we somehow have to live with it. Since an
explicit annotation fails in your example, I would suggest an auxiliary
class with zero and one:

class sup_a =
fixes sup_a :: "'a => 'a => 'a" (infixl "⊔1" 65)

class inf_a =
fixes inf_a :: "'a => 'a => 'a" (infixl "⊓1" 65)

class test = ord + times + one + sup_a + inf_a +
assumes a[simp]: "a = 1"
and b[simp]:"a = b"
and [simp]: "a ≤ b"
and [simp]: "¬ a < b"
begin
end

sublocale test < testlattice!: lattice "op ≤" "op <" "op ⊓1" "op ⊔1"
apply unfold_locales
by simp_all

class zero_one = zero + one

class bounded = zero_one + test

The obscure problem is likely to occur if classes are combined with
different parameters which are not mentioned in the body of the class
declaration, e.g. by assume.

  1. Why squnion and sqinter symbols are not defined in separate classes
    as most of the other symbols? This would make there reuse simpler.

The point is that inf and sup carry no syntax by default, so you are
free to use squnion and sqinter in syntax as you like; only by importing
Lattice_Syntax from the library this gets attached to inf and sup.

  1. Why the proof for the above sublocale fails if I remove assumption b
    from test?
    assumption a should replace any element with 1.

a is not applied by the simplifier since it would loop: "a = 1 = 1 = 1 =
...". You can apply it manually e.g. using apply (subst a).

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:03):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hi Florian,

sublocale test< testlattice!: lattice "op ≤" "op<" "op ⊓1" "op ⊔1"
apply unfold_locales
by simp_all

class zero_one = zero + one

class bounded = zero_one + test
The obscure problem is likely to occur if classes are combined with
different parameters which are not mentioned in the body of the class
declaration, e.g. by assume.
I managed to go forward using bot instead of zero. This is a good
solution for me.

  1. Why the proof for the above sublocale fails if I remove assumption b
    from test?
    assumption a should replace any element with 1.
    a is not applied by the simplifier since it would loop: "a = 1 = 1 = 1 =
    ...". You can apply it manually e.g. using apply (subst a).
    I tried apply (subst a), but when using on "x = y" it only replace x to
    1, and
    I did not know how to replace y with 1. The second application of subst will
    change again 1 to 1.

Best regards,

Viorel

view this post on Zulip Email Gateway (Aug 18 2022 at 16:03):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
apply (subst (1) a)
apply (subst (2) a)

Hope this helps,
Florian
signature.asc

Last updated: Apr 26 2024 at 08:19 UTC