[isabelle] subst not acting at all like I expected


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:

  foo :: "('a => bool) => ('a => bool) => 'a => bool" (infixr "**" 35)

lemma assoc_state:
  "((P ** Q) ** R) s = (P ** Q ** R) s"

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?


Rafal Kolanski.

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