author  paulson 
Thu, 11 Dec 1997 10:30:33 +0100  
changeset 4387  31d5a5a191e8 
parent 4369  11b217d9d880 
child 4477  b3e5857d8d99 
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 

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

13 
goal thy "!!t. t: tiling A ==> \ 
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 

3423  24 
goalw thy [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 

3423  29 
goalw thy [below_def] "below 0 = {}"; 
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 

3423  34 
goalw thy [below_def] 
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 

3423  40 
goalw thy [below_def] 
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 

3423  46 
goal thy "{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); 
3423  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 

3423  59 
goal thy "(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 

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

69 
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

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 

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

73 
goalw thy [evnodd_def] "evnodd A b <= A"; 
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 

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

80 
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

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 

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

84 
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

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 

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

88 
goalw thy [evnodd_def] "evnodd {} b = {}"; 
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 

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

92 
goalw thy [evnodd_def] 
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)"; 
4089  95 
by (simp_tac (simpset() addsplits [expand_if]) 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 

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

104 
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

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, ...*) 
4089  110 
by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc] 
3919  111 
addsplits [expand_if]) 1 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

114 

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

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

117 
qed "domino_finite"; 
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 

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

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

121 

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

122 
goal thy "!!t. t:tiling domino ==> finite t"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

123 
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

124 
by (rtac Finites.emptyI 1); 
4089  125 
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

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

127 

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

128 
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

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

131 
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

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

133 
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

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

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

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

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

141 

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

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

144 
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

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

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

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

148 
by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1); 
4387  149 
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

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

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

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

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

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

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

157 
(rtac card_Diff 1 
4089  158 
THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 
159 
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

160 
qed "mutil_not_tiling"; 