14 |
14 |
15 goal thy "!!t. t: tiling A ==> \ |
15 goal thy "!!t. t: tiling A ==> \ |
16 \ u: tiling A --> t <= Compl u --> t Un u : tiling A"; |
16 \ u: tiling A --> t <= Compl u --> t Un u : tiling A"; |
17 by (etac tiling.induct 1); |
17 by (etac tiling.induct 1); |
18 by (Simp_tac 1); |
18 by (Simp_tac 1); |
19 by (fast_tac (!claset addIs tiling.intrs |
19 by (simp_tac (!simpset addsimps [Un_assoc]) 1); |
20 addss (!simpset addsimps [Un_assoc])) 1); |
20 by (blast_tac (!claset addIs tiling.intrs) 1); |
21 qed_spec_mp "tiling_UnI"; |
21 qed_spec_mp "tiling_UnI"; |
22 |
22 |
23 |
23 |
24 (*** Chess boards ***) |
24 (*** Chess boards ***) |
25 |
25 |
27 Addsimps [below_0, below_Suc]; |
27 Addsimps [below_0, below_Suc]; |
28 |
28 |
29 goal thy "ALL i. (i: below k) = (i<k)"; |
29 goal thy "ALL i. (i: below k) = (i<k)"; |
30 by (nat_ind_tac "k" 1); |
30 by (nat_ind_tac "k" 1); |
31 by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq]))); |
31 by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq]))); |
32 by (Fast_tac 1); |
32 by (Blast_tac 1); |
33 qed_spec_mp "below_less_iff"; |
33 qed_spec_mp "below_less_iff"; |
34 |
34 |
35 Addsimps [below_less_iff]; |
35 Addsimps [below_less_iff]; |
36 |
36 |
37 goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; |
37 goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; |
38 by (Simp_tac 1); |
38 by (Simp_tac 1); |
39 by (Fast_tac 1); |
39 by (Blast_tac 1); |
40 qed "Sigma_Suc1"; |
40 qed "Sigma_Suc1"; |
41 |
41 |
42 goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; |
42 goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; |
43 by (Simp_tac 1); |
43 by (Simp_tac 1); |
44 by (Fast_tac 1); |
44 by (Blast_tac 1); |
45 qed "Sigma_Suc2"; |
45 qed "Sigma_Suc2"; |
46 |
46 |
47 (*Deletion is essential to allow use of Sigma_Suc1,2*) |
47 (*Deletion is essential to allow use of Sigma_Suc1,2*) |
48 Delsimps [below_Suc]; |
48 Delsimps [below_Suc]; |
49 |
49 |
53 by (resolve_tac tiling.intrs 1); |
53 by (resolve_tac tiling.intrs 1); |
54 by (assume_tac 2); |
54 by (assume_tac 2); |
55 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
55 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
56 "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \ |
56 "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \ |
57 \ {(i, n1+n1), (i, Suc(n1+n1))}" 1); |
57 \ {(i, n1+n1), (i, Suc(n1+n1))}" 1); |
58 by (Fast_tac 2); |
58 by (Blast_tac 2); |
59 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1); |
59 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1); |
60 by (fast_tac (!claset addEs [less_asym] |
60 by (blast_tac (!claset addEs [less_irrefl, less_asym] |
61 addSDs [below_less_iff RS iffD1]) 1); |
61 addSDs [below_less_iff RS iffD1]) 1); |
62 qed "dominoes_tile_row"; |
62 qed "dominoes_tile_row"; |
63 |
63 |
64 goal thy "(below m) Times below(n + n) : tiling domino"; |
64 goal thy "(below m) Times below(n + n) : tiling domino"; |
65 by (nat_ind_tac "m" 1); |
65 by (nat_ind_tac "m" 1); |
66 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1]))); |
66 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1]))); |
67 by (fast_tac (!claset addIs [equalityI, tiling_UnI, dominoes_tile_row] |
67 by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row] |
68 addEs [below_less_iff RS iffD1 RS less_irrefl]) 1); |
68 addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1); |
69 qed "dominoes_tile_matrix"; |
69 qed "dominoes_tile_matrix"; |
70 |
70 |
71 |
71 |
72 (*** Basic properties of evnodd ***) |
72 (*** Basic properties of evnodd ***) |
73 |
73 |
81 |
81 |
82 (* finite X ==> finite(evnodd X b) *) |
82 (* finite X ==> finite(evnodd X b) *) |
83 bind_thm("finite_evnodd", evnodd_subset RS finite_subset); |
83 bind_thm("finite_evnodd", evnodd_subset RS finite_subset); |
84 |
84 |
85 goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b"; |
85 goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b"; |
86 by (Fast_tac 1); |
86 by (Blast_tac 1); |
87 qed "evnodd_Un"; |
87 qed "evnodd_Un"; |
88 |
88 |
89 goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b"; |
89 goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b"; |
90 by (Fast_tac 1); |
90 by (Blast_tac 1); |
91 qed "evnodd_Diff"; |
91 qed "evnodd_Diff"; |
92 |
92 |
93 goalw thy [evnodd_def] "evnodd {} b = {}"; |
93 goalw thy [evnodd_def] "evnodd {} b = {}"; |
94 by (Simp_tac 1); |
94 by (Simp_tac 1); |
95 qed "evnodd_empty"; |
95 qed "evnodd_empty"; |
111 by (REPEAT_FIRST assume_tac); |
111 by (REPEAT_FIRST assume_tac); |
112 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*) |
112 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*) |
113 by (REPEAT (asm_full_simp_tac (!simpset addsimps |
113 by (REPEAT (asm_full_simp_tac (!simpset addsimps |
114 [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] |
114 [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] |
115 setloop split_tac [expand_if]) 1 |
115 setloop split_tac [expand_if]) 1 |
116 THEN Fast_tac 1)); |
116 THEN Blast_tac 1)); |
117 qed "domino_singleton"; |
117 qed "domino_singleton"; |
118 |
118 |
119 goal thy "!!d. d:domino ==> finite d"; |
119 goal thy "!!d. d:domino ==> finite d"; |
120 by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI] |
120 by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] |
121 addEs [domino.elim]) 1); |
121 addSEs [domino.elim]) 1); |
122 qed "domino_finite"; |
122 qed "domino_finite"; |
123 |
123 |
124 |
124 |
125 (*** Tilings of dominoes ***) |
125 (*** Tilings of dominoes ***) |
126 |
126 |
127 goal thy "!!t. t:tiling domino ==> finite t"; |
127 goal thy "!!t. t:tiling domino ==> finite t"; |
128 by (eresolve_tac [tiling.induct] 1); |
128 by (eresolve_tac [tiling.induct] 1); |
129 by (rtac finite_emptyI 1); |
129 by (rtac finite_emptyI 1); |
130 by (fast_tac (!claset addIs [domino_finite, finite_UnI]) 1); |
130 by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1); |
131 qed "tiling_domino_finite"; |
131 qed "tiling_domino_finite"; |
132 |
132 |
133 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)"; |
133 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)"; |
134 by (eresolve_tac [tiling.induct] 1); |
134 by (eresolve_tac [tiling.induct] 1); |
135 by (simp_tac (!simpset addsimps [evnodd_def]) 1); |
135 by (simp_tac (!simpset addsimps [evnodd_def]) 1); |
141 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1); |
141 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1); |
142 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, |
142 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, |
143 tiling_domino_finite, |
143 tiling_domino_finite, |
144 evnodd_subset RS finite_subset, |
144 evnodd_subset RS finite_subset, |
145 card_insert_disjoint]) 1); |
145 card_insert_disjoint]) 1); |
146 by (fast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); |
146 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); |
147 qed "tiling_domino_0_1"; |
147 qed "tiling_domino_0_1"; |
148 |
148 |
149 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \ |
149 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \ |
150 \ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \ |
150 \ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \ |
151 \ |] ==> t' ~: tiling domino"; |
151 \ |] ==> t' ~: tiling domino"; |