[isabelle] Simplifier weakness in some object logics

[Cezary Kaliszyk]

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

[Tobias Nipkow]

Post by Cezary Kaliszyk
Dear all,
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

Post by Cezary Kaliszyk
Regards,
Cezary