# Re: [isabelle] subst not acting at all like I expected

`The problem is that your expectations are incorrect. If we show the
``full bracketing, you are starting with the expression
`
((C ** (B ** A)) ** D)
and the result of applying your substitution should be
(C ** ((B ** A) ** D)).
Isabelle gives you precisely this. You were expecting to see
(C ** (B ** (A ** D))),
which requires a further application of your equality.

`This sort of thing is not trivial to work out in your head. I had to
``write it down. That is why we prefer to leave it to computers :-)
`
Larry Paulson
On 31 Mar 2009, at 08:46, Rafal Kolanski wrote:

Gentlemen,

`While trying to figure out a way to do a step of a more complex
``tactic, I came across subst doing something unexpected to me.
``Given a right-associative operator and an associativity property
``about it:
`
consts
foo :: "('a => bool) => ('a => bool) => 'a => bool" (infixr "**" 35)
lemma assoc_state:
"((P ** Q) ** R) s = (P ** Q ** R) s"
sorry
When I try to use it for a specific rewrite:
lemma "((C ** B ** A) ** D) s"
apply (subst assoc_state[where P=C and Q="B ** A" and R=D])
I get: "(C ** (B ** A) ** D) s"
whereas I expect "(C ** B ** A ** D) s"
Does anyone know why this is the case?
Sincerely,
Rafal Kolanski.

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