# Re: [isabelle] Defining operators

Thanks. After experimenting a bit more I found I could move the definition of the quadratic operator to the body of the class as:
definition quad :: "'a ⇒ ('a ⇒ 'a)" ("Q _ " [100] 900) where "(Q a) b = ⦃ a b a ⦄"
(A more standard notation would be Q(a)b rather than (Q a) b, but this caused a Type unification error.)
Isabelle can then correctly prove:
lemma cube1:
assumes "tripotent u"
shows "( Q(u) ∘ Q(u) ∘ Q(u) ) a = (Q u) a"
However, what I'd then like to conclude is:
lemma cube2:
assumes "tripotent u"
shows "Q(u) ∘ Q(u) ∘ Q(u) = Q(u)"
which I was hoping would be an immediate consequence of fun_eq_iff from HOL.thy, but it seems not?
Thanks for any pointers you can give.
Christopher

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