IsarMathLib version 1.6.8 released

This release is  the first version of the IsarMathLib library for the new Isabelle2009. There is a little bit of new formalized mathematics as well.

The new CommutativeSemigroup_ZF theory is another take on the subject of summing up elements of some finite subset of a semigroup. This is similar to what was done in the Semigroup theory, but this time the approach is more specific to the case when the semigroup operation is commutative and does not require a linear order on the elements that we are summing up. This formalizes the definition of \sum_A a where a: X \rightarrow G is an indexed  family of elements of the semigroup G and  A\subseteq X is some finite subset of the index set. I have  written a bit about it that previously.

I also added a couple of theorems on the notion of lifting an operation to subsets. This is just a name I came up with for the operation on subsets of X that is defined naturally by any binary operation on X. I discussed this in the “Interval arithmetic in groups – pass  2” post.


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: