Sophie Tourret (Oct 10 2022 at 14:36): Sophie Tourret (Oct 10 2022 at 14:36):Hello,
I am trying to show (with Isabelle2021-1) that a countable type is a linorder type (which should follow from the fact that nat is a linorder). Since both are typeclasses, I am trying to show this using the subclass relation.
However, when I type
subclass (in countable) linorder
I get the error:
Conflict of type arities for classes preorder < ord:
sum :: (countable, countable) preorder and
sum :: (finite, finite) ord
There is only one instance of sum in countable and none in linorder. I don't understand where this error message comes from. Can someone help?
MWE (in Scratch.thy):
theory Scratch
imports "HOL-Library.Library"
begin
subclass (in countable) linorder
end
Given that countable does not entail the existence of an order (syntactically, there is no <), I am not sure what you expect to happen here exactly
Mathias Fleury (Oct 11 2022 at 15:37):term "(x :: 'a :: {countable}) ≤ x"
(*
Type unification failed: Variable 'a::countable not of sort ord
*)
In slightly more words: image int are also countable, but you cannot use the same order as the one defined by default over integer. And isabelle's typeclasses to not allow two instantiations of the same operator
Mathias Fleury (Oct 11 2022 at 15:52):With the following you get at least the theorems:
context
fixes a :: "'a :: {countable}"
begin
interpretation X: linorder where
less_eq = "λ(a::'a) b. to_nat a ≤ to_nat b" and
less = "λa b. to_nat a < to_nat b"
by unfold_locales
auto
Perhaps I should add that Isabelle typeclasses work like Haskell type classes: you can only have one instance per combination of type and type class, and instances are forever and unchanging. You cannot ‘delete’ or ‘locally forget’ a type class instance. If you import two theories that each have a linorder type class for some given type, you wil get an error.
The Isabelle linorder type class does not just mean that ‘there is some linear order on this type’, but rather ‘there is one canonical linear order on this type and whenever I write ≤ this is what I mean by it’.
This is the reason why e.g. there is no order instance for lists and products by default because there are a number of reasonable orders on this, e.g. the lexicographic order and the pointwise order.
Another unrelated limitation is that if you have a type class a and a type class b which assumes the existence of some operation f (as is the case here with countable and linorder), you cannot say something like ‘Every type of class a also has an instance of type b where we instantiate f as follows.’
That last limitation could, I think, be lifted in principle. But things being as they are, it is not possible to do this. The usual workaround is to introduce an additional typeclass countable_linorder that is a superclass of both countable and ord (the syntactic type class that only assumes the existence of ≤ with no laws) and that assumes that (≤) is simply defined in the way that follows from countable. Then you can show that countable_linorder is a subclass of linorder.
You will then, however, have to explicitly demand countable_linorder in many places where you would normally only require countable, and you will have to instantiate countable_linorder for every concrete type where you want to make use of this linorder class that comes out of countability.
Last updated: Dec 21 2024 at 16:20 UTC