Suppose I have some locale where a type-class can be inferred from the assumptions.
locale some_locale =
fixes xs :: "'x list"
assumes xs_contains_UNIV: "set xs = UNIV"
begin
lemma finite_type: "OFCLASS('x, finite_class)"
proof (intro class.finite.of_class.intro class.finite.intro)
have "finite (set xs)" ..
then show "finite (UNIV :: 'x set)" unfolding xs_contains_UNIV .
qed
Can I then instantiate the type-class in some way?
Direct instantiation (instance
, instantiation
) does not work in locale contexts.
I also had no luck with interpretation
, as finite
has no fixed constants,
so I cannot specify the type I want to interpret.
interpretation finite (* subgoal: "class.finite TYPE('a)" for an arbitrary type 'a *)
proof
show "finite (UNIV :: 'x set)" (* "Failed to refine any pending goal", because of the type mismatch *) sorry
show "finite (UNIV :: 'a set)" (* would work, but impossible to prove for arbitrary type 'a *) oops
instance 'x :: finite (* not possible in locale context (Bad context for command "instance") *)
I know that I could simply fixes xs :: "'x::finite list"
,
which is probably the solution I will have to accept,
but that just seems redundant.
It's currently (Isabelle2021-1) impossible to instantiate a type class inside a locale. However, you can interpret the local context of the type class inside a locale. This makes all the theorems and definitions available that have been made inside the type class context, but not the definitions and theorems that have been proven outside of this context.
If that is not enough for your use case, then adding the sort constraint to the locale declaration is the way to go.
Note that this only works if the type variable
'x
in the locale is renamed to'a
, as theinterpretation
command for unknown reasons insists on using the type variable'a
.