[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)
"((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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and