Re: [isabelle] Calculation-style reasoning, reflexive equality, and strangeness
On Tue, 14 Sep 2010, Simon Winwood wrote:
Consider the following proof
"X = Y"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and