The release adds about 50 facts leading to a theorem named *prod_list_of_sets* that can be informally stated as follows:

Suppose is a commutative semigroup, is a linearly ordered set, an indexed collection of elements of and a nonempty list of finite, nonempty and mutually disjoint subsets of the index set . Then we have

In words, we can multiply the elements over each index set for and multiply the results, or we can multiply all elements for and the results are the same.

The actual notation in the formal text is rather ugly and looks like this:

This is because although Isabelle allows to define notation with binders I couldn’t figure out how to use binders of the form in locales. The notation that is easy to define is to denote a product of elements of a list (in this case this list is and to denote a product of elements given by indices in set and a function .

I should probably come up with some deep motivation for proving this theorem, but the truth is, I proved it by mistake. I was planning to prove Lemma 2.2 from Lakos’s paper, but I didn’t look at it for a long time and I forgot what is says. That’s OK though as we can use *prod_list_of_sets *to show that in commutative semigroups we can multiply lists in any order, something I didn’t quite know how to approach.

These are the perils and joys of writing formalized proofs in fifteen minutes increments while setting up problems for kids to solve so that I can give them more TV time with (somewhat) clear consciousness.

### Like this:

Like Loading...

*Related*

Tags: IsarMathLib

This entry was posted on December 19, 2008 at 11:04 pm and is filed under announcements, IsarMathLib releases. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

## Leave a Reply