Theory KnightsTour

(* Author: Lukas Koller *)

theory KnightsTour
  imports Main
begin

section ‹Introduction and Definitions›

text ‹A Knight's path is a sequence of moves on a chessboard s.t.\ every step in sequence is a 
valid move for a Knight and that the Knight visits every square on the boards exactly once. 
A Knight is a chess figure that is only able to move two squares vertically and one square 
horizontally or two squares horizontally and one square vertically. Finding a Knight's path is an 
instance of the Hamiltonian Path Problem. A Knight's circuit is a Knight's path, where additionally 
the Knight can move from the last square to the first square of the path, forming a loop.

Cull and De Curtins cite‹"cull_decurtins_1987"› prove the existence of a Knight's path on a ‹n×m›-board for
sufficiently large ‹n› and ‹m›. The main idea for the proof is to inductivly construct a Knight's 
path for the ‹n×m›-board from a few pre-computed Knight's paths for small boards, i.e. ‹5×5›, 
‹8×6›, ..., ‹8×9›. The paths for small boards are transformed (i.e. transpose, mirror, translate) 
and concatenated to create paths for larger boards.

While formalizing the proofs I discovered two mistakes in the original proof in 
cite‹"cull_decurtins_1987"›: (i) the pre-computed path for the ‹6×6›-board that ends in 
the upper-left (in Figure 2) and (ii) the pre-computed path for the ‹8×8›-board that ends in 
the upper-left (in Figure 5) are incorrect: on the ‹6×6›-board the Knight cannot step 
from square 26 to square 27; in the ‹8×8›-board the Knight cannot step from square 27 to 
square 28. In this formalization I have replaced the two incorrect paths with correct paths.›

text ‹A square on a board is identified by its coordinates.›
type_synonym square = "int × int"
text ‹A board is represented as a set of squares. Note, that this allows boards to have an 
arbitrary shape and do not necessarily need to be rectangular.›
type_synonym board = "square set"

text ‹A (rectangular) ‹(n×m)›-board is the set of all squares ‹(i,j)› where ‹1 ≤ i ≤ n› 
and ‹1 ≤ j ≤ m›. ‹(1,1)› is the lower-left corner, and ‹(n,m)› is the upper-right corner.›
definition board :: "nat ⇒ nat ⇒ board" where
  "board n m = {(i,j) |i j. 1 ≤ i ∧ i ≤ int n ∧ 1 ≤ j ∧ j ≤ int m}"

text ‹A path is a sequence of steps on a board. A path is represented by the list of visited 
squares on the board. Each square on the ‹(n×m)›-board is identified by its coordinates ‹(i,j)›.›
type_synonym path = "square list"

text ‹A Knight can only move two squares vertically and one square horizontally or two squares 
horizontally and one square vertically. Thus, a knight at position ‹(i,j)› can only move 
to ‹(i±1,j±2)› or ‹(i±2,j±1)›.›
definition valid_step :: "square ⇒ square ⇒ bool" where
  "valid_step si sj ≡ (case si of (i,j) ⇒ sj ∈ {(i+1,j+2),(i-1,j+2),(i+1,j-2),(i-1,j-2),
                                                (i+2,j+1),(i-2,j+1),(i+2,j-1),(i-2,j-1)})"

text ‹Now we define an inductive predicate that characterizes a Knight's path. A square ‹si› can be
pre-pended to a current Knight's path ‹sj#ps› if (i) there is a valid step from the square ‹si› to 
the first square ‹sj› of the current path and (ii) the square ‹si› has not been visited yet.›
inductive knights_path :: "board ⇒ path ⇒ bool" where
  "knights_path {si} [si]"
| "si ∉ b ⟹ valid_step si sj ⟹ knights_path b (sj#ps) ⟹ knights_path (b ∪ {si}) (si#sj#ps)"

code_pred knights_path .

text ‹A sequence is a Knight's circuit iff the sequence if a Knight's path and there is a valid 
step from the last square to the first square.›
definition "knights_circuit b ps ≡ (knights_path b ps ∧ valid_step (last ps) (hd ps))"

section ‹Executable Checker for a Knight's Path›

text ‹This section gives the implementation and correctness-proof for an executable checker for a
knights-path w.r.t.\ the definition @{const knights_path}.›

subsection ‹Implementation of an Executable Checker›

fun row_exec :: "nat ⇒ int set" where
  "row_exec 0 = {}"
| "row_exec m = insert (int m) (row_exec (m-1))"

fun board_exec_aux :: "nat ⇒ int set ⇒ board" where
  "board_exec_aux 0 M = {}"  
| "board_exec_aux k M = {(int k,j) |j. j ∈ M} ∪ board_exec_aux (k-1) M"

text ‹Compute a board.›
fun board_exec :: "nat ⇒ nat ⇒ board" where
  "board_exec n m = board_exec_aux n (row_exec m)"

fun step_checker :: "square ⇒ square ⇒ bool" where
  "step_checker (i,j) (i',j') = 
    ((i+1,j+2) = (i',j') ∨ (i-1,j+2) = (i',j') ∨ (i+1,j-2) = (i',j') ∨ (i-1,j-2) = (i',j') 
     ∨ (i+2,j+1) = (i',j') ∨ (i-2,j+1) = (i',j') ∨ (i+2,j-1) = (i',j') ∨ (i-2,j-1) = (i',j'))"

fun path_checker :: "board ⇒ path ⇒ bool" where
  "path_checker b [] = False"
| "path_checker b [si] = ({si} = b)"
| "path_checker b (si#sj#ps) = (si ∈ b ∧ step_checker si sj ∧ path_checker (b - {si}) (sj#ps))"

fun circuit_checker :: "board ⇒ path ⇒ bool" where
  "circuit_checker b ps = (path_checker b ps ∧ step_checker (last ps) (hd ps))"

subsection ‹Correctness Proof of the Executable Checker›

lemma row_exec_leq: "j ∈ row_exec m ⟷ 1 ≤ j ∧ j ≤ int m"
  by (induction m) auto

lemma board_exec_aux_leq_mem: "(i,j) ∈ board_exec_aux k M ⟷ 1 ≤ i ∧ i ≤ int k ∧ j ∈ M"
  by (induction k M rule: board_exec_aux.induct) auto

lemma board_exec_leq: "(i,j) ∈ board_exec n m ⟷ 1 ≤ i ∧ i ≤ int n ∧ 1 ≤ j ∧ j ≤ int m"
  using board_exec_aux_leq_mem row_exec_leq by auto

lemma board_exec_correct: "board n m = board_exec n m"
  unfolding board_def using board_exec_leq by auto

lemma step_checker_correct: "step_checker si sj ⟷ valid_step si sj"
proof
  assume "step_checker si sj"
  then show "valid_step si sj"
    unfolding valid_step_def 
    apply (cases si)
    apply (cases sj)
    apply auto
    done
next
  assume assms: "valid_step si sj"
  then show "step_checker si sj"
    unfolding valid_step_def by auto
qed

lemma step_checker_rev: "step_checker (i,j) (i',j') ⟹ step_checker (i',j') (i,j)"
  apply (simp only: step_checker.simps)
  by (elim disjE) auto

lemma knights_path_intro_rev: 
  assumes "si ∈ b" "valid_step si sj" "knights_path (b - {si}) (sj#ps)" 
  shows "knights_path b (si#sj#ps)"
  using assms
proof -
  assume assms: "si ∈ b" "valid_step si sj" "knights_path (b - {si}) (sj#ps)"
  then have "si ∉ (b - {si})" "b - {si} ∪ {si} = b"
    by auto
  then show ?thesis
    using assms knights_path.intros(2)[of si "b - {si}"] by auto
qed

text ‹Final correctness corollary for the executable checker @{const path_checker}.›
lemma path_checker_correct: "path_checker b ps ⟷ knights_path b ps"
proof
  assume "path_checker b ps"
  then show "knights_path b ps"
  proof (induction rule: path_checker.induct)
    case (3 si sj xs b)
    then show ?case using step_checker_correct knights_path_intro_rev by auto
  qed (auto intro: knights_path.intros)
next
  assume "knights_path b ps"
  then show "path_checker b ps"                  
    using step_checker_correct 
    by (induction rule: knights_path.induct) (auto elim: knights_path.cases)
qed

corollary knights_path_exec_simp: "knights_path (board n m) ps ⟷ path_checker (board_exec n m) ps"
  using board_exec_correct path_checker_correct[symmetric] by simp

lemma circuit_checker_correct: "circuit_checker b ps ⟷ knights_circuit b ps"
  unfolding knights_circuit_def using path_checker_correct step_checker_correct by auto

corollary knights_circuit_exec_simp: 
  "knights_circuit (board n m) ps ⟷ circuit_checker (board_exec n m) ps"
  using board_exec_correct circuit_checker_correct[symmetric] by simp

section ‹Basic Properties of @{const knights_path} and @{const knights_circuit}›

lemma board_leq_subset: "n1 ≤ n2 ∧ m1 ≤ m2 ⟹ board n1 m1 ⊆ board n2 m2"
  unfolding board_def by auto

lemma finite_row_exec: "finite (row_exec m)"
  by (induction m) auto

lemma finite_board_exec_aux: "finite M ⟹ finite (board_exec_aux n M)"
  by (induction n) auto

lemma board_finite: "finite (board n m)"
  using finite_board_exec_aux finite_row_exec by (simp only: board_exec_correct) auto

lemma card_row_exec: "card (row_exec m) = m"
proof (induction m)
  case (Suc m)
  have "int (Suc m) ∉ row_exec m"
    using row_exec_leq by auto
  then have "card (insert (int (Suc m)) (row_exec m)) = 1 + card (row_exec m)"
    using card_Suc_eq by (metis Suc plus_1_eq_Suc row_exec.simps(1))
  then have "card (row_exec (Suc m)) = 1 + card (row_exec m)"
    by auto
  then show ?case using Suc.IH by auto 
qed auto

lemma set_comp_ins: 
  "{(k,j) |j. j ∈ insert x M} = insert (k,x) {(k,j) |j. j ∈ M}" (is "?Mi = ?iM")
proof
  show "?Mi ⊆ ?iM"
  proof
    fix y assume "y ∈ ?Mi"
    then obtain j where [simp]: "y = (k,j)" and "j ∈ insert x M" by blast
    then have "j = x ∨ j ∈ M" by auto
    then show "y ∈ ?iM" by (elim disjE) auto
  qed
next
  show "?iM ⊆ ?Mi"
  proof
    fix y assume "y ∈ ?iM"
    then obtain j where [simp]: "y = (k,j)" and "j ∈ insert x M" by blast
    then have "j = x ∨ j ∈ M" by auto
    then show "y ∈ ?Mi" by (elim disjE) auto
  qed
qed

lemma finite_card_set_comp: "finite M ⟹ card {(k,j) |j. j ∈ M} = card M"
proof (induction M rule: finite_induct)
  case (insert x M)
  then show ?case using set_comp_ins[of k x M] by auto
qed auto

lemma card_board_exec_aux: "finite M ⟹ card (board_exec_aux k M) = k * card M"
proof (induction k)
  case (Suc k)
  let ?M'="{(int (Suc k),j) |j. j ∈ M}"
  let ?rec_k="board_exec_aux k M"

  have finite: "finite ?M'" "finite ?rec_k"
    using Suc finite_board_exec_aux by auto
  then have card_Un_simp: "card (?M' ∪ ?rec_k) = card ?M' + card ?rec_k"
    using board_exec_aux_leq_mem card_Un_Int[of ?M' ?rec_k] by auto
  
  have card_M: "card ?M' = card M"
    using Suc finite_card_set_comp by auto
  
  have "card (board_exec_aux (Suc k) M) = card ?M' + card ?rec_k"
    using card_Un_simp by auto
  also have "... = card M + k * card M"
    using Suc card_M by auto
  also have "... = (Suc k) * card M"
    by auto
  finally show ?case .
qed auto

lemma card_board: "card (board n m) = n * m"
proof -
  have "card (board n m) = card (board_exec_aux n (row_exec m))"
    using board_exec_correct by auto
  also have "... = n * m"
    using card_row_exec card_board_exec_aux finite_row_exec by auto
  finally show ?thesis .
qed

lemma knights_path_board_non_empty: "knights_path b ps ⟹ b ≠ {}"
  by (induction arbitrary: ps rule: knights_path.induct) auto

lemma knights_path_board_m_n_geq_1: "knights_path (board n m) ps ⟹ min n m ≥ 1"
  unfolding board_def using knights_path_board_non_empty by fastforce

lemma knights_path_non_nil: "knights_path b ps ⟹ ps ≠ []"
  by (induction arbitrary: b rule: knights_path.induct) auto

lemma knights_path_set_eq: "knights_path b ps ⟹ set ps = b"
  by (induction rule: knights_path.induct) auto

lemma knights_path_subset: 
  "knights_path b1 ps1 ⟹ knights_path b2 ps2 ⟹ set ps1 ⊆ set ps2 ⟷ b1 ⊆ b2"
  using knights_path_set_eq by auto

lemma knights_path_board_unique: "knights_path b1 ps ⟹ knights_path b2 ps ⟹ b1 = b2"
  using knights_path_set_eq by auto

lemma valid_step_neq: "valid_step si sj ⟹ si ≠ sj"
  unfolding valid_step_def by auto

lemma valid_step_non_transitive: "valid_step si sj ⟹ valid_step sj sk ⟹ ¬valid_step si sk"
proof -
  assume assms: "valid_step si sj" "valid_step sj sk"
  obtain ii ji ij jj ik jk where [simp]: "si = (ii,ji)" "sj = (ij,jj)" "sk = (ik,jk)" by force
  then have "step_checker (ii,ji) (ij,jj)" "step_checker (ij,jj) (ik,jk)" 
    using assms step_checker_correct by auto
  then show "¬valid_step si sk"
    apply (simp add: step_checker_correct[symmetric])
    apply (elim disjE)
    apply auto
    done
qed

lemma knights_path_distinct: "knights_path b ps ⟹ distinct ps"
proof (induction rule: knights_path.induct)
  case (2 si b sj ps)
  then have "si ∉ set (sj # ps)"
    using knights_path_set_eq valid_step_neq by blast
  then show ?case using 2 by auto
qed auto

lemma knights_path_length: "knights_path b ps ⟹ length ps = card b"
  using knights_path_set_eq knights_path_distinct by (metis distinct_card)

lemma knights_path_take: 
  assumes "knights_path b ps" "0 < k" "k < length ps"
  shows "knights_path (set (take k ps)) (take k ps)"
  using assms 
proof (induction arbitrary: k rule: knights_path.induct)
  case (2 si b sj ps)
  then have "k = 1 ∨ k = 2 ∨ 2 < k" by force
  then show ?case
    using 2
  proof (elim disjE)
    assume "k = 2"
    then have "take k (si#sj#ps) = [si,sj]" "si ∉ {sj}" using 2 valid_step_neq by auto
    then show ?thesis using 2 knights_path.intros by auto
  next
    assume "2 < k"
    then have k_simps: "k-2 = k-1-1" "0 < k-2" "k-2 < length ps" and
        take_simp1: "take k (si#sj#ps) = si#take (k-1) (sj#ps)" and
        take_simp2: "take k (si#sj#ps) = si#sj#take (k-1-1) ps"
      using assms 2 take_Cons'[of k si "sj#ps"] take_Cons'[of "k-1" sj ps] by auto
    then have "knights_path (set (take (k-1) (sj#ps))) (take (k-1) (sj#ps))"
      using 2 k_simps by auto
    then have kp: "knights_path (set (take (k-1) (sj#ps))) (sj#take (k-2) ps)"
      using take_Cons'[of "k-1" sj ps] by (auto simp: k_simps elim: knights_path.cases)

    have no_mem: "si ∉ set (take (k-1) (sj#ps))"
      using 2 set_take_subset[of "k-1" "sj#ps"] knights_path_set_eq by blast
    have "knights_path (set (take (k-1) (sj#ps)) ∪ {si}) (si#sj#take (k-2) ps)"
      using knights_path.intros(2)[OF no_mem ‹valid_step si sj› kp] by auto
    then show ?thesis using k_simps take_simp2 knights_path_set_eq by metis
  qed (auto intro: knights_path.intros)
qed auto

lemma knights_path_drop: 
  assumes "knights_path b ps" "0 < k" "k < length ps"
  shows "knights_path (set (drop k ps)) (drop k ps)"
  using assms
proof (induction arbitrary: k rule: knights_path.induct)
  case (2 si b sj ps)
  then have "(k = 1 ∧ ps = []) ∨ (k = 1 ∧ ps ≠ []) ∨ 1 < k" by force
  then show ?case
    using 2
  proof (elim disjE)
    assume "k = 1 ∧ ps ≠ []"
    then show ?thesis using 2 knights_path_set_eq by force
  next
    assume "1 < k"
    then have "0 < k-1" "k-1 < length (sj#ps)" "drop k (si#sj#ps) = drop (k-1) (sj#ps)" 
      using assms 2 drop_Cons'[of k si "sj#ps"] by auto
    then show ?thesis
      using 2 by auto
  qed (auto intro: knights_path.intros)
qed auto

text ‹A Knight's path can be split to form two new disjoint Knight's paths.›
corollary knights_path_split:             
  assumes "knights_path b ps" "0 < k" "k < length ps"
  shows 
    "∃b1 b2. knights_path b1 (take k ps) ∧ knights_path b2 (drop k ps) ∧ b1 ∪ b2 = b ∧ b1 ∩ b2 = {}"
  using assms
proof -
  let ?b1="set (take k ps)" 
  let ?b2="set (drop k ps)"
  have kp1: "knights_path ?b1 (take k ps)" and kp2: "knights_path ?b2 (drop k ps)"
    using assms knights_path_take knights_path_drop by auto
  have union: "?b1 ∪ ?b2 = b"
    using assms knights_path_set_eq by (metis append_take_drop_id set_append)
  have inter: "?b1 ∩ ?b2 = {}"
    using assms knights_path_distinct by (metis append_take_drop_id distinct_append)
  show ?thesis using kp1 kp2 union inter by auto
qed

text ‹Append two disjoint Knight's paths.›
corollary knights_path_append:             
  assumes "knights_path b1 ps1" "knights_path b2 ps2" "b1 ∩ b2 = {}" "valid_step (last ps1) (hd ps2)"
  shows "knights_path (b1 ∪ b2) (ps1 @ ps2)"
  using assms
proof (induction arbitrary: ps2 b2 rule: knights_path.induct)
  case (1 si)
  then have "si ∉ b2" "ps2 ≠ []" "valid_step si (hd ps2)" "knights_path b2 (hd ps2#tl ps2)" 
    using knights_path_non_nil by auto
  then have "knights_path (b2 ∪ {si}) (si#hd ps2#tl ps2)"
    using knights_path.intros by blast
  then show ?case using ‹ps2 ≠ []› by auto
next
  case (2 si b1 sj ps1)
  then have "si ∉ b1 ∪ b2" "valid_step si sj" "knights_path (b1 ∪ b2) (sj#ps1@ps2)" by auto
  then have "knights_path (b1 ∪ b2 ∪ {si}) (si#sj#ps1@ps2)"
    using knights_path.intros by auto
  then show ?case by auto
qed

lemma valid_step_rev: "valid_step si sj ⟹ valid_step sj si"
  using step_checker_correct step_checker_rev by (metis prod.exhaust_sel)

text ‹Reverse a Knight's path.›
corollary knights_path_rev:
  assumes "knights_path b ps"
  shows "knights_path b (rev ps)"
  using assms
proof (induction rule: knights_path.induct)
  case (2 si b sj ps)
  then have "knights_path {si} [si]" "b ∩ {si} = {}" "valid_step (last (rev (sj # ps))) (hd [si])"
    using valid_step_rev by (auto intro: knights_path.intros)
  then have "knights_path (b ∪ {si}) ((rev (sj#ps))@[si])"
    using 2 knights_path_append by blast
  then show ?case by auto
qed (auto intro: knights_path.intros)

text ‹Reverse a Knight's circuit.›
corollary knights_circuit_rev:
  assumes "knights_circuit b ps"
  shows "knights_circuit b (rev ps)"
  using assms knights_path_rev valid_step_rev
  unfolding knights_circuit_def by (auto simp: hd_rev last_rev)

(* Function to rotate a Knight's circuit to start with (1,1),(3,2),... *)
(* fun rot_c_acc :: "path ⇒ path ⇒ path" where
  "rot_c_acc (si#sj#ps) acc = 
    (if si = (1,1) then 
      if sj = (3,2) then si#rev (sj#ps@acc) else si#sj#ps@acc
    else rot_c_acc (sj#ps) (si#acc))"
| "rot_c_acc _ acc = []"

definition "rot_c ps ≡ rot_c_acc ps []" *)

lemma knights_circuit_rotate1:
  assumes "knights_circuit b (si#ps)"
  shows "knights_circuit b (ps@[si])"
proof (cases "ps = []")
  case True
  then show ?thesis using assms by auto
next
  case False
  have kp1: "knights_path b (si#ps)" "valid_step (last (si#ps)) (hd (si#ps))"
    using assms unfolding knights_circuit_def by auto
  then have kp_elim: "si ∉ (b - {si})" "valid_step si (hd ps)" "knights_path (b - {si}) ps"
    using ‹ps ≠ []› by (auto elim: knights_path.cases)
  then have vs': "valid_step (last (ps@[si])) (hd (ps@[si]))"
    using ‹ps ≠ []› valid_step_rev by auto

  have kp2: "knights_path {si} [si]" "(b - {si}) ∩ {si} = {}"
    by (auto intro: knights_path.intros)

  have vs: "valid_step (last ps) (hd [si])"
    using ‹ps ≠ []› ‹valid_step (last (si#ps)) (hd (si#ps))› by auto

  have "(b - {si}) ∪ {si} = b"
    using kp1 kp_elim knights_path_set_eq by force
  then show ?thesis
    unfolding knights_circuit_def
    using vs knights_path_append[OF ‹knights_path (b - {si}) ps› kp2] vs' by auto
qed

text ‹A Knight's circuit can be rotated to start at any square on the board.›
lemma knights_circuit_rotate_to:
  assumes "knights_circuit b ps" "hd (drop k ps) = si" "k < length ps"
  shows "∃ps'. knights_circuit b ps' ∧ hd ps' = si"
  using assms
proof (induction k arbitrary: b ps)
  case (Suc k)
  let ?sj="hd ps"
  let ?ps'="tl ps"           
  show ?case
  proof (cases "si = ?sj")
    case True
    then show ?thesis using Suc by auto
  next
    case False
    then have "?ps' ≠ []"
      using Suc by (metis drop_Nil drop_Suc drop_eq_Nil2 le_antisym nat_less_le)
    then have "knights_circuit b (?sj#?ps')"
      using Suc by (metis list.exhaust_sel tl_Nil)
    then have "knights_circuit b (?ps'@[?sj])" "hd (drop k (?ps'@[?sj])) = si" 
      using Suc knights_circuit_rotate1 by (auto simp: drop_Suc)
    then show ?thesis using Suc by auto
  qed
qed auto

text ‹For positive boards (1,1) can only have (2,3) and (3,2) as a neighbour.›
lemma valid_step_1_1:
  assumes "valid_step (1,1) (i,j)" "i > 0" "j > 0"
  shows "(i,j) = (2,3) ∨ (i,j) = (3,2)"
  using assms unfolding valid_step_def by auto

lemma list_len_g_1_split: "length xs > 1 ⟹ ∃x1 x2 xs'. xs = x1#x2#xs'"
proof (induction xs)
  case (Cons x xs)
  then have "length xs > 0" by auto
  then have "length xs ≥ 1" by presburger
  then have "length xs = 1 ∨ length xs > 1" by auto
  then show ?case 
  proof (elim disjE)
    assume "length xs = 1"
    then obtain x1 where [simp]: "xs = [x1]"
      using length_Suc_conv[of xs 0] by auto
    then show ?thesis by auto
  next
    assume "1 < length xs"
    then show ?thesis using Cons by auto
  qed
qed auto

lemma list_len_g_3_split: "length xs > 3 ⟹ ∃x1 x2 xs' x3. xs = x1#x2#xs'@[x3]"
proof (induction xs)
  case (Cons x xs)
  then have "length xs = 3 ∨ length xs > 3" by auto
  then show ?case 
  proof (elim disjE)
    assume "length xs = 3"
    then obtain x1 xs1 where [simp]: "xs = x1#xs1" "length xs1 = 2"
      using length_Suc_conv[of xs 2] by auto
    then obtain x2 xs2 where [simp]: "xs1 = x2#xs2" "length xs2 = 1"
      using length_Suc_conv[of xs1 1] by auto
    then obtain x3 where [simp]: "xs2 = [x3]"
      using length_Suc_conv[of xs2 0] by auto
    then show ?thesis by auto
  next
    assume "length xs > 3"
    then show ?thesis using Cons by auto
  qed
qed auto

text ‹Any Knight's circuit on a positive board can be rotated to start with (1,1) and 
end with (3,2).›
corollary rotate_knights_circuit:
  assumes "knights_circuit (board n m) ps" "min n m ≥ 5"
  shows "∃ps. knights_circuit (board n m) ps ∧ hd ps = (1,1) ∧ last ps = (3,2)"
  using assms
proof -
  let ?b="board n m"
  have "knights_path ?b ps"
    using assms unfolding knights_circuit_def by auto
  then have "(1,1) ∈ set ps"
    using assms knights_path_set_eq by (auto simp: board_def)
  then obtain k where "hd (drop k ps) = (1,1)" "k < length ps"
    by (metis hd_drop_conv_nth in_set_conv_nth)
  then obtain psr where psr_prems: "knights_circuit ?b psr" "hd psr = (1,1)"
    using assms knights_circuit_rotate_to by blast
  then have kp: "knights_path ?b psr" and "valid_step (last psr) (1,1)"
    unfolding knights_circuit_def by auto

  have "(1,1) ∈ ?b" "(1,2) ∈ ?b" "(1,3) ∈ ?b"
    using assms unfolding board_def by auto
  then have "(1,1) ∈ set psr" "(1,2) ∈ set psr" "(1,3) ∈ set psr"
    using kp knights_path_set_eq by auto

  have "3 < card ?b"
    using assms board_leq_subset card_board[of 5 5]
          card_mono[OF board_finite[of n m], of "board 5 5"] by auto
  then have "3 < length psr"
    using knights_path_length kp by auto
  then obtain sj ps' sk where [simp]: "psr = (1,1)#sj#ps'@[sk]"
    using ‹hd psr = (1,1)› list_len_g_3_split[of psr] by auto
  have "sj ≠ sk"
    using kp knights_path_distinct by force

  have vs_sk: "valid_step sk (1,1)"
    using ‹valid_step (last psr) (1,1)› by simp

  have vs_sj: "valid_step (1,1) sj" and kp': "knights_path (?b - {(1,1)}) (sj#ps'@[sk])"
    using kp by (auto elim: knights_path.cases)

  have "sj ∈ set psr" "sk ∈ set psr" by auto
  then have "sj ∈ ?b" "sk ∈ ?b"
    using kp knights_path_set_eq by blast+
  then have "0 < fst sj ∧ 0 < snd sj" "0 < fst sk ∧ 0 < snd sk"
    unfolding board_def by auto
  then have "sk = (2,3) ∨ sk = (3,2)" "sj = (2,3) ∨ sj = (3,2)"
    using vs_sk vs_sj valid_step_1_1 valid_step_rev by (metis prod.collapse)+
  then have "sk = (3,2) ∨ sj = (3,2)"
    using ‹sj ≠ sk› by auto
  then show ?thesis
  proof (elim disjE)
    assume "sk = (3,2)"
    then have "last psr = (3,2)" by auto
    then show ?thesis using psr_prems by auto
  next
    assume "sj = (3,2)"
    then have vs: "valid_step (last ((1,1)#rev (sj#ps'@[sk]))) (hd ((1,1)#rev (sj#ps'@[sk])))"
      unfolding valid_step_def by auto

    have rev_simp: "rev (sj#ps'@[sk]) = sk#(rev ps')@[sj]" by auto

    have "knights_path (?b - {(1,1)}) (rev (sj#ps'@[sk]))"
      using knights_path_rev[OF kp'] by auto
    then have "(1,1) ∉ (?b - {(1,1)})" "valid_step (1,1) sk" 
         "knights_path (?b - {(1,1)}) (sk#(rev ps')@[sj])"
      using assms vs_sk valid_step_rev by (auto simp: rev_simp)
    then have "knights_path (?b - {(1, 1)} ∪ {(1, 1)}) ((1,1)#sk#(rev ps')@[sj])"
      using knights_path.intros(2)[of "(1,1)" "?b - {(1,1)}" sk "(rev ps')@[sj]"] by auto
    then have "knights_path ?b ((1,1)#rev (sj#ps'@[sk]))"
      using assms by (simp add: board_def insert_absorb rev_simp)
    then have "knights_circuit ?b ((1,1)#rev (sj#ps'@[sk]))"
      unfolding knights_circuit_def using vs by auto
    then show ?thesis
      using ‹sj = (3,2)› by auto
  qed
qed

section ‹Transposing Paths and Boards›

subsection ‹Implementation of Path and Board Transposition›

definition "transpose_square si = (case si of (i,j) ⇒ (j,i))"

fun transpose :: "path ⇒ path" where
  "transpose [] = []"
| "transpose (si#ps) = (transpose_square si)#transpose ps"

definition transpose_board :: "board ⇒ board" where
  "transpose_board b ≡ {(j,i) |i j. (i,j) ∈ b}"

subsection ‹Correctness of Path and Board Transposition›

lemma transpose2: "transpose_square (transpose_square si) = si"
  unfolding transpose_square_def by (auto split: prod.splits)

lemma transpose_nil: "ps = [] ⟷ transpose ps = []"
  using transpose.elims by blast

lemma transpose_length: "length ps = length (transpose ps)"
  by (induction ps) auto

lemma hd_transpose: "ps ≠[] ⟹ hd (transpose ps) = transpose_square (hd ps)"
  by (induction ps) (auto simp: transpose_square_def)

lemma last_transpose: "ps ≠[] ⟹ last (transpose ps) = transpose_square (last ps)"
proof (induction ps)
  case (Cons si ps)
  then show ?case
  proof (cases "ps = []")
    case True
    then show ?thesis using Cons by (auto simp: transpose_square_def)      
  next
    case False
    then show ?thesis using Cons transpose_nil by auto
  qed
qed auto

lemma take_transpose: 
  shows "take k (transpose ps) = transpose (take k ps)"
proof (induction ps arbitrary: k)
  case Nil
  then show ?case by auto
next
  case (Cons si ps)
  then obtain i j where "si = (i,j)" by force
  then have "k = 0 ∨ k > 0" by auto
  then show ?case 
  proof (elim disjE)
    assume "k > 0"
    then show ?thesis using Cons.IH by (auto simp: ‹si = (i,j)› take_Cons')
  qed auto
qed

lemma drop_transpose: 
  shows "drop k (transpose ps) = transpose (drop k ps)"
proof (induction ps arbitrary: k)
  case Nil
  then show ?case by auto
next
  case (Cons si ps)
  then obtain i j where "si = (i,j)" by force
  then have "k = 0 ∨ k > 0" by auto
  then show ?case 
  proof (elim disjE)
    assume "k > 0"
    then show ?thesis using Cons.IH by (auto simp: ‹si = (i,j)› drop_Cons')
  qed auto
qed

lemma transpose_board_correct: "si ∈ b ⟷ (transpose_square si) ∈ transpose_board b"
  unfolding transpose_board_def transpose_square_def by (auto split: prod.splits)

lemma transpose_board: "transpose_board (board n m) = board m n"
  unfolding board_def using transpose_board_correct by (auto simp: transpose_square_def)

lemma insert_transpose_board: 
  "insert (transpose_square si) (transpose_board b) = transpose_board (insert si b)"
  unfolding transpose_board_def transpose_square_def by (auto split: prod.splits)

lemma transpose_board2: "transpose_board (transpose_board b) = b"
  unfolding transpose_board_def by auto

lemma transpose_union: "transpose_board (b1 ∪ b2) = transpose_board b1 ∪ transpose_board b2"
  unfolding transpose_board_def by auto

lemma transpose_valid_step: 
  "valid_step si sj ⟷ valid_step (transpose_square si) (transpose_square sj)"
  unfolding valid_step_def transpose_square_def by (auto split: prod.splits)

lemma transpose_knights_path':  
  assumes "knights_path b ps" 
  shows "knights_path (transpose_board b) (transpose ps)"
  using assms
proof (induction rule: knights_path.induct)
  case (1 si)
  then have "transpose_board {si} = {transpose_square si}" "transpose [si] = [transpose_square si]"
    using transpose_board_correct by (auto simp: transpose_square_def split: prod.splits)
  then show ?case by (auto intro: knights_path.intros)
next
  case (2 si b sj ps)
  then have prems: "transpose_square si ∉ transpose_board b" 
            "valid_step (transpose_square si) (transpose_square sj)" 
            and "transpose (sj#ps) = transpose_square sj#transpose ps"
    using 2 transpose_board_correct transpose_valid_step by auto
  then show ?case 
    using 2 knights_path.intros(2)[OF prems] insert_transpose_board by auto
qed

corollary transpose_knights_path: 
  assumes "knights_path (board n m) ps" 
  shows "knights_path (board m n) (transpose ps)"
  using assms transpose_knights_path'[of "board n m" ps] by (auto simp: transpose_board) 

corollary transpose_knights_circuit: 
  assumes "knights_circuit (board n m) ps" 
  shows "knights_circuit (board m n) (transpose ps)"
  using assms 
proof -
  have "knights_path (board n m) ps" and vs: "valid_step (last ps) (hd ps)"
    using assms unfolding knights_circuit_def by auto
  then have kp_t: "knights_path (board m n) (transpose ps)" and "ps ≠ []"
    using transpose_knights_path knights_path_non_nil by auto
  then have "valid_step (last (transpose ps)) (hd (transpose ps))"
    using vs hd_transpose last_transpose transpose_valid_step by auto
  then show ?thesis using kp_t by (auto simp: knights_circuit_def)
qed

section ‹Mirroring Paths and Boards›

subsection ‹Implementation of Path and Board Mirroring›

abbreviation "min1 ps ≡ Min ((fst) ` set ps)"
abbreviation "max1 ps ≡ Max ((fst) ` set ps)"
abbreviation "min2 ps ≡ Min ((snd) ` set ps)"
abbreviation "max2 ps ≡ Max ((snd) ` set ps)"

definition mirror1_square :: "int ⇒ square ⇒ square" where 
  "mirror1_square n si = (case si of (i,j) ⇒ (n-i,j))"

fun mirror1_aux :: "int ⇒ path ⇒ path" where
  "mirror1_aux n [] = []"
| "mirror1_aux n (si#ps) = (mirror1_square n si)#mirror1_aux n ps"

definition "mirror1 ps = mirror1_aux (max1 ps + min1 ps) ps"

definition mirror1_board :: "int ⇒ board ⇒ board" where
  "mirror1_board n b ≡ {mirror1_square n si |si. si ∈ b}"

definition mirror2_square :: "int ⇒ square ⇒ square" where 
  "mirror2_square m si = (case si of (i,j) ⇒ (i,m-j))"

fun mirror2_aux :: "int ⇒ path ⇒ path" where
  "mirror2_aux m [] = []"
| "mirror2_aux m (si#ps) = (mirror2_square m si)#mirror2_aux m ps"

definition "mirror2 ps = mirror2_aux (max2 ps + min2 ps) ps"

definition mirror2_board :: "int ⇒ board ⇒ board" where
  "mirror2_board m b ≡ {mirror2_square m si |si. si ∈ b}"

subsection ‹Correctness of Path and Board Mirroring›

lemma mirror1_board_id: "mirror1_board (int n+1) (board n m) = board n m" (is "_ = ?b")
proof
  show "mirror1_board (int n+1) ?b ⊆ ?b"
  proof
    fix si'
    assume assms: "si' ∈ mirror1_board (int n+1) ?b"
    then obtain i' j' where [simp]: "si' = (i',j')" by force
    then have "(i',j') ∈ mirror1_board (int n+1) ?b"
      using assms by auto
    then obtain i j where "(i,j) ∈ ?b" "mirror1_square (int n+1) (i,j) = (i',j')"
      unfolding mirror1_board_def by auto
    then have "1 ≤ i ∧ i ≤ int n" "1 ≤ j ∧ j ≤ int m" "i'=(int n+1)-i" "j'=j"
      unfolding board_def mirror1_square_def by auto
    then have "1 ≤ i' ∧ i' ≤ int n" "1 ≤ j' ∧ j' ≤ int m"
      by auto
    then show "si' ∈ ?b"
      unfolding board_def by auto
  qed
next
  show "?b ⊆ mirror1_board (int n+1) ?b"
  proof
    fix si
    assume assms: "si ∈ ?b"
    then obtain i j where [simp]: "si = (i,j)" by force
    then have "(i,j) ∈ ?b"
      using assms by auto
    then have "1 ≤ i ∧ i ≤ int n" "1 ≤ j ∧ j ≤ int m"
      unfolding board_def by auto
    then obtain i' j' where "i'=(int n+1)-i" "j'=j" by auto
    then have "(i',j') ∈ ?b" "mirror1_square (int n+1) (i',j') = (i,j)" 
      using ‹1 ≤ i ∧ i ≤ int n› ‹1 ≤ j ∧ j ≤ int m› 
      unfolding mirror1_square_def by (auto simp: board_def)
    then show "si ∈ mirror1_board (int n+1) ?b"
      unfolding mirror1_board_def by force
  qed
qed

lemma mirror2_board_id: "mirror2_board (int m+1) (board n m) = board n m" (is "_ = ?b")
proof
  show "mirror2_board (int m+1) ?b ⊆ ?b"
  proof
    fix si'
    assume assms: "si' ∈ mirror2_board (int m+1) ?b"
    then obtain i' j' where [simp]: "si' = (i',j')" by force
    then have "(i',j') ∈ mirror2_board (int m+1) ?b"
      using assms by auto
    then obtain i j where "(i,j) ∈ ?b" "mirror2_square (int m+1) (i,j) = (i',j')"
      unfolding mirror2_board_def by auto
    then have "1 ≤ i ∧ i ≤ int n" "1 ≤ j ∧ j ≤ int m" "i'=i" "j'=(int m+1)-j"
      unfolding board_def mirror2_square_def by auto
    then have "1 ≤ i' ∧ i' ≤ int n" "1 ≤ j' ∧ j' ≤ int m"
      by auto
    then show "si' ∈ ?b"
      unfolding board_def by auto
  qed
next
  show "?b ⊆ mirror2_board (int m+1) ?b"
  proof
    fix si
    assume assms: "si ∈ ?b"
    then obtain i j where [simp]: "si = (i,j)" by force
    then have "(i,j) ∈ ?b"
      using assms by auto
    then have "1 ≤ i ∧ i ≤ int n" "1 ≤ j ∧ j ≤ int m"
      unfolding board_def by auto
    then obtain i' j' where "i'=i" "j'=(int m+1)-j" by auto
    then have "(i',j') ∈ ?b" "mirror2_square (int m+1) (i',j') = (i,j)" 
      using ‹1 ≤ i ∧ i ≤ int n› ‹1 ≤ j ∧ j ≤ int m› 
      unfolding mirror2_square_def by (auto simp: board_def)
    then show "si ∈ mirror2_board (int m+1) ?b"
      unfolding mirror2_board_def by force
  qed
qed

lemma knights_path_min1: "knights_path (board n m) ps ⟹ min1 ps = 1"
proof -
  assume assms: "knights_path (board n m) ps"
  then have "min n m ≥ 1"
    using knights_path_board_m_n_geq_1 by auto
  then have "(1,1) ∈ board n m" and ge_1: "∀(i,j) ∈ board n m. i ≥ 1"
    unfolding board_def by auto
  then have finite: "finite ((fst) ` board n m)" and 
          non_empty: "(fst) ` board n m ≠ {}" and
          mem_1: "1 ∈ (fst) ` board n m"
    using board_finite by auto (metis fstI image_eqI)
  then have "Min ((fst) ` board n m) = 1"
    using ge_1 by (auto simp: Min_eq_iff)
  then show ?thesis
    using assms knights_path_set_eq by auto
qed

lemma knights_path_min2: "knights_path (board n m) ps ⟹ min2 ps = 1"
proof -
  assume assms: "knights_path (board n m) ps"
  then have "min n m ≥ 1"
    using knights_path_board_m_n_geq_1 by auto
  then have "(1,1) ∈ board n m" and ge_1: "∀(i,j) ∈ board n m. j ≥ 1"
    unfolding board_def by auto
  then have finite: "finite ((snd) ` board n m)" and 
          non_empty: "(snd) ` board n m ≠ {}" and
          mem_1: "1 ∈ (snd) ` board n m"
    using board_finite by auto (metis sndI image_eqI)
  then have "Min ((snd) ` board n m) = 1"
    using ge_1 by (auto simp: Min_eq_iff)
  then show ?thesis
    using assms knights_path_set_eq by auto
qed

lemma knights_path_max1: "knights_path (board n m) ps ⟹ max1 ps = int n"
proof -
  assume assms: "knights_path (board n m) ps"
  then have "min n m ≥ 1"
    using knights_path_board_m_n_geq_1 by auto
  then have "(int n,1) ∈ board n m" and leq_n: "∀(i,j) ∈ board n m. i ≤ int n"
    unfolding board_def by auto
  then have finite: "finite ((fst) ` board n m)" and 
          non_empty: "(fst) ` board n m ≠ {}" and
          mem_1: "int n ∈ (fst) ` board n m"
    using board_finite by auto (metis fstI image_eqI)
  then have "Max ((fst) ` board n m) = int n"
    using leq_n by (auto simp: Max_eq_iff)
  then show ?thesis
    using assms knights_path_set_eq by auto
qed

lemma knights_path_max2: "knights_path (board n m) ps ⟹ max2 ps = int m"
proof -
  assume assms: "knights_path (board n m) ps"
  then have "min n m ≥ 1"
    using knights_path_board_m_n_geq_1 by auto
  then have "(1,int m) ∈ board n m" and leq_m: "∀(i,j) ∈ board n m. j ≤ int m"
    unfolding board_def by auto
  then have finite: "finite ((snd) ` board n m)" and 
          non_empty: "(snd) ` board n m ≠ {}" and
          mem_1: "int m ∈ (snd) ` board n m"
    using board_finite by auto (metis sndI image_eqI)
  then have "Max ((snd) ` board n m) = int m"
    using leq_m by (auto simp: Max_eq_iff)
  then show ?thesis
    using assms knights_path_set_eq by auto
qed

lemma mirror1_aux_nil: "ps = [] ⟷ mirror1_aux m ps = []"
  using mirror1_aux.elims by blast

lemma mirror1_nil: "ps = [] ⟷ mirror1 ps = []"
  unfolding mirror1_def using mirror1_aux_nil by blast

lemma mirror2_aux_nil: "ps = [] ⟷ mirror2_aux m ps = []"
  using mirror2_aux.elims by blast

lemma mirror2_nil: "ps = [] ⟷ mirror2 ps = []"
  unfolding mirror2_def using mirror2_aux_nil by blast

lemma length_mirror1_aux: "length ps = length (mirror1_aux n ps)"
  by (induction ps) auto

lemma length_mirror1: "length ps = length (mirror1 ps)"
  unfolding mirror1_def using length_mirror1_aux by auto

lemma length_mirror2_aux: "length ps = length (mirror2_aux n ps)"
  by (induction ps) auto

lemma length_mirror2: "length ps = length (mirror2 ps)"
  unfolding mirror2_def using length_mirror2_aux by auto

lemma mirror1_board_iff:"si ∉ b ⟷ mirror1_square n si ∉ mirror1_board n b"
  unfolding mirror1_board_def mirror1_square_def by (auto split: prod.splits)

lemma mirror2_board_iff:"si ∉ b ⟷ mirror2_square n si ∉ mirror2_board n b"
  unfolding mirror2_board_def mirror2_square_def by (auto split: prod.splits)

lemma insert_mirror1_board: 
  "insert (mirror1_square n si) (mirror1_board n b) = mirror1_board n (insert si b)"
  unfolding mirror1_board_def mirror1_square_def by (auto split: prod.splits)

lemma insert_mirror2_board: 
  "insert (mirror2_square n si) (mirror2_board n b) = mirror2_board n (insert si b)"
  unfolding mirror2_board_def mirror2_square_def by (auto split: prod.splits)

lemma valid_step_mirror1: 
  "valid_step si sj ⟷ valid_step (mirror1_square n si) (mirror1_square n sj)" 
proof
  assume assms: "valid_step si sj"
  obtain i j i' j' where [simp]: "si = (i,j)" "sj = (i',j')" by force
  then have "valid_step (n-i,j) (n-i',j')"
    using assms unfolding valid_step_def
    apply simp
    apply (elim disjE)
    apply auto
    done
  then show "valid_step (mirror1_square n si) (mirror1_square n sj)"
    unfolding mirror1_square_def by auto
next
  assume assms: "valid_step (mirror1_square n si) (mirror1_square n sj)"
  obtain i j i' j' where [simp]: "si = (i,j)" "sj = (i',j')" by force
  then have "valid_step (i,j) (i',j')"
    using assms unfolding valid_step_def mirror1_square_def
    apply simp
    apply (elim disjE)
    apply auto
    done
  then show "valid_step si sj"
    unfolding mirror1_square_def by auto
qed

lemma valid_step_mirror2: 
  "valid_step si sj ⟷ valid_step (mirror2_square m si) (mirror2_square m sj)"
proof
  assume assms: "valid_step si sj"
  obtain i j i' j' where [simp]: "si = (i,j)" "sj = (i',j')" by force
  then have "valid_step (i,m-j) (i',m-j')"
    using assms unfolding valid_step_def
    apply simp
    apply (elim disjE)
    apply auto
    done
  then show "valid_step (mirror2_square m si) (mirror2_square m sj)"
    unfolding mirror2_square_def by auto
next
  assume assms: "valid_step (mirror2_square m si) (mirror2_square m sj)"
  obtain i j i' j' where [simp]: "si = (i,j)" "sj = (i',j')" by force
  then have "valid_step (i,j) (i',j')"
    using assms unfolding valid_step_def mirror2_square_def
    apply simp
    apply (elim disjE)
    apply auto
    done
  then show "valid_step si sj"
    unfolding mirror1_square_def by auto
qed

lemma hd_mirror1:
  assumes "knights_path (board n m) ps" "hd ps = (i,j)"
  shows "hd (mirror1 ps) = (int n+1-i,j)"
  using assms
proof -
  have "hd (mirror1 ps) = hd (mirror1_aux (int n+1) ps)"
    unfolding mirror1_def using assms knights_path_min1 knights_path_max1 by auto
  also have "... = hd (mirror1_aux (int n+1) ((hd ps)#(tl ps)))"
    using assms knights_path_non_nil by (metis list.collapse)
  also have "... = (int n+1-i,j)"
    using assms by (auto simp: mirror1_square_def)
  finally show ?thesis .
qed

lemma last_mirror1_aux:
  assumes "ps ≠ []" "last ps = (i,j)"
  shows "last (mirror1_aux n ps) = (n-i,j)"
  using assms
proof (induction ps)
  case (Cons si ps)
  then show ?case 
    using mirror1_aux_nil Cons by (cases "ps = []") (auto simp: mirror1_square_def)
qed auto

lemma last_mirror1:
  assumes "knights_path (board n m) ps" "last ps = (i,j)"
  shows "last (mirror1 ps) = (int n+1-i,j)"
  unfolding mirror1_def using assms last_mirror1_aux knights_path_non_nil
  by (simp add: knights_path_max1 knights_path_min1)

lemma hd_mirror2:
  assumes "knights_path (board n m) ps" "hd ps = (i,j)"
  shows "hd (mirror2 ps) = (i,int m+1-j)"
  using assms
proof -
  have "hd (mirror2 ps) = hd (mirror2_aux (int m+1) ps)"
    unfolding mirror2_def using assms knights_path_min2 knights_path_max2 by auto
  also have "... = hd (mirror2_aux (int m+1) ((hd ps)#(tl ps)))"
    using assms knights_path_non_nil by (metis list.collapse)
  also have "... = (i,int m+1-j)"
    using assms by (auto simp: mirror2_square_def)
  finally show ?thesis .
qed

lemma last_mirror2_aux:
  assumes "ps ≠ []" "last ps = (i,j)"
  shows "last (mirror2_aux m ps) = (i,m-j)"
  using assms
proof (induction ps)
  case (Cons si ps)
  then show ?case 
    using mirror2_aux_nil Cons by (cases "ps = []") (auto simp: mirror2_square_def)
qed auto

lemma last_mirror2:
  assumes "knights_path (board n m) ps" "last ps = (i,j)"
  shows "last (mirror2 ps) = (i,int m+1-j)"
  unfolding mirror2_def using assms last_mirror2_aux knights_path_non_nil
  by (simp add: knights_path_max2 knights_path_min2)

lemma mirror1_aux_knights_path:
  assumes "knights_path b ps" 
  shows "knights_path (mirror1_board n b) (mirror1_aux n ps)"
  using assms
proof (induction rule: knights_path.induct)
  case (1 si)
  then have "mirror1_board n {si} = {mirror1_square n si}" 
    unfolding mirror1_board_def by blast
  then show ?case by (auto intro: knights_path.intros)
next
  case (2 si b sj ps)
  then have prems: "mirror1_square n si ∉ mirror1_board n b" 
            "valid_step (mirror1_square n si) (mirror1_square n sj)" 
            and "mirror1_aux n (sj#ps) = mirror1_square n sj#mirror1_aux n ps"
    using 2 mirror1_board_iff valid_step_mirror1 by auto
  then show ?case 
    using 2 knights_path.intros(2)[OF prems] insert_mirror1_board by auto
qed

corollary mirror1_knights_path:
  assumes "knights_path (board n m) ps" 
  shows "knights_path (board n m) (mirror1 ps)"
  using assms
proof -
  have [simp]: "min1 ps = 1" "max1 ps = int n"
    using assms knights_path_min1 knights_path_max1 by auto
  then have "mirror1_board (int n+1) (board n m) = (board n m)"
    using mirror1_board_id by auto
  then have "knights_path (board n m) (mirror1_aux (int n+1) ps)"
    using assms mirror1_aux_knights_path[of "board n m" ps "int n+1"] by auto
  then show ?thesis unfolding mirror1_def by auto
qed

lemma mirror2_aux_knights_path:
  assumes "knights_path b ps" 
  shows "knights_path (mirror2_board n b) (mirror2_aux n ps)"
  using assms
proof (induction rule: knights_path.induct)
  case (1 si)
  then have "mirror2_board n {si} = {mirror2_square n si}" 
    unfolding mirror2_board_def by blast
  then show ?case by (auto intro: knights_path.intros)
next
  case (2 si b sj ps)
  then have prems: "mirror2_square n si ∉ mirror2_board n b" 
            "valid_step (mirror2_square n si) (mirror2_square n sj)" 
            and "mirror2_aux n (sj#ps) = mirror2_square n sj#mirror2_aux n ps"
    using 2 mirror2_board_iff valid_step_mirror2 by auto
  then show ?case 
    using 2 knights_path.intros(2)[OF prems] insert_mirror2_board by auto
qed

corollary mirror2_knights_path:
  assumes "knights_path (board n m) ps" 
  shows "knights_path (board n m) (mirror2 ps)"
proof -
  have [simp]: "min2 ps = 1" "max2 ps = int m"
    using assms knights_path_min2 knights_path_max2 by auto
  then have "mirror2_board (int m+1) (board n m) = (board n m)"
    using mirror2_board_id by auto
  then have "knights_path (board n m) (mirror2_aux (int m+1) ps)"
    using assms mirror2_aux_knights_path[of "board n m" ps "int m+1"] by auto
  then show ?thesis unfolding mirror2_def by auto
qed

subsection ‹Rotate Knight's Paths›

text ‹Transposing (@{const transpose}) and mirroring (along first axis ‹mirror1›) a Knight's path 
preserves the Knight's path's property. Tranpose+Mirror1 equals a 90deg-clockwise turn.›
corollary rot90_knights_path:
  assumes "knights_path (board n m) ps" 
  shows "knights_path (board m n) (mirror1 (transpose ps))"
  using assms transpose_knights_path mirror1_knights_path by auto

lemma hd_rot90_knights_path: 
  assumes "knights_path (board n m) ps" "hd ps = (i,j)"
  shows "hd (mirror1 (transpose ps)) = (int m+1-j,i)"
  using assms
proof -
  have "hd (transpose ps) = (j,i)" "knights_path (board m n) (transpose ps)"
    using assms knights_path_non_nil hd_transpose transpose_knights_path 
    by (auto simp: transpose_square_def)
  then show ?thesis using hd_mirror1 by auto
qed

lemma last_rot90_knights_path: 
  assumes "knights_path (board n m) ps" "last ps = (i,j)"
  shows "last (mirror1 (transpose ps)) = (int m+1-j,i)"
  using assms
proof -
  have "last (transpose ps) = (j,i)" "knights_path (board m n) (transpose ps)"
    using assms knights_path_non_nil last_transpose transpose_knights_path 
    by (auto simp: transpose_square_def)
  then show ?thesis using last_mirror1 by auto
qed

section ‹Translating Paths and Boards›

text ‹When constructing knight's paths for larger boards multiple knight's paths for smaller boards
are concatenated. To concatenate paths the the coordinates in the path need to be translated. 
Therefore, simple auxiliary functions are provided.›

subsection ‹Implementation of Path and Board Translation›

text ‹Translate the coordinates for a path by ‹(k1,k2)›.›
fun trans_path :: "int × int ⇒ path ⇒ path" where
  "trans_path (k1,k2) [] = []"
| "trans_path (k1,k2) ((i,j)#xs) = (i+k1,j+k2)#(trans_path (k1,k2) xs)"

text ‹Translate the coordinates of a board by ‹(k1,k2)›.›
definition trans_board :: "int × int ⇒ board ⇒ board" where 
  "trans_board t b ≡ (case t of (k1,k2) ⇒ {(i+k1,j+k2)|i j. (i,j) ∈ b})"

subsection ‹Correctness of Path and Board Translation›

lemma trans_path_length: "length ps = length (trans_path (k1,k2) ps)"
  by (induction ps) auto

lemma trans_path_non_nil: "ps ≠ [] ⟹ trans_path (k1,k2) ps ≠ []"
  by (induction ps) auto

lemma trans_path_correct: "(i,j) ∈ set ps ⟷ (i+k1,j+k2) ∈ set (trans_path (k1,k2) ps)"
proof (induction ps)
  case (Cons si ps)
  then show ?case by (cases si) auto
qed auto

lemma trans_path_non_nil_last: 
  "ps ≠ [] ⟹ last (trans_path (k1,k2) ps) = last (trans_path (k1,k2) ((i,j)#ps))"
  using trans_path_non_nil by (induction ps) auto

lemma hd_trans_path:
  assumes "ps ≠ []" "hd ps = (i,j)"
  shows "hd (trans_path (k1,k2) ps) = (i+k1,j+k2)"
  using assms by (induction ps) auto

lemma last_trans_path:
  assumes "ps ≠ []" "last ps = (i,j)"
  shows "last (trans_path (k1,k2) ps) = (i+k1,j+k2)"
  using assms
proof (induction ps)
  case (Cons si ps)
  then show ?case 
    using trans_path_non_nil_last[symmetric] 
    apply (cases si) 
    apply (cases "ps = []")
    apply auto
    done
qed (auto)

lemma take_trans: 
  shows "take k (trans_path (k1,k2) ps) = trans_path (k1,k2) (take k ps)"
proof (induction ps arbitrary: k)
  case Nil
  then show ?case by auto
next
  case (Cons si ps)
  then obtain i j where "si = (i,j)" by force
  then have "k = 0 ∨ k > 0" by auto
  then show ?case 
  proof (elim disjE)
    assume "k > 0"
    then show ?thesis using Cons.IH by (auto simp: ‹si = (i,j)› take_Cons')
  qed auto
qed

lemma drop_trans: 
  shows "drop k (trans_path (k1,k2) ps) = trans_path (k1,k2) (drop k ps)"
proof (induction ps arbitrary: k)
  case Nil
  then show ?case by auto
next
  case (Cons si ps)
  then obtain i j where "si = (i,j)" by force
  then have "k = 0 ∨ k > 0" by auto
  then show ?case 
  proof (elim disjE)
    assume "k > 0"
    then show ?thesis using Cons.IH by (auto simp: ‹si = (i,j)› drop_Cons')
  qed auto
qed

lemma trans_board_correct: "(i,j) ∈ b ⟷ (i+k1,j+k2) ∈ trans_board (k1,k2) b"
  unfolding trans_board_def by auto

lemma board_subset: "n1 ≤ n2 ⟹ m1 ≤ m2 ⟹ board n1 m1 ⊆ board n2 m2"
  unfolding board_def by auto

text ‹Board concatenation›
corollary board_concat: 
  shows "board n m1 ∪ trans_board (0,int m1) (board n m2) = board n (m1+m2)" (is "?b1 ∪ ?b2 = ?b")
proof
  show "?b1 ∪ ?b2 ⊆ ?b" unfolding board_def trans_board_def by auto
next
  show "?b ⊆ ?b1 ∪ ?b2"
  proof
    fix x
    assume "x ∈ ?b"
    then obtain i j where x_split: "x = (i,j)" "1 ≤ i ∧ i ≤ int n" "1 ≤ j ∧ j ≤ int (m1+m2)" 
      unfolding board_def by auto
    then have "j ≤ int m1 ∨ (int m1 < j ∧ j ≤ int (m1+m2))" by auto
    then show "x ∈ ?b1 ∪ ?b2"
    proof
      assume "j ≤ int m1"
      then show "x ∈ ?b1 ∪ ?b2" using x_split unfolding board_def by auto
    next
      assume asm: "int m1 < j ∧ j ≤ int (m1+m2)"
      then have "(i,j-int m1) ∈ board n m2" using x_split unfolding board_def by auto
      then show "x ∈ ?b1 ∪ ?b2" 
        using x_split asm trans_board_correct[of i "j-int m1" "board n m2" 0 "int m1"] by auto
    qed
  qed
qed

lemma transpose_trans_board: 
  "transpose_board (trans_board (k1,k2) b) = trans_board (k2,k1) (transpose_board b)"
  unfolding transpose_board_def trans_board_def by blast

corollary board_concatT: 
  shows "board n1 m ∪ trans_board (int n1,0) (board n2 m) = board (n1+n2) m" (is "?b1 ∪ ?b2 = ?b")
proof -
  let ?b1T="board m n1"
  let ?b2T="trans_board (0,int n1) (board m n2)"
  have "?b1 ∪ ?b2 = transpose_board (?b1T ∪ ?b2T) "
    using transpose_board2 transpose_union transpose_board transpose_trans_board by auto
  also have "... = transpose_board (board m (n1+n2))"
    using board_concat by auto
  also have "... = board (n1+n2) m"
    using transpose_board by auto
  finally show ?thesis .
qed

lemma trans_valid_step: 
  "valid_step (i,j) (i',j') ⟹ valid_step (i+k1,j+k2) (i'+k1,j'+k2)"
  unfolding valid_step_def by auto

text ‹Translating a path and a boards preserves the validity.›
lemma trans_knights_path:
  assumes "knights_path b ps"
  shows "knights_path (trans_board (k1,k2) b) (trans_path (k1,k2) ps)"
  using assms
proof (induction rule: knights_path.induct)
  case (2 si b sj xs)
  then obtain i j i' j' where split: "si = (i,j)" "sj = (i',j')" by force
  let ?si="(i+k1,j+k2)"
  let ?sj="(i'+k1,j'+k2)"
  let ?xs="trans_path (k1,k2) xs"
  let ?b="trans_board (k1,k2) b"
  have simps: "trans_path (k1,k2) (si#sj#xs) = ?si#?sj#?xs" 
              "?b ∪ {?si} = trans_board (k1,k2) (b ∪ {si})"
    unfolding trans_board_def using split by auto
  have "?si ∉ ?b" "valid_step ?si ?sj" "knights_path ?b (?sj#?xs)"
    using 2 split trans_valid_step by (auto simp: trans_board_def)
  then have "knights_path (?b ∪ {?si}) (?si#?sj#?xs)"
    using knights_path.intros by auto
  then show ?case using simps by auto
qed (auto simp: trans_board_def intro: knights_path.intros)

text ‹Predicate that indicates if two squares ‹si› and ‹sj› are adjacent in ‹ps›.›
definition step_in :: "path ⇒ square ⇒ square ⇒ bool" where
  "step_in ps si sj ≡ (∃k. 0 < k ∧ k < length ps ∧ last (take k ps) = si ∧ hd (drop k ps) = sj)"

lemma step_in_Cons: "step_in ps si sj ⟹ step_in (sk#ps) si sj"
proof -
  assume "step_in ps si sj"
  then obtain k where "0 < k ∧ k < length ps" "last (take k ps) = si" "hd (drop k ps) = sj"
    unfolding step_in_def by auto 
  then have "0 < k+1 ∧ k+1 < length (sk#ps)" 
      "last (take (k+1) (sk#ps)) = si" "hd (drop (k+1) (sk#ps)) = sj"
    by auto
  then show ?thesis
    by (auto simp: step_in_def)
qed

lemma step_in_append: "step_in ps si sj ⟹ step_in (ps@ps') si sj"
proof -
  assume "step_in ps si sj"
  then obtain k where "0 < k ∧ k < length ps" "last (take k ps) = si" "hd (drop k ps) = sj"
    unfolding step_in_def by auto 
  then have "0 < k ∧ k < length (ps@ps')" 
      "last (take k (ps@ps')) = si" "hd (drop k (ps@ps')) = sj"
    by auto
  then show ?thesis
    by (auto simp: step_in_def)
qed

lemma step_in_prepend: "step_in ps si sj ⟹ step_in (ps'@ps) si sj"
  using step_in_Cons by (induction ps' arbitrary: ps) auto

lemma step_in_valid_step: "knights_path b ps ⟹ step_in ps si sj ⟹ valid_step si sj"
proof -
  assume assms: "knights_path b ps" "step_in ps si sj"
  then obtain k where k_prems: "0 < k ∧ k < length ps" "last (take k ps) = si" "hd (drop k ps) = sj"
    unfolding step_in_def by auto
  then have "k = 1 ∨ k > 1" by auto
  then show ?thesis
  proof (elim disjE)
    assume "k = 1"
    then obtain ps' where "ps = si#sj#ps'"
      using k_prems list_len_g_1_split by fastforce
    then show ?thesis
      using assms by (auto elim: knights_path.cases)
  next
    assume "k > 1"
    then have "0 < k-1 ∧ k-1 < length ps"
      using k_prems by auto
    then obtain b where "knights_path b (drop (k-1) ps)"
      using assms knights_path_split by blast

    obtain ps' where "drop (k-1) ps = si#sj#ps'"
      using k_prems ‹0 < k - 1 ∧ k - 1 < length ps›
      by (metis Cons_nth_drop_Suc Suc_diff_1 hd_drop_conv_nth last_snoc take_hd_drop)
    then show ?thesis
      using ‹knights_path b (drop (k-1) ps)› by (auto elim: knights_path.cases)
  qed
qed

lemma trans_step_in: 
  "step_in ps (i,j) (i',j') ⟹ step_in (trans_path (k1,k2) ps) (i+k1,j+k2) (i'+k1,j'+k2)"
proof -
  let ?ps'="trans_path (k1,k2) ps"
  assume "step_in ps (i,j) (i',j')"
  then obtain k where "0 < k ∧ k < length ps" "last (take k ps) = (i,j)" "hd (drop k ps) = (i',j')"
    unfolding step_in_def by auto
  then have "take k ps ≠ []" "drop k ps ≠ []" by fastforce+
  then have "0 < k ∧ k < length ?ps'" 
      "last (take k ?ps') = (i+k1,j+k2)" "hd (drop k ?ps') = (i'+k1,j'+k2)"
    using trans_path_length
          last_trans_path[OF ‹take k ps ≠ []› ‹last (take k ps) = (i,j)›] take_trans 
          hd_trans_path[OF ‹drop k ps ≠ []› ‹hd (drop k ps) = (i',j')›] drop_trans
    by auto
  then show ?thesis
    by (auto simp: step_in_def) 
qed

lemma transpose_step_in: 
  "step_in ps si sj ⟹ step_in (transpose ps) (transpose_square si) (transpose_square sj)"
  (is "_ ⟹ step_in ?psT ?siT ?sjT")
proof -
  assume "step_in ps si sj"
  then obtain k where 
      k_prems: "0 < k" "k < length ps" "last (take k ps) = si" "hd (drop k ps) = sj"
    unfolding step_in_def by auto
  then have non_nil: "take k ps ≠ []" "drop k ps ≠ []" by fastforce+
  have "take k ?psT = transpose (take k ps)" "drop k ?psT = transpose (drop k ps)"
    using take_transpose drop_transpose by auto
  then have "last (take k ?psT) = ?siT" "hd (drop k ?psT) = ?sjT"
    using non_nil k_prems hd_transpose last_transpose by auto
  then show "step_in ?psT ?siT ?sjT"
    unfolding step_in_def using k_prems transpose_length by auto
qed
  
lemma hd_take: "0 < k ⟹ hd xs = hd (take k xs)"
  by (induction xs) auto

lemma last_drop: "k < length xs ⟹ last xs = last (drop k xs)"
  by (induction xs) auto

subsection ‹Concatenate Knight's Paths and Circuits›

text ‹Concatenate two knight's path on a ‹n×m›-board along the 2nd axis if the first path contains
the step ‹si → sj› and there are valid steps ‹si → hd ps2'› and ‹sj → last ps2'›, where 
‹ps2'› is ‹ps2› is translated by ‹m1›. An arbitrary step in ‹ps2› is preserved.›
corollary knights_path_split_concat_si_prev:
  assumes "knights_path (board n m1) ps1" "knights_path (board n m2) ps2" 
          "step_in ps1 si sj" "hd ps2 = (ih,jh)" "last ps2 = (il,jl)" "step_in ps2 (i,j) (i',j')"
          "valid_step si (ih,int m1+jh)" "valid_step (il,int m1+jl) sj"
  shows "∃ps. knights_path (board n (m1+m2)) ps ∧ hd ps = hd ps1  
    ∧ last ps = last ps1 ∧ step_in ps (i,int m1+j) (i',int m1+j')"
  using assms
proof -
  let ?b1="board n m1"
  let ?b2="board n m2"
  let ?ps2'="trans_path (0,int m1) ps2"
  let ?b'="trans_board (0,int m1) ?b2"
  have kp2': "knights_path ?b' ?ps2'" using assms trans_knights_path by auto
  then have "?ps2' ≠ []" using knights_path_non_nil by auto

  obtain k where k_prems: 
    "0 < k" "k < length ps1" "last (take k ps1) = si" "hd (drop k ps1) = sj"
    using assms unfolding step_in_def by auto
  let ?ps="(take k ps1) @ ?ps2' @ (drop k ps1)"
  obtain b1 b2 where b_prems: "knights_path b1 (take k ps1)" "knights_path b2 (drop k ps1)" 
      "b1 ∪ b2 = ?b1" "b1 ∩ b2 = {}"
    using assms ‹0 < k› ‹k < length ps1› knights_path_split by blast

  have "hd ?ps2' = (ih,int m1+jh)" "last ?ps2' = (il,int m1+jl)"
    using assms knights_path_non_nil hd_trans_path last_trans_path by auto
  then have "hd ?ps2' = (ih,int m1+jh)" "last ((take k ps1) @ ?ps2') = (il,int m1+jl)"
    using ‹?ps2' ≠ []› by auto
  then have vs: "valid_step (last (take k ps1)) (hd ?ps2')" 
      "valid_step (last ((take k ps1) @ ?ps2')) (hd (drop k ps1))"
    using assms k_prems by auto

  have "?b1 ∩ ?b' = {}" unfolding board_def trans_board_def by auto
  then have "b1 ∩ ?b' = {} ∧ (b1 ∪ ?b') ∩ b2 = {}" using b_prems by blast
  then have inter_empty: "b1 ∩ ?b' = {}" "(b1 ∪ ?b') ∩ b2 = {}" by auto

  have "knights_path (b1 ∪ ?b') ((take k ps1) @ ?ps2')"
    using kp2' b_prems inter_empty vs knights_path_append by auto
  then have "knights_path (b1 ∪ ?b' ∪ b2) ?ps"
    using b_prems inter_empty vs knights_path_append[where ps1="(take k ps1) @ ?ps2'"] by auto
  then have "knights_path (?b1 ∪ ?b') ?ps" 
    using b_prems Un_commute Un_assoc by metis
  then have kp: "knights_path (board n (m1+m2)) ?ps"
    using board_concat[of n m1 m2] by auto

  have hd: "hd ?ps = hd ps1"
    using assms ‹0 < k› knights_path_non_nil hd_take by auto

  have last: "last ?ps = last ps1"
    using assms ‹k < length ps1› knights_path_non_nil last_drop by auto

  have m_simps: "j+int m1 = int m1+j" "j'+int m1 = int m1+j'" by auto
  have si: "step_in ?ps (i,int m1+j) (i',int m1+j')"
    using assms step_in_append[OF step_in_prepend[OF trans_step_in], 
                  of ps2 i j i' j' "take k ps1" 0 "int m1" "drop k ps1"] 
    by (auto simp: m_simps)
  
  show ?thesis using kp hd last si by auto
qed

lemma len1_hd_last: "length xs = 1 ⟹ hd xs = last xs"
  by (induction xs) auto

text ‹Weaker version of @{thm knights_path_split_concat_si_prev}.›
corollary knights_path_split_concat:
  assumes "knights_path (board n m1) ps1" "knights_path (board n m2) ps2" 
          "step_in ps1 si sj" "hd ps2 = (ih,jh)" "last ps2 = (il,jl)"
          "valid_step si (ih,int m1+jh)" "valid_step (il,int m1+jl) sj"
  shows "∃ps. knights_path (board n (m1+m2)) ps ∧ hd ps = hd ps1 ∧ last ps = last ps1"
proof -
  have "length ps2 = 1 ∨ length ps2 > 1"
    using assms knights_path_non_nil by (meson length_0_conv less_one linorder_neqE_nat)
  then show ?thesis
  proof (elim disjE)
    let ?sk="(ih,int m1+jh)"
    assume "length ps2 = 1"
    (* contradiction *)
    then have "(ih,jh) = (il,jl)"
      using assms len1_hd_last by metis
    then have "valid_step si ?sk" "valid_step ?sk sj" "valid_step si sj"
      using assms step_in_valid_step by auto
    then show ?thesis
      using valid_step_non_transitive by blast
  next
    assume "length ps2 > 1"
    then obtain i1 j1 i2 j2 ps2' where "ps2 = (i1,j1)#(i2,j2)#ps2'"
      using list_len_g_1_split by fastforce
    then have "last (take 1 ps2) = (i1,j1)" "hd (drop 1 ps2) = (i2,j2)" by auto
    then have "step_in ps2 (i1,j1) (i2,j2)" using ‹length ps2 > 1› by (auto simp: step_in_def)
    then show ?thesis
      using assms knights_path_split_concat_si_prev by blast
  qed
qed

text ‹Concatenate two knight's path on a ‹n×m›-board along the 1st axis.›
corollary knights_path_split_concatT:
  assumes "knights_path (board n1 m) ps1" "knights_path (board n2 m) ps2" 
          "step_in ps1 si sj" "hd ps2 = (ih,jh)" "last ps2 = (il,jl)"
          "valid_step si (int n1+ih,jh)" "valid_step (int n1+il,jl) sj"
  shows "∃ps. knights_path (board (n1+n2) m) ps ∧ hd ps = hd ps1 ∧ last ps = last ps1"
  using assms
proof -
  let ?ps1T="transpose ps1"
  let ?ps2T="transpose ps2"
  have kps: "knights_path (board m n1) ?ps1T" "knights_path (board m n2) ?ps2T"
    using assms transpose_knights_path by auto

  let ?siT="transpose_square si"
  let ?sjT="transpose_square sj"
  have si: "step_in ?ps1T ?siT ?sjT"
    using assms transpose_step_in by auto

  have "ps1 ≠ []" "ps2 ≠ []"
    using assms knights_path_non_nil by auto
  then have hd_last2: "hd ?ps2T = (jh,ih)" "last ?ps2T = (jl,il)"
    using assms hd_transpose last_transpose by (auto simp: transpose_square_def)

  have vs: "valid_step ?siT (jh,int n1+ih)" "valid_step (jl,int n1+il) ?sjT"
    using assms transpose_valid_step by (auto simp: transpose_square_def split: prod.splits)

  then obtain ps where 
    ps_prems: "knights_path (board m (n1+n2)) ps" "hd ps = hd ?ps1T" "last ps = last ?ps1T"
    using knights_path_split_concat[OF kps si hd_last2 vs] by auto
  then have "ps ≠ []" using knights_path_non_nil by auto
  let ?psT="transpose ps"
  have "knights_path (board (n1+n2) m) ?psT" "hd ?psT = hd ps1" "last ?psT = last ps1"
    using ‹ps1 ≠ []› ‹ps ≠ []› ps_prems transpose_knights_path hd_transpose last_transpose 
    by (auto simp: transpose2)
  then show ?thesis by auto
qed

text ‹Concatenate two Knight's path along the 2nd axis. There is a valid step from the last square 
in the first Knight's path ‹ps1› to the first square in the second Knight's path ‹ps2›.›
corollary knights_path_concat:
  assumes "knights_path (board n m1) ps1" "knights_path (board n m2) ps2" 
          "hd ps2 = (ih,jh)" "valid_step (last ps1) (ih,int m1+jh)"
  shows "knights_path (board n (m1+m2)) (ps1 @ (trans_path (0,int m1) ps2))"
proof -
  let ?ps2'="trans_path (0,int m1) ps2"
  let ?b="trans_board (0,int m1) (board n m2)"
  have inter_empty: "board n m1 ∩ ?b = {}"
    unfolding board_def trans_board_def by auto
  have "hd ?ps2' = (ih,int m1+jh)"
    using assms knights_path_non_nil hd_trans_path by auto
  then have kp: "knights_path (board n m1) ps1" "knights_path ?b ?ps2'" and 
        vs: "valid_step (last ps1) (hd ?ps2')"
    using assms trans_knights_path by auto
  then show "knights_path (board n (m1+m2)) (ps1 @ ?ps2')"
    using knights_path_append[OF kp inter_empty vs] board_concat by auto
qed

text ‹Concatenate two Knight's path along the 2nd axis. The first Knight's path end in 
‹(2,m1-1)› (lower-right) and the second Knight's paths start in ‹(1,1)› (lower-left).›
corollary knights_path_lr_concat:
  assumes "knights_path (board n m1) ps1" "knights_path (board n m2) ps2" 
          "last ps1 = (2,int m1-1)" "hd ps2 = (1,1)"
  shows "knights_path (board n (m1+m2)) (ps1 @ (trans_path (0,int m1) ps2))"
proof -
  have "valid_step (last ps1) (1,int m1+1)"
    using assms unfolding valid_step_def by auto
  then show ?thesis
    using assms knights_path_concat by auto
qed

text ‹Concatenate two Knight's circuits along the 2nd axis. In the first Knight's path the 
squares ‹(2,m1-1)› and ‹(4,m1)› are adjacent and the second Knight's cirucit starts in ‹(1,1)› 
(lower-left) and end in ‹(3,2)›.›
corollary knights_circuit_lr_concat:
  assumes "knights_circuit (board n m1) ps1" "knights_circuit (board n m2) ps2"
          "step_in ps1 (2,int m1-1) (4,int m1)" 
          "hd ps2 = (1,1)" "last ps2 = (3,2)" "step_in ps2 (2,int m2-1) (4,int m2)"
  shows "∃ps. knights_circuit (board n (m1+m2)) ps ∧ step_in ps (2,int (m1+m2)-1) (4,int (m1+m2))"
proof -
  have kp1: "knights_path (board n m1) ps1" and kp2: "knights_path (board n m2) ps2" 
    and vs: "valid_step (last ps1) (hd ps1)"
    using assms unfolding knights_circuit_def by auto

  have m_simps: "int m1 + (int m2-1) = int (m1+m2)-1" "int m1 + int m2 = int (m1+m2)" by auto

  have "valid_step (2,int m1-1) (1,int m1+1)" "valid_step (3,int m1+2) (4,int m1)"
    unfolding valid_step_def by auto
  then obtain ps where "knights_path (board n (m1+m2)) ps" "hd ps = hd ps1" "last ps = last ps1" and 
      si: "step_in ps (2,int (m1+m2)-1) (4,int (m1+m2))"
    using assms kp1 kp2 
          knights_path_split_concat_si_prev[of n m1 ps1 m2 ps2 "(2,int m1-1)" 
                                              "(4,int m1)" 1 1 3 2 2 "int m2-1" 4 "int m2"] 
    by (auto simp only: m_simps)
  then have "knights_circuit (board n (m1+m2)) ps"
    using vs by (auto simp: knights_circuit_def)
  then show ?thesis
    using si by auto
qed

section ‹Parsing Paths›

text ‹In this section functions are implemented to parse and construct paths. The parser converts 
the matrix representation (‹(nat list) list›) used in cite‹"cull_decurtins_1987"› to a path 
(‹path›).›

text ‹for debugging›
fun test_path :: "path ⇒ bool" where
  "test_path (si#sj#xs) = (step_checker si sj ∧ test_path (sj#xs))"
| "test_path _ = True"

fun f_opt :: "('a ⇒ 'a) ⇒ 'a option ⇒ 'a option" where
  "f_opt _ None = None"
| "f_opt f (Some a) = Some (f a)"

fun add_opt_fst_sq :: "int ⇒ square option ⇒ square option" where
  "add_opt_fst_sq _ None = None"
| "add_opt_fst_sq k (Some (i,j)) = Some (k+i,j)"

fun find_k_in_col :: "nat ⇒ nat list ⇒ int option" where
  "find_k_in_col k [] = None"
| "find_k_in_col k (c#cs) = (if c = k then Some 1 else f_opt ((+) 1) (find_k_in_col k cs))"

fun find_k_sqr :: "nat ⇒ (nat list) list ⇒ square option" where
  "find_k_sqr k [] = None"
| "find_k_sqr k (r#rs) = (case find_k_in_col k r of 
      None ⇒ f_opt (λ(i,j). (i+1,j)) (find_k_sqr k rs)
    | Some j ⇒ Some (1,j))"

text ‹Auxiliary function to easily parse pre-computed boards from paper.›
fun to_sqrs :: "nat ⇒ (nat list) list ⇒ path option" where
  "to_sqrs 0 rs = Some []"
| "to_sqrs k rs = (case find_k_sqr k rs of
      None ⇒ None
    | Some si ⇒ f_opt (λps. ps@[si]) (to_sqrs (k-1) rs))"

fun num_elems :: "(nat list) list ⇒ nat" where
  "num_elems (r#rs) = length r * length (r#rs)"

text ‹Convert a matrix (‹nat list list›) to a path (‹path›). With this function we implicitly 
define the lower-left corner to be ‹(1,1)› and the upper-right corner to be ‹(n,m)›.›
definition "to_path rs ≡ to_sqrs (num_elems rs) (rev rs)"

text ‹Example›
value "to_path 
  [[3,22,13,16,5],
  [12,17,4,21,14],
  [23,2,15,6,9],
  [18,11,8,25,20],
  [1,24,19,10,7::nat]]"

section ‹Knight's Paths for ‹5×m›-Boards›

text ‹Given here are knight's paths, ‹kp5xmlr› and ‹kp5xmur›, for the ‹(5×m)›-board that start 
in the lower-left corner for ‹m∈{5,6,7,8,9}›. The path ‹kp5xmlr› ends in the lower-right corner, 
whereas the path ‹kp5xmur› ends in the upper-right corner. 
The tables show the visited squares numbered in ascending order.›

abbreviation "b5x5 ≡ board 5 5"

text ‹A Knight's path for the ‹(5×5)›-board that starts in the lower-left and ends in the 
lower-right.
  \begin{table}[H]
    \begin{tabular}{lllll}
       3 & 22 & 13 & 16 &  5 \\
      12 & 17 &  4 & 21 & 14 \\
      23 &  2 & 15 &  6 &  9 \\
      18 & 11 &  8 & 25 & 20 \\
       1 & 24 & 19 & 10 &  7
    \end{tabular}
  \end{table}›
abbreviation "kp5x5lr ≡ the (to_path 
  [[3,22,13,16,5],
  [12,17,4,21,14],
  [23,2,15,6,9],
  [18,11,8,25,20],
  [1,24,19,10,7]])"
lemma kp_5x5_lr: "knights_path b5x5 kp5x5lr"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x5_lr_hd: "hd kp5x5lr = (1,1)" by eval

lemma kp_5x5_lr_last: "last kp5x5lr = (2,4)" by eval

lemma kp_5x5_lr_non_nil: "kp5x5lr ≠ []" by eval

text ‹A Knight's path for the ‹(5×5)›-board that starts in the lower-left and ends in the 
upper-right.
  \begin{table}[H]
    \begin{tabular}{lllll}
       7 & 12 & 15 & 20 &  5 \\
      16 & 21 &  6 & 25 & 14 \\
      11 &  8 & 13 &  4 & 19 \\
      22 & 17 &  2 &  9 & 24 \\
       1 & 10 & 23 & 18 &  3
    \end{tabular}
  \end{table}›
abbreviation "kp5x5ur ≡ the (to_path 
  [[7,12,15,20,5],
  [16,21,6,25,14],
  [11,8,13,4,19],
  [22,17,2,9,24],
  [1,10,23,18,3]])"
lemma kp_5x5_ur: "knights_path b5x5 kp5x5ur"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x5_ur_hd: "hd kp5x5ur = (1,1)" by eval

lemma kp_5x5_ur_last: "last kp5x5ur = (4,4)" by eval

lemma kp_5x5_ur_non_nil: "kp5x5ur ≠ []" by eval

abbreviation "b5x6 ≡ board 5 6"

text ‹A Knight's path for the ‹(5×6)›-board that starts in the lower-left and ends in the 
lower-right.
  \begin{table}[H]
    \begin{tabular}{llllll}
       7 & 14 & 21 & 28 &  5 & 12 \\
      22 & 27 &  6 & 13 & 20 & 29 \\
      15 &  8 & 17 & 24 & 11 &  4 \\
      26 & 23 &  2 &  9 & 30 & 19 \\
       1 & 16 & 25 & 18 &  3 & 10
    \end{tabular}
  \end{table}›
abbreviation "kp5x6lr ≡ the (to_path 
  [[7,14,21,28,5,12],
  [22,27,6,13,20,29],
  [15,8,17,24,11,4],
  [26,23,2,9,30,19],
  [1,16,25,18,3,10]])"
lemma kp_5x6_lr: "knights_path b5x6 kp5x6lr"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x6_lr_hd: "hd kp5x6lr = (1,1)" by eval

lemma kp_5x6_lr_last: "last kp5x6lr = (2,5)" by eval

lemma kp_5x6_lr_non_nil: "kp5x6lr ≠ []" by eval

text ‹A Knight's path for the ‹(5×6)›-board that starts in the lower-left and ends in the 
upper-right.
  \begin{table}[H]
    \begin{tabular}{llllll}
       3 & 10 & 29 & 20 &  5 & 12 \\
      28 & 19 &  4 & 11 & 30 & 21 \\
       9 &  2 & 17 & 24 & 13 &  6 \\
      18 & 27 &  8 & 15 & 22 & 25 \\
       1 & 16 & 23 & 26 &  7 & 14
    \end{tabular}
  \end{table}›
abbreviation "kp5x6ur ≡ the (to_path 
  [[3,10,29,20,5,12],
  [28,19,4,11,30,21],
  [9,2,17,24,13,6],
  [18,27,8,15,22,25],
  [1,16,23,26,7,14]])"
lemma kp_5x6_ur: "knights_path b5x6 kp5x6ur"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x6_ur_hd: "hd kp5x6ur = (1,1)" by eval

lemma kp_5x6_ur_last: "last kp5x6ur = (4,5)" by eval

lemma kp_5x6_ur_non_nil: "kp5x6ur ≠ []" by eval

abbreviation "b5x7 ≡ board 5 7"

text ‹A Knight's path for the ‹(5×7)›-board that starts in the lower-left and ends in the 
lower-right.
  \begin{table}[H]
    \begin{tabular}{lllllll}
       3 & 12 & 21 & 30 &  5 & 14 & 23 \\
      20 & 29 &  4 & 13 & 22 & 31 &  6 \\
      11 &  2 & 19 & 32 &  7 & 24 & 15 \\
      28 & 33 & 10 & 17 & 26 & 35 &  8 \\
       1 & 18 & 27 & 34 &  9 & 16 & 25
    \end{tabular}
  \end{table}›
abbreviation "kp5x7lr ≡ the (to_path 
  [[3,12,21,30,5,14,23],
  [20,29,4,13,22,31,6],
  [11,2,19,32,7,24,15],
  [28,33,10,17,26,35,8],
  [1,18,27,34,9,16,25]])"
lemma kp_5x7_lr: "knights_path b5x7 kp5x7lr"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x7_lr_hd: "hd kp5x7lr = (1,1)" by eval

lemma kp_5x7_lr_last: "last kp5x7lr = (2,6)" by eval

lemma kp_5x7_lr_non_nil: "kp5x7lr ≠ []" by eval

text ‹A Knight's path for the ‹(5×7)›-board that starts in the lower-left and ends in the 
upper-right.
  \begin{table}[H]
    \begin{tabular}{lllllll}
       3 & 32 & 11 & 34 &  5 & 26 & 13 \\
      10 & 19 &  4 & 25 & 12 & 35 &  6 \\
      31 &  2 & 33 & 20 & 23 & 14 & 27 \\
      18 &  9 & 24 & 29 & 16 &  7 & 22 \\
       1 & 30 & 17 &  8 & 21 & 28 & 15
    \end{tabular}
  \end{table}›
abbreviation "kp5x7ur ≡ the (to_path 
  [[3,32,11,34,5,26,13],
  [10,19,4,25,12,35,6],
  [31,2,33,20,23,14,27],
  [18,9,24,29,16,7,22],
  [1,30,17,8,21,28,15]])"
lemma kp_5x7_ur: "knights_path b5x7 kp5x7ur"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x7_ur_hd: "hd kp5x7ur = (1,1)" by eval

lemma kp_5x7_ur_last: "last kp5x7ur = (4,6)" by eval

lemma kp_5x7_ur_non_nil: "kp5x7ur ≠ []" by eval

abbreviation "b5x8 ≡ board 5 8"

text ‹A Knight's path for the ‹(5×8)›-board that starts in the lower-left and ends in the 
lower-right.
  \begin{table}[H]
    \begin{tabular}{llllllll}
       3 & 12 & 37 & 26 &  5 & 14 & 17 & 28 \\
      34 & 23 &  4 & 13 & 36 & 27 &  6 & 15 \\
      11 &  2 & 35 & 38 & 25 & 16 & 29 & 18 \\
      22 & 33 & 24 &  9 & 20 & 31 & 40 &  7 \\
       1 & 10 & 21 & 32 & 39 &  8 & 19 & 30
    \end{tabular}
  \end{table}›
abbreviation "kp5x8lr ≡ the (to_path 
  [[3,12,37,26,5,14,17,28],
  [34,23,4,13,36,27,6,15],
  [11,2,35,38,25,16,29,18],
  [22,33,24,9,20,31,40,7],
  [1,10,21,32,39,8,19,30]])"
lemma kp_5x8_lr: "knights_path b5x8 kp5x8lr"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x8_lr_hd: "hd kp5x8lr = (1,1)" by eval

lemma kp_5x8_lr_last: "last kp5x8lr = (2,7)" by eval

lemma kp_5x8_lr_non_nil: "kp5x8lr ≠ []" by eval

text ‹A Knight's path for the ‹(5×8)›-board that starts in the lower-left and ends in the 
upper-right.
  \begin{table}[H]
    \begin{tabular}{llllllll}
      33 &  8 & 17 & 38 & 35 &  6 & 15 & 24 \\
      18 & 37 & 34 &  7 & 16 & 25 & 40 &  5 \\
       9 & 32 & 29 & 36 & 39 & 14 & 23 & 26 \\
      30 & 19 &  2 & 11 & 28 & 21 &  4 & 13 \\
       1 & 10 & 31 & 20 &  3 & 12 & 27 & 22
    \end{tabular}
  \end{table}›
abbreviation "kp5x8ur ≡ the (to_path 
  [[33,8,17,38,35,6,15,24],
  [18,37,34,7,16,25,40,5],
  [9,32,29,36,39,14,23,26],
  [30,19,2,11,28,21,4,13],
  [1,10,31,20,3,12,27,22]])"
lemma kp_5x8_ur: "knights_path b5x8 kp5x8ur"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x8_ur_hd: "hd kp5x8ur = (1,1)" by eval

lemma kp_5x8_ur_last: "last kp5x8ur = (4,7)" by eval

lemma kp_5x8_ur_non_nil: "kp5x8ur ≠ []" by eval

abbreviation "b5x9 ≡ board 5 9"

text ‹
  A Knight's path for the ‹(5×9)›-board that starts in the lower-left and ends in the lower-right.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
       9 &  4 & 11 & 16 & 23 & 42 & 33 & 36 & 25 \\
      12 & 17 &  8 &  3 & 32 & 37 & 24 & 41 & 34 \\
       5 & 10 & 15 & 20 & 43 & 22 & 35 & 26 & 29 \\
      18 & 13 &  2 &  7 & 38 & 31 & 28 & 45 & 40 \\
       1 &  6 & 19 & 14 & 21 & 44 & 39 & 30 & 27
    \end{tabular}
  \end{table}›
abbreviation "kp5x9lr ≡ the (to_path 
  [[9,4,11,16,23,42,33,36,25],
  [12,17,8,3,32,37,24,41,34],
  [5,10,15,20,43,22,35,26,29],
  [18,13,2,7,38,31,28,45,40],
  [1,6,19,14,21,44,39,30,27]])"
lemma kp_5x9_lr: "knights_path b5x9 kp5x9lr"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x9_lr_hd: "hd kp5x9lr = (1,1)" by eval

lemma kp_5x9_lr_last: "last kp5x9lr = (2,8)" by eval

lemma kp_5x9_lr_non_nil: "kp5x9lr ≠ []" by eval

text ‹
  A Knight's path for the ‹(5×9)›-board that starts in the lower-left and ends in the upper-right.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
       9 &  4 & 11 & 16 & 27 & 32 & 35 & 40 & 25 \\
      12 & 17 &  8 &  3 & 36 & 41 & 26 & 45 & 34 \\
       5 & 10 & 15 & 20 & 31 & 28 & 33 & 24 & 39 \\
      18 & 13 &  2 &  7 & 42 & 37 & 22 & 29 & 44 \\
       1 &  6 & 19 & 14 & 21 & 30 & 43 & 38 & 23
    \end{tabular}
  \end{table}›
abbreviation "kp5x9ur ≡ the (to_path 
  [[9,4,11,16,27,32,35,40,25],
  [12,17,8,3,36,41,26,45,34],
  [5,10,15,20,31,28,33,24,39],
  [18,13,2,7,42,37,22,29,44],
  [1,6,19,14,21,30,43,38,23]])"
lemma kp_5x9_ur: "knights_path b5x9 kp5x9ur"
  by (simp only: knights_path_exec_simp) eval

lemma kp_5x9_ur_hd: "hd kp5x9ur = (1,1)" by eval

lemma kp_5x9_ur_last: "last kp5x9ur = (4,8)" by eval

lemma kp_5x9_ur_non_nil: "kp5x9ur ≠ []" by eval

lemmas kp_5xm_lr = 
  kp_5x5_lr kp_5x5_lr_hd kp_5x5_lr_last kp_5x5_lr_non_nil
  kp_5x6_lr kp_5x6_lr_hd kp_5x6_lr_last kp_5x6_lr_non_nil
  kp_5x7_lr kp_5x7_lr_hd kp_5x7_lr_last kp_5x7_lr_non_nil
  kp_5x8_lr kp_5x8_lr_hd kp_5x8_lr_last kp_5x8_lr_non_nil
  kp_5x9_lr kp_5x9_lr_hd kp_5x9_lr_last kp_5x9_lr_non_nil

lemmas kp_5xm_ur = 
  kp_5x5_ur kp_5x5_ur_hd kp_5x5_ur_last kp_5x5_ur_non_nil
  kp_5x6_ur kp_5x6_ur_hd kp_5x6_ur_last kp_5x6_ur_non_nil
  kp_5x7_ur kp_5x7_ur_hd kp_5x7_ur_last kp_5x7_ur_non_nil
  kp_5x8_ur kp_5x8_ur_hd kp_5x8_ur_last kp_5x8_ur_non_nil
  kp_5x9_ur kp_5x9_ur_hd kp_5x9_ur_last kp_5x9_ur_non_nil

text ‹For every ‹5×m›-board with ‹m ≥ 5› there exists a knight's path that starts in 
‹(1,1)› (bottom-left) and ends in ‹(2,m-1)› (bottom-right).›
lemma knights_path_5xm_lr_exists: 
  assumes "m ≥ 5" 
  shows "∃ps. knights_path (board 5 m) ps ∧ hd ps = (1,1) ∧ last ps = (2,int m-1)"
  using assms
proof (induction m rule: less_induct)
  case (less m)
  then have "m ∈ {5,6,7,8,9} ∨ 5 ≤ m-5" by auto
  then show ?case
  proof (elim disjE)
    assume "m ∈ {5,6,7,8,9}"
    then show ?thesis using kp_5xm_lr by fastforce
  next
    assume m_ge: "5 ≤ m-5" (* ⟷ 10 ≤ m *)
    then obtain ps1 where ps1_IH: "knights_path (board 5 (m-5)) ps1" "hd ps1 = (1,1)" 
                                "last ps1 = (2,int (m-5)-1)" "ps1 ≠ []"
      using less.IH[of "m-5"] knights_path_non_nil by auto

    let ?ps2="kp5x5lr"
    let ?ps2'="ps1 @ trans_path (0,int (m-5)) ?ps2"
    have "knights_path b5x5 ?ps2" "hd ?ps2 = (1, 1)" "?ps2 ≠ []" "last ?ps2 = (2,4)"
      using kp_5xm_lr by auto
    then have 1: "knights_path (board 5 m) ?ps2'"         
      using m_ge ps1_IH knights_path_lr_concat[of 5 "m-5" ps1 5 ?ps2] by auto

    have 2: "hd ?ps2' = (1,1)" using ps1_IH by auto

    have "last (trans_path (0,int (m-5)) ?ps2) = (2,int m-1)"
      using m_ge last_trans_path[OF ‹?ps2 ≠ []› ‹last ?ps2 = (2,4)›] by auto
    then have 3: "last ?ps2' = (2,int m-1)"
      using last_appendR[OF trans_path_non_nil[OF ‹?ps2 ≠ []›],symmetric] by metis
    
    show ?thesis using 1 2 3 by auto
  qed
qed

text ‹For every ‹5×m›-board with ‹m ≥ 5› there exists a knight's path that starts in 
‹(1,1)› (bottom-left) and ends in ‹(4,m-1)› (top-right).›
lemma knights_path_5xm_ur_exists: 
  assumes "m ≥ 5" 
  shows "∃ps. knights_path (board 5 m) ps ∧ hd ps = (1,1) ∧ last ps = (4,int m-1)"
  using assms
proof -
  have "m ∈ {5,6,7,8,9} ∨ 5 ≤ m-5" using assms by auto
  then show ?thesis
  proof (elim disjE)
    assume "m ∈ {5,6,7,8,9}"
    then show ?thesis using kp_5xm_ur by fastforce
  next
    assume m_ge: "5 ≤ m-5" (* ⟷ 10 ≤ m *)
    then obtain ps1 where ps_prems: "knights_path (board 5 (m-5)) ps1" "hd ps1 = (1,1)" 
                                   "last ps1 = (2,int (m-5)-1)" "ps1 ≠ []"
      using knights_path_5xm_lr_exists[of "(m-5)"] knights_path_non_nil by auto
    let ?ps2="kp5x5ur"
    let ?ps'="ps1 @ trans_path (0,int (m-5)) ?ps2"
    have "knights_path b5x5 ?ps2" "hd ?ps2 = (1, 1)" "?ps2 ≠ []" 
         "last ?ps2 = (4,4)"
      using kp_5xm_ur by auto
    then have 1: "knights_path (board 5 m) ?ps'"              
      using m_ge ps_prems knights_path_lr_concat[of 5 "m-5" ps1 5 ?ps2] by auto

    have 2: "hd ?ps' = (1,1)" using ps_prems by auto

    have "last (trans_path (0,int (m-5)) ?ps2) = (4,int m-1)"
      using m_ge last_trans_path[OF ‹?ps2 ≠ []› ‹last ?ps2 = (4,4)›] by auto
    then have 3: "last ?ps' = (4,int m-1)"
      using last_appendR[OF trans_path_non_nil[OF ‹?ps2 ≠ []›],symmetric] by metis
    
    show ?thesis using 1 2 3 by auto
  qed
qed

text ‹@{thm knights_path_5xm_lr_exists} and @{thm knights_path_5xm_lr_exists} formalize Lemma 1 
from cite‹"cull_decurtins_1987"›.›
lemmas knights_path_5xm_exists = knights_path_5xm_lr_exists knights_path_5xm_ur_exists

section ‹Knight's Paths and Circuits for ‹6×m›-Boards›

abbreviation "b6x5 ≡ board 6 5"

text ‹
  A Knight's path for the ‹(6×5)›-board that starts in the lower-left and ends in the upper-left.
  \begin{table}[H]
    \begin{tabular}{lllll}
      10 & 19 &  4 & 29 & 12 \\
       3 & 30 & 11 & 20 &  5 \\
      18 &  9 & 24 & 13 & 28 \\
      25 &  2 & 17 &  6 & 21 \\
      16 & 23 &  8 & 27 & 14 \\
       1 & 26 & 15 & 22 &  7
    \end{tabular}
  \end{table}›
abbreviation "kp6x5ul ≡ the (to_path 
  [[10,19,4,29,12],
  [3,30,11,20,5],
  [18,9,24,13,28],
  [25,2,17,6,21],
  [16,23,8,27,14],
  [1,26,15,22,7]])"
lemma kp_6x5_ul: "knights_path b6x5 kp6x5ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_6x5_ul_hd: "hd kp6x5ul = (1,1)" by eval

lemma kp_6x5_ul_last: "last kp6x5ul = (5,2)" by eval

lemma kp_6x5_ul_non_nil: "kp6x5ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(6×5)›-board.
  \begin{table}[H]
    \begin{tabular}{lllll}
      16 &  9 &  6 & 27 & 18 \\
       7 & 26 & 17 & 14 &  5 \\
      10 & 15 &  8 & 19 & 28 \\
      25 & 30 & 23 &  4 & 13 \\
      22 & 11 &  2 & 29 & 20 \\
       1 & 24 & 21 & 12 &  3
    \end{tabular}
  \end{table}›
abbreviation "kc6x5 ≡ the (to_path 
  [[16,9,6,27,18],
  [7,26,17,14,5],
  [10,15,8,19,28],
  [25,30,23,4,13],
  [22,11,2,29,20],
  [1,24,21,12,3]])"
lemma kc_6x5: "knights_circuit b6x5 kc6x5"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_6x5_hd: "hd kc6x5 = (1,1)" by eval

lemma kc_6x5_non_nil: "kc6x5 ≠ []" by eval

abbreviation "b6x6 ≡ board 6 6"

text ‹The path given for the ‹6×6›-board that ends in the upper-left is wrong. The Knight cannot 
move from square 26 to square 27.
  \begin{table}[H]
    \begin{tabular}{llllll}
      14 & 23 &  6 & 28 & 12 & 21 \\
       7 & 36 & 13 & 22 &  5 & \color{red}{27} \\
      24 & 15 & 29 & 35 & 20 & 11 \\
      30 &  8 & 17 & \color{red}{26} & 34 &  4 \\
      16 & 25 &  2 & 32 & 10 & 19 \\
       1 & 31 &  9 & 18 &  3 & 33
    \end{tabular}
  \end{table}›
abbreviation "kp6x6ul_false ≡ the (to_path 
  [[14,23,6,28,12,21],
  [7,36,13,22,5,27],
  [24,15,29,35,20,11],
  [30,8,17,26,34,4],
  [16,25,2,32,10,19],
  [1,31,9,18,3,33]])"

lemma "¬knights_path b6x6 kp6x6ul_false"
  by (simp only: knights_path_exec_simp) eval

text ‹I have computed a correct Knight's path for the ‹6×6›-board that ends in the upper-left.
A Knight's path for the ‹(6×6)›-board that starts in the lower-left and ends in the upper-left.
  \begin{table}[H]
    \begin{tabular}{llllll}
       8 & 25 & 10 & 21 &  6 & 23 \\
      11 & 36 &  7 & 24 & 33 & 20 \\
      26 &  9 & 34 &  3 & 22 &  5 \\
      35 & 12 & 15 & 30 & 19 & 32 \\
      14 & 27 &  2 & 17 &  4 & 29 \\
       1 & 16 & 13 & 28 & 31 & 18
    \end{tabular}
  \end{table}›
abbreviation "kp6x6ul ≡ the (to_path 
  [[8,25,10,21,6,23],
  [11,36,7,24,33,20],
  [26,9,34,3,22,5],
  [35,12,15,30,19,32],
  [14,27,2,17,4,29],
  [1,16,13,28,31,18]])"
lemma kp_6x6_ul: "knights_path b6x6 kp6x6ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_6x6_ul_hd: "hd kp6x6ul = (1,1)" by eval

lemma kp_6x6_ul_last: "last kp6x6ul = (5,2)" by eval

lemma kp_6x6_ul_non_nil: "kp6x6ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(6×6)›-board.
  \begin{table}[H]
    \begin{tabular}{llllll}
       4 & 25 & 34 & 15 & 18 &  7 \\
      35 & 14 &  5 &  8 & 33 & 16 \\
      24 &  3 & 26 & 17 &  6 & 19 \\
      13 & 36 & 23 & 30 &  9 & 32 \\
      22 & 27 &  2 & 11 & 20 & 29 \\
       1 & 12 & 21 & 28 & 31 & 10
    \end{tabular}
  \end{table}›
abbreviation "kc6x6 ≡ the (to_path 
  [[4,25,34,15,18,7],
  [35,14,5,8,33,16],
  [24,3,26,17,6,19],
  [13,36,23,30,9,32],
  [22,27,2,11,20,29],
  [1,12,21,28,31,10]])"
lemma kc_6x6: "knights_circuit b6x6 kc6x6"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_6x6_hd: "hd kc6x6 = (1,1)" by eval

lemma kc_6x6_non_nil: "kc6x6 ≠ []" by eval

abbreviation "b6x7 ≡ board 6 7"

text ‹A Knight's path for the ‹(6×7)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllll}
      18 & 23 &  8 & 39 & 16 & 25 &  6 \\
       9 & 42 & 17 & 24 &  7 & 40 & 15 \\
      22 & 19 & 32 & 41 & 38 &  5 & 26 \\
      33 & 10 & 21 & 28 & 31 & 14 & 37 \\
      20 & 29 &  2 & 35 & 12 & 27 &  4 \\
       1 & 34 & 11 & 30 &  3 & 36 & 13
    \end{tabular}
  \end{table}›
abbreviation "kp6x7ul ≡ the (to_path 
  [[18,23,8,39,16,25,6],
  [9,42,17,24,7,40,15],
  [22,19,32,41,38,5,26],
  [33,10,21,28,31,14,37],
  [20,29,2,35,12,27,4],
  [1,34,11,30,3,36,13]])"
lemma kp_6x7_ul: "knights_path b6x7 kp6x7ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_6x7_ul_hd: "hd kp6x7ul = (1,1)" by eval

lemma kp_6x7_ul_last: "last kp6x7ul = (5,2)" by eval

lemma kp_6x7_ul_non_nil: "kp6x7ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(6×7)›-board.
  \begin{table}[H]
    \begin{tabular}{lllllll}
      26 & 37 &  8 & 17 & 28 & 31 &  6 \\
       9 & 18 & 27 & 36 &  7 & 16 & 29 \\
      38 & 25 & 10 & 19 & 30 &  5 & 32 \\
      11 & 42 & 23 & 40 & 35 & 20 & 15 \\
      24 & 39 &  2 & 13 & 22 & 33 &  4 \\
       1 & 12 & 41 & 34 &  3 & 14 & 21
    \end{tabular}
  \end{table}›
abbreviation "kc6x7 ≡ the (to_path 
  [[26,37,8,17,28,31,6],
  [9,18,27,36,7,16,29],
  [38,25,10,19,30,5,32],
  [11,42,23,40,35,20,15],
  [24,39,2,13,22,33,4],
  [1,12,41,34,3,14,21]])"
lemma kc_6x7: "knights_circuit b6x7 kc6x7"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_6x7_hd: "hd kc6x7 = (1,1)" by eval

lemma kc_6x7_non_nil: "kc6x7 ≠ []" by eval

abbreviation "b6x8 ≡ board 6 8"

text ‹A Knight's path for the ‹(6×8)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{llllllll}
      18 & 31 &  8 & 35 & 16 & 33 &  6 & 45 \\
       9 & 48 & 17 & 32 &  7 & 46 & 15 & 26 \\
      30 & 19 & 36 & 47 & 34 & 27 & 44 &  5 \\
      37 & 10 & 21 & 28 & 43 & 40 & 25 & 14 \\
      20 & 29 &  2 & 39 & 12 & 23 &  4 & 41 \\
       1 & 38 & 11 & 22 &  3 & 42 & 13 & 24
    \end{tabular}
  \end{table}›
abbreviation "kp6x8ul ≡ the (to_path 
  [[18,31,8,35,16,33,6,45],
  [9,48,17,32,7,46,15,26],
  [30,19,36,47,34,27,44,5],
  [37,10,21,28,43,40,25,14],
  [20,29,2,39,12,23,4,41],
  [1,38,11,22,3,42,13,24]])"
lemma kp_6x8_ul: "knights_path b6x8 kp6x8ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_6x8_ul_hd: "hd kp6x8ul = (1,1)" by eval

lemma kp_6x8_ul_last: "last kp6x8ul = (5,2)" by eval

lemma kp_6x8_ul_non_nil: "kp6x8ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(6×8)›-board.
  \begin{table}[H]
    \begin{tabular}{llllllll}
      30 & 35 &  8 & 15 & 28 & 39 &  6 & 13 \\
       9 & 16 & 29 & 36 &  7 & 14 & 27 & 38 \\
      34 & 31 & 10 & 23 & 40 & 37 & 12 &  5 \\
      17 & 48 & 33 & 46 & 11 & 22 & 41 & 26 \\
      32 & 45 &  2 & 19 & 24 & 43 &  4 & 21 \\
       1 & 18 & 47 & 44 &  3 & 20 & 25 & 42
    \end{tabular}
  \end{table}›
abbreviation "kc6x8 ≡ the (to_path 
  [[30,35,8,15,28,39,6,13],
  [9,16,29,36,7,14,27,38],
  [34,31,10,23,40,37,12,5],
  [17,48,33,46,11,22,41,26],
  [32,45,2,19,24,43,4,21],
  [1,18,47,44,3,20,25,42]])"
lemma kc_6x8: "knights_circuit b6x8 kc6x8"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_6x8_hd: "hd kc6x8 = (1,1)" by eval

lemma kc_6x8_non_nil: "kc6x8 ≠ []" by eval

abbreviation "b6x9 ≡ board 6 9"

text ‹A Knight's path for the ‹(6×9)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
      22 & 45 & 10 & 53 & 20 & 47 &  8 & 35 & 18 \\
      11 & 54 & 21 & 46 &  9 & 36 & 19 & 48 &  7 \\
      44 & 23 & 42 & 37 & 52 & 49 & 32 & 17 & 34 \\
      41 & 12 & 25 & 50 & 27 & 38 & 29 &  6 & 31 \\
      24 & 43 &  2 & 39 & 14 & 51 &  4 & 33 & 16 \\
       1 & 40 & 13 & 26 &  3 & 28 & 15 & 30 &  5
    \end{tabular}
  \end{table}›
abbreviation "kp6x9ul ≡ the (to_path 
  [[22,45,10,53,20,47,8,35,18],
  [11,54,21,46,9,36,19,48,7],
  [44,23,42,37,52,49,32,17,34],
  [41,12,25,50,27,38,29,6,31],
  [24,43,2,39,14,51,4,33,16],
  [1,40,13,26,3,28,15,30,5]])"
lemma kp_6x9_ul: "knights_path b6x9 kp6x9ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_6x9_ul_hd: "hd kp6x9ul = (1,1)" by eval

lemma kp_6x9_ul_last: "last kp6x9ul = (5,2)" by eval

lemma kp_6x9_ul_non_nil: "kp6x9ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(6×9)›-board.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
      14 & 49 &  4 & 51 & 24 & 39 &  6 & 29 & 22 \\
       3 & 52 & 13 & 40 &  5 & 32 & 23 & 42 &  7 \\
      48 & 15 & 50 & 25 & 38 & 41 & 28 & 21 & 30 \\
      53 &  2 & 37 & 12 & 33 & 26 & 31 &  8 & 43 \\
      16 & 47 & 54 & 35 & 18 & 45 & 10 & 27 & 20 \\
       1 & 36 & 17 & 46 & 11 & 34 & 19 & 44 &  9
    \end{tabular}
  \end{table}›
abbreviation "kc6x9 ≡ the (to_path 
  [[14,49,4,51,24,39,6,29,22],
  [3,52,13,40,5,32,23,42,7],
  [48,15,50,25,38,41,28,21,30],
  [53,2,37,12,33,26,31,8,43],
  [16,47,54,35,18,45,10,27,20],
  [1,36,17,46,11,34,19,44,9]])"
lemma kc_6x9: "knights_circuit b6x9 kc6x9"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_6x9_hd: "hd kc6x9 = (1,1)" by eval

lemma kc_6x9_non_nil: "kc6x9 ≠ []" by eval

lemmas kp_6xm_ul = 
  kp_6x5_ul kp_6x5_ul_hd kp_6x5_ul_last kp_6x5_ul_non_nil
  kp_6x6_ul kp_6x6_ul_hd kp_6x6_ul_last kp_6x6_ul_non_nil
  kp_6x7_ul kp_6x7_ul_hd kp_6x7_ul_last kp_6x7_ul_non_nil
  kp_6x8_ul kp_6x8_ul_hd kp_6x8_ul_last kp_6x8_ul_non_nil
  kp_6x9_ul kp_6x9_ul_hd kp_6x9_ul_last kp_6x9_ul_non_nil

lemmas kc_6xm = 
  kc_6x5 kc_6x5_hd kc_6x5_non_nil
  kc_6x6 kc_6x6_hd kc_6x6_non_nil
  kc_6x7 kc_6x7_hd kc_6x7_non_nil
  kc_6x8 kc_6x8_hd kc_6x8_non_nil
  kc_6x9 kc_6x9_hd kc_6x9_non_nil

text ‹For every ‹6×m›-board with ‹m ≥ 5› there exists a knight's path that starts in 
‹(1,1)› (bottom-left) and ends in ‹(5,2)› (top-left).›
lemma knights_path_6xm_ul_exists: 
  assumes "m ≥ 5" 
  shows "∃ps. knights_path (board 6 m) ps ∧ hd ps = (1,1) ∧ last ps = (5,2)"
  using assms
proof (induction m rule: less_induct)
  case (less m)
  then have "m ∈ {5,6,7,8,9} ∨ 5 ≤ m-5" by auto
  then show ?case
  proof (elim disjE)
    assume "m ∈ {5,6,7,8,9}"
    then show ?thesis using kp_6xm_ul by fastforce
  next
    let ?ps1="kp6x5ul"
    let ?b1="board 6 5"
    have ps1_prems: "knights_path ?b1 ?ps1" "hd ?ps1 = (1,1)" "last ?ps1 = (5,2)" 
      using kp_6xm_ul by auto
    assume m_ge: "5 ≤ m-5" (* ⟷ 10 ≤ m *)
    then obtain ps2 where ps2_IH: "knights_path (board 6 (m-5)) ps2" "hd ps2 = (1,1)" 
                                "last ps2 = (5,2)"
      using less.IH[of "m-5"] knights_path_non_nil by auto

    have "27 < length ?ps1" "last (take 27 ?ps1) = (2,4)" "hd (drop 27 ?ps1) = (4,5)" by eval+
    then have "step_in ?ps1 (2,4) (4,5)"
      unfolding step_in_def using zero_less_numeral by blast
    then have "step_in ?ps1 (2,4) (4,5)" 
              "valid_step (2,4) (1,int 5+1)" 
              "valid_step (5,int 5+2) (4,5)"
      unfolding valid_step_def by auto
    then show ?thesis
      using ‹5 ≤ m-5› ps1_prems ps2_IH knights_path_split_concat[of 6 5 ?ps1 "m-5" ps2] by auto
  qed
qed

text ‹For every ‹6×m›-board with ‹m ≥ 5› there exists a knight's circuit.›
lemma knights_circuit_6xm_exists: 
  assumes "m ≥ 5" 
  shows "∃ps. knights_circuit (board 6 m) ps"
  using assms
proof -
  have "m ∈ {5,6,7,8,9} ∨ 5 ≤ m-5" using assms by auto
  then show ?thesis
  proof (elim disjE)
    assume "m ∈ {5,6,7,8,9}"
    then show ?thesis using kc_6xm by fastforce
  next
    let ?ps1="rev kc6x5"
    have "knights_circuit b6x5 ?ps1" "last ?ps1 = (1,1)"
      using kc_6xm knights_circuit_rev by (auto simp: last_rev)
    then have ps1_prems: "knights_path b6x5 ?ps1" "valid_step (last ?ps1) (hd ?ps1)"
      unfolding knights_circuit_def using valid_step_rev by auto
    assume m_ge: "5 ≤ m-5" (* ⟷ 10 ≤ m *)
    then obtain ps2 where ps2_prems: "knights_path (board 6 (m-5)) ps2" "hd ps2 = (1,1)" 
                                   "last ps2 = (5,2)"
      using knights_path_6xm_ul_exists[of "(m-5)"] knights_path_non_nil by auto

    have "2 < length ?ps1" "last (take 2 ?ps1) = (2,4)" "hd (drop 2 ?ps1) = (4,5)" by eval+
    then have "step_in ?ps1 (2,4) (4,5)"
      unfolding step_in_def using zero_less_numeral by blast
    then have "step_in ?ps1 (2,4) (4,5)" 
              "valid_step (2,4) (1,int 5+1)" 
              "valid_step (5,int 5+2) (4,5)"
      unfolding valid_step_def by auto
    then have "∃ps. knights_path (board 6 m) ps ∧ hd ps = hd ?ps1 ∧ last ps = last ?ps1"              
      using m_ge ps1_prems ps2_prems knights_path_split_concat[of 6 5 ?ps1 "m-5" ps2] by auto
    then show ?thesis using ps1_prems by (auto simp: knights_circuit_def)
  qed
qed

text ‹@{thm knights_path_6xm_ul_exists} and @{thm knights_circuit_6xm_exists} formalize Lemma 2 
from cite‹"cull_decurtins_1987"›.›
lemmas knights_path_6xm_exists = knights_path_6xm_ul_exists knights_circuit_6xm_exists

section ‹Knight's Paths and Circuits for ‹8×m›-Boards›

abbreviation "b8x5 ≡ board 8 5"

text ‹A Knight's path for the ‹(8×5)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllll}
      28 &  7 & 22 & 39 & 26 \\
      23 & 40 & 27 &  6 & 21 \\
       8 & 29 & 38 & 25 & 14 \\
      37 & 24 & 15 & 20 &  5 \\
      16 &  9 & 30 & 13 & 34 \\
      31 & 36 & 33 &  4 & 19 \\
      10 & 17 &  2 & 35 & 12 \\
       1 & 32 & 11 & 18 &  3
    \end{tabular}
  \end{table}›
abbreviation "kp8x5ul ≡ the (to_path 
  [[28,7,22,39,26],
  [23,40,27,6,21],
  [8,29,38,25,14],
  [37,24,15,20,5],
  [16,9,30,13,34],
  [31,36,33,4,19],
  [10,17,2,35,12],
  [1,32,11,18,3]])"
lemma kp_8x5_ul: "knights_path b8x5 kp8x5ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_8x5_ul_hd: "hd kp8x5ul = (1,1)" by eval

lemma kp_8x5_ul_last: "last kp8x5ul = (7,2)" by eval

lemma kp_8x5_ul_non_nil: "kp8x5ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(8×5)›-board.
  \begin{table}[H]
    \begin{tabular}{lllll}
      26 &  7 & 28 & 15 & 24 \\
      31 & 16 & 25 &  6 & 29 \\
       8 & 27 & 30 & 23 & 14 \\
      17 & 32 & 39 & 34 &  5 \\
      38 &  9 & 18 & 13 & 22 \\
      19 & 40 & 33 &  4 & 35 \\
      10 & 37 &  2 & 21 & 12 \\
       1 & 20 & 11 & 36 &  3
    \end{tabular}
  \end{table}›
abbreviation "kc8x5 ≡ the (to_path 
  [[26,7,28,15,24],
  [31,16,25,6,29],
  [8,27,30,23,14],
  [17,32,39,34,5],
  [38,9,18,13,22],
  [19,40,33,4,35],
  [10,37,2,21,12],
  [1,20,11,36,3]])"
lemma kc_8x5: "knights_circuit b8x5 kc8x5"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_8x5_hd: "hd kc8x5 = (1,1)" by eval

lemma kc_8x5_last: "last kc8x5 = (3,2)" by eval

lemma kc_8x5_non_nil: "kc8x5 ≠ []" by eval

lemma kc_8x5_si: "step_in kc8x5 (2,4) (4,5)"  (is "step_in ?ps _ _")
proof -
  have "0 < (21::nat)" "21 < length ?ps" "last (take 21 ?ps) = (2,4)" "hd (drop 21 ?ps) = (4,5)" 
    by eval+
  then show ?thesis unfolding step_in_def by blast
qed

abbreviation "b8x6 ≡ board 8 6"

text ‹A Knight's path for the ‹(8×6)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{llllll}
      42 & 11 & 26 &  9 & 34 & 13 \\
      25 & 48 & 43 & 12 & 27 &  8 \\
      44 & 41 & 10 & 33 & 14 & 35 \\
      47 & 24 & 45 & 20 &  7 & 28 \\
      40 & 19 & 32 &  3 & 36 & 15 \\
      23 & 46 & 21 &  6 & 29 &  4 \\
      18 & 39 &  2 & 31 & 16 & 37 \\
       1 & 22 & 17 & 38 &  5 & 30
    \end{tabular}
  \end{table}›
abbreviation "kp8x6ul ≡ the (to_path 
  [[42,11,26,9,34,13],
  [25,48,43,12,27,8],
  [44,41,10,33,14,35],
  [47,24,45,20,7,28],
  [40,19,32,3,36,15],
  [23,46,21,6,29,4],
  [18,39,2,31,16,37],
  [1,22,17,38,5,30]])"
lemma kp_8x6_ul: "knights_path b8x6 kp8x6ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_8x6_ul_hd: "hd kp8x6ul = (1,1)" by eval

lemma kp_8x6_ul_last: "last kp8x6ul = (7,2)" by eval

lemma kp_8x6_ul_non_nil: "kp8x6ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(8×6)›-board. I have reversed circuit s.t. the circuit steps 
from ‹(2,5)› to ‹(4,6)› and not the other way around. This makes the proofs easier.
  \begin{table}[H]
    \begin{tabular}{llllll}
       8 & 29 & 24 & 45 & 12 & 37 \\
      25 & 46 &  9 & 38 & 23 & 44 \\
      30 &  7 & 28 & 13 & 36 & 11 \\
      47 & 26 & 39 & 10 & 43 & 22 \\
       6 & 31 &  4 & 27 & 14 & 35 \\
       3 & 48 & 17 & 40 & 21 & 42 \\
      32 &  5 &  2 & 19 & 34 & 15 \\
       1 & 18 & 33 & 16 & 41 & 20
    \end{tabular}
  \end{table}›
abbreviation "kc8x6 ≡ the (to_path 
  [[8,29,24,45,12,37],
  [25,46,9,38,23,44],
  [30,7,28,13,36,11],
  [47,26,39,10,43,22],
  [6,31,4,27,14,35],
  [3,48,17,40,21,42],
  [32,5,2,19,34,15],
  [1,18,33,16,41,20]])"
lemma kc_8x6: "knights_circuit b8x6 kc8x6"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_8x6_hd: "hd kc8x6 = (1,1)" by eval

lemma kc_8x6_non_nil: "kc8x6 ≠ []" by eval

lemma kc_8x6_si: "step_in kc8x6 (2,5) (4,6)" (is "step_in ?ps _ _")
proof -
  have "0 < (34::nat)" "34 < length ?ps" 
        "last (take 34 ?ps) = (2,5)" "hd (drop 34 ?ps) = (4,6)" by eval+
  then show ?thesis unfolding step_in_def by blast
qed

abbreviation "b8x7 ≡ board 8 7"

text ‹A Knight's path for the ‹(8×7)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllll}
      38 & 19 &  6 & 55 & 46 & 21 &  8 \\
       5 & 56 & 39 & 20 &  7 & 54 & 45 \\
      18 & 37 &  4 & 47 & 34 &  9 & 22 \\
       3 & 48 & 35 & 40 & 53 & 44 & 33 \\
      36 & 17 & 52 & 49 & 32 & 23 & 10 \\
      51 &  2 & 29 & 14 & 41 & 26 & 43 \\
      16 & 13 & 50 & 31 & 28 & 11 & 24 \\
       1 & 30 & 15 & 12 & 25 & 42 & 27
    \end{tabular}
  \end{table}›
abbreviation "kp8x7ul ≡ the (to_path 
  [[38,19,6,55,46,21,8],
  [5,56,39,20,7,54,45],
  [18,37,4,47,34,9,22],
  [3,48,35,40,53,44,33],
  [36,17,52,49,32,23,10],
  [51,2,29,14,41,26,43],
  [16,13,50,31,28,11,24],
  [1,30,15,12,25,42,27]])"
lemma kp_8x7_ul: "knights_path b8x7 kp8x7ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_8x7_ul_hd: "hd kp8x7ul = (1,1)" by eval

lemma kp_8x7_ul_last: "last kp8x7ul = (7,2)" by eval

lemma kp_8x7_ul_non_nil: "kp8x7ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(8×7)›-board. I have reversed circuit s.t. the circuit steps 
from ‹(2,6)› to ‹(4,7)› and not the other way around. This makes the proofs easier.
  \begin{table}[H]
    \begin{tabular}{lllllll}
      36 & 31 & 18 & 53 & 20 & 29 & 44 \\
      17 & 54 & 35 & 30 & 45 & 52 & 21 \\
      32 & 37 & 46 & 19 &  8 & 43 & 28 \\
      55 & 16 &  7 & 34 & 27 & 22 & 51 \\
      38 & 33 & 26 & 47 &  6 &  9 & 42 \\
       3 & 56 & 15 & 12 & 25 & 50 & 23 \\
      14 & 39 &  2 &  5 & 48 & 41 & 10 \\
       1 &  4 & 13 & 40 & 11 & 24 & 49 
    \end{tabular}
  \end{table}›
abbreviation "kc8x7 ≡ the (to_path 
  [[36,31,18,53,20,29,44],
  [17,54,35,30,45,52,21],
  [32,37,46,19,8,43,28],
  [55,16,7,34,27,22,51],
  [38,33,26,47,6,9,42],
  [3,56,15,12,25,50,23],
  [14,39,2,5,48,41,10],
  [1,4,13,40,11,24,49]])"
lemma kc_8x7: "knights_circuit b8x7 kc8x7"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_8x7_hd: "hd kc8x7 = (1,1)" by eval

lemma kc_8x7_non_nil: "kc8x7 ≠ []" by eval

lemma kc_8x7_si: "step_in kc8x7 (2,6) (4,7)" (is "step_in ?ps _ _")
proof -
  have "0 < (41::nat)" "41 < length ?ps" 
        "last (take 41 ?ps) = (2,6)" "hd (drop 41 ?ps) = (4,7)" by eval+
  then show ?thesis unfolding step_in_def by blast
qed

abbreviation "b8x8 ≡ board 8 8"

text ‹The path given for the ‹8×8›-board that ends in the upper-left is wrong. The Knight cannot 
move from square 27 to square 28.
  \begin{table}[H]
    \begin{tabular}{llllllll}
      24 & 11 & 37 &  9 & 26 & 21 & 39 &  7 \\
      36 & 64 & 24 & 22 & 38 &  8 & \color{red}{27} & 20 \\
      12 & 23 & 10 & 53 & 58 & 49 &  6 & \color{red}{28} \\
      63 & 35 & 61 & 50 & 55 & 52 & 19 & 40 \\
      46 & 13 & 54 & 57 & 48 & 59 & 29 &  5 \\
      34 & 62 & 47 & 60 & 51 & 56 & 41 & 18 \\
      14 & 45 &  2 & 32 & 16 & 43 &  4 & 30 \\
       1 & 33 & 15 & 44 &  3 & 31 & 17 & 42
    \end{tabular}
  \end{table}›
abbreviation "kp8x8ul_false ≡ the (to_path 
  [[24,11,37,9,26,21,39,7],
  [36,64,25,22,38,8,27,20],
  [12,23,10,53,58,49,6,28],
  [63,35,61,50,55,52,19,40],
  [46,13,54,57,48,59,29,5],
  [34,62,47,60,51,56,41,18],
  [14,45,2,32,16,43,4,30],
  [1,33,15,44,3,31,17,42]])"

lemma "¬knights_path b8x8 kp8x8ul_false"
  by (simp only: knights_path_exec_simp) eval

text ‹I have computed a correct Knight's path for the ‹8×8›-board that ends in the upper-left.
  \begin{table}[H]
    \begin{tabular}{llllllll}
      38 & 41 & 36 & 27 & 32 & 43 & 20 & 25 \\
      35 & 64 & 39 & 42 & 21 & 26 & 29 & 44 \\
      40 & 37 &  6 & 33 & 28 & 31 & 24 & 19 \\
       5 & 34 & 63 & 14 &  7 & 22 & 45 & 30 \\
      62 & 13 &  4 &  9 & 58 & 49 & 18 & 23 \\
       3 & 10 & 61 & 52 & 15 &  8 & 57 & 46 \\
      12 & 53 &  2 & 59 & 48 & 55 & 50 & 17 \\
       1 & 60 & 11 & 54 & 51 & 16 & 47 & 56
    \end{tabular}
  \end{table}›
abbreviation "kp8x8ul ≡ the (to_path 
  [[38,41,36,27,32,43,20,25],
  [35,64,39,42,21,26,29,44],
  [40,37,6,33,28,31,24,19],
  [5,34,63,14,7,22,45,30],
  [62,13,4,9,58,49,18,23],
  [3,10,61,52,15,8,57,46],
  [12,53,2,59,48,55,50,17],
  [1,60,11,54,51,16,47,56]])" 

lemma kp_8x8_ul: "knights_path b8x8 kp8x8ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_8x8_ul_hd: "hd kp8x8ul = (1,1)" by eval

lemma kp_8x8_ul_last: "last kp8x8ul = (7,2)" by eval

lemma kp_8x8_ul_non_nil: "kp8x8ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(8×8)›-board.
  \begin{table}[H]
    \begin{tabular}{llllllll}
      48 & 13 & 30 &  9 & 56 & 45 & 28 &  7 \\
      31 & 10 & 47 & 50 & 29 &  8 & 57 & 44 \\
      14 & 49 & 12 & 55 & 46 & 59 &  6 & 27 \\
      11 & 32 & 37 & 60 & 51 & 54 & 43 & 58 \\
      36 & 15 & 52 & 63 & 38 & 61 & 26 &  5 \\
      33 & 64 & 35 & 18 & 53 & 40 & 23 & 42 \\
      16 & 19 &  2 & 39 & 62 & 21 &  4 & 25 \\
       1 & 34 & 17 & 20 &  3 & 24 & 41 & 22
    \end{tabular}
  \end{table}›
abbreviation "kc8x8 ≡ the (to_path 
  [[48,13,30,9,56,45,28,7],
  [31,10,47,50,29,8,57,44],
  [14,49,12,55,46,59,6,27],
  [11,32,37,60,51,54,43,58],
  [36,15,52,63,38,61,26,5],
  [33,64,35,18,53,40,23,42],
  [16,19,2,39,62,21,4,25],
  [1,34,17,20,3,24,41,22]])"
lemma kc_8x8: "knights_circuit b8x8 kc8x8"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_8x8_hd: "hd kc8x8 = (1,1)" by eval

lemma kc_8x8_non_nil: "kc8x8 ≠ []" by eval

lemma kc_8x8_si: "step_in kc8x8 (2,7) (4,8)" (is "step_in ?ps _ _")
proof -
  have "0 < (4::nat)" "4 < length ?ps" 
        "last (take 4 ?ps) = (2,7)" "hd (drop 4 ?ps) = (4,8)" by eval+
  then show ?thesis unfolding step_in_def by blast
qed

abbreviation "b8x9 ≡ board 8 9"

text ‹A Knight's path for the ‹(8×9)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
      32 & 47 &  6 & 71 & 30 & 45 &  8 & 43 & 26 \\
       5 & 72 & 31 & 46 &  7 & 70 & 27 & 22 &  9 \\
      48 & 33 &  4 & 29 & 64 & 23 & 44 & 25 & 42 \\
       3 & 60 & 35 & 62 & 69 & 28 & 41 & 10 & 21 \\
      34 & 49 & 68 & 65 & 36 & 63 & 24 & 55 & 40 \\
      59 &  2 & 61 & 16 & 67 & 56 & 37 & 20 & 11 \\
      50 & 15 & 66 & 57 & 52 & 13 & 18 & 39 & 54 \\
       1 & 58 & 51 & 14 & 17 & 38 & 53 & 12 & 19
    \end{tabular}
  \end{table}›
abbreviation "kp8x9ul ≡ the (to_path 
  [[32,47,6,71,30,45,8,43,26],
  [5,72,31,46,7,70,27,22,9],
  [48,33,4,29,64,23,44,25,42],
  [3,60,35,62,69,28,41,10,21],
  [34,49,68,65,36,63,24,55,40],
  [59,2,61,16,67,56,37,20,11],
  [50,15,66,57,52,13,18,39,54],
  [1,58,51,14,17,38,53,12,19]])"
lemma kp_8x9_ul: "knights_path b8x9 kp8x9ul"
  by (simp only: knights_path_exec_simp) eval

lemma kp_8x9_ul_hd: "hd kp8x9ul = (1,1)" by eval

lemma kp_8x9_ul_last: "last kp8x9ul = (7,2)" by eval

lemma kp_8x9_ul_non_nil: "kp8x9ul ≠ []" by eval

text ‹A Knight's circuit for the ‹(8×9)›-board.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
      42 & 19 & 38 &  5 & 36 & 21 & 34 &  7 & 60 \\
      39 &  4 & 41 & 20 & 63 &  6 & 59 & 22 & 33 \\
      18 & 43 & 70 & 37 & 58 & 35 & 68 & 61 &  8 \\
       3 & 40 & 49 & 64 & 69 & 62 & 57 & 32 & 23 \\
      50 & 17 & 44 & 71 & 48 & 67 & 54 &  9 & 56 \\
      45 &  2 & 65 & 14 & 27 & 12 & 29 & 24 & 31 \\
      16 & 51 & 72 & 47 & 66 & 53 & 26 & 55 & 10 \\
       1 & 46 & 15 & 52 & 13 & 28 & 11 & 30 & 25
    \end{tabular}
  \end{table}›
abbreviation "kc8x9 ≡ the (to_path 
  [[42,19,38,5,36,21,34,7,60],
  [39,4,41,20,63,6,59,22,33],
  [18,43,70,37,58,35,68,61,8],
  [3,40,49,64,69,62,57,32,23],
  [50,17,44,71,48,67,54,9,56],
  [45,2,65,14,27,12,29,24,31],
  [16,51,72,47,66,53,26,55,10],
  [1,46,15,52,13,28,11,30,25]])"
lemma kc_8x9: "knights_circuit b8x9 kc8x9"
  by (simp only: knights_circuit_exec_simp) eval

lemma kc_8x9_hd: "hd kc8x9 = (1,1)" by eval

lemma kc_8x9_non_nil: "kc8x9 ≠ []" by eval

lemma kc_8x9_si: "step_in kc8x9 (2,8) (4,9)" (is "step_in ?ps _ _")
proof -
  have "0 < (55::nat)" "55 < length ?ps" 
        "last (take 55 ?ps) = (2,8)" "hd (drop 55 ?ps) = (4,9)" by eval+
  then show ?thesis unfolding step_in_def by blast
qed

lemmas kp_8xm_ul = 
  kp_8x5_ul kp_8x5_ul_hd kp_8x5_ul_last kp_8x5_ul_non_nil
  kp_8x6_ul kp_8x6_ul_hd kp_8x6_ul_last kp_8x6_ul_non_nil
  kp_8x7_ul kp_8x7_ul_hd kp_8x7_ul_last kp_8x7_ul_non_nil
  kp_8x8_ul kp_8x8_ul_hd kp_8x8_ul_last kp_8x8_ul_non_nil
  kp_8x9_ul kp_8x9_ul_hd kp_8x9_ul_last kp_8x9_ul_non_nil

lemmas kc_8xm = 
  kc_8x5 kc_8x5_hd kc_8x5_last kc_8x5_non_nil kc_8x5_si
  kc_8x6 kc_8x6_hd kc_8x6_non_nil kc_8x6_si
  kc_8x7 kc_8x7_hd kc_8x7_non_nil kc_8x7_si
  kc_8x8 kc_8x8_hd kc_8x8_non_nil kc_8x8_si
  kc_8x9 kc_8x9_hd kc_8x9_non_nil kc_8x9_si

text ‹For every ‹8×m›-board with ‹m ≥ 5› there exists a knight's circuit.›
lemma knights_circuit_8xm_exists: 
  assumes "m ≥ 5" 
  shows "∃ps. knights_circuit (board 8 m) ps ∧ step_in ps (2,int m-1) (4,int m)"
  using assms
proof (induction m rule: less_induct)
  case (less m)
  then have "m ∈ {5,6,7,8,9} ∨ 5 ≤ m-5" by auto
  then show ?case
  proof (elim disjE)
    assume "m ∈ {5,6,7,8,9}"
    then show ?thesis using kc_8xm by fastforce
  next
    let ?ps2="kc8x5"
    let ?b2="board 8 5"
    have ps2_prems: "knights_circuit ?b2 ?ps2" "hd ?ps2 = (1,1)" "last ?ps2 = (3,2)"
      using kc_8xm by auto
    have "21 < length ?ps2" "last (take 21 ?ps2) = (2,int 5-1)" "hd (drop 21 ?ps2) = (4,int 5)" 
      by eval+
    then have si: "step_in ?ps2 (2,int 5-1) (4,int 5)"
      unfolding step_in_def using zero_less_numeral by blast
    assume m_ge: "5 ≤ m-5" (* ⟷ 10 ≤ m *)
    then obtain ps1 where ps1_IH: "knights_circuit (board 8 (m-5)) ps1"
                                "step_in ps1 (2,int (m-5)-1) (4,int (m-5))"
      using less.IH[of "m-5"] knights_path_non_nil by auto
    then show ?thesis
      using m_ge ps2_prems si knights_circuit_lr_concat[of 8 "m-5" ps1 5 ?ps2] by auto
  qed
qed

text ‹For every ‹8×m›-board with ‹m ≥ 5› there exists a knight's path that starts in 
‹(1,1)› (bottom-left) and ends in ‹(7,2)› (top-left).›
lemma knights_path_8xm_ul_exists: 
  assumes "m ≥ 5" 
  shows "∃ps. knights_path (board 8 m) ps ∧ hd ps = (1,1) ∧ last ps = (7,2)"
  using assms
proof -
  have "m ∈ {5,6,7,8,9} ∨ 5 ≤ m-5" using assms by auto
  then show ?thesis
  proof (elim disjE)
    assume "m ∈ {5,6,7,8,9}"
    then show ?thesis using kp_8xm_ul by fastforce
  next
    let ?ps1="kp8x5ul"
    have ps1_prems: "knights_path b8x5 ?ps1" "hd ?ps1 = (1,1)" "last ?ps1 = (7,2)"
      using kp_8xm_ul by auto
    assume m_ge: "5 ≤ m-5" (* ⟷ 10 ≤ m *)
    then have b_prems: "5 ≤ min 8 (m-5)"
      unfolding board_def by auto

    obtain ps2 where "knights_circuit (board 8 (m-5)) ps2"
      using m_ge knights_circuit_8xm_exists[of "(m-5)"] knights_path_non_nil by auto
    then obtain ps2' where ps2'_prems': "knights_circuit (board 8 (m-5)) ps2'" 
        "hd ps2' = (1,1)" "last ps2' = (3,2)"
      using b_prems ‹5 ≤ min 8 (m-5)› rotate_knights_circuit by blast
    then have ps2'_path: "knights_path (board 8 (m-5)) (rev ps2')" 
      "valid_step (last ps2') (hd ps2')" "hd (rev ps2') = (3,2)" "last (rev ps2') = (1,1)"
      unfolding knights_circuit_def using knights_path_rev by (auto simp: hd_rev last_rev)

    have "34 < length ?ps1" "last (take 34 ?ps1) = (4,5)" "hd (drop 34 ?ps1) = (2,4)" by eval+
    then have "step_in ?ps1 (4,5) (2,4)"
      unfolding step_in_def using zero_less_numeral by blast
    then have "step_in ?ps1 (4,5) (2,4)" 
              "valid_step (4,5) (3,int 5+2)" 
              "valid_step (1,int 5+1) (2,4)"
      unfolding valid_step_def by auto
    then have "∃ps. knights_path (board 8 m) ps ∧ hd ps = hd ?ps1 ∧ last ps = last ?ps1"              
      using m_ge ps1_prems ps2'_prems' ps2'_path 
            knights_path_split_concat[of 8 5 ?ps1 "m-5" "rev ps2'"] by auto
    then show ?thesis using ps1_prems by auto
  qed
qed

text ‹@{thm knights_circuit_8xm_exists} and @{thm knights_path_8xm_ul_exists} formalize Lemma 3 
from cite‹"cull_decurtins_1987"›.›
lemmas knights_path_8xm_exists = knights_circuit_8xm_exists knights_path_8xm_ul_exists

section ‹Knight's Paths and Circuits for ‹n×m›-Boards›

text ‹In this section the desired theorems are proved. The proof uses the previous lemmas to 
construct paths and circuits for arbitrary ‹n×m›-boards.›

text ‹A Knight's path for the ‹(5×5)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllll}
       7 & 20 &  9 & 14 &  5 \\
      10 & 25 &  6 & 21 & 16 \\
      19 &  8 & 15 &  4 & 13 \\
      24 & 11 &  2 & 17 & 22 \\
       1 & 18 & 23 & 12 &  3
    \end{tabular}
  \end{table}›
abbreviation "kp5x5ul ≡ the (to_path 
  [[7,20,9,14,5],
  [10,25,6,21,16],
  [19,8,15,4,13],
  [24,11,2,17,22],
  [1,18,23,12,3]])"
lemma kp_5x5_ul: "knights_path b5x5 kp5x5ul"
  by (simp only: knights_path_exec_simp) eval

text ‹A Knight's path for the ‹(5×7)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllll}
      17 & 14 & 25 &  6 & 19 &  8 & 29 \\
      26 & 35 & 18 & 15 & 28 &  5 & 20 \\
      13 & 16 & 27 & 24 &  7 & 30 &  9 \\
      34 & 23 &  2 & 11 & 32 & 21 &  4 \\
       1 & 12 & 33 & 22 &  3 & 10 & 31
    \end{tabular}
  \end{table}›
abbreviation "kp5x7ul ≡ the (to_path 
  [[17,14,25,6,19,8,29],
  [26,35,18,15,28,5,20],
  [13,16,27,24,7,30,9],
  [34,23,2,11,32,21,4],
  [1,12,33,22,3,10,31]])"
lemma kp_5x7_ul: "knights_path b5x7 kp5x7ul"
  by (simp only: knights_path_exec_simp) eval

text ‹A Knight's path for the ‹(5×9)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
       7 & 12 & 37 & 42 &  5 & 18 & 23 & 32 & 27 \\
      38 & 45 &  6 & 11 & 36 & 31 & 26 & 19 & 24 \\
      13 &  8 & 43 &  4 & 41 & 22 & 17 & 28 & 33 \\
      44 & 39 &  2 & 15 & 10 & 35 & 30 & 25 & 20 \\
       1 & 14 &  9 & 40 &  3 & 16 & 21 & 34 & 29
    \end{tabular}
  \end{table}›
abbreviation "kp5x9ul ≡ the (to_path 
  [[7,12,37,42,5,18,23,32,27],
  [38,45,6,11,36,31,26,19,24],
  [13,8,43,4,41,22,17,28,33],
  [44,39,2,15,10,35,30,25,20],
  [1,14,9,40,3,16,21,34,29]])"
lemma kp_5x9_ul: "knights_path b5x9 kp5x9ul"
  by (simp only: knights_path_exec_simp) eval

abbreviation "b7x7 ≡ board 7 7"

text ‹A Knight's path for the ‹(7×7)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllll}
       9 & 30 & 19 & 42 &  7 & 32 & 17 \\
      20 & 49 &  8 & 31 & 18 & 43 &  6 \\
      29 & 10 & 41 & 36 & 39 & 16 & 33 \\
      48 & 21 & 38 & 27 & 34 &  5 & 44 \\
      11 & 28 & 35 & 40 & 37 & 26 & 15 \\
      22 & 47 &  2 & 13 & 24 & 45 &  4 \\
       1 & 12 & 23 & 46 &  3 & 14 & 25
    \end{tabular}
  \end{table}›
abbreviation "kp7x7ul ≡ the (to_path 
  [[9,30,19,42,7,32,17],
  [20,49,8,31,18,43,6],
  [29,10,41,36,39,16,33],
  [48,21,38,27,34,5,44],
  [11,28,35,40,37,26,15],
  [22,47,2,13,24,45,4],
  [1,12,23,46,3,14,25]])"
lemma kp_7x7_ul: "knights_path b7x7 kp7x7ul"
  by (simp only: knights_path_exec_simp) eval

abbreviation "b7x9 ≡ board 7 9"

text ‹A Knight's path for the ‹(7×9)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
      59 &  4 & 17 & 50 & 37 &  6 & 19 & 30 & 39 \\
      16 & 63 & 58 &  5 & 18 & 51 & 38 &  7 & 20 \\
       3 & 60 & 49 & 36 & 57 & 42 & 29 & 40 & 31 \\
      48 & 15 & 62 & 43 & 52 & 35 & 56 & 21 &  8 \\
      61 &  2 & 13 & 26 & 45 & 28 & 41 & 32 & 55 \\
      14 & 47 & 44 & 11 & 24 & 53 & 34 &  9 & 22 \\
       1 & 12 & 25 & 46 & 27 & 10 & 23 & 54 & 33
    \end{tabular}
  \end{table}›
abbreviation "kp7x9ul ≡ the (to_path 
  [[59,4,17,50,37,6,19,30,39],
  [16,63,58,5,18,51,38,7,20],
  [3,60,49,36,57,42,29,40,31],
  [48,15,62,43,52,35,56,21,8],
  [61,2,13,26,45,28,41,32,55],
  [14,47,44,11,24,53,34,9,22],
  [1,12,25,46,27,10,23,54,33]])"
lemma kp_7x9_ul: "knights_path b7x9 kp7x9ul"
  by (simp only: knights_path_exec_simp) eval

abbreviation "b9x7 ≡ board 9 7"

text ‹A Knight's path for the ‹(9×7)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllll}
       5 & 20 & 53 & 48 &  7 & 22 & 31 \\
      52 & 63 &  6 & 21 & 32 & 55 &  8 \\
      19 &  4 & 49 & 54 & 47 & 30 & 23 \\
      62 & 51 & 46 & 33 & 56 &  9 & 58 \\
       3 & 18 & 61 & 50 & 59 & 24 & 29 \\
      14 & 43 & 34 & 45 & 28 & 57 & 10 \\
      17 &  2 & 15 & 60 & 35 & 38 & 25 \\
      42 & 13 & 44 & 27 & 40 & 11 & 36 \\
       1 & 16 & 41 & 12 & 37 & 26 & 39
    \end{tabular}
  \end{table}›
abbreviation "kp9x7ul ≡ the (to_path 
  [[5,20,53,48,7,22,31],
  [52,63,6,21,32,55,8],
  [19,4,49,54,47,30,23],
  [62,51,46,33,56,9,58],
  [3,18,61,50,59,24,29],
  [14,43,34,45,28,57,10],
  [17,2,15,60,35,38,25],
  [42,13,44,27,40,11,36],
  [1,16,41,12,37,26,39]])"
lemma kp_9x7_ul: "knights_path b9x7 kp9x7ul"
  by (simp only: knights_path_exec_simp) eval

abbreviation "b9x9 ≡ board 9 9"

text ‹A Knight's path for the ‹(9×9)›-board that starts in the lower-left and ends in the 
upper-left.
  \begin{table}[H]
    \begin{tabular}{lllllllll}
      13 & 26 & 39 & 52 & 11 & 24 & 37 & 50 &  9 \\
      40 & 81 & 12 & 25 & 38 & 51 & 10 & 23 & 36 \\
      27 & 14 & 53 & 58 & 63 & 68 & 73 &  8 & 49 \\
      80 & 41 & 64 & 67 & 72 & 57 & 62 & 35 & 22 \\
      15 & 28 & 59 & 54 & 65 & 74 & 69 & 48 &  7 \\
      42 & 79 & 66 & 71 & 76 & 61 & 56 & 21 & 34 \\
      29 & 16 & 77 & 60 & 55 & 70 & 75 &  6 & 47 \\
      78 & 43 &  2 & 31 & 18 & 45 &  4 & 33 & 20 \\
       1 & 30 & 17 & 44 &  3 & 32 & 19 & 46 &  5
    \end{tabular}
  \end{table}›
abbreviation "kp9x9ul ≡ the (to_path 
  [[13,26,39,52,11,24,37,50,9],
  [40,81,12,25,38,51,10,23,36],
  [27,14,53,58,63,68,73,8,49],
  [80,41,64,67,72,57,62,35,22],
  [15,28,59,54,65,74,69,48,7],
  [42,79,66,71,76,61,56,21,34],
  [29,16,77,60,55,70,75,6,47],
  [78,43,2,31,18,45,4,33,20],
  [1,30,17,44,3,32,19,46,5]])"
lemma kp_9x9_ul: "knights_path b9x9 kp9x9ul"
  by (simp only: knights_path_exec_simp) eval 

text ‹The following lemma is a sub-proof used in Lemma 4 in cite‹"cull_decurtins_1987"›. 
I moved the sub-proof out to a separate lemma.›
lemma knights_circuit_exists_even_n_gr10:
  assumes "even n" "n ≥ 10" "m ≥ 5"
          "∃ps. knights_path (board (n-5) m) ps ∧ hd ps = (int (n-5),1) 
            ∧ last ps = (int (n-5)-1,int m-1)"
  shows "∃ps. knights_circuit (board m n) ps"
  using assms
proof -
  let ?b2="board (n-5) m"
  assume "n ≥ 10"
  then obtain ps2 where ps2_prems: "knights_path ?b2 ps2" "hd ps2 = (int (n-5),1)" 
      "last ps2 = (int (n-5)-1,int m-1)"
    using assms by auto
  let ?ps2_m2="mirror2 ps2"
  have ps2_m2_prems: "knights_path ?b2 ?ps2_m2" "hd ?ps2_m2 = (int (n-5),int m)" 
      "last ?ps2_m2 = (int (n-5)-1,2)"
    using ps2_prems mirror2_knights_path hd_mirror2 last_mirror2 by auto

  obtain ps1 where ps1_prems: "knights_path (board 5 m) ps1" "hd ps1 = (1,1)""last ps1 = (2,int m-1)"
    using assms knights_path_5xm_exists by auto
  let ?ps1'="trans_path (int (n-5),0) ps1"
  let ?b1'="trans_board (int (n-5),0) (board 5 m)"
  have ps1'_prems: "knights_path ?b1' ?ps1'" "hd ?ps1' = (int (n-5)+1,1)" 
      "last ?ps1' = (int (n-5)+2,int m-1)"
    using ps1_prems trans_knights_path knights_path_non_nil hd_trans_path last_trans_path by auto

  let ?ps="?ps1'@?ps2_m2"
  let ?psT="transpose ?ps"

  have "n-5 ≥ 5" using ‹n ≥ 10› by auto
  have inter: "?b1' ∩ ?b2 = {}"
    unfolding trans_board_def board_def using ‹n-5 ≥ 5› by auto
  have union: "?b1' ∪ ?b2 = board n m"
    using ‹n-5 ≥ 5› board_concatT[of "n-5" m 5] by auto

  have vs: "valid_step (last ?ps1') (hd ?ps2_m2)" and "valid_step (last ?ps2_m2) (hd ?ps1')"
    unfolding valid_step_def using ps1'_prems ps2_m2_prems by auto
  then have vs_c: "valid_step (last ?ps) (hd ?ps)"
    using ps1'_prems ps2_m2_prems knights_path_non_nil by auto

  have "knights_path (board n m) ?ps"
    using ps1'_prems ps2_m2_prems inter vs union knights_path_append[of ?b1' ?ps1' ?b2 ?ps2_m2] 
    by auto
  then have "knights_circuit (board n m) ?ps"
    unfolding knights_circuit_def using vs_c by auto
  then show ?thesis using transpose_knights_circuit by auto
qed

text ‹For every ‹n×m›-board with ‹min n m ≥ 5› and odd ‹n› there exists a Knight's path that 
starts in ‹(n,1)› (top-left) and ends in ‹(n-1,m-1)› (top-right).›
text ‹This lemma formalizes Lemma 4 from cite‹"cull_decurtins_1987"›. Formalizing the proof of 
this lemma was quite challenging as a lot of details on how to exactly combine the boards are 
left out in the original proof in cite‹"cull_decurtins_1987"›.›
lemma knights_path_odd_n_exists:
  assumes "odd n" "min n m ≥ 5"
  shows "∃ps. knights_path (board n m) ps ∧ hd ps = (int n,1) ∧ last ps = (int n-1,int m-1)"
  using assms
proof -
  obtain x where "x = n + m" by auto
  then show ?thesis
    using assms
  proof (induction x arbitrary: n m rule: less_induct)
    case (less x)
    then have "m = 5 ∨ m = 6 ∨ m = 7 ∨ m = 8 ∨ m = 9 ∨ m ≥ 10" by auto
    then show ?case
    proof (elim disjE)
      assume [simp]: "m = 5"
      have "odd n" "n ≥ 5" using less by auto
      then have "n = 5 ∨ n = 7 ∨ n = 9 ∨ n-5 ≥ 5" by presburger
      then show ?thesis
      proof (elim disjE)
        assume [simp]: "n = 5"
        let ?ps="mirror1 (transpose kp5x5ul)"
        have kp: "knights_path (board n m) ?ps"
          using kp_5x5_ul rot90_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 5› ‹n = 5› | eval)+
        then show ?thesis using kp by auto
      next
        assume [simp]: "n = 7"
        let ?ps="mirror1 (transpose kp5x7ul)"
        have kp: "knights_path (board n m) ?ps"
          using kp_5x7_ul rot90_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 5› ‹n = 7› | eval)+
        then show ?thesis using kp by auto
      next
        assume [simp]: "n = 9"
        let ?ps="mirror1 (transpose kp5x9ul)"
        have kp: "knights_path (board n m) ?ps"
          using kp_5x9_ul rot90_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 5› ‹n = 9› | eval)+
        then show ?thesis using kp by auto
      next
        let ?b2="board m (n-5)"
        assume "n-5 ≥ 5"
        then have "∃ps. knights_circuit ?b2 ps"
        proof -
          have "n-5 = 6 ∨ n-5 = 8 ∨ n-5 ≥ 10" 
            using ‹n-5 ≥ 5› less by presburger
          then show ?thesis
          proof (elim disjE)
            assume "n-5 = 6"
            then obtain ps where "knights_circuit (board (n-5) m) ps"
              using knights_path_6xm_exists[of m] by auto
            then show ?thesis 
              using transpose_knights_circuit by auto
          next
            assume "n-5 = 8"
            then obtain ps where "knights_circuit (board (n-5) m) ps"
              using knights_path_8xm_exists[of m] by auto
            then show ?thesis 
              using transpose_knights_circuit by auto
          next
            assume "n-5 ≥ 10"
            then show ?thesis 
              using less less.IH[of "n-10+m" "n-10" m]
                    knights_circuit_exists_even_n_gr10[of "n-5" m] by auto
          qed
        qed
        then obtain ps2 where "knights_circuit ?b2 ps2" "hd ps2 = (1,1)" "last ps2 = (3,2)"
          using ‹n-5 ≥ 5› rotate_knights_circuit[of m "n-5"] by auto
        then have rev_ps2_prems: "knights_path ?b2 (rev ps2)" "valid_step (last ps2) (hd ps2)"
            "hd (rev ps2) = (3,2)" "last (rev ps2) = (1,1)"
          unfolding knights_circuit_def using knights_path_rev by (auto simp: hd_rev last_rev)

        let ?ps1="kp5x5ul"
        have ps1_prems: "knights_path (board 5 5) ?ps1" "hd ?ps1 = (1,1)" "last ?ps1 = (4,2)"
          using kp_5x5_ul by simp eval+

        have "16 < length ?ps1" "last (take 16 ?ps1) = (4,5)" "hd (drop 16 ?ps1) = (2,4)" by eval+
        then have si: "step_in ?ps1 (4,5) (2,4)"
          unfolding step_in_def using zero_less_numeral by blast

        have vs: "valid_step (4,5) (3,int 5+2)" "valid_step (1,int 5+1) (2,4)"
          unfolding valid_step_def by auto

        obtain ps where "knights_path (board m n) ps" "hd ps = (1,1)" "last ps = (4,2)"
          using ‹n-5 ≥ 5› ps1_prems rev_ps2_prems si vs
              knights_path_split_concat[of 5 5 ?ps1 "n-5" "rev ps2" "(4,5)" "(2,4)"] by auto
        then show ?thesis
          using rot90_knights_path hd_rot90_knights_path last_rot90_knights_path by fastforce
      qed
    next
      assume [simp]: "m = 6"
      then obtain ps where 
          ps_prems: "knights_path (board m n) ps" "hd ps = (1,1)" "last ps = (int m-1,2)"
        using less knights_path_6xm_exists[of n] by auto
      let ?ps'="mirror1 (transpose ps)"
      have "knights_path (board n m) ?ps'" "hd ?ps' = (int n,1)" "last ?ps' = (int n-1,int m-1)"
        using ps_prems rot90_knights_path hd_rot90_knights_path last_rot90_knights_path by auto
      then show ?thesis by auto
    next
      assume [simp]: "m = 7"
      have "odd n" "n ≥ 5" using less by auto
      then have "n = 5 ∨ n = 7 ∨ n = 9 ∨ n-5 ≥ 5" by presburger
      then show ?thesis
      proof (elim disjE)
        assume [simp]: "n = 5"
        let ?ps="mirror1 kp5x7lr"
        have kp: "knights_path (board n m) ?ps"
          using kp_5x7_lr mirror1_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 7› ‹n = 5› | eval)+
        then show ?thesis using kp by auto
      next
        assume [simp]: "n = 7"
        let ?ps="mirror1 (transpose kp7x7ul)"
        have kp: "knights_path (board n m) ?ps"
          using kp_7x7_ul rot90_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 7› ‹n = 7› | eval)+
        then show ?thesis using kp by auto
      next
        assume [simp]: "n = 9"
        let ?ps="mirror1 (transpose kp7x9ul)"
        have kp: "knights_path (board n m) ?ps"
          using kp_7x9_ul rot90_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 7› ‹n = 9› | eval)+
        then show ?thesis using kp by auto
      next
        let ?b2="board m (n-5)"
        let ?b2T="board (n-5) m"
        assume "n-5 ≥ 5"
        then have "∃ps. knights_circuit ?b2 ps"
        proof -
          have "n-5 = 6 ∨ n-5 = 8 ∨ n-5 ≥ 10" 
            using ‹n-5 ≥ 5› less by presburger
          then show ?thesis
          proof (elim disjE)
            assume "n-5 = 6"
            then obtain ps where "knights_circuit (board (n-5) m) ps"
              using knights_path_6xm_exists[of m] by auto
            then show ?thesis 
              using transpose_knights_circuit by auto
          next
            assume "n-5 = 8"
            then obtain ps where "knights_circuit (board (n-5) m) ps"
              using knights_path_8xm_exists[of m] by auto
            then show ?thesis 
              using transpose_knights_circuit by auto
          next
            assume "n-5 ≥ 10"
            then show ?thesis 
              using less less.IH[of "n-10+m" "n-10" m]
                    knights_circuit_exists_even_n_gr10[of "n-5" m] by auto
          qed
        qed
        then obtain ps2 where ps2_prems: "knights_circuit ?b2 ps2" "hd ps2 = (1,1)" 
            "last ps2 = (3,2)"
          using ‹n-5 ≥ 5› rotate_knights_circuit[of m "n-5"] by auto
        let ?ps2T="transpose ps2"
        have ps2T_prems: "knights_path ?b2T ?ps2T" "hd ?ps2T = (1,1)" "last ?ps2T = (2,3)"
          using ps2_prems transpose_knights_path knights_path_non_nil hd_transpose last_transpose 
          unfolding knights_circuit_def transpose_square_def by auto

        let ?ps1="kp5x7lr"
        have ps1_prems: "knights_path b5x7 ?ps1" "hd ?ps1 = (1,1)" "last ?ps1 = (2,6)"
          using kp_5x7_lr by simp eval+

        have "29 < length ?ps1" "last (take 29 ?ps1) = (4,2)" "hd (drop 29 ?ps1) = (5,4)" by eval+
        then have si: "step_in ?ps1 (4,2) (5,4)"
          unfolding step_in_def using zero_less_numeral by blast

        have vs: "valid_step (4,2) (int 5+1,1)" "valid_step (int 5+2,3) (5,4)"
          unfolding valid_step_def by auto

        obtain ps where "knights_path (board n m) ps" "hd ps = (1,1)" "last ps = (2,6)"
          using ‹n-5 ≥ 5› ps1_prems ps2T_prems si vs
              knights_path_split_concatT[of 5 m ?ps1 "n-5" ?ps2T "(4,2)" "(5,4)"] by auto
        then show ?thesis
          using mirror1_knights_path hd_mirror1 last_mirror1 by fastforce
      qed
    next
      assume [simp]: "m = 8"
      then obtain ps where ps_prems: "knights_path (board m n) ps" "hd ps = (1,1)" 
          "last ps = (int m-1,2)"
        using less knights_path_8xm_exists[of n] by auto
      let ?ps'="mirror1 (transpose ps)"
      have "knights_path (board n m) ?ps'" "hd ?ps' = (int n,1)" "last ?ps' = (int n-1,int m-1)"
        using ps_prems rot90_knights_path hd_rot90_knights_path last_rot90_knights_path by auto
      then show ?thesis by auto
    next
      assume [simp]: "m = 9"
      have "odd n" "n ≥ 5" using less by auto
      then have "n = 5 ∨ n = 7 ∨ n = 9 ∨ n-5 ≥ 5" by presburger
      then show ?thesis
      proof (elim disjE)
        assume [simp]: "n = 5"
        let ?ps="mirror1 kp5x9lr"
        have kp: "knights_path (board n m) ?ps"
          using kp_5x9_lr mirror1_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 9› ‹n = 5› | eval)+
        then show ?thesis using kp by auto
      next
        assume [simp]: "n = 7"
        let ?ps="mirror1 (transpose kp9x7ul)"
        have kp: "knights_path (board n m) ?ps"
          using kp_9x7_ul rot90_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 9› ‹n = 7› | eval)+
        then show ?thesis using kp by auto
      next
        assume [simp]: "n = 9"
        let ?ps="mirror1 (transpose kp9x9ul)"
        have kp: "knights_path (board n m) ?ps"
          using kp_9x9_ul rot90_knights_path by auto
        have "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
          by (simp only: ‹m = 9› ‹n = 9› | eval)+
        then show ?thesis using kp by auto
      next
        let ?b2="board m (n-5)"
        let ?b2T="board (n-5) m"
        assume "n-5 ≥ 5"
        then have "∃ps. knights_circuit ?b2 ps"
        proof -
          have "n-5 = 6 ∨ n-5 = 8 ∨ n-5 ≥ 10" 
            using ‹n-5 ≥ 5› less by presburger
          then show ?thesis
          proof (elim disjE)
            assume "n-5 = 6"
            then obtain ps where "knights_circuit (board (n-5) m) ps"
              using knights_path_6xm_exists[of m] by auto
            then show ?thesis 
              using transpose_knights_circuit by auto
          next
            assume "n-5 = 8"
            then obtain ps where "knights_circuit (board (n-5) m) ps"
              using knights_path_8xm_exists[of m] by auto
            then show ?thesis 
              using transpose_knights_circuit by auto
          next
            assume "n-5 ≥ 10"
            then show ?thesis 
              using less less.IH[of "n-10+m" "n-10" m]
                    knights_circuit_exists_even_n_gr10[of "n-5" m] by auto
          qed
        qed
        then obtain ps2 where ps2_prems: "knights_circuit ?b2 ps2" "hd ps2 = (1,1)" 
            "last ps2 = (3,2)"
          using ‹n-5 ≥ 5› rotate_knights_circuit[of m "n-5"] by auto
        let ?ps2T="transpose (rev ps2)"
        have ps2T_prems: "knights_path ?b2T ?ps2T" "hd ?ps2T = (2,3)" "last ?ps2T = (1,1)"
          using ps2_prems knights_path_rev transpose_knights_path knights_path_non_nil 
                hd_transpose last_transpose 
          unfolding knights_circuit_def transpose_square_def by (auto simp: hd_rev last_rev)

        let ?ps1="kp5x9lr"
        have ps1_prems: "knights_path b5x9 ?ps1" "hd ?ps1 = (1,1)" "last ?ps1 = (2,8)"
          using kp_5x9_lr by simp eval+

        have "16 < length ?ps1" "last (take 16 ?ps1) = (5,4)" "hd (drop 16 ?ps1) = (4,2)" by eval+
        then have si: "step_in ?ps1 (5,4) (4,2)"
          unfolding step_in_def using zero_less_numeral by blast

        have vs: "valid_step (5,4) (int 5+2,3)" "valid_step (int 5+1,1) (4,2)"
          unfolding valid_step_def by auto

        obtain ps where "knights_path (board n m) ps" "hd ps = (1,1)" "last ps = (2,8)"
          using ‹n-5 ≥ 5› ps1_prems ps2T_prems si vs
              knights_path_split_concatT[of 5 m ?ps1 "n-5" ?ps2T "(5,4)" "(4,2)"] by auto
        then show ?thesis
          using mirror1_knights_path hd_mirror1 last_mirror1 by fastforce
      qed
    next
      let ?b1="board n 5"
      let ?b2="board n (m-5)"
      assume "m ≥ 10"
      then have "n+5 < x" "5 ≤ min n 5" "n+(m-5) < x" "5 ≤ min n (m-5)" 
        using less by auto
      then obtain ps1 ps2 where kp_prems: 
          "knights_path ?b1 ps1" "hd ps1 = (int n,1)" "last ps1 = (int n-1,4)"
          "knights_path (board n (m-5)) ps2" "hd ps2 = (int n,1)" "last ps2 = (int n-1,int (m-5)-1)"
        using less.prems less.IH[of "n+5" n "5"] less.IH[of "n+(m-5)" n "m-5"] by auto
      let ?ps="ps1@trans_path (0,int 5) ps2"
      have "valid_step (last ps1) (int n,int 5+1)" 
        unfolding valid_step_def using kp_prems by auto
      then have "knights_path (board n m) ?ps" "hd ?ps = (int n,1)" "last ?ps = (int n-1,int m-1)"
        using ‹m ≥ 10› kp_prems knights_path_concat[of n 5 ps1 "m-5" ps2] 
              knights_path_non_nil trans_path_non_nil last_trans_path by auto
      then show ?thesis by auto
    qed
  qed
qed

text ‹Auxiliary lemma that constructs a Knight's circuit if ‹m ≥ 5› and ‹n ≥ 10 ∧ even n›.›
lemma knights_circuit_exists_n_even_gr_10: 
  assumes "n ≥ 10 ∧ even n" "m ≥ 5"
  shows "∃ps. knights_circuit (board n m) ps"
  using assms
proof -
  obtain ps1 where ps1_prems: "knights_path (board 5 m) ps1" "hd ps1 = (1,1)" 
      "last ps1 = (2,int m-1)"
    using assms knights_path_5xm_exists by auto
  let ?ps1'="trans_path (int (n-5),0) ps1"
  let ?b5xm'="trans_board (int (n-5),0) (board 5 m)"
  have ps1'_prems: "knights_path ?b5xm' ?ps1'" "hd ?ps1' = (int (n-5)+1,1)" 
      "last ?ps1' = (int (n-5)+2,int m-1)"
    using ps1_prems trans_knights_path knights_path_non_nil hd_trans_path last_trans_path by auto
    
  assume "n ≥ 10 ∧ even n"
  then have "odd (n-5)" "min (n-5) m ≥ 5" using assms by auto
  then obtain ps2 where ps2_prems: "knights_path (board (n-5) m) ps2" "hd ps2 = (int (n-5),1)" 
      "last ps2 = (int (n-5)-1,int m-1)"
    using knights_path_odd_n_exists[of "n-5" m] by auto
  let ?ps2'="mirror2 ps2"
  have ps2'_prems: "knights_path (board (n-5) m) ?ps2'" "hd ?ps2' = (int (n-5),int m)" 
      "last ?ps2' = (int (n-5)-1,2)"
    using ps2_prems mirror2_knights_path hd_mirror2 last_mirror2 by auto

  have inter: "?b5xm' ∩ board (n-5) m = {}" 
    unfolding trans_board_def board_def by auto 

  have union: "board n m = ?b5xm' ∪ board (n-5) m"
    using ‹n ≥ 10 ∧ even n› board_concatT[of "n-5" m 5] by auto

  have vs: "valid_step (last ?ps1') (hd ?ps2')" "valid_step (last ?ps2') (hd ?ps1')"
    using ps1'_prems ps2'_prems unfolding valid_step_def by auto

  let ?ps="?ps1' @ ?ps2'"
  have "last ?ps = last ?ps2'" "hd ?ps = hd ?ps1'"
    using ps1'_prems ps2'_prems knights_path_non_nil by auto
  then have vs_c: "valid_step (last ?ps) (hd ?ps)"
    using vs by auto

  have "knights_path (board n m) ?ps"
    using ps1'_prems ps2'_prems inter union vs knights_path_append by auto
  then show ?thesis
    using vs_c unfolding knights_circuit_def by blast
qed

text ‹Final Theorem 1: For every ‹n×m›-board with ‹min n m ≥ 5› and ‹n*m› even there exists a 
Knight's circuit.›
theorem knights_circuit_exists: 
  assumes "min n m ≥ 5" "even (n*m)"
  shows "∃ps. knights_circuit (board n m) ps"
  using assms
proof -
  have "n = 6 ∨ m = 6 ∨ n = 8 ∨ m = 8 ∨ (n ≥ 10 ∧ even n) ∨ (m ≥ 10 ∧ even m)"
    using assms by auto
  then show ?thesis
  proof (elim disjE)
    assume "n = 6"
    then show ?thesis
      using assms knights_path_6xm_exists by auto
  next
    assume "m = 6"
    then obtain ps where "knights_circuit (board m n) ps"
      using assms knights_path_6xm_exists by auto
    then show ?thesis
      using transpose_knights_circuit by auto
  next
    assume "n = 8"
    then show ?thesis
      using assms knights_path_8xm_exists by auto
  next
    assume "m = 8"
    then obtain ps where "knights_circuit (board m n) ps"
      using assms knights_path_8xm_exists by auto
    then show ?thesis
      using transpose_knights_circuit by auto
  next
    assume "n ≥ 10 ∧ even n"
    then show ?thesis
      using assms knights_circuit_exists_n_even_gr_10 by auto
  next
    assume "m ≥ 10 ∧ even m"
    then obtain ps where "knights_circuit (board m n) ps"
      using assms knights_circuit_exists_n_even_gr_10 by auto
    then show ?thesis
      using transpose_knights_circuit by auto
  qed
qed

text ‹Final Theorem 2: for every ‹n×m›-board with ‹min n m ≥ 5› there exists a Knight's path.›
theorem knights_path_exists: 
  assumes "min n m ≥ 5"
  shows "∃ps. knights_path (board n m) ps"
  using assms
proof -
  have "odd n ∨ odd m ∨ even (n*m)" by simp
  then show ?thesis
  proof (elim disjE)
    assume "odd n"
    then show ?thesis
      using assms knights_path_odd_n_exists by auto
  next
    assume "odd m"
    then obtain ps where "knights_path (board m n) ps"
      using assms knights_path_odd_n_exists by auto
    then show ?thesis
      using transpose_knights_path by auto
  next
    assume "even (n*m)"
    then show ?thesis
      using assms knights_circuit_exists by (auto simp: knights_circuit_def)
  qed
qed

text ‹THE END›

end