Theory Latin_Square
theory Latin_Square
imports Marriage.Marriage
begin
text ‹
This theory is about Latin Squares. A Latin Square is a $n \times n$ table filled with
integers from 1 to n where each number appears exactly once in each row and each column.
As described in "Das Buch der Beweise" a nice way to describe these squares by a $3 \times n$ matrix.
Each column of this matrix contains the index of the row r, the index of the column c and the
number in the cell (r,c). This $3 \times n$ matrix is called orthogonal array ("Zeilenmatrix").
I thought about different ways to formalize this orthogonal array, and came up with this:
As the order of the columns in the array does not matter at all and no column can be a
duplicate of another column, the orthogonal array is in fact a set of 3-tuples. Another
advantage of formalizing it as a set is that it can easily model partially filled squares.
For these 3-tuples I decided against 3-lists and against $nat \times nat \times nat$
(which is really $(nat \times nat) \times nat$) in favor of
a function from a type with three elements to nat.
Additionally I use the numbers $0$ to $n-1$ instead of $1$ to $n$ for indexing the rows and columns as
well as for filling the cells.
›