[isabelle-dev] locales, groups, metric spaces?

Lawrence Paulson lp15 at cam.ac.uk
Tue Apr 16 16:26:06 CEST 2019

This doesn’t look right to me, as surely the topology is derived from the metric, rather than metric space material being adjoined to a topology.

In HOL Light, a metric space is an abstract type represented by pairs (S,d) where S is the carrier and d is the distance function. Could that be the best approach for us, or should we use a locale? But then the notion of a metric space is a property rather than a type.


> On 16 Apr 2019, at 14:08, Fabian Immler <immler at in.tum.de> wrote:
> Combining it with the anonymous relativization efforts
> https://github.com/xanonec/HOL-Types_To_Sets_Ext/blob/master/Topology/Topological_Space_OW.thy#L52
> it could look like this:
> locale topological_space_ow =
>  fixes π”˜ :: "'at set" and Ο„ :: "'at set β‡’ bool"
>  assumes open_UNIV[simp, intro]: "Ο„ π”˜"
>  assumes open_Int[intro]: "⟦ S βŠ† π”˜; T βŠ† π”˜; Ο„ S; Ο„ T ⟧ ⟹ Ο„ (S ∩ T)"
>  assumes open_Union[intro]: "⟦ K βŠ† Pow π”˜; βˆ€S∈K. Ο„ S ⟧ ⟹ Ο„ (⋃K)"
> locale metric_space_ow = topological_space_ow +
>  fixes dist:: "'at β‡’ 'at β‡’ real"
>  assumes open_dist: "S βŠ† π”˜ ⟹ Ο„ S ⟷ (βˆ€x∈S. βˆƒe>0. βˆ€y. dist y x < e ⟢ y ∈ S)"
>  assumes dist_eq_0_iff [simp]: "x ∈ π”˜ ⟹ y ∈ π”˜ ⟹ dist x y = 0 ⟷ x = y"
>    and dist_triangle2: "x ∈ π”˜ ⟹ y ∈ π”˜ ⟹ dist x y ≀ dist x z + dist y z"
> Of course, this is yet another approach and different from the "topology-as-value" approach from Abstract_Topology (http://isabelle.in.tum.de/repos/isabelle/file/538919322852/src/HOL/Analysis/Abstract_Topology.thy#l19)
> One would need to think about if or how it makes sense to combine such a "locale-only" approach with a "topology-as-value"/"metric-space-as-value" approach.  (Projecting the topology out of the metric-space value and having these as parameters of the locales?)
> Fabian

More information about the isabelle-dev mailing list