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

[Fabian Immler]

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/20190415/c619b54a/attachment.bin>