equal
deleted
inserted
replaced
58 qed |
58 qed |
59 |
59 |
60 |
60 |
61 subsection {* Basic properties of ``below'' *} |
61 subsection {* Basic properties of ``below'' *} |
62 |
62 |
63 constdefs |
63 definition below :: "nat => nat set" where |
64 below :: "nat => nat set" |
|
65 "below n == {i. i < n}" |
64 "below n == {i. i < n}" |
66 |
65 |
67 lemma below_less_iff [iff]: "(i: below k) = (i < k)" |
66 lemma below_less_iff [iff]: "(i: below k) = (i < k)" |
68 by (simp add: below_def) |
67 by (simp add: below_def) |
69 |
68 |
82 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2 |
81 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2 |
83 |
82 |
84 |
83 |
85 subsection {* Basic properties of ``evnodd'' *} |
84 subsection {* Basic properties of ``evnodd'' *} |
86 |
85 |
87 constdefs |
86 definition evnodd :: "(nat * nat) set => nat => (nat * nat) set" where |
88 evnodd :: "(nat * nat) set => nat => (nat * nat) set" |
|
89 "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}" |
87 "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}" |
90 |
88 |
91 lemma evnodd_iff: |
89 lemma evnodd_iff: |
92 "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)" |
90 "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)" |
93 by (simp add: evnodd_def) |
91 by (simp add: evnodd_def) |
245 qed |
243 qed |
246 |
244 |
247 |
245 |
248 subsection {* Main theorem *} |
246 subsection {* Main theorem *} |
249 |
247 |
250 constdefs |
248 definition mutilated_board :: "nat => nat => (nat * nat) set" where |
251 mutilated_board :: "nat => nat => (nat * nat) set" |
|
252 "mutilated_board m n == |
249 "mutilated_board m n == |
253 below (2 * (m + 1)) <*> below (2 * (n + 1)) |
250 below (2 * (m + 1)) <*> below (2 * (n + 1)) |
254 - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}" |
251 - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}" |
255 |
252 |
256 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino" |
253 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino" |