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.