时间戳

首页 > 解决方案 > 试图证明一个类型是 `euclidean_semiring` 的一个实例（在 Isabelle 中）

types - 试图证明一个类型是 `euclidean_semiring` 的一个实例（在 Isabelle 中）

问题描述

我在 Isabelle/HOL 中使用 Nonstandard_Analysis 会话，我试图证明该类型'a::euclidean_semiring star是euclidean_semiring.

我正在展示

instance star ::  (euclidean_semiring) euclidean_semiring
proof (intro_classes)
  show "euclidean_size (0::'a star) = (0::nat)"

但得到以下错误

  No type arity star :: euclidean_semiring

即使只是陈述所需的目标陈述。似乎有点像第 22 条规则。euclidean_semiring指定如下

  class euclidean_semiring = semidom_modulo + 
   fixes euclidean_size :: "'a ⇒ nat"
   assumes size_0 [simp]: "euclidean_size 0 = 0"
   assumes mod_size_less: 
     "b ≠ 0 ⟹ euclidean_size (a mod b) < euclidean_size b"
   assumes size_mult_mono:
     "b ≠ 0 ⟹ euclidean_size a ≤ euclidean_size (a * b)"

我已经展示了

instance star :: (semidom_modulo) semidom_modulo

实际上我想知道这个特定示例是否给出错误的原因，即使我已经能够显示类似的东西，例如instance star :: (semiring_parity) semiring_parity因为这个特定类型类euclidean_semiring有一个参数，即euclidean_size.

当然，我最希望对错误消息进行更好的解释和建议的解决方法（如果可能的话），但查看证明形式的示例也会有所帮助

  instance X :: (Y) Y

尤其是当Y是一个带参数的类型类时，就像euclidean_semiring这样。

标签： typesisabelle

解决方案

是的，如果类型类具有必须使用的参数instantiation并为它们提供定义。

    instantiation star :: (euclidean_semiring) euclidean_semiring
    begin

    definition euclidean_size_star where
      "euclidean_size_star x = …&quot;
      
    instance proof (intro_classes)
      …
    qed

    end

您可以在使用库的任何地方找到此示例，例如forinstantiation的实例化。euclidean_semiringnat

推荐阅读