# Theory Mutil

Up to index of Isabelle/HOL/Induct

theory Mutil
imports Main
begin

    (*  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