Email Gateway (Jan 24 2021 at 23:13): Email Gateway (Jan 24 2021 at 23:13):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I observed the following behavior on Isabelle2021-RC2:
lemma
assumes P and "a = b" and "c = d" and "e = f"
shows "R a c e"
using assms(1)
apply(subst assms(2), subst assms(3), subst assms(4))
(P ⟹ P ⟹ P ⟹ R b d f)
oops
lemma
assumes P and "a = b" and "c = d" and "e = f"
shows "R a c e"
using assms(1)
apply(rewrite assms(2), rewrite assms(3), rewrite assms(4))
(P ⟹ P ⟹ P ⟹ R b d f)
oops
As you can see, the premises are duplicated with every substitution using
either subst or rewrite from HOL-Library.Rewrite.
I am posting this as an explicit new thread, as I am not certain whether
this is desired/expected, whether it is unique to Isabelle2021-RC2 or
whether this is a regression.
If this behavior is desired/expected, how can the duplication be avoided
when designing methods using Eisbach, apart from using an additional method
to remove the duplicate premises explicitly after every invocation of
subst/rewrite?
Kind Regards,
Mikhail Chekhov
Last updated: Jan 04 2025 at 20:18 UTC