Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] rewrite, subst,uses and sequential compositio...


view this post on Zulip 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: Mar 29 2024 at 12:28 UTC