[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.