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 a,b are nonempty lists of elements of a semigroup G (i.e. a : n \rightarrow G and b : k\rightarrow G for some positive natural numbers n,k) then we have \prod a \sqcup b = \left( \prod a \right) \cdot \left( \prod b \right).


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: