# HG changeset patch
# User paulson
# Date 952622838 -3600
# Node ID 86b04d47b8535ffad4b9632a906855985347f90e
# Parent  f1c80ed70f48b38a81c0ce37d716631d3f742b82
nicely tarted up Mutil

diff -r f1c80ed70f48 -r 86b04d47b853 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Thu Mar 09 17:27:54 2000 +0100
+++ b/src/HOL/Induct/Mutil.ML	Thu Mar 09 18:27:18 2000 +0100
@@ -7,26 +7,27 @@
 *)
 
 Addsimps tiling.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";
+Goal "t: tiling A ==> u: tiling A --> t <= -u --> t Un u : tiling A";
 by (etac tiling.induct 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [Un_assoc]) 1);
-by (blast_tac (claset() addIs tiling.intrs) 1);
+by (simp_tac (simpset() addsimps [Un_assoc]) 2);
+by Auto_tac;
 qed_spec_mp "tiling_UnI";
 
+AddIs [tiling_UnI];
 
 (*** Chess boards ***)
 
 Goalw [below_def] "(i: below k) = (i<k)";
-by (Blast_tac 1);
+by Auto_tac;
 qed "below_less_iff";
 AddIffs [below_less_iff];
 
 Goalw [below_def] "below 0 = {}";
-by (Simp_tac 1);
+by Auto_tac;
 qed "below_0";
 Addsimps [below_0];
 
@@ -40,113 +41,113 @@
 by Auto_tac;
 qed "Sigma_Suc2";
 
+Addsimps [Sigma_Suc1, Sigma_Suc2];
+
+Goal "({i} Times {n}) Un ({i} Times {m}) = {(i,m), (i,n)}";
+by Auto_tac;
+qed "sing_Times_lemma";
+
 Goal "{i} Times below(n+n) : tiling domino";
 by (induct_tac "n" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2])));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
 by (resolve_tac tiling.intrs 1);
-by (assume_tac 2);
-by (subgoal_tac    (*seems the easiest way of turning one to the other*)
-    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
-\    {(i, n+n), (i, Suc(n+n))}" 1);
-by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
-by Auto_tac;
+by (ALLGOALS
+    (asm_simp_tac (simpset() addsimps [sing_Times_lemma, domino.horiz])));
 qed "dominoes_tile_row";
 
+AddSIs [dominoes_tile_row]; 
+
 Goal "(below m) Times below(n+n) : tiling domino";
 by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1])));
-by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row]
-                        addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
+by Auto_tac;
 qed "dominoes_tile_matrix";
 
 
-(*** Basic properties of evnodd ***)
-
-Goalw [evnodd_def] "(i,j): evnodd A b = ((i,j): A  &  (i+j) mod 2 = b)";
-by (Simp_tac 1);
-qed "evnodd_iff";
+(*** Basic properties of colored ***)
 
-Goalw [evnodd_def] "evnodd A b <= A";
-by (rtac Int_lower1 1);
-qed "evnodd_subset";
+Goalw [colored_def] "finite X ==> finite(colored b X)";
+by Auto_tac;
+qed "finite_colored";
 
-(* finite X ==> finite(evnodd X b) *)
-bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
+Goalw [colored_def] "colored b (A Un B) = colored b A Un colored b B";
+by Auto_tac;
+qed "colored_Un";
 
-Goalw [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
-by (Blast_tac 1);
-qed "evnodd_Un";
+Goalw [colored_def] "colored b (A - B) = colored b A - colored b B";
+by Auto_tac;
+qed "colored_Diff";
 
-Goalw [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
-by (Blast_tac 1);
-qed "evnodd_Diff";
+Goalw [colored_def] "colored b {} = {}";
+by Auto_tac;
+qed "colored_empty";
 
-Goalw [evnodd_def] "evnodd {} b = {}";
-by (Simp_tac 1);
-qed "evnodd_empty";
+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)";
+by Auto_tac;
+qed "colored_insert";
 
-Goalw [evnodd_def]
-    "evnodd (insert (i,j) C) b = \
-\      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
-by Auto_tac;
-qed "evnodd_insert";
-
-Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert];
+Addsimps [finite_colored, colored_Un, colored_Diff, colored_empty, 
+	  colored_insert];
 
 
 (*** Dominoes ***)
 
-Goal "[| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
-by (eresolve_tac [domino.elim] 1);
-by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
-by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
-by (REPEAT_FIRST assume_tac);
-(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
-by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, mod_Suc]));
+Goal "d:domino ==> finite d";
+by (etac domino.elim 1);
+by Auto_tac;
+qed "domino_finite";
+Addsimps [domino_finite];
+
+Goal "[| d:domino; b<2 |] ==> EX i j. colored b d = {(i,j)}";
+by (etac domino.elim 1);
+by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
 qed "domino_singleton";
 
-Goal "d:domino ==> finite d";
-by (blast_tac (claset() addSEs [domino.elim]) 1);
-qed "domino_finite";
-
+Goal "d:domino \
+\     ==> EX i j i' j'. colored 0 d = {(i,j)} & colored 1 d = {(i',j')}";
+by (blast_tac (claset() addDs [domino_singleton]) 1);
+qed "domino_singleton_01";
 
 (*** Tilings of dominoes ***)
 
 Goal "t:tiling domino ==> finite t";
 by (eresolve_tac [tiling.induct] 1);
-by (rtac Finites.emptyI 1);
-by (blast_tac (claset() addSIs [finite_UnI] addIs [domino_finite]) 1);
+by Auto_tac;
 qed "tiling_domino_finite";
 
-Goal "t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
+Addsimps [tiling_domino_finite];
+
+Goal "t: tiling domino ==> card(colored 0 t) = card(colored 1 t)";
 by (eresolve_tac [tiling.induct] 1);
-by (simp_tac (simpset() addsimps [evnodd_def]) 1);
-by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
+by (dtac domino_singleton_01 2);
 by Auto_tac;
-by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
-by Auto_tac;
-by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd t b" 1);
-by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1);
-by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] 
-                        addEs  [equalityE]) 1);
+(*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 (Asm_simp_tac 1);
+by (auto_tac (claset(), simpset() addsimps [colored_def]));
 qed "tiling_domino_0_1";
 
-(*Final argument is surprisingly complex.  Note the use of small simpsets
-  to avoid moving Sucs, etc.*)
-Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
-\        t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
-\     |] ==> t' ~: tiling domino";
+(*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";
 by (rtac notI 1);
-by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
-by (asm_full_simp_tac (HOL_ss addsimps [less_not_refl, tiling_domino_0_1]) 1);
-by (subgoal_tac "t : tiling domino" 1);
-by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
-by (asm_full_simp_tac (simpset() 
-		       addsimps [mod_less, tiling_domino_0_1 RS sym]) 1);
-(*Cardinality is smaller because of the two elements fewer*)
+by (subgoal_tac "card (colored 0 (t - {(i,j)} - {(i',j')})) < \
+\                card (colored 1 (t - {(i,j)} - {(i',j')}))" 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 (REPEAT
-    (rtac card_Diff1_less 1 
-     THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 
-     THEN asm_simp_tac (simpset() addsimps [mod_less, evnodd_iff]) 1));
+by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], 
+			 simpset() addsimps [colored_def])));
+qed "gen_mutil_not_tiling";
+
+(*Apply the general theorem to the well-known case*)
+Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n) |] \
+\     ==> t - {(0,0)} - {(Suc(m+m), Suc(n+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";
+
diff -r f1c80ed70f48 -r 86b04d47b853 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Thu Mar 09 17:27:54 2000 +0100
+++ b/src/HOL/Induct/Mutil.thy	Thu Mar 09 18:27:18 2000 +0100
@@ -10,23 +10,23 @@
 
 Mutil = Main +
 
+consts     tiling :: "'a set set => 'a set set"
+inductive "tiling A"
+  intrs
+    empty  "{} : tiling A"
+    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
+
 consts    domino :: "(nat*nat)set set"
 inductive domino
   intrs
     horiz  "{(i, j), (i, Suc j)} : domino"
     vertl  "{(i, j), (Suc i, j)} : domino"
 
-consts     tiling :: "'a set set => 'a set set"
-inductive "tiling A"
-  intrs
-    empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
-
 constdefs
   below   :: "nat => nat set"
    "below n    == {i. i<n}"
   
-  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
-   "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
+  colored  :: "[nat, (nat*nat)set] => (nat*nat)set"
+   "colored b A == A Int {(i,j). (i+j) mod 2 = b}"
 
 end