1(*  Title:      ZF/Induct/Mutil.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1996  University of Cambridge
4*)
5
6section \<open>The Mutilated Chess Board Problem, formalized inductively\<close>
7
8theory Mutil imports ZF begin
9
10text \<open>
11  Originator is Max Black, according to J A Robinson.  Popularized as
12  the Mutilated Checkerboard Problem by J McCarthy.
13\<close>
14
15consts
16  domino :: i
17  tiling :: "i => i"
18
19inductive
20  domains "domino" \<subseteq> "Pow(nat \<times> nat)"
21  intros
22    horiz: "[| i \<in> nat;  j \<in> nat |] ==> {<i,j>, <i,succ(j)>} \<in> domino"
23    vertl: "[| i \<in> nat;  j \<in> nat |] ==> {<i,j>, <succ(i),j>} \<in> domino"
24  type_intros empty_subsetI cons_subsetI PowI SigmaI nat_succI
25
26inductive
27  domains "tiling(A)" \<subseteq> "Pow(\<Union>(A))"
28  intros
29    empty: "0 \<in> tiling(A)"
30    Un: "[| a \<in> A;  t \<in> tiling(A);  a \<inter> t = 0 |] ==> a \<union> t \<in> tiling(A)"
31  type_intros empty_subsetI Union_upper Un_least PowI
32  type_elims PowD [elim_format]
33
34definition
35  evnodd :: "[i, i] => i"  where
36  "evnodd(A,b) == {z \<in> A. \<exists>i j. z = <i,j> \<and> (i #+ j) mod 2 = b}"
37
38
39subsection \<open>Basic properties of evnodd\<close>
40
41lemma evnodd_iff: "<i,j>: evnodd(A,b) \<longleftrightarrow> <i,j>: A & (i#+j) mod 2 = b"
42  by (unfold evnodd_def) blast
43
44lemma evnodd_subset: "evnodd(A, b) \<subseteq> A"
45  by (unfold evnodd_def) blast
46
47lemma Finite_evnodd: "Finite(X) ==> Finite(evnodd(X,b))"
48  by (rule lepoll_Finite, rule subset_imp_lepoll, rule evnodd_subset)
49
50lemma evnodd_Un: "evnodd(A \<union> B, b) = evnodd(A,b) \<union> evnodd(B,b)"
51  by (simp add: evnodd_def Collect_Un)
52
53lemma evnodd_Diff: "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"
54  by (simp add: evnodd_def Collect_Diff)
55
56lemma evnodd_cons [simp]:
57  "evnodd(cons(<i,j>,C), b) =
58    (if (i#+j) mod 2 = b then cons(<i,j>, evnodd(C,b)) else evnodd(C,b))"
59  by (simp add: evnodd_def Collect_cons)
60
61lemma evnodd_0 [simp]: "evnodd(0, b) = 0"
62  by (simp add: evnodd_def)
63
64
65subsection \<open>Dominoes\<close>
66
67lemma domino_Finite: "d \<in> domino ==> Finite(d)"
68  by (blast intro!: Finite_cons Finite_0 elim: domino.cases)
69
70lemma domino_singleton:
71    "[| d \<in> domino; b<2 |] ==> \<exists>i' j'. evnodd(d,b) = {<i',j'>}"
72  apply (erule domino.cases)
73   apply (rule_tac [2] k1 = "i#+j" in mod2_cases [THEN disjE])
74     apply (rule_tac k1 = "i#+j" in mod2_cases [THEN disjE])
75       apply (rule add_type | assumption)+
76      (*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
77      apply (auto simp add: mod_succ succ_neq_self dest: ltD)
78  done
79
80
81subsection \<open>Tilings\<close>
82
83text \<open>The union of two disjoint tilings is a tiling\<close>
84
85lemma tiling_UnI:
86    "t \<in> tiling(A) ==> u \<in> tiling(A) ==> t \<inter> u = 0 ==> t \<union> u \<in> tiling(A)"
87  apply (induct set: tiling)
88   apply (simp add: tiling.intros)
89  apply (simp add: Un_assoc subset_empty_iff [THEN iff_sym])
90  apply (blast intro: tiling.intros)
91  done
92
93lemma tiling_domino_Finite: "t \<in> tiling(domino) ==> Finite(t)"
94  apply (induct set: tiling)
95   apply (rule Finite_0)
96  apply (blast intro!: Finite_Un intro: domino_Finite)
97  done
98
99lemma tiling_domino_0_1: "t \<in> tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"
100  apply (induct set: tiling)
101   apply (simp add: evnodd_def)
102  apply (rule_tac b1 = 0 in domino_singleton [THEN exE])
103    prefer 2
104    apply simp
105   apply assumption
106  apply (rule_tac b1 = 1 in domino_singleton [THEN exE])
107    prefer 2
108    apply simp
109   apply assumption
110  apply safe
111  apply (subgoal_tac "\<forall>p b. p \<in> evnodd (a,b) \<longrightarrow> p\<notin>evnodd (t,b)")
112   apply (simp add: evnodd_Un Un_cons tiling_domino_Finite
113     evnodd_subset [THEN subset_Finite] Finite_imp_cardinal_cons)
114  apply (blast dest!: evnodd_subset [THEN subsetD] elim: equalityE)
115  done
116
117lemma dominoes_tile_row:
118    "[| i \<in> nat;  n \<in> nat |] ==> {i} * (n #+ n) \<in> tiling(domino)"
119  apply (induct_tac n)
120   apply (simp add: tiling.intros)
121  apply (simp add: Un_assoc [symmetric] Sigma_succ2)
122  apply (rule tiling.intros)
123    prefer 2 apply assumption
124   apply (rename_tac n')
125   apply (subgoal_tac (*seems the easiest way of turning one to the other*)
126     "{i}*{succ (n'#+n') } \<union> {i}*{n'#+n'} =
127       {<i,n'#+n'>, <i,succ (n'#+n') >}")
128    prefer 2 apply blast
129  apply (simp add: domino.horiz)
130  apply (blast elim: mem_irrefl mem_asym)
131  done
132
133lemma dominoes_tile_matrix:
134    "[| m \<in> nat;  n \<in> nat |] ==> m * (n #+ n) \<in> tiling(domino)"
135  apply (induct_tac m)
136   apply (simp add: tiling.intros)
137  apply (simp add: Sigma_succ1)
138  apply (blast intro: tiling_UnI dominoes_tile_row elim: mem_irrefl)
139  done
140
141lemma eq_lt_E: "[| x=y; x<y |] ==> P"
142  by auto
143
144theorem mutil_not_tiling: "[| m \<in> nat;  n \<in> nat;
145         t = (succ(m)#+succ(m))*(succ(n)#+succ(n));
146         t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |]
147      ==> t' \<notin> tiling(domino)"
148  apply (rule notI)
149  apply (drule tiling_domino_0_1)
150  apply (erule_tac x = "|A|" for A in eq_lt_E)
151  apply (subgoal_tac "t \<in> tiling (domino)")
152   prefer 2 (*Requires a small simpset that won't move the succ applications*)
153   apply (simp only: nat_succI add_type dominoes_tile_matrix)
154  apply (simp add: evnodd_Diff mod2_add_self mod2_succ_succ
155    tiling_domino_0_1 [symmetric])
156  apply (rule lt_trans)
157   apply (rule Finite_imp_cardinal_Diff,
158     simp add: tiling_domino_Finite Finite_evnodd Finite_Diff,
159     simp add: evnodd_iff nat_0_le [THEN ltD] mod2_add_self)+
160  done
161
162end
163