28 horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino" |
28 horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino" |
29 vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino" |
29 vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino" |
30 |
30 |
31 text {* \medskip Sets of squares of the given colour*} |
31 text {* \medskip Sets of squares of the given colour*} |
32 |
32 |
33 constdefs |
33 definition |
34 coloured :: "nat => (nat \<times> nat) set" |
34 coloured :: "nat => (nat \<times> nat) set" |
35 "coloured b == {(i, j). (i + j) mod 2 = b}" |
35 "coloured b = {(i, j). (i + j) mod 2 = b}" |
36 |
36 |
37 syntax whites :: "(nat \<times> nat) set" |
37 abbreviation |
38 blacks :: "(nat \<times> nat) set" |
38 whites :: "(nat \<times> nat) set" |
39 |
39 "whites == coloured 0" |
40 translations |
40 blacks :: "(nat \<times> nat) set" |
41 "whites" == "coloured 0" |
41 "blacks == coloured (Suc 0)" |
42 "blacks" == "coloured (Suc 0)" |
|
43 |
42 |
44 |
43 |
45 text {* \medskip The union of two disjoint tilings is a tiling *} |
44 text {* \medskip The union of two disjoint tilings is a tiling *} |
46 |
45 |
47 lemma tiling_UnI [intro]: |
46 lemma tiling_UnI [intro]: |