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



On Tue, 14 Sep 2010, Simon Winwood wrote:

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.

The calculational system tries rules from the context in the given order (cf. print_trans_rules), and trans comes before forw_subst in the main HOL library as one would normally expect.

The reason why the intermediate reflexive step above is ignored is due to the policy to filter out results that do not make progress: composing trans with a reflexive result duplicates the original fact, so it is filtered out in the enumeration. This principle has been there in Isar calculations almost from the very beginning around 1999/2000 -- it allows more useful steps involving advanced substitution rules.


	Makarius





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