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:


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.