21 |
21 |
22 (* Finite(X) ==> Finite(evnodd(X,b)) *) |
22 (* Finite(X) ==> Finite(evnodd(X,b)) *) |
23 bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite); |
23 bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite); |
24 |
24 |
25 goalw thy [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)"; |
25 goalw thy [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)"; |
26 by (simp_tac (!simpset addsimps [Collect_Un]) 1); |
26 by (simp_tac (simpset() addsimps [Collect_Un]) 1); |
27 qed "evnodd_Un"; |
27 qed "evnodd_Un"; |
28 |
28 |
29 goalw thy [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"; |
29 goalw thy [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"; |
30 by (simp_tac (!simpset addsimps [Collect_Diff]) 1); |
30 by (simp_tac (simpset() addsimps [Collect_Diff]) 1); |
31 qed "evnodd_Diff"; |
31 qed "evnodd_Diff"; |
32 |
32 |
33 goalw thy [evnodd_def] |
33 goalw thy [evnodd_def] |
34 "evnodd(cons(<i,j>,C), b) = \ |
34 "evnodd(cons(<i,j>,C), b) = \ |
35 \ if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))"; |
35 \ if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))"; |
36 by (asm_simp_tac (!simpset addsimps [evnodd_def, Collect_cons] |
36 by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons] |
37 setloop split_tac [expand_if]) 1); |
37 setloop split_tac [expand_if]) 1); |
38 qed "evnodd_cons"; |
38 qed "evnodd_cons"; |
39 |
39 |
40 goalw thy [evnodd_def] "evnodd(0, b) = 0"; |
40 goalw thy [evnodd_def] "evnodd(0, b) = 0"; |
41 by (simp_tac (!simpset addsimps [evnodd_def]) 1); |
41 by (simp_tac (simpset() addsimps [evnodd_def]) 1); |
42 qed "evnodd_0"; |
42 qed "evnodd_0"; |
43 |
43 |
44 Addsimps [evnodd_cons, evnodd_0]; |
44 Addsimps [evnodd_cons, evnodd_0]; |
45 |
45 |
46 (*** Dominoes ***) |
46 (*** Dominoes ***) |
47 |
47 |
48 goal thy "!!d. d:domino ==> Finite(d)"; |
48 goal thy "!!d. d:domino ==> Finite(d)"; |
49 by (blast_tac (!claset addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1); |
49 by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1); |
50 qed "domino_Finite"; |
50 qed "domino_Finite"; |
51 |
51 |
52 goal thy "!!d. [| d:domino; b<2 |] ==> EX i' j'. evnodd(d,b) = {<i',j'>}"; |
52 goal thy "!!d. [| d:domino; b<2 |] ==> EX i' j'. evnodd(d,b) = {<i',j'>}"; |
53 by (eresolve_tac [domino.elim] 1); |
53 by (eresolve_tac [domino.elim] 1); |
54 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 2); |
54 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 2); |
55 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 1); |
55 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 1); |
56 by (REPEAT_FIRST (ares_tac [add_type])); |
56 by (REPEAT_FIRST (ares_tac [add_type])); |
57 (*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*) |
57 (*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*) |
58 by (REPEAT (asm_simp_tac (!simpset addsimps [mod_succ, succ_neq_self] |
58 by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self] |
59 setloop split_tac [expand_if]) 1 |
59 setloop split_tac [expand_if]) 1 |
60 THEN blast_tac (!claset addDs [ltD]) 1)); |
60 THEN blast_tac (claset() addDs [ltD]) 1)); |
61 qed "domino_singleton"; |
61 qed "domino_singleton"; |
62 |
62 |
63 |
63 |
64 (*** Tilings ***) |
64 (*** Tilings ***) |
65 |
65 |
66 (** The union of two disjoint tilings is a tiling **) |
66 (** The union of two disjoint tilings is a tiling **) |
67 |
67 |
68 goal thy "!!t. t: tiling(A) ==> \ |
68 goal thy "!!t. t: tiling(A) ==> \ |
69 \ u: tiling(A) --> t Int u = 0 --> t Un u : tiling(A)"; |
69 \ u: tiling(A) --> t Int u = 0 --> t Un u : tiling(A)"; |
70 by (etac tiling.induct 1); |
70 by (etac tiling.induct 1); |
71 by (simp_tac (!simpset addsimps tiling.intrs) 1); |
71 by (simp_tac (simpset() addsimps tiling.intrs) 1); |
72 by (asm_full_simp_tac (!simpset addsimps [Un_assoc, |
72 by (asm_full_simp_tac (simpset() addsimps [Un_assoc, |
73 subset_empty_iff RS iff_sym]) 1); |
73 subset_empty_iff RS iff_sym]) 1); |
74 by (blast_tac (!claset addIs tiling.intrs) 1); |
74 by (blast_tac (claset() addIs tiling.intrs) 1); |
75 qed_spec_mp "tiling_UnI"; |
75 qed_spec_mp "tiling_UnI"; |
76 |
76 |
77 goal thy "!!t. t:tiling(domino) ==> Finite(t)"; |
77 goal thy "!!t. t:tiling(domino) ==> Finite(t)"; |
78 by (eresolve_tac [tiling.induct] 1); |
78 by (eresolve_tac [tiling.induct] 1); |
79 by (resolve_tac [Finite_0] 1); |
79 by (resolve_tac [Finite_0] 1); |
80 by (blast_tac (!claset addSIs [Finite_Un] addIs [domino_Finite]) 1); |
80 by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1); |
81 qed "tiling_domino_Finite"; |
81 qed "tiling_domino_Finite"; |
82 |
82 |
83 goal thy "!!t. t: tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"; |
83 goal thy "!!t. t: tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"; |
84 by (eresolve_tac [tiling.induct] 1); |
84 by (eresolve_tac [tiling.induct] 1); |
85 by (simp_tac (!simpset addsimps [evnodd_def]) 1); |
85 by (simp_tac (simpset() addsimps [evnodd_def]) 1); |
86 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); |
86 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); |
87 by (Simp_tac 2 THEN assume_tac 1); |
87 by (Simp_tac 2 THEN assume_tac 1); |
88 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); |
88 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); |
89 by (Simp_tac 2 THEN assume_tac 1); |
89 by (Simp_tac 2 THEN assume_tac 1); |
90 by (Step_tac 1); |
90 by (Step_tac 1); |
91 by (subgoal_tac "ALL p b. p:evnodd(a,b) --> p~:evnodd(ta,b)" 1); |
91 by (subgoal_tac "ALL p b. p:evnodd(a,b) --> p~:evnodd(ta,b)" 1); |
92 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_cons, tiling_domino_Finite, |
92 by (asm_simp_tac (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite, |
93 evnodd_subset RS subset_Finite, |
93 evnodd_subset RS subset_Finite, |
94 Finite_imp_cardinal_cons]) 1); |
94 Finite_imp_cardinal_cons]) 1); |
95 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); |
95 by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); |
96 qed "tiling_domino_0_1"; |
96 qed "tiling_domino_0_1"; |
97 |
97 |
98 goal thy "!!i n. [| i: nat; n: nat |] ==> {i} * (n #+ n) : tiling(domino)"; |
98 goal thy "!!i n. [| i: nat; n: nat |] ==> {i} * (n #+ n) : tiling(domino)"; |
99 by (nat_ind_tac "n" [] 1); |
99 by (nat_ind_tac "n" [] 1); |
100 by (simp_tac (!simpset addsimps tiling.intrs) 1); |
100 by (simp_tac (simpset() addsimps tiling.intrs) 1); |
101 by (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_succ2]) 1); |
101 by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1); |
102 by (resolve_tac tiling.intrs 1); |
102 by (resolve_tac tiling.intrs 1); |
103 by (assume_tac 2); |
103 by (assume_tac 2); |
104 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
104 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
105 "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1); |
105 "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1); |
106 by (Blast_tac 2); |
106 by (Blast_tac 2); |
107 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1); |
107 by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1); |
108 by (blast_tac (!claset addEs [mem_irrefl, mem_asym]) 1); |
108 by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1); |
109 qed "dominoes_tile_row"; |
109 qed "dominoes_tile_row"; |
110 |
110 |
111 goal thy "!!m n. [| m: nat; n: nat |] ==> m * (n #+ n) : tiling(domino)"; |
111 goal thy "!!m n. [| m: nat; n: nat |] ==> m * (n #+ n) : tiling(domino)"; |
112 by (nat_ind_tac "m" [] 1); |
112 by (nat_ind_tac "m" [] 1); |
113 by (simp_tac (!simpset addsimps tiling.intrs) 1); |
113 by (simp_tac (simpset() addsimps tiling.intrs) 1); |
114 by (asm_simp_tac (!simpset addsimps [Sigma_succ1]) 1); |
114 by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1); |
115 by (blast_tac (!claset addIs [tiling_UnI, dominoes_tile_row] |
115 by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] |
116 addEs [mem_irrefl]) 1); |
116 addEs [mem_irrefl]) 1); |
117 qed "dominoes_tile_matrix"; |
117 qed "dominoes_tile_matrix"; |
118 |
118 |
119 |
119 |
120 goal thy "!!m n. [| m: nat; n: nat; \ |
120 goal thy "!!m n. [| m: nat; n: nat; \ |
122 \ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] ==> \ |
122 \ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] ==> \ |
123 \ t' ~: tiling(domino)"; |
123 \ t' ~: tiling(domino)"; |
124 by (resolve_tac [notI] 1); |
124 by (resolve_tac [notI] 1); |
125 by (dresolve_tac [tiling_domino_0_1] 1); |
125 by (dresolve_tac [tiling_domino_0_1] 1); |
126 by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1); |
126 by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1); |
127 by (asm_full_simp_tac (!simpset addsimps [lt_not_refl]) 1); |
127 by (asm_full_simp_tac (simpset() addsimps [lt_not_refl]) 1); |
128 by (subgoal_tac "t : tiling(domino)" 1); |
128 by (subgoal_tac "t : tiling(domino)" 1); |
129 (*Requires a small simpset that won't move the succ applications*) |
129 (*Requires a small simpset that won't move the succ applications*) |
130 by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, |
130 by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, |
131 dominoes_tile_matrix]) 2); |
131 dominoes_tile_matrix]) 2); |
132 by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1); |
132 by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1); |
133 by (asm_simp_tac (!simpset addsimps add_ac) 2); |
133 by (asm_simp_tac (simpset() addsimps add_ac) 2); |
134 by (asm_full_simp_tac |
134 by (asm_full_simp_tac |
135 (!simpset addsimps [evnodd_Diff, mod2_add_self, |
135 (simpset() addsimps [evnodd_Diff, mod2_add_self, |
136 mod2_succ_succ, tiling_domino_0_1 RS sym]) 1); |
136 mod2_succ_succ, tiling_domino_0_1 RS sym]) 1); |
137 by (resolve_tac [lt_trans] 1); |
137 by (resolve_tac [lt_trans] 1); |
138 by (REPEAT |
138 by (REPEAT |
139 (rtac Finite_imp_cardinal_Diff 1 |
139 (rtac Finite_imp_cardinal_Diff 1 |
140 THEN |
140 THEN |
141 asm_simp_tac (!simpset addsimps [tiling_domino_Finite, Finite_evnodd, |
141 asm_simp_tac (simpset() addsimps [tiling_domino_Finite, Finite_evnodd, |
142 Finite_Diff]) 1 |
142 Finite_Diff]) 1 |
143 THEN |
143 THEN |
144 asm_simp_tac (!simpset addsimps [evnodd_iff, nat_0_le RS ltD, |
144 asm_simp_tac (simpset() addsimps [evnodd_iff, nat_0_le RS ltD, |
145 mod2_add_self]) 1)); |
145 mod2_add_self]) 1)); |
146 qed "mutil_not_tiling"; |
146 qed "mutil_not_tiling"; |