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

[Lawrence Paulson]

Thanks. It’s too late for the next release anyway, surely.

NB although HOL Light’s metric.ml has over 2000 theorems, only about 130 seem to mention metric spaces directly. Huge chunks of this file have already been ported to Analysis.

Larry

> On 18 Apr 2019, at 04:10, Fabian Immler <immler at in.tum.de> wrote:
> 
> On 4/16/2019 10:26 AM, Lawrence Paulson wrote:
>> 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.
> Such an abstract type is a useful idiom to formalize mathematical structures (there are successful applications for measure spaces, topologies, homeomorphisms).
> 
> One advantage (of such an abstract type, compared to locales) is that the projection to the distance function is a global constant. This makes it easy to use find_theorems.
> 
> I don't know if anyone has experience with the abstract type idiom for hierarchies of structures. A disadvantage might be that instead of sublocale relations, I guess one would need to work with coercions from normed vector spaces, metric spaces, topological spaces, etc.
> I don't really know what the limitations are and how well that works out in practice.
> 
> Fabian
> 
> 
>>> 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
>