1 (* Title: HOL/Isar_examples/MutilatedCheckerboard.thy |
1 (* Title: HOL/Isar_examples/MutilatedCheckerboard.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory (original script) |
3 Author: Markus Wenzel, TU Muenchen (Isar document) |
4 Markus Wenzel, TU Muenchen (Isar document) |
4 Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts) |
5 |
5 |
6 The Mutilated Chess Board Problem, formalized inductively. |
6 The Mutilated Checker Board Problem, formalized inductively. |
7 Originator is Max Black, according to J A Robinson. |
7 Originator is Max Black, according to J A Robinson. |
8 Popularized as the Mutilated Checkerboard Problem by J McCarthy. |
8 Popularized as the Mutilated Checkerboard Problem by J McCarthy. |
|
9 |
|
10 See also HOL/Induct/Mutil for the original Isabelle tactic scripts. |
9 *) |
11 *) |
10 |
12 |
11 theory MutilatedCheckerboard = Main:; |
13 theory MutilatedCheckerboard = Main:; |
12 |
14 |
13 |
15 |
30 thus "u : ??T --> t Int u = {} --> t Un u : ??T" (is "??P t"); |
32 thus "u : ??T --> t Int u = {} --> t Un u : ??T" (is "??P t"); |
31 proof (induct t set: tiling); |
33 proof (induct t set: tiling); |
32 show "??P {}"; by simp; |
34 show "??P {}"; by simp; |
33 |
35 |
34 fix a t; |
36 fix a t; |
35 assume "a:A" "t : ??T" "??P t" "a <= - t"; |
37 assume "a : A" "t : ??T" "??P t" "a <= - t"; |
36 show "??P (a Un t)"; |
38 show "??P (a Un t)"; |
37 proof (intro impI); |
39 proof (intro impI); |
38 assume "u : ??T" "(a Un t) Int u = {}"; |
40 assume "u : ??T" "(a Un t) Int u = {}"; |
39 have hyp: "t Un u: ??T"; by blast; |
41 have hyp: "t Un u: ??T"; by blast; |
40 have "a <= - (t Un u)"; by blast; |
42 have "a <= - (t Un u)"; by blast; |
43 finally; show "... : ??T"; .; |
45 finally; show "... : ??T"; .; |
44 qed; |
46 qed; |
45 qed; |
47 qed; |
46 qed; |
48 qed; |
47 |
49 |
48 lemma tiling_UnI: "[| t : tiling A; u : tiling A; t Int u = {} |] ==> t Un u : tiling A"; |
|
49 by (rule tiling_Un [rulify]); |
|
50 |
|
51 |
50 |
52 section {* Basic properties of below *}; |
51 section {* Basic properties of below *}; |
53 |
52 |
54 constdefs |
53 constdefs |
55 below :: "nat => nat set" |
54 below :: "nat => nat set" |
56 "below n == {i. i < n}"; |
55 "below n == {i. i < n}"; |
57 |
56 |
58 lemma below_less_iff [iff]: "(i: below k) = (i < k)"; |
57 lemma below_less_iff [iff]: "(i: below k) = (i < k)"; |
59 by (simp add: below_def); |
58 by (simp add: below_def); |
60 |
59 |
61 lemma below_0 [simp]: "below 0 = {}"; |
60 lemma below_0: "below 0 = {}"; |
62 by (simp add: below_def); |
61 by (simp add: below_def); |
63 |
62 |
64 lemma Sigma_Suc1: "below (Suc n) Times B = ({n} Times B) Un (below n Times B)"; |
63 lemma Sigma_Suc1: "below (Suc n) Times B = ({n} Times B) Un (below n Times B)"; |
65 by (simp add: below_def less_Suc_eq) blast; |
64 by (simp add: below_def less_Suc_eq) blast; |
66 |
65 |
71 |
70 |
72 |
71 |
73 section {* Basic properties of evnodd *}; |
72 section {* Basic properties of evnodd *}; |
74 |
73 |
75 constdefs |
74 constdefs |
76 evnodd :: "[(nat * nat) set, nat] => (nat * nat) set" |
75 evnodd :: "(nat * nat) set => nat => (nat * nat) set" |
77 "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"; |
76 "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"; |
78 |
77 |
79 lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"; |
78 lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"; |
80 by (simp add: evnodd_def); |
79 by (simp add: evnodd_def); |
81 |
80 |
82 lemma evnodd_subset: "evnodd A b <= A"; |
81 lemma evnodd_subset: "evnodd A b <= A"; |
83 proof (unfold evnodd_def); |
82 by (unfold evnodd_def, rule Int_lower1); |
84 show "!!B. A Int B <= A"; by (rule Int_lower1); |
|
85 qed; |
|
86 |
83 |
87 lemma evnoddD: "x : evnodd A b ==> x : A"; |
84 lemma evnoddD: "x : evnodd A b ==> x : A"; |
88 by (rule subsetD, rule evnodd_subset); |
85 by (rule subsetD, rule evnodd_subset); |
89 |
86 |
90 lemma evnodd_finite [simp]: "finite A ==> finite (evnodd A b)"; |
87 lemma evnodd_finite: "finite A ==> finite (evnodd A b)"; |
91 by (rule finite_subset, rule evnodd_subset); |
88 by (rule finite_subset, rule evnodd_subset); |
92 |
89 |
93 lemma evnodd_Un [simp]: "evnodd (A Un B) b = evnodd A b Un evnodd B b"; |
90 lemma evnodd_Un: "evnodd (A Un B) b = evnodd A b Un evnodd B b"; |
94 by (unfold evnodd_def) blast; |
91 by (unfold evnodd_def) blast; |
95 |
92 |
96 lemma evnodd_Diff [simp]: "evnodd (A - B) b = evnodd A b - evnodd B b"; |
93 lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b"; |
97 by (unfold evnodd_def) blast; |
94 by (unfold evnodd_def) blast; |
98 |
95 |
99 lemma evnodd_empty [simp]: "evnodd {} b = {}"; |
96 lemma evnodd_empty: "evnodd {} b = {}"; |
100 by (simp add: evnodd_def); |
97 by (simp add: evnodd_def); |
101 |
98 |
102 lemma evnodd_insert [simp]: "evnodd (insert (i, j) C) b = |
99 lemma evnodd_insert: "evnodd (insert (i, j) C) b = |
103 (if (i + j) mod 2 = b then insert (i, j) (evnodd C b) else evnodd C b)"; |
100 (if (i + j) mod 2 = b then insert (i, j) (evnodd C b) else evnodd C b)"; |
104 by (simp add: evnodd_def) blast; |
101 by (simp add: evnodd_def) blast; |
105 |
102 |
106 |
103 |
107 section {* Dominoes *}; |
104 section {* Dominoes *}; |
109 consts |
106 consts |
110 domino :: "(nat * nat) set set"; |
107 domino :: "(nat * nat) set set"; |
111 |
108 |
112 inductive domino |
109 inductive domino |
113 intrs |
110 intrs |
114 horiz: "{(i, j), (i, Suc j)} : domino" |
111 horiz: "{(i, j), (i, j + 1)} : domino" |
115 vertl: "{(i, j), (Suc i, j)} : domino"; |
112 vertl: "{(i, j), (i + 1, j)} : domino"; |
116 |
113 |
117 |
114 |
118 lemma dominoes_tile_row: "{i} Times below (n + n) : tiling domino" |
115 lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino" |
119 (is "??P n" is "??B n : ??T"); |
116 (is "??P n" is "??B n : ??T"); |
120 proof (induct n); |
117 proof (induct n); |
121 have "??B 0 = {}"; by simp; |
118 show "??P 0"; by (simp add: below_0 tiling.empty); |
122 also; have "... : ??T"; by (rule tiling.empty); |
|
123 finally; show "??P 0"; .; |
|
124 |
119 |
125 fix n; assume hyp: "??P n"; |
120 fix n; assume hyp: "??P n"; |
126 let ??a = "{i} Times {Suc (n + n)} Un {i} Times {n + n}"; |
121 let ??a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}"; |
127 |
122 |
128 have "??B (Suc n) = ??a Un ??B n"; by (simp add: Sigma_Suc Un_assoc); |
123 have "??B (Suc n) = ??a Un ??B n"; by (simp add: Sigma_Suc Un_assoc); |
129 also; have "... : ??T"; |
124 also; have "... : ??T"; |
130 proof (rule tiling.Un); |
125 proof (rule tiling.Un); |
131 have "{(i, n + n), (i, Suc (n + n))} : domino"; by (rule domino.horiz); |
126 have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz); |
132 also; have "{(i, n + n), (i, Suc (n + n))} = ??a"; by blast; |
127 also; have "{(i, 2 * n), (i, 2 * n + 1)} = ??a"; by blast; |
133 finally; show "??a : domino"; .; |
128 finally; show "... : domino"; .; |
134 show "??B n : ??T"; by (rule hyp); |
129 show "??B n : ??T"; by (rule hyp); |
135 show "??a <= - ??B n"; by force; |
130 show "??a <= - ??B n"; by force; |
136 qed; |
131 qed; |
137 finally; show "??P (Suc n)"; .; |
132 finally; show "??P (Suc n)"; .; |
138 qed; |
133 qed; |
139 |
134 |
140 lemma dominoes_tile_matrix: "below m Times below (n + n) : tiling domino" |
135 lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino" |
141 (is "??P m" is "??B m : ??T"); |
136 (is "??P m" is "??B m : ??T"); |
142 proof (induct m); |
137 proof (induct m); |
143 show "??P 0"; by (simp add: tiling.empty) -- {* same as above *}; |
138 show "??P 0"; by (simp add: below_0 tiling.empty); |
144 |
139 |
145 fix m; assume hyp: "??P m"; |
140 fix m; assume hyp: "??P m"; |
146 let ??t = "{m} Times below (n + n)"; |
141 let ??t = "{m} Times below (2 * n)"; |
147 |
142 |
148 have "??B (Suc m) = ??t Un ??B m"; by (simp add: Sigma_Suc); |
143 have "??B (Suc m) = ??t Un ??B m"; by (simp add: Sigma_Suc); |
149 also; have "... : ??T"; |
144 also; have "... : ??T"; |
150 proof (rule tiling_UnI); |
145 proof (rule tiling_Un [rulify]); |
151 show "??t : ??T"; by (rule dominoes_tile_row); |
146 show "??t : ??T"; by (rule dominoes_tile_row); |
152 show "??B m : ??T"; by (rule hyp); |
147 show "??B m : ??T"; by (rule hyp); |
153 show "??t Int ??B m = {}"; by blast; |
148 show "??t Int ??B m = {}"; by blast; |
154 qed; |
149 qed; |
155 finally; show "??P (Suc m)"; .; |
150 finally; show "??P (Suc m)"; .; |
160 proof -; |
155 proof -; |
161 assume "b < 2"; |
156 assume "b < 2"; |
162 assume "d : domino"; |
157 assume "d : domino"; |
163 thus ??thesis (is "??P d"); |
158 thus ??thesis (is "??P d"); |
164 proof (induct d set: domino); |
159 proof (induct d set: domino); |
|
160 have b_cases: "b = 0 | b = 1"; by arith; |
165 fix i j; |
161 fix i j; |
166 have b_cases: "b = 0 | b = 1"; by arith; |
162 note [simp] = evnodd_empty evnodd_insert mod_Suc; |
167 note [simp] = less_Suc_eq mod_Suc; |
163 from b_cases; show "??P {(i, j), (i, j + 1)}"; by rule auto; |
168 from b_cases; show "??P {(i, j), (i, Suc j)}"; by rule auto; |
164 from b_cases; show "??P {(i, j), (i + 1, j)}"; by rule auto; |
169 from b_cases; show "??P {(i, j), (Suc i, j)}"; by rule auto; |
|
170 qed; |
165 qed; |
171 qed; |
166 qed; |
172 |
167 |
173 lemma domino_finite: "d: domino ==> finite d"; |
168 lemma domino_finite: "d: domino ==> finite d"; |
174 proof (induct set: domino); |
169 proof (induct set: domino); |
175 fix i j; |
170 fix i j; |
176 show "finite {(i, j), (i, Suc j)}"; by (intro Finites.intrs); |
171 show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intrs); |
177 show "finite {(i, j), (Suc i, j)}"; by (intro Finites.intrs); |
172 show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intrs); |
178 qed; |
173 qed; |
179 |
174 |
180 |
175 |
181 section {* Tilings of dominoes *}; |
176 section {* Tilings of dominoes *}; |
182 |
177 |
183 lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ??T ==> ??F t"); |
178 lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ??T ==> ??F t"); |
184 proof -; |
179 proof -; |
185 assume "t : ??T"; |
180 assume "t : ??T"; |
186 thus "??F t"; |
181 thus "??F t"; |
187 proof (induct set: tiling); |
182 proof (induct t set: tiling); |
188 show "??F {}"; by (rule Finites.emptyI); |
183 show "??F {}"; by (rule Finites.emptyI); |
189 fix a t; assume "??F t"; |
184 fix a t; assume "??F t"; |
190 assume "a : domino"; hence "??F a"; by (rule domino_finite); |
185 assume "a : domino"; hence "??F a"; by (rule domino_finite); |
191 thus "??F (a Un t)"; by (rule finite_UnI); |
186 thus "??F (a Un t)"; by (rule finite_UnI); |
192 qed; |
187 qed; |
235 |
230 |
236 section {* Main theorem *}; |
231 section {* Main theorem *}; |
237 |
232 |
238 constdefs |
233 constdefs |
239 mutilated_board :: "nat => nat => (nat * nat) set" |
234 mutilated_board :: "nat => nat => (nat * nat) set" |
240 "mutilated_board m n == below (Suc m + Suc m) Times below (Suc n + Suc n) |
235 "mutilated_board m n == below (2 * (m + 1)) Times below (2 * (n + 1)) |
241 - {(0, 0)} - {(Suc (m + m), Suc (n + n))}"; |
236 - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"; |
242 |
237 |
243 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino" (is "_ ~: ??T"); |
238 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"; |
244 proof (unfold mutilated_board_def); |
239 proof (unfold mutilated_board_def); |
245 let ??t = "below (Suc m + Suc m) Times below (Suc n + Suc n)"; |
240 let ??T = "tiling domino"; |
|
241 let ??t = "below (2 * (m + 1)) Times below (2 * (n + 1))"; |
246 let ??t' = "??t - {(0, 0)}"; |
242 let ??t' = "??t - {(0, 0)}"; |
247 let ??t'' = "??t' - {(Suc (m + m), Suc (n + n))}"; |
243 let ??t'' = "??t' - {(2 * m + 1, 2 * n + 1)}"; |
248 show "??t'' ~: ??T"; |
244 show "??t'' ~: ??T"; |
249 proof; |
245 proof; |
|
246 have t: "??t : ??T"; by (rule dominoes_tile_matrix); |
|
247 assume t'': "??t'' : ??T"; |
|
248 |
250 let ??e = evnodd; |
249 let ??e = evnodd; |
251 note [simp] = evnodd_iff; |
|
252 assume t'': "??t'' : ??T"; |
|
253 |
|
254 have t: "??t : ??T"; by (rule dominoes_tile_matrix); |
|
255 have fin: "finite (??e ??t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t); |
250 have fin: "finite (??e ??t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t); |
256 |
251 |
|
252 note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff; |
257 have "card (??e ??t'' 0) < card (??e ??t' 0)"; |
253 have "card (??e ??t'' 0) < card (??e ??t' 0)"; |
258 proof -; |
254 proof -; |
259 have "card (??e ??t' 0 - {(Suc (m + m), Suc (n + n))}) < card (??e ??t' 0)"; |
255 have "card (??e ??t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (??e ??t' 0)"; |
260 proof (rule card_Diff1_less); |
256 proof (rule card_Diff1_less); |
261 show "finite (??e ??t' 0)"; by (rule finite_subset, rule fin) force; |
257 show "finite (??e ??t' 0)"; by (rule finite_subset, rule fin) force; |
262 show "(Suc (m + m), Suc (n + n)) : ??e ??t' 0"; by simp; |
258 show "(2 * m + 1, 2 * n + 1) : ??e ??t' 0"; by simp; |
263 qed; |
259 qed; |
264 thus ??thesis; by simp; |
260 thus ??thesis; by simp; |
265 qed; |
261 qed; |
266 also; have "... < card (??e ??t 0)"; |
262 also; have "... < card (??e ??t 0)"; |
267 proof -; |
263 proof -; |
269 with fin; have "card (??e ??t 0 - {(0, 0)}) < card (??e ??t 0)"; by (rule card_Diff1_less); |
265 with fin; have "card (??e ??t 0 - {(0, 0)}) < card (??e ??t 0)"; by (rule card_Diff1_less); |
270 thus ??thesis; by simp; |
266 thus ??thesis; by simp; |
271 qed; |
267 qed; |
272 also; from t; have "... = card (??e ??t 1)"; by (rule tiling_domino_01); |
268 also; from t; have "... = card (??e ??t 1)"; by (rule tiling_domino_01); |
273 also; have "??e ??t 1 = ??e ??t'' 1"; by simp; |
269 also; have "??e ??t 1 = ??e ??t'' 1"; by simp; |
274 also; have "card ... = card (??e ??t'' 0)"; by (rule sym, rule tiling_domino_01); |
270 also; from t''; have "card ... = card (??e ??t'' 0)"; by (rule tiling_domino_01 [RS sym]); |
275 finally; show False; ..; |
271 finally; show False; ..; |
276 qed; |
272 qed; |
277 qed; |
273 qed; |
278 |
274 |
279 |
275 |