# [isabelle] Calculation-style reasoning, reflexive equality, and strangeness

Tom and I have stumbled upon an interesting feature of Isabelle's
calculation style reasoning support. Consider the following proof
lemma
"X = Y"
proof -
have "X = z" sorry
also have "\<dots> = z" by simp
also (* want X = z, get X = X *)
After the 'also', calculation is "X = X", rather than
the "X = z" you would expect. We figured that the reason for
this is that the chaining rule is forw_subst
[| a = b; P b |] ==> P a
which, when unified with the above two rules gives P == %x. x = x
hence P X == X = X
I suppose this is a corner case, but it could be solved by trying trans
before forw_subst.
Simon

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