Email Gateway (Aug 18 2022 at 16:05): Email Gateway (Aug 18 2022 at 16:05):From: Simon Winwood <sjw@cse.unsw.edu.au>
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
Email Gateway (Aug 18 2022 at 16:05):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 24 2024 at 20:16 UTC