author  paulson 
Thu, 24 Jun 2004 17:52:55 +0200  
changeset 15004  44ac09ba7213 
parent 14944  efbaecbdc05c 
child 15042  fa7d27ef7e59 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

4 
Additions by Jeremy Avigad in Feb 2004 
12396  5 
*) 
6 

7 
header {* Finite sets *} 

8 

14485  9 
theory Finite_Set = Divides + Power + Inductive: 
12396  10 

11 
subsection {* Collection of finite sets *} 

12 

13 
consts Finites :: "'a set set" 

13737  14 
syntax 
15 
finite :: "'a set => bool" 

16 
translations 

17 
"finite A" == "A : Finites" 

12396  18 

19 
inductive Finites 

20 
intros 

21 
emptyI [simp, intro!]: "{} : Finites" 

22 
insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" 

23 

24 
axclass finite \<subseteq> type 

25 
finite: "finite UNIV" 

26 

13737  27 
lemma ex_new_if_finite:  "does not depend on def of finite at all" 
14661  28 
assumes "\<not> finite (UNIV :: 'a set)" and "finite A" 
29 
shows "\<exists>a::'a. a \<notin> A" 

30 
proof  

31 
from prems have "A \<noteq> UNIV" by blast 

32 
thus ?thesis by blast 

33 
qed 

12396  34 

35 
lemma finite_induct [case_names empty insert, induct set: Finites]: 

36 
"finite F ==> 

37 
P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" 

38 
 {* Discharging @{text "x \<notin> F"} entails extra work. *} 

39 
proof  

13421  40 
assume "P {}" and 
41 
insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 

12396  42 
assume "finite F" 
43 
thus "P F" 

44 
proof induct 

45 
show "P {}" . 

46 
fix F x assume F: "finite F" and P: "P F" 

47 
show "P (insert x F)" 

48 
proof cases 

49 
assume "x \<in> F" 

50 
hence "insert x F = F" by (rule insert_absorb) 

51 
with P show ?thesis by (simp only:) 

52 
next 

53 
assume "x \<notin> F" 

54 
from F this P show ?thesis by (rule insert) 

55 
qed 

56 
qed 

57 
qed 

58 

59 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 

60 
"finite F ==> F \<subseteq> A ==> 

61 
P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==> 

62 
P F" 

63 
proof  

13421  64 
assume "P {}" and insert: 
65 
"!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 

12396  66 
assume "finite F" 
67 
thus "F \<subseteq> A ==> P F" 

68 
proof induct 

69 
show "P {}" . 

70 
fix F x assume "finite F" and "x \<notin> F" 

71 
and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 

72 
show "P (insert x F)" 

73 
proof (rule insert) 

74 
from i show "x \<in> A" by blast 

75 
from i have "F \<subseteq> A" by blast 

76 
with P show "P F" . 

77 
qed 

78 
qed 

79 
qed 

80 

81 
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" 

82 
 {* The union of two finite sets is finite. *} 

83 
by (induct set: Finites) simp_all 

84 

85 
lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A" 

86 
 {* Every subset of a finite set is finite. *} 

87 
proof  

88 
assume "finite B" 

89 
thus "!!A. A \<subseteq> B ==> finite A" 

90 
proof induct 

91 
case empty 

92 
thus ?case by simp 

93 
next 

94 
case (insert F x A) 

95 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" . 

96 
show "finite A" 

97 
proof cases 

98 
assume x: "x \<in> A" 

99 
with A have "A  {x} \<subseteq> F" by (simp add: subset_insert_iff) 

100 
with r have "finite (A  {x})" . 

101 
hence "finite (insert x (A  {x}))" .. 

102 
also have "insert x (A  {x}) = A" by (rule insert_Diff) 

103 
finally show ?thesis . 

104 
next 

105 
show "A \<subseteq> F ==> ?thesis" . 

106 
assume "x \<notin> A" 

107 
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) 

108 
qed 

109 
qed 

110 
qed 

111 

112 
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" 

113 
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) 

114 

115 
lemma finite_Int [simp, intro]: "finite F  finite G ==> finite (F Int G)" 

116 
 {* The converse obviously fails. *} 

117 
by (blast intro: finite_subset) 

118 

119 
lemma finite_insert [simp]: "finite (insert a A) = finite A" 

120 
apply (subst insert_is_Un) 

14208  121 
apply (simp only: finite_Un, blast) 
12396  122 
done 
123 

124 
lemma finite_empty_induct: 

125 
"finite A ==> 

126 
P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A  {a})) ==> P {}" 

127 
proof  

128 
assume "finite A" 

129 
and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A  {a})" 

130 
have "P (A  A)" 

131 
proof  

132 
fix c b :: "'a set" 

133 
presume c: "finite c" and b: "finite b" 

134 
and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y  {x})" 

135 
from c show "c \<subseteq> b ==> P (b  c)" 

136 
proof induct 

137 
case empty 

138 
from P1 show ?case by simp 

139 
next 

140 
case (insert F x) 

141 
have "P (b  F  {x})" 

142 
proof (rule P2) 

143 
from _ b show "finite (b  F)" by (rule finite_subset) blast 

144 
from insert show "x \<in> b  F" by simp 

145 
from insert show "P (b  F)" by simp 

146 
qed 

147 
also have "b  F  {x} = b  insert x F" by (rule Diff_insert [symmetric]) 

148 
finally show ?case . 

149 
qed 

150 
next 

151 
show "A \<subseteq> A" .. 

152 
qed 

153 
thus "P {}" by simp 

154 
qed 

155 

156 
lemma finite_Diff [simp]: "finite B ==> finite (B  Ba)" 

157 
by (rule Diff_subset [THEN finite_subset]) 

158 

159 
lemma finite_Diff_insert [iff]: "finite (A  insert a B) = finite (A  B)" 

160 
apply (subst Diff_insert) 

161 
apply (case_tac "a : A  B") 

162 
apply (rule finite_insert [symmetric, THEN trans]) 

14208  163 
apply (subst insert_Diff, simp_all) 
12396  164 
done 
165 

166 

13825  167 
subsubsection {* Image and Inverse Image over Finite Sets *} 
168 

169 
lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" 

170 
 {* The image of a finite set is finite. *} 

171 
by (induct set: Finites) simp_all 

172 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

173 
lemma finite_surj: "finite A ==> B <= f ` A ==> finite B" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

174 
apply (frule finite_imageI) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

175 
apply (erule finite_subset, assumption) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

176 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

177 

13825  178 
lemma finite_range_imageI: 
179 
"finite (range g) ==> finite (range (%x. f (g x)))" 

14208  180 
apply (drule finite_imageI, simp) 
13825  181 
done 
182 

12396  183 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
184 
proof  

185 
have aux: "!!A. finite (A  {}) = finite A" by simp 

186 
fix B :: "'a set" 

187 
assume "finite B" 

188 
thus "!!A. f`A = B ==> inj_on f A ==> finite A" 

189 
apply induct 

190 
apply simp 

191 
apply (subgoal_tac "EX y:A. f y = x & F = f ` (A  {y})") 

192 
apply clarify 

193 
apply (simp (no_asm_use) add: inj_on_def) 

14208  194 
apply (blast dest!: aux [THEN iffD1], atomize) 
12396  195 
apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl) 
14208  196 
apply (frule subsetD [OF equalityD2 insertI1], clarify) 
12396  197 
apply (rule_tac x = xa in bexI) 
198 
apply (simp_all add: inj_on_image_set_diff) 

199 
done 

200 
qed (rule refl) 

201 

202 

13825  203 
lemma inj_vimage_singleton: "inj f ==> f`{a} \<subseteq> {THE x. f x = a}" 
204 
 {* The inverse image of a singleton under an injective function 

205 
is included in a singleton. *} 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

206 
apply (auto simp add: inj_on_def) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

207 
apply (blast intro: the_equality [symmetric]) 
13825  208 
done 
209 

210 
lemma finite_vimageI: "[finite F; inj h] ==> finite (h ` F)" 

211 
 {* The inverse image of a finite set under an injective function 

212 
is finite. *} 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

213 
apply (induct set: Finites, simp_all) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

214 
apply (subst vimage_insert) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

215 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  216 
done 
217 

218 

12396  219 
subsubsection {* The finite UNION of finite sets *} 
220 

221 
lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)" 

222 
by (induct set: Finites) simp_all 

223 

224 
text {* 

225 
Strengthen RHS to 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

226 
@{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}? 
12396  227 

228 
We'd need to prove 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

229 
@{prop "finite C ==> ALL A B. (UNION A B) <= C > finite {x. x:A & B x \<noteq> {}}"} 
12396  230 
by induction. *} 
231 

232 
lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))" 

233 
by (blast intro: finite_UN_I finite_subset) 

234 

235 

236 
subsubsection {* Sigma of finite sets *} 

237 

238 
lemma finite_SigmaI [simp]: 

239 
"finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)" 

240 
by (unfold Sigma_def) (blast intro!: finite_UN_I) 

241 

242 
lemma finite_Prod_UNIV: 

243 
"finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)" 

244 
apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)") 

245 
apply (erule ssubst) 

14208  246 
apply (erule finite_SigmaI, auto) 
12396  247 
done 
248 

249 
instance unit :: finite 

250 
proof 

251 
have "finite {()}" by simp 

252 
also have "{()} = UNIV" by auto 

253 
finally show "finite (UNIV :: unit set)" . 

254 
qed 

255 

256 
instance * :: (finite, finite) finite 

257 
proof 

258 
show "finite (UNIV :: ('a \<times> 'b) set)" 

259 
proof (rule finite_Prod_UNIV) 

260 
show "finite (UNIV :: 'a set)" by (rule finite) 

261 
show "finite (UNIV :: 'b set)" by (rule finite) 

262 
qed 

263 
qed 

264 

265 

266 
subsubsection {* The powerset of a finite set *} 

267 

268 
lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A" 

269 
proof 

270 
assume "finite (Pow A)" 

271 
with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast 

272 
thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp 

273 
next 

274 
assume "finite A" 

275 
thus "finite (Pow A)" 

276 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

277 
qed 

278 

279 
lemma finite_converse [iff]: "finite (r^1) = finite r" 

280 
apply (subgoal_tac "r^1 = (%(x,y). (y,x))`r") 

281 
apply simp 

282 
apply (rule iffI) 

283 
apply (erule finite_imageD [unfolded inj_on_def]) 

284 
apply (simp split add: split_split) 

285 
apply (erule finite_imageI) 

14208  286 
apply (simp add: converse_def image_def, auto) 
12396  287 
apply (rule bexI) 
288 
prefer 2 apply assumption 

289 
apply simp 

290 
done 

291 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

292 

12396  293 
subsubsection {* Finiteness of transitive closure *} 
294 

295 
text {* (Thanks to Sidi Ehmety) *} 

296 

297 
lemma finite_Field: "finite r ==> finite (Field r)" 

298 
 {* A finite relation has a finite field (@{text "= domain \<union> range"}. *} 

299 
apply (induct set: Finites) 

300 
apply (auto simp add: Field_def Domain_insert Range_insert) 

301 
done 

302 

303 
lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r" 

304 
apply clarify 

305 
apply (erule trancl_induct) 

306 
apply (auto simp add: Field_def) 

307 
done 

308 

309 
lemma finite_trancl: "finite (r^+) = finite r" 

310 
apply auto 

311 
prefer 2 

312 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

313 
apply (rule finite_SigmaI) 

314 
prefer 3 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
13595
diff
changeset

315 
apply (blast intro: r_into_trancl' finite_subset) 
12396  316 
apply (auto simp add: finite_Field) 
317 
done 

318 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

319 
lemma finite_cartesian_product: "[ finite A; finite B ] ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

320 
finite (A <*> B)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

321 
by (rule finite_SigmaI) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

322 

12396  323 

324 
subsection {* Finite cardinality *} 

325 

326 
text {* 

327 
This definition, although traditional, is ugly to work with: @{text 

328 
"card A == LEAST n. EX f. A = {f i  i. i < n}"}. Therefore we have 

329 
switched to an inductive one: 

330 
*} 

331 

332 
consts cardR :: "('a set \<times> nat) set" 

333 

334 
inductive cardR 

335 
intros 

336 
EmptyI: "({}, 0) : cardR" 

337 
InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR" 

338 

339 
constdefs 

340 
card :: "'a set => nat" 

341 
"card A == THE n. (A, n) : cardR" 

342 

343 
inductive_cases cardR_emptyE: "({}, n) : cardR" 

344 
inductive_cases cardR_insertE: "(insert a A,n) : cardR" 

345 

346 
lemma cardR_SucD: "(A, n) : cardR ==> a : A > (EX m. n = Suc m)" 

347 
by (induct set: cardR) simp_all 

348 

349 
lemma cardR_determ_aux1: 

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

14208  351 
apply (induct set: cardR, auto) 
352 
apply (simp add: insert_Diff_if, auto) 

12396  353 
apply (drule cardR_SucD) 
354 
apply (blast intro!: cardR.intros) 

355 
done 

356 

357 
lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR" 

358 
by (drule cardR_determ_aux1) auto 

359 

360 
lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)" 

361 
apply (induct set: cardR) 

362 
apply (safe elim!: cardR_emptyE cardR_insertE) 

363 
apply (rename_tac B b m) 

364 
apply (case_tac "a = b") 

365 
apply (subgoal_tac "A = B") 

14208  366 
prefer 2 apply (blast elim: equalityE, blast) 
12396  367 
apply (subgoal_tac "EX C. A = insert b C & B = insert a C") 
368 
prefer 2 

369 
apply (rule_tac x = "A Int B" in exI) 

370 
apply (blast elim: equalityE) 

371 
apply (frule_tac A = B in cardR_SucD) 

372 
apply (blast intro!: cardR.intros dest!: cardR_determ_aux2) 

373 
done 

374 

375 
lemma cardR_imp_finite: "(A, n) : cardR ==> finite A" 

376 
by (induct set: cardR) simp_all 

377 

378 
lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR" 

379 
by (induct set: Finites) (auto intro!: cardR.intros) 

380 

381 
lemma card_equality: "(A,n) : cardR ==> card A = n" 

382 
by (unfold card_def) (blast intro: cardR_determ) 

383 

384 
lemma card_empty [simp]: "card {} = 0" 

385 
by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE) 

386 

387 
lemma card_insert_disjoint [simp]: 

388 
"finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" 

389 
proof  

390 
assume x: "x \<notin> A" 

391 
hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)" 

392 
apply (auto intro!: cardR.intros) 

393 
apply (rule_tac A1 = A in finite_imp_cardR [THEN exE]) 

394 
apply (force dest: cardR_imp_finite) 

395 
apply (blast intro!: cardR.intros intro: cardR_determ) 

396 
done 

397 
assume "finite A" 

398 
thus ?thesis 

399 
apply (simp add: card_def aux) 

400 
apply (rule the_equality) 

401 
apply (auto intro: finite_imp_cardR 

402 
cong: conj_cong simp: card_def [symmetric] card_equality) 

403 
done 

404 
qed 

405 

406 
lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" 

407 
apply auto 

14208  408 
apply (drule_tac a = x in mk_disjoint_insert, clarify) 
409 
apply (rotate_tac 1, auto) 

12396  410 
done 
411 

412 
lemma card_insert_if: 

413 
"finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" 

414 
by (simp add: insert_absorb) 

415 

416 
lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A  {x})) = card A" 

14302  417 
apply(rule_tac t = A in insert_Diff [THEN subst], assumption) 
418 
apply(simp del:insert_Diff_single) 

419 
done 

12396  420 

421 
lemma card_Diff_singleton: 

422 
"finite A ==> x: A ==> card (A  {x}) = card A  1" 

423 
by (simp add: card_Suc_Diff1 [symmetric]) 

424 

425 
lemma card_Diff_singleton_if: 

426 
"finite A ==> card (A{x}) = (if x : A then card A  1 else card A)" 

427 
by (simp add: card_Diff_singleton) 

428 

429 
lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A  {x}))" 

430 
by (simp add: card_insert_if card_Suc_Diff1) 

431 

432 
lemma card_insert_le: "finite A ==> card A <= card (insert x A)" 

433 
by (simp add: card_insert_if) 

434 

435 
lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" 

14208  436 
apply (induct set: Finites, simp, clarify) 
12396  437 
apply (subgoal_tac "finite A & A  {x} <= F") 
14208  438 
prefer 2 apply (blast intro: finite_subset, atomize) 
12396  439 
apply (drule_tac x = "A  {x}" in spec) 
440 
apply (simp add: card_Diff_singleton_if split add: split_if_asm) 

14208  441 
apply (case_tac "card A", auto) 
12396  442 
done 
443 

444 
lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B" 

445 
apply (simp add: psubset_def linorder_not_le [symmetric]) 

446 
apply (blast dest: card_seteq) 

447 
done 

448 

449 
lemma card_mono: "finite B ==> A <= B ==> card A <= card B" 

14208  450 
apply (case_tac "A = B", simp) 
12396  451 
apply (simp add: linorder_not_less [symmetric]) 
452 
apply (blast dest: card_seteq intro: order_less_imp_le) 

453 
done 

454 

455 
lemma card_Un_Int: "finite A ==> finite B 

456 
==> card A + card B = card (A Un B) + card (A Int B)" 

14208  457 
apply (induct set: Finites, simp) 
12396  458 
apply (simp add: insert_absorb Int_insert_left) 
459 
done 

460 

461 
lemma card_Un_disjoint: "finite A ==> finite B 

462 
==> A Int B = {} ==> card (A Un B) = card A + card B" 

463 
by (simp add: card_Un_Int) 

464 

465 
lemma card_Diff_subset: 

466 
"finite A ==> B <= A ==> card A  card B = card (A  B)" 

467 
apply (subgoal_tac "(A  B) Un B = A") 

468 
prefer 2 apply blast 

14331  469 
apply (rule nat_add_right_cancel [THEN iffD1]) 
12396  470 
apply (rule card_Un_disjoint [THEN subst]) 
471 
apply (erule_tac [4] ssubst) 

472 
prefer 3 apply blast 

473 
apply (simp_all add: add_commute not_less_iff_le 

474 
add_diff_inverse card_mono finite_subset) 

475 
done 

476 

477 
lemma card_Diff1_less: "finite A ==> x: A ==> card (A  {x}) < card A" 

478 
apply (rule Suc_less_SucD) 

479 
apply (simp add: card_Suc_Diff1) 

480 
done 

481 

482 
lemma card_Diff2_less: 

483 
"finite A ==> x: A ==> y: A ==> card (A  {x}  {y}) < card A" 

484 
apply (case_tac "x = y") 

485 
apply (simp add: card_Diff1_less) 

486 
apply (rule less_trans) 

487 
prefer 2 apply (auto intro!: card_Diff1_less) 

488 
done 

489 

490 
lemma card_Diff1_le: "finite A ==> card (A  {x}) <= card A" 

491 
apply (case_tac "x : A") 

492 
apply (simp_all add: card_Diff1_less less_imp_le) 

493 
done 

494 

495 
lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B" 

14208  496 
by (erule psubsetI, blast) 
12396  497 

14889  498 
lemma insert_partition: 
499 
"[ x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 > c1 \<inter> c2 = {}] 

500 
==> x \<inter> \<Union> F = {}" 

501 
by auto 

502 

503 
(* main cardinality theorem *) 

504 
lemma card_partition [rule_format]: 

505 
"finite C ==> 

506 
finite (\<Union> C) > 

507 
(\<forall>c\<in>C. card c = k) > 

508 
(\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 > c1 \<inter> c2 = {}) > 

509 
k * card(C) = card (\<Union> C)" 

510 
apply (erule finite_induct, simp) 

511 
apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 

512 
finite_subset [of _ "\<Union> (insert x F)"]) 

513 
done 

514 

12396  515 

516 
subsubsection {* Cardinality of image *} 

517 

518 
lemma card_image_le: "finite A ==> card (f ` A) <= card A" 

14208  519 
apply (induct set: Finites, simp) 
12396  520 
apply (simp add: le_SucI finite_imageI card_insert_if) 
521 
done 

522 

523 
lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A" 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

524 
apply (induct set: Finites, simp_all, atomize, safe) 
14208  525 
apply (unfold inj_on_def, blast) 
12396  526 
apply (subst card_insert_disjoint) 
14208  527 
apply (erule finite_imageI, blast, blast) 
12396  528 
done 
529 

530 
lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A" 

531 
by (simp add: card_seteq card_image) 

532 

533 

534 
subsubsection {* Cardinality of the Powerset *} 

535 

536 
lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *) 

537 
apply (induct set: Finites) 

538 
apply (simp_all add: Pow_insert) 

14208  539 
apply (subst card_Un_disjoint, blast) 
540 
apply (blast intro: finite_imageI, blast) 

12396  541 
apply (subgoal_tac "inj_on (insert x) (Pow F)") 
542 
apply (simp add: card_image Pow_insert) 

543 
apply (unfold inj_on_def) 

544 
apply (blast elim!: equalityE) 

545 
done 

546 

547 
text {* 

548 
\medskip Relates to equivalence classes. Based on a theorem of 

549 
F. Kammüller's. The @{prop "finite C"} premise is redundant. 

550 
*} 

551 

552 
lemma dvd_partition: 

553 
"finite C ==> finite (Union C) ==> 

554 
ALL c : C. k dvd card c ==> 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

555 
(ALL c1: C. ALL c2: C. c1 \<noteq> c2 > c1 Int c2 = {}) ==> 
12396  556 
k dvd card (Union C)" 
14208  557 
apply (induct set: Finites, simp_all, clarify) 
12396  558 
apply (subst card_Un_disjoint) 
559 
apply (auto simp add: dvd_add disjoint_eq_subset_Compl) 

560 
done 

561 

562 

563 
subsection {* A fold functional for finite sets *} 

564 

565 
text {* 

566 
For @{text n} nonnegative we have @{text "fold f e {x1, ..., xn} = 

567 
f x1 (... (f xn e))"} where @{text f} is at least leftcommutative. 

568 
*} 

569 

570 
consts 

571 
foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set" 

572 

573 
inductive "foldSet f e" 

574 
intros 

575 
emptyI [intro]: "({}, e) : foldSet f e" 

576 
insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e" 

577 

578 
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e" 

579 

580 
constdefs 

581 
fold :: "('b => 'a => 'a) => 'a => 'b set => 'a" 

582 
"fold f e A == THE x. (A, x) : foldSet f e" 

583 

584 
lemma Diff1_foldSet: "(A  {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e" 

14208  585 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
12396  586 

587 
lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A" 

588 
by (induct set: foldSet) auto 

589 

590 
lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e" 

591 
by (induct set: Finites) auto 

592 

593 

594 
subsubsection {* Leftcommutative operations *} 

595 

596 
locale LC = 

597 
fixes f :: "'b => 'a => 'a" (infixl "\<cdot>" 70) 

598 
assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

599 

600 
lemma (in LC) foldSet_determ_aux: 

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

602 
(ALL y. (A, y) : foldSet f e > y = x)" 

603 
apply (induct n) 

604 
apply (auto simp add: less_Suc_eq) 

14208  605 
apply (erule foldSet.cases, blast) 
606 
apply (erule foldSet.cases, blast, clarify) 

12396  607 
txt {* force simplification of @{text "card A < card (insert ...)"}. *} 
608 
apply (erule rev_mp) 

609 
apply (simp add: less_Suc_eq_le) 

610 
apply (rule impI) 

611 
apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb") 

612 
apply (subgoal_tac "Aa = Ab") 

14208  613 
prefer 2 apply (blast elim!: equalityE, blast) 
12396  614 
txt {* case @{prop "xa \<notin> xb"}. *} 
615 
apply (subgoal_tac "Aa  {xb} = Ab  {xa} & xb : Aa & xa : Ab") 

14208  616 
prefer 2 apply (blast elim!: equalityE, clarify) 
12396  617 
apply (subgoal_tac "Aa = insert xb Ab  {xa}") 
618 
prefer 2 apply blast 

619 
apply (subgoal_tac "card Aa <= card Ab") 

620 
prefer 2 

621 
apply (rule Suc_le_mono [THEN subst]) 

622 
apply (simp add: card_Suc_Diff1) 

623 
apply (rule_tac A1 = "Aa  {xb}" and f1 = f in finite_imp_foldSet [THEN exE]) 

624 
apply (blast intro: foldSet_imp_finite finite_Diff) 

625 
apply (frule (1) Diff1_foldSet) 

626 
apply (subgoal_tac "ya = f xb x") 

627 
prefer 2 apply (blast del: equalityCE) 

628 
apply (subgoal_tac "(Ab  {xa}, x) : foldSet f e") 

629 
prefer 2 apply simp 

630 
apply (subgoal_tac "yb = f xa x") 

631 
prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet) 

632 
apply (simp (no_asm_simp) add: left_commute) 

633 
done 

634 

635 
lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x" 

636 
by (blast intro: foldSet_determ_aux [rule_format]) 

637 

638 
lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y" 

639 
by (unfold fold_def) (blast intro: foldSet_determ) 

640 

641 
lemma fold_empty [simp]: "fold f e {} = e" 

642 
by (unfold fold_def) blast 

643 

644 
lemma (in LC) fold_insert_aux: "x \<notin> A ==> 

645 
((insert x A, v) : foldSet f e) = 

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

647 
apply auto 

648 
apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) 

649 
apply (fastsimp dest: foldSet_imp_finite) 

650 
apply (blast intro: foldSet_determ) 

651 
done 

652 

653 
lemma (in LC) fold_insert: 

654 
"finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)" 

655 
apply (unfold fold_def) 

656 
apply (simp add: fold_insert_aux) 

657 
apply (rule the_equality) 

658 
apply (auto intro: finite_imp_foldSet 

659 
cong add: conj_cong simp add: fold_def [symmetric] fold_equality) 

660 
done 

661 

662 
lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)" 

14208  663 
apply (induct set: Finites, simp) 
12396  664 
apply (simp add: left_commute fold_insert) 
665 
done 

666 

667 
lemma (in LC) fold_nest_Un_Int: 

668 
"finite A ==> finite B 

669 
==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)" 

14208  670 
apply (induct set: Finites, simp) 
12396  671 
apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb) 
672 
done 

673 

674 
lemma (in LC) fold_nest_Un_disjoint: 

675 
"finite A ==> finite B ==> A Int B = {} 

676 
==> fold f e (A Un B) = fold f (fold f e B) A" 

677 
by (simp add: fold_nest_Un_Int) 

678 

679 
declare foldSet_imp_finite [simp del] 

680 
empty_foldSetE [rule del] foldSet.intros [rule del] 

681 
 {* Delete rules to do with @{text foldSet} relation. *} 

682 

683 

684 

685 
subsubsection {* Commutative monoids *} 

686 

687 
text {* 

688 
We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} 

689 
instead of @{text "'b => 'a => 'a"}. 

690 
*} 

691 

692 
locale ACe = 

693 
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) 

694 
and e :: 'a 

695 
assumes ident [simp]: "x \<cdot> e = x" 

696 
and commute: "x \<cdot> y = y \<cdot> x" 

697 
and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" 

698 

699 
lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

700 
proof  

701 
have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute) 

702 
also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc) 

703 
also have "z \<cdot> x = x \<cdot> z" by (simp only: commute) 

704 
finally show ?thesis . 

705 
qed 

706 

12718  707 
lemmas (in ACe) AC = assoc commute left_commute 
12396  708 

12693  709 
lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" 
12396  710 
proof  
711 
have "x \<cdot> e = x" by (rule ident) 

712 
thus ?thesis by (subst commute) 

713 
qed 

714 

715 
lemma (in ACe) fold_Un_Int: 

716 
"finite A ==> finite B ==> 

717 
fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)" 

14208  718 
apply (induct set: Finites, simp) 
13400  719 
apply (simp add: AC insert_absorb Int_insert_left 
13421  720 
LC.fold_insert [OF LC.intro]) 
12396  721 
done 
722 

723 
lemma (in ACe) fold_Un_disjoint: 

724 
"finite A ==> finite B ==> A Int B = {} ==> 

725 
fold f e (A Un B) = fold f e A \<cdot> fold f e B" 

726 
by (simp add: fold_Un_Int) 

727 

728 
lemma (in ACe) fold_Un_disjoint2: 

729 
"finite A ==> finite B ==> A Int B = {} ==> 

730 
fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B" 

731 
proof  

732 
assume b: "finite B" 

733 
assume "finite A" 

734 
thus "A Int B = {} ==> 

735 
fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B" 

736 
proof induct 

737 
case empty 

738 
thus ?case by simp 

739 
next 

740 
case (insert F x) 

13571  741 
have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))" 
12396  742 
by simp 
13571  743 
also have "... = (f o g) x (fold (f o g) e (F \<union> B))" 
13400  744 
by (rule LC.fold_insert [OF LC.intro]) 
13421  745 
(insert b insert, auto simp add: left_commute) 
13571  746 
also from insert have "fold (f o g) e (F \<union> B) = 
747 
fold (f o g) e F \<cdot> fold (f o g) e B" by blast 

748 
also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B" 

12396  749 
by (simp add: AC) 
13571  750 
also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)" 
13400  751 
by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert, 
14661  752 
auto simp add: left_commute) 
12396  753 
finally show ?case . 
754 
qed 

755 
qed 

756 

757 

758 
subsection {* Generalized summation over a set *} 

759 

760 
constdefs 

14738  761 
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" 
12396  762 
"setsum f A == if finite A then fold (op + o f) 0 A else 0" 
763 

764 
syntax 

14738  765 
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_:_. _)" [0, 51, 10] 10) 
12396  766 
syntax (xsymbols) 
14738  767 
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
14565  768 
syntax (HTML output) 
14738  769 
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
12396  770 
translations 
771 
"\<Sum>i:A. b" == "setsum (%i. b) A"  {* Beware of argument permutation! *} 

772 

773 

774 
lemma setsum_empty [simp]: "setsum f {} = 0" 

775 
by (simp add: setsum_def) 

776 

777 
lemma setsum_insert [simp]: 

778 
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" 

13365  779 
by (simp add: setsum_def 
14738  780 
LC.fold_insert [OF LC.intro] add_left_commute) 
12396  781 

14944  782 
lemma setsum_reindex [rule_format]: 
783 
"finite B ==> inj_on f B > setsum h (f ` B) = setsum (h \<circ> f) B" 

14485  784 
apply (rule finite_induct, assumption, force) 
785 
apply (rule impI, auto) 

786 
apply (simp add: inj_on_def) 

787 
apply (subgoal_tac "f x \<notin> f ` F") 

788 
apply (subgoal_tac "finite (f ` F)") 

789 
apply (auto simp add: setsum_insert) 

790 
apply (simp add: inj_on_def) 

14944  791 
done 
12396  792 

14944  793 
lemma setsum_reindex_id: 
794 
"finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)" 

14485  795 
by (auto simp add: setsum_reindex id_o) 
12396  796 

797 
lemma setsum_cong: 

798 
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" 

799 
apply (case_tac "finite B") 

14208  800 
prefer 2 apply (simp add: setsum_def, simp) 
12396  801 
apply (subgoal_tac "ALL C. C <= B > (ALL x:C. f x = g x) > setsum f C = setsum g C") 
802 
apply simp 

14208  803 
apply (erule finite_induct, simp) 
804 
apply (simp add: subset_insert_iff, clarify) 

12396  805 
apply (subgoal_tac "finite C") 
806 
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) 

807 
apply (subgoal_tac "C = insert x (C  {x})") 

808 
prefer 2 apply blast 

809 
apply (erule ssubst) 

810 
apply (drule spec) 

811 
apply (erule (1) notE impE) 

14302  812 
apply (simp add: Ball_def del:insert_Diff_single) 
12396  813 
done 
814 

14944  815 
lemma setsum_reindex_cong: 
816 
"[finite A; inj_on f A; B = f ` A; !!a. g a = h (f a)] 

817 
==> setsum h B = setsum g A" 

818 
by (simp add: setsum_reindex cong: setsum_cong) 

819 

14485  820 
lemma setsum_0: "setsum (%i. 0) A = 0" 
821 
apply (case_tac "finite A") 

822 
prefer 2 apply (simp add: setsum_def) 

823 
apply (erule finite_induct, auto) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

824 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

825 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

826 
lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

827 
apply (subgoal_tac "setsum f F = setsum (%x. 0) F") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

828 
apply (erule ssubst, rule setsum_0) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

829 
apply (rule setsum_cong, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

830 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

831 

14485  832 
lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A" 
833 
 {* Could allow many @{text "card"} proofs to be simplified. *} 

834 
by (induct set: Finites) auto 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

835 

14485  836 
lemma setsum_Un_Int: "finite A ==> finite B 
837 
==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" 

838 
 {* The reversed orientation looks more natural, but LOOPS as a simprule! *} 

839 
apply (induct set: Finites, simp) 

14738  840 
apply (simp add: add_ac Int_insert_left insert_absorb) 
14485  841 
done 
842 

843 
lemma setsum_Un_disjoint: "finite A ==> finite B 

844 
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" 

845 
apply (subst setsum_Un_Int [symmetric], auto) 

846 
done 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

847 

14485  848 
lemma setsum_UN_disjoint: 
849 
"finite I ==> (ALL i:I. finite (A i)) ==> 

850 
(ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}) ==> 

851 
setsum f (UNION I A) = setsum (%i. setsum f (A i)) I" 

852 
apply (induct set: Finites, simp, atomize) 

853 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 

854 
prefer 2 apply blast 

855 
apply (subgoal_tac "A x Int UNION F A = {}") 

856 
prefer 2 apply blast 

857 
apply (simp add: setsum_Un_disjoint) 

858 
done 

859 

860 
lemma setsum_Union_disjoint: 

861 
"finite C ==> (ALL A:C. finite A) ==> 

862 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ==> 

863 
setsum f (Union C) = setsum (setsum f) C" 

864 
apply (frule setsum_UN_disjoint [of C id f]) 

865 
apply (unfold Union_def id_def, assumption+) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

866 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

867 

14661  868 
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
869 
(\<Sum>x:A. (\<Sum>y:B x. f x y)) = 

870 
(\<Sum>z:(SIGMA x:A. B x). f (fst z) (snd z))" 

14485  871 
apply (subst Sigma_def) 
872 
apply (subst setsum_UN_disjoint) 

873 
apply assumption 

874 
apply (rule ballI) 

875 
apply (drule_tac x = i in bspec, assumption) 

14661  876 
apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
14485  877 
apply (rule finite_surj) 
878 
apply auto 

879 
apply (rule setsum_cong, rule refl) 

880 
apply (subst setsum_UN_disjoint) 

881 
apply (erule bspec, assumption) 

882 
apply auto 

883 
done 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

884 

14485  885 
lemma setsum_cartesian_product: "finite A ==> finite B ==> 
14661  886 
(\<Sum>x:A. (\<Sum>y:B. f x y)) = 
887 
(\<Sum>z:A <*> B. f (fst z) (snd z))" 

14485  888 
by (erule setsum_Sigma, auto); 
889 

890 
lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" 

891 
apply (case_tac "finite A") 

892 
prefer 2 apply (simp add: setsum_def) 

893 
apply (erule finite_induct, auto) 

14738  894 
apply (simp add: add_ac) 
14485  895 
done 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

896 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

897 
subsubsection {* Properties in more restricted classes of structures *} 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

898 

14485  899 
lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" 
900 
apply (case_tac "finite A") 

901 
prefer 2 apply (simp add: setsum_def) 

902 
apply (erule rev_mp) 

903 
apply (erule finite_induct, auto) 

904 
done 

905 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

906 
lemma setsum_eq_0_iff [simp]: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

907 
"finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

908 
by (induct set: Finites) auto 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

909 

14485  910 
lemma setsum_constant_nat [simp]: 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

911 
"finite A ==> (\<Sum>x: A. y) = (card A) * y" 
14740  912 
 {* Later generalized to any @{text comm_semiring_1_cancel}. *} 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

913 
by (erule finite_induct, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

914 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

915 
lemma setsum_Un: "finite A ==> finite B ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

916 
(setsum f (A Un B) :: nat) = setsum f A + setsum f B  setsum f (A Int B)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

917 
 {* For the natural numbers, we have subtraction. *} 
14738  918 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

919 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

920 
lemma setsum_Un_ring: "finite A ==> finite B ==> 
14738  921 
(setsum f (A Un B) :: 'a :: comm_ring_1) = 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

922 
setsum f A + setsum f B  setsum f (A Int B)" 
14738  923 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

924 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

925 
lemma setsum_diff1: "(setsum f (A  {a}) :: nat) = 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

926 
(if a:A then setsum f A  f a else setsum f A)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

927 
apply (case_tac "finite A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

928 
prefer 2 apply (simp add: setsum_def) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

929 
apply (erule finite_induct) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

930 
apply (auto simp add: insert_Diff_if) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

931 
apply (drule_tac a = a in mk_disjoint_insert, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

932 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

933 

14738  934 
lemma setsum_negf: "finite A ==> setsum (%x.  (f x)::'a::comm_ring_1) A = 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

935 
 setsum f A" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

936 
by (induct set: Finites, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

937 

14738  938 
lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::comm_ring_1)  g x) A = 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

939 
setsum f A  setsum g A" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

940 
by (simp add: diff_minus setsum_addf setsum_negf) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

941 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

942 
lemma setsum_nonneg: "[ finite A; 
14738  943 
\<forall>x \<in> A. (0::'a::ordered_semidom) \<le> f x ] ==> 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

944 
0 \<le> setsum f A"; 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

945 
apply (induct set: Finites, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

946 
apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

947 
apply (blast intro: add_mono) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

948 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

949 

14485  950 
subsubsection {* Cardinality of unions and Sigma sets *} 
951 

952 
lemma card_UN_disjoint: 

953 
"finite I ==> (ALL i:I. finite (A i)) ==> 

954 
(ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}) ==> 

955 
card (UNION I A) = setsum (%i. card (A i)) I" 

956 
apply (subst card_eq_setsum) 

957 
apply (subst finite_UN, assumption+) 

958 
apply (subgoal_tac "setsum (%i. card (A i)) I = 

959 
setsum (%i. (setsum (%x. 1) (A i))) I") 

960 
apply (erule ssubst) 

961 
apply (erule setsum_UN_disjoint, assumption+) 

962 
apply (rule setsum_cong) 

963 
apply simp+ 

964 
done 

965 

966 
lemma card_Union_disjoint: 

967 
"finite C ==> (ALL A:C. finite A) ==> 

968 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ==> 

969 
card (Union C) = setsum card C" 

970 
apply (frule card_UN_disjoint [of C id]) 

971 
apply (unfold Union_def id_def, assumption+) 

972 
done 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

973 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

974 
lemma SigmaI_insert: "y \<notin> A ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

975 
(SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

976 
by auto 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

977 

14485  978 
lemma card_cartesian_product_singleton: "finite A ==> 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

979 
card({x} <*> A) = card(A)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

980 
apply (subgoal_tac "inj_on (%y .(x,y)) A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

981 
apply (frule card_image, assumption) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

982 
apply (subgoal_tac "(Pair x ` A) = {x} <*> A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

983 
apply (auto simp add: inj_on_def) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

984 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

985 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

986 
lemma card_SigmaI [rule_format,simp]: "finite A ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

987 
(ALL a:A. finite (B a)) > 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

988 
card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

989 
apply (erule finite_induct, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

990 
apply (subst SigmaI_insert, assumption) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

991 
apply (subst card_Un_disjoint) 
14485  992 
apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

993 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

994 

14485  995 
lemma card_cartesian_product: "[ finite A; finite B ] ==> 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

996 
card (A <*> B) = card(A) * card(B)" 
14485  997 
by simp 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

998 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

999 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1000 
subsection {* Generalized product over a set *} 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1001 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1002 
constdefs 
14738  1003 
setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1004 
"setprod f A == if finite A then fold (op * o f) 1 A else 1" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1005 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1006 
syntax 
14738  1007 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_:_. _)" [0, 51, 10] 10) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1008 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1009 
syntax (xsymbols) 
14738  1010 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
14565  1011 
syntax (HTML output) 
14738  1012 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1013 
translations 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1014 
"\<Prod>i:A. b" == "setprod (%i. b) A"  {* Beware of argument permutation! *} 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1015 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1016 
lemma setprod_empty [simp]: "setprod f {} = 1" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1017 
by (auto simp add: setprod_def) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1018 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1019 
lemma setprod_insert [simp]: "[ finite A; a \<notin> A ] ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1020 
setprod f (insert a A) = f a * setprod f A" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1021 
by (auto simp add: setprod_def LC_def LC.fold_insert 
14738  1022 
mult_left_commute) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1023 

14748  1024 
lemma setprod_reindex [rule_format]: 
1025 
"finite B ==> inj_on f B > setprod h (f ` B) = setprod (h \<circ> f) B" 

14485  1026 
apply (rule finite_induct, assumption, force) 
1027 
apply (rule impI, auto) 

1028 
apply (simp add: inj_on_def) 

1029 
apply (subgoal_tac "f x \<notin> f ` F") 

1030 
apply (subgoal_tac "finite (f ` F)") 

1031 
apply (auto simp add: setprod_insert) 

1032 
apply (simp add: inj_on_def) 

14748  1033 
done 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1034 

14485  1035 
lemma setprod_reindex_id: "finite B ==> inj_on f B ==> 
1036 
setprod f B = setprod id (f ` B)" 

1037 
by (auto simp add: setprod_reindex id_o) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1038 

14661  1039 
lemma setprod_reindex_cong: "finite A ==> inj_on f A ==> 
14485  1040 
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" 
1041 
by (frule setprod_reindex, assumption, simp) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1042 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1043 
lemma setprod_cong: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1044 
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1045 
apply (case_tac "finite B") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1046 
prefer 2 apply (simp add: setprod_def, simp) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1047 
apply (subgoal_tac "ALL C. C <= B > (ALL x:C. f x = g x) > setprod f C = setprod g C") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1048 
apply simp 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1049 
apply (erule finite_induct, simp) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1050 
apply (simp add: subset_insert_iff, clarify) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1051 
apply (subgoal_tac "finite C") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1052 
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1053 
apply (subgoal_tac "C = insert x (C  {x})") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1054 
prefer 2 apply blast 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1055 
apply (erule ssubst) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1056 
apply (drule spec) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1057 
apply (erule (1) notE impE) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1058 
apply (simp add: Ball_def del:insert_Diff_single) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1059 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1060 

14485  1061 
lemma setprod_1: "setprod (%i. 1) A = 1" 
1062 
apply (case_tac "finite A") 

14738  1063 
apply (erule finite_induct, auto simp add: mult_ac) 
14485  1064 
apply (simp add: setprod_def) 
1065 
done 

1066 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1067 
lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1068 
apply (subgoal_tac "setprod f F = setprod (%x. 1) F") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1069 
apply (erule ssubst, rule setprod_1) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1070 
apply (rule setprod_cong, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1071 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1072 

14485  1073 
lemma setprod_Un_Int: "finite A ==> finite B 
1074 
==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" 

1075 
apply (induct set: Finites, simp) 

14738  1076 
apply (simp add: mult_ac insert_absorb) 
1077 
apply (simp add: mult_ac Int_insert_left insert_absorb) 

14485  1078 
done 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1079 

14485  1080 
lemma setprod_Un_disjoint: "finite A ==> finite B 
1081 
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" 

14738  1082 
apply (subst setprod_Un_Int [symmetric], auto simp add: mult_ac) 
14485  1083 
done 
1084 

1085 
lemma setprod_UN_disjoint: 

1086 
"finite I ==> (ALL i:I. finite (A i)) ==> 

1087 
(ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}) ==> 

1088 
setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" 

1089 
apply (induct set: Finites, simp, atomize) 

1090 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 

1091 
prefer 2 apply blast 

1092 
apply (subgoal_tac "A x Int UNION F A = {}") 

1093 
prefer 2 apply blast 

1094 
apply (simp add: setprod_Un_disjoint) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1095 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1096 

14485  1097 
lemma setprod_Union_disjoint: 
1098 
"finite C ==> (ALL A:C. finite A) ==> 

1099 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ==> 

1100 
setprod f (Union C) = setprod (setprod f) C" 

1101 
apply (frule setprod_UN_disjoint [of C id f]) 

1102 
apply (unfold Union_def id_def, assumption+) 

1103 
done 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1104 

14661  1105 
lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
1106 
(\<Prod>x:A. (\<Prod>y: B x. f x y)) = 

1107 
(\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))" 

14485  1108 
apply (subst Sigma_def) 
1109 
apply (subst setprod_UN_disjoint) 

1110 
apply assumption 

1111 
apply (rule ballI) 

1112 
apply (drule_tac x = i in bspec, assumption) 

14661  1113 
apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
14485  1114 
apply (rule finite_surj) 
1115 
apply auto 

1116 
apply (rule setprod_cong, rule refl) 

1117 
apply (subst setprod_UN_disjoint) 

1118 
apply (erule bspec, assumption) 

1119 
apply auto 

1120 
done 

1121 

14661  1122 
lemma setprod_cartesian_product: "finite A ==> finite B ==> 
1123 
(\<Prod>x:A. (\<Prod>y: B. f x y)) = 

1124 
(\<Prod>z:(A <*> B). f (fst z) (snd z))" 

14485  1125 
by (erule setprod_Sigma, auto) 
1126 

1127 
lemma setprod_timesf: "setprod (%x. f x * g x) A = 

1128 
(setprod f A * setprod g A)" 

1129 
apply (case_tac "finite A") 

14738  1130 
prefer 2 apply (simp add: setprod_def mult_ac) 
14485  1131 
apply (erule finite_induct, auto) 
14738  1132 
apply (simp add: mult_ac) 
14485  1133 
done 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1134 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1135 
subsubsection {* Properties in more restricted classes of structures *} 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1136 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1137 
lemma setprod_eq_1_iff [simp]: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1138 
"finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1139 
by (induct set: Finites) auto 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1140 

15004  1141 
lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1142 
apply (erule finite_induct) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1143 
apply (auto simp add: power_Suc) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1144 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1145 

15004  1146 
lemma setprod_zero: 
1147 
"finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1148 
apply (induct set: Finites, force, clarsimp) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1149 
apply (erule disjE, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1150 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1151 

15004  1152 
lemma setprod_nonneg [rule_format]: 
1153 
"(ALL x: A. (0::'a::ordered_idom) \<le> f x) > 0 \<le> setprod f A" 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1154 
apply (case_tac "finite A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1155 
apply (induct set: Finites, force, clarsimp) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1156 
apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1157 
apply (rule mult_mono, assumption+) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1158 
apply (auto simp add: setprod_def) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1159 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1160 

14738  1161 
lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1162 
> 0 < setprod f A" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1163 
apply (case_tac "finite A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1164 
apply (induct set: Finites, force, clarsimp) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1165 
apply (subgoal_tac "0 * 0 < f x * setprod f F", force) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1166 
apply (rule mult_strict_mono, assumption+) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1167 
apply (auto simp add: setprod_def) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1168 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1169 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1170 
lemma setprod_nonzero [rule_format]: 
14738  1171 
"(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 > x = 0  y = 0) ==> 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1172 
finite A ==> (ALL x: A. f x \<noteq> (0::'a)) > setprod f A \<noteq> 0" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1173 
apply (erule finite_induct, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1174 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1175 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1176 
lemma setprod_zero_eq: 
14738  1177 
"(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 > x = 0  y = 0) ==> 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1178 
finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1179 
apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1180 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1181 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1182 
lemma setprod_nonzero_field: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1183 
"finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1184 
apply (rule setprod_nonzero, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1185 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1186 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1187 
lemma setprod_zero_eq_field: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1188 
"finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1189 
apply (rule setprod_zero_eq, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1190 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1191 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1192 
lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1193 
(setprod f (A Un B) :: 'a ::{field}) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1194 
= setprod f A * setprod f B / setprod f (A Int B)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1195 
apply (subst setprod_Un_Int [symmetric], auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1196 
apply (subgoal_tac "finite (A Int B)") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1197 
apply (frule setprod_nonzero_field [of "A Int B" f], assumption) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1198 
apply (subst times_divide_eq_right [THEN sym], auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1199 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1200 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1201 
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1202 
(setprod f (A  {a}) :: 'a :: {field}) = 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1203 
(if a:A then setprod f A / f a else setprod f A)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1204 
apply (erule finite_induct) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1205 
apply (auto simp add: insert_Diff_if) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1206 
apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1207 
apply (erule ssubst) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1208 
apply (subst times_divide_eq_right [THEN sym]) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1209 
apply (auto simp add: mult_ac) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1210 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1211 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1212 
lemma setprod_inversef: "finite A ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1213 
ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1214 
setprod (inverse \<circ> f) A = inverse (setprod f A)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1215 
apply (erule finite_induct) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1216 
apply (simp, simp) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1217 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1218 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1219 
lemma setprod_dividef: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1220 
"[finite A; 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1221 
\<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})] 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1222 
==> setprod (%x. f x / g x) A = setprod f A / setprod g A" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1223 
apply (subgoal_tac 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1224 
"setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1225 
apply (erule ssubst) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1226 
apply (subst divide_inverse) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1227 
apply (subst setprod_timesf) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1228 
apply (subst setprod_inversef, assumption+, rule refl) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1229 
apply (rule setprod_cong, rule refl) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1230 
apply (subst divide_inverse, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1231 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1232 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1233 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1234 
subsection{* Min and Max of finite linearly ordered sets *} 
13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1235 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1236 
text{* Seemed easier to define directly than via fold. *} 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1237 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1238 
lemma ex_Max: fixes S :: "('a::linorder)set" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1239 
assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m" 
13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1240 
using fin 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1241 
proof (induct) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1242 
case empty thus ?case by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1243 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1244 
case (insert S x) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1245 
show ?case 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1246 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1247 
assume "S = {}" thus ?thesis by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1248 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1249 
assume nonempty: "S \<noteq> {}" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1250 
then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1251 
show ?thesis 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1252 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1253 
assume "x \<le> m" thus ?thesis using m by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1254 
next 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1255 
assume "~ x \<le> m" thus ?thesis using m 
14661  1256 
by(simp add:linorder_not_le order_less_le)(blast intro: order_trans) 
13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1257 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1258 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1259 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1260 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1261 
lemma ex_Min: fixes S :: "('a::linorder)set" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1262 
assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s" 
13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1263 
using fin 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1264 
proof (induct) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1265 
case empty thus ?case by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1266 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1267 
case (insert S x) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1268 
show ?case 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1269 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1270 
assume "S = {}" thus ?thesis by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1271 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1272 
assume nonempty: "S \<noteq> {}" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1273 
then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1274 
show ?thesis 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1275 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1276 
assume "m \<le> x" thus ?thesis using m by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1277 
next 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1278 
assume "~ m \<le> x" thus ?thesis using m 
14661  1279 
by(simp add:linorder_not_le order_less_le)(blast intro: order_trans) 
13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1280 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1281 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1282 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1283 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1284 
constdefs 
14661  1285 
Min :: "('a::linorder)set => 'a" 
1286 
"Min S == THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)" 

13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1287 

14661  1288 
Max :: "('a::linorder)set => 'a" 
1289 
"Max S == THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)" 

13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1290 

14661  1291 
lemma Min [simp]: 
1292 
assumes a: "finite S" "S \<noteq> {}" 

1293 
shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)") 

13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1294 
proof (unfold Min_def, rule theI') 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1295 
show "\<exists>!m. ?P m" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1296 
proof (rule ex_ex1I) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1297 
show "\<exists>m. ?P m" using ex_Min[OF a] by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1298 
next 
14661  1299 
fix m1 m2 assume "?P m1" and "?P m2" 
1300 
thus "m1 = m2" by (blast dest: order_antisym) 

13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1301 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1302 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1303 

14661  1304 
lemma Max [simp]: 
1305 
assumes a: "finite S" "S \<noteq> {}" 

1306 
shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)") 

13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1307 
proof (unfold Max_def, rule theI') 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1308 
show "\<exists>!m. ?P m" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1309 
proof (rule ex_ex1I) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1310 
show "\<exists>m. ?P m" using ex_Max[OF a] by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1311 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1312 
fix m1 m2 assume "?P m1" "?P m2" 
14661  1313 
thus "m1 = m2" by (blast dest: order_antisym) 
13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1314 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1315 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

1316 

14661  1317 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1318 
subsection {* Theorems about @{text "choose"} *} 
12396  1319 

1320 
text {* 

1321 
\medskip Basic theorem about @{text "choose"}. By Florian 

14661  1322 
Kamm\"uller, tidied by LCP. 
12396  1323 
*} 
1324 

1325 
lemma card_s_0_eq_empty: 

1326 
"finite A ==> card {B. B \<subseteq> A & card B = 0} = 1" 

1327 
apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) 

1328 
apply (simp cong add: rev_conj_cong) 

1329 
done 

1330 

1331 
lemma choose_deconstruct: "finite M ==> x \<notin> M 

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

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

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

1335 
apply safe 

1336 
apply (auto intro: finite_subset [THEN card_insert_disjoint]) 

1337 
apply (drule_tac x = "xa  {x}" in spec) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1338 
apply (subgoal_tac "x \<notin> xa", auto) 
12396  1339 
apply (erule rev_mp, subst card_Diff_singleton) 
1340 
apply (auto intro: finite_subset) 

1341 
done 

1342 

1343 
lemma card_inj_on_le: 

14748  1344 
"[inj_on f A; f ` A \<subseteq> B; finite B ] ==> card A \<le> card B" 
1345 
apply (subgoal_tac "finite A") 

1346 
apply (force intro: card_mono simp add: card_image [symmetric]) 

14944  1347 
apply (blast intro: finite_imageD dest: finite_subset) 
14748  1348 
done 
12396  1349 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1350 
lemma card_bij_eq: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1351 
"[inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; 
13595  1352 
finite A; finite B ] ==> card A = card B" 
12396  1353 
by (auto intro: le_anti_sym card_inj_on_le) 
1354 

13595  1355 
text{*There are as many subsets of @{term A} having cardinality @{term k} 
1356 
as there are sets obtained from the former by inserting a fixed element 

1357 
@{term x} into each.*} 

1358 
lemma constr_bij: 

1359 
"[finite A; x \<notin> A] ==> 

1360 
card {B. EX C. C <= A & card(C) = k & B = insert x C} = 

12396  1361 
card {B. B <= A & card(B) = k}" 
1362 
apply (rule_tac f = "%s. s  {x}" and g = "insert x" in card_bij_eq) 

13595  1363 
apply (auto elim!: equalityE simp add: inj_on_def) 
1364 
apply (subst Diff_insert0, auto) 

1365 
txt {* finiteness of the two sets *} 

1366 
apply (rule_tac [2] B = "Pow (A)" in finite_subset) 

1367 
apply (rule_tac B = "Pow (insert x A)" in finite_subset) 

1368 
apply fast+ 

12396  1369 
done 
1370 

1371 
text {* 

1372 
Main theorem: combinatorial statement about number of subsets of a set. 

1373 
*} 

1374 

1375 
lemma n_sub_lemma: 

1376 
"!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" 

1377 
apply (induct k) 

14208  1378 
apply (simp add: card_s_0_eq_empty, atomize) 
12396  1379 
apply (rotate_tac 1, erule finite_induct) 
13421  1380 
apply (simp_all (no_asm_simp) cong add: conj_cong 
1381 
add: card_s_0_eq_empty choose_deconstruct) 

12396  1382 
apply (subst card_Un_disjoint) 
1383 
prefer 4 apply (force simp add: constr_bij) 

1384 
prefer 3 apply force 

1385 
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] 

2298d5b8e530
renamed theory Finite to Finite_Set and converted;
