Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 23 2022 at 09:16):

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).

The following works:

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?

Thanks for any suggestions,

Christopher

view this post on Zulip Email Gateway (Aug 23 2022 at 09:16):

From: Christopher Hoskin <christopher.hoskin@gmail.com>
Dear Manuel,

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.

Christopher

view this post on Zulip Email Gateway (Aug 23 2022 at 09:16):

From: Christopher Hoskin <christopher.hoskin@gmail.com>
Dear Wenda,

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.

Best wishes,

Christopher

Last updated: Apr 26 2024 at 08:19 UTC