在语言环境中的实例化类
假设我有一些位置可以从假设中推断出类型类。
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
然后可以以某种方式实例化类型？
直接实例化（实例，Intantiation）在环境上下文中不起作用。 我也没有解释的运气，因为有限>没有固定常数， 因此，我无法指定要解释的类型。
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") *)
我知道我可以简单地修复XS ::“'x ::有限列表”， 这可能是我必须接受的解决方案， 但这似乎只是多余的。
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.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
目前（Isabelle2021-1）无法实例化语言环境中的类型类。但是，您可以解释语言环境中类型类的本地上下文。这使得在类型类上下文中所做的所有定理和定义都可以在此上下文之外证明的定义和定理。
如果对于您的用例还不够，那么将排序限制添加到语言环境声明是必需的。
请注意，仅当类型变量
'x的类型变量被重命名为'a，为drights命令，出于未知的原因，使用类型变量'a。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
'xin the locale is renamed to'a, as theinterpretationcommand for unknown reasons insists on using the type variable'a.