src/HOL/Finite_Set.thy
 changeset 31380 f25536c0bb80 parent 31080 21ffc770ebc0 child 31438 a1c4c1500abe
```     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jun 02 15:53:34 2009 +0200
1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jun 02 16:23:43 2009 +0200
1.3 @@ -1926,34 +1926,40 @@
1.4  But now that we have @{text setsum} things are easy:
1.5  *}
1.6
1.7 -definition card :: "'a set \<Rightarrow> nat"
1.8 -where "card A = setsum (\<lambda>x. 1) A"
1.9 +definition card :: "'a set \<Rightarrow> nat" where
1.10 +  "card A = setsum (\<lambda>x. 1) A"
1.11 +
1.12 +lemmas card_eq_setsum = card_def
1.13
1.14  lemma card_empty [simp]: "card {} = 0"
1.16 -
1.17 -lemma card_infinite [simp]: "~ finite A ==> card A = 0"
1.19 -
1.20 -lemma card_eq_setsum: "card A = setsum (%x. 1) A"
1.22 +  by (simp add: card_def)
1.23
1.24  lemma card_insert_disjoint [simp]:
1.25    "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
1.27 +  by (simp add: card_def)
1.28
1.29  lemma card_insert_if:
1.30    "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
1.32 +  by (simp add: insert_absorb)
1.33 +
1.34 +lemma card_infinite [simp]: "~ finite A ==> card A = 0"
1.35 +  by (simp add: card_def)
1.36 +
1.37 +lemma card_ge_0_finite:
1.38 +  "card A > 0 \<Longrightarrow> finite A"
1.39 +  by (rule ccontr) simp
1.40
1.41  lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
1.42 -apply auto
1.43 -apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
1.44 -done
1.45 +  apply auto
1.46 +  apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
1.47 +  done
1.48 +
1.49 +lemma finite_UNIV_card_ge_0:
1.50 +  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
1.51 +  by (rule ccontr) simp
1.52
1.53  lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
1.54 -by auto
1.55 -
1.56 +  by auto
1.57
1.58  lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
1.59  apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
1.60 @@ -2049,6 +2055,24 @@
1.61         finite_subset [of _ "\<Union> (insert x F)"])
1.62  done
1.63
1.64 +lemma card_eq_UNIV_imp_eq_UNIV:
1.65 +  assumes fin: "finite (UNIV :: 'a set)"
1.66 +  and card: "card A = card (UNIV :: 'a set)"
1.67 +  shows "A = (UNIV :: 'a set)"
1.68 +proof
1.69 +  show "A \<subseteq> UNIV" by simp
1.70 +  show "UNIV \<subseteq> A"
1.71 +  proof
1.72 +    fix x
1.73 +    show "x \<in> A"
1.74 +    proof (rule ccontr)
1.75 +      assume "x \<notin> A"
1.76 +      then have "A \<subset> UNIV" by auto
1.77 +      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
1.78 +      with card show False by simp
1.79 +    qed
1.80 +  qed
1.81 +qed
1.82
1.83  text{*The form of a finite set of given cardinality*}
1.84
1.85 @@ -2078,6 +2102,17 @@
1.86   apply(auto intro:ccontr)
1.87  done
1.88
1.89 +lemma finite_fun_UNIVD2:
1.90 +  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1.91 +  shows "finite (UNIV :: 'b set)"
1.92 +proof -
1.93 +  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
1.94 +    by(rule finite_imageI)
1.95 +  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
1.96 +    by(rule UNIV_eq_I) auto
1.97 +  ultimately show "finite (UNIV :: 'b set)" by simp
1.98 +qed
1.99 +
1.100  lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
1.101  apply (cases "finite A")
1.102  apply (erule finite_induct)
```