author  wenzelm 
Mon, 03 Nov 1997 12:13:18 +0100  
changeset 4089  96fba19bcbe2 
parent 3919  c036caebfc75 
child 4328  44364221a99d 
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); 
4089  19 
by (simp_tac (simpset() addsimps [Un_assoc]) 1); 
20 
by (blast_tac (claset() addIs tiling.intrs) 1); 

3120
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)"; 

4089  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))"; 

4089  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); 
4089  50 
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

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); 
4089  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); 
4089  63 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1]))); 
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)"; 
4089  97 
by (simp_tac (simpset() addsplits [expand_if]) 1); 
3718  98 
by (Blast_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

100 

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

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

105 

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

106 
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

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

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

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

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

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

116 

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

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

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

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

122 
(*** Tilings of dominoes ***) 
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 
goal thy "!!t. t:tiling domino ==> finite t"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

125 
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

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

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

129 

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

130 
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

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

133 
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

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

135 
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

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

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

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

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

142 

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

143 
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

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

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

152 
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

153 
by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1); 
4089  154 
by (asm_simp_tac (simpset() addsimps add_ac) 2); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

155 
by (asm_full_simp_tac 
4089  156 
(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

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

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

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

162 
qed "mutil_not_tiling"; 