Isabelle 中集合中元素的操作
operation of elements in a set in Isabelle
最近的工作，是关于代数的semantics.I想在Isabelle中表达一个集合中元素的新运算，元素很复杂。
该运算是二元运算的扩展。并且这个二进制操作很容易通过语言环境完成。比如:a⊕b=c
locale Probjia = Prob + Prep + fixes probjiao :: "'b ⇒ 'b ⇒ 'b" (infixl "⊕" 90)
但是，我不知道如何表达集合中元素的这种操作。提示：我不知道这个集合有多少个元素。
希望，⊕A,A={a,b,c,d,……}，则⊕A = a⊕b⊕c⊕d……
谁能给我一些建议？或者我可以自己学习的一些例子。我的英文不是很好，希望表达清楚。
可以在语言环境 comm_monoid_set 中使用运算符 F 将可交换幺半群运算提升到 有限 集。您需要一个幺半群，以便空集可以表示为中性元素。我建议您查看预定义函数 sum 和 prod 是如何定义的（输入 term "sum" 并按住 Ctrl 键单击 sum 以获取定义） .在您的情况下，您可能想要声明一个子区域设置关系：
context Probjia begin
sublocale probjiao: comm_monoid_set probjiao neutral_element_for_probjiao
defines Probjiao = probjiao.F
其中 neutral_element_for_probjiao 是您操作的中性元素。完成证明后，Probjiao 就是你的运算符的提升版本。
最近的工作，是关于代数的semantics.I想在Isabelle中表达一个集合中元素的新运算，元素很复杂。 该运算是二元运算的扩展。并且这个二进制操作很容易通过语言环境完成。比如:a⊕b=c
locale Probjia = Prob + Prep + fixes probjiao :: "'b ⇒ 'b ⇒ 'b" (infixl "⊕" 90)
但是，我不知道如何表达集合中元素的这种操作。提示：我不知道这个集合有多少个元素。
希望，⊕A,A={a,b,c,d,……}，则⊕A = a⊕b⊕c⊕d……
谁能给我一些建议？或者我可以自己学习的一些例子。我的英文不是很好，希望表达清楚。
可以在语言环境 comm_monoid_set 中使用运算符 F 将可交换幺半群运算提升到 有限 集。您需要一个幺半群，以便空集可以表示为中性元素。我建议您查看预定义函数 sum 和 prod 是如何定义的（输入 term "sum" 并按住 Ctrl 键单击 sum 以获取定义） .在您的情况下，您可能想要声明一个子区域设置关系：
context Probjia begin
sublocale probjiao: comm_monoid_set probjiao neutral_element_for_probjiao
defines Probjiao = probjiao.F
其中 neutral_element_for_probjiao 是您操作的中性元素。完成证明后，Probjiao 就是你的运算符的提升版本。