author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10375  d943898cc3a9 
child 10785  53547a02f2a1 
permissions  rwrr 
9421  1 
(* Title: HOL/Finite.ML 
923  2 
ID: $Id$ 
1531  3 
Author: Lawrence C Paulson & Tobias Nipkow 
4 
Copyright 1995 University of Cambridge & TU Muenchen 

923  5 

9421  6 
Finite sets and their cardinality. 
923  7 
*) 
8 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

9 
section "finite"; 
1531  10 

923  11 
(*Discharging ~ x:y entails extra work*) 
5316  12 
val major::prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

13 
"[ finite F; P({}); \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

14 
\ !!F x. [ finite F; x ~: F; P(F) ] ==> P(insert x F) \ 
923  15 
\ ] ==> P(F)"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

16 
by (rtac (major RS Finites.induct) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

17 
by (excluded_middle_tac "a:A" 2); 
923  18 
by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) 
19 
by (REPEAT (ares_tac prems 1)); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

20 
qed "finite_induct"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

21 

5316  22 
val major::subs::prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

23 
"[ finite F; F <= A; \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

24 
\ P({}); \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

25 
\ !!F a. [ finite F; a:A; a ~: F; P(F) ] ==> P(insert a F) \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

26 
\ ] ==> P(F)"; 
4386  27 
by (rtac (subs RS rev_mp) 1); 
28 
by (rtac (major RS finite_induct) 1); 

29 
by (ALLGOALS (blast_tac (claset() addIs prems))); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

30 
qed "finite_subset_induct"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

31 

c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

32 
Addsimps Finites.intrs; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

33 
AddSIs Finites.intrs; 
923  34 

35 
(*The union of two finite sets is finite*) 

5316  36 
Goal "[ finite F; finite G ] ==> finite(F Un G)"; 
37 
by (etac finite_induct 1); 

38 
by (ALLGOALS Asm_simp_tac); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

39 
qed "finite_UnI"; 
923  40 

41 
(*Every subset of a finite set is finite*) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

42 
Goal "finite B ==> ALL A. A<=B > finite A"; 
4304  43 
by (etac finite_induct 1); 
9399  44 
by (ALLGOALS (simp_tac (simpset() addsimps [subset_insert_iff]))); 
45 
by Safe_tac; 

46 
by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 1); 

47 
by (ALLGOALS Blast_tac); 

4304  48 
val lemma = result(); 
49 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

50 
Goal "[ A<=B; finite B ] ==> finite A"; 
4423  51 
by (dtac lemma 1); 
4304  52 
by (Blast_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

53 
qed "finite_subset"; 
923  54 

5069  55 
Goal "finite(F Un G) = (finite F & finite G)"; 
4304  56 
by (blast_tac (claset() 
8554
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

57 
addIs [inst "B" "?X Un ?Y" finite_subset, finite_UnI]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

58 
qed "finite_Un"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

59 
AddIffs[finite_Un]; 
1531  60 

8554
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

61 
(*The converse obviously fails*) 
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

62 
Goal "finite F  finite G ==> finite(F Int G)"; 
5413  63 
by (blast_tac (claset() addIs [finite_subset]) 1); 
8554
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

64 
qed "finite_Int"; 
5413  65 

8554
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

66 
Addsimps [finite_Int]; 
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

67 
AddIs [finite_Int]; 
5413  68 

5069  69 
Goal "finite(insert a A) = finite A"; 
1553  70 
by (stac insert_is_Un 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

71 
by (simp_tac (HOL_ss addsimps [finite_Un]) 1); 
3427
e7cef2081106
Removed a few redundant additions of simprules or classical rules
paulson
parents:
3416
diff
changeset

72 
by (Blast_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

73 
qed "finite_insert"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

74 
Addsimps[finite_insert]; 
1531  75 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

76 
(*The image of a finite set is finite *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

77 
Goal "finite F ==> finite(h``F)"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

78 
by (etac finite_induct 1); 
1264  79 
by (Simp_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

80 
by (Asm_simp_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

81 
qed "finite_imageI"; 
923  82 

8155  83 
Goal "finite (range g) ==> finite (range (%x. f (g x)))"; 
84 
by (Simp_tac 1); 

85 
by (etac finite_imageI 1); 

86 
qed "finite_range_imageI"; 

87 

5316  88 
val major::prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

89 
"[ finite c; finite b; \ 
1465  90 
\ P(b); \ 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

91 
\ !!x y. [ finite y; x:y; P(y) ] ==> P(y{x}) \ 
923  92 
\ ] ==> c<=b > P(bc)"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

93 
by (rtac (major RS finite_induct) 1); 
2031  94 
by (stac Diff_insert 2); 
923  95 
by (ALLGOALS (asm_simp_tac 
5537  96 
(simpset() addsimps prems@[Diff_subset RS finite_subset]))); 
1531  97 
val lemma = result(); 
923  98 

5316  99 
val prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

100 
"[ finite A; \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

101 
\ P(A); \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

102 
\ !!a A. [ finite A; a:A; P(A) ] ==> P(A{a}) \ 
923  103 
\ ] ==> P({})"; 
104 
by (rtac (Diff_cancel RS subst) 1); 

1531  105 
by (rtac (lemma RS mp) 1); 
923  106 
by (REPEAT (ares_tac (subset_refl::prems) 1)); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

107 
qed "finite_empty_induct"; 
1531  108 

109 

1618  110 
(* finite B ==> finite (B  Ba) *) 
111 
bind_thm ("finite_Diff", Diff_subset RS finite_subset); 

1531  112 
Addsimps [finite_Diff]; 
113 

5626  114 
Goal "finite(A  insert a B) = finite(AB)"; 
6162  115 
by (stac Diff_insert 1); 
5626  116 
by (case_tac "a : AB" 1); 
3457  117 
by (rtac (finite_insert RS sym RS trans) 1); 
3368  118 
by (stac insert_Diff 1); 
5626  119 
by (ALLGOALS Asm_full_simp_tac); 
120 
qed "finite_Diff_insert"; 

121 
AddIffs [finite_Diff_insert]; 

122 

8554
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

123 
(*lemma merely for classical reasoner in the proof below: force_tac can't 
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

124 
prove it.*) 
5626  125 
Goal "finite(A{}) = finite A"; 
126 
by (Simp_tac 1); 

127 
val lemma = result(); 

3368  128 

4059  129 
(*Lemma for proving finite_imageD*) 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

130 
Goal "finite B ==> ALL A. f``A = B > inj_on f A > finite A"; 
1553  131 
by (etac finite_induct 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

132 
by (ALLGOALS Asm_simp_tac); 
3708  133 
by (Clarify_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

134 
by (subgoal_tac "EX y:A. f y = x & F = f``(A{y})" 1); 
3708  135 
by (Clarify_tac 1); 
8081  136 
by (full_simp_tac (simpset() addsimps [inj_on_def]) 1); 
8554
ba33995b87ff
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
paulson
parents:
8442
diff
changeset

137 
by (blast_tac (claset() addSDs [lemma RS iffD1]) 1); 
3368  138 
by (thin_tac "ALL A. ?PP(A)" 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

139 
by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); 
3708  140 
by (Clarify_tac 1); 
3368  141 
by (res_inst_tac [("x","xa")] bexI 1); 
4059  142 
by (ALLGOALS 
4830  143 
(asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff]))); 
3368  144 
val lemma = result(); 
145 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

146 
Goal "[ finite(f``A); inj_on f A ] ==> finite A"; 
3457  147 
by (dtac lemma 1); 
3368  148 
by (Blast_tac 1); 
149 
qed "finite_imageD"; 

150 

4014  151 
(** The finite UNION of finite sets **) 
152 

9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

153 
Goal "finite A ==> (ALL a:A. finite(B a)) > finite(UN a:A. B a)"; 
5316  154 
by (etac finite_induct 1); 
4153  155 
by (ALLGOALS Asm_simp_tac); 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

156 
bind_thm("finite_UN_I", ballI RSN (2, result() RS mp)); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

157 

5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

158 
(*strengthen RHS to 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

159 
((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}}) ? 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

160 
we'd need to prove 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

161 
finite C ==> ALL A B. (UNION A B) <= C > finite {x. x:A & B x ~= {}} 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

162 
by induction*) 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

163 
Goal "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"; 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

164 
by (blast_tac (claset() addIs [finite_UN_I, finite_subset]) 1); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

165 
qed "finite_UN"; 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

166 
Addsimps [finite_UN]; 
4014  167 

168 
(** Sigma of finite sets **) 

169 

5069  170 
Goalw [Sigma_def] 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

171 
"[ finite A; ALL a:A. finite(B a) ] ==> finite(SIGMA a:A. B a)"; 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

172 
by (blast_tac (claset() addSIs [finite_UN_I]) 1); 
4014  173 
bind_thm("finite_SigmaI", ballI RSN (2,result())); 
174 
Addsimps [finite_SigmaI]; 

3368  175 

8262  176 
Goal "[ finite (UNIV::'a set); finite (UNIV::'b set)] ==> finite (UNIV::('a * 'b) set)"; 
177 
by (subgoal_tac "(UNIV::('a * 'b) set) = Sigma UNIV (%x. UNIV)" 1); 

178 
by (etac ssubst 1); 

179 
by (etac finite_SigmaI 1); 

180 
by Auto_tac; 

181 
qed "finite_Prod_UNIV"; 

182 

183 
Goal "finite (UNIV :: ('a::finite * 'b::finite) set)"; 

8320  184 
by (rtac (finite_Prod_UNIV) 1); 
185 
by (rtac finite 1); 

186 
by (rtac finite 1); 

8262  187 
qed "finite_Prod"; 
188 

9351  189 
Goal "finite (UNIV :: unit set)"; 
190 
by (subgoal_tac "UNIV = {()}" 1); 

191 
by (etac ssubst 1); 

192 
by Auto_tac; 

193 
qed "finite_unit"; 

194 

3368  195 
(** The powerset of a finite set **) 
196 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

197 
Goal "finite(Pow A) ==> finite A"; 
3368  198 
by (subgoal_tac "finite ((%x.{x})``A)" 1); 
3457  199 
by (rtac finite_subset 2); 
200 
by (assume_tac 3); 

3368  201 
by (ALLGOALS 
4830  202 
(fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD]))); 
3368  203 
val lemma = result(); 
204 

5069  205 
Goal "finite(Pow A) = finite A"; 
3457  206 
by (rtac iffI 1); 
207 
by (etac lemma 1); 

3368  208 
(*Opposite inclusion: finite A ==> finite (Pow A) *) 
3340  209 
by (etac finite_induct 1); 
210 
by (ALLGOALS 

211 
(asm_simp_tac 

4089  212 
(simpset() addsimps [finite_UnI, finite_imageI, Pow_insert]))); 
3368  213 
qed "finite_Pow_iff"; 
214 
AddIffs [finite_Pow_iff]; 

3340  215 

5069  216 
Goal "finite(r^1) = finite r"; 
3457  217 
by (subgoal_tac "r^1 = (%(x,y).(y,x))``r" 1); 
218 
by (Asm_simp_tac 1); 

219 
by (rtac iffI 1); 

4830  220 
by (etac (rewrite_rule [inj_on_def] finite_imageD) 1); 
221 
by (simp_tac (simpset() addsplits [split_split]) 1); 

3457  222 
by (etac finite_imageI 1); 
4746  223 
by (simp_tac (simpset() addsimps [converse_def,image_def]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

224 
by Auto_tac; 
5516  225 
by (rtac bexI 1); 
226 
by (assume_tac 2); 

4763  227 
by (Simp_tac 1); 
4746  228 
qed "finite_converse"; 
229 
AddIffs [finite_converse]; 

1531  230 

8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

231 
Goal "finite (lessThan (k::nat))"; 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

232 
by (induct_tac "k" 1); 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

233 
by (simp_tac (simpset() addsimps [lessThan_Suc]) 2); 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

234 
by Auto_tac; 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

235 
qed "finite_lessThan"; 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

236 

0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

237 
Goal "finite (atMost (k::nat))"; 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

238 
by (induct_tac "k" 1); 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

239 
by (simp_tac (simpset() addsimps [atMost_Suc]) 2); 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

240 
by Auto_tac; 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

241 
qed "finite_atMost"; 
8971  242 
AddIffs [finite_lessThan, finite_atMost]; 
8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

243 

8889  244 
(* A bounded set of natural numbers is finite *) 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

245 
Goal "(ALL i:N. i<(n::nat)) ==> finite N"; 
8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

246 
by (rtac finite_subset 1); 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

247 
by (rtac finite_lessThan 2); 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

248 
by Auto_tac; 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

249 
qed "bounded_nat_set_is_finite"; 
8889  250 

251 

1548  252 
section "Finite cardinality  'card'"; 
1531  253 

9108  254 
bind_thm ("cardR_emptyE", cardR.mk_cases "({},n) : cardR"); 
255 
bind_thm ("cardR_insertE", cardR.mk_cases "(insert a A,n) : cardR"); 

1531  256 

5626  257 
AddSEs [cardR_emptyE]; 
258 
AddSIs cardR.intrs; 

259 

9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

260 
Goal "[ (A,n) : cardR ] ==> a : A > (EX m. n = Suc m)"; 
6162  261 
by (etac cardR.induct 1); 
262 
by (Blast_tac 1); 

263 
by (Blast_tac 1); 

5626  264 
qed "cardR_SucD"; 
265 

9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

266 
Goal "(A,m): cardR ==> (ALL n a. m = Suc n > a:A > (A{a},n) : cardR)"; 
6162  267 
by (etac cardR.induct 1); 
8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

268 
by Auto_tac; 
6162  269 
by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1); 
8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

270 
by Auto_tac; 
7499  271 
by (ftac cardR_SucD 1); 
6162  272 
by (Blast_tac 1); 
5626  273 
val lemma = result(); 
274 

275 
Goal "[ (insert a A, Suc m) : cardR; a ~: A ] ==> (A,m) : cardR"; 

6162  276 
by (dtac lemma 1); 
277 
by (Asm_full_simp_tac 1); 

5626  278 
val lemma = result(); 
279 

9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

280 
Goal "(A,m): cardR ==> (ALL n. (A,n) : cardR > n=m)"; 
6162  281 
by (etac cardR.induct 1); 
282 
by (safe_tac (claset() addSEs [cardR_insertE])); 

283 
by (rename_tac "B b m" 1); 

284 
by (case_tac "a = b" 1); 

285 
by (subgoal_tac "A = B" 1); 

286 
by (blast_tac (claset() addEs [equalityE]) 2); 

287 
by (Blast_tac 1); 

9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

288 
by (subgoal_tac "EX C. A = insert b C & B = insert a C" 1); 
6162  289 
by (res_inst_tac [("x","A Int B")] exI 2); 
290 
by (blast_tac (claset() addEs [equalityE]) 2); 

291 
by (forw_inst_tac [("A","B")] cardR_SucD 1); 

292 
by (blast_tac (claset() addDs [lemma]) 1); 

5626  293 
qed_spec_mp "cardR_determ"; 
294 

295 
Goal "(A,n) : cardR ==> finite(A)"; 

296 
by (etac cardR.induct 1); 

297 
by Auto_tac; 

298 
qed "cardR_imp_finite"; 

299 

300 
Goal "finite(A) ==> EX n. (A, n) : cardR"; 

301 
by (etac finite_induct 1); 

302 
by Auto_tac; 

303 
qed "finite_imp_cardR"; 

304 

305 
Goalw [card_def] "(A,n) : cardR ==> card A = n"; 

306 
by (blast_tac (claset() addIs [cardR_determ]) 1); 

307 
qed "card_equality"; 

308 

309 
Goalw [card_def] "card {} = 0"; 

310 
by (Blast_tac 1); 

311 
qed "card_empty"; 

312 
Addsimps [card_empty]; 

313 

314 
Goal "x ~: A ==> \ 

315 
\ ((insert x A, n) : cardR) = \ 

316 
\ (EX m. (A, m) : cardR & n = Suc m)"; 

317 
by Auto_tac; 

318 
by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1); 

319 
by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1); 

320 
by (blast_tac (claset() addIs [cardR_determ]) 1); 

321 
val lemma = result(); 

322 

323 
Goalw [card_def] 

324 
"[ finite A; x ~: A ] ==> card (insert x A) = Suc(card A)"; 

325 
by (asm_simp_tac (simpset() addsimps [lemma]) 1); 

9969  326 
by (rtac some_equality 1); 
5626  327 
by (auto_tac (claset() addIs [finite_imp_cardR], 
328 
simpset() addcongs [conj_cong] 

329 
addsimps [symmetric card_def, 

330 
card_equality])); 

331 
qed "card_insert_disjoint"; 

332 
Addsimps [card_insert_disjoint]; 

333 

334 
(* Delete rules to do with cardR relation: obsolete *) 

335 
Delrules [cardR_emptyE]; 

336 
Delrules cardR.intrs; 

337 

7958  338 
Goal "finite A ==> (card A = 0) = (A = {})"; 
339 
by Auto_tac; 

340 
by (dres_inst_tac [("a","x")] mk_disjoint_insert 1); 

341 
by (Clarify_tac 1); 

342 
by (rotate_tac ~1 1); 

343 
by Auto_tac; 

344 
qed "card_0_eq"; 

345 
Addsimps[card_0_eq]; 

346 

5626  347 
Goal "finite A ==> card(insert x A) = (if x:A then card A else Suc(card(A)))"; 
348 
by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1); 

349 
qed "card_insert_if"; 

350 

7821  351 
Goal "[ finite A; x: A ] ==> Suc (card (A{x})) = card A"; 
5626  352 
by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); 
353 
by (assume_tac 1); 

354 
by (Asm_simp_tac 1); 

355 
qed "card_Suc_Diff1"; 

356 

7821  357 
Goal "[ finite A; x: A ] ==> card (A{x}) = card A  1"; 
358 
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1 RS sym]) 1); 

359 
qed "card_Diff_singleton"; 

360 

9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

361 
Goal "finite A ==> card (A{x}) = (if x:A then card A  1 else card A)"; 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

362 
by (asm_simp_tac (simpset() addsimps [card_Diff_singleton]) 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

363 
qed "card_Diff_singleton_if"; 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

364 

5626  365 
Goal "finite A ==> card(insert x A) = Suc(card(A{x}))"; 
366 
by (asm_simp_tac (simpset() addsimps [card_insert_if,card_Suc_Diff1]) 1); 

367 
qed "card_insert"; 

3352  368 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

369 
Goal "finite A ==> card A <= card (insert x A)"; 
5626  370 
by (asm_simp_tac (simpset() addsimps [card_insert_if]) 1); 
4768
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

371 
qed "card_insert_le"; 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

372 

9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

373 
Goal "finite B ==> ALL A. A <= B > card B <= card A > A = B"; 
3352  374 
by (etac finite_induct 1); 
9338  375 
by (Simp_tac 1); 
3708  376 
by (Clarify_tac 1); 
9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

377 
by (subgoal_tac "finite A & A{x} <= F" 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

378 
by (blast_tac (claset() addIs [finite_subset]) 2); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

379 
by (dres_inst_tac [("x","A{x}")] spec 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

380 
by (asm_full_simp_tac (simpset() addsimps [card_Diff_singleton_if] 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

381 
addsplits [split_if_asm]) 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

382 
by (case_tac "card A" 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

383 
by Auto_tac; 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

384 
qed_spec_mp "card_seteq"; 
3352  385 

9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

386 
Goalw [psubset_def] "[ finite B; A < B ] ==> card A < card B"; 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

387 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

388 
by (blast_tac (claset() addDs [card_seteq]) 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

389 
qed "psubset_card_mono" ; 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

390 

2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

391 
Goal "[ finite B; A <= B ] ==> card A <= card B"; 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

392 
by (case_tac "A=B" 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

393 
by (Asm_simp_tac 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

394 
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

395 
by (blast_tac (claset() addDs [card_seteq] addIs [order_less_imp_le]) 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

396 
qed "card_mono" ; 
5416
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

397 

9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

398 
Goal "[ finite A; finite B ] \ 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

399 
\ ==> card A + card B = card (A Un B) + card (A Int B)"; 
3352  400 
by (etac finite_induct 1); 
5416
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

401 
by (Simp_tac 1); 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

402 
by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1); 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

403 
qed "card_Un_Int"; 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

404 

9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

405 
Goal "[ finite A; finite B; A Int B = {} ] \ 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

406 
\ ==> card (A Un B) = card A + card B"; 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

407 
by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1); 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

408 
qed "card_Un_disjoint"; 
3352  409 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

410 
Goal "[ finite A; B<=A ] ==> card A  card B = card (A  B)"; 
3352  411 
by (subgoal_tac "(AB) Un B = A" 1); 
412 
by (Blast_tac 2); 

3457  413 
by (rtac (add_right_cancel RS iffD1) 1); 
414 
by (rtac (card_Un_disjoint RS subst) 1); 

415 
by (etac ssubst 4); 

3352  416 
by (Blast_tac 3); 
417 
by (ALLGOALS 

418 
(asm_simp_tac 

4089  419 
(simpset() addsimps [add_commute, not_less_iff_le, 
5416
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

420 
add_diff_inverse, card_mono, finite_subset]))); 
3352  421 
qed "card_Diff_subset"; 
1531  422 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

423 
Goal "[ finite A; x: A ] ==> card(A{x}) < card A"; 
2031  424 
by (rtac Suc_less_SucD 1); 
5626  425 
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1); 
426 
qed "card_Diff1_less"; 

1618  427 

10375
d943898cc3a9
new lemma card_Diff2_less for mulilated chess board
paulson
parents:
10098
diff
changeset

428 
Goal "[ finite A; x: A; y: A ] ==> card(A{x}{y}) < card A"; 
d943898cc3a9
new lemma card_Diff2_less for mulilated chess board
paulson
parents:
10098
diff
changeset

429 
by (case_tac "x=y" 1); 
d943898cc3a9
new lemma card_Diff2_less for mulilated chess board
paulson
parents:
10098
diff
changeset

430 
by (asm_simp_tac (simpset() addsimps [card_Diff1_less]) 1); 
d943898cc3a9
new lemma card_Diff2_less for mulilated chess board
paulson
parents:
10098
diff
changeset

431 
by (rtac less_trans 1); 
d943898cc3a9
new lemma card_Diff2_less for mulilated chess board
paulson
parents:
10098
diff
changeset

432 
by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], simpset()))); 
d943898cc3a9
new lemma card_Diff2_less for mulilated chess board
paulson
parents:
10098
diff
changeset

433 
qed "card_Diff2_less"; 
d943898cc3a9
new lemma card_Diff2_less for mulilated chess board
paulson
parents:
10098
diff
changeset

434 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

435 
Goal "finite A ==> card(A{x}) <= card A"; 
4768
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

436 
by (case_tac "x: A" 1); 
5626  437 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le]))); 
438 
qed "card_Diff1_le"; 

1531  439 

5626  440 
Goal "[ finite B; A <= B; card A < card B ] ==> A < B"; 
441 
by (etac psubsetI 1); 

442 
by (Blast_tac 1); 

443 
qed "card_psubset"; 

444 

445 
(*** Cardinality of image ***) 

446 

447 
Goal "finite A ==> card (f `` A) <= card A"; 

448 
by (etac finite_induct 1); 

9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

449 
by (Simp_tac 1); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

450 
by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI, 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

451 
card_insert_if]) 1); 
5626  452 
qed "card_image_le"; 
453 

454 
Goal "finite(A) ==> inj_on f A > card (f `` A) = card A"; 

455 
by (etac finite_induct 1); 

456 
by (ALLGOALS Asm_simp_tac); 

457 
by Safe_tac; 

458 
by (rewtac inj_on_def); 

459 
by (Blast_tac 1); 

460 
by (stac card_insert_disjoint 1); 

461 
by (etac finite_imageI 1); 

462 
by (Blast_tac 1); 

463 
by (Blast_tac 1); 

464 
qed_spec_mp "card_image"; 

465 

466 
Goal "[ finite A; f``A <= A; inj_on f A ] ==> f``A = A"; 

9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

467 
by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1); 
5626  468 
qed "endo_inj_surj"; 
469 

470 
(*** Cardinality of the Powerset ***) 

471 

472 
Goal "finite A ==> card (Pow A) = 2 ^ card A"; 

473 
by (etac finite_induct 1); 

474 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); 

475 
by (stac card_Un_disjoint 1); 

476 
by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1])); 

477 
by (subgoal_tac "inj_on (insert x) (Pow F)" 1); 

478 
by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1); 

479 
by (rewtac inj_on_def); 

480 
by (blast_tac (claset() addSEs [equalityE]) 1); 

481 
qed "card_Pow"; 

482 

3368  483 

3430  484 
(*Relates to equivalence classes. Based on a theorem of F. Kammueller's. 
3368  485 
The "finite C" premise is redundant*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

486 
Goal "finite C ==> finite (Union C) > \ 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

487 
\ (ALL c : C. k dvd card c) > \ 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

488 
\ (ALL c1: C. ALL c2: C. c1 ~= c2 > c1 Int c2 = {}) \ 
3368  489 
\ > k dvd card(Union C)"; 
490 
by (etac finite_induct 1); 

491 
by (ALLGOALS Asm_simp_tac); 

3708  492 
by (Clarify_tac 1); 
3368  493 
by (stac card_Un_disjoint 1); 
494 
by (ALLGOALS 

4089  495 
(asm_full_simp_tac (simpset() 
3368  496 
addsimps [dvd_add, disjoint_eq_subset_Compl]))); 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

497 
by (thin_tac "ALL c:F. ?PP(c)" 1); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

498 
by (thin_tac "ALL c:F. ?PP(c) & ?QQ(c)" 1); 
3708  499 
by (Clarify_tac 1); 
3368  500 
by (ball_tac 1); 
501 
by (Blast_tac 1); 

502 
qed_spec_mp "dvd_partition"; 

503 

5616  504 

505 
(*** foldSet ***) 

506 

9108  507 
bind_thm ("empty_foldSetE", foldSet.mk_cases "({}, x) : foldSet f e"); 
5616  508 

509 
AddSEs [empty_foldSetE]; 

510 
AddIs foldSet.intrs; 

511 

512 
Goal "[ (A{x},y) : foldSet f e; x: A ] ==> (A, f x y) : foldSet f e"; 

513 
by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1); 

514 
by Auto_tac; 

5626  515 
qed "Diff1_foldSet"; 
5616  516 

517 
Goal "(A, x) : foldSet f e ==> finite(A)"; 

518 
by (eresolve_tac [foldSet.induct] 1); 

519 
by Auto_tac; 

520 
qed "foldSet_imp_finite"; 

521 

522 
Addsimps [foldSet_imp_finite]; 

523 

524 

525 
Goal "finite(A) ==> EX x. (A, x) : foldSet f e"; 

526 
by (etac finite_induct 1); 

527 
by Auto_tac; 

528 
qed "finite_imp_foldSet"; 

529 

530 

531 
Open_locale "LC"; 

532 

5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

533 
val f_lcomm = thm "lcomm"; 
5616  534 

535 

536 
Goal "ALL A x. card(A) < n > (A, x) : foldSet f e > \ 

537 
\ (ALL y. (A, y) : foldSet f e > y=x)"; 

538 
by (induct_tac "n" 1); 

539 
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq])); 

540 
by (etac foldSet.elim 1); 

541 
by (Blast_tac 1); 

542 
by (etac foldSet.elim 1); 

543 
by (Blast_tac 1); 

544 
by (Clarify_tac 1); 

545 
(*force simplification of "card A < card (insert ...)"*) 

546 
by (etac rev_mp 1); 

547 
by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1); 

548 
by (rtac impI 1); 

549 
(** LEVEL 10 **) 

550 
by (rename_tac "Aa xa ya Ab xb yb" 1); 

551 
by (case_tac "xa=xb" 1); 

552 
by (subgoal_tac "Aa = Ab" 1); 

9837  553 
by (blast_tac (claset() addSEs [equalityE]) 2); 
5616  554 
by (Blast_tac 1); 
555 
(*case xa ~= xb*) 

556 
by (subgoal_tac "Aa{xb} = Ab{xa} & xb : Aa & xa : Ab" 1); 

9837  557 
by (blast_tac (claset() addSEs [equalityE]) 2); 
5616  558 
by (Clarify_tac 1); 
559 
by (subgoal_tac "Aa = insert xb Ab  {xa}" 1); 

9837  560 
by (Blast_tac 2); 
5616  561 
(** LEVEL 20 **) 
562 
by (subgoal_tac "card Aa <= card Ab" 1); 

563 
by (rtac (Suc_le_mono RS subst) 2); 

5626  564 
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 2); 
5616  565 
by (res_inst_tac [("A1", "Aa{xb}"), ("f1","f")] 
566 
(finite_imp_foldSet RS exE) 1); 

567 
by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1); 

7499  568 
by (ftac Diff1_foldSet 1 THEN assume_tac 1); 
5616  569 
by (subgoal_tac "ya = f xb x" 1); 
9837  570 
by (blast_tac (claset() delrules [equalityCE]) 2); 
5616  571 
by (subgoal_tac "(Ab  {xa}, x) : foldSet f e" 1); 
572 
by (Asm_full_simp_tac 2); 

573 
by (subgoal_tac "yb = f xa x" 1); 

9837  574 
by (blast_tac (claset() delrules [equalityCE] 
575 
addDs [Diff1_foldSet]) 2); 

5616  576 
by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1); 
577 
val lemma = result(); 

578 

579 

580 
Goal "[ (A, x) : foldSet f e; (A, y) : foldSet f e ] ==> y=x"; 

9736  581 
by (blast_tac (claset() addIs [rulify lemma]) 1); 
5616  582 
qed "foldSet_determ"; 
583 

584 
Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y"; 

585 
by (blast_tac (claset() addIs [foldSet_determ]) 1); 

586 
qed "fold_equality"; 

587 

588 
Goalw [fold_def] "fold f e {} = e"; 

589 
by (Blast_tac 1); 

590 
qed "fold_empty"; 

591 
Addsimps [fold_empty]; 

592 

5626  593 

5616  594 
Goal "x ~: A ==> \ 
595 
\ ((insert x A, v) : foldSet f e) = \ 

596 
\ (EX y. (A, y) : foldSet f e & v = f x y)"; 

597 
by Auto_tac; 

598 
by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1); 

599 
by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1); 

600 
by (blast_tac (claset() addIs [foldSet_determ]) 1); 

601 
val lemma = result(); 

602 

603 
Goalw [fold_def] 

604 
"[ finite A; x ~: A ] ==> fold f e (insert x A) = f x (fold f e A)"; 

605 
by (asm_simp_tac (simpset() addsimps [lemma]) 1); 

9969  606 
by (rtac some_equality 1); 
5616  607 
by (auto_tac (claset() addIs [finite_imp_foldSet], 
608 
simpset() addcongs [conj_cong] 

609 
addsimps [symmetric fold_def, 

610 
fold_equality])); 

611 
qed "fold_insert"; 

612 

8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

613 
Goal "finite A ==> ALL e. f x (fold f e A) = fold f (f x e) A"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

614 
by (etac finite_induct 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

615 
by (Simp_tac 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

616 
by (asm_simp_tac (simpset() addsimps [f_lcomm, fold_insert]) 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

617 
qed_spec_mp "fold_commute"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

618 

c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

619 
Goal "[ finite A; finite B ] \ 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

620 
\ ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

621 
by (etac finite_induct 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

622 
by (Simp_tac 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

623 
by (asm_simp_tac (simpset() addsimps [fold_insert, fold_commute, 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

624 
Int_insert_left, insert_absorb]) 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

625 
qed "fold_nest_Un_Int"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

626 

c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

627 
Goal "[ finite A; finite B; A Int B = {} ] \ 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

628 
\ ==> fold f e (A Un B) = fold f (fold f e B) A"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

629 
by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

630 
qed "fold_nest_Un_disjoint"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

631 

5626  632 
(* Delete rules to do with foldSet relation: obsolete *) 
633 
Delsimps [foldSet_imp_finite]; 

634 
Delrules [empty_foldSetE]; 

635 
Delrules foldSet.intrs; 

636 

6024  637 
Close_locale "LC"; 
5616  638 

639 
Open_locale "ACe"; 

640 

8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

641 
(*We enter a more restrictive framework, with f :: ['a,'a] => 'a 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

642 
instead of ['b,'a] => 'a 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

643 
At present, none of these results are used!*) 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

644 

5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

645 
val f_ident = thm "ident"; 
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

646 
val f_commute = thm "commute"; 
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

647 
val f_assoc = thm "assoc"; 
5616  648 

649 

650 
Goal "f x (f y z) = f y (f x z)"; 

651 
by (rtac (f_commute RS trans) 1); 

652 
by (rtac (f_assoc RS trans) 1); 

653 
by (rtac (f_commute RS arg_cong) 1); 

654 
qed "f_left_commute"; 

655 

656 
val f_ac = [f_assoc, f_commute, f_left_commute]; 

657 

658 
Goal "f e x = x"; 

659 
by (stac f_commute 1); 

660 
by (rtac f_ident 1); 

661 
qed "f_left_ident"; 

662 

663 
val f_idents = [f_left_ident, f_ident]; 

664 

665 
Goal "[ finite A; finite B ] \ 

666 
\ ==> f (fold f e A) (fold f e B) = \ 

667 
\ f (fold f e (A Un B)) (fold f e (A Int B))"; 

668 
by (etac finite_induct 1); 

669 
by (simp_tac (simpset() addsimps f_idents) 1); 

670 
by (asm_simp_tac (simpset() addsimps f_ac @ f_idents @ 

671 
[export fold_insert,insert_absorb, Int_insert_left]) 1); 

672 
qed "fold_Un_Int"; 

673 

674 
Goal "[ finite A; finite B; A Int B = {} ] \ 

675 
\ ==> fold f e (A Un B) = f (fold f e A) (fold f e B)"; 

676 
by (asm_simp_tac (simpset() addsimps fold_Un_Int::f_idents) 1); 

677 
qed "fold_Un_disjoint"; 

678 

679 
Goal 

680 
"[ finite A; finite B ] ==> A Int B = {} > \ 

9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

681 
\ fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)"; 
5616  682 
by (etac finite_induct 1); 
683 
by (simp_tac (simpset() addsimps f_idents) 1); 

684 
by (asm_full_simp_tac (simpset() addsimps f_ac @ f_idents @ 

685 
[export fold_insert,insert_absorb, Int_insert_left]) 1); 

686 
qed "fold_Un_disjoint2"; 

687 

6024  688 
Close_locale "ACe"; 
5616  689 

690 

8981  691 
(*** setsum: generalized summation over a set ***) 
5616  692 

693 
Goalw [setsum_def] "setsum f {} = 0"; 

6162  694 
by (Simp_tac 1); 
5616  695 
qed "setsum_empty"; 
696 
Addsimps [setsum_empty]; 

697 

698 
Goalw [setsum_def] 

699 
"[ finite F; a ~: F ] ==> setsum f (insert a F) = f(a) + setsum f F"; 

8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

700 
by (asm_simp_tac (simpset() addsimps [export fold_insert, 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

701 
thm "plus_ac0_left_commute"]) 1); 
5616  702 
qed "setsum_insert"; 
703 
Addsimps [setsum_insert]; 

704 

9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

705 
Goal "setsum (%i. 0) A = 0"; 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

706 
by (case_tac "finite A" 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

707 
by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); 
9002  708 
by (etac finite_induct 1); 
709 
by Auto_tac; 

710 
qed "setsum_0"; 

711 

9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

712 
Goal "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"; 
9002  713 
by (etac finite_induct 1); 
714 
by Auto_tac; 

715 
qed "setsum_eq_0_iff"; 

716 
Addsimps [setsum_eq_0_iff]; 

717 

9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

718 
Goal "setsum f A = Suc n ==> EX a:A. 0 < f a"; 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

719 
by (case_tac "finite A" 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

720 
by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
9002  721 
by (etac rev_mp 1); 
722 
by (etac finite_induct 1); 

723 
by Auto_tac; 

724 
qed "setsum_SucD"; 

725 

8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

726 
(*Could allow many "card" proofs to be simplified*) 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

727 
Goal "finite A ==> card A = setsum (%x. 1) A"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

728 
by (etac finite_induct 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

729 
by Auto_tac; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

730 
qed "card_eq_setsum"; 
5616  731 

9002  732 
(*The reversed orientation looks more natural, but LOOPS as a simprule!*) 
8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

733 
Goal "[ finite A; finite B ] \ 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

734 
\ ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

735 
by (etac finite_induct 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

736 
by (Simp_tac 1); 
8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

737 
by (asm_full_simp_tac (simpset() addsimps (thms "plus_ac0") @ 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

738 
[Int_insert_left, insert_absorb]) 1); 
8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

739 
qed "setsum_Un_Int"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

740 

8981  741 
Goal "[ finite A; finite B; A Int B = {} ] \ 
742 
\ ==> setsum g (A Un B) = setsum g A + setsum g B"; 

743 
by (stac (setsum_Un_Int RS sym) 1); 

744 
by Auto_tac; 

745 
qed "setsum_Un_disjoint"; 

746 

9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

747 
Goal "finite I \ 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

748 
\ ==> (ALL i:I. finite (A i)) > \ 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

749 
\ (ALL i:I. ALL j:I. i~=j > A i Int A j = {}) > \ 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

750 
\ setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; 
8981  751 
by (etac finite_induct 1); 
9096
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

752 
by (Simp_tac 1); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

753 
by (Clarify_tac 1); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

754 
by (subgoal_tac "ALL i:F. x ~= i" 1); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

755 
by (Blast_tac 2); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

756 
by (subgoal_tac "A x Int UNION F A = {}" 1); 
5c4d4364f854
tidied; weakened the (impossible) premises of setsum_UN_disjoint
paulson
parents:
9086
diff
changeset

757 
by (Blast_tac 2); 
8981  758 
by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1); 
759 
qed_spec_mp "setsum_UN_disjoint"; 

760 

9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

761 
Goal "setsum (%x. f x + g x) A = setsum f A + setsum g A"; 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

762 
by (case_tac "finite A" 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

763 
by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
8981  764 
by (etac finite_induct 1); 
765 
by Auto_tac; 

766 
by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1); 

767 
qed "setsum_addf"; 

768 

769 
(** For the natural numbers, we have subtraction **) 

770 

8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

771 
Goal "[ finite A; finite B ] \ 
8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

772 
\ ==> (setsum f (A Un B) :: nat) = \ 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

773 
\ setsum f A + setsum f B  setsum f (A Int B)"; 
8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

774 
by (stac (setsum_Un_Int RS sym) 1); 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

775 
by Auto_tac; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

776 
qed "setsum_Un"; 
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

777 

9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

778 
Goal "(setsum f (A{a}) :: nat) = \ 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

779 
\ (if a:A then setsum f A  f a else setsum f A)"; 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

780 
by (case_tac "finite A" 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

781 
by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
6162  782 
by (etac finite_induct 1); 
783 
by (auto_tac (claset(), simpset() addsimps [insert_Diff_if])); 

784 
by (dres_inst_tac [("a","a")] mk_disjoint_insert 1); 

8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

785 
by Auto_tac; 
5616  786 
qed_spec_mp "setsum_diff1"; 
7834  787 

9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

788 
val prems = Goal 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

789 
"[ A = B; !!x. x:B ==> f x = g x] ==> setsum f A = setsum g B"; 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

790 
by (case_tac "finite B" 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

791 
by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

792 
by (simp_tac (simpset() addsimps prems) 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

793 
by (subgoal_tac 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

794 
"ALL C. C <= B > (ALL x:C. f x = g x) > setsum f C = setsum g C" 1); 
9399  795 
by (asm_simp_tac (simpset() addsimps prems) 1); 
9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

796 
by (etac finite_induct 1); 
9338  797 
by (Simp_tac 1); 
9399  798 
by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1); 
9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

799 
by (Clarify_tac 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

800 
by (subgoal_tac "finite C" 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

801 
by (blast_tac (claset() addDs [rotate_prems 1 finite_subset]) 2); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

802 
by (subgoal_tac "C = insert x (C{x})" 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

803 
by (Blast_tac 2); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

804 
by (etac ssubst 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

805 
by (dtac spec 1); 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

806 
by (mp_tac 1); 
9399  807 
by (asm_full_simp_tac (simpset() addsimps Ball_def::prems) 1); 
9086
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

808 
qed "setsum_cong"; 
e4592e43e703
now setsum f A = 0 unless A is finite; proved setsum_cong
paulson
parents:
9074
diff
changeset

809 

7834  810 

811 
(*** Basic theorem about "choose". By Florian Kammueller, tidied by LCP ***) 

812 

813 
Goal "finite A ==> card {B. B <= A & card B = 0} = 1"; 

814 
by (asm_simp_tac (simpset() addcongs [conj_cong] 

10098
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

815 
addsimps [finite_subset RS card_0_eq]) 1); 
7834  816 
by (simp_tac (simpset() addcongs [rev_conj_cong]) 1); 
817 
qed "card_s_0_eq_empty"; 

818 

819 
Goal "[ finite M; x ~: M ] \ 

820 
\ ==> {s. s <= insert x M & card(s) = Suc k} \ 

821 
\ = {s. s <= M & card(s) = Suc k} Un \ 

822 
\ {s. EX t. t <= M & card(t) = k & s = insert x t}"; 

823 
by Safe_tac; 

824 
by (auto_tac (claset() addIs [finite_subset RS card_insert_disjoint], 

825 
simpset())); 

826 
by (dres_inst_tac [("x","xa  {x}")] spec 1); 

827 
by (subgoal_tac ("x ~: xa") 1); 

828 
by Auto_tac; 

829 
by (etac rev_mp 1 THEN stac card_Diff_singleton 1); 

7958  830 
by (auto_tac (claset() addIs [finite_subset], simpset())); 
7834  831 
qed "choose_deconstruct"; 
832 

8140  833 
Goal "[ finite(A); finite(B); f``A <= B; inj_on f A ] \ 
7834  834 
\ ==> card A <= card B"; 
835 
by (auto_tac (claset() addIs [card_mono], 

8140  836 
simpset() addsimps [card_image RS sym])); 
7834  837 
qed "card_inj_on_le"; 
838 

839 
Goal "[ finite A; finite B; \ 

8140  840 
\ f``A <= B; inj_on f A; g``B <= A; inj_on g B ] \ 
7834  841 
\ ==> card(A) = card(B)"; 
842 
by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset())); 

843 
qed "card_bij_eq"; 

844 

10098
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

845 
Goal "[ finite A; x ~: A ] \ 
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

846 
\ ==> card{B. EX C. C <= A & card(C) = k & B = insert x C} = \ 
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

847 
\ card {B. B <= A & card(B) = k}"; 
8140  848 
by (res_inst_tac [("f", "%s. s  {x}"), ("g","insert x")] card_bij_eq 1); 
10098
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

849 
by (res_inst_tac [("B","Pow(insert x A)")] finite_subset 1); 
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

850 
by (res_inst_tac [("B","Pow(A)")] finite_subset 3); 
8320  851 
by (REPEAT(Fast_tac 1)); 
7834  852 
(* arity *) 
8140  853 
by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def])); 
7834  854 
by (stac Diff_insert0 1); 
855 
by Auto_tac; 

856 
qed "constr_bij"; 

857 

858 
(* Main theorem: combinatorial theorem about number of subsets of a set *) 

10098
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

859 
Goal "(ALL A. finite A > card {B. B <= A & card B = k} = (card A choose k))"; 
7834  860 
by (induct_tac "k" 1); 
9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

861 
by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1); 
7834  862 
(* first 0 case finished *) 
7842
6858c98385c3
simplified and generalized n_sub_lemma and n_subsets
paulson
parents:
7834
diff
changeset

863 
(* prepare finite set induction *) 
6858c98385c3
simplified and generalized n_sub_lemma and n_subsets
paulson
parents:
7834
diff
changeset

864 
by (rtac allI 1 THEN rtac impI 1); 
7834  865 
(* second induction *) 
866 
by (etac finite_induct 1); 

7842
6858c98385c3
simplified and generalized n_sub_lemma and n_subsets
paulson
parents:
7834
diff
changeset

867 
by (ALLGOALS 
9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

868 
(asm_simp_tac (simpset() addcongs [conj_cong] 
10098
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

869 
addsimps [card_s_0_eq_empty, choose_deconstruct]))); 
7834  870 
by (stac card_Un_disjoint 1); 
9074
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

871 
by (force_tac (claset(), simpset() addsimps [constr_bij]) 4); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

872 
by (Force_tac 3); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

873 
by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2, 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

874 
inst "B" "Pow (insert ?x ?F)" finite_subset]) 2); 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

875 
by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2 
2313ddc415a1
inserted some "addsimps [subset_empty]"; also tidied (a lot)
paulson
parents:
9002
diff
changeset

876 
RSN (2, finite_subset)]) 1); 
7834  877 
qed "n_sub_lemma"; 
878 

10098
ab0a3188f398
deleted card_0_empty_iff because it is the same as card_0_eq;
paulson
parents:
9969
diff
changeset

879 
Goal "finite A ==> card {B. B <= A & card(B) = k} = ((card A) choose k)"; 
7834  880 
by (asm_simp_tac (simpset() addsimps [n_sub_lemma]) 1); 
881 
qed "n_subsets"; 