|
1 (* Title: ZF/ex/Mutil |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 The Mutilated Checkerboard Problem, formalized inductively |
|
7 *) |
|
8 |
|
9 open Mutil; |
|
10 |
|
11 |
|
12 (** Basic properties of evnodd **) |
|
13 |
|
14 Goalw [evnodd_def] "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b"; |
|
15 by (Blast_tac 1); |
|
16 qed "evnodd_iff"; |
|
17 |
|
18 Goalw [evnodd_def] "evnodd(A, b) \\<subseteq> A"; |
|
19 by (Blast_tac 1); |
|
20 qed "evnodd_subset"; |
|
21 |
|
22 (* Finite(X) ==> Finite(evnodd(X,b)) *) |
|
23 bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite); |
|
24 |
|
25 Goalw [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)"; |
|
26 by (simp_tac (simpset() addsimps [Collect_Un]) 1); |
|
27 qed "evnodd_Un"; |
|
28 |
|
29 Goalw [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"; |
|
30 by (simp_tac (simpset() addsimps [Collect_Diff]) 1); |
|
31 qed "evnodd_Diff"; |
|
32 |
|
33 Goalw [evnodd_def] |
|
34 "evnodd(cons(<i,j>,C), b) = \ |
|
35 \ (if (i#+j) mod 2 = b then cons(<i,j>, evnodd(C,b)) else evnodd(C,b))"; |
|
36 by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]) 1); |
|
37 qed "evnodd_cons"; |
|
38 |
|
39 Goalw [evnodd_def] "evnodd(0, b) = 0"; |
|
40 by (simp_tac (simpset() addsimps [evnodd_def]) 1); |
|
41 qed "evnodd_0"; |
|
42 |
|
43 Addsimps [evnodd_cons, evnodd_0]; |
|
44 |
|
45 (*** Dominoes ***) |
|
46 |
|
47 Goal "d \\<in> domino ==> Finite(d)"; |
|
48 by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1); |
|
49 qed "domino_Finite"; |
|
50 |
|
51 Goal "[| d \\<in> domino; b<2 |] ==> \\<exists>i' j'. evnodd(d,b) = {<i',j'>}"; |
|
52 by (eresolve_tac [domino.elim] 1); |
|
53 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 2); |
|
54 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 1); |
|
55 by (REPEAT_FIRST (ares_tac [add_type])); |
|
56 (*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*) |
|
57 by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self]) 1 |
|
58 THEN blast_tac (claset() addDs [ltD]) 1)); |
|
59 qed "domino_singleton"; |
|
60 |
|
61 |
|
62 (*** Tilings ***) |
|
63 |
|
64 (** The union of two disjoint tilings is a tiling **) |
|
65 |
|
66 Goal "t \\<in> tiling(A) ==> \ |
|
67 \ u \\<in> tiling(A) --> t Int u = 0 --> t Un u \\<in> tiling(A)"; |
|
68 by (etac tiling.induct 1); |
|
69 by (simp_tac (simpset() addsimps tiling.intrs) 1); |
|
70 by (asm_full_simp_tac (simpset() addsimps [Un_assoc, |
|
71 subset_empty_iff RS iff_sym]) 1); |
|
72 by (blast_tac (claset() addIs tiling.intrs) 1); |
|
73 qed_spec_mp "tiling_UnI"; |
|
74 |
|
75 Goal "t \\<in> tiling(domino) ==> Finite(t)"; |
|
76 by (eresolve_tac [tiling.induct] 1); |
|
77 by (rtac Finite_0 1); |
|
78 by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1); |
|
79 qed "tiling_domino_Finite"; |
|
80 |
|
81 Goal "t \\<in> tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"; |
|
82 by (eresolve_tac [tiling.induct] 1); |
|
83 by (simp_tac (simpset() addsimps [evnodd_def]) 1); |
|
84 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); |
|
85 by (Simp_tac 2 THEN assume_tac 1); |
|
86 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); |
|
87 by (Simp_tac 2 THEN assume_tac 1); |
|
88 by Safe_tac; |
|
89 by (subgoal_tac "\\<forall>p b. p \\<in> evnodd(a,b) --> p\\<notin>evnodd(t,b)" 1); |
|
90 by (asm_simp_tac |
|
91 (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite, |
|
92 evnodd_subset RS subset_Finite, |
|
93 Finite_imp_cardinal_cons]) 1); |
|
94 by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] |
|
95 addEs [equalityE]) 1); |
|
96 qed "tiling_domino_0_1"; |
|
97 |
|
98 Goal "[| i \\<in> nat; n \\<in> nat |] ==> {i} * (n #+ n) \\<in> tiling(domino)"; |
|
99 by (induct_tac "n" 1); |
|
100 by (simp_tac (simpset() addsimps tiling.intrs) 1); |
|
101 by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1); |
|
102 by (resolve_tac tiling.intrs 1); |
|
103 by (assume_tac 2); |
|
104 by (rename_tac "n'" 1); |
|
105 by (subgoal_tac (*seems the easiest way of turning one to the other*) |
|
106 "{i}*{succ(n'#+n')} Un {i}*{n'#+n'} = {<i,n'#+n'>, <i,succ(n'#+n')>}" 1); |
|
107 by (Blast_tac 2); |
|
108 by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1); |
|
109 by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1); |
|
110 qed "dominoes_tile_row"; |
|
111 |
|
112 Goal "[| m \\<in> nat; n \\<in> nat |] ==> m * (n #+ n) \\<in> tiling(domino)"; |
|
113 by (induct_tac "m" 1); |
|
114 by (simp_tac (simpset() addsimps tiling.intrs) 1); |
|
115 by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1); |
|
116 by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] |
|
117 addEs [mem_irrefl]) 1); |
|
118 qed "dominoes_tile_matrix"; |
|
119 |
|
120 Goal "[| x=y; x<y |] ==> P"; |
|
121 by Auto_tac; |
|
122 qed "eq_lt_E"; |
|
123 |
|
124 Goal "[| m \\<in> nat; n \\<in> nat; \ |
|
125 \ t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); \ |
|
126 \ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] \ |
|
127 \ ==> t' \\<notin> tiling(domino)"; |
|
128 by (rtac notI 1); |
|
129 by (dtac tiling_domino_0_1 1); |
|
130 by (eres_inst_tac [("x", "|?A|")] eq_lt_E 1); |
|
131 by (subgoal_tac "t \\<in> tiling(domino)" 1); |
|
132 (*Requires a small simpset that won't move the succ applications*) |
|
133 by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, |
|
134 dominoes_tile_matrix]) 2); |
|
135 by (asm_full_simp_tac |
|
136 (simpset() addsimps [evnodd_Diff, mod2_add_self, |
|
137 mod2_succ_succ, tiling_domino_0_1 RS sym]) 1); |
|
138 by (rtac lt_trans 1); |
|
139 by (REPEAT |
|
140 (rtac Finite_imp_cardinal_Diff 1 |
|
141 THEN |
|
142 asm_simp_tac (simpset() addsimps [tiling_domino_Finite, Finite_evnodd, |
|
143 Finite_Diff]) 1 |
|
144 THEN |
|
145 asm_simp_tac (simpset() addsimps [evnodd_iff, nat_0_le RS ltD, |
|
146 mod2_add_self]) 1)); |
|
147 qed "mutil_not_tiling"; |