IsarMathLib version 1.6.3 released

The release happened actually more than a week ago, but it is only now that I got around to write about it.

The release brought very little of new formalized mathematics. Most of the effort went into getting the TiddlyWiki rendering work with more  IsarMathLib theories. This requires improving the Isar parser and modifying the theories  to conform to the Isar dialect that the parses assumes. As I modify the theories the Tiddly Formal Math site content diverges from the last released proof document and this release fixes that. The only significant change was the addition of a small tutorial on reading Isar formal proofs in the new Introduction.thy theory.

The IsarMathLib’s TiddlyWiki rendering got some praise on the Mizar mailing list recently.

IsarMathLib updated to Isabelle 2007

I have released version 1.6.2 of IsarMathLib . This is the first version that has been verified with Isabelle 2007. I also added a new thery file about folds in ZF set theory, presented before on this blog, and rewrote the theory file about semigroups.

new version of IsarMathLib released

I have decided to suspend the Metamath to Isabelle/ZF translation and do some native Isabelle/ZF development for a change.The next long term goal is to add integration to IsarMathLib. It seems that the integral most often formalized is the gauge integral . This is a reason good enough to try something else. Searching for alternatives I found an interesting paper “Notes on Lebesgue Integration” by Gyula Lakos on a general approach to defining the Lebesgue integral. The paper constructs an integral for functions valued in a topological groups with respect to measures valued in (possibly) another topological group.
This release is the first step towards the goal of formalizing this construction.
The material added in version 1.6.0 is mostly about finite sequences (a.k.a. lists) and operations on them: concatenation, appending an element, discarding the first or last element and folding with a binary operation. This last notion is studied in the new Semigroup_ZF.thy theory where we prove some properties of products of finite sequences of semigroup elements. The development ends in a theorem that states that if are nonempty lists of elements of a semigroup (i.e. and for some positive natural numbers ) then we have .