--- a/src/HOL/Induct/Mutil.thy Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Mutil.thy Sat Feb 03 17:40:16 2001 +0100
@@ -1,29 +1,150 @@
-(* Title: HOL/Induct/Mutil
+(* Title: HOL/Induct/Mutil.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
- Originator is Max Black, according to J A Robinson.
- Popularized as the Mutilated Checkerboard Problem by J McCarthy
*)
-Mutil = Main +
+header {* The Mutilated Chess Board Problem *}
+
+theory Mutil = Main:
-consts tiling :: "'a set set => 'a set set"
+text {*
+ The Mutilated Chess Board Problem, formalized inductively.
+
+ Originator is Max Black, according to J A Robinson. Popularized as
+ the Mutilated Checkerboard Problem by J McCarthy.
+*}
+
+consts tiling :: "'a set set => 'a set set"
inductive "tiling A"
- intrs
- empty "{} : tiling A"
- Un "[| a: A; t: tiling A; a Int t = {} |] ==> a Un t : tiling A"
+ intros [simp, intro]
+ empty: "{} \<in> tiling A"
+ Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
-consts domino :: "(nat*nat)set set"
+consts domino :: "(nat \<times> nat) set set"
inductive domino
- intrs
- horiz "{(i, j), (i, Suc j)} : domino"
- vertl "{(i, j), (Suc i, j)} : domino"
+ intros [simp]
+ horiz: "{(i, j), (i, Suc j)} \<in> domino"
+ vertl: "{(i, j), (Suc i, j)} \<in> domino"
constdefs
- coloured :: "nat => (nat*nat)set"
- "coloured b == {(i,j). (i+j) mod #2 = b}"
+ coloured :: "nat => (nat \<times> nat) set"
+ "coloured b == {(i, j). (i + j) mod #2 = b}"
+
+
+text {* \medskip The union of two disjoint tilings is a tiling *}
+
+lemma tiling_UnI [rule_format, intro]:
+ "t \<in> tiling A ==> u \<in> tiling A --> t \<inter> u = {} --> t \<union> u \<in> tiling A"
+ apply (erule tiling.induct)
+ prefer 2
+ apply (simp add: Un_assoc)
+ apply auto
+ done
+
+
+text {* \medskip Chess boards *}
+
+lemma Sigma_Suc1 [simp]:
+ "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
+ apply (unfold lessThan_def)
+ apply auto
+ done
+
+lemma Sigma_Suc2 [simp]:
+ "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
+ apply (unfold lessThan_def)
+ apply auto
+ done
+
+lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
+ apply auto
+ done
+
+lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (#2 * n) \<in> tiling domino"
+ apply (induct n)
+ apply (simp_all add: Un_assoc [symmetric])
+ apply (rule tiling.Un)
+ apply (auto simp add: sing_Times_lemma)
+ done
+
+lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (#2 * n) \<in> tiling domino"
+ apply (induct m)
+ apply auto
+ done
+
+
+text {* \medskip @{term coloured} and Dominoes *}
+
+lemma coloured_insert [simp]:
+ "coloured b \<inter> (insert (i, j) t) =
+ (if (i + j) mod #2 = b then insert (i, j) (coloured b \<inter> t)
+ else coloured b \<inter> t)"
+ apply (unfold coloured_def)
+ apply auto
+ done
+
+lemma domino_singletons:
+ "d \<in> domino ==>
+ (\<exists>i j. coloured 0 \<inter> d = {(i, j)}) \<and>
+ (\<exists>m n. coloured 1 \<inter> d = {(m, n)})"
+ apply (erule domino.cases)
+ apply (auto simp add: mod_Suc)
+ done
+
+lemma domino_finite [simp]: "d \<in> domino ==> finite d"
+ apply (erule domino.cases)
+ apply auto
+ done
+
+
+text {* \medskip Tilings of dominoes *}
+
+lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
+ apply (erule tiling.induct)
+ apply auto
+ done
+
+declare
+ Int_Un_distrib [simp]
+ Diff_Int_distrib [simp]
+
+lemma tiling_domino_0_1:
+ "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
+ apply (erule tiling.induct)
+ apply (drule_tac [2] domino_singletons)
+ apply auto
+ apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
+ -- {* this lemma tells us that both ``inserts'' are non-trivial *}
+ apply (simp (no_asm_simp))
+ apply blast
+ done
+
+
+text {* \medskip Final argument is surprisingly complex *}
+
+theorem gen_mutil_not_tiling:
+ "t \<in> tiling domino ==>
+ (i + j) mod #2 = 0 ==> (m + n) mod #2 = 0 ==>
+ {(i, j), (m, n)} \<subseteq> t
+ ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
+ apply (rule notI)
+ apply (subgoal_tac
+ "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
+ card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
+ apply (force simp only: tiling_domino_0_1)
+ apply (simp add: tiling_domino_0_1 [symmetric])
+ apply (simp add: coloured_def card_Diff2_less)
+ done
+
+text {* Apply the general theorem to the well-known case *}
+
+theorem mutil_not_tiling:
+ "t = lessThan (#2 * Suc m) \<times> lessThan (#2 * Suc n)
+ ==> t - {(0, 0)} - {(Suc (#2 * m), Suc (#2 * n))} \<notin> tiling domino"
+ apply (rule gen_mutil_not_tiling)
+ apply (blast intro!: dominoes_tile_matrix)
+ apply auto
+ done
end