# HG changeset patch
# User paulson
# Date 973272837 -3600
# Node ID d943898cc3a995af111d04957b53a24b4f963c24
# Parent  d72638f2b78e6d74fbcaa9ace33840062b2a7427
new lemma card_Diff2_less for mulilated chess board

diff -r d72638f2b78e -r d943898cc3a9 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Nov 03 17:57:00 2000 +0100
+++ b/src/HOL/Finite.ML	Fri Nov 03 18:33:57 2000 +0100
@@ -425,6 +425,13 @@
 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
 qed "card_Diff1_less";
 
+Goal "[| finite A; x: A; y: A |] ==> card(A-{x}-{y}) < card A"; 
+by (case_tac "x=y" 1);
+by (asm_simp_tac (simpset() addsimps [card_Diff1_less]) 1);
+by (rtac less_trans 1);
+by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], simpset())));
+qed "card_Diff2_less";
+
 Goal "finite A ==> card(A-{x}) <= card A";
 by (case_tac "x: A" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le])));
diff -r d72638f2b78e -r d943898cc3a9 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Fri Nov 03 17:57:00 2000 +0100
+++ b/src/HOL/Induct/Mutil.ML	Fri Nov 03 18:33:57 2000 +0100
@@ -60,8 +60,13 @@
 \                           else coloured b Int t)";
 by Auto_tac;
 qed "coloured_insert";
+Addsimps [coloured_insert];
 
-Addsimps [coloured_insert];
+Goal "d:domino ==> (EX i j. coloured 0 Int d = {(i,j)}) & \
+\                  (EX m n. coloured 1 Int d = {(m,n)})";
+by (etac domino.elim 1);
+by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
+qed "domino_singletons";
 
 Goal "d:domino ==> finite d";
 by (etac domino.elim 1);
@@ -69,12 +74,6 @@
 qed "domino_finite";
 Addsimps [domino_finite];
 
-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";
-
 
 (*** Tilings of dominoes ***)
 
@@ -97,17 +96,15 @@
 
 (*Final argument is surprisingly complex*)
 Goal "[| t : 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";
+\        (i+j) mod #2 = 0;  (m+n) mod #2 = 0;  \
+\        {(i,j),(m,n)} <= t |]    \
+\     ==> (t - {(i,j)} - {(m,n)}) ~: tiling domino";
 by (rtac notI 1);
-by (subgoal_tac "card (coloured 0 Int (t - {(i,j)} - {(k,l)})) < \
-\                card (coloured 1 Int (t - {(i,j)} - {(k,l)}))" 1);
+by (subgoal_tac "card (coloured 0 Int (t - {(i,j)} - {(m,n)})) < \
+\                card (coloured 1 Int (t - {(i,j)} - {(m,n)}))" 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 [coloured_def])));
+by (asm_full_simp_tac (simpset() addsimps [coloured_def, card_Diff2_less]) 1); 
 qed "gen_mutil_not_tiling";
 
 (*Apply the general theorem to the well-known case*)