# [isabelle] Defining operators

Hello,
I'm trying to teach myself Isabelle, and have come across something I
don't understand. I'm trying to model Jordan *-triples (e.g. the
complex numbers equipped with the ternary product {a b c} =
1/2(ab^*c+cb^*a) where ^* denotes conjugation. The triple product has
a quadratic operator associated with it defined by Q(a)b = {a b a}.
I can model the ternary multiplication as:
class triple = ab_group_add +
fixes triple :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("⦃ _ _ _ ⦄" [100,100,100] 1000)
(There are other axioms which I have omitted for simplicity as
removing them doesn't affect the outcome described below.)
I then attempt to define the quadratic operator as:
fixes Qsig :: "'a ⇒ 'a ⇒ 'a" ("Q⇩_ _ " 1000)
assumes Qdef: "Q⇩a b = ⦃ a b a ⦄"
Clearly I have introduced some rules beyond what I intended, as
Isabelle is then able to prove statements which aren't in general true
in the mathematical theory. e.g.
lemma Qop: "Q⇩u (Q⇩u (Q⇩u a)) = ⦃ u a u ⦄" by (rule local.Qdef)
is considered true. (This should require the additional assumption
that u is a tripotent i.e. ⦃ u u u ⦄ = u along with the omitted axioms
on the multiplication.)
How is Isabelle actually interpreting what I have entered, and what
should I have put?
(Sorry if this is a very basic question. I am still new to this and
finding it hard going.)
Thank you for any help you are able to offer.
Christopher Hoskin

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*