src/HOL/Induct/Mutil.thy
author wenzelm
Sat Feb 03 17:40:16 2001 +0100 (2001-02-03)
changeset 11046 b5f5942781a0
parent 9930 c02d48a47ed1
child 11464 ddea204de5bc
permissions -rw-r--r--
Induct: converted some theories to new-style format;
     1 (*  Title:      HOL/Induct/Mutil.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 header {* The Mutilated Chess Board Problem *}
     8 
     9 theory Mutil = Main:
    10 
    11 text {*
    12   The Mutilated Chess Board Problem, formalized inductively.
    13 
    14   Originator is Max Black, according to J A Robinson.  Popularized as
    15   the Mutilated Checkerboard Problem by J McCarthy.
    16 *}
    17 
    18 consts tiling :: "'a set set => 'a set set"
    19 inductive "tiling A"
    20   intros [simp, intro]
    21     empty: "{} \<in> tiling A"
    22     Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
    23 
    24 consts domino :: "(nat \<times> nat) set set"
    25 inductive domino
    26   intros [simp]
    27     horiz: "{(i, j), (i, Suc j)} \<in> domino"
    28     vertl: "{(i, j), (Suc i, j)} \<in> domino"
    29 
    30 constdefs
    31   coloured :: "nat => (nat \<times> nat) set"
    32    "coloured b == {(i, j). (i + j) mod #2 = b}"
    33 
    34 
    35 text {* \medskip The union of two disjoint tilings is a tiling *}
    36 
    37 lemma tiling_UnI [rule_format, intro]:
    38   "t \<in> tiling A ==> u \<in> tiling A --> t \<inter> u = {} --> t \<union> u \<in> tiling A"
    39   apply (erule tiling.induct)
    40    prefer 2
    41    apply (simp add: Un_assoc)
    42   apply auto
    43   done
    44 
    45 
    46 text {* \medskip Chess boards *}
    47 
    48 lemma Sigma_Suc1 [simp]:
    49   "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
    50   apply (unfold lessThan_def)
    51   apply auto
    52   done
    53 
    54 lemma Sigma_Suc2 [simp]:
    55   "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
    56   apply (unfold lessThan_def)
    57   apply auto
    58   done
    59 
    60 lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
    61   apply auto
    62   done
    63 
    64 lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (#2 * n) \<in> tiling domino"
    65   apply (induct n)
    66    apply (simp_all add: Un_assoc [symmetric])
    67   apply (rule tiling.Un)
    68     apply (auto simp add: sing_Times_lemma)
    69   done
    70 
    71 lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (#2 * n) \<in> tiling domino"
    72   apply (induct m)
    73    apply auto
    74   done
    75 
    76 
    77 text {* \medskip @{term coloured} and Dominoes *}
    78 
    79 lemma coloured_insert [simp]:
    80   "coloured b \<inter> (insert (i, j) t) =
    81    (if (i + j) mod #2 = b then insert (i, j) (coloured b \<inter> t)
    82     else coloured b \<inter> t)"
    83   apply (unfold coloured_def)
    84   apply auto
    85   done
    86 
    87 lemma domino_singletons:
    88   "d \<in> domino ==>
    89     (\<exists>i j. coloured 0 \<inter> d = {(i, j)}) \<and>
    90     (\<exists>m n. coloured 1 \<inter> d = {(m, n)})"
    91   apply (erule domino.cases)
    92    apply (auto simp add: mod_Suc)
    93   done
    94 
    95 lemma domino_finite [simp]: "d \<in> domino ==> finite d"
    96   apply (erule domino.cases)
    97    apply auto
    98   done
    99 
   100 
   101 text {* \medskip Tilings of dominoes *}
   102 
   103 lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
   104   apply (erule tiling.induct)
   105    apply auto
   106   done
   107 
   108 declare
   109   Int_Un_distrib [simp]
   110   Diff_Int_distrib [simp]
   111 
   112 lemma tiling_domino_0_1:
   113   "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
   114   apply (erule tiling.induct)
   115    apply (drule_tac [2] domino_singletons)
   116    apply auto
   117   apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
   118     -- {* this lemma tells us that both ``inserts'' are non-trivial *}
   119    apply (simp (no_asm_simp))
   120   apply blast
   121   done
   122 
   123 
   124 text {* \medskip Final argument is surprisingly complex *}
   125 
   126 theorem gen_mutil_not_tiling:
   127   "t \<in> tiling domino ==>
   128     (i + j) mod #2 = 0 ==> (m + n) mod #2 = 0 ==>
   129     {(i, j), (m, n)} \<subseteq> t
   130   ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
   131   apply (rule notI)
   132   apply (subgoal_tac
   133     "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
   134       card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
   135    apply (force simp only: tiling_domino_0_1)
   136   apply (simp add: tiling_domino_0_1 [symmetric])
   137   apply (simp add: coloured_def card_Diff2_less)
   138   done
   139 
   140 text {* Apply the general theorem to the well-known case *}
   141 
   142 theorem mutil_not_tiling:
   143   "t = lessThan (#2 * Suc m) \<times> lessThan (#2 * Suc n)
   144     ==> t - {(0, 0)} - {(Suc (#2 * m), Suc (#2 * n))} \<notin> tiling domino"
   145   apply (rule gen_mutil_not_tiling)
   146      apply (blast intro!: dominoes_tile_matrix)
   147     apply auto
   148   done
   149 
   150 end