13 |
13 |
14 Originator is Max Black, according to J A Robinson. Popularized as |
14 Originator is Max Black, according to J A Robinson. Popularized as |
15 the Mutilated Checkerboard Problem by J McCarthy. |
15 the Mutilated Checkerboard Problem by J McCarthy. |
16 *} |
16 *} |
17 |
17 |
18 consts tiling :: "'a set set => 'a set set" |
18 inductive_set |
19 inductive "tiling A" |
19 tiling :: "'a set set => 'a set set" |
20 intros |
20 for A :: "'a set set" |
|
21 where |
21 empty [simp, intro]: "{} \<in> tiling A" |
22 empty [simp, intro]: "{} \<in> tiling A" |
22 Un [simp, intro]: "[| a \<in> A; t \<in> tiling A; a \<inter> t = {} |] |
23 | Un [simp, intro]: "[| a \<in> A; t \<in> tiling A; a \<inter> t = {} |] |
23 ==> a \<union> t \<in> tiling A" |
24 ==> a \<union> t \<in> tiling A" |
24 |
25 |
25 consts domino :: "(nat \<times> nat) set set" |
26 inductive_set |
26 inductive domino |
27 domino :: "(nat \<times> nat) set set" |
27 intros |
28 where |
28 horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino" |
29 horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino" |
29 vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino" |
30 | vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino" |
30 |
31 |
31 text {* \medskip Sets of squares of the given colour*} |
32 text {* \medskip Sets of squares of the given colour*} |
32 |
33 |
33 definition |
34 definition |
34 coloured :: "nat => (nat \<times> nat) set" where |
35 coloured :: "nat => (nat \<times> nat) set" where |