Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simplifier weakness in some object logics

Email Gateway (Aug 22 2022 at 18:41):

From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear all,

Consider the following lemma:

lemma "(⋀B. X1 = B) ⟹ X1 = X2"
by simp

In HOL it works, but for example in ZF it does not work. The simp
trace says that it works if the premise is added to the rewrite rules,
which happens in HOL but does not happen in ZF. What controls whether
premises are added as rewrite rules by rhe simplifier in object
logics? How to get similar behavior as in HOL for this lemma?

Regards,
Cezary

Email Gateway (Aug 22 2022 at 18:41):

From: Tobias Nipkow <nipkow@in.tum.de>
On 27/10/2018 11:52, Cezary Kaliszyk wrote:

Dear all,

Consider the following lemma:

lemma "(⋀B. X1 = B) ⟹ X1 = X2"
by simp

In HOL it works, but for example in ZF it does not work. The simp
trace says that it works if the premise is added to the rewrite rules,
which happens in HOL but does not happen in ZF. What controls whether
premises are added as rewrite rules by rhe simplifier in object
logics? How to get similar behavior as in HOL for this lemma?

I am afraid you have to look at the source code to figure out why it works for
HOL and not ZF. The key file for HOL should be Tools/simpdata.ML. It probably
does something the corresponding file for ZF does not do.

Tobias

Regards,
Cezary

smime.p7s

Last updated: Apr 26 2024 at 20:16 UTC