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

Question

我正在 Isabelle/HOL 中使用 Nonstandard_Analysis 会话，我试图证明类型 'a::euclidean_semiring star 是 euclidean_semiring.[=24= 的一个实例]

我正在展示

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 是因为这个特定类型-class euclidean_semiring有一个参数，即euclidean_size.

当然，我更希望能更好地解释错误消息和建议的解决方法（如果可能），但查看证明形式

的示例也会有所帮助

  instance X :: (Y) Y

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

Answer 1

是的，如果类型 class 有参数，您必须使用 instantiation 并为它们给出定义。

    instantiation star :: (euclidean_semiring) euclidean_semiring
    begin

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

    end

您可以在库中使用 instantiation 的任何地方找到这方面的示例，例如euclidean_semiring 对 nat 的实例化。

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

Trying to prove that a type is an instance of `euclidean_semiring` (in Isabelle)

types

isabelle