Re: [Isarmathlib-devel] A contribution

[Slawomir Kolodynski]

>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