src/HOL/Induct/Mutil.thy
 changeset 11046 b5f5942781a0 parent 9930 c02d48a47ed1 child 11464 ddea204de5bc
```     1.1 --- a/src/HOL/Induct/Mutil.thy	Sat Feb 03 15:22:57 2001 +0100
1.2 +++ b/src/HOL/Induct/Mutil.thy	Sat Feb 03 17:40:16 2001 +0100
1.3 @@ -1,29 +1,150 @@
1.4 -(*  Title:      HOL/Induct/Mutil
1.5 +(*  Title:      HOL/Induct/Mutil.thy
1.6      ID:         \$Id\$
1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.8      Copyright   1996  University of Cambridge
1.9 -
1.10 -The Mutilated Chess Board Problem, formalized inductively
1.11 -  Originator is Max Black, according to J A Robinson.
1.12 -  Popularized as the Mutilated Checkerboard Problem by J McCarthy
1.13  *)
1.14
1.15 -Mutil = Main +
1.16 +header {* The Mutilated Chess Board Problem *}
1.17 +
1.18 +theory Mutil = Main:
1.19
1.20 -consts     tiling :: "'a set set => 'a set set"
1.21 +text {*
1.22 +  The Mutilated Chess Board Problem, formalized inductively.
1.23 +
1.24 +  Originator is Max Black, according to J A Robinson.  Popularized as
1.25 +  the Mutilated Checkerboard Problem by J McCarthy.
1.26 +*}
1.27 +
1.28 +consts tiling :: "'a set set => 'a set set"
1.29  inductive "tiling A"
1.30 -  intrs
1.31 -    empty  "{} : tiling A"
1.32 -    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
1.33 +  intros [simp, intro]
1.34 +    empty: "{} \<in> tiling A"
1.35 +    Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
1.36
1.37 -consts    domino :: "(nat*nat)set set"
1.38 +consts domino :: "(nat \<times> nat) set set"
1.39  inductive domino
1.40 -  intrs
1.41 -    horiz  "{(i, j), (i, Suc j)} : domino"
1.42 -    vertl  "{(i, j), (Suc i, j)} : domino"
1.43 +  intros [simp]
1.44 +    horiz: "{(i, j), (i, Suc j)} \<in> domino"
1.45 +    vertl: "{(i, j), (Suc i, j)} \<in> domino"
1.46
1.47  constdefs
1.48 -  coloured  :: "nat => (nat*nat)set"
1.49 -   "coloured b == {(i,j). (i+j) mod #2 = b}"
1.50 +  coloured :: "nat => (nat \<times> nat) set"
1.51 +   "coloured b == {(i, j). (i + j) mod #2 = b}"
1.52 +
1.53 +
1.54 +text {* \medskip The union of two disjoint tilings is a tiling *}
1.55 +
1.56 +lemma tiling_UnI [rule_format, intro]:
1.57 +  "t \<in> tiling A ==> u \<in> tiling A --> t \<inter> u = {} --> t \<union> u \<in> tiling A"
1.58 +  apply (erule tiling.induct)
1.59 +   prefer 2
1.60 +   apply (simp add: Un_assoc)
1.61 +  apply auto
1.62 +  done
1.63 +
1.64 +
1.65 +text {* \medskip Chess boards *}
1.66 +
1.67 +lemma Sigma_Suc1 [simp]:
1.68 +  "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
1.69 +  apply (unfold lessThan_def)
1.70 +  apply auto
1.71 +  done
1.72 +
1.73 +lemma Sigma_Suc2 [simp]:
1.74 +  "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
1.75 +  apply (unfold lessThan_def)
1.76 +  apply auto
1.77 +  done
1.78 +
1.79 +lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
1.80 +  apply auto
1.81 +  done
1.82 +
1.83 +lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (#2 * n) \<in> tiling domino"
1.84 +  apply (induct n)
1.85 +   apply (simp_all add: Un_assoc [symmetric])
1.86 +  apply (rule tiling.Un)
1.87 +    apply (auto simp add: sing_Times_lemma)
1.88 +  done
1.89 +
1.90 +lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (#2 * n) \<in> tiling domino"
1.91 +  apply (induct m)
1.92 +   apply auto
1.93 +  done
1.94 +
1.95 +
1.96 +text {* \medskip @{term coloured} and Dominoes *}
1.97 +
1.98 +lemma coloured_insert [simp]:
1.99 +  "coloured b \<inter> (insert (i, j) t) =
1.100 +   (if (i + j) mod #2 = b then insert (i, j) (coloured b \<inter> t)
1.101 +    else coloured b \<inter> t)"
1.102 +  apply (unfold coloured_def)
1.103 +  apply auto
1.104 +  done
1.105 +
1.106 +lemma domino_singletons:
1.107 +  "d \<in> domino ==>
1.108 +    (\<exists>i j. coloured 0 \<inter> d = {(i, j)}) \<and>
1.109 +    (\<exists>m n. coloured 1 \<inter> d = {(m, n)})"
1.110 +  apply (erule domino.cases)
1.111 +   apply (auto simp add: mod_Suc)
1.112 +  done
1.113 +
1.114 +lemma domino_finite [simp]: "d \<in> domino ==> finite d"
1.115 +  apply (erule domino.cases)
1.116 +   apply auto
1.117 +  done
1.118 +
1.119 +
1.120 +text {* \medskip Tilings of dominoes *}
1.121 +
1.122 +lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
1.123 +  apply (erule tiling.induct)
1.124 +   apply auto
1.125 +  done
1.126 +
1.127 +declare
1.128 +  Int_Un_distrib [simp]
1.129 +  Diff_Int_distrib [simp]
1.130 +
1.131 +lemma tiling_domino_0_1:
1.132 +  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
1.133 +  apply (erule tiling.induct)
1.134 +   apply (drule_tac [2] domino_singletons)
1.135 +   apply auto
1.136 +  apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
1.137 +    -- {* this lemma tells us that both ``inserts'' are non-trivial *}
1.138 +   apply (simp (no_asm_simp))
1.139 +  apply blast
1.140 +  done
1.141 +
1.142 +
1.143 +text {* \medskip Final argument is surprisingly complex *}
1.144 +
1.145 +theorem gen_mutil_not_tiling:
1.146 +  "t \<in> tiling domino ==>
1.147 +    (i + j) mod #2 = 0 ==> (m + n) mod #2 = 0 ==>
1.148 +    {(i, j), (m, n)} \<subseteq> t
1.149 +  ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
1.150 +  apply (rule notI)
1.151 +  apply (subgoal_tac
1.152 +    "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
1.153 +      card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
1.154 +   apply (force simp only: tiling_domino_0_1)
1.155 +  apply (simp add: tiling_domino_0_1 [symmetric])
1.156 +  apply (simp add: coloured_def card_Diff2_less)
1.157 +  done
1.158 +
1.159 +text {* Apply the general theorem to the well-known case *}
1.160 +
1.161 +theorem mutil_not_tiling:
1.162 +  "t = lessThan (#2 * Suc m) \<times> lessThan (#2 * Suc n)
1.163 +    ==> t - {(0, 0)} - {(Suc (#2 * m), Suc (#2 * n))} \<notin> tiling domino"
1.164 +  apply (rule gen_mutil_not_tiling)
1.165 +     apply (blast intro!: dominoes_tile_matrix)
1.166 +    apply auto
1.167 +  done
1.168
1.169  end
```