[isabelle] Importing HOL.Topological_Spaces and"HOL-Analy... · Archive Mirror: Isabelle Users Mailing List

From: Christopher Hoskin <christopher.hoskin@gmail.com>
I'm trying to define and work with the Lower Topology on a partially
ordered set (Gierz et al, Definition III-1.1).

theory Scratch
  imports HOL.Lattices Main HOL.Topological_Spaces
begin

class lower_topology = order + "open" +
  assumes open_generated_order: "open = generate_topology (range (λJ.
{K. ¬J≤K}))"
begin

subclass topological_space
  unfolding open_generated_order
  by (rule topological_space_generate_topology)
end

end

However, I also want to work with the concept of a topological basis,
and add "HOL-Analysis.Elementary_Topology" to the list of imports.
This seems to break my definition of the lower topology - class,
subclass, unfolding and end are all underlined in red, and I
have the following error message:

Type unification failed: Variable 'a::lower_topology not of sort
topological_space

Failed to meet type constraint:

Term:  open :: ??'a set ⇒ bool
Type:  'a set ⇒ bool

Coercion Inference:

Local coercion insertion on the operand failed:
Variable 'a::lower_topology not of sort topological_space

Now trying to infer coercions globally.

Coercion inference failed:
failed to unify invariant arguments
Variable 'a::lower_topology not of sort topological_space

The same problem occurs if I omit importing HOL.Topological_Spaces
and just import "HOL-Analysis.Elementary_Topology".

I'm afraid it's beyond my grasp of Isabelle's type system to
understand what is happening here?

Email Gateway (Aug 23 2022 at 09:16):

Thanks for the suggestion. I get the same error if I import
"HOL-Analysis.Analysis" (plus a huge performance hit - the time it
takes Isabelle to be ready to validate my session goes from about
20sec to 8 minutes).

My approach to the lower topology is modeled on the definition of the
order_topology in the Topological_spaces.thy file.

Email Gateway (Aug 23 2022 at 09:16):

Thank you for your lucid explanation. Your solution does indeed work.
The subclass topological_space... block can then also be removed
since this is now in the definition.

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Importing HOL.Topological_Spaces and"HOL-Analy...

Email Gateway (Aug 23 2022 at 09:16):

Email Gateway (Aug 23 2022 at 09:16):

Email Gateway (Aug 23 2022 at 09:16):