--- a/src/HOL/Induct/Mutil.ML Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(* Title: HOL/Induct/Mutil
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
-*)
-
-Addsimps (tiling.intrs @ domino.intrs);
-AddIs tiling.intrs;
-
-(** The union of two disjoint tilings is a tiling **)
-
-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;
-qed_spec_mp "tiling_UnI";
-
-AddIs [tiling_UnI];
-
-(*** Chess boards ***)
-
-Goalw [lessThan_def]
- "lessThan(Suc n) <*> B = ({n} <*> B) Un ((lessThan n) <*> B)";
-by Auto_tac;
-qed "Sigma_Suc1";
-
-Goalw [lessThan_def]
- "A <*> lessThan(Suc n) = (A <*> {n}) Un (A <*> (lessThan n))";
-by Auto_tac;
-qed "Sigma_Suc2";
-
-Addsimps [Sigma_Suc1, Sigma_Suc2];
-
-Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
-by Auto_tac;
-qed "sing_Times_lemma";
-
-Goal "{i} <*> lessThan(#2*n) : tiling domino";
-by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
-by (rtac tiling.Un 1);
-by (auto_tac (claset(), simpset() addsimps [sing_Times_lemma]));
-qed "dominoes_tile_row";
-
-AddSIs [dominoes_tile_row];
-
-Goal "(lessThan m) <*> lessThan(#2*n) : tiling domino";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "dominoes_tile_matrix";
-
-
-(*** "coloured" and Dominoes ***)
-
-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 "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);
-by Auto_tac;
-qed "domino_finite";
-Addsimps [domino_finite];
-
-
-(*** Tilings of dominoes ***)
-
-Goal "t:tiling domino ==> finite t";
-by (etac tiling.induct 1);
-by Auto_tac;
-qed "tiling_domino_finite";
-
-Addsimps [tiling_domino_finite, Int_Un_distrib, Diff_Int_distrib];
-
-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;
-(*this lemma tells us that both "inserts" are non-trivial*)
-by (subgoal_tac "ALL p C. C Int a = {p} --> p ~: t" 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "tiling_domino_0_1";
-
-(*Final argument is surprisingly complex*)
-Goal "[| t : 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)} - {(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 (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*)
-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);
-by Auto_tac;
-qed "mutil_not_tiling";
-