# HG changeset patch
# User paulson
# Date 954167153 -7200
# Node ID a24f7e5ee7effe6d886df3653bd5aa0a9fd78383
# Parent  b7c3f264f8acc4871e78ce097d7002f72c505dd1
simplified constant "colored"

diff -r b7c3f264f8ac -r a24f7e5ee7ef src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Sun Mar 26 22:31:11 2000 +0200
+++ b/src/HOL/Induct/Mutil.ML	Mon Mar 27 16:25:53 2000 +0200
@@ -6,7 +6,7 @@
 The Mutilated Chess Board Problem, formalized inductively
 *)
 
-Addsimps tiling.intrs;
+Addsimps (tiling.intrs @ domino.intrs);
 AddIs    tiling.intrs;
 
 (** The union of two disjoint tilings is a tiling **)
@@ -49,10 +49,9 @@
 
 Goal "{i} Times below(n+n) : tiling domino";
 by (induct_tac "n" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
+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, domino.horiz])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [sing_Times_lemma])));
 qed "dominoes_tile_row";
 
 AddSIs [dominoes_tile_row]; 
@@ -63,35 +62,16 @@
 qed "dominoes_tile_matrix";
 
 
-(*** Basic properties of colored ***)
-
-Goalw [colored_def] "finite X ==> finite(colored b X)";
-by Auto_tac;
-qed "finite_colored";
-
-Goalw [colored_def] "colored b (A Un B) = colored b A Un colored b B";
-by Auto_tac;
-qed "colored_Un";
-
-Goalw [colored_def] "colored b (A - B) = colored b A - colored b B";
-by Auto_tac;
-qed "colored_Diff";
-
-Goalw [colored_def] "colored b {} = {}";
-by Auto_tac;
-qed "colored_empty";
+(*** "colored" and Dominoes ***)
 
 Goalw [colored_def]
-    "colored b (insert (i,j) C) = \
-\      (if (i+j) mod 2 = b then insert (i,j) (colored b C) else colored b C)";
+    "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)";
 by Auto_tac;
 qed "colored_insert";
 
-Addsimps [finite_colored, colored_Un, colored_Diff, colored_empty, 
-	  colored_insert];
-
-
-(*** Dominoes ***)
+Addsimps [colored_insert];
 
 Goal "d:domino ==> finite d";
 by (etac domino.elim 1);
@@ -99,15 +79,12 @@
 qed "domino_finite";
 Addsimps [domino_finite];
 
-Goal "[| d:domino; b<2 |] ==> EX i j. colored b d = {(i,j)}";
+Goal "d:domino ==> (EX i j. colored 0 Int d = {(i,j)}) & \
+\                  (EX k l. colored 1 Int d = {(k,l)})";
 by (etac domino.elim 1);
 by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
-qed "domino_singleton";
+qed "domino_singletons";
 
-Goal "d:domino ==> (EX i j. colored 0 d = {(i,j)}) & \
-\                  (EX i' j'. colored 1 d = {(i',j')})";
-by (blast_tac (claset() addSIs [domino_singleton]) 1);
-qed "domino_singleton_01";
 
 (*** Tilings of dominoes ***)
 
@@ -116,26 +93,26 @@
 by Auto_tac;
 qed "tiling_domino_finite";
 
-Addsimps [tiling_domino_finite];
+Addsimps [tiling_domino_finite, Int_Un_distrib, Diff_Int_distrib];
 
-Goal "t: tiling domino ==> card(colored 0 t) = card(colored 1 t)";
+Goal "t: tiling domino ==> card(colored 0 Int t) = card(colored 1 Int t)";
 by (etac tiling.induct 1);
-by (dtac domino_singleton_01 2);
+by (dtac domino_singletons 2);
 by Auto_tac;
 (*this lemma tells us that both "inserts" are non-trivial*)
-by (subgoal_tac "ALL p b. p : colored b a --> p ~: colored b t" 1);
+by (subgoal_tac "ALL p C. C Int a = {p} --> p ~: t" 1);
 by (Asm_simp_tac 1);
-by (auto_tac (claset(), simpset() addsimps [colored_def]));
+by (blast_tac (claset() addEs [equalityE]) 1);
 qed "tiling_domino_0_1";
 
 (*Final argument is surprisingly complex*)
 Goal "[| t : tiling domino;       \
-\        (i+j) mod 2 = 0;  (i'+j') mod 2 = 0;  \
-\        {(i,j),(i',j')} <= t;  j' ~= j |]    \
-\     ==> (t - {(i,j)} - {(i',j')}) ~: tiling domino";
+\        (i+j) mod 2 = 0;  (k+l) mod 2 = 0;  \
+\        {(i,j),(k,l)} <= t;  l ~= j |]    \
+\     ==> (t - {(i,j)} - {(k,l)}) ~: tiling domino";
 by (rtac notI 1);
-by (subgoal_tac "card (colored 0 (t - {(i,j)} - {(i',j')})) < \
-\                card (colored 1 (t - {(i,j)} - {(i',j')}))" 1);
+by (subgoal_tac "card (colored 0 Int (t - {(i,j)} - {(k,l)})) < \
+\                card (colored 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);
diff -r b7c3f264f8ac -r a24f7e5ee7ef src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Sun Mar 26 22:31:11 2000 +0200
+++ b/src/HOL/Induct/Mutil.thy	Mon Mar 27 16:25:53 2000 +0200
@@ -24,9 +24,9 @@
 
 constdefs
   below   :: "nat => nat set"
-   "below n    == {i. i<n}"
+   "below n   == {i. i<n}"
   
-  colored  :: "[nat, (nat*nat)set] => (nat*nat)set"
-   "colored b A == A Int {(i,j). (i+j) mod 2 = b}"
+  colored  :: "nat => (nat*nat)set"
+   "colored b == {(i,j). (i+j) mod 2 = b}"
 
 end