1 (* Title: HOL/Induct/Mutil.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Tobias Nipkow, TUM (part 2) |
|
5 *) |
|
6 |
|
7 header {* The Mutilated Chess Board Problem *} |
|
8 |
|
9 theory Mutil imports Main begin |
|
10 |
|
11 subsection{* The Mutilated Chess Board Cannot be Tiled by Dominoes *} |
|
12 |
|
13 text {* |
|
14 The Mutilated Chess Board Problem, formalized inductively. |
|
15 |
|
16 Originator is Max Black, according to J A Robinson. Popularized as |
|
17 the Mutilated Checkerboard Problem by J McCarthy. |
|
18 *} |
|
19 |
|
20 inductive_set |
|
21 tiling :: "'a set set => 'a set set" |
|
22 for A :: "'a set set" |
|
23 where |
|
24 empty [simp, intro]: "{} \<in> tiling A" |
|
25 | Un [simp, intro]: "[| a \<in> A; t \<in> tiling A; a \<inter> t = {} |] |
|
26 ==> a \<union> t \<in> tiling A" |
|
27 |
|
28 inductive_set |
|
29 domino :: "(nat \<times> nat) set set" |
|
30 where |
|
31 horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino" |
|
32 | vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino" |
|
33 |
|
34 text {* \medskip Sets of squares of the given colour*} |
|
35 |
|
36 definition |
|
37 coloured :: "nat => (nat \<times> nat) set" where |
|
38 "coloured b = {(i, j). (i + j) mod 2 = b}" |
|
39 |
|
40 abbreviation |
|
41 whites :: "(nat \<times> nat) set" where |
|
42 "whites == coloured 0" |
|
43 |
|
44 abbreviation |
|
45 blacks :: "(nat \<times> nat) set" where |
|
46 "blacks == coloured (Suc 0)" |
|
47 |
|
48 |
|
49 text {* \medskip The union of two disjoint tilings is a tiling *} |
|
50 |
|
51 lemma tiling_UnI [intro]: |
|
52 "[|t \<in> tiling A; u \<in> tiling A; t \<inter> u = {} |] ==> t \<union> u \<in> tiling A" |
|
53 apply (induct set: tiling) |
|
54 apply (auto simp add: Un_assoc) |
|
55 done |
|
56 |
|
57 |
|
58 lemma tiling_Diff1E [intro]: |
|
59 assumes "t-a \<in> tiling A" "a \<in> A" "a \<subseteq> t" |
|
60 shows "t \<in> tiling A" |
|
61 proof - |
|
62 from assms(2-3) have "EX r. t = r Un a & r Int a = {}" |
|
63 by (metis Diff_disjoint Int_commute Un_Diff_cancel Un_absorb1 Un_commute) |
|
64 thus ?thesis using assms(1,2) |
|
65 by (auto simp:Un_Diff) |
|
66 (metis Compl_Diff_eq Diff_Compl Diff_empty Int_commute Un_Diff_cancel |
|
67 Un_commute double_complement tiling.Un) |
|
68 qed |
|
69 |
|
70 |
|
71 text {* \medskip Chess boards *} |
|
72 |
|
73 lemma Sigma_Suc1 [simp]: |
|
74 "{0..< Suc n} \<times> B = ({n} \<times> B) \<union> ({0..<n} \<times> B)" |
|
75 by auto |
|
76 |
|
77 lemma Sigma_Suc2 [simp]: |
|
78 "A \<times> {0..< Suc n} = (A \<times> {n}) \<union> (A \<times> {0..<n})" |
|
79 by auto |
|
80 |
|
81 lemma dominoes_tile_row [intro!]: "{i} \<times> {0..< 2*n} \<in> tiling domino" |
|
82 apply (induct n) |
|
83 apply (simp_all del:Un_insert_left add: Un_assoc [symmetric]) |
|
84 done |
|
85 |
|
86 lemma dominoes_tile_matrix: "{0..<m} \<times> {0..< 2*n} \<in> tiling domino" |
|
87 by (induct m) auto |
|
88 |
|
89 |
|
90 text {* \medskip @{term coloured} and Dominoes *} |
|
91 |
|
92 lemma coloured_insert [simp]: |
|
93 "coloured b \<inter> (insert (i, j) t) = |
|
94 (if (i + j) mod 2 = b then insert (i, j) (coloured b \<inter> t) |
|
95 else coloured b \<inter> t)" |
|
96 by (auto simp add: coloured_def) |
|
97 |
|
98 lemma domino_singletons: |
|
99 "d \<in> domino ==> |
|
100 (\<exists>i j. whites \<inter> d = {(i, j)}) \<and> |
|
101 (\<exists>m n. blacks \<inter> d = {(m, n)})"; |
|
102 apply (erule domino.cases) |
|
103 apply (auto simp add: mod_Suc) |
|
104 done |
|
105 |
|
106 lemma domino_finite [simp]: "d \<in> domino ==> finite d" |
|
107 by (erule domino.cases, auto) |
|
108 |
|
109 |
|
110 text {* \medskip Tilings of dominoes *} |
|
111 |
|
112 lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t" |
|
113 by (induct set: tiling) auto |
|
114 |
|
115 declare |
|
116 Int_Un_distrib [simp] |
|
117 Diff_Int_distrib [simp] |
|
118 |
|
119 lemma tiling_domino_0_1: |
|
120 "t \<in> tiling domino ==> card(whites \<inter> t) = card(blacks \<inter> t)" |
|
121 apply (induct set: tiling) |
|
122 apply (drule_tac [2] domino_singletons) |
|
123 apply auto |
|
124 apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t") |
|
125 -- {* this lemma tells us that both ``inserts'' are non-trivial *} |
|
126 apply (simp (no_asm_simp)) |
|
127 apply blast |
|
128 done |
|
129 |
|
130 |
|
131 text {* \medskip Final argument is surprisingly complex *} |
|
132 |
|
133 theorem gen_mutil_not_tiling: |
|
134 "t \<in> tiling domino ==> |
|
135 (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==> |
|
136 {(i, j), (m, n)} \<subseteq> t |
|
137 ==> (t - {(i,j)} - {(m,n)}) \<notin> tiling domino" |
|
138 apply (rule notI) |
|
139 apply (subgoal_tac |
|
140 "card (whites \<inter> (t - {(i,j)} - {(m,n)})) < |
|
141 card (blacks \<inter> (t - {(i,j)} - {(m,n)}))") |
|
142 apply (force simp only: tiling_domino_0_1) |
|
143 apply (simp add: tiling_domino_0_1 [symmetric]) |
|
144 apply (simp add: coloured_def card_Diff2_less) |
|
145 done |
|
146 |
|
147 text {* Apply the general theorem to the well-known case *} |
|
148 |
|
149 theorem mutil_not_tiling: |
|
150 "t = {0..< 2 * Suc m} \<times> {0..< 2 * Suc n} |
|
151 ==> t - {(0,0)} - {(Suc(2 * m), Suc(2 * n))} \<notin> tiling domino" |
|
152 apply (rule gen_mutil_not_tiling) |
|
153 apply (blast intro!: dominoes_tile_matrix) |
|
154 apply auto |
|
155 done |
|
156 |
|
157 |
|
158 subsection{* The Mutilated Chess Board Can be Tiled by Ls *} |
|
159 |
|
160 text{* We remove any square from a chess board of size $2^n \times 2^n$. |
|
161 The result can be tiled by L-shaped tiles. |
|
162 Found in Velleman's \emph{How to Prove it}. |
|
163 |
|
164 The four possible L-shaped tiles are obtained by dropping |
|
165 one of the four squares from $\{(x,y),(x+1,y),(x,y+1),(x+1,y+1)\}$: *} |
|
166 |
|
167 definition "L2 (x::nat) (y::nat) = {(x,y), (x+1,y), (x, y+1)}" |
|
168 definition "L3 (x::nat) (y::nat) = {(x,y), (x+1,y), (x+1, y+1)}" |
|
169 definition "L0 (x::nat) (y::nat) = {(x+1,y), (x,y+1), (x+1, y+1)}" |
|
170 definition "L1 (x::nat) (y::nat) = {(x,y), (x,y+1), (x+1, y+1)}" |
|
171 |
|
172 text{* All tiles: *} |
|
173 |
|
174 definition Ls :: "(nat * nat) set set" where |
|
175 "Ls \<equiv> { L0 x y | x y. True} \<union> { L1 x y | x y. True} \<union> |
|
176 { L2 x y | x y. True} \<union> { L3 x y | x y. True}" |
|
177 |
|
178 lemma LinLs: "L0 i j : Ls & L1 i j : Ls & L2 i j : Ls & L3 i j : Ls" |
|
179 by(fastsimp simp:Ls_def) |
|
180 |
|
181 |
|
182 text{* Square $2^n \times 2^n$ grid, shifted by $i$ and $j$: *} |
|
183 |
|
184 definition "square2 (n::nat) (i::nat) (j::nat) = {i..< 2^n+i} \<times> {j..< 2^n+j}" |
|
185 |
|
186 lemma in_square2[simp]: |
|
187 "(a,b) : square2 n i j \<longleftrightarrow> i\<le>a \<and> a<2^n+i \<and> j\<le>b \<and> b<2^n+j" |
|
188 by(simp add:square2_def) |
|
189 |
|
190 lemma square2_Suc: "square2 (Suc n) i j = |
|
191 square2 n i j \<union> square2 n (2^n + i) j \<union> square2 n i (2^n + j) \<union> |
|
192 square2 n (2^n + i) (2^n + j)" |
|
193 by(auto simp:square2_def) |
|
194 |
|
195 lemma square2_disj: "square2 n i j \<inter> square2 n x y = {} \<longleftrightarrow> |
|
196 (2^n+i \<le> x \<or> 2^n+x \<le> i) \<or> (2^n+j \<le> y \<or> 2^n+y \<le> j)" (is "?A = ?B") |
|
197 proof- |
|
198 { assume ?B hence ?A by(auto simp:square2_def) } |
|
199 moreover |
|
200 { assume "\<not> ?B" |
|
201 hence "(max i x, max j y) : square2 n i j \<inter> square2 n x y" by simp |
|
202 hence "\<not> ?A" by blast } |
|
203 ultimately show ?thesis by blast |
|
204 qed |
|
205 |
|
206 text{* Some specific lemmas: *} |
|
207 |
|
208 lemma pos_pow2: "(0::nat) < 2^(n::nat)" |
|
209 by simp |
|
210 |
|
211 declare nat_zero_less_power_iff[simp del] zero_less_power[simp del] |
|
212 |
|
213 lemma Diff_insert_if: shows |
|
214 "B \<noteq> {} \<Longrightarrow> a:A \<Longrightarrow> A - insert a B = (A-B - {a})" and |
|
215 "B \<noteq> {} \<Longrightarrow> a ~: A \<Longrightarrow> A - insert a B = A-B" |
|
216 by auto |
|
217 |
|
218 lemma DisjI1: "A Int B = {} \<Longrightarrow> (A-X) Int B = {}" |
|
219 by blast |
|
220 lemma DisjI2: "A Int B = {} \<Longrightarrow> A Int (B-X) = {}" |
|
221 by blast |
|
222 |
|
223 text{* The main theorem: *} |
|
224 |
|
225 declare [[max_clauses = 200]] |
|
226 |
|
227 theorem Ls_can_tile: "i \<le> a \<Longrightarrow> a < 2^n + i \<Longrightarrow> j \<le> b \<Longrightarrow> b < 2^n + j |
|
228 \<Longrightarrow> square2 n i j - {(a,b)} : tiling Ls" |
|
229 proof(induct n arbitrary: a b i j) |
|
230 case 0 thus ?case by (simp add:square2_def) |
|
231 next |
|
232 case (Suc n) note IH = Suc(1) and a = Suc(2-3) and b = Suc(4-5) |
|
233 hence "a<2^n+i \<and> b<2^n+j \<or> |
|
234 2^n+i\<le>a \<and> a<2^(n+1)+i \<and> b<2^n+j \<or> |
|
235 a<2^n+i \<and> 2^n+j\<le>b \<and> b<2^(n+1)+j \<or> |
|
236 2^n+i\<le>a \<and> a<2^(n+1)+i \<and> 2^n+j\<le>b \<and> b<2^(n+1)+j" (is "?A|?B|?C|?D") |
|
237 by simp arith |
|
238 moreover |
|
239 { assume "?A" |
|
240 hence "square2 n i j - {(a,b)} : tiling Ls" using IH a b by auto |
|
241 moreover have "square2 n (2^n+i) j - {(2^n+i,2^n+j - 1)} : tiling Ls" |
|
242 by(rule IH)(insert pos_pow2[of n], auto) |
|
243 moreover have "square2 n i (2^n+j) - {(2^n+i - 1, 2^n+j)} : tiling Ls" |
|
244 by(rule IH)(insert pos_pow2[of n], auto) |
|
245 moreover have "square2 n (2^n+i) (2^n+j) - {(2^n+i, 2^n+j)} : tiling Ls" |
|
246 by(rule IH)(insert pos_pow2[of n], auto) |
|
247 ultimately |
|
248 have "square2 (n+1) i j - {(a,b)} - L0 (2^n+i - 1) (2^n+j - 1) \<in> tiling Ls" |
|
249 using a b `?A` |
|
250 by (clarsimp simp: square2_Suc L0_def Un_Diff Diff_insert_if) |
|
251 (fastsimp intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2] |
|
252 simp:Int_Un_distrib2) |
|
253 } moreover |
|
254 { assume "?B" |
|
255 hence "square2 n (2^n+i) j - {(a,b)} : tiling Ls" using IH a b by auto |
|
256 moreover have "square2 n i j - {(2^n+i - 1,2^n+j - 1)} : tiling Ls" |
|
257 by(rule IH)(insert pos_pow2[of n], auto) |
|
258 moreover have "square2 n i (2^n+j) - {(2^n+i - 1, 2^n+j)} : tiling Ls" |
|
259 by(rule IH)(insert pos_pow2[of n], auto) |
|
260 moreover have "square2 n (2^n+i) (2^n+j) - {(2^n+i, 2^n+j)} : tiling Ls" |
|
261 by(rule IH)(insert pos_pow2[of n], auto) |
|
262 ultimately |
|
263 have "square2 (n+1) i j - {(a,b)} - L1 (2^n+i - 1) (2^n+j - 1) \<in> tiling Ls" |
|
264 using a b `?B` |
|
265 by (simp add: square2_Suc L1_def Un_Diff Diff_insert_if le_diff_conv2) |
|
266 (fastsimp intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2] |
|
267 simp:Int_Un_distrib2) |
|
268 } moreover |
|
269 { assume "?C" |
|
270 hence "square2 n i (2^n+j) - {(a,b)} : tiling Ls" using IH a b by auto |
|
271 moreover have "square2 n i j - {(2^n+i - 1,2^n+j - 1)} : tiling Ls" |
|
272 by(rule IH)(insert pos_pow2[of n], auto) |
|
273 moreover have "square2 n (2^n+i) j - {(2^n+i, 2^n+j - 1)} : tiling Ls" |
|
274 by(rule IH)(insert pos_pow2[of n], auto) |
|
275 moreover have "square2 n (2^n+i) (2^n+j) - {(2^n+i, 2^n+j)} : tiling Ls" |
|
276 by(rule IH)(insert pos_pow2[of n], auto) |
|
277 ultimately |
|
278 have "square2 (n+1) i j - {(a,b)} - L3 (2^n+i - 1) (2^n+j - 1) \<in> tiling Ls" |
|
279 using a b `?C` |
|
280 by (simp add: square2_Suc L3_def Un_Diff Diff_insert_if le_diff_conv2) |
|
281 (fastsimp intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2] |
|
282 simp:Int_Un_distrib2) |
|
283 } moreover |
|
284 { assume "?D" |
|
285 hence "square2 n (2^n+i) (2^n+j) -{(a,b)} : tiling Ls" using IH a b by auto |
|
286 moreover have "square2 n i j - {(2^n+i - 1,2^n+j - 1)} : tiling Ls" |
|
287 by(rule IH)(insert pos_pow2[of n], auto) |
|
288 moreover have "square2 n (2^n+i) j - {(2^n+i, 2^n+j - 1)} : tiling Ls" |
|
289 by(rule IH)(insert pos_pow2[of n], auto) |
|
290 moreover have "square2 n i (2^n+j) - {(2^n+i - 1, 2^n+j)} : tiling Ls" |
|
291 by(rule IH)(insert pos_pow2[of n], auto) |
|
292 ultimately |
|
293 have "square2 (n+1) i j - {(a,b)} - L2 (2^n+i - 1) (2^n+j - 1) \<in> tiling Ls" |
|
294 using a b `?D` |
|
295 by (simp add: square2_Suc L2_def Un_Diff Diff_insert_if le_diff_conv2) |
|
296 (fastsimp intro!: tiling_UnI DisjI1 DisjI2 square2_disj[THEN iffD2] |
|
297 simp:Int_Un_distrib2) |
|
298 } moreover |
|
299 have "?A \<Longrightarrow> L0 (2^n + i - 1) (2^n + j - 1) \<subseteq> square2 (n+1) i j - {(a, b)}" |
|
300 using a b by(simp add:L0_def) arith moreover |
|
301 have "?B \<Longrightarrow> L1 (2^n + i - 1) (2^n + j - 1) \<subseteq> square2 (n+1) i j - {(a, b)}" |
|
302 using a b by(simp add:L1_def) arith moreover |
|
303 have "?C \<Longrightarrow> L3 (2^n + i - 1) (2^n + j - 1) \<subseteq> square2 (n+1) i j - {(a, b)}" |
|
304 using a b by(simp add:L3_def) arith moreover |
|
305 have "?D \<Longrightarrow> L2 (2^n + i - 1) (2^n + j - 1) \<subseteq> square2 (n+1) i j - {(a, b)}" |
|
306 using a b by(simp add:L2_def) arith |
|
307 ultimately show ?case by simp (metis LinLs tiling_Diff1E) |
|
308 qed |
|
309 |
|
310 corollary Ls_can_tile00: |
|
311 "a < 2^n \<Longrightarrow> b < 2^n \<Longrightarrow> square2 n 0 0 - {(a, b)} \<in> tiling Ls" |
|
312 by(rule Ls_can_tile) auto |
|
313 |
|
314 end |
|