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