Theory Latin_Square

(*  Title:       Latin Squares
    Author:      Alexander Bentkamp <bentkamp at gmail.com>, 2015
    Maintainer:  Alexander Bentkamp <bentkamp at gmail.com>
*)

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.
›

datatype latin_type = Row | Col | Num

text‹latin\_type is of sort enum, needed for "value" command›
instantiation latin_type :: enum
begin
  definition "enum_latin_type == [Row, Col, Num]"
  definition "enum_all_latin_type (P:: latin_type  bool) = (P Row  P Col  P Num)"
  definition "enum_ex_latin_type (P:: latin_type  bool) = (x. P x)"

instance
  apply standard
     apply (auto simp add: enum_latin_type_def enum_all_latin_type_def enum_ex_latin_type_def)
   apply (case_tac x,auto)
by (metis latin_type.exhaust)

end


text‹Given a latin\_type t, you might want to reference the other two.
   These are "next t" and "next (next t)":›
definition [simp]:"next t  (case t of Row  Col | Col  Num | Num  Row)"

lemma all_types_next_eqiv:"(t. P (next t))  (t. P t)"
  apply (rule iffI)
   using next_def latin_type.case latin_type.exhaust apply metis
  apply metis
done

text ‹We call a column of the orthogonal array a latin\_entry:›
type_synonym latin_entry = "latin_type  nat"

text ‹This function removes one element of the 3-tupel and returns the other two as a pair:›
definition without :: "latin_type  latin_entry  nat × nat" where
[simp]:"without t  λe. (e (next t), e (next (next t)))"

value "without Row (λt. case t of Row  0 | Col  1 | Num  2)" ― ‹returns (1,2)›

abbreviation "row_col  without Num" text ‹returns row and column of a latin\_entry as a pair.›
abbreviation "col_num  without Row" text ‹returns column and number of a latin\_entry as a pair.›
abbreviation "num_row  without Col" text ‹returns number and row of a latin\_entry as a pair.›

text‹A partial latin square is a square that contains each number at most once in each row and each
   column, but not all cells have to be filled. Equivalently we can say that any two rows of the
   orthogonal array contain each pair of two numbers at most once. This can be expressed using the
   inj\_on predicate:›
definition partial_latin_square :: "latin_entry set  nat  bool" where
"partial_latin_square s n 
  (t. inj_on (without t) s)  ― ‹numbers are unique in each column (t=Row), numbers are unique in each row (t=Col), rows-column combinations are specified unambiguously (t=Num)›
  (es. t. e t < n) ― ‹all numbers, column indices and row indices are <n›"

value "partial_latin_square {
  (λt. case t of Row  0 | Col  1 | Num  0),
  (λt. case t of Row  1 | Col  0 | Num  1)
} 2" ― ‹True›

value "partial_latin_square {
  (λt. case t of Row  0 | Col  0 | Num  1),
  (λt. case t of Row  1 | Col  0 | Num  1)
} 2" ― ‹False, because 1 appears twice in column 0›

text ‹Looking at the orthogonal array a latin square is given iff any two rows of the
   orthogonal array contain each pair of two numbers at exactly once:›
definition latin_square :: "latin_entry set  nat  bool" where
"latin_square s n 
  (t. bij_betw (without t) s ({0..<n}×{0..<n}))" (* numbers exactly once in each column (t=Row), numbers exactly once in each row (t=Col), rows-column combinations are specified exactly once (t=Num) *)

value "latin_square {
  (λt. case t of Row  0 | Col  0 | Num  1),  (λt. case t of Row  0 | Col  1 | Num  0),
  (λt. case t of Row  1 | Col  0 | Num  0),  (λt. case t of Row  1 | Col  1 | Num  1)
} 2" ― ‹True›

value "latin_square {
  (λt. case t of Row  0 | Col  0 | Num  1),  (λt. case t of Row  0 | Col  1 | Num  0),
  (λt. case t of Row  1 | Col  0 | Num  0),  (λt. case t of Row  1 | Col  1 | Num  0)
} 2" ― ‹False, because 0 appears twice in Col 1 and twice in Row 1›

text ‹A latin rectangle is a partial latin square in which the first m rows are filled and the following
   rows are empty:›
definition latin_rect :: "latin_entry set  nat  nat  bool" where
"latin_rect s m n 
  m  n 
  partial_latin_square s n 
  bij_betw row_col s ({0..<m}×{0..<n}) 
  bij_betw num_row s ({0..<n}×{0..<m})"

value "latin_rect {
  (λt. case t of Row  0 | Col  0 | Num  1),  (λt. case t of Row  0 | Col  1 | Num  0)
} 1 2" ― ‹True›

value "latin_rect {
  (λt. case t of Row  0 | Col  0 | Num  1),  (λt. case t of Row  0 | Col  1 | Num  0),
  (λt. case t of Row  1 | Col  0 | Num  0),  (λt. case t of Row  1 | Col  1 | Num  1)
} 1 2" ― ‹False›

text ‹There is another equivalent description of latin rectangles, which is easier to prove:›
lemma latin_rect_iff:
"mn  partial_latin_square s n  card s = n*m  (es. e Row < m)  latin_rect s m n"
proof (rule iffI)
  assume prems:"mn  partial_latin_square s n  card s = n * m  (es. e Row < m)"

  have bij1:"bij_betw row_col s ({0..<m}×{0..<n})" using prems
  proof
    have "inj_on row_col s" using prems partial_latin_square_def by blast
    moreover have "{0..<m} × {0..<n} = row_col ` s"
    proof-
      have "row_col ` s  {0..<m} × {0..<n}" using prems partial_latin_square_def by auto
      moreover have "card (row_col ` s) = card ({0..<m} × {0..<n})" using prems card_image[OF inj_on row_col s] by auto
      ultimately show "{0..<m} × {0..<n} = row_col ` s" using card_subset_eq[of "{0..<m} × {0..<n}" "row_col ` s"] by auto
    qed
    ultimately show ?thesis unfolding bij_betw_def by auto
  qed

  have bij2:"bij_betw num_row s ({0..<n}×{0..<m})" using prems
  proof
    have "inj_on num_row s" using prems partial_latin_square_def by blast
    moreover have "{0..<n} × {0..<m} = num_row ` s"
    proof-
      have "num_row ` s  {0..<n} × {0..<m}" using prems partial_latin_square_def by auto
      moreover have "card (num_row ` s) = card ({0..<n} × {0..<m})" using prems card_image[OF inj_on num_row s] by auto
      ultimately show "{0..<n} × {0..<m} = num_row ` s" using card_subset_eq[of "{0..<n} × {0..<m}" "num_row ` s"] by auto
    qed
    ultimately show ?thesis unfolding bij_betw_def by auto
  qed

  from prems bij1 bij2 show "latin_rect s m n" unfolding latin_rect_def by auto
next
  assume prems:"latin_rect s m n"
  have "mn" "partial_latin_square s n" using latin_rect_def prems by auto
  moreover have "card s = m * n"
  proof -
    have "bij_betw row_col s ({0..<m} × {0..<n})" using latin_rect_def prems by auto
    then show ?thesis using bij_betw_same_card[of row_col s "{0..<m} × {0..<n}"] by auto
  qed
  moreover have "es. e Row < m" using latin_rect_def prems using atLeast0LessThan bij_betwE by fastforce
  ultimately show "mn  partial_latin_square s n  card s = n * m  (es. e Row < m)" by auto
qed

text ‹A square is a latin square iff it is a partial latin square with all $n^2$ cells filled:›
lemma partial_latin_square_full:
"partial_latin_square s n  card s = n*n  latin_square s n"
proof (rule iffI)
  assume prem: "partial_latin_square s n  card s = n * n"
  have "t. (without t) ` s  {0..<n} × {0..<n}"
  proof
    fix t show "(without t) ` s  {0..<n} × {0..<n}" using partial_latin_square_def next_def atLeast0LessThan prem by (cases t) auto
  qed
  then show "partial_latin_square s n  card s = n * n  latin_square s n"
    unfolding latin_square_def using partial_latin_square_def
    by (metis bij_betw_def card_atLeastLessThan card_cartesian_product card_image card_subset_eq diff_zero finite_SigmaI finite_atLeastLessThan)
next
  assume prem:"latin_square s n"
  then have "bij_betw row_col s ({0..<n} × {0..<n})" using latin_square_def by blast
  moreover have "partial_latin_square s n"
  proof -
    have "t. es. (without t) e  ({0..<n}×{0..<n})" using prem latin_square_def bij_betwE by metis
    then have 1:"es.t. e t < n" using latin_square_def all_types_next_eqiv[of "λt. es. e t < n"] bij_betwE by auto
    have 2:"(t. inj_on (without t) s)" using prem bij_betw_def latin_square_def by auto
    from 1 2 show ?thesis using partial_latin_square_def by auto
  qed
  ultimately show "partial_latin_square s n  card s = n*n" by (auto simp add:  bij_betw_same_card)
qed

text ‹Now we prove Lemma 1 from chapter 27 in "Das Buch der Beweise". But first some lemmas, that prove
   very intuitive facts:›

lemma bij_restrict:
assumes "bij_betw f A B" "aA. P a  Q (f a)"
shows "bij_betw f {aA. P a} {bB. Q b}"
proof -
  have inj: "inj_on f {aA. P a}" using assms bij_betw_def by (metis (mono_tags, lifting) inj_onD inj_onI mem_Collect_eq)
  have surj1: "f ` {aA. P a}  {bB. Q b}" using assms(1) assms(2) bij_betwE by blast
  have surj2: "{bB. Q b}  f ` {aA. P a}"
  proof
    fix b
    assume "b  {b  B. Q b}"
    then obtain a where "f a = b" "aA" using assms(1) bij_betw_inv_into_right bij_betwE bij_betw_inv_into mem_Collect_eq by (metis (no_types, lifting))
    then show "b  f ` {aA. P a}" using b  {b  B. Q b} assms(2) by blast
  qed
  with inj surj1 surj2 show ?thesis using bij_betw_imageI by fastforce
qed

lemma cartesian_product_margin1:
assumes "aA"
shows "{pA×B. fst p = a} = {a}×B"
using SigmaI assms by auto

lemma cartesian_product_margin2:
assumes "bB"
shows "{pA×B. snd p = b} = A×{b}"
using SigmaI assms by auto

text ‹The union of sets containing at most k elements each cannot contain more elements than
   the number of sets times k:›
lemma limited_family_union: "finite B  PB. card P  k  card (B)  card B * k"
proof (induction B rule:finite_induct)
  case empty
  then show ?case by auto
next
  case (insert P B)
  have "card ((insert P B))  card P + card (B)" by (simp add: card_Un_le)
  then have "card ((insert P B))  card P + card B * k" using insert by auto
  then show ?case using insert by simp
qed

text ‹If f hits each element at most k times, the domain of f can only be k times bigger than the
   image of f:›
lemma limited_preimages:
assumes "x  f ` D. card ((f -` {x})D)  k" "finite D"
shows "card D  card (f ` D) * k "
proof -
  let ?preimages = "(λx. (f -` {x})D) ` (f ` D)"
  have "D = ?preimages" by auto
  have "card (?preimages)  card ?preimages * k" using limited_family_union[of "?preimages" k] assms by auto
  moreover have "card (?preimages) * k  card (f ` D) * k" using card_image_le[of "f ` D" "λx. (f -` {x})D"] assms by auto
  ultimately have "card (?preimages)  card (f ` D) * k" using le_trans by blast
  then show ?thesis using D = ?preimages by metis
qed

text ‹Let $A_1, \dots, A_n$ be sets with $k>0$ elements each. Any element is only contained in at most $k$ of
   these sets. Then there are more different elements in total than sets $A_i$:›
lemma union_limited_replicates:
assumes "finite I" "iI. finite (A i)" "k>0" "iI. card (A i) = k" "iI. x(A i). card {iI. xA i}  k"
shows "card (iI. (A i))  card I" using assms
proof -
  let ?pairs = "{(i,x). iI  xA i}"

  have card_pairs: "card ?pairs = card I * k" using assms
  proof (induction I rule:finite_induct)
    case empty
    then show ?case using card_eq_0_iff by auto
  next
    case (insert i0 I)
    have "iI. x(A i). card {iI. xA i}  k"
    proof (rule ballI)+
      fix i x assume "i  I" "xA i"
      then have "card {i  insert i0 I. x  A i}  k" using insert by auto
      moreover have "finite {i  insert i0 I. x  A i}" using insert by auto
      ultimately show "card  {iI. xA i}  k" using card_mono[of "{i  insert i0 I. x  A i}" "{i  I. x  A i}"] le_trans by blast
    qed
    then have card_S: "card {(i, x). i  I  x  A i} = card I * k" using insert by auto

    have card_B: "card {(i, x). i=i0  xA i0} = k" using insert by auto

    have "{(i, x). i  insert i0 I  x  A i} = {(i, x). i  I  x  A i}  {(i, x). i=i0  xA i0}" by auto
    moreover have "{(i, x). i  I  x  A i}  {(i, x). i=i0  xA i0} = {}" using insert by auto
    moreover have "finite {(i, x). i  I  x  A i}" using insert rev_finite_subset[of "I × (A ` I)" "{(i, x). i  I  x  A i}"] by auto
    moreover have "finite {(i, x). i=i0  xA i0}" using insert card_B card.infinite neq0_conv by blast
    ultimately have "card {(i, x). i  insert i0 I  x  A i} = card {(i, x). i  I  x  A i} + card {(i, x). i=i0  xA i0}" by (simp add: card_Un_disjoint)
    with card_S card_B have "card {(i, x). i  insert i0 I  x  A i} = (card I + 1) * k" by auto
    then show ?case using insert by auto
  qed

  define f where "f ix = (case ix of (i,x)  x)" for ix :: "'a × 'b"

  have preimages_le_k: "x  f ` ?pairs. card ((f -` {x})  ?pairs)  k"
  proof
    fix x0 assume x0_def: "x0  f ` ?pairs"
    have "(f -` {x0})  ?pairs = {(i,x). iI  xA i  x=x0}" using f_def by auto
    moreover have "card {(i,x). iI  xA i  x=x0} = card {iI. x0A i}" using finite I
    proof -
      have "inj_on (λi. (i,x0)) {iI. x0A i}" by (meson Pair_inject inj_onI)
      moreover have "(λi. (i,x0)) ` {iI. x0A i} = {(i,x). iI  xA i  x=x0}" by (rule subset_antisym) blast+
      ultimately show ?thesis using card_image by fastforce
    qed
    ultimately have 1:"card ((f -` {x0})  ?pairs) = card  {iI. x0A i}" by auto

    have"i0. x0A i0  i0I" using x0_def f_def by auto
    then have "card {iI. x0A i}  k" using assms by auto
    with 1 show "card ((f -` {x0})  ?pairs)  k" by auto
  qed

  have "card ?pairs  card (f ` ?pairs) * k"
  proof -
    have "finite {(i, x). i  I  x  A i}" using assms card_pairs not_finite_existsD by fastforce
    then show ?thesis using limited_preimages[of f ?pairs k, OF preimages_le_k] by auto
  qed

  then have "card I   card (f ` ?pairs) " using card_pairs assms by auto
  moreover have "f ` ?pairs = (iI. (A i))" using f_def [abs_def] by auto
  ultimately show ?thesis using f_def by auto
qed

text ‹In a $m \times n$ latin rectangle each number appears in m columns:›
lemma latin_rect_card_col:
assumes "latin_rect s m n" "x<n"
shows "card {e Col|e. es  e Num = x} = m"
proof -
  have "card {e  s. e Num = x} = m"
  proof -
    have 1:"bij_betw num_row s ({0..<n}×{0..<m})" using assms latin_rect_def by auto
    have 2:"es. e Num = x  fst (num_row e) = x" by simp
    have "bij_betw num_row {es. e Num = x} ({x}×{0..<m})"
      using bij_restrict[OF 1 2] cartesian_product_margin1[of x "{0..<n}" " {0..<m}"] assms by auto
    then show ?thesis using card_cartesian_product by (simp add: bij_betw_same_card)
  qed
  moreover have "card {es. e Num = x} = card {e Col |e. e  s  e Num = x}"
  proof -
    have "inj_on col_num s" using assms latin_rect_def[of s m n] partial_latin_square_def[of s n] by blast
    then have "inj_on col_num {es. e Num = x}" by (metis (mono_tags, lifting) inj_onD inj_onI mem_Collect_eq)
    then have "inj_on (λe. e Col) {es. e Num = x}" unfolding inj_on_def using without_def by auto
    moreover have "(λe. e Col) ` {es. e Num = x} = {e Col |e. e  s  e Num = x}" by (rule subset_antisym) blast+
    ultimately show ?thesis using card_image by fastforce
  qed
  ultimately show ?thesis by auto
qed

text ‹In a $m \times n$ latin rectangle each column contains m numbers:›
lemma latin_rect_card_num:
assumes "latin_rect s m n" "x<n"
shows "card {e Num|e. es  e Col = x} = m"
proof -
  have "card {e  s. e Col = x} = m"
  proof -
    have 1:"bij_betw row_col s ({0..<m}×{0..<n})" using assms latin_rect_def by auto
    have 2:"es. e Col = x  snd (row_col e) = x" by simp
    have "bij_betw row_col {es. e Col = x} ({0..<m}×{x})"
      using bij_restrict[OF 1 2] cartesian_product_margin2[of x "{0..<n}" " {0..<m}"] assms by auto
    then show ?thesis using card_cartesian_product by (simp add: bij_betw_same_card)
  qed
  moreover have "card {es. e Col = x} = card {e Num |e. e  s  e Col = x}"
  proof -
    have "inj_on col_num s" using assms latin_rect_def[of s m n] partial_latin_square_def[of s n] by blast
    then have "inj_on col_num {es. e Col = x}" by (metis (mono_tags, lifting) inj_onD inj_onI mem_Collect_eq)
    then have "inj_on (λe. e Num) {es. e Col = x}" unfolding inj_on_def using without_def by auto
    moreover have "(λe. e Num) ` {es. e Col = x} = {e Num |e. e  s  e Col = x}" by (rule subset_antisym) blast+
    ultimately show ?thesis using card_image by fastforce
  qed
  ultimately show ?thesis by auto
qed

text ‹Finally we prove lemma 1 chapter 27 of "Das Buch der Beweise":›
theorem
  assumes "latin_rect s (n-m) n" "mn"
  shows "s'. ss'  latin_square s' n"
using assms
proof (induction m arbitrary:s) ― ‹induction over the number of empty rows›
  case 0
  then have "bij_betw row_col s ({0..<n} × {0..<n})" using latin_rect_def by auto
  then have "card s = n*n" by (simp add:bij_betw_same_card)
  then show ?case using partial_latin_square_full 0 latin_rect_def by auto
next
  case (Suc m)

  ― ‹We use the Hall theorem on the sets $A_j$ of numbers that do not occur in column $j$:›
  let ?not_in_column = "λj. {0..<n} - {e Num |e. es  e Col = j}"

  ― ‹Proof of the hall condition:›
  have "J{0..<n}. card J  card (jJ. ?not_in_column j)"
  proof (rule allI; rule impI)
    fix J assume J_def:"J{0..<n}"
    have "jJ. card (?not_in_column j) = Suc m"
    proof
      fix j assume j_def:"jJ"
      have "{e Num |e. es  e Col = j}  {0..<n}" using atLeastLessThan_iff Suc latin_rect_def partial_latin_square_def by auto
      moreover then have "finite {e Num |e. es  e Col = j}" using finite_subset by auto
      ultimately have "card (?not_in_column j) = card {0..<n} - card {e Num |e. e  s  e Col = j}" using card_Diff_subset[of "{e Num |e. es  e Col = j}" "{0..<n}"] by auto
      then show "card(?not_in_column j) = Suc m" using latin_rect_card_num J_def j_def Suc by auto
    qed
    moreover have "j0J. x?not_in_column j0. card {j  J. x  ?not_in_column j}  Suc m"
    proof (rule ballI; rule ballI)
      fix j0 x assume "j0  J" "x  ?not_in_column j0"
      then have "card ({0..<n} - {e Col|e. es  e Num = x}) = Suc m"
      proof -
        have "card {e Col|e. es  e Num = x} = n - Suc m" using latin_rect_card_col x  ?not_in_column j0 Suc by auto
        moreover have "{e Col|e. es  e Num = x}{0..<n}" using Suc latin_rect_def partial_latin_square_def by auto
        moreover then have "finite {e Col|e. es  e Num = x}" using finite_subset by auto
        ultimately show ?thesis using card_Diff_subset[of "{e Col|e. es  e Num = x}" "{0..<n}"] using Suc.prems by auto
      qed
      moreover have "{j  J. x  ?not_in_column j}  {0..<n} - {e Col|e. es  e Num = x}" using Diff_mono J_def using x  ?not_in_column j0 by blast
      ultimately show "card {j  J. x  ?not_in_column j}  Suc m" by (metis (no_types, lifting) card_mono finite_Diff finite_atLeastLessThan)
    qed
    moreover have "finite J" using J_def finite_subset by auto
    ultimately show "card J  card (jJ. ?not_in_column j)" using union_limited_replicates[of J ?not_in_column "Suc m"] by auto
  qed

  ― ‹The Hall theorem gives us a system of distinct representatives, which we can use to fill the next row:›
  then obtain R where R_def:"j{0..<n}. R j  ?not_in_column j  inj_on R {0..<n}" using marriage_HV[of "{0..<n}" "?not_in_column"] by blast

  define new_row where "new_row = (λj. rec_latin_type (n - Suc m) j (R j)) ` {0..<n}"
  define s' where "s' = s  new_row"

  ― ‹s' is now a latin rect with one more row:›
  have "latin_rect s' (n-m) n"
  proof -
    ― ‹We prove all four criteria specified in the lemma latinrectiff:›
    have "n-m  n" by auto
    moreover have "partial_latin_square s' n"
    proof -
      have "inj_on (without Col) s'" unfolding inj_on_def
      proof (rule ballI; rule ballI; rule impI)
        fix e1 e2 assume "e1  s'" "e2  s'" "num_row e1 = num_row e2"
        then have "e1 Num = e2 Num" "e1 Row = e2 Row" using without_def by auto
        moreover have "e1 Col = e2 Col"
        proof (cases)
          assume "e1 Row = n - Suc m"
          then have "e2 Row = n - Suc m" using without_def num_row e1 = num_row e2 by auto
          have "es. e Row < n - Suc m" using Suc latin_rect_iff by blast
          then have "e1  new_row" "e2  new_row"  using s'_def e1  s' e2  s' e1 Row = n - Suc m e2 Row = n - Suc m by auto
          then have "e1 Num = R (e1 Col)" "e2 Num = R (e2 Col)" using new_row_def by auto
          then have "R (e1 Col) = R (e2 Col)" using e1 Num = e2 Num by auto
          moreover have "e1 Col < n" "e2 Col < n" using e1  new_row e2  new_row new_row_def by auto
          ultimately show "e1 Col = e2 Col" using R_def inj_on_def by (metis (mono_tags, lifting) atLeast0LessThan lessThan_iff)
        next
          assume "e1 Row  n - Suc m"
          then have "e1s" "e2s" using new_row_def s'_def e1s' e2s' e1 Row = e2 Row by auto
          then show "e1 Col = e2 Col" using Suc latin_rect_def bij_betw_def by (metis num_row e1 = num_row e2 inj_onD)
        qed
        ultimately show "e1=e2" using latin_type.induct[of "λt. e1 t = e2 t"] by auto
      qed
      moreover have "inj_on (without Row) s'" unfolding inj_on_def
      proof (rule ballI; rule ballI; rule impI)
        fix e1 e2 assume "e1  s'" "e2  s'" "col_num e1 = col_num e2"
        then have "e1 Col = e2 Col" "e1 Num = e2 Num" using without_def by auto
        moreover have "e1 Row = e2 Row"
        proof (cases)
          assume "e1 Row = n - Suc m"
          have "es. e Row < n - Suc m" using Suc latin_rect_iff by blast
          then have "e2 Num  ?not_in_column (e2 Col)" using R_def new_row_def e1 Col = e2 Col e1 Num = e2 Num using s'_def e1  s' e1 Row = n - Suc m by auto
          then show "e1 Row = e2 Row" using new_row_def e1 Row = n - Suc m  s'_def e2  s' by auto
        next
          assume "e1 Row  n - Suc m"
          then have "e1s" using new_row_def s'_def e1s' by auto
          then have "e2 Num  ?not_in_column (e2 Col)" using e1 Col = e2 Col e1 Num = e2 Num by auto
          then have "e2s" using new_row_def s'_def e2s' R_def by auto
          moreover have "inj_on col_num s" using Suc.prems latin_rect_def[of s "(n - Suc m)" n] partial_latin_square_def[of s n] by blast
          ultimately show "e1 Row = e2 Row" using Suc latin_rect_def by (metis col_num e1 = col_num e2 e1  s inj_onD)
        qed
        ultimately show "e1=e2" using latin_type.induct[of "λt. e1 t = e2 t"] by auto
      qed
      moreover have "inj_on (without Num) s'" unfolding inj_on_def
      proof (rule ballI; rule ballI; rule impI)
        fix e1 e2 assume "e1  s'" "e2  s'" "row_col e1 = row_col e2"
        then have "e1 Row = e2 Row" "e1 Col = e2 Col" using without_def by auto
        moreover have "e1 Num = e2 Num"
        proof (cases)
          assume "e1 Row = n - Suc m"
          then have "e2 Row = n - Suc m" using without_def row_col e1 = row_col e2 by auto
          have "es. e Row < n - Suc m" using Suc latin_rect_iff by blast
          then show "e1 Num = e2 Num" using e1 Col = e2 Col using new_row_def s'_def e1  s' e2  s' e1 Row = n - Suc m e2 Row = n - Suc m by auto
        next
          assume "e1 Row  n - Suc m"
          then have "e1s" "e2s" using new_row_def s'_def e1s' e2s' e1 Row = e2 Row by auto
          then show "e1 Num = e2 Num" using Suc latin_rect_def bij_betw_def by (metis row_col e1 = row_col e2 inj_onD)
        qed
        ultimately show "e1=e2" using latin_type.induct[of "λt. e1 t = e2 t"] by auto
      qed
      moreover have "es'. t. e t < n"
      proof (rule ballI; rule allI)
        fix e t assume "es'"
        then show "e t < n"
        proof (cases)
          assume "enew_row"
          then show ?thesis using new_row_def R_def by (induction t) auto
        next
          assume "enew_row"
          then show ?thesis using s'_def es' latin_rect_def partial_latin_square_def Suc by auto
        qed
      qed
      ultimately show "partial_latin_square s' n" unfolding partial_latin_square_def using latin_type.induct[of "λt. inj_on (without t) s'"] by auto
    qed
    moreover have "card s' = n * (n - m)"
    proof -
      have card_s:"card s = n * (n - Suc m)" using latin_rect_iff Suc by auto
      have card_new_row:"card new_row = n" unfolding new_row_def
      proof -
        have "inj_on (λj. rec_latin_type (n - Suc m) j (R j)) {0..<n}" unfolding inj_on_def
        proof (rule ballI; rule ballI; rule impI)
          fix j1 j2 assume "j1  {0..<n}" "j2  {0..<n}" "rec_latin_type (n - Suc m) j1 (R j1) = rec_latin_type (n - Suc m) j2 (R j2)"
          then show  "j1 = j2" using latin_type.rec(2)[of "(n - Suc m)" j1 "R j1"] latin_type.rec(2)[of _ j2 _] by auto
        qed
        then show "card ((λj. rec_latin_type (n - Suc m) j (R j)) ` {0..<n}) = n" by (simp add: card_image)
      qed
      have "s  new_row = {}"
      proof -
        have "es. e Row < n - Suc m" using Suc latin_rect_iff by blast
        then have "e  new_row. e  s" using new_row_def by auto
        then show ?thesis by blast
      qed
      moreover have "finite s" using Suc latin_rect_def by (metis bij_betw_finite finite_SigmaI finite_atLeastLessThan)
      moreover have "finite new_row" using new_row_def by simp
      ultimately have "card s' = card s + card new_row" using s'_def card_Un_disjoint by auto
      with card_s card_new_row show ?thesis using Suc by (metis Suc_diff_Suc Suc_le_lessD add.commute mult_Suc_right)
    qed
    moreover have "es'. e Row < (n - m)"
    proof (rule ballI; cases)
      fix e
      assume "enew_row"
      then show "e Row < n - m" using Suc new_row_def R_def by auto
    next
      fix e
      assume "e  s'" "enew_row"
      then have "e Row < n - Suc m"  using latin_rect_iff Suc  s'_def es' by auto
      then show "e Row < n - m" by auto
    qed
    ultimately show ?thesis using latin_rect_iff[of "n-m" n] by auto
  qed

  ― ‹Finally we use the induction hypothesis:›
  then obtain s'' where "s'  s''" "latin_square s'' n" using Suc by auto
  then have "s  s''" using s'_def by auto
  then show "s'. s  s'  latin_square s' n" using latin_square s'' n by auto
qed

end