src/HOL/Induct/Mutil.thy
changeset 11046 b5f5942781a0
parent 9930 c02d48a47ed1
child 11464 ddea204de5bc
     1.1 --- a/src/HOL/Induct/Mutil.thy	Sat Feb 03 15:22:57 2001 +0100
     1.2 +++ b/src/HOL/Induct/Mutil.thy	Sat Feb 03 17:40:16 2001 +0100
     1.3 @@ -1,29 +1,150 @@
     1.4 -(*  Title:      HOL/Induct/Mutil
     1.5 +(*  Title:      HOL/Induct/Mutil.thy
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1996  University of Cambridge
     1.9 -
    1.10 -The Mutilated Chess Board Problem, formalized inductively
    1.11 -  Originator is Max Black, according to J A Robinson.
    1.12 -  Popularized as the Mutilated Checkerboard Problem by J McCarthy
    1.13  *)
    1.14  
    1.15 -Mutil = Main +
    1.16 +header {* The Mutilated Chess Board Problem *}
    1.17 +
    1.18 +theory Mutil = Main:
    1.19  
    1.20 -consts     tiling :: "'a set set => 'a set set"
    1.21 +text {*
    1.22 +  The Mutilated Chess Board Problem, formalized inductively.
    1.23 +
    1.24 +  Originator is Max Black, according to J A Robinson.  Popularized as
    1.25 +  the Mutilated Checkerboard Problem by J McCarthy.
    1.26 +*}
    1.27 +
    1.28 +consts tiling :: "'a set set => 'a set set"
    1.29  inductive "tiling A"
    1.30 -  intrs
    1.31 -    empty  "{} : tiling A"
    1.32 -    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
    1.33 +  intros [simp, intro]
    1.34 +    empty: "{} \<in> tiling A"
    1.35 +    Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
    1.36  
    1.37 -consts    domino :: "(nat*nat)set set"
    1.38 +consts domino :: "(nat \<times> nat) set set"
    1.39  inductive domino
    1.40 -  intrs
    1.41 -    horiz  "{(i, j), (i, Suc j)} : domino"
    1.42 -    vertl  "{(i, j), (Suc i, j)} : domino"
    1.43 +  intros [simp]
    1.44 +    horiz: "{(i, j), (i, Suc j)} \<in> domino"
    1.45 +    vertl: "{(i, j), (Suc i, j)} \<in> domino"
    1.46  
    1.47  constdefs
    1.48 -  coloured  :: "nat => (nat*nat)set"
    1.49 -   "coloured b == {(i,j). (i+j) mod #2 = b}"
    1.50 +  coloured :: "nat => (nat \<times> nat) set"
    1.51 +   "coloured b == {(i, j). (i + j) mod #2 = b}"
    1.52 +
    1.53 +
    1.54 +text {* \medskip The union of two disjoint tilings is a tiling *}
    1.55 +
    1.56 +lemma tiling_UnI [rule_format, intro]:
    1.57 +  "t \<in> tiling A ==> u \<in> tiling A --> t \<inter> u = {} --> t \<union> u \<in> tiling A"
    1.58 +  apply (erule tiling.induct)
    1.59 +   prefer 2
    1.60 +   apply (simp add: Un_assoc)
    1.61 +  apply auto
    1.62 +  done
    1.63 +
    1.64 +
    1.65 +text {* \medskip Chess boards *}
    1.66 +
    1.67 +lemma Sigma_Suc1 [simp]:
    1.68 +  "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
    1.69 +  apply (unfold lessThan_def)
    1.70 +  apply auto
    1.71 +  done
    1.72 +
    1.73 +lemma Sigma_Suc2 [simp]:
    1.74 +  "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
    1.75 +  apply (unfold lessThan_def)
    1.76 +  apply auto
    1.77 +  done
    1.78 +
    1.79 +lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
    1.80 +  apply auto
    1.81 +  done
    1.82 +
    1.83 +lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (#2 * n) \<in> tiling domino"
    1.84 +  apply (induct n)
    1.85 +   apply (simp_all add: Un_assoc [symmetric])
    1.86 +  apply (rule tiling.Un)
    1.87 +    apply (auto simp add: sing_Times_lemma)
    1.88 +  done
    1.89 +
    1.90 +lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (#2 * n) \<in> tiling domino"
    1.91 +  apply (induct m)
    1.92 +   apply auto
    1.93 +  done
    1.94 +
    1.95 +
    1.96 +text {* \medskip @{term coloured} and Dominoes *}
    1.97 +
    1.98 +lemma coloured_insert [simp]:
    1.99 +  "coloured b \<inter> (insert (i, j) t) =
   1.100 +   (if (i + j) mod #2 = b then insert (i, j) (coloured b \<inter> t)
   1.101 +    else coloured b \<inter> t)"
   1.102 +  apply (unfold coloured_def)
   1.103 +  apply auto
   1.104 +  done
   1.105 +
   1.106 +lemma domino_singletons:
   1.107 +  "d \<in> domino ==>
   1.108 +    (\<exists>i j. coloured 0 \<inter> d = {(i, j)}) \<and>
   1.109 +    (\<exists>m n. coloured 1 \<inter> d = {(m, n)})"
   1.110 +  apply (erule domino.cases)
   1.111 +   apply (auto simp add: mod_Suc)
   1.112 +  done
   1.113 +
   1.114 +lemma domino_finite [simp]: "d \<in> domino ==> finite d"
   1.115 +  apply (erule domino.cases)
   1.116 +   apply auto
   1.117 +  done
   1.118 +
   1.119 +
   1.120 +text {* \medskip Tilings of dominoes *}
   1.121 +
   1.122 +lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
   1.123 +  apply (erule tiling.induct)
   1.124 +   apply auto
   1.125 +  done
   1.126 +
   1.127 +declare
   1.128 +  Int_Un_distrib [simp]
   1.129 +  Diff_Int_distrib [simp]
   1.130 +
   1.131 +lemma tiling_domino_0_1:
   1.132 +  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
   1.133 +  apply (erule tiling.induct)
   1.134 +   apply (drule_tac [2] domino_singletons)
   1.135 +   apply auto
   1.136 +  apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
   1.137 +    -- {* this lemma tells us that both ``inserts'' are non-trivial *}
   1.138 +   apply (simp (no_asm_simp))
   1.139 +  apply blast
   1.140 +  done
   1.141 +
   1.142 +
   1.143 +text {* \medskip Final argument is surprisingly complex *}
   1.144 +
   1.145 +theorem gen_mutil_not_tiling:
   1.146 +  "t \<in> tiling domino ==>
   1.147 +    (i + j) mod #2 = 0 ==> (m + n) mod #2 = 0 ==>
   1.148 +    {(i, j), (m, n)} \<subseteq> t
   1.149 +  ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
   1.150 +  apply (rule notI)
   1.151 +  apply (subgoal_tac
   1.152 +    "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
   1.153 +      card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
   1.154 +   apply (force simp only: tiling_domino_0_1)
   1.155 +  apply (simp add: tiling_domino_0_1 [symmetric])
   1.156 +  apply (simp add: coloured_def card_Diff2_less)
   1.157 +  done
   1.158 +
   1.159 +text {* Apply the general theorem to the well-known case *}
   1.160 +
   1.161 +theorem mutil_not_tiling:
   1.162 +  "t = lessThan (#2 * Suc m) \<times> lessThan (#2 * Suc n)
   1.163 +    ==> t - {(0, 0)} - {(Suc (#2 * m), Suc (#2 * n))} \<notin> tiling domino"
   1.164 +  apply (rule gen_mutil_not_tiling)
   1.165 +     apply (blast intro!: dominoes_tile_matrix)
   1.166 +    apply auto
   1.167 +  done
   1.168  
   1.169  end