39 proof (intro impI); |
42 proof (intro impI); |
40 assume "u : ?T" "(a Un t) Int u = {}"; |
43 assume "u : ?T" "(a Un t) Int u = {}"; |
41 have hyp: "t Un u: ?T"; by (blast!); |
44 have hyp: "t Un u: ?T"; by (blast!); |
42 have "a <= - (t Un u)"; by (blast!); |
45 have "a <= - (t Un u)"; by (blast!); |
43 with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un); |
46 with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un); |
44 also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc); |
47 also; have "a Un (t Un u) = (a Un t) Un u"; |
|
48 by (simp only: Un_assoc); |
45 finally; show "... : ?T"; .; |
49 finally; show "... : ?T"; .; |
46 qed; |
50 qed; |
47 qed; |
51 qed; |
48 qed; |
52 qed; |
49 |
53 |
50 |
54 |
51 section {* Basic properties of below *}; |
55 subsection {* Basic properties of below *}; |
52 |
56 |
53 constdefs |
57 constdefs |
54 below :: "nat => nat set" |
58 below :: "nat => nat set" |
55 "below n == {i. i < n}"; |
59 "below n == {i. i < n}"; |
56 |
60 |
58 by (simp add: below_def); |
62 by (simp add: below_def); |
59 |
63 |
60 lemma below_0: "below 0 = {}"; |
64 lemma below_0: "below 0 = {}"; |
61 by (simp add: below_def); |
65 by (simp add: below_def); |
62 |
66 |
63 lemma Sigma_Suc1: "below (Suc n) Times B = ({n} Times B) Un (below n Times B)"; |
67 lemma Sigma_Suc1: |
|
68 "below (Suc n) Times B = ({n} Times B) Un (below n Times B)"; |
64 by (simp add: below_def less_Suc_eq) blast; |
69 by (simp add: below_def less_Suc_eq) blast; |
65 |
70 |
66 lemma Sigma_Suc2: "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))"; |
71 lemma Sigma_Suc2: |
|
72 "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))"; |
67 by (simp add: below_def less_Suc_eq) blast; |
73 by (simp add: below_def less_Suc_eq) blast; |
68 |
74 |
69 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2; |
75 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2; |
70 |
76 |
71 |
77 |
72 section {* Basic properties of evnodd *}; |
78 subsection {* Basic properties of evnodd *}; |
73 |
79 |
74 constdefs |
80 constdefs |
75 evnodd :: "(nat * nat) set => nat => (nat * nat) set" |
81 evnodd :: "(nat * nat) set => nat => (nat * nat) set" |
76 "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"; |
82 "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"; |
77 |
83 |
78 lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"; |
84 lemma evnodd_iff: |
|
85 "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"; |
79 by (simp add: evnodd_def); |
86 by (simp add: evnodd_def); |
80 |
87 |
81 lemma evnodd_subset: "evnodd A b <= A"; |
88 lemma evnodd_subset: "evnodd A b <= A"; |
82 by (unfold evnodd_def, rule Int_lower1); |
89 by (unfold evnodd_def, rule Int_lower1); |
83 |
90 |
95 |
102 |
96 lemma evnodd_empty: "evnodd {} b = {}"; |
103 lemma evnodd_empty: "evnodd {} b = {}"; |
97 by (simp add: evnodd_def); |
104 by (simp add: evnodd_def); |
98 |
105 |
99 lemma evnodd_insert: "evnodd (insert (i, j) C) b = |
106 lemma evnodd_insert: "evnodd (insert (i, j) C) b = |
100 (if (i + j) mod 2 = b then insert (i, j) (evnodd C b) else evnodd C b)"; |
107 (if (i + j) mod 2 = b |
|
108 then insert (i, j) (evnodd C b) else evnodd C b)"; |
101 by (simp add: evnodd_def) blast; |
109 by (simp add: evnodd_def) blast; |
102 |
110 |
103 |
111 |
104 section {* Dominoes *}; |
112 subsection {* Dominoes *}; |
105 |
113 |
106 consts |
114 consts |
107 domino :: "(nat * nat) set set"; |
115 domino :: "(nat * nat) set set"; |
108 |
116 |
109 inductive domino |
117 inductive domino |
110 intrs |
118 intrs |
111 horiz: "{(i, j), (i, j + 1)} : domino" |
119 horiz: "{(i, j), (i, j + 1)} : domino" |
112 vertl: "{(i, j), (i + 1, j)} : domino"; |
120 vertl: "{(i, j), (i + 1, j)} : domino"; |
113 |
121 |
114 |
|
115 lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino" |
122 lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino" |
116 (is "?P n" is "?B n : ?T"); |
123 (is "?P n" is "?B n : ?T"); |
117 proof (induct n); |
124 proof (induct n); |
118 show "?P 0"; by (simp add: below_0 tiling.empty); |
125 show "?P 0"; by (simp add: below_0 tiling.empty); |
119 |
126 |
121 let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}"; |
128 let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}"; |
122 |
129 |
123 have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc); |
130 have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc); |
124 also; have "... : ?T"; |
131 also; have "... : ?T"; |
125 proof (rule tiling.Un); |
132 proof (rule tiling.Un); |
126 have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz); |
133 have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; |
|
134 by (rule domino.horiz); |
127 also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast; |
135 also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast; |
128 finally; show "... : domino"; .; |
136 finally; show "... : domino"; .; |
129 from hyp; show "?B n : ?T"; .; |
137 from hyp; show "?B n : ?T"; .; |
130 show "?a <= - ?B n"; by force; |
138 show "?a <= - ?B n"; by force; |
131 qed; |
139 qed; |
132 finally; show "?P (Suc n)"; .; |
140 finally; show "?P (Suc n)"; .; |
133 qed; |
141 qed; |
134 |
142 |
135 lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino" |
143 lemma dominoes_tile_matrix: |
|
144 "below m Times below (2 * n) : tiling domino" |
136 (is "?P m" is "?B m : ?T"); |
145 (is "?P m" is "?B m : ?T"); |
137 proof (induct m); |
146 proof (induct m); |
138 show "?P 0"; by (simp add: below_0 tiling.empty); |
147 show "?P 0"; by (simp add: below_0 tiling.empty); |
139 |
148 |
140 fix m; assume hyp: "?P m"; |
149 fix m; assume hyp: "?P m"; |
171 show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intrs); |
180 show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intrs); |
172 show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intrs); |
181 show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intrs); |
173 qed; |
182 qed; |
174 |
183 |
175 |
184 |
176 section {* Tilings of dominoes *}; |
185 subsection {* Tilings of dominoes *}; |
177 |
186 |
178 lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t"); |
187 lemma tiling_domino_finite: |
|
188 "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t"); |
179 proof -; |
189 proof -; |
180 assume "t : ?T"; |
190 assume "t : ?T"; |
181 thus "?F t"; |
191 thus "?F t"; |
182 proof (induct t set: tiling); |
192 proof (induct t set: tiling); |
183 show "?F {}"; by (rule Finites.emptyI); |
193 show "?F {}"; by (rule Finites.emptyI); |
199 let ?e = evnodd; |
210 let ?e = evnodd; |
200 assume "a : domino" "t : ?T" |
211 assume "a : domino" "t : ?T" |
201 and hyp: "card (?e t 0) = card (?e t 1)" |
212 and hyp: "card (?e t 0) = card (?e t 1)" |
202 and "a <= - t"; |
213 and "a <= - t"; |
203 |
214 |
204 have card_suc: "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"; |
215 have card_suc: |
|
216 "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"; |
205 proof -; |
217 proof -; |
206 fix b; assume "b < 2"; |
218 fix b; assume "b < 2"; |
207 have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton); |
219 have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton); |
208 thus "?thesis b"; |
220 thus "?thesis b"; |
209 proof (elim exE); |
221 proof (elim exE); |
210 have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un); |
222 have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un); |
211 also; fix i j; assume e: "?e a b = {(i, j)}"; |
223 also; fix i j; assume e: "?e a b = {(i, j)}"; |
212 also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp; |
224 also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp; |
213 also; have "card ... = Suc (card (?e t b))"; |
225 also; have "card ... = Suc (card (?e t b))"; |
214 proof (rule card_insert_disjoint); |
226 proof (rule card_insert_disjoint); |
215 show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite); |
227 show "finite (?e t b)"; |
|
228 by (rule evnodd_finite, rule tiling_domino_finite); |
216 have "(i, j) : ?e a b"; by (simp!); |
229 have "(i, j) : ?e a b"; by (simp!); |
217 thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD); |
230 thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD); |
218 qed; |
231 qed; |
219 finally; show ?thesis; .; |
232 finally; show ?thesis; .; |
220 qed; |
233 qed; |
221 qed; |
234 qed; |
222 hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp; |
235 hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp; |
223 also; from hyp; have "card (?e t 0) = card (?e t 1)"; .; |
236 also; from hyp; have "card (?e t 0) = card (?e t 1)"; .; |
224 also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; by simp; |
237 also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; |
|
238 by simp; |
225 finally; show "?P (a Un t)"; .; |
239 finally; show "?P (a Un t)"; .; |
226 qed; |
240 qed; |
227 qed; |
241 qed; |
228 |
242 |
229 |
243 |
230 section {* Main theorem *}; |
244 subsection {* Main theorem *}; |
231 |
245 |
232 constdefs |
246 constdefs |
233 mutilated_board :: "nat => nat => (nat * nat) set" |
247 mutilated_board :: "nat => nat => (nat * nat) set" |
234 "mutilated_board m n == below (2 * (m + 1)) Times below (2 * (n + 1)) |
248 "mutilated_board m n == |
235 - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"; |
249 below (2 * (m + 1)) Times below (2 * (n + 1)) |
|
250 - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"; |
236 |
251 |
237 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"; |
252 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"; |
238 proof (unfold mutilated_board_def); |
253 proof (unfold mutilated_board_def); |
239 let ?T = "tiling domino"; |
254 let ?T = "tiling domino"; |
240 let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))"; |
255 let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))"; |
241 let ?t' = "?t - {(0, 0)}"; |
256 let ?t' = "?t - {(0, 0)}"; |
242 let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"; |
257 let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"; |
|
258 |
243 show "?t'' ~: ?T"; |
259 show "?t'' ~: ?T"; |
244 proof; |
260 proof; |
245 have t: "?t : ?T"; by (rule dominoes_tile_matrix); |
261 have t: "?t : ?T"; by (rule dominoes_tile_matrix); |
246 assume t'': "?t'' : ?T"; |
262 assume t'': "?t'' : ?T"; |
247 |
263 |
248 let ?e = evnodd; |
264 let ?e = evnodd; |
249 have fin: "finite (?e ?t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t); |
265 have fin: "finite (?e ?t 0)"; |
|
266 by (rule evnodd_finite, rule tiling_domino_finite, rule t); |
250 |
267 |
251 note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff; |
268 note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff; |
252 have "card (?e ?t'' 0) < card (?e ?t' 0)"; |
269 have "card (?e ?t'' 0) < card (?e ?t' 0)"; |
253 proof -; |
270 proof -; |
254 have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)"; |
271 have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)"; |
259 thus ?thesis; by simp; |
276 thus ?thesis; by simp; |
260 qed; |
277 qed; |
261 also; have "... < card (?e ?t 0)"; |
278 also; have "... < card (?e ?t 0)"; |
262 proof -; |
279 proof -; |
263 have "(0, 0) : ?e ?t 0"; by simp; |
280 have "(0, 0) : ?e ?t 0"; by simp; |
264 with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; by (rule card_Diff1_less); |
281 with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; |
|
282 by (rule card_Diff1_less); |
265 thus ?thesis; by simp; |
283 thus ?thesis; by simp; |
266 qed; |
284 qed; |
267 also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01); |
285 also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01); |
268 also; have "?e ?t 1 = ?e ?t'' 1"; by simp; |
286 also; have "?e ?t 1 = ?e ?t'' 1"; by simp; |
269 also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]); |
287 also; from t''; have "card ... = card (?e ?t'' 0)"; |
|
288 by (rule tiling_domino_01 [RS sym]); |
270 finally; show False; ..; |
289 finally; show False; ..; |
271 qed; |
290 qed; |
272 qed; |
291 qed; |
273 |
292 |
274 |
|
275 end; |
293 end; |