In my recent work，it is about algebraic semantics.I want to expression an new operation of elements in a set in Isabelle, and the elements is very complex. This operation is an extension of the binary operation. and this binary operation have finished by locale easily. such as :a⊕b=c
locale Probjia = Prob + Prep + fixes probjiao :: "'b ⇒ 'b ⇒ 'b" (infixl "⊕" 90)
BUT,i do not know how to expression this operation of elements in a set. Tips: i do not know how many elements in this set.
I hope, ⊕A, A={a,b,c,d,......}, then ⊕A = a⊕b⊕c⊕d......
Can anyone give me some advises ? or some example i can learn by myself. My English is not very good, hope to express clearly.
A commutative monoid operation can be lifted to finite sets using the operator F in the locale comm_monoid_set. You need a monoid such that the empty set can be represented as the neutral element. I recommend that you have a look how the pre-defined functions sum and prod are defined (enter term "sum" and and Ctrl-Click on sum to get to the definition). In your case, you probably want to declare a sublocale relationship:
context Probjia begin
sublocale probjiao: comm_monoid_set probjiao neutral_element_for_probjiao
defines Probjiao = probjiao.F
where neutral_element_for_probjiao is the neutral element for your operation. After you've finished the proof, Probjiao then is the lifted version of your operator.