Email Gateway (Aug 23 2022 at 09:16): Email Gateway (Aug 23 2022 at 09:16):From: Manuel Eberl <eberlm@in.tum.de>
You should never import theories from a larger development directly.
HOL.Topological_Spaces is already part of Complex_Main, so for that you
should import Complex_Main. For HOL-Analysis.Elementary_Topology, you
should import "HOL-Analysis.Analysis".
Since the latter subsumes the former, I would recommend you just import
"HOL-Analysis.Analysis" and see if it works then.
Manuel
Email Gateway (Aug 23 2022 at 09:16):From: Wenda Li <wl302@cam.ac.uk>
Dear Christopher,
The fundamental cause of your problem is due to an extra type constraint introduced in HOL/Real_Vector_Spaces.thy (line 1322 in Isabelle2020):
text ‹Only allow \<^term>‹open› in class ‹topological_space›.›
setup ‹Sign.add_const_constraint
(\<^const_name>‹open›, SOME \<^typ>‹'a::topological_space set ⇒ bool›)›
This constraint has been inherited by HOL-Analysis.Elementary_Topology. Without this constraint, the type variable ‘a in the constant open :: "'a set ⇒ bool" is of sort open, but with this constraint it is constrained to be a topological_space. Your lower_topology is defined upon the ‘open’ class, and this class introduced the constant ‘open’ that caused this incompatibility.
I am not sure why this constraint is introduced in the first place. As long as you are willing to strengthen the typeclass ‘open’ to topological_space, the incompatibility can disappear:
class lower_topology = order + topological_space
subclass topological_space
unfolding open_generated_order
by (rule topological_space_generate_topology)
end
Hope this helps,
Wenda
Last updated: Apr 25 2024 at 12:23 UTC