Re: [Isarmathlib-devel] A contribution

[daniel]

>One thing that I don't like in your metric space development is that you use the real1 locale.

You're right about using the real1 context, I already started to change it to an ordered field.
If one changes the real numbers with an ordered field, then we get a topology also.
An examples is the rational numbers with the ecludian metric which take values in the rational numbers.

Note that a non trivial ordered field has zero characteristic, hence contains a copy of the rational numbers (Q).
Now consider the following $\<Union>{Ball S x d q. <x,q>\<in>SxQ \<and> q<r}$ with r a real number.
The the union gives the following set $Ball S x d r$ which is  a ball with real radius. So the topology
is the same with any ordered field.

>Another  thing you might want to consider is (not) putting assumptions in definitions.

I put those assumptions so that the definition has meaning. It makes you unable to use
the definition rule unless you are in an appropiate situation. For example, consider the topology
of base $U$. It is imposible to say nothing about it if $U$ doesn't satisfy the base condition,
because it doesn't exist. Or consider the partition topology, if you have a base $B$ which
isn't a partition, the partition topology $PTopology X B$ definition rule can be used but is
a partition topology only in name (this last one is a perfect example of what I called "meaning").

>The definition of metric is a good example.

This two examples I described have nothing to do about what you dicussed about a metric on an ordered field,
because you're right, it has a lot of mathematical meaning. For example to build the real numbers as the complete metric space obtain from the rational numbers, you cannot define a metric which take values in
the real numbers; but in an ordered field (usually $Q$ itself).

Either way, if you consider it best, I'll remove those conditions of
the definitions. As I said  it makes no difference in the results.

Daniel

>the case of the partitions

Partitions_ZF theory contains some as-hoc tools that were needed for some particular proof. If some other definitions suite you better, go ahead.

> in the context real0 and real1 there is mistake
Good catch, thanks.

One thing that I don't like in your metric space development is that you use the real1 locale. This locale is used for the construction of a particular model or real numbers. The construction allows to claim that there exist quadruplets of sets that satisfy the predicate IsAmodelOfReals(K,A,M,r). However, there is no reason to restrict the definition of metric to this particular model of reals. I would prefer the approach where we put an assumption in a locale that IsAmodelOfReals(K,A,M,r) and that is your set of real numbers, without any specifics. This is how it is done Complex_ZF.thy's locale complex0.
Another  thing you might want to consider is (not) putting assumptions in definitions. To be honest I didn't know this is even possible in Isabelle. I see one good reason to do it: standard mathematicians do it. Every definition in standard math starts with some assumptions that set the context for which this definitions is intended to be used. However, not having the premises in definitions allows more flexibility in the contexts you can use it. The definition of metric is a good example. It would be interesting to see how far one can go assuming that metrics are valued in an ordered field (without assuming the least upper bound property that would make it a model of reals). If you move your assumptions to theorems (from definitions) you can show exactly what you can prove without the least upper bound property and where this property plays a role.

Please treat the above as my opinions only. The rule number one is that who does the work decides how it should be done.

Slawekk


--- On Sat, 9/8/12, daniel <address@hidden> wrote:

From: daniel <address@hidden>
Subject: Re: [Isarmathlib-devel] A contribution
To: address@hidden
Date: Saturday, September 8, 2012, 3:23 AM

I did some more work. From now on, the web page you should check for my
files is just:

https://belenus.unirioja.es/~daconcep/

The real numbers are not so easy to work with, the metric spaces need some rewriting.

In the case of the partitions, I tried to work with the existing definition, but my skills
with this kind of functions is very limited. I'm used to HOL.

By the way, in the context real0 and real1 there is mistake (copy-paste, I guess). The "minus" for reals and integers have the same name for their definition rule (rminus_def). I guess on the integers was supposed to be
"iminus_def".

Daniel

>Is there any particular topology that may be useful to include for future work?

Metric spaces would be interesting. Historically, the equivalence of Heine and Cauchy definitions of convergence was one of first things that were noticed (by Sierpinski) to be dependent on the Axiom of Choice. But I think it's best to write about things that interest you, or the background for them if that is too far off.

Slawekk

---

From: daniel <address@hidden>
To: address@hidden
Sent: Thursday, September 6, 2012 4:18 PM
Subject: Re: [Isarmathlib-devel] A contribution

I'll write more informal text and try to change the style. I'll keep the html document updated.
Is there any particular topology that may be useful to include for future work?

Daniel

_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel

-----Inline Attachment Follows-----

_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel

_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel