## IsarMathLib 1.6.6 released

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

Suppose $G$ is a commutative semigroup, $X$ is a linearly ordered set, $\{a_x\}_{x\in X}$ an indexed collection of elements of $G$ and $M : n \rightarrow X$ a nonempty list of finite, nonempty and mutually disjoint subsets of the index set $X$. Then we have $\prod_{i=0}^{n-1} \prod_{x\in M_i} a_x = \prod_{x\in \bigcup_{i \in n} M_i} a_x$

In words, we can multiply the elements over each index set $M_i$ for $i\in n$ and multiply the results, or we can multiply all elements $a_x$ for $x\in \bigcup_{i \in n} M_i$ and the results are the same.

The actual notation in the formal text is rather ugly and looks like this: $\prod \{\langle i,\prod (M_i, a)\rangle . i \in n \} = \prod (\bigcup i\in n . M_i,a).$

This is because although Isabelle allows to define notation with binders I couldn’t figure out how to use binders of the form $\prod_{i\in A}$ in locales. The notation that is easy to define is $\prod b$ to denote a product of elements of a list $b : n \rightarrow G$ (in this case this list is $\{\langle i,\prod (M_i, a)\rangle . i \in n \}$ and $\prod (A,a)$ to denote a product of elements given by indices in set $A\subseteq X$ and a function $a: X\rightarrow G$.

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.