伊莎贝尔有加法版的"Power.thy"吗？

Question

在 Isabelle 中，我定义了一个函数 f:'a -> nat，其中 'a 是一些扩展幺半群的代数结构（即群、半环、环、积分域、域...） .

我想在其他构造中将此函数的输出用作我的类型 'a 的 "coefficients"。也就是说，如果 x:'a 和 n:nat，我希望能够使用一些操作 ·:'a -> nat -> 'a 让我告诉伊莎贝尔 n·x = x + x + ... + x。

通过搜索，我找到了我想要的“Power.thy" theory and, in a sense, it does what I want. However, it does it for the "multiplicative version" of my problem. This is an issue if I want to change 'a for e.g. the integers. Using it would mean that instead of computing n·x, Isabelle would do x^n. Is there an analogous version to "Power.thy”？或者还有其他方法可以规避这个问题吗？

Answer 1

我不知道有任何预定义常量可以实现这样的操作，但可以通过迭代加法轻松实现，例如，在 nat:

上使用 comppow

definition scale :: "nat => 'a => 'a" where
  "scale a n = ((plus a) ^^ n) 0"

其中plus指的是你的结构的加法运算，0是中性元素。如果您正在使用来自 Isabelle/HOL 的算术类型 classes，您应该将排序约束 'a :: monoid 添加到 scale 的类型。

Complex_Main中还有一个class操作scaleR实现了这样的系数缩放操作，但是它允许real个数，不仅[=12] =]s，因此您的结构可能无法满足所有必需的公理（类型 class real_vector）。

Answer 2

一个非常惯用的表达方式是乘法和 »of_nat«:

context semiring_1
begin

definition scale :: "nat ⇒ 'a ⇒ 'a"
  where "scale n = times (of_nat n)"

lemma [simp]:
  "scale 0 a = 0"
  "scale (Suc n) a = a + scale n a"
  by (simp_all add: scale_def algebra_simps)

lemma
  "((plus a) ^^ n) 0 = scale n a"
  by (induct n) (simp_all)

end

伊莎贝尔有加法版的"Power.thy"吗？

Is there an additive version of "Power.thy" in Isabelle?

theorem-proving

isabelle