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

[Fabian Immler]

On April 16, 2019 10:26:06 AM EDT, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>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.
Right, that is just how things are set up for type classes, such that they share the same "open" constant. Here it probably makes more sense to define an open predictate and issue a sublocale command.

Fabian

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