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

I am using the Nonstandard_Analysis session in Isabelle/HOL, and I am trying to prove that the type 'a::euclidean_semiring star is an instance of euclidean_semiring.

I am showing

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

but get the following error

  No type arity star :: euclidean_semiring

even when just stating the required goal statements. Seems like a bit of a catch-22. euclidean_semiring is specified as follows

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

and I have already shown

instance star :: (semidom_modulo) semidom_modulo

Actually I am wondering if the reason this particular example is giving an error, even though I have been able to show similar things such as instance star :: (semiring_parity) semiring_parity is because this particular type-class euclidean_semiring has a parameter, namely euclidean_size.

Of course, I would most prefer a better explanation of the error message and a suggested workaround (if possible), but it would also be helpful to see examples of proving things of the form

  instance X :: (Y) Y

especially when Y is a type-class which takes a parameter, just as euclidean_semiring does.

Solution

Yes, if the type class has parameters you have to do use instantiation and give definitions for them.

    instantiation star :: (euclidean_semiring) euclidean_semiring
    begin

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

    end

You can find examples for this anywhere in the library where instantiation is used, e.g. the instantiation of euclidean_semiring for nat.