author  paulson 
Wed, 07 May 1997 12:50:26 +0200  
changeset 3120  c58423c20740 
child 3357  c224dddc5f71 
permissions  rwrr 
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 