author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46582  dcc312f22ee8 
child 55656  eb07b0acbebc 
permissions  rwrr 
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{paulsonmutilatedboard} 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 

37671  17 
inductive_set tiling :: "'a set set => 'a set set" 
23746  18 
for A :: "'a set set" 
37671  19 
where 
20 
empty: "{} : tiling A" 

21 
 Un: "a : A ==> t : tiling A ==> a <=  t ==> a Un t : 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: 
37671  27 
assumes "t : tiling A" 
28 
and "u : tiling A" 

29 
and "t Int u = {}" 

18153  30 
shows "t Un u : tiling A" 
10408  31 
proof  
32 
let ?T = "tiling A" 

18153  33 
from `t : ?T` and `t Int u = {}` 
34 
show "t Un u : ?T" 

10408  35 
proof (induct t) 
11987  36 
case empty 
18153  37 
with `u : ?T` show "{} Un u : ?T" by simp 
9475  38 
next 
11987  39 
case (Un a t) 
10408  40 
show "(a Un t) Un u : ?T" 
41 
proof  

42 
have "a Un (t Un u) : ?T" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

43 
using `a : A` 
10408  44 
proof (rule tiling.Un) 
18153  45 
from `(a Un t) Int u = {}` have "t Int u = {}" by blast 
46 
then show "t Un u: ?T" by (rule Un) 

23373  47 
from `a <=  t` and `(a Un t) Int u = {}` 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

48 
show "a <=  (t Un u)" by blast 
10408  49 
qed 
50 
also have "a Un (t Un u) = (a Un t) Un u" 

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 

37671  60 
definition below :: "nat => nat set" 
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 

10007  63 
lemma below_less_iff [iff]: "(i: below k) = (i < k)" 
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 

7761  69 
lemma Sigma_Suc1: 
10007  70 
"m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)" 
71 
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

72 

7761  73 
lemma Sigma_Suc2: 
37671  74 
"m = n + 2 ==> A <*> below m = 
75 
(A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)" 

13187  76 
by (auto simp add: below_def) 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

77 

10007  78 
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

79 

33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

80 

10007  81 
subsection {* Basic properties of ``evnodd'' *} 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

82 

37671  83 
definition evnodd :: "(nat * nat) set => nat => (nat * nat) set" 
84 
where "evnodd A b = A Int {(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

85 

37671  86 
lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)" 
10007  87 
by (simp add: evnodd_def) 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

88 

10007  89 
lemma evnodd_subset: "evnodd A b <= A" 
37671  90 
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

91 

10007  92 
lemma evnoddD: "x : evnodd A b ==> x : A" 
37671  93 
by (rule subsetD) (rule evnodd_subset) 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

94 

10007  95 
lemma evnodd_finite: "finite A ==> finite (evnodd A b)" 
37671  96 
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

97 

10007  98 
lemma evnodd_Un: "evnodd (A Un B) b = evnodd A b Un evnodd B b" 
37671  99 
unfolding evnodd_def by blast 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

100 

10007  101 
lemma evnodd_Diff: "evnodd (A  B) b = evnodd A b  evnodd B b" 
37671  102 
unfolding evnodd_def by blast 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

103 

10007  104 
lemma evnodd_empty: "evnodd {} b = {}" 
105 
by (simp add: evnodd_def) 

7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

106 

7385  107 
lemma evnodd_insert: "evnodd (insert (i, j) C) b = 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

108 
(if (i + j) mod 2 = b 
10007  109 
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

110 
by (simp add: evnodd_def) 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

111 

33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

112 

10007  113 
subsection {* Dominoes *} 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

114 

37671  115 
inductive_set domino :: "(nat * nat) set set" 
116 
where 

117 
horiz: "{(i, j), (i, j + 1)} : domino" 

118 
 vertl: "{(i, j), (i + 1, j)} : domino" 

7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

119 

7800  120 
lemma dominoes_tile_row: 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

121 
"{i} <*> below (2 * n) : tiling domino" 
11987  122 
(is "?B n : ?T") 
10007  123 
proof (induct n) 
11987  124 
case 0 
125 
show ?case by (simp add: below_0 tiling.empty) 

126 
next 

127 
case (Suc n) 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

128 
let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}" 
10007  129 
have "?B (Suc n) = ?a Un ?B n" 
130 
by (auto simp add: Sigma_Suc Un_assoc) 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset

131 
also have "... : ?T" 
10007  132 
proof (rule tiling.Un) 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

133 
have "{(i, 2 * n), (i, 2 * n + 1)} : domino" 
10007  134 
by (rule domino.horiz) 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

135 
also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast 
10007  136 
finally show "... : domino" . 
11987  137 
show "?B n : ?T" by (rule Suc) 
10007  138 
show "?a <=  ?B n" by blast 
139 
qed 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset

140 
finally show ?case . 
10007  141 
qed 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

142 

7761  143 
lemma dominoes_tile_matrix: 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

144 
"below m <*> below (2 * n) : tiling domino" 
11987  145 
(is "?B m : ?T") 
10007  146 
proof (induct m) 
11987  147 
case 0 
148 
show ?case by (simp add: below_0 tiling.empty) 

149 
next 

150 
case (Suc m) 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

151 
let ?t = "{m} <*> below (2 * n)" 
10007  152 
have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc) 
46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset

153 
also have "... : ?T" 
10408  154 
proof (rule tiling_Un) 
10007  155 
show "?t : ?T" by (rule dominoes_tile_row) 
11987  156 
show "?B m : ?T" by (rule Suc) 
10007  157 
show "?t Int ?B m = {}" by blast 
158 
qed 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset

159 
finally show ?case . 
10007  160 
qed 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

161 

7761  162 
lemma domino_singleton: 
37671  163 
assumes "d : domino" 
164 
and "b < 2" 

18241  165 
shows "EX i j. evnodd d b = {(i, j)}" (is "?P d") 
37671  166 
using assms 
18241  167 
proof induct 
168 
from `b < 2` have b_cases: "b = 0  b = 1" by arith 

169 
fix i j 

170 
note [simp] = evnodd_empty evnodd_insert mod_Suc 

171 
from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto 

172 
from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto 

10007  173 
qed 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

174 

18153  175 
lemma domino_finite: 
37671  176 
assumes "d: domino" 
18153  177 
shows "finite d" 
37671  178 
using assms 
18192  179 
proof induct 
180 
fix i j :: nat 

22273  181 
show "finite {(i, j), (i, j + 1)}" by (intro finite.intros) 
182 
show "finite {(i, j), (i + 1, j)}" by (intro finite.intros) 

10007  183 
qed 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

184 

33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

185 

10007  186 
subsection {* Tilings of dominoes *} 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

187 

7761  188 
lemma tiling_domino_finite: 
18241  189 
assumes t: "t : tiling domino" (is "t : ?T") 
18153  190 
shows "finite t" (is "?F t") 
18241  191 
using t 
18153  192 
proof induct 
22273  193 
show "?F {}" by (rule finite.emptyI) 
18153  194 
fix a t assume "?F t" 
195 
assume "a : domino" then have "?F a" by (rule domino_finite) 

23373  196 
from this and `?F t` show "?F (a Un 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: 
18241  200 
assumes t: "t : tiling domino" (is "t : ?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)` 

210 
and at = `a <=  t` 

211 
have card_suc: 

212 
"!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))" 

213 
proof  

214 
fix b :: nat assume "b < 2" 

215 
have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un) 

216 
also obtain i j where e: "?e a b = {(i, j)}" 

10007  217 
proof  
23373  218 
from `a \<in> domino` and `b < 2` 
18153  219 
have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton) 
220 
then show ?thesis by (blast intro: that) 

10007  221 
qed 
46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset

222 
also have "... Un ?e t b = insert (i, j) (?e t b)" by simp 
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset

223 
also have "card ... = Suc (card (?e t b))" 
18153  224 
proof (rule card_insert_disjoint) 
23373  225 
from `t \<in> tiling domino` have "finite t" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

226 
by (rule tiling_domino_finite) 
23373  227 
then show "finite (?e t b)" 
228 
by (rule evnodd_finite) 

18153  229 
from e have "(i, j) : ?e a b" by simp 
230 
with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD) 

231 
qed 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
40880
diff
changeset

232 
finally show "?thesis b" . 
10007  233 
qed 
18153  234 
then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp 
235 
also from hyp have "card (?e t 0) = card (?e t 1)" . 

236 
also from card_suc have "Suc ... = card (?e (a Un t) 1)" 

237 
by simp 

238 
finally show ?case . 

10007  239 
qed 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

240 

33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

241 

10007  242 
subsection {* Main theorem *} 
7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

243 

37671  244 
definition mutilated_board :: "nat => nat => (nat * nat) set" 
46582  245 
where 
246 
"mutilated_board m n = 

247 
below (2 * (m + 1)) <*> below (2 * (n + 1)) 

248 
 {(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

249 

10007  250 
theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino" 
251 
proof (unfold mutilated_board_def) 

252 
let ?T = "tiling domino" 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

253 
let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))" 
10007  254 
let ?t' = "?t  {(0, 0)}" 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

255 
let ?t'' = "?t'  {(2 * m + 1, 2 * n + 1)}" 
46582  256 

10007  257 
show "?t'' ~: ?T" 
258 
proof 

259 
have t: "?t : ?T" by (rule dominoes_tile_matrix) 

260 
assume t'': "?t'' : ?T" 

7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

261 

10007  262 
let ?e = evnodd 
263 
have fin: "finite (?e ?t 0)" 

264 
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

265 

10007  266 
note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff 
267 
have "card (?e ?t'' 0) < card (?e ?t' 0)" 

268 
proof  

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

269 
have "card (?e ?t' 0  {(2 * m + 1, 2 * n + 1)}) 
10007  270 
< card (?e ?t' 0)" 
271 
proof (rule card_Diff1_less) 

10408  272 
from _ fin show "finite (?e ?t' 0)" 
10007  273 
by (rule finite_subset) auto 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

274 
show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp 
10007  275 
qed 
18153  276 
then show ?thesis by simp 
10007  277 
qed 
278 
also have "... < card (?e ?t 0)" 

279 
proof  

280 
have "(0, 0) : ?e ?t 0" by simp 

281 
with fin have "card (?e ?t 0  {(0, 0)}) < card (?e ?t 0)" 

282 
by (rule card_Diff1_less) 

18153  283 
then show ?thesis by simp 
10007  284 
qed 
285 
also from t have "... = card (?e ?t 1)" 

286 
by (rule tiling_domino_01) 

287 
also have "?e ?t 1 = ?e ?t'' 1" by simp 

288 
also from t'' have "card ... = card (?e ?t'' 0)" 

289 
by (rule tiling_domino_01 [symmetric]) 

18153  290 
finally have "... < ..." . then show False .. 
10007  291 
qed 
292 
qed 

7382
33c01075d343
The Mutilated Chess Board Problem  Isar'ized version of HOL/Inductive/Mutil;
wenzelm
parents:
diff
changeset

293 

10007  294 
end 