src/HOL/Induct/Mutil.ML
changeset 3423 3684a4420a67
parent 3414 804c8a178a7f
child 3718 d78cf498a88c
equal deleted inserted replaced
3422:16ae2c20801c 3423:3684a4420a67
     1 (*  Title:      HOL/ex/Mutil
     1 (*  Title:      HOL/Induct/Mutil
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     4     Copyright   1996  University of Cambridge
     5 
     5 
     6 The Mutilated Chess Board Problem, formalized inductively
     6 The Mutilated Chess Board Problem, formalized inductively
    21 qed_spec_mp "tiling_UnI";
    21 qed_spec_mp "tiling_UnI";
    22 
    22 
    23 
    23 
    24 (*** Chess boards ***)
    24 (*** Chess boards ***)
    25 
    25 
    26 val [below_0, below_Suc] = nat_recs below_def;
    26 goalw thy [below_def] "(i: below k) = (i<k)";
    27 Addsimps [below_0, below_Suc];
    27 by (Blast_tac 1);
       
    28 qed "below_less_iff";
       
    29 AddIffs [below_less_iff];
    28 
    30 
    29 goal thy "ALL i. (i: below k) = (i<k)";
    31 goalw thy [below_def] "below 0 = {}";
    30 by (nat_ind_tac "k" 1);
    32 by (Simp_tac 1);
    31 by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
    33 qed "below_0";
    32 by (Blast_tac 1);
    34 Addsimps [below_0];
    33 qed_spec_mp "below_less_iff";
       
    34 
    35 
    35 Addsimps [below_less_iff];
    36 goalw thy [below_def]
    36 
    37     "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
    37 goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
    38 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    38 by (Simp_tac 1);
       
    39 by (Blast_tac 1);
    39 by (Blast_tac 1);
    40 qed "Sigma_Suc1";
    40 qed "Sigma_Suc1";
    41 
    41 
    42 goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
    42 goalw thy [below_def]
    43 by (Simp_tac 1);
    43     "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
       
    44 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    44 by (Blast_tac 1);
    45 by (Blast_tac 1);
    45 qed "Sigma_Suc2";
    46 qed "Sigma_Suc2";
    46 
    47 
    47 (*Deletion is essential to allow use of Sigma_Suc1,2*)
    48 goal thy "{i} Times below(n+n) : tiling domino";
    48 Delsimps [below_Suc];
       
    49 
       
    50 goal thy "{i} Times below(n + n) : tiling domino";
       
    51 by (nat_ind_tac "n" 1);
    49 by (nat_ind_tac "n" 1);
    52 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
    50 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
    53 by (resolve_tac tiling.intrs 1);
    51 by (resolve_tac tiling.intrs 1);
    54 by (assume_tac 2);
    52 by (assume_tac 2);
    55 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
    53 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
    56     "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
    54     "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
    57 \    {(i, n+n), (i, Suc(n+n))}" 1);
    55 \    {(i, n+n), (i, Suc(n+n))}" 1);
    58 by (Blast_tac 2);
    56 by (Blast_tac 2);
    59 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
    57 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
    60 by (blast_tac (!claset addEs  [less_irrefl, less_asym]
    58 by (Auto_tac());
    61                        addSDs [below_less_iff RS iffD1]) 1);
       
    62 qed "dominoes_tile_row";
    59 qed "dominoes_tile_row";
    63 
    60 
    64 goal thy "(below m) Times below(n + n) : tiling domino";
    61 goal thy "(below m) Times below(n+n) : tiling domino";
    65 by (nat_ind_tac "m" 1);
    62 by (nat_ind_tac "m" 1);
    66 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
    63 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
    67 by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
    64 by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
    68                       addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
    65                        addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
    69 qed "dominoes_tile_matrix";
    66 qed "dominoes_tile_matrix";
    70 
    67 
    71 
    68 
    72 (*** Basic properties of evnodd ***)
    69 (*** Basic properties of evnodd ***)
    73 
    70 
    94 by (Simp_tac 1);
    91 by (Simp_tac 1);
    95 qed "evnodd_empty";
    92 qed "evnodd_empty";
    96 
    93 
    97 goalw thy [evnodd_def]
    94 goalw thy [evnodd_def]
    98     "evnodd (insert (i,j) C) b = \
    95     "evnodd (insert (i,j) C) b = \
    99 \    (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
    96 \      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
   100 by (asm_full_simp_tac (!simpset addsimps [evnodd_def] 
    97 by (simp_tac (!simpset setloop (split_tac [expand_if] THEN' Step_tac)) 1);
   101              setloop (split_tac [expand_if] THEN' Step_tac)) 1);
       
   102 qed "evnodd_insert";
    98 qed "evnodd_insert";
       
    99 
       
   100 Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert];
   103 
   101 
   104 
   102 
   105 (*** Dominoes ***)
   103 (*** Dominoes ***)
   106 
   104 
   107 goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
   105 goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
   108 by (eresolve_tac [domino.elim] 1);
   106 by (eresolve_tac [domino.elim] 1);
   109 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
   107 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
   110 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
   108 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
   111 by (REPEAT_FIRST assume_tac);
   109 by (REPEAT_FIRST assume_tac);
   112 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
   110 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
   113 by (REPEAT (asm_full_simp_tac (!simpset addsimps
   111 by (REPEAT (asm_full_simp_tac (!simpset addsimps [less_Suc_eq, mod_Suc] 
   114                           [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
       
   115                           setloop split_tac [expand_if]) 1
   112                           setloop split_tac [expand_if]) 1
   116            THEN Blast_tac 1));
   113            THEN Blast_tac 1));
   117 qed "domino_singleton";
   114 qed "domino_singleton";
   118 
   115 
   119 goal thy "!!d. d:domino ==> finite d";
   116 goal thy "!!d. d:domino ==> finite d";
   136 by (Simp_tac 2 THEN assume_tac 1);
   133 by (Simp_tac 2 THEN assume_tac 1);
   137 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
   134 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
   138 by (Simp_tac 2 THEN assume_tac 1);
   135 by (Simp_tac 2 THEN assume_tac 1);
   139 by (Step_tac 1);
   136 by (Step_tac 1);
   140 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
   137 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
   141 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
   138 by (asm_simp_tac (!simpset addsimps [tiling_domino_finite]) 1);
   142                                      tiling_domino_finite,
       
   143                                      evnodd_subset RS finite_subset]) 1);
       
   144 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
   139 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
   145 qed "tiling_domino_0_1";
   140 qed "tiling_domino_0_1";
   146 
   141 
   147 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
   142 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
   148 \                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
   143 \                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
   155 (*Requires a small simpset that won't move the Suc applications*)
   150 (*Requires a small simpset that won't move the Suc applications*)
   156 by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
   151 by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
   157 by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
   152 by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
   158 by (asm_simp_tac (!simpset addsimps add_ac) 2);
   153 by (asm_simp_tac (!simpset addsimps add_ac) 2);
   159 by (asm_full_simp_tac 
   154 by (asm_full_simp_tac 
   160     (!simpset addsimps [evnodd_Diff, evnodd_insert, evnodd_empty, 
   155     (!simpset addsimps [mod_less, tiling_domino_0_1 RS sym]) 1);
   161                         mod_less, tiling_domino_0_1 RS sym]) 1);
       
   162 by (rtac less_trans 1);
   156 by (rtac less_trans 1);
   163 by (REPEAT
   157 by (REPEAT
   164     (rtac card_Diff 1 
   158     (rtac card_Diff 1 
   165      THEN
   159      THEN asm_simp_tac (!simpset addsimps [tiling_domino_finite]) 1 
   166      asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1 
   160      THEN asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
   167      THEN
       
   168      asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
       
   169 qed "mutil_not_tiling";
   161 qed "mutil_not_tiling";
   170