184 assumes d: "d: domino" |
184 assumes d: "d: domino" |
185 shows "finite d" |
185 shows "finite d" |
186 using d |
186 using d |
187 proof induct |
187 proof induct |
188 fix i j :: nat |
188 fix i j :: nat |
189 show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros) |
189 show "finite {(i, j), (i, j + 1)}" by (intro finite.intros) |
190 show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros) |
190 show "finite {(i, j), (i + 1, j)}" by (intro finite.intros) |
191 qed |
191 qed |
192 |
192 |
193 |
193 |
194 subsection {* Tilings of dominoes *} |
194 subsection {* Tilings of dominoes *} |
195 |
195 |
196 lemma tiling_domino_finite: |
196 lemma tiling_domino_finite: |
197 assumes t: "t : tiling domino" (is "t : ?T") |
197 assumes t: "t : tiling domino" (is "t : ?T") |
198 shows "finite t" (is "?F t") |
198 shows "finite t" (is "?F t") |
199 using t |
199 using t |
200 proof induct |
200 proof induct |
201 show "?F {}" by (rule Finites.emptyI) |
201 show "?F {}" by (rule finite.emptyI) |
202 fix a t assume "?F t" |
202 fix a t assume "?F t" |
203 assume "a : domino" then have "?F a" by (rule domino_finite) |
203 assume "a : domino" then have "?F a" by (rule domino_finite) |
204 then show "?F (a Un t)" by (rule finite_UnI) |
204 then show "?F (a Un t)" by (rule finite_UnI) |
205 qed |
205 qed |
206 |
206 |