src/HOL/Induct/Mutil.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4387 31d5a5a191e8
child 4686 74a12e86b20b
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson@3423
     1
(*  Title:      HOL/Induct/Mutil
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120
     4
    Copyright   1996  University of Cambridge
paulson@3120
     5
paulson@3120
     6
The Mutilated Chess Board Problem, formalized inductively
paulson@3120
     7
*)
paulson@3120
     8
paulson@3120
     9
Addsimps tiling.intrs;
paulson@3120
    10
paulson@3120
    11
(** The union of two disjoint tilings is a tiling **)
paulson@3120
    12
paulson@3120
    13
goal thy "!!t. t: tiling A ==> \
paulson@3120
    14
\              u: tiling A --> t <= Compl u --> t Un u : tiling A";
paulson@3120
    15
by (etac tiling.induct 1);
paulson@3120
    16
by (Simp_tac 1);
wenzelm@4089
    17
by (simp_tac (simpset() addsimps [Un_assoc]) 1);
wenzelm@4089
    18
by (blast_tac (claset() addIs tiling.intrs) 1);
paulson@3120
    19
qed_spec_mp "tiling_UnI";
paulson@3120
    20
paulson@3120
    21
paulson@3120
    22
(*** Chess boards ***)
paulson@3120
    23
paulson@3423
    24
goalw thy [below_def] "(i: below k) = (i<k)";
paulson@3120
    25
by (Blast_tac 1);
paulson@3423
    26
qed "below_less_iff";
paulson@3423
    27
AddIffs [below_less_iff];
paulson@3120
    28
paulson@3423
    29
goalw thy [below_def] "below 0 = {}";
paulson@3423
    30
by (Simp_tac 1);
paulson@3423
    31
qed "below_0";
paulson@3423
    32
Addsimps [below_0];
paulson@3120
    33
paulson@3423
    34
goalw thy [below_def]
paulson@3423
    35
    "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
wenzelm@4089
    36
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
paulson@3120
    37
by (Blast_tac 1);
paulson@3120
    38
qed "Sigma_Suc1";
paulson@3120
    39
paulson@3423
    40
goalw thy [below_def]
paulson@3423
    41
    "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
wenzelm@4089
    42
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
paulson@3120
    43
by (Blast_tac 1);
paulson@3120
    44
qed "Sigma_Suc2";
paulson@3120
    45
paulson@3423
    46
goal thy "{i} Times below(n+n) : tiling domino";
paulson@3120
    47
by (nat_ind_tac "n" 1);
wenzelm@4089
    48
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2])));
paulson@3120
    49
by (resolve_tac tiling.intrs 1);
paulson@3120
    50
by (assume_tac 2);
paulson@3120
    51
by (subgoal_tac    (*seems the easiest way of turning one to the other*)
paulson@3120
    52
    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
paulson@3120
    53
\    {(i, n+n), (i, Suc(n+n))}" 1);
paulson@3120
    54
by (Blast_tac 2);
wenzelm@4089
    55
by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
paulson@4477
    56
by Auto_tac;
paulson@3120
    57
qed "dominoes_tile_row";
paulson@3120
    58
paulson@3423
    59
goal thy "(below m) Times below(n+n) : tiling domino";
paulson@3120
    60
by (nat_ind_tac "m" 1);
wenzelm@4089
    61
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1])));
wenzelm@4089
    62
by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row]
paulson@3423
    63
                       addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
paulson@3120
    64
qed "dominoes_tile_matrix";
paulson@3120
    65
paulson@3120
    66
paulson@3120
    67
(*** Basic properties of evnodd ***)
paulson@3120
    68
paulson@3120
    69
goalw thy [evnodd_def] "(i,j): evnodd A b = ((i,j): A  &  (i+j) mod 2 = b)";
paulson@3120
    70
by (Simp_tac 1);
paulson@3120
    71
qed "evnodd_iff";
paulson@3120
    72
paulson@3120
    73
goalw thy [evnodd_def] "evnodd A b <= A";
paulson@3120
    74
by (rtac Int_lower1 1);
paulson@3120
    75
qed "evnodd_subset";
paulson@3120
    76
paulson@3120
    77
(* finite X ==> finite(evnodd X b) *)
paulson@3120
    78
bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
paulson@3120
    79
paulson@3120
    80
goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
paulson@3120
    81
by (Blast_tac 1);
paulson@3120
    82
qed "evnodd_Un";
paulson@3120
    83
paulson@3120
    84
goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
paulson@3120
    85
by (Blast_tac 1);
paulson@3120
    86
qed "evnodd_Diff";
paulson@3120
    87
paulson@3120
    88
goalw thy [evnodd_def] "evnodd {} b = {}";
paulson@3120
    89
by (Simp_tac 1);
paulson@3120
    90
qed "evnodd_empty";
paulson@3120
    91
paulson@3120
    92
goalw thy [evnodd_def]
paulson@3120
    93
    "evnodd (insert (i,j) C) b = \
paulson@3423
    94
\      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
wenzelm@4089
    95
by (simp_tac (simpset() addsplits [expand_if]) 1);
paulson@3718
    96
by (Blast_tac 1);
paulson@3120
    97
qed "evnodd_insert";
paulson@3120
    98
paulson@3423
    99
Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert];
paulson@3423
   100
paulson@3120
   101
paulson@3120
   102
(*** Dominoes ***)
paulson@3120
   103
paulson@3120
   104
goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
paulson@3120
   105
by (eresolve_tac [domino.elim] 1);
paulson@3120
   106
by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
paulson@3120
   107
by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
paulson@3120
   108
by (REPEAT_FIRST assume_tac);
paulson@3120
   109
(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
wenzelm@4089
   110
by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc] 
nipkow@3919
   111
                          addsplits [expand_if]) 1
paulson@3120
   112
           THEN Blast_tac 1));
paulson@3120
   113
qed "domino_singleton";
paulson@3120
   114
paulson@3120
   115
goal thy "!!d. d:domino ==> finite d";
wenzelm@4089
   116
by (blast_tac (claset() addSEs [domino.elim]) 1);
paulson@3120
   117
qed "domino_finite";
paulson@3120
   118
paulson@3120
   119
paulson@3120
   120
(*** Tilings of dominoes ***)
paulson@3120
   121
paulson@3120
   122
goal thy "!!t. t:tiling domino ==> finite t";
paulson@3120
   123
by (eresolve_tac [tiling.induct] 1);
nipkow@3414
   124
by (rtac Finites.emptyI 1);
wenzelm@4089
   125
by (blast_tac (claset() addSIs [finite_UnI] addIs [domino_finite]) 1);
paulson@3120
   126
qed "tiling_domino_finite";
paulson@3120
   127
paulson@3120
   128
goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
paulson@3120
   129
by (eresolve_tac [tiling.induct] 1);
wenzelm@4089
   130
by (simp_tac (simpset() addsimps [evnodd_def]) 1);
paulson@3120
   131
by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
paulson@3120
   132
by (Simp_tac 2 THEN assume_tac 1);
paulson@3120
   133
by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
paulson@3120
   134
by (Simp_tac 2 THEN assume_tac 1);
paulson@3718
   135
by (Clarify_tac 1);
paulson@3120
   136
by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
wenzelm@4089
   137
by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1);
paulson@4387
   138
by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] 
paulson@4387
   139
                        addEs  [equalityE]) 1);
paulson@3120
   140
qed "tiling_domino_0_1";
paulson@3120
   141
paulson@4387
   142
(*Final argument is surprisingly complex.  Note the use of small simpsets
paulson@4387
   143
  to avoid moving Sucs, etc.*)
paulson@3120
   144
goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
paulson@3120
   145
\                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
paulson@3120
   146
\                |] ==> t' ~: tiling domino";
paulson@3120
   147
by (rtac notI 1);
paulson@3120
   148
by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
paulson@4387
   149
by (asm_full_simp_tac (HOL_ss addsimps [less_not_refl, tiling_domino_0_1]) 1);
paulson@3120
   150
by (subgoal_tac "t : tiling domino" 1);
paulson@3120
   151
by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
paulson@4387
   152
by (asm_full_simp_tac (simpset() 
paulson@4387
   153
		       addsimps [mod_less, tiling_domino_0_1 RS sym]) 1);
paulson@4387
   154
(*Cardinality is smaller because of the two elements fewer*)
paulson@3120
   155
by (rtac less_trans 1);
paulson@3120
   156
by (REPEAT
paulson@3120
   157
    (rtac card_Diff 1 
wenzelm@4089
   158
     THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 
wenzelm@4089
   159
     THEN asm_simp_tac (simpset() addsimps [mod_less, evnodd_iff]) 1));
paulson@3120
   160
qed "mutil_not_tiling";