Email Gateway (Aug 22 2022 at 18:48): Email Gateway (Aug 22 2022 at 18:48):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear list,
Consider the following HOL lemma:
lemma "a ⟹ a ⟶ b ⟹ b" by simp
It is accepted by Isabelle in a plain HOL-Main environment.
However if I import Number Theory _and_ Eisbach, it is no longer accepted.
If I import just one of these (either only Main+Eisbach or
HOL-Number_Theory") it is ok.
A minimal problematic theory is attached.
Is it possible to have this lemma accepted?
Regards,
Cezary
(The attached file is loaded with 'isabelle jedit -l HOL-Number_Theory
issue.thy')
issue.thy
Email Gateway (Aug 22 2022 at 18:52):From: Makarius <makarius@sketis.net>
The word "inconsistency" usually means a breakdown of the logic, but
this is merely a proof tool failure.
theory issue
imports
Main
"HOL-Eisbach.Eisbach"
"HOL-Number_Theory.Totient"
begin
lemma "a ⟹ a ⟶ b ⟹ b"
by simp
end
This works if you import "HOL-Eisbach.Eisbach" last: this theory is an
extension of Pure (not Main), and thus provokes unclear situations about
merge of tool contexts. Here the problem is probably due to the
"solvers" for the Simplifier in Pure vs. HOL.
Ultimately it is a left-over maintenance problem: Eisbach needs some
further cleanup, such that it can be incorporated into Pure, and no
longer needs to extend Pure.
Makarius
Email Gateway (Aug 22 2022 at 18:57):From: Peter Lammich <lammich@in.tum.de>
Anyway, its strange that a theory that lives in a session named HOL-... is
based on Pure, and causes problems if actually used with HOL?
Why not simply base Eisbach.thy on HOL? It could be a stub that just does
imports Main Eisbach_Pure
Are there reasons why this wouldn't work?
Peter
Email Gateway (Aug 22 2022 at 18:58):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Thanks: Indeed reordering the imports also works in our more complicated cases.
Regards,
Cezary
Last updated: Apr 20 2024 at 01:05 UTC