Stream: Is there code for X?

Topic: "bookkeeping" of indices in partitioned lists?

stuebinm (Feb 01 2025 at 16:50):

I'm formalising some (set-theory based) mathematics considering the cartesian product of some sets $S_1 \times ... \times S_n$ and "partitions", i.e. products of only a few of these sets whose indices are in some set $J$ & those whose are not in $J$, e.g. for $$J = {1,...,k}$

$$\underbrace{S_1 \times ... \times S_k}_A \times \underbrace{S_{k+1} \times ... \times S_n}_B$$

I have written these in isabelle as folds over 'a set list. Now I'd like to not require that $J$ contain the first $k$ integers (i.e. allow more general partitions, which'd fit nicely with the partition function on lists), but that makes it difficult to work with elements of these sets, and especially it makes it hard to talk about "merging" these partitions back into the original product, since it requires keeping track of all these indices. I've now written half a theory dealing purely with "indexed" sublists which can be seen as partitions & merged back into the original list, but that's very orthogonal to my original problem and I wonder if I'm either reinventing something or simply holding things wrong.

Mathias Fleury (Feb 01 2025 at 18:16):

Isn't that your structure basically a Map (https://isabelle.in.tum.de/library/HOL/HOL/Map.html) nat ⇀ 'a set with a finite domain?

Mathias Fleury (Feb 01 2025 at 18:16):

Here is the finite version: https://isabelle.in.tum.de/library/HOL/HOL-Probability/HOL-Library.Finite_Map.html

stuebinm (Feb 02 2025 at 10:16):

yes! thanks a lot for the hint; don't know what possessed me to not notice I was shoving a (finite) Map into lists. Good to know there's a finite map though, I'd not seen it before

Last updated: Apr 18 2025 at 20:21 UTC