Defining the Distributive Depth of an Operator

I am working on defining the relations between Bras and Kets in Mathematica, and I am using the CircleDot operator to represent multiplication. I seem to have some trouble defining how operations on expressions containing CircleDot distribute into the expression.

The behavior I am trying to achieve is:

ConjugateTranspose[2 I\[CircleDot]Bra[x]]
(* should yield -2 I \[CircleDot]Ket[x] *)


I have already defined the ConjugateTranspose of a Bra, so this already works:

ConjugateTranspose[Bra[x]]
(* already properly yields Ket[x] *)


I have tried this:

ConjugateTranspose[Times[u_, (c_ /; NumberQ[c])]\[CircleDot]Bra[x_]] ^:=


Conjugate[Times[u, (c /; NumberQ[c])]][CircleDot]Ket[x]

As per Define an operator with the distributive property, I have tried:

CircleDot /:
Simplify[CircleDot[pre___, a_ b_, mid___, Ket[x_], post___]] :=
Simplify@Apply[CircleDot,
Simplify /@ {pre, mid, Simplify[a b], Ket[x], post}]


What does seem to work is this:

ConjugateTranspose[I \[CircleDot]Bra[x]]
(* yields -I Ket[x] *)


But it doesn't seem that the ConjugateTranspose will distribute and apply to the 2 I and Bra[x] individually and I'm a bit stuck. Any help would be much appreciated! Thanks!

• Have you tried not putting Simplify[] in your rule definitions? – J. M.'s ennui Apr 17 '17 at 3:45