27 horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino" |
27 horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino" |
28 vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino" |
28 vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino" |
29 |
29 |
30 constdefs |
30 constdefs |
31 coloured :: "nat => (nat \<times> nat) set" |
31 coloured :: "nat => (nat \<times> nat) set" |
32 "coloured b == {(i, j). (i + j) mod # 2 = b}" |
32 "coloured b == {(i, j). (i + j) mod 2 = b}" |
33 |
33 |
34 |
34 |
35 text {* \medskip The union of two disjoint tilings is a tiling *} |
35 text {* \medskip The union of two disjoint tilings is a tiling *} |
36 |
36 |
37 lemma tiling_UnI [rule_format, intro]: |
37 lemma tiling_UnI [rule_format, intro]: |
59 |
59 |
60 lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}" |
60 lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}" |
61 apply auto |
61 apply auto |
62 done |
62 done |
63 |
63 |
64 lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (# 2 * n) \<in> tiling domino" |
64 lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (2 * n) \<in> tiling domino" |
65 apply (induct n) |
65 apply (induct n) |
66 apply (simp_all add: Un_assoc [symmetric]) |
66 apply (simp_all add: Un_assoc [symmetric]) |
67 apply (rule tiling.Un) |
67 apply (rule tiling.Un) |
68 apply (auto simp add: sing_Times_lemma) |
68 apply (auto simp add: sing_Times_lemma) |
69 done |
69 done |
70 |
70 |
71 lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (# 2 * n) \<in> tiling domino" |
71 lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino" |
72 apply (induct m) |
72 apply (induct m) |
73 apply auto |
73 apply auto |
74 done |
74 done |
75 |
75 |
76 |
76 |
77 text {* \medskip @{term coloured} and Dominoes *} |
77 text {* \medskip @{term coloured} and Dominoes *} |
78 |
78 |
79 lemma coloured_insert [simp]: |
79 lemma coloured_insert [simp]: |
80 "coloured b \<inter> (insert (i, j) t) = |
80 "coloured b \<inter> (insert (i, j) t) = |
81 (if (i + j) mod # 2 = b then insert (i, j) (coloured b \<inter> t) |
81 (if (i + j) mod 2 = b then insert (i, j) (coloured b \<inter> t) |
82 else coloured b \<inter> t)" |
82 else coloured b \<inter> t)" |
83 apply (unfold coloured_def) |
83 apply (unfold coloured_def) |
84 apply auto |
84 apply auto |
85 done |
85 done |
86 |
86 |
123 |
123 |
124 text {* \medskip Final argument is surprisingly complex *} |
124 text {* \medskip Final argument is surprisingly complex *} |
125 |
125 |
126 theorem gen_mutil_not_tiling: |
126 theorem gen_mutil_not_tiling: |
127 "t \<in> tiling domino ==> |
127 "t \<in> tiling domino ==> |
128 (i + j) mod # 2 = 0 ==> (m + n) mod # 2 = 0 ==> |
128 (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==> |
129 {(i, j), (m, n)} \<subseteq> t |
129 {(i, j), (m, n)} \<subseteq> t |
130 ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino" |
130 ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino" |
131 apply (rule notI) |
131 apply (rule notI) |
132 apply (subgoal_tac |
132 apply (subgoal_tac |
133 "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) < |
133 "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) < |
138 done |
138 done |
139 |
139 |
140 text {* Apply the general theorem to the well-known case *} |
140 text {* Apply the general theorem to the well-known case *} |
141 |
141 |
142 theorem mutil_not_tiling: |
142 theorem mutil_not_tiling: |
143 "t = lessThan (# 2 * Suc m) \<times> lessThan (# 2 * Suc n) |
143 "t = lessThan (2 * Suc m) \<times> lessThan (2 * Suc n) |
144 ==> t - {(0, 0)} - {(Suc (# 2 * m), Suc (# 2 * n))} \<notin> tiling domino" |
144 ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} \<notin> tiling domino" |
145 apply (rule gen_mutil_not_tiling) |
145 apply (rule gen_mutil_not_tiling) |
146 apply (blast intro!: dominoes_tile_matrix) |
146 apply (blast intro!: dominoes_tile_matrix) |
147 apply auto |
147 apply auto |
148 done |
148 done |
149 |
149 |