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
```