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

[Fabian Immler]

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

On 4/16/2019 7:29 AM, Lawrence Paulson wrote:
> And what about metric spaces themselves? (Not that we could include very much in the next release, but still)
> Larry
> 
>> On 15 Apr 2019, at 16:31, Fabian Immler <immler at in.tum.de> wrote:
>>
>>
>> On 4/15/2019 5:57 AM, Lawrence Paulson wrote:
>>> In the context of the recent discussions about Algebra, we could revisit these issues in the context of metric spaces, which we still don’t have (except as type classes). A metric space has a carrier and a binary relation, so syntactically it’s similar to a monoid, except that we don’t expect to extend one with additional fields. So, at least, we should be able to avoid records.
>>> But what about the path from metric spaces to normed vector spaces, etc.?
>> Do you mean with explicit carrier sets and without records?
>>
>> The algebraic part could look like this [1]:
>>
>> locale semigroup_add_on_with =
>>   fixes S::"'a set" and pls::"'a⇒'a⇒'a"
>>   assumes add_assoc: "a ∈ S ⟹ b ∈ S ⟹ c ∈ S ⟹ pls (pls a b) c = pls a (pls b c)"
>>   assumes add_mem: "a ∈ S ⟹ b ∈ S ⟹ pls a b ∈ S"
>>
>> Which leads up to the notion of vector space [2]:
>> "vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_)"
>> which looks horrible here because of the explicit mention of all of the parameters (I don't recall why). Written as a locale with named parameters, it would look much nicer:
>>
>> locale vector_space_on_with = ab_group_add_on_with +
>>   fixes scl::"'f::comm_ring_1⇒_"
>>   assumes "x ∈ S ⟹ y ∈ S ⟹ scl a (pls x y) = pls (scl a x) (scl a y)"  …
>>
>> For a normed vector space, I guess one would write something like this (assuming that the parameters for the carrier set have the same name in metric_space and vector_space_on_with)
>>
>> locale normed_vector_space = metric_space + vector_space_on_with +
>>   fixes norm::"'a => real"
>>   assumes "dist x y = norm (x - y)"
>>   assumes "norm (x + y) <= norm x + norm y" ...
>>
>> Fabian
>>
>>
>> [1] http://isabelle.in.tum.de/repos/isabelle/file/538919322852/src/HOL/Types_To_Sets/Examples/Group_On_With.thy#l12
>> [2] http://isabelle.in.tum.de/repos/isabelle/file/538919322852/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy#l90
>>
>>
>>> Larry
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190416/ce1d41a9/attachment.bin>