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.



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: