isabelle - 将类型变量定义为两个选项之一

Question

在 Isabelle/HOL 中，我们想在自然数或整数上定义多变量多项式。有没有办法写

datatype ('a::???) polynomial = ...

并指定'a应该是nat或者int？像这样的语法'a::nat|int起初看起来很直观，但不幸的是不起作用。

一种可能的替代方法是指定'a::comm_semiring（可能还添加countable），但我们并不真正需要抽象可交换半环的全部通用性。

标签： isabelle