equal
deleted
inserted
replaced
30 qed "below_0"; |
30 qed "below_0"; |
31 Addsimps [below_0]; |
31 Addsimps [below_0]; |
32 |
32 |
33 Goalw [below_def] |
33 Goalw [below_def] |
34 "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; |
34 "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; |
35 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
35 by Auto_tac; |
36 by (Blast_tac 1); |
|
37 qed "Sigma_Suc1"; |
36 qed "Sigma_Suc1"; |
38 |
37 |
39 Goalw [below_def] |
38 Goalw [below_def] |
40 "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; |
39 "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; |
41 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
40 by Auto_tac; |
42 by (Blast_tac 1); |
|
43 qed "Sigma_Suc2"; |
41 qed "Sigma_Suc2"; |
44 |
42 |
45 Goal "{i} Times below(n+n) : tiling domino"; |
43 Goal "{i} Times below(n+n) : tiling domino"; |
46 by (induct_tac "n" 1); |
44 by (induct_tac "n" 1); |
47 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2]))); |
45 by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2]))); |
48 by (resolve_tac tiling.intrs 1); |
46 by (resolve_tac tiling.intrs 1); |
49 by (assume_tac 2); |
47 by (assume_tac 2); |
50 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
48 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
51 "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \ |
49 "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \ |
52 \ {(i, n+n), (i, Suc(n+n))}" 1); |
50 \ {(i, n+n), (i, Suc(n+n))}" 1); |
89 qed "evnodd_empty"; |
87 qed "evnodd_empty"; |
90 |
88 |
91 Goalw [evnodd_def] |
89 Goalw [evnodd_def] |
92 "evnodd (insert (i,j) C) b = \ |
90 "evnodd (insert (i,j) C) b = \ |
93 \ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)"; |
91 \ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)"; |
94 by (Simp_tac 1); |
92 by Auto_tac; |
95 by (Blast_tac 1); |
|
96 qed "evnodd_insert"; |
93 qed "evnodd_insert"; |
97 |
94 |
98 Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert]; |
95 Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert]; |
99 |
96 |
100 |
97 |
104 by (eresolve_tac [domino.elim] 1); |
101 by (eresolve_tac [domino.elim] 1); |
105 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2); |
102 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2); |
106 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1); |
103 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1); |
107 by (REPEAT_FIRST assume_tac); |
104 by (REPEAT_FIRST assume_tac); |
108 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*) |
105 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*) |
109 by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1 |
106 by(auto_tac (claset(), simpset() addsimps [less_Suc_eq, mod_Suc])); |
110 THEN Blast_tac 1)); |
|
111 qed "domino_singleton"; |
107 qed "domino_singleton"; |
112 |
108 |
113 Goal "d:domino ==> finite d"; |
109 Goal "d:domino ==> finite d"; |
114 by (blast_tac (claset() addSEs [domino.elim]) 1); |
110 by (blast_tac (claset() addSEs [domino.elim]) 1); |
115 qed "domino_finite"; |
111 qed "domino_finite"; |
125 |
121 |
126 Goal "t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)"; |
122 Goal "t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)"; |
127 by (eresolve_tac [tiling.induct] 1); |
123 by (eresolve_tac [tiling.induct] 1); |
128 by (simp_tac (simpset() addsimps [evnodd_def]) 1); |
124 by (simp_tac (simpset() addsimps [evnodd_def]) 1); |
129 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); |
125 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); |
130 by (Simp_tac 2 THEN assume_tac 1); |
126 by Auto_tac; |
131 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); |
127 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); |
132 by (Simp_tac 2 THEN assume_tac 1); |
128 by Auto_tac; |
133 by (Clarify_tac 1); |
|
134 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd t b" 1); |
129 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd t b" 1); |
135 by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1); |
130 by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1); |
136 by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] |
131 by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] |
137 addEs [equalityE]) 1); |
132 addEs [equalityE]) 1); |
138 qed "tiling_domino_0_1"; |
133 qed "tiling_domino_0_1"; |