Posts Tagged ‘IsarMathLib releases’

IsarMathLib version 1.12.1

May 12, 2020

This version updates IsarMathLib to Isabelle2020. It was the easiest update ever – nothing had to be changed, so I just changed the abstract in the proof document with the project description.

IsarMathLib version 1.12.0

May 5, 2020

This release adds three theory files contributed by Daniel de la Concepción Sáez. Two them, Topology_ZF_properties_2 and Topology_ZF_properties_3 have been in IsarMathLib for a long time, but I forgot to add them to the file that lists theories to be presented, so they were not showing up in the Isabelle generated HTML presentation or the proof document. Now they do.

The third theory TopologicalGroup_Uniformity_ZF (see also the section Topological groups – uniformity in the proof document or the outline) is brand new in this release and contains a proof that  every topological group is a uniform space.


IsarMathLib version 1.11.0

February 11, 2020

I have released the next IsarMathLib version both on the GNU Savannah server and the IsarMathLib’s repository on GitHub. This release adds a theory about unifom spaces.

IsarMathLib version 1.10.0

November 23, 2019

This release adds a short theory on neighborhood systems in topological spaces. Besides the usual places for the sources, proof document and the outline on the GNU Savannah server one can download those from the GitHub mirror.

Years ago I had a plan to formalize some notion of measure and integration that would be different and perhaps more general than the usual Borel/Lebesque measure.  I recently came back to this and searched a bit what is known about measures and integration taking values in topological groups. One of the things I found was a story about Grothendieck’s manuscript titled “L’intégration à valeurs dans un groupe topologique” that he presented to Dieudonné when he arrived to the University of Nancy to become a doctoral student there. The paper was harshly criticized by Dieudonné for its “reprehensible tendency to gratuitous generality” (I love gratuitous generality). The manuscript is now lost for ever probably.

On the measure side of things I found an old (1973) bookA Theory of Semigroup Valued Measures”  by Maurice Sion and some earlier papers on the subject. The Google preview of the book suggests that the setting considered there are topological semigroups. This notion depends on uniform spaces, which depend on neighborhood systems, hence the the subject of new theory in this release.

For the integration I found an interesting paperLattice Valuations: a Generalisation of Measure and Integral” by  Bram Westerbaan. This presents a unification of the notions of measure and integral under a common notion of lattice valuations (that would be a gratuitous generality again I guess). This is done in the setting of (partially) ordered abelian (topological) group. From my point of view I was kind of hoping that someone has come up with a way to define say SO(3) valued measures, or at least SO(2) if we really need the group to be abelian.

There is also the paper “Notes on Lebesgue integration” by Gyula Lakos that I had known before. This one is written is style that is very difficult to formalize and assumes that we already have measures.

IsarMathLib version 1.9.8 released

August 29, 2019

This new version updates IsarMathLib to Isabelle2019.

In related news, I have put the project on GitHub. I am planning to maintain IsarMathLib repositories both on the GNU Savannah and GitHub at least for some time.

IsarMathLib updated to Isabelle2016-1

March 20, 2017

I finally got around to update IsarMathLib to Isabelle2016-1 that was released in  December last year. This was a quite time consuming update. The Isabelle system integrates LaTeX to be able to typeset well looking document proofs. This indeed works well – when it does. When there is a problem though it requires  LaTeX specific knowledge or long time to fix. This is what happened this time. The Isabelle team removed an element of its LaTeX setup that was obsoleted a couple of releases ago. They provided a script that was supposed to make necessary changes to theory files, but in my case running it on IsarMathLib’s 78 theory files just caused the errors to multiply. Fortunately Isabelle distribution sources provide lots of examples how LaTeX should be currently set up. After struggling for some time to understand the errors scattered over a 10MB log file I just created the IsarMathLib LaTeX setup from scratch following the examples and it worked. The IsarMathLib’s proof document and outline look better than ever.

IsarMathLib 1.9.4 and other news

April 17, 2016

I updated IsarMathLib to work with Isabelle 2016 a couple of weeks ago. The distribution and the proof document are available in the usual places.

In other news, back in October 2015 Daniel De La Concepción, an IsarMathLib contributor, published an informal version of some of his contributions in a paper titled “New equivalences to axioms weaker than AC in topology”.


IsarMathLib 1.9.0 released

July 26, 2013

I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.

Here is a short description of what is in the new theories:


IsarMathLib 1.8.0 released

February 25, 2013

I have released the 1.8.0 version of IsarMathLib. This version works with the new Isabelle2013 (released about two weeks ago). The new material in this release mostly comes from contributions by Daniel de la Concepción Sáez, who added 5 theory files with about a hundred theorems about general topology. The subjects range from convergence of nets and filters and related continuity properties of functions, through some generalized notions of compactness and connectedness, to rather abstract (like, category theory abstract) subjects of heredity and spectra of topological properties. Unfortunately, it will take some time before those theories will be presented on the site, as my parser is not good enough to parse Daniel’s advanced Isar style.  I will work on this though and in the meantime an interested reader can have a look at the Isabelle generated full proof document or the outline.

As for myself, I have finished the proof that the function (x_0, x_1,...,x_{n-1})\mapsto \sum_{i=0}^{n-1}x_i is continuous in the natural topology on the space of n-element sequences of a topological group.

IsarMathLib 1.7.5

October 9, 2012

The 1.7.5 version of IsarMathLib has been released. The new formal math there consists of two theory files contributed by Daniel de la Concepción Sáez with over 70 theorems about various examples of topological spaces.