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