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