src/HOL/Induct/Mutil.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 21404 eb85850d3eb7
child 23506 332a9f5c7c29
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     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 imports Main begin
    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
    21     empty [simp, intro]: "{} \<in> tiling A"
    22     Un [simp, intro]:    "[| a \<in> A; t \<in> tiling A; a \<inter> t = {} |] 
    23                           ==> a \<union> t \<in> tiling A"
    24 
    25 consts domino :: "(nat \<times> nat) set set"
    26 inductive domino
    27   intros
    28     horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino"
    29     vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino"
    30 
    31 text {* \medskip Sets of squares of the given colour*}
    32 
    33 definition
    34   coloured :: "nat => (nat \<times> nat) set" where
    35   "coloured b = {(i, j). (i + j) mod 2 = b}"
    36 
    37 abbreviation
    38   whites  :: "(nat \<times> nat) set" where
    39   "whites == coloured 0"
    40 
    41 abbreviation
    42   blacks  :: "(nat \<times> nat) set" where
    43   "blacks == coloured (Suc 0)"
    44 
    45 
    46 text {* \medskip The union of two disjoint tilings is a tiling *}
    47 
    48 lemma tiling_UnI [intro]:
    49      "[|t \<in> tiling A; u \<in> tiling A; t \<inter> u = {} |] ==>  t \<union> u \<in> tiling A"
    50   apply (induct set: tiling)
    51   apply (auto simp add: Un_assoc)
    52   done
    53 
    54 
    55 text {* \medskip Chess boards *}
    56 
    57 lemma Sigma_Suc1 [simp]:
    58      "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
    59   by (auto simp add: lessThan_def)
    60 
    61 lemma Sigma_Suc2 [simp]:
    62      "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
    63   by (auto simp add: lessThan_def)
    64 
    65 lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
    66   by auto
    67 
    68 lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (2 * n) \<in> tiling domino"
    69   apply (induct n)
    70    apply (simp_all add: Un_assoc [symmetric])
    71   apply (rule tiling.Un)
    72     apply (auto simp add: sing_Times_lemma)
    73   done
    74 
    75 lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino"
    76   by (induct m) auto
    77 
    78 
    79 text {* \medskip @{term coloured} and Dominoes *}
    80 
    81 lemma coloured_insert [simp]:
    82      "coloured b \<inter> (insert (i, j) t) =
    83       (if (i + j) mod 2 = b then insert (i, j) (coloured b \<inter> t)
    84        else coloured b \<inter> t)"
    85   by (auto simp add: coloured_def)
    86 
    87 lemma domino_singletons:
    88      "d \<in> domino ==>
    89        (\<exists>i j. whites \<inter> d = {(i, j)}) \<and>
    90        (\<exists>m n. blacks \<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   by (erule domino.cases, auto)
    97 
    98 
    99 text {* \medskip Tilings of dominoes *}
   100 
   101 lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
   102   by (induct set: tiling) auto
   103 
   104 declare
   105   Int_Un_distrib [simp]
   106   Diff_Int_distrib [simp]
   107 
   108 lemma tiling_domino_0_1:
   109      "t \<in> tiling domino ==> card(whites \<inter> t) = card(blacks \<inter> t)"
   110   apply (induct set: tiling)
   111    apply (drule_tac [2] domino_singletons)
   112    apply auto
   113   apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
   114     -- {* this lemma tells us that both ``inserts'' are non-trivial *}
   115    apply (simp (no_asm_simp))
   116   apply blast
   117   done
   118 
   119 
   120 text {* \medskip Final argument is surprisingly complex *}
   121 
   122 theorem gen_mutil_not_tiling:
   123        "t \<in> tiling domino ==>
   124 	 (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==>
   125 	 {(i, j), (m, n)} \<subseteq> t
   126        ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
   127   apply (rule notI)
   128   apply (subgoal_tac
   129           "card (whites \<inter> (t - {(i, j)} - {(m, n)})) <
   130            card (blacks \<inter> (t - {(i, j)} - {(m, n)}))")
   131    apply (force simp only: tiling_domino_0_1)
   132   apply (simp add: tiling_domino_0_1 [symmetric])
   133   apply (simp add: coloured_def card_Diff2_less)
   134   done
   135 
   136 text {* Apply the general theorem to the well-known case *}
   137 
   138 theorem mutil_not_tiling:
   139        "t = lessThan (2 * Suc m) \<times> lessThan (2 * Suc n)
   140 	 ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} \<notin> tiling domino"
   141   apply (rule gen_mutil_not_tiling)
   142      apply (blast intro!: dominoes_tile_matrix)
   143     apply auto
   144   done
   145 
   146 end