Fix 'a with typeclass · Beginner Questions

I introduce variables with fix A :: "'a set", which I later use and need 'a to have a specific typeclass. Is there a way to fix variables with the additional restriction that they are in a typeclass?

Manuel Eberl (Jun 21 2021 at 13:28):

fix A :: "`a :: myclass set"

Max Nowak (Jun 21 2021 at 13:30):

Now I get the following though:
Sort constraint linorder inconsistent with default type for type variable "'a"

Manuel Eberl (Jun 21 2021 at 13:32):

Then you already have a type 'a in your context that doesn't have that type class.

Manuel Eberl (Jun 21 2021 at 13:32):

So you probably have to annotate it with that type class even earlier.

Manuel Eberl (Jun 21 2021 at 13:33):

Come to think of it, I don't think I can think of any common situation where it would be required to add a type class annotation to a fix command.

Manuel Eberl (Jun 21 2021 at 13:33):

If you don't understand what you need to do, you should perhaps post some more context so that we can see what it is that you are attempting to do.

Max Nowak (Jun 21 2021 at 13:37):

Yeah I have a (in linorder) on my lemma, and yet it complains that 'a isn't of sort linorder.
My lemma:

lemma (in linorder): "myprop myfunc"
  unfolding myprop_def
proof (safe)
  fix A :: "'a set"
  have "..." using other_lemma[of A] (* <-- error here that A is not of sort linorder*)
qed

I hope that's enough code.

Manuel Eberl (Jun 21 2021 at 13:38):

Ah, yes, this is an oddity of the way type classes work in Isabelle. When you are in the linorder context, you do not actually have the sort linorder on the type variable 'a and there is no way to get it.

Manuel Eberl (Jun 21 2021 at 13:38):

Ideally, you should prove your other_lemma also in a linorder context (i.e. with in linorder) so that you can use it here.

Manuel Eberl (Jun 21 2021 at 13:39):

If that is not possible for some reason, you will have to prove everything that builds on it also outside the linorder context, with an explicit linorder sort annotation.