author | blanchet |
Thu, 28 Aug 2014 07:30:16 +0200 | |
changeset 58066 | 96e987003a01 |
parent 55656 | eb07b0acbebc |
child 58614 | 7338eb25226c |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Mutilated_Checkerboard.thy |
7385 | 2 |
Author: Markus Wenzel, TU Muenchen (Isar document) |
31758 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
4 |
*) |
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
5 |
|
10007 | 6 |
header {* The Mutilated Checker Board Problem *} |
7761 | 7 |
|
31758 | 8 |
theory Mutilated_Checkerboard |
9 |
imports Main |
|
10 |
begin |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
11 |
|
37671 | 12 |
text {* The Mutilated Checker Board Problem, formalized inductively. |
40880 | 13 |
See \cite{paulson-mutilated-board} for the original tactic script version. *} |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
14 |
|
10007 | 15 |
subsection {* Tilings *} |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
16 |
|
55656 | 17 |
inductive_set tiling :: "'a set set \<Rightarrow> 'a set set" |
23746 | 18 |
for A :: "'a set set" |
37671 | 19 |
where |
55656 | 20 |
empty: "{} \<in> tiling A" |
21 |
| Un: "a \<in> A \<Longrightarrow> t \<in> tiling A \<Longrightarrow> a \<subseteq> - t \<Longrightarrow> a \<union> t \<in> tiling A" |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
22 |
|
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
23 |
|
10007 | 24 |
text "The union of two disjoint tilings is a tiling." |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
25 |
|
7761 | 26 |
lemma tiling_Un: |
55656 | 27 |
assumes "t \<in> tiling A" |
28 |
and "u \<in> tiling A" |
|
29 |
and "t \<inter> u = {}" |
|
30 |
shows "t \<union> u \<in> tiling A" |
|
10408 | 31 |
proof - |
32 |
let ?T = "tiling A" |
|
55656 | 33 |
from `t \<in> ?T` and `t \<inter> u = {}` |
34 |
show "t \<union> u \<in> ?T" |
|
10408 | 35 |
proof (induct t) |
11987 | 36 |
case empty |
55656 | 37 |
with `u \<in> ?T` show "{} \<union> u \<in> ?T" by simp |
9475 | 38 |
next |
11987 | 39 |
case (Un a t) |
55656 | 40 |
show "(a \<union> t) \<union> u \<in> ?T" |
10408 | 41 |
proof - |
55656 | 42 |
have "a \<union> (t \<union> u) \<in> ?T" |
43 |
using `a \<in> A` |
|
10408 | 44 |
proof (rule tiling.Un) |
55656 | 45 |
from `(a \<union> t) \<inter> u = {}` have "t \<inter> u = {}" by blast |
46 |
then show "t \<union> u \<in> ?T" by (rule Un) |
|
47 |
from `a \<subseteq> - t` and `(a \<union> t) \<inter> u = {}` |
|
48 |
show "a \<subseteq> - (t \<union> u)" by blast |
|
10408 | 49 |
qed |
55656 | 50 |
also have "a \<union> (t \<union> u) = (a \<union> t) \<union> u" |
10408 | 51 |
by (simp only: Un_assoc) |
52 |
finally show ?thesis . |
|
53 |
qed |
|
10007 | 54 |
qed |
55 |
qed |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
56 |
|
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
57 |
|
10007 | 58 |
subsection {* Basic properties of ``below'' *} |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
59 |
|
55656 | 60 |
definition below :: "nat \<Rightarrow> nat set" |
37671 | 61 |
where "below n = {i. i < n}" |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
62 |
|
55656 | 63 |
lemma below_less_iff [iff]: "i \<in> below k \<longleftrightarrow> i < k" |
10007 | 64 |
by (simp add: below_def) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
65 |
|
10007 | 66 |
lemma below_0: "below 0 = {}" |
67 |
by (simp add: below_def) |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
68 |
|
55656 | 69 |
lemma Sigma_Suc1: "m = n + 1 \<Longrightarrow> below m \<times> B = ({n} \<times> B) \<union> (below n \<times> B)" |
10007 | 70 |
by (simp add: below_def less_Suc_eq) blast |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
71 |
|
7761 | 72 |
lemma Sigma_Suc2: |
55656 | 73 |
"m = n + 2 \<Longrightarrow> |
74 |
A \<times> below m = (A \<times> {n}) \<union> (A \<times> {n + 1}) \<union> (A \<times> below n)" |
|
13187 | 75 |
by (auto simp add: below_def) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
76 |
|
10007 | 77 |
lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2 |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
78 |
|
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
79 |
|
10007 | 80 |
subsection {* Basic properties of ``evnodd'' *} |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
81 |
|
55656 | 82 |
definition evnodd :: "(nat \<times> nat) set \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set" |
83 |
where "evnodd A b = A \<inter> {(i, j). (i + j) mod 2 = b}" |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
84 |
|
55656 | 85 |
lemma evnodd_iff: "(i, j) \<in> evnodd A b \<longleftrightarrow> (i, j) \<in> A \<and> (i + j) mod 2 = b" |
10007 | 86 |
by (simp add: evnodd_def) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
87 |
|
55656 | 88 |
lemma evnodd_subset: "evnodd A b \<subseteq> A" |
37671 | 89 |
unfolding evnodd_def by (rule Int_lower1) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
90 |
|
55656 | 91 |
lemma evnoddD: "x \<in> evnodd A b \<Longrightarrow> x \<in> A" |
37671 | 92 |
by (rule subsetD) (rule evnodd_subset) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
93 |
|
55656 | 94 |
lemma evnodd_finite: "finite A \<Longrightarrow> finite (evnodd A b)" |
37671 | 95 |
by (rule finite_subset) (rule evnodd_subset) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
96 |
|
55656 | 97 |
lemma evnodd_Un: "evnodd (A \<union> B) b = evnodd A b \<union> evnodd B b" |
37671 | 98 |
unfolding evnodd_def by blast |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
99 |
|
10007 | 100 |
lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b" |
37671 | 101 |
unfolding evnodd_def by blast |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
102 |
|
10007 | 103 |
lemma evnodd_empty: "evnodd {} b = {}" |
104 |
by (simp add: evnodd_def) |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
105 |
|
7385 | 106 |
lemma evnodd_insert: "evnodd (insert (i, j) C) b = |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
107 |
(if (i + j) mod 2 = b |
10007 | 108 |
then insert (i, j) (evnodd C b) else evnodd C b)" |
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
31758
diff
changeset
|
109 |
by (simp add: evnodd_def) |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
110 |
|
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
111 |
|
10007 | 112 |
subsection {* Dominoes *} |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
113 |
|
55656 | 114 |
inductive_set domino :: "(nat \<times> nat) set set" |
37671 | 115 |
where |
55656 | 116 |
horiz: "{(i, j), (i, j + 1)} \<in> domino" |
117 |
| vertl: "{(i, j), (i + 1, j)} \<in> domino" |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
118 |
|
7800 | 119 |
lemma dominoes_tile_row: |
55656 | 120 |
"{i} \<times> below (2 * n) \<in> tiling domino" |
121 |
(is "?B n \<in> ?T") |
|
10007 | 122 |
proof (induct n) |
11987 | 123 |
case 0 |
124 |
show ?case by (simp add: below_0 tiling.empty) |
|
125 |
next |
|
126 |
case (Suc n) |
|
55656 | 127 |
let ?a = "{i} \<times> {2 * n + 1} \<union> {i} \<times> {2 * n}" |
128 |
have "?B (Suc n) = ?a \<union> ?B n" |
|
10007 | 129 |
by (auto simp add: Sigma_Suc Un_assoc) |
55656 | 130 |
also have "\<dots> \<in> ?T" |
10007 | 131 |
proof (rule tiling.Un) |
55656 | 132 |
have "{(i, 2 * n), (i, 2 * n + 1)} \<in> domino" |
10007 | 133 |
by (rule domino.horiz) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
134 |
also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast |
55656 | 135 |
finally show "\<dots> \<in> domino" . |
136 |
show "?B n \<in> ?T" by (rule Suc) |
|
137 |
show "?a \<subseteq> - ?B n" by blast |
|
10007 | 138 |
qed |
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset
|
139 |
finally show ?case . |
10007 | 140 |
qed |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
141 |
|
7761 | 142 |
lemma dominoes_tile_matrix: |
55656 | 143 |
"below m \<times> below (2 * n) \<in> tiling domino" |
144 |
(is "?B m \<in> ?T") |
|
10007 | 145 |
proof (induct m) |
11987 | 146 |
case 0 |
147 |
show ?case by (simp add: below_0 tiling.empty) |
|
148 |
next |
|
149 |
case (Suc m) |
|
55656 | 150 |
let ?t = "{m} \<times> below (2 * n)" |
151 |
have "?B (Suc m) = ?t \<union> ?B m" by (simp add: Sigma_Suc) |
|
152 |
also have "\<dots> \<in> ?T" |
|
10408 | 153 |
proof (rule tiling_Un) |
55656 | 154 |
show "?t \<in> ?T" by (rule dominoes_tile_row) |
155 |
show "?B m \<in> ?T" by (rule Suc) |
|
156 |
show "?t \<inter> ?B m = {}" by blast |
|
10007 | 157 |
qed |
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset
|
158 |
finally show ?case . |
10007 | 159 |
qed |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
160 |
|
7761 | 161 |
lemma domino_singleton: |
55656 | 162 |
assumes "d \<in> domino" |
37671 | 163 |
and "b < 2" |
55656 | 164 |
shows "\<exists>i j. evnodd d b = {(i, j)}" (is "?P d") |
37671 | 165 |
using assms |
18241 | 166 |
proof induct |
55656 | 167 |
from `b < 2` have b_cases: "b = 0 \<or> b = 1" by arith |
18241 | 168 |
fix i j |
169 |
note [simp] = evnodd_empty evnodd_insert mod_Suc |
|
170 |
from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto |
|
171 |
from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto |
|
10007 | 172 |
qed |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
173 |
|
18153 | 174 |
lemma domino_finite: |
55656 | 175 |
assumes "d \<in> domino" |
18153 | 176 |
shows "finite d" |
37671 | 177 |
using assms |
18192 | 178 |
proof induct |
179 |
fix i j :: nat |
|
22273 | 180 |
show "finite {(i, j), (i, j + 1)}" by (intro finite.intros) |
181 |
show "finite {(i, j), (i + 1, j)}" by (intro finite.intros) |
|
10007 | 182 |
qed |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
183 |
|
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
184 |
|
10007 | 185 |
subsection {* Tilings of dominoes *} |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
186 |
|
7761 | 187 |
lemma tiling_domino_finite: |
55656 | 188 |
assumes t: "t \<in> tiling domino" (is "t \<in> ?T") |
18153 | 189 |
shows "finite t" (is "?F t") |
18241 | 190 |
using t |
18153 | 191 |
proof induct |
22273 | 192 |
show "?F {}" by (rule finite.emptyI) |
18153 | 193 |
fix a t assume "?F t" |
55656 | 194 |
assume "a \<in> domino" |
195 |
then have "?F a" by (rule domino_finite) |
|
196 |
from this and `?F t` show "?F (a \<union> t)" by (rule finite_UnI) |
|
10007 | 197 |
qed |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
198 |
|
7761 | 199 |
lemma tiling_domino_01: |
55656 | 200 |
assumes t: "t \<in> tiling domino" (is "t \<in> ?T") |
18153 | 201 |
shows "card (evnodd t 0) = card (evnodd t 1)" |
18241 | 202 |
using t |
18153 | 203 |
proof induct |
204 |
case empty |
|
205 |
show ?case by (simp add: evnodd_def) |
|
206 |
next |
|
207 |
case (Un a t) |
|
208 |
let ?e = evnodd |
|
209 |
note hyp = `card (?e t 0) = card (?e t 1)` |
|
55656 | 210 |
and at = `a \<subseteq> - t` |
18153 | 211 |
have card_suc: |
55656 | 212 |
"\<And>b. b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))" |
18153 | 213 |
proof - |
55656 | 214 |
fix b :: nat |
215 |
assume "b < 2" |
|
216 |
have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un) |
|
18153 | 217 |
also obtain i j where e: "?e a b = {(i, j)}" |
10007 | 218 |
proof - |
23373 | 219 |
from `a \<in> domino` and `b < 2` |
55656 | 220 |
have "\<exists>i j. ?e a b = {(i, j)}" by (rule domino_singleton) |
18153 | 221 |
then show ?thesis by (blast intro: that) |
10007 | 222 |
qed |
55656 | 223 |
also have "\<dots> \<union> ?e t b = insert (i, j) (?e t b)" by simp |
224 |
also have "card \<dots> = Suc (card (?e t b))" |
|
18153 | 225 |
proof (rule card_insert_disjoint) |
23373 | 226 |
from `t \<in> tiling domino` have "finite t" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
227 |
by (rule tiling_domino_finite) |
23373 | 228 |
then show "finite (?e t b)" |
229 |
by (rule evnodd_finite) |
|
55656 | 230 |
from e have "(i, j) \<in> ?e a b" by simp |
231 |
with at show "(i, j) \<notin> ?e t b" by (blast dest: evnoddD) |
|
18153 | 232 |
qed |
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset
|
233 |
finally show "?thesis b" . |
10007 | 234 |
qed |
55656 | 235 |
then have "card (?e (a \<union> t) 0) = Suc (card (?e t 0))" by simp |
18153 | 236 |
also from hyp have "card (?e t 0) = card (?e t 1)" . |
55656 | 237 |
also from card_suc have "Suc \<dots> = card (?e (a \<union> t) 1)" |
18153 | 238 |
by simp |
239 |
finally show ?case . |
|
10007 | 240 |
qed |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
241 |
|
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
242 |
|
10007 | 243 |
subsection {* Main theorem *} |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
244 |
|
55656 | 245 |
definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set" |
46582 | 246 |
where |
247 |
"mutilated_board m n = |
|
55656 | 248 |
below (2 * (m + 1)) \<times> below (2 * (n + 1)) |
46582 | 249 |
- {(0, 0)} - {(2 * m + 1, 2 * n + 1)}" |
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
250 |
|
55656 | 251 |
theorem mutil_not_tiling: "mutilated_board m n \<notin> tiling domino" |
10007 | 252 |
proof (unfold mutilated_board_def) |
253 |
let ?T = "tiling domino" |
|
55656 | 254 |
let ?t = "below (2 * (m + 1)) \<times> below (2 * (n + 1))" |
10007 | 255 |
let ?t' = "?t - {(0, 0)}" |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
256 |
let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}" |
46582 | 257 |
|
55656 | 258 |
show "?t'' \<notin> ?T" |
10007 | 259 |
proof |
55656 | 260 |
have t: "?t \<in> ?T" by (rule dominoes_tile_matrix) |
261 |
assume t'': "?t'' \<in> ?T" |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
262 |
|
10007 | 263 |
let ?e = evnodd |
264 |
have fin: "finite (?e ?t 0)" |
|
265 |
by (rule evnodd_finite, rule tiling_domino_finite, rule t) |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
266 |
|
10007 | 267 |
note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff |
268 |
have "card (?e ?t'' 0) < card (?e ?t' 0)" |
|
269 |
proof - |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
270 |
have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) |
10007 | 271 |
< card (?e ?t' 0)" |
272 |
proof (rule card_Diff1_less) |
|
10408 | 273 |
from _ fin show "finite (?e ?t' 0)" |
10007 | 274 |
by (rule finite_subset) auto |
55656 | 275 |
show "(2 * m + 1, 2 * n + 1) \<in> ?e ?t' 0" by simp |
10007 | 276 |
qed |
18153 | 277 |
then show ?thesis by simp |
10007 | 278 |
qed |
55656 | 279 |
also have "\<dots> < card (?e ?t 0)" |
10007 | 280 |
proof - |
55656 | 281 |
have "(0, 0) \<in> ?e ?t 0" by simp |
10007 | 282 |
with fin have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)" |
283 |
by (rule card_Diff1_less) |
|
18153 | 284 |
then show ?thesis by simp |
10007 | 285 |
qed |
55656 | 286 |
also from t have "\<dots> = card (?e ?t 1)" |
10007 | 287 |
by (rule tiling_domino_01) |
288 |
also have "?e ?t 1 = ?e ?t'' 1" by simp |
|
55656 | 289 |
also from t'' have "card \<dots> = card (?e ?t'' 0)" |
10007 | 290 |
by (rule tiling_domino_01 [symmetric]) |
55656 | 291 |
finally have "\<dots> < \<dots>" . then show False .. |
10007 | 292 |
qed |
293 |
qed |
|
7382
33c01075d343
The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset
|
294 |
|
10007 | 295 |
end |