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 :-)
On 31 Mar 2009, at 08:46, Rafal Kolanski wrote:
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
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