author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8981  fe1f3d52e027 
child 9002  a752f2499dae 
permissions  rwrr 
1465  1 
(* Title: HOL/Finite.thy 
923  2 
ID: $Id$ 
1531  3 
Author: Lawrence C Paulson & Tobias Nipkow 
4 
Copyright 1995 University of Cambridge & TU Muenchen 

923  5 

1531  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); 
44 
by (Simp_tac 1); 

4089  45 
by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1])); 
4304  46 
by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2); 
1264  47 
by (ALLGOALS Asm_simp_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*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

130 
Goal "finite B ==> !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 

5316  153 
Goal "finite A ==> (!a:A. finite(B a)) > finite(UN a:A. B a)"; 
154 
by (etac finite_induct 1); 

4153  155 
by (ALLGOALS Asm_simp_tac); 
4014  156 
bind_thm("finite_UnionI", ballI RSN (2, result() RS mp)); 
157 
Addsimps [finite_UnionI]; 

158 

159 
(** Sigma of finite sets **) 

160 

5069  161 
Goalw [Sigma_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

162 
"[ finite A; !a:A. finite(B a) ] ==> finite(SIGMA a:A. B a)"; 
4153  163 
by (blast_tac (claset() addSIs [finite_UnionI]) 1); 
4014  164 
bind_thm("finite_SigmaI", ballI RSN (2,result())); 
165 
Addsimps [finite_SigmaI]; 

3368  166 

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

169 
by (etac ssubst 1); 

170 
by (etac finite_SigmaI 1); 

171 
by Auto_tac; 

172 
qed "finite_Prod_UNIV"; 

173 

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

8320  175 
by (rtac (finite_Prod_UNIV) 1); 
176 
by (rtac finite 1); 

177 
by (rtac finite 1); 

8262  178 
qed "finite_Prod"; 
179 

3368  180 
(** The powerset of a finite set **) 
181 

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

182 
Goal "finite(Pow A) ==> finite A"; 
3368  183 
by (subgoal_tac "finite ((%x.{x})``A)" 1); 
3457  184 
by (rtac finite_subset 2); 
185 
by (assume_tac 3); 

3368  186 
by (ALLGOALS 
4830  187 
(fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD]))); 
3368  188 
val lemma = result(); 
189 

5069  190 
Goal "finite(Pow A) = finite A"; 
3457  191 
by (rtac iffI 1); 
192 
by (etac lemma 1); 

3368  193 
(*Opposite inclusion: finite A ==> finite (Pow A) *) 
3340  194 
by (etac finite_induct 1); 
195 
by (ALLGOALS 

196 
(asm_simp_tac 

4089  197 
(simpset() addsimps [finite_UnI, finite_imageI, Pow_insert]))); 
3368  198 
qed "finite_Pow_iff"; 
199 
AddIffs [finite_Pow_iff]; 

3340  200 

5069  201 
Goal "finite(r^1) = finite r"; 
3457  202 
by (subgoal_tac "r^1 = (%(x,y).(y,x))``r" 1); 
203 
by (Asm_simp_tac 1); 

204 
by (rtac iffI 1); 

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

3457  207 
by (etac finite_imageI 1); 
4746  208 
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

209 
by Auto_tac; 
5516  210 
by (rtac bexI 1); 
211 
by (assume_tac 2); 

4763  212 
by (Simp_tac 1); 
4746  213 
qed "finite_converse"; 
214 
AddIffs [finite_converse]; 

1531  215 

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

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

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

218 
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

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

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

221 

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

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

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

224 
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

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

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

228 

8889  229 
(* A bounded set of natural numbers is finite *) 
8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

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

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

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

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

234 
qed "bounded_nat_set_is_finite"; 
8889  235 

236 

1548  237 
section "Finite cardinality  'card'"; 
1531  238 

8981  239 
val cardR_emptyE = cardR.mk_cases "({},n) : cardR"; 
240 
val cardR_insertE = cardR.mk_cases "(insert a A,n) : cardR"; 

1531  241 

5626  242 
AddSEs [cardR_emptyE]; 
243 
AddSIs cardR.intrs; 

244 

245 
Goal "[ (A,n) : cardR ] ==> a : A > (? m. n = Suc m)"; 

6162  246 
by (etac cardR.induct 1); 
247 
by (Blast_tac 1); 

248 
by (Blast_tac 1); 

5626  249 
qed "cardR_SucD"; 
250 

251 
Goal "(A,m): cardR ==> (!n a. m = Suc n > a:A > (A{a},n) : cardR)"; 

6162  252 
by (etac cardR.induct 1); 
8911
c35b74bad518
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
paulson
parents:
8889
diff
changeset

253 
by Auto_tac; 
6162  254 
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

255 
by Auto_tac; 
7499  256 
by (ftac cardR_SucD 1); 
6162  257 
by (Blast_tac 1); 
5626  258 
val lemma = result(); 
259 

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

6162  261 
by (dtac lemma 1); 
262 
by (Asm_full_simp_tac 1); 

5626  263 
val lemma = result(); 
264 

265 
Goal "(A,m): cardR ==> (!n. (A,n) : cardR > n=m)"; 

6162  266 
by (etac cardR.induct 1); 
267 
by (safe_tac (claset() addSEs [cardR_insertE])); 

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

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

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

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

272 
by (Blast_tac 1); 

273 
by (subgoal_tac "? C. A = insert b C & B = insert a C" 1); 

274 
by (res_inst_tac [("x","A Int B")] exI 2); 

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

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

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

5626  278 
qed_spec_mp "cardR_determ"; 
279 

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

281 
by (etac cardR.induct 1); 

282 
by Auto_tac; 

283 
qed "cardR_imp_finite"; 

284 

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

286 
by (etac finite_induct 1); 

287 
by Auto_tac; 

288 
qed "finite_imp_cardR"; 

289 

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

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

292 
qed "card_equality"; 

293 

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

295 
by (Blast_tac 1); 

296 
qed "card_empty"; 

297 
Addsimps [card_empty]; 

298 

299 
Goal "x ~: A ==> \ 

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

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

302 
by Auto_tac; 

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

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

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

306 
val lemma = result(); 

307 

308 
Goalw [card_def] 

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

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

311 
by (rtac select_equality 1); 

312 
by (auto_tac (claset() addIs [finite_imp_cardR], 

313 
simpset() addcongs [conj_cong] 

314 
addsimps [symmetric card_def, 

315 
card_equality])); 

316 
qed "card_insert_disjoint"; 

317 
Addsimps [card_insert_disjoint]; 

318 

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

320 
Delrules [cardR_emptyE]; 

321 
Delrules cardR.intrs; 

322 

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

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

326 
by (Clarify_tac 1); 

327 
by (rotate_tac ~1 1); 

328 
by Auto_tac; 

329 
qed "card_0_eq"; 

330 
Addsimps[card_0_eq]; 

331 

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

334 
qed "card_insert_if"; 

335 

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

339 
by (Asm_simp_tac 1); 

340 
qed "card_Suc_Diff1"; 

341 

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

344 
qed "card_Diff_singleton"; 

345 

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

348 
qed "card_insert"; 

3352  349 

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

350 
Goal "finite A ==> card A <= card (insert x A)"; 
5626  351 
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

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

353 

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

354 
Goal "finite A ==> !B. B <= A > card(B) <= card(A)"; 
3352  355 
by (etac finite_induct 1); 
356 
by (Simp_tac 1); 

3708  357 
by (Clarify_tac 1); 
3352  358 
by (case_tac "x:B" 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

359 
by (dres_inst_tac [("A","B")] mk_disjoint_insert 1); 
8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
8554
diff
changeset

360 
by (asm_full_simp_tac (simpset() addsimps [le_SucI, subset_insert_iff]) 2); 
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
8554
diff
changeset

361 
by (force_tac (claset(), 
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
8554
diff
changeset

362 
simpset() addsimps [subset_insert_iff, finite_subset] 
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
8554
diff
changeset

363 
delsimps [insert_subset]) 1); 
3352  364 
qed_spec_mp "card_mono"; 
365 

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

366 

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

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

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

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

371 
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

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

373 

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

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

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

376 
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

377 
qed "card_Un_disjoint"; 
3352  378 

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

379 
Goal "[ finite A; B<=A ] ==> card A  card B = card (A  B)"; 
3352  380 
by (subgoal_tac "(AB) Un B = A" 1); 
381 
by (Blast_tac 2); 

3457  382 
by (rtac (add_right_cancel RS iffD1) 1); 
383 
by (rtac (card_Un_disjoint RS subst) 1); 

384 
by (etac ssubst 4); 

3352  385 
by (Blast_tac 3); 
386 
by (ALLGOALS 

387 
(asm_simp_tac 

4089  388 
(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

389 
add_diff_inverse, card_mono, finite_subset]))); 
3352  390 
qed "card_Diff_subset"; 
1531  391 

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

392 
Goal "[ finite A; x: A ] ==> card(A{x}) < card A"; 
2031  393 
by (rtac Suc_less_SucD 1); 
5626  394 
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1); 
395 
qed "card_Diff1_less"; 

1618  396 

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

397 
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

398 
by (case_tac "x: A" 1); 
5626  399 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le]))); 
400 
qed "card_Diff1_le"; 

1531  401 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

402 
Goalw [psubset_def] "finite B ==> !A. A < B > card(A) < card(B)"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

403 
by (etac finite_induct 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

404 
by (Simp_tac 1); 
3708  405 
by (Clarify_tac 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

406 
by (case_tac "x:A" 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

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

408 
by (dres_inst_tac [("A","A")]mk_disjoint_insert 1); 
4775  409 
by (Clarify_tac 1); 
410 
by (rotate_tac ~3 1); 

411 
by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1); 

3708  412 
by (Blast_tac 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

413 
(*2*) 
3708  414 
by (eres_inst_tac [("P","?a<?b")] notE 1); 
4775  415 
by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

416 
by (case_tac "A=F" 1); 
8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
8554
diff
changeset

417 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_SucI]))); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

418 
qed_spec_mp "psubset_card" ; 
3368  419 

7821  420 
Goal "[ A <= B; card B <= card A; finite B ] ==> A = B"; 
5626  421 
by (case_tac "A < B" 1); 
7497  422 
by (datac psubset_card 1 1); 
5626  423 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [psubset_eq]))); 
424 
qed "card_seteq"; 

425 

426 
Goal "[ finite B; A <= B; card A < card B ] ==> A < B"; 

427 
by (etac psubsetI 1); 

428 
by (Blast_tac 1); 

429 
qed "card_psubset"; 

430 

431 
(*** Cardinality of image ***) 

432 

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

434 
by (etac finite_induct 1); 

435 
by (Simp_tac 1); 

8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
8554
diff
changeset

436 
by (asm_simp_tac (simpset() addsimps [le_SucI,finite_imageI,card_insert_if]) 1); 
5626  437 
qed "card_image_le"; 
438 

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

440 
by (etac finite_induct 1); 

441 
by (ALLGOALS Asm_simp_tac); 

442 
by Safe_tac; 

443 
by (rewtac inj_on_def); 

444 
by (Blast_tac 1); 

445 
by (stac card_insert_disjoint 1); 

446 
by (etac finite_imageI 1); 

447 
by (Blast_tac 1); 

448 
by (Blast_tac 1); 

449 
qed_spec_mp "card_image"; 

450 

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

7497  452 
by (etac card_seteq 1); 
453 
by (dtac (card_image RS sym) 1); 

454 
by Auto_tac; 

5626  455 
qed "endo_inj_surj"; 
456 

457 
(*** Cardinality of the Powerset ***) 

458 

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

460 
by (etac finite_induct 1); 

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

462 
by (stac card_Un_disjoint 1); 

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

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

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

466 
by (rewtac inj_on_def); 

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

468 
qed "card_Pow"; 

469 

3368  470 

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

473 
Goal "finite C ==> finite (Union C) > \ 
3368  474 
\ (! c : C. k dvd card c) > \ 
475 
\ (! c1: C. ! c2: C. c1 ~= c2 > c1 Int c2 = {}) \ 

476 
\ > k dvd card(Union C)"; 

477 
by (etac finite_induct 1); 

478 
by (ALLGOALS Asm_simp_tac); 

3708  479 
by (Clarify_tac 1); 
3368  480 
by (stac card_Un_disjoint 1); 
481 
by (ALLGOALS 

4089  482 
(asm_full_simp_tac (simpset() 
3368  483 
addsimps [dvd_add, disjoint_eq_subset_Compl]))); 
484 
by (thin_tac "!c:F. ?PP(c)" 1); 

485 
by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1); 

3708  486 
by (Clarify_tac 1); 
3368  487 
by (ball_tac 1); 
488 
by (Blast_tac 1); 

489 
qed_spec_mp "dvd_partition"; 

490 

5616  491 

492 
(*** foldSet ***) 

493 

6141  494 
val empty_foldSetE = foldSet.mk_cases "({}, x) : foldSet f e"; 
5616  495 

496 
AddSEs [empty_foldSetE]; 

497 
AddIs foldSet.intrs; 

498 

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

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

501 
by Auto_tac; 

5626  502 
qed "Diff1_foldSet"; 
5616  503 

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

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

506 
by Auto_tac; 

507 
qed "foldSet_imp_finite"; 

508 

509 
Addsimps [foldSet_imp_finite]; 

510 

511 

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

513 
by (etac finite_induct 1); 

514 
by Auto_tac; 

515 
qed "finite_imp_foldSet"; 

516 

517 

518 
Open_locale "LC"; 

519 

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

520 
val f_lcomm = thm "lcomm"; 
5616  521 

522 

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

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

525 
by (induct_tac "n" 1); 

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

527 
by (etac foldSet.elim 1); 

528 
by (Blast_tac 1); 

529 
by (etac foldSet.elim 1); 

530 
by (Blast_tac 1); 

531 
by (Clarify_tac 1); 

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

533 
by (etac rev_mp 1); 

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

535 
by (rtac impI 1); 

536 
(** LEVEL 10 **) 

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

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

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

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

541 
by (Blast_tac 1); 

542 
(*case xa ~= xb*) 

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

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

545 
by (Clarify_tac 1); 

546 
by (subgoal_tac "Aa = insert xb Ab  {xa}" 1); 

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

548 
(** LEVEL 20 **) 

549 
by (subgoal_tac "card Aa <= card Ab" 1); 

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

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

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

7499  555 
by (ftac Diff1_foldSet 1 THEN assume_tac 1); 
5616  556 
by (subgoal_tac "ya = f xb x" 1); 
557 
by (Blast_tac 2); 

558 
by (subgoal_tac "(Ab  {xa}, x) : foldSet f e" 1); 

559 
by (Asm_full_simp_tac 2); 

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

5626  561 
by (blast_tac (claset() addDs [Diff1_foldSet]) 2); 
5616  562 
by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1); 
563 
val lemma = result(); 

564 

565 

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

567 
by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1); 

568 
qed "foldSet_determ"; 

569 

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

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

572 
qed "fold_equality"; 

573 

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

575 
by (Blast_tac 1); 

576 
qed "fold_empty"; 

577 
Addsimps [fold_empty]; 

578 

5626  579 

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

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

583 
by Auto_tac; 

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

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

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

587 
val lemma = result(); 

588 

589 
Goalw [fold_def] 

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

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

592 
by (rtac select_equality 1); 

593 
by (auto_tac (claset() addIs [finite_imp_foldSet], 

594 
simpset() addcongs [conj_cong] 

595 
addsimps [symmetric fold_def, 

596 
fold_equality])); 

597 
qed "fold_insert"; 

598 

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

599 
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

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

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

602 
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

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

604 

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

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

606 
\ ==> 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

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

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

609 
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

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

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

612 

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

613 
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

614 
\ ==> 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

615 
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

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

617 

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

620 
Delrules [empty_foldSetE]; 

621 
Delrules foldSet.intrs; 

622 

6024  623 
Close_locale "LC"; 
5616  624 

625 
Open_locale "ACe"; 

626 

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

627 
(*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

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

629 
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

630 

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

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

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

633 
val f_assoc = thm "assoc"; 
5616  634 

635 

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

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

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

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

640 
qed "f_left_commute"; 

641 

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

643 

644 
Goal "f e x = x"; 

645 
by (stac f_commute 1); 

646 
by (rtac f_ident 1); 

647 
qed "f_left_ident"; 

648 

649 
val f_idents = [f_left_ident, f_ident]; 

650 

651 
Goal "[ finite A; finite B ] \ 

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

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

654 
by (etac finite_induct 1); 

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

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

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

658 
qed "fold_Un_Int"; 

659 

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

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

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

663 
qed "fold_Un_disjoint"; 

664 

665 
Goal 

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

667 
\ fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)"; 

668 
by (etac finite_induct 1); 

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

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

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

672 
qed "fold_Un_disjoint2"; 

673 

6024  674 
Close_locale "ACe"; 
5616  675 

676 

8981  677 
(*** setsum: generalized summation over a set ***) 
5616  678 

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

6162  680 
by (Simp_tac 1); 
5616  681 
qed "setsum_empty"; 
682 
Addsimps [setsum_empty]; 

683 

684 
Goalw [setsum_def] 

685 
"[ 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

686 
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

687 
thm "plus_ac0_left_commute"]) 1); 
5616  688 
qed "setsum_insert"; 
689 
Addsimps [setsum_insert]; 

690 

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

691 
(*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

692 
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

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

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

695 
qed "card_eq_setsum"; 
5616  696 

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

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

698 
\ ==> 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

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

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

701 
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

702 
[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

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

704 

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

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

708 
by Auto_tac; 

709 
qed "setsum_Un_disjoint"; 

710 

711 
Goal "[ finite I ] \ 

712 
\ ==> (ALL i:I. finite (A i)) > (ALL i:I. ALL j:I. A i Int A j = {}) \ 

713 
\ > setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; 

714 
by (etac finite_induct 1); 

715 
by (Simp_tac 1); 

716 
by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1); 

717 
qed_spec_mp "setsum_UN_disjoint"; 

718 

719 
Goal "finite A ==> setsum (%x. f x + g x) A = setsum f A + setsum g A"; 

720 
by (etac finite_induct 1); 

721 
by Auto_tac; 

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

723 
qed "setsum_addf"; 

724 

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

726 

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

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

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

729 
\ 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

730 
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

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

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

733 

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

734 
Goal "finite F \ 
8963
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

735 
\ ==> (setsum f (F{a}) :: nat) = \ 
0d4abacae6aa
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
paulson
parents:
8911
diff
changeset

736 
\ (if a:F then setsum f F  f a else setsum f F)"; 
6162  737 
by (etac finite_induct 1); 
738 
by (auto_tac (claset(), simpset() addsimps [insert_Diff_if])); 

739 
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

740 
by Auto_tac; 
5616  741 
qed_spec_mp "setsum_diff1"; 
7834  742 

743 

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

745 

746 
Goal "finite S ==> (card S = 0) = (S = {})"; 

747 
by (auto_tac (claset() addDs [card_Suc_Diff1], 

748 
simpset())); 

749 
qed "card_0_empty_iff"; 

750 

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

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

753 
addsimps [finite_subset RS card_0_empty_iff]) 1); 

754 
by (simp_tac (simpset() addcongs [rev_conj_cong]) 1); 

755 
qed "card_s_0_eq_empty"; 

756 

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

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

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

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

761 
by Safe_tac; 

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

763 
simpset())); 

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

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

766 
by Auto_tac; 

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

7958  768 
by (auto_tac (claset() addIs [finite_subset], simpset())); 
7834  769 
qed "choose_deconstruct"; 
770 

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

8140  774 
simpset() addsimps [card_image RS sym])); 
7834  775 
qed "card_inj_on_le"; 
776 

777 
Goal "[ finite A; finite B; \ 

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

781 
qed "card_bij_eq"; 

782 

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

784 
\ ==> card{s. EX t. t <= M & card(t) = k & s = insert x t} = \ 

785 
\ card {s. s <= M & card(s) = k}"; 

8140  786 
by (res_inst_tac [("f", "%s. s  {x}"), ("g","insert x")] card_bij_eq 1); 
7834  787 
by (res_inst_tac [("B","Pow(insert x M)")] finite_subset 1); 
788 
by (res_inst_tac [("B","Pow(M)")] finite_subset 3); 

8320  789 
by (REPEAT(Fast_tac 1)); 
7834  790 
(* arity *) 
8140  791 
by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def])); 
7834  792 
by (stac Diff_insert0 1); 
793 
by Auto_tac; 

794 
qed "constr_bij"; 

795 

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

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

797 
Goal "(ALL A. finite A > card {s. s <= A & card s = k} = (card A choose k))"; 
7834  798 
by (induct_tac "k" 1); 
799 
by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1); 

800 
(* first 0 case finished *) 

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

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

802 
by (rtac allI 1 THEN rtac impI 1); 
7834  803 
(* second induction *) 
804 
by (etac finite_induct 1); 

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

805 
by (ALLGOALS 
6858c98385c3
simplified and generalized n_sub_lemma and n_subsets
paulson
parents:
7834
diff
changeset

806 
(simp_tac (simpset() addcongs [conj_cong] addsimps [card_s_0_eq_empty]))); 
7834  807 
by (stac choose_deconstruct 1); 
808 
by (assume_tac 1); 

809 
by (assume_tac 1); 

810 
by (stac card_Un_disjoint 1); 

811 
by (Force_tac 3); 

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

812 
(** LEVEL 10 **) 
6858c98385c3
simplified and generalized n_sub_lemma and n_subsets
paulson
parents:
7834
diff
changeset

813 
(* use bijection *) 
6858c98385c3
simplified and generalized n_sub_lemma and n_subsets
paulson
parents:
7834
diff
changeset

814 
by (force_tac (claset(), simpset() addsimps [constr_bij]) 3); 
7834  815 
(* finite goal *) 
816 
by (res_inst_tac [("B","Pow F")] finite_subset 1); 

817 
by (Blast_tac 1); 

818 
by (etac (finite_Pow_iff RS iffD2) 1); 

819 
(* finite goal *) 

820 
by (res_inst_tac [("B","Pow (insert x F)")] finite_subset 1); 

821 
by (Blast_tac 1); 

822 
by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2]) 1); 

823 
qed "n_sub_lemma"; 

824 

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

825 
Goal "finite M ==> card {s. s <= M & card(s) = k} = ((card M) choose k)"; 
7834  826 
by (asm_simp_tac (simpset() addsimps [n_sub_lemma]) 1); 
827 
qed "n_subsets"; 