33 qed "below_0"; |
33 qed "below_0"; |
34 Addsimps [below_0]; |
34 Addsimps [below_0]; |
35 |
35 |
36 goalw thy [below_def] |
36 goalw thy [below_def] |
37 "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; |
37 "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; |
38 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
38 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
39 by (Blast_tac 1); |
39 by (Blast_tac 1); |
40 qed "Sigma_Suc1"; |
40 qed "Sigma_Suc1"; |
41 |
41 |
42 goalw thy [below_def] |
42 goalw thy [below_def] |
43 "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; |
43 "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; |
44 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
44 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
45 by (Blast_tac 1); |
45 by (Blast_tac 1); |
46 qed "Sigma_Suc2"; |
46 qed "Sigma_Suc2"; |
47 |
47 |
48 goal thy "{i} Times below(n+n) : tiling domino"; |
48 goal thy "{i} Times below(n+n) : tiling domino"; |
49 by (nat_ind_tac "n" 1); |
49 by (nat_ind_tac "n" 1); |
50 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2]))); |
50 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2]))); |
51 by (resolve_tac tiling.intrs 1); |
51 by (resolve_tac tiling.intrs 1); |
52 by (assume_tac 2); |
52 by (assume_tac 2); |
53 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
53 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
54 "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \ |
54 "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \ |
55 \ {(i, n+n), (i, Suc(n+n))}" 1); |
55 \ {(i, n+n), (i, Suc(n+n))}" 1); |
56 by (Blast_tac 2); |
56 by (Blast_tac 2); |
57 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1); |
57 by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1); |
58 by (Auto_tac()); |
58 by (Auto_tac()); |
59 qed "dominoes_tile_row"; |
59 qed "dominoes_tile_row"; |
60 |
60 |
61 goal thy "(below m) Times below(n+n) : tiling domino"; |
61 goal thy "(below m) Times below(n+n) : tiling domino"; |
62 by (nat_ind_tac "m" 1); |
62 by (nat_ind_tac "m" 1); |
63 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1]))); |
63 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1]))); |
64 by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row] |
64 by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row] |
65 addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1); |
65 addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1); |
66 qed "dominoes_tile_matrix"; |
66 qed "dominoes_tile_matrix"; |
67 |
67 |
68 |
68 |
69 (*** Basic properties of evnodd ***) |
69 (*** Basic properties of evnodd ***) |
92 qed "evnodd_empty"; |
92 qed "evnodd_empty"; |
93 |
93 |
94 goalw thy [evnodd_def] |
94 goalw thy [evnodd_def] |
95 "evnodd (insert (i,j) C) b = \ |
95 "evnodd (insert (i,j) C) b = \ |
96 \ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)"; |
96 \ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)"; |
97 by (simp_tac (!simpset addsplits [expand_if]) 1); |
97 by (simp_tac (simpset() addsplits [expand_if]) 1); |
98 by (Blast_tac 1); |
98 by (Blast_tac 1); |
99 qed "evnodd_insert"; |
99 qed "evnodd_insert"; |
100 |
100 |
101 Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert]; |
101 Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert]; |
102 |
102 |
107 by (eresolve_tac [domino.elim] 1); |
107 by (eresolve_tac [domino.elim] 1); |
108 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2); |
108 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2); |
109 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1); |
109 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1); |
110 by (REPEAT_FIRST assume_tac); |
110 by (REPEAT_FIRST assume_tac); |
111 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*) |
111 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*) |
112 by (REPEAT (asm_full_simp_tac (!simpset addsimps [less_Suc_eq, mod_Suc] |
112 by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc] |
113 addsplits [expand_if]) 1 |
113 addsplits [expand_if]) 1 |
114 THEN Blast_tac 1)); |
114 THEN Blast_tac 1)); |
115 qed "domino_singleton"; |
115 qed "domino_singleton"; |
116 |
116 |
117 goal thy "!!d. d:domino ==> finite d"; |
117 goal thy "!!d. d:domino ==> finite d"; |
118 by (blast_tac (!claset addSEs [domino.elim]) 1); |
118 by (blast_tac (claset() addSEs [domino.elim]) 1); |
119 qed "domino_finite"; |
119 qed "domino_finite"; |
120 |
120 |
121 |
121 |
122 (*** Tilings of dominoes ***) |
122 (*** Tilings of dominoes ***) |
123 |
123 |
124 goal thy "!!t. t:tiling domino ==> finite t"; |
124 goal thy "!!t. t:tiling domino ==> finite t"; |
125 by (eresolve_tac [tiling.induct] 1); |
125 by (eresolve_tac [tiling.induct] 1); |
126 by (rtac Finites.emptyI 1); |
126 by (rtac Finites.emptyI 1); |
127 by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1); |
127 by (blast_tac (claset() addSIs [finite_UnI] addIs [domino_finite]) 1); |
128 qed "tiling_domino_finite"; |
128 qed "tiling_domino_finite"; |
129 |
129 |
130 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)"; |
130 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)"; |
131 by (eresolve_tac [tiling.induct] 1); |
131 by (eresolve_tac [tiling.induct] 1); |
132 by (simp_tac (!simpset addsimps [evnodd_def]) 1); |
132 by (simp_tac (simpset() addsimps [evnodd_def]) 1); |
133 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); |
133 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); |
134 by (Simp_tac 2 THEN assume_tac 1); |
134 by (Simp_tac 2 THEN assume_tac 1); |
135 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); |
135 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); |
136 by (Simp_tac 2 THEN assume_tac 1); |
136 by (Simp_tac 2 THEN assume_tac 1); |
137 by (Clarify_tac 1); |
137 by (Clarify_tac 1); |
138 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1); |
138 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1); |
139 by (asm_simp_tac (!simpset addsimps [tiling_domino_finite]) 1); |
139 by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1); |
140 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); |
140 by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); |
141 qed "tiling_domino_0_1"; |
141 qed "tiling_domino_0_1"; |
142 |
142 |
143 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \ |
143 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \ |
144 \ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \ |
144 \ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \ |
145 \ |] ==> t' ~: tiling domino"; |
145 \ |] ==> t' ~: tiling domino"; |
149 by (Asm_full_simp_tac 1); |
149 by (Asm_full_simp_tac 1); |
150 by (subgoal_tac "t : tiling domino" 1); |
150 by (subgoal_tac "t : tiling domino" 1); |
151 (*Requires a small simpset that won't move the Suc applications*) |
151 (*Requires a small simpset that won't move the Suc applications*) |
152 by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2); |
152 by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2); |
153 by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1); |
153 by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1); |
154 by (asm_simp_tac (!simpset addsimps add_ac) 2); |
154 by (asm_simp_tac (simpset() addsimps add_ac) 2); |
155 by (asm_full_simp_tac |
155 by (asm_full_simp_tac |
156 (!simpset addsimps [mod_less, tiling_domino_0_1 RS sym]) 1); |
156 (simpset() addsimps [mod_less, tiling_domino_0_1 RS sym]) 1); |
157 by (rtac less_trans 1); |
157 by (rtac less_trans 1); |
158 by (REPEAT |
158 by (REPEAT |
159 (rtac card_Diff 1 |
159 (rtac card_Diff 1 |
160 THEN asm_simp_tac (!simpset addsimps [tiling_domino_finite]) 1 |
160 THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 |
161 THEN asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1)); |
161 THEN asm_simp_tac (simpset() addsimps [mod_less, evnodd_iff]) 1)); |
162 qed "mutil_not_tiling"; |
162 qed "mutil_not_tiling"; |