伊莎贝尔集合中元素的运算

Question

在我最近的工作中，它是关于代数语义的，我想在伊莎贝尔的集合中表达元素的一种新运算，而元素是非常复杂的。此操作是二进制操作的扩展。并且这个二进制操作很容易地通过地区完成。比如:a⊕b=c

locale Probjia = Prob + Prep + fixes probjiao :: "'b ⇒ 'b ⇒ 'b" (infixl "⊕" 90)

但是，我不知道如何在一个集合中表达这个元素的操作。小贴士:我不知道这组中有多少元素。

我希望，A={a，b，c，d，.}，⊕A =a⊕b⊕c⊕d.

有人能给我一些建议吗？或者是一些我可以自己学习的例子。我的英语不是很好，希望能表达清楚。

Answer 1

利用局部中的算子F，可以将交换单半群运算提升到comm_monoid_set有限comm_monoid_set集。您需要一个单子，这样空集可以表示为中性元素。我建议您查看一下预定义函数sum和prod是如何定义的(输入term "sum"和单击sum以获得定义)。在您的示例中，您可能希望声明一个子区域设置关系：

context Probjia begin
sublocale probjiao: comm_monoid_set probjiao neutral_element_for_probjiao
  defines Probjiao = probjiao.F

其中neutral_element_for_probjiao是操作的中性元素。在您完成验证之后，Probjiao就是您的操作符的解压版本。