src/HOL/Induct/Mutil.ML
author paulson
Wed, 07 May 1997 12:50:26 +0200
changeset 3120 c58423c20740
child 3357 c224dddc5f71
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Mutil
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
The Mutilated Chess Board Problem, formalized inductively
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
open Mutil;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
Addsimps tiling.intrs;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
(** The union of two disjoint tilings is a tiling **)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
goal thy "!!t. t: tiling A ==> \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
\              u: tiling A --> t <= Compl u --> t Un u : tiling A";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
by (etac tiling.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
by (Simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
by (simp_tac (!simpset addsimps [Un_assoc]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
by (blast_tac (!claset addIs tiling.intrs) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
qed_spec_mp "tiling_UnI";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
(*** Chess boards ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
val [below_0, below_Suc] = nat_recs below_def;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
Addsimps [below_0, below_Suc];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
goal thy "ALL i. (i: below k) = (i<k)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
by (nat_ind_tac "k" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
qed_spec_mp "below_less_iff";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
Addsimps [below_less_iff];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
by (Simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
qed "Sigma_Suc1";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
by (Simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
qed "Sigma_Suc2";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
(*Deletion is essential to allow use of Sigma_Suc1,2*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
Delsimps [below_Suc];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
goal thy "{i} Times below(n + n) : tiling domino";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
by (nat_ind_tac "n" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
by (resolve_tac tiling.intrs 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
by (assume_tac 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
by (subgoal_tac    (*seems the easiest way of turning one to the other*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
\    {(i, n+n), (i, Suc(n+n))}" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    58
by (Blast_tac 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
by (blast_tac (!claset addEs  [less_irrefl, less_asym]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
                       addSDs [below_less_iff RS iffD1]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
qed "dominoes_tile_row";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    64
goal thy "(below m) Times below(n + n) : tiling domino";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    65
by (nat_ind_tac "m" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    68
                      addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
qed "dominoes_tile_matrix";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    70
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    71
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    72
(*** Basic properties of evnodd ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    73
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    74
goalw thy [evnodd_def] "(i,j): evnodd A b = ((i,j): A  &  (i+j) mod 2 = b)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    75
by (Simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    76
qed "evnodd_iff";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    77
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
goalw thy [evnodd_def] "evnodd A b <= A";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    79
by (rtac Int_lower1 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    80
qed "evnodd_subset";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    81
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    82
(* finite X ==> finite(evnodd X b) *)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    83
bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    84
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    85
goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    86
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    87
qed "evnodd_Un";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    88
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    89
goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    90
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    91
qed "evnodd_Diff";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    92
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    93
goalw thy [evnodd_def] "evnodd {} b = {}";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    94
by (Simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    95
qed "evnodd_empty";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    96
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    97
goalw thy [evnodd_def]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    98
    "evnodd (insert (i,j) C) b = \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    99
\    (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   100
by (asm_full_simp_tac (!simpset addsimps [evnodd_def] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   101
             setloop (split_tac [expand_if] THEN' Step_tac)) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   102
qed "evnodd_insert";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   103
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   104
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   105
(*** Dominoes ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   106
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   107
goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   108
by (eresolve_tac [domino.elim] 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   109
by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   110
by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   111
by (REPEAT_FIRST assume_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   112
(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   113
by (REPEAT (asm_full_simp_tac (!simpset addsimps
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   114
                          [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   115
                          setloop split_tac [expand_if]) 1
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   116
           THEN Blast_tac 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   117
qed "domino_singleton";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   118
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   119
goal thy "!!d. d:domino ==> finite d";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   120
by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   121
                      addSEs [domino.elim]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   122
qed "domino_finite";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   123
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   124
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   125
(*** Tilings of dominoes ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   126
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   127
goal thy "!!t. t:tiling domino ==> finite t";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   128
by (eresolve_tac [tiling.induct] 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   129
by (rtac finite_emptyI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   130
by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   131
qed "tiling_domino_finite";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   132
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   133
goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   134
by (eresolve_tac [tiling.induct] 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   135
by (simp_tac (!simpset addsimps [evnodd_def]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   136
by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   137
by (Simp_tac 2 THEN assume_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   138
by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   139
by (Simp_tac 2 THEN assume_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   140
by (Step_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   141
by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   142
by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   143
                                     tiling_domino_finite,
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   144
                                     evnodd_subset RS finite_subset,
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   145
                                     card_insert_disjoint]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   146
by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   147
qed "tiling_domino_0_1";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   148
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   149
goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   150
\                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   151
\                |] ==> t' ~: tiling domino";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   152
by (rtac notI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   153
by (dtac tiling_domino_0_1 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   154
by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   155
by (Asm_full_simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   156
by (subgoal_tac "t : tiling domino" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   157
(*Requires a small simpset that won't move the Suc applications*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   158
by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   159
by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   160
by (asm_simp_tac (!simpset addsimps add_ac) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   161
by (asm_full_simp_tac 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   162
    (!simpset addsimps [evnodd_Diff, evnodd_insert, evnodd_empty, 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   163
                        mod_less, tiling_domino_0_1 RS sym]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   164
by (rtac less_trans 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   165
by (REPEAT
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   166
    (rtac card_Diff 1 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   167
     THEN
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   168
     asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   169
     THEN
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   170
     asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   171
qed "mutil_not_tiling";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   172