author  wenzelm 
Mon, 22 Jun 1998 17:26:46 +0200  
changeset 5069  3ea049f7979d 
parent 4686  74a12e86b20b 
child 5143  b94cd208f073 
permissions  rwrr 
3423  1 
(* Title: HOL/Induct/Mutil 
3120
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 
Addsimps tiling.intrs; 
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 
(** The union of two disjoint tilings is a tiling **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 

5069  13 
Goal "!!t. t: tiling A ==> \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
\ 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

15 
by (etac tiling.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
by (Simp_tac 1); 
4089  17 
by (simp_tac (simpset() addsimps [Un_assoc]) 1); 
18 
by (blast_tac (claset() addIs tiling.intrs) 1); 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 
qed_spec_mp "tiling_UnI"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
(*** Chess boards ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 

5069  24 
Goalw [below_def] "(i: below k) = (i<k)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
by (Blast_tac 1); 
3423  26 
qed "below_less_iff"; 
27 
AddIffs [below_less_iff]; 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 

5069  29 
Goalw [below_def] "below 0 = {}"; 
3423  30 
by (Simp_tac 1); 
31 
qed "below_0"; 

32 
Addsimps [below_0]; 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 

5069  34 
Goalw [below_def] 
3423  35 
"below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; 
4089  36 
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
qed "Sigma_Suc1"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 

5069  40 
Goalw [below_def] 
3423  41 
"A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; 
4089  42 
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
qed "Sigma_Suc2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 

5069  46 
Goal "{i} Times below(n+n) : tiling domino"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
by (nat_ind_tac "n" 1); 
4089  48 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

49 
by (resolve_tac tiling.intrs 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 
by (assume_tac 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
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

52 
"({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 
\ {(i, n+n), (i, Suc(n+n))}" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 
by (Blast_tac 2); 
4089  55 
by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4387
diff
changeset

56 
by Auto_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 
qed "dominoes_tile_row"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

58 

5069  59 
Goal "(below m) Times below(n+n) : tiling domino"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 
by (nat_ind_tac "m" 1); 
4089  61 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1]))); 
62 
by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row] 

3423  63 
addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

64 
qed "dominoes_tile_matrix"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

65 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

66 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 
(*** Basic properties of evnodd ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 

5069  69 
Goalw [evnodd_def] "(i,j): evnodd A b = ((i,j): A & (i+j) mod 2 = b)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

70 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

71 
qed "evnodd_iff"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

72 

5069  73 
Goalw [evnodd_def] "evnodd A b <= A"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
by (rtac Int_lower1 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 
qed "evnodd_subset"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

77 
(* finite X ==> finite(evnodd X b) *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 
bind_thm("finite_evnodd", evnodd_subset RS finite_subset); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

79 

5069  80 
Goalw [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

81 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
qed "evnodd_Un"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 

5069  84 
Goalw [evnodd_def] "evnodd (A  B) b = evnodd A b  evnodd B b"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

85 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

86 
qed "evnodd_Diff"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

87 

5069  88 
Goalw [evnodd_def] "evnodd {} b = {}"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

89 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

90 
qed "evnodd_empty"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

91 

5069  92 
Goalw [evnodd_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

93 
"evnodd (insert (i,j) C) b = \ 
3423  94 
\ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)"; 
4686  95 
by (Simp_tac 1); 
3718  96 
by (Blast_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

97 
qed "evnodd_insert"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

98 

3423  99 
Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert]; 
100 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

101 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

102 
(*** Dominoes ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

103 

5069  104 
Goal "!!d. [ d:domino; b<2 ] ==> EX i j. evnodd d b = {(i,j)}"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

105 
by (eresolve_tac [domino.elim] 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

106 
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

107 
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

108 
by (REPEAT_FIRST assume_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

109 
(*Four similar cases: case (i+j) mod 2 = b, 2#b, ...*) 
4686  110 
by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

111 
THEN Blast_tac 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

112 
qed "domino_singleton"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

113 

5069  114 
Goal "!!d. d:domino ==> finite d"; 
4089  115 
by (blast_tac (claset() addSEs [domino.elim]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

116 
qed "domino_finite"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

117 

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 
(*** Tilings of dominoes ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

120 

5069  121 
Goal "!!t. t:tiling domino ==> finite t"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

122 
by (eresolve_tac [tiling.induct] 1); 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3357
diff
changeset

123 
by (rtac Finites.emptyI 1); 
4089  124 
by (blast_tac (claset() addSIs [finite_UnI] addIs [domino_finite]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

125 
qed "tiling_domino_finite"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

126 

5069  127 
Goal "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

128 
by (eresolve_tac [tiling.induct] 1); 
4089  129 
by (simp_tac (simpset() addsimps [evnodd_def]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

130 
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

131 
by (Simp_tac 2 THEN assume_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

132 
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

133 
by (Simp_tac 2 THEN assume_tac 1); 
3718  134 
by (Clarify_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

135 
by (subgoal_tac "ALL p b. p : evnodd a b > p ~: evnodd ta b" 1); 
4089  136 
by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1); 
4387  137 
by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] 
138 
addEs [equalityE]) 1); 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

139 
qed "tiling_domino_0_1"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

140 

4387  141 
(*Final argument is surprisingly complex. Note the use of small simpsets 
142 
to avoid moving Sucs, etc.*) 

5069  143 
Goal "!!m n. [ t = below(Suc m + Suc m) Times below(Suc n + Suc n); \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

144 
\ t' = t  {(0,0)}  {(Suc(m+m), Suc(n+n))} \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

145 
\ ] ==> t' ~: tiling domino"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

146 
by (rtac notI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

147 
by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1); 
4387  148 
by (asm_full_simp_tac (HOL_ss addsimps [less_not_refl, tiling_domino_0_1]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

149 
by (subgoal_tac "t : tiling domino" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

150 
by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2); 
4387  151 
by (asm_full_simp_tac (simpset() 
152 
addsimps [mod_less, tiling_domino_0_1 RS sym]) 1); 

153 
(*Cardinality is smaller because of the two elements fewer*) 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

154 
by (rtac less_trans 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

155 
by (REPEAT 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

156 
(rtac card_Diff 1 
4089  157 
THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 
158 
THEN asm_simp_tac (simpset() addsimps [mod_less, evnodd_iff]) 1)); 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

159 
qed "mutil_not_tiling"; 