# HG changeset patch
# User paulson
# Date 968747236 -7200
# Node ID c02d48a47ed185241e66df3aa305a792980b55ee
# Parent  75df69217b576a740ab47e8eaa28dd336e208304
tidying and updating for revised Mutilated Chess Board article

diff -r 75df69217b57 -r c02d48a47ed1 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Mon Sep 11 20:44:53 2000 +0200
+++ b/src/HOL/Induct/Mutil.ML	Tue Sep 12 10:27:16 2000 +0200
@@ -11,7 +11,7 @@
 
 (** The union of two disjoint tilings is a tiling **)
 
-Goal "t: tiling A ==> u: tiling A --> t <= -u --> t Un u : tiling A";
+Goal "t: tiling A ==> u: tiling A --> t Int u = {} --> t Un u : tiling A";
 by (etac tiling.induct 1);
 by (simp_tac (simpset() addsimps [Un_assoc]) 2);
 by Auto_tac;
@@ -41,7 +41,7 @@
 by (induct_tac "n" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
 by (rtac tiling.Un 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [sing_Times_lemma])));
+by (auto_tac (claset(), simpset() addsimps [sing_Times_lemma]));  
 qed "dominoes_tile_row";
 
 AddSIs [dominoes_tile_row]; 
@@ -52,16 +52,16 @@
 qed "dominoes_tile_matrix";
 
 
-(*** "colored" and Dominoes ***)
+(*** "coloured" and Dominoes ***)
 
-Goalw [colored_def]
-    "colored b Int (insert (i,j) C) = \
-\      (if (i+j) mod #2 = b then insert (i,j) (colored b Int C) \
-\                          else colored b Int C)";
+Goalw [coloured_def]
+    "coloured b Int (insert (i,j) t) = \
+\      (if (i+j) mod #2 = b then insert (i,j) (coloured b Int t) \
+\                           else coloured b Int t)";
 by Auto_tac;
-qed "colored_insert";
+qed "coloured_insert";
 
-Addsimps [colored_insert];
+Addsimps [coloured_insert];
 
 Goal "d:domino ==> finite d";
 by (etac domino.elim 1);
@@ -69,8 +69,8 @@
 qed "domino_finite";
 Addsimps [domino_finite];
 
-Goal "d:domino ==> (EX i j. colored 0 Int d = {(i,j)}) & \
-\                  (EX k l. colored 1 Int d = {(k,l)})";
+Goal "d:domino ==> (EX i j. coloured 0 Int d = {(i,j)}) & \
+\                  (EX k l. coloured 1 Int d = {(k,l)})";
 by (etac domino.elim 1);
 by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
 qed "domino_singletons";
@@ -85,7 +85,7 @@
 
 Addsimps [tiling_domino_finite, Int_Un_distrib, Diff_Int_distrib];
 
-Goal "t: tiling domino ==> card(colored 0 Int t) = card(colored 1 Int t)";
+Goal "t: tiling domino ==> card(coloured 0 Int t) = card(coloured 1 Int t)";
 by (etac tiling.induct 1);
 by (dtac domino_singletons 2);
 by Auto_tac;
@@ -101,17 +101,17 @@
 \        {(i,j),(k,l)} <= t;  l ~= j |]    \
 \     ==> (t - {(i,j)} - {(k,l)}) ~: tiling domino";
 by (rtac notI 1);
-by (subgoal_tac "card (colored 0 Int (t - {(i,j)} - {(k,l)})) < \
-\                card (colored 1 Int (t - {(i,j)} - {(k,l)}))" 1);
+by (subgoal_tac "card (coloured 0 Int (t - {(i,j)} - {(k,l)})) < \
+\                card (coloured 1 Int (t - {(i,j)} - {(k,l)}))" 1);
 by (force_tac (claset(), HOL_ss addsimps [tiling_domino_0_1]) 1);
 by (asm_simp_tac (simpset() addsimps [tiling_domino_0_1 RS sym]) 1);
 by (rtac less_trans 1);
 by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], 
-			 simpset() addsimps [colored_def])));
+			 simpset() addsimps [coloured_def])));
 qed "gen_mutil_not_tiling";
 
 (*Apply the general theorem to the well-known case*)
-Goal "[| t = lessThan(#2 * Suc m) <*> lessThan(#2 * Suc n) |] \
+Goal "t = lessThan(#2 * Suc m) <*> lessThan(#2 * Suc n) \
 \     ==> t - {(0,0)} - {(Suc(#2*m), Suc(#2*n))} ~: tiling domino";
 by (rtac gen_mutil_not_tiling 1);
 by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1);
diff -r 75df69217b57 -r c02d48a47ed1 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Mon Sep 11 20:44:53 2000 +0200
+++ b/src/HOL/Induct/Mutil.thy	Tue Sep 12 10:27:16 2000 +0200
@@ -14,7 +14,7 @@
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
+    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
 
 consts    domino :: "(nat*nat)set set"
 inductive domino
@@ -23,7 +23,7 @@
     vertl  "{(i, j), (Suc i, j)} : domino"
 
 constdefs
-  colored  :: "nat => (nat*nat)set"
-   "colored b == {(i,j). (i+j) mod #2 = b}"
+  coloured  :: "nat => (nat*nat)set"
+   "coloured b == {(i,j). (i+j) mod #2 = b}"
 
 end