在语言环境上下文中实例化类型类

Question

假设我有一些可以从假设中推断出类型 class 的语言环境。

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

然后我可以用某种方式实例化类型-class吗？

直接实例化（instance、instantiation）在语言环境上下文中不起作用。我也没有运气 interpretation，因为 finite 没有固定的常量，所以我无法指定我想要解释的类型。

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") *)

我知道我可以 fixes xs :: "'x::finite list", 这可能是我必须接受的解决方案，但这似乎是多余的。

Answer 1

目前 (Isabelle2021-1) 无法在语言环境中实例化类型 class。但是，您可以在语言环境中解释 class 类型的本地上下文。这使得类型 class 上下文中的所有定理和定义都可用，但在该上下文之外证明的定义和定理不可用。

interpretation finite 
proof
  show "finite (UNIV :: 'a set)"

如果这对您的用例来说还不够，那么将排序约束添加到区域设置声明是可行的方法。

请注意，这仅在语言环境中的类型变量 'x 重命名为 'a 时有效，因为 interpretation 命令出于未知原因坚持使用类型变量 'a.

在语言环境上下文中实例化类型类

Instantiate type classes in locale contexts

typeclass

isabelle

isar

在语言环境上下文中实例化类型 类

Instantiate type classes in locale contexts

typeclass

isabelle

isar

在语言环境上下文中实例化类型类