author  paulson 
Fri, 06 Jun 1997 10:46:26 +0200  
changeset 3423  3684a4420a67 
parent 3414  804c8a178a7f 
child 3718  d78cf498a88c 
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 
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 

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

27 
by (Blast_tac 1); 
3423  28 
qed "below_less_iff"; 
29 
AddIffs [below_less_iff]; 

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

30 

3423  31 
goalw thy [below_def] "below 0 = {}"; 
32 
by (Simp_tac 1); 

33 
qed "below_0"; 

34 
Addsimps [below_0]; 

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

35 

3423  36 
goalw thy [below_def] 
37 
"below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)"; 

38 
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); 

3120
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 

3423  42 
goalw thy [below_def] 
43 
"A Times below(Suc n) = (A Times {n}) Un (A Times (below n))"; 

44 
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); 

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

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

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

47 

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

49 
by (nat_ind_tac "n" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 
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

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

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

53 
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

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

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

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

57 
by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1); 
3423  58 
by (Auto_tac()); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

60 

3423  61 
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

62 
by (nat_ind_tac "m" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

63 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1]))); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

64 
by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row] 
3423  65 
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

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

67 

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 
(*** Basic properties of evnodd ***) 
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 
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

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

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

74 

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

75 
goalw thy [evnodd_def] "evnodd A b <= A"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

78 

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

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

80 
bind_thm("finite_evnodd", evnodd_subset RS finite_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 
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

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

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

85 

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

86 
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

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

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

89 

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

90 
goalw thy [evnodd_def] "evnodd {} b = {}"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

93 

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

94 
goalw thy [evnodd_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

95 
"evnodd (insert (i,j) C) b = \ 
3423  96 
\ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)"; 
97 
by (simp_tac (!simpset setloop (split_tac [expand_if] THEN' Step_tac)) 1); 

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

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

99 

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

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

102 

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

103 
(*** Dominoes ***) 
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 
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

106 
by (eresolve_tac [domino.elim] 1); 
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) 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

108 
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

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

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

112 
setloop split_tac [expand_if]) 1 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

115 

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

116 
goal thy "!!d. d:domino ==> finite d"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3357
diff
changeset

117 
by (blast_tac (!claset addSEs [domino.elim]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

122 

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

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

124 
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

125 
by (rtac Finites.emptyI 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

126 
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

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

128 

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

129 
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

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

131 
by (simp_tac (!simpset addsimps [evnodd_def]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

132 
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

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

134 
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

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

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

137 
by (subgoal_tac "ALL p b. p : evnodd a b > p ~: evnodd ta b" 1); 
3423  138 
by (asm_simp_tac (!simpset addsimps [tiling_domino_finite]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

139 
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

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

141 

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

142 
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

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

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

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

146 
by (dtac tiling_domino_0_1 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); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

148 
by (Asm_full_simp_tac 1); 
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 
(*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

151 
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

152 
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

153 
by (asm_simp_tac (!simpset addsimps add_ac) 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

154 
by (asm_full_simp_tac 
3423  155 
(!simpset addsimps [mod_less, tiling_domino_0_1 RS sym]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

161 
qed "mutil_not_tiling"; 