(* Title: HOL/Induct/Mutil.thy ID: $Id: Mutil.thy,v 1.17 2005/06/17 14:13:07 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) header {* The Mutilated Chess Board Problem *} theory Mutil imports Main begin text {* The Mutilated Chess Board Problem, formalized inductively. Originator is Max Black, according to J A Robinson. Popularized as the Mutilated Checkerboard Problem by J McCarthy. *} consts tiling :: "'a set set => 'a set set" inductive "tiling A" intros empty [simp, intro]: "{} ∈ tiling A" Un [simp, intro]: "[| a ∈ A; t ∈ tiling A; a ∩ t = {} |] ==> a ∪ t ∈ tiling A" consts domino :: "(nat × nat) set set" inductive domino intros horiz [simp]: "{(i, j), (i, Suc j)} ∈ domino" vertl [simp]: "{(i, j), (Suc i, j)} ∈ domino" text {* \medskip Sets of squares of the given colour*} constdefs coloured :: "nat => (nat × nat) set" "coloured b == {(i, j). (i + j) mod 2 = b}" syntax whites :: "(nat × nat) set" blacks :: "(nat × nat) set" translations "whites" == "coloured 0" "blacks" == "coloured (Suc 0)" text {* \medskip The union of two disjoint tilings is a tiling *} lemma tiling_UnI [intro]: "[|t ∈ tiling A; u ∈ tiling A; t ∩ u = {} |] ==> t ∪ u ∈ tiling A" apply (induct set: tiling) apply (auto simp add: Un_assoc) done text {* \medskip Chess boards *} lemma Sigma_Suc1 [simp]: "lessThan (Suc n) × B = ({n} × B) ∪ ((lessThan n) × B)" by (auto simp add: lessThan_def) lemma Sigma_Suc2 [simp]: "A × lessThan (Suc n) = (A × {n}) ∪ (A × (lessThan n))" by (auto simp add: lessThan_def) lemma sing_Times_lemma: "({i} × {n}) ∪ ({i} × {m}) = {(i, m), (i, n)}" by auto lemma dominoes_tile_row [intro!]: "{i} × lessThan (2 * n) ∈ tiling domino" apply (induct n) apply (simp_all add: Un_assoc [symmetric]) apply (rule tiling.Un) apply (auto simp add: sing_Times_lemma) done lemma dominoes_tile_matrix: "(lessThan m) × lessThan (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 add: coloured_def) lemma domino_singletons: "d ∈ domino ==> (∃i j. whites ∩ d = {(i, j)}) ∧ (∃m n. blacks ∩ d = {(m, n)})"; apply (erule domino.cases) apply (auto simp add: mod_Suc) done lemma domino_finite [simp]: "d ∈ domino ==> finite d" by (erule domino.cases, auto) text {* \medskip Tilings of dominoes *} lemma tiling_domino_finite [simp]: "t ∈ tiling domino ==> finite t" by (induct set: tiling, auto) declare Int_Un_distrib [simp] Diff_Int_distrib [simp] lemma tiling_domino_0_1: "t ∈ tiling domino ==> card(whites ∩ t) = card(blacks ∩ t)" apply (induct set: tiling) apply (drule_tac [2] domino_singletons) apply auto apply (subgoal_tac "∀p C. C ∩ a = {p} --> p ∉ t") -- {* this lemma tells us that both ``inserts'' are non-trivial *} apply (simp (no_asm_simp)) apply blast done text {* \medskip Final argument is surprisingly complex *} theorem gen_mutil_not_tiling: "t ∈ tiling domino ==> (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==> {(i, j), (m, n)} ⊆ t ==> (t - {(i, j)} - {(m, n)}) ∉ tiling domino" apply (rule notI) apply (subgoal_tac "card (whites ∩ (t - {(i, j)} - {(m, n)})) < card (blacks ∩ (t - {(i, j)} - {(m, n)}))") apply (force simp only: tiling_domino_0_1) apply (simp add: tiling_domino_0_1 [symmetric]) apply (simp add: coloured_def card_Diff2_less) done text {* Apply the general theorem to the well-known case *} theorem mutil_not_tiling: "t = lessThan (2 * Suc m) × lessThan (2 * Suc n) ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} ∉ tiling domino" apply (rule gen_mutil_not_tiling) apply (blast intro!: dominoes_tile_matrix) apply auto done end
lemma tiling_UnI:
[| t ∈ tiling A; u ∈ tiling A; t ∩ u = {} |] ==> t ∪ u ∈ tiling A
lemma Sigma_Suc1:
{..<Suc n} × B = {n} × B ∪ {..<n} × B
lemma Sigma_Suc2:
A × {..<Suc n} = A × {n} ∪ A × {..<n}
lemma sing_Times_lemma:
{i} × {n} ∪ {i} × {m} = {(i, m), (i, n)}
lemma dominoes_tile_row:
{i} × {..<2 * n} ∈ tiling domino
lemma dominoes_tile_matrix:
{..<m} × {..<2 * n} ∈ tiling domino
lemma coloured_insert:
coloured b ∩ insert (i, j) t = (if (i + j) mod 2 = b then insert (i, j) (coloured b ∩ t) else coloured b ∩ t)
lemma domino_singletons:
d ∈ domino ==> (∃i j. whites ∩ d = {(i, j)}) ∧ (∃m n. blacks ∩ d = {(m, n)})
lemma domino_finite:
d ∈ domino ==> finite d
lemma tiling_domino_finite:
t ∈ tiling domino ==> finite t
lemma tiling_domino_0_1:
t ∈ tiling domino ==> card (whites ∩ t) = card (blacks ∩ t)
theorem gen_mutil_not_tiling:
[| t ∈ tiling domino; (i + j) mod 2 = 0; (m + n) mod 2 = 0; {(i, j), (m, n)} ⊆ t |] ==> t - {(i, j)} - {(m, n)} ∉ tiling domino
theorem mutil_not_tiling:
t = {..<2 * Suc m} × {..<2 * Suc n} ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} ∉ tiling domino