Theory Tilings

(*
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
                Tobias Nipkow, TUM
*)

theory Tilings imports Main begin

section‹Inductive Tiling›

inductive_set
  tiling :: "'a set set ⇒ 'a set set"
  for A :: "'a set set" where
    empty [simp, intro]: "{} ∈ tiling A" |
    Un [simp, intro]:    "⟦ a ∈ A; t ∈ tiling A; a ∩ t = {} ⟧
                         ⟹ a ∪ t ∈ tiling A"

lemma tiling_UnI [intro]:
  "⟦ t ∈ tiling A; u ∈ tiling A; t ∩ u = {} ⟧ ⟹  t ∪ u ∈ tiling A"
  by (induct set: tiling) (auto simp: Un_assoc)

lemma tiling_Diff1E:
  assumes "t-a ∈ tiling A" and "a ∈ A" and "a ⊆ t"
  shows "t ∈ tiling A"
  by (metis Diff_disjoint Diff_partition assms tiling.Un)

lemma tiling_finite:
  assumes "⋀a. a ∈ A ⟹ finite a"
  shows "t ∈ tiling A ⟹ finite t"
  by (induct set: tiling) (use assms in auto)


section‹The Mutilated Chess Board Cannot be Tiled by Dominoes›

text ‹The originator of this problem is Max Black, according to J A
Robinson. It was popularized as the \emph{Mutilated Checkerboard Problem} by
J McCarthy.›

inductive_set domino :: "(nat × nat) set set" where
  horiz [simp]: "{(i, j), (i, Suc j)} ∈ domino" |
  vertl [simp]: "{(i, j), (Suc i, j)} ∈ domino"

lemma domino_finite: "d ∈ domino ⟹ finite d"
  by (erule domino.cases, auto)

declare tiling_finite[OF domino_finite, simp]

text ‹\medskip Sets of squares of the given colour›

definition
  coloured :: "nat ⇒ (nat × nat) set" where
  "coloured b = {(i, j). (i + j) mod 2 = b}"

abbreviation
  whites  :: "(nat × nat) set" where
  "whites ≡ coloured 0"

abbreviation
  blacks  :: "(nat × nat) set" where
  "blacks ≡ coloured (Suc 0)"


text ‹\medskip Chess boards›

lemma Sigma_Suc1 [simp]:
  "{0..< Suc n} × B = ({n} × B) ∪ ({0..<n} × B)"
  by auto

lemma Sigma_Suc2 [simp]:
  "A × {0..< Suc n} = (A × {n}) ∪ (A × {0..<n})"
  by auto

lemma dominoes_tile_row [intro!]: "{i} × {0..< 2*n} ∈ tiling domino"
  by (induct n) (auto simp flip: Un_insert_left Un_assoc)

lemma dominoes_tile_matrix: "{0..<m} × {0..< 2*n} ∈ tiling domino"
  by (induct m) auto


text ‹\medskip @{term coloured} and Dominoes›

lemma coloured_insert [simp]:
  "coloured b ∩ (insert (i, j) t) =
   (if (i + j) mod 2 = b then insert (i, j) (coloured b ∩ t)
    else coloured b ∩ t)"
by (auto simp: coloured_def)

lemma domino_singletons:
  "d ∈ domino ⟹
   (∃i j. whites ∩ d = {(i, j)}) ∧
   (∃m n. blacks ∩ d = {(m, n)})"
  by (elim domino.cases) (auto simp: mod_Suc)


text ‹\medskip Tilings of dominoes›

declare
  Int_Un_distrib [simp]
  Diff_Int_distrib [simp]

lemma tiling_domino_0_1:
  "t ∈ tiling domino ⟹ card(whites ∩ t) = card(blacks ∩ t)"
proof (induct set: tiling)
  case empty
  then show ?case
    by auto
next
  case (Un d t)
  ― ‹this fact tells us that both ``inserts'' are non-trivial›
  then have "⋀p C. C ∩ d = {p} ⟶ p ∉ t"
    by auto
  moreover
  obtain w b where "whites ∩ d = {w}" "blacks ∩ d = {b}"
    using Un.hyps domino_singletons by force
  ultimately show ?case
    using Un by auto
qed


text ‹\medskip Final argument is surprisingly complex›

theorem gen_mutil_not_tiling:
  assumes "t ∈ tiling domino" "(i + j) mod 2 = 0"
    "(m + n) mod 2 = 0" "{(i, j), (m, n)} ⊆ t"
  shows "t - {(i, j)} - {(m, n)} ∉ tiling domino"
proof -
  have "card (whites ∩ (t - {(i,j)} - {(m,n)})) 
      < card (blacks ∩ (t - {(i,j)} - {(m,n)}))"
    using assms unfolding tiling_domino_0_1 [symmetric]
    by (simp flip: tiling_domino_0_1) (simp add: coloured_def card_Diff2_less)
  then show ?thesis
    by (metis nat_neq_iff tiling_domino_0_1)
qed

text ‹Apply the general theorem to the well-known case›

theorem mutil_not_tiling:
  assumes "t = {0..< 2 * Suc m} × {0..< 2 * Suc n}"
  shows "t - {(0,0)} - {(Suc(2 * m), Suc(2 * n))} ∉ tiling domino"
proof -
  have "t ∈ tiling domino"
    using assms dominoes_tile_matrix by blast
  with assms show ?thesis
    by (intro gen_mutil_not_tiling) auto
qed


section‹The Mutilated Chess Board Can be Tiled by Ls›

text‹Remove a arbitrary square from a chess board of size $2^n \times 2^n$.
The result can be tiled by L-shaped tiles:
\begin{picture}(8,8)
\put(0,0){\framebox(4,4){}}
\put(4,0){\framebox(4,4){}}
\put(0,4){\framebox(4,4){}}
\end{picture}.
The four possible L-shaped tiles are obtained by dropping
one of the four squares from $\{(x,y),(x+1,y),(x,y+1),(x+1,y+1)\}$:›

definition "L2 (x::nat) (y::nat) = {(x,y), (x+1,y), (x, y+1)}"
definition "L3 (x::nat) (y::nat) = {(x,y), (x+1,y), (x+1, y+1)}"
definition "L0 (x::nat) (y::nat) = {(x+1,y), (x,y+1), (x+1, y+1)}"
definition "L1 (x::nat) (y::nat) = {(x,y), (x,y+1), (x+1, y+1)}"

text‹All tiles:›

definition Ls :: "(nat * nat) set set" where
  "Ls ≡ { L0 x y | x y. True} ∪ { L1 x y | x y. True} ∪
      { L2 x y | x y. True} ∪ { L3 x y | x y. True}"

lemma LinLs: "L0 i j : Ls & L1 i j : Ls & L2 i j : Ls & L3 i j : Ls"
  by(fastforce simp: Ls_def)


text‹Square $2^n \times 2^n$ grid, shifted by $i$ and $j$:›

definition "square2 (n::nat) (i::nat) (j::nat) = {i..< 2^n+i} × {j..< 2^n+j}"

lemma in_square2[simp]:
  "(a,b) : square2 n i j ⟷ i≤a ∧ a<2^n+i ∧ j≤b ∧ b<2^n+j"
  by(simp add:square2_def)

lemma square2_Suc: "square2 (Suc n) i j =
  square2 n i j ∪ square2 n (2^n + i) j ∪ square2 n i (2^n + j) ∪
  square2 n (2^n + i) (2^n + j)"
  by auto

lemma square2_disj: "square2 n i j ∩ square2 n x y = {} ⟷
  (2^n+i ≤ x ∨ 2^n+x ≤ i) ∨ (2^n+j ≤ y ∨ 2^n+y ≤ j)" (is "?A = ?B")
proof-
  { assume ?B hence ?A by(auto simp:square2_def) }
  moreover
  { assume "¬ ?B"
    hence "(max i x, max j y) : square2 n i j ∩ square2 n x y" by simp
    hence "¬ ?A" by blast }
  ultimately show ?thesis by blast
qed

text‹Some specific lemmas:›

lemma pos_pow2: "(0::nat) < 2^n"
  by simp

declare nat_zero_less_power_iff[simp del] zero_less_power[simp del]

lemma Diff_insert_if: shows
  "B ≠ {} ⟹ a ∈ A ⟹ A - insert a B = (A-B - {a})" and
  "B ≠ {} ⟹ a ∉ A ⟹ A - insert a B = A-B"
  by auto

lemma DisjI1: "A ∩ B = {} ⟹ (A-X) ∩ B = {}"
  by blast

lemma DisjI2: "A ∩ B = {} ⟹ A ∩ (B-X) = {}"
  by blast

text‹The main theorem:›

theorem Ls_can_tile: "i ≤ a ⟹ a < 2^n + i ⟹ j ≤ b ⟹ b < 2^n + j
  ⟹ square2 n i j - {(a,b)} ∈ tiling Ls"
proof(induct n arbitrary: a b i j)
  case 0 thus ?case by (simp add:square2_def)
next
  case (Suc n) note IH = Suc(1) and a = Suc(2-3) and b = Suc(4-5)
  hence "a<2^n+i ∧ b<2^n+j ∨
         2^n+i≤a ∧ a<2^(n+1)+i ∧ b<2^n+j ∨
         a<2^n+i ∧ 2^n+j≤b ∧ b<2^(n+1)+j ∨
         2^n+i≤a ∧ a<2^(n+1)+i ∧ 2^n+j≤b ∧ b<2^(n+1)+j" (is "?A|?B|?C|?D")
    by simp arith
  moreover
  { assume "?A"
    hence "square2 n i j - {(a,b)} ∈ tiling Ls" using IH a b by auto
    moreover 
    have "square2 n (2^n+i) j - {(2^n+i,2^n+j - 1)} ∈ tiling Ls"
         "square2 n i (2^n+j) - {(2^n+i - 1, 2^n+j)} ∈ tiling Ls"
         "square2 n (2^n+i) (2^n+j) - {(2^n+i, 2^n+j)} ∈ tiling Ls"
      by (simp_all add: IH le_add_diff pos_pow2)
    ultimately
    have "square2 (n+1) i j - {(a,b)} - L0 (2^n+i - 1) (2^n+j - 1) ∈ tiling Ls"
      using  a b ‹?A›
      by (clarsimp simp: square2_Suc L0_def Un_Diff Diff_insert_if)
         (fastforce intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2]
                   simp:Int_Un_distrib2)
  } moreover
  { assume "?B"
    hence "square2 n (2^n+i) j - {(a,b)} ∈ tiling Ls" using IH a b by auto
    moreover 
    have "square2 n i j - {(2^n+i - 1,2^n+j - 1)} ∈ tiling Ls"
         "square2 n i (2^n+j) - {(2^n+i - 1, 2^n+j)} ∈ tiling Ls"
         "square2 n (2^n+i) (2^n+j) - {(2^n+i, 2^n+j)} ∈ tiling Ls"
      by (simp_all add: IH le_add_diff pos_pow2)
    ultimately
    have "square2 (n+1) i j - {(a,b)} - L1 (2^n+i - 1) (2^n+j - 1) ∈ tiling Ls"
      using  a b ‹?B›
      by (simp add: square2_Suc L1_def Un_Diff Diff_insert_if le_diff_conv2)
         (fastforce intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2]
                   simp:Int_Un_distrib2)
  } moreover
  { assume "?C"
    hence "square2 n i (2^n+j) - {(a,b)} ∈ tiling Ls" using IH a b by auto
    moreover 
    have "square2 n i j - {(2^n+i - 1,2^n+j - 1)} ∈ tiling Ls"
         "square2 n (2^n+i) j - {(2^n+i, 2^n+j - 1)} ∈ tiling Ls"
         "square2 n (2^n+i) (2^n+j) - {(2^n+i, 2^n+j)} ∈ tiling Ls"
      by (simp_all add: IH le_add_diff pos_pow2)
    ultimately
    have "square2 (n+1) i j - {(a,b)} - L3 (2^n+i - 1) (2^n+j - 1) ∈ tiling Ls"
      using  a b ‹?C›
      by (simp add: square2_Suc L3_def Un_Diff Diff_insert_if le_diff_conv2)
         (fastforce intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2]
                   simp:Int_Un_distrib2)
  } moreover
  { assume "?D"
    hence "square2 n (2^n+i) (2^n+j) -{(a,b)} ∈ tiling Ls" using IH a b by auto
    moreover 
    have "square2 n i j - {(2^n+i - 1,2^n+j - 1)} ∈ tiling Ls"
         "square2 n (2^n+i) j - {(2^n+i, 2^n+j - 1)} ∈ tiling Ls"
         "square2 n i (2^n+j) - {(2^n+i - 1, 2^n+j)} ∈ tiling Ls"
      by (simp_all add: IH le_add_diff pos_pow2)
    ultimately
    have "square2 (n+1) i j - {(a,b)} - L2 (2^n+i - 1) (2^n+j - 1) ∈ tiling Ls"
      using  a b ‹?D›
      by (simp add: square2_Suc L2_def Un_Diff Diff_insert_if le_diff_conv2)
         (fastforce intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2]
                   simp:Int_Un_distrib2)
  } moreover
  have "?A ⟹ L0 (2^n + i - 1) (2^n + j - 1) ⊆ square2 (n+1) i j - {(a, b)}"
    using a b by(simp add:L0_def) arith moreover
  have "?B ⟹ L1 (2^n + i - 1) (2^n + j - 1) ⊆ square2 (n+1) i j - {(a, b)}"
    using a b by(simp add:L1_def) arith moreover
  have "?C ⟹ L3 (2^n + i - 1) (2^n + j - 1) ⊆ square2 (n+1) i j - {(a, b)}"
    using a b by(simp add:L3_def) arith moreover
  have "?D ⟹ L2 (2^n + i - 1) (2^n + j - 1) ⊆ square2 (n+1) i j - {(a, b)}"
    using a b by(simp add:L2_def) arith
  ultimately show ?case by simp (metis LinLs tiling_Diff1E)
qed

corollary Ls_can_tile00:
  "a < 2^n ⟹ b < 2^n ⟹ square2 n 0 0 - {(a, b)} ∈ tiling Ls"
  by(intro Ls_can_tile) auto

end