1.1 --- a/src/HOL/Finite_Set.thy Tue Jan 18 09:44:29 2011 +0100
1.2 +++ b/src/HOL/Finite_Set.thy Fri Jan 21 09:41:59 2011 +0100
1.3 @@ -9,96 +9,59 @@
1.4 imports Option Power
1.5 begin
1.6
1.7 +-- {* FIXME move *}
1.8 +
1.9 +lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
1.10 + -- {* The inverse image of a singleton under an injective function
1.11 + is included in a singleton. *}
1.12 + apply (auto simp add: inj_on_def)
1.13 + apply (blast intro: the_equality [symmetric])
1.14 + done
1.15 +
1.16 subsection {* Predicate for finite sets *}
1.17
1.18 -inductive finite :: "'a set => bool"
1.19 +inductive finite :: "'a set \<Rightarrow> bool"
1.20 where
1.21 emptyI [simp, intro!]: "finite {}"
1.22 - | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
1.23 + | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
1.24 +
1.25 +lemma finite_induct [case_names empty insert, induct set: finite]:
1.26 + -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
1.27 + assumes "finite F"
1.28 + assumes "P {}"
1.29 + and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
1.30 + shows "P F"
1.31 +using `finite F` proof induct
1.32 + show "P {}" by fact
1.33 + fix x F assume F: "finite F" and P: "P F"
1.34 + show "P (insert x F)"
1.35 + proof cases
1.36 + assume "x \<in> F"
1.37 + hence "insert x F = F" by (rule insert_absorb)
1.38 + with P show ?thesis by (simp only:)
1.39 + next
1.40 + assume "x \<notin> F"
1.41 + from F this P show ?thesis by (rule insert)
1.42 + qed
1.43 +qed
1.44 +
1.45 +
1.46 +subsubsection {* Choice principles *}
1.47
1.48 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
1.49 assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
1.50 shows "\<exists>a::'a. a \<notin> A"
1.51 proof -
1.52 from assms have "A \<noteq> UNIV" by blast
1.53 - thus ?thesis by blast
1.54 + then show ?thesis by blast
1.55 qed
1.56
1.57 -lemma finite_induct [case_names empty insert, induct set: finite]:
1.58 - "finite F ==>
1.59 - P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
1.60 - -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
1.61 -proof -
1.62 - assume "P {}" and
1.63 - insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
1.64 - assume "finite F"
1.65 - thus "P F"
1.66 - proof induct
1.67 - show "P {}" by fact
1.68 - fix x F assume F: "finite F" and P: "P F"
1.69 - show "P (insert x F)"
1.70 - proof cases
1.71 - assume "x \<in> F"
1.72 - hence "insert x F = F" by (rule insert_absorb)
1.73 - with P show ?thesis by (simp only:)
1.74 - next
1.75 - assume "x \<notin> F"
1.76 - from F this P show ?thesis by (rule insert)
1.77 - qed
1.78 - qed
1.79 -qed
1.80 +text {* A finite choice principle. Does not need the SOME choice operator. *}
1.81
1.82 -lemma finite_ne_induct[case_names singleton insert, consumes 2]:
1.83 -assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
1.84 - \<lbrakk> \<And>x. P{x};
1.85 - \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
1.86 - \<Longrightarrow> P F"
1.87 -using fin
1.88 -proof induct
1.89 - case empty thus ?case by simp
1.90 -next
1.91 - case (insert x F)
1.92 - show ?case
1.93 - proof cases
1.94 - assume "F = {}"
1.95 - thus ?thesis using `P {x}` by simp
1.96 - next
1.97 - assume "F \<noteq> {}"
1.98 - thus ?thesis using insert by blast
1.99 - qed
1.100 -qed
1.101 -
1.102 -lemma finite_subset_induct [consumes 2, case_names empty insert]:
1.103 - assumes "finite F" and "F \<subseteq> A"
1.104 - and empty: "P {}"
1.105 - and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
1.106 - shows "P F"
1.107 -proof -
1.108 - from `finite F` and `F \<subseteq> A`
1.109 - show ?thesis
1.110 - proof induct
1.111 - show "P {}" by fact
1.112 - next
1.113 - fix x F
1.114 - assume "finite F" and "x \<notin> F" and
1.115 - P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
1.116 - show "P (insert x F)"
1.117 - proof (rule insert)
1.118 - from i show "x \<in> A" by blast
1.119 - from i have "F \<subseteq> A" by blast
1.120 - with P show "P F" .
1.121 - show "finite F" by fact
1.122 - show "x \<notin> F" by fact
1.123 - qed
1.124 - qed
1.125 -qed
1.126 -
1.127 -
1.128 -text{* A finite choice principle. Does not need the SOME choice operator. *}
1.129 lemma finite_set_choice:
1.130 - "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
1.131 -proof (induct set: finite)
1.132 - case empty thus ?case by simp
1.133 + "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
1.134 +proof (induct rule: finite_induct)
1.135 + case empty then show ?case by simp
1.136 next
1.137 case (insert a A)
1.138 then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
1.139 @@ -109,16 +72,16 @@
1.140 qed
1.141
1.142
1.143 -text{* Finite sets are the images of initial segments of natural numbers: *}
1.144 +subsubsection {* Finite sets are the images of initial segments of natural numbers *}
1.145
1.146 lemma finite_imp_nat_seg_image_inj_on:
1.147 - assumes fin: "finite A"
1.148 - shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
1.149 -using fin
1.150 -proof induct
1.151 + assumes "finite A"
1.152 + shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}"
1.153 +using assms proof induct
1.154 case empty
1.155 - show ?case
1.156 - proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp
1.157 + show ?case
1.158 + proof
1.159 + show "\<exists>f. {} = f ` {i::nat. i < 0} \<and> inj_on f {i. i < 0}" by simp
1.160 qed
1.161 next
1.162 case (insert a A)
1.163 @@ -132,8 +95,8 @@
1.164 qed
1.165
1.166 lemma nat_seg_image_imp_finite:
1.167 - "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
1.168 -proof (induct n)
1.169 + "A = f ` {i::nat. i < n} \<Longrightarrow> finite A"
1.170 +proof (induct n arbitrary: A)
1.171 case 0 thus ?case by simp
1.172 next
1.173 case (Suc n)
1.174 @@ -152,12 +115,12 @@
1.175 qed
1.176
1.177 lemma finite_conv_nat_seg_image:
1.178 - "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
1.179 -by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
1.180 + "finite A \<longleftrightarrow> (\<exists>(n::nat) f. A = f ` {i::nat. i < n})"
1.181 + by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
1.182
1.183 lemma finite_imp_inj_to_nat_seg:
1.184 -assumes "finite A"
1.185 -shows "EX f n::nat. f`A = {i. i<n} & inj_on f A"
1.186 + assumes "finite A"
1.187 + shows "\<exists>f n::nat. f ` A = {i. i < n} \<and> inj_on f A"
1.188 proof -
1.189 from finite_imp_nat_seg_image_inj_on[OF `finite A`]
1.190 obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
1.191 @@ -168,160 +131,131 @@
1.192 thus ?thesis by blast
1.193 qed
1.194
1.195 -lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
1.196 -by(fastsimp simp: finite_conv_nat_seg_image)
1.197 +lemma finite_Collect_less_nat [iff]:
1.198 + "finite {n::nat. n < k}"
1.199 + by (fastsimp simp: finite_conv_nat_seg_image)
1.200
1.201 -text {* Finiteness and set theoretic constructions *}
1.202 +lemma finite_Collect_le_nat [iff]:
1.203 + "finite {n::nat. n \<le> k}"
1.204 + by (simp add: le_eq_less_or_eq Collect_disj_eq)
1.205
1.206 -lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
1.207 -by (induct set: finite) simp_all
1.208
1.209 -lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
1.210 - -- {* Every subset of a finite set is finite. *}
1.211 -proof -
1.212 - assume "finite B"
1.213 - thus "!!A. A \<subseteq> B ==> finite A"
1.214 - proof induct
1.215 - case empty
1.216 - thus ?case by simp
1.217 +subsubsection {* Finiteness and common set operations *}
1.218 +
1.219 +lemma rev_finite_subset:
1.220 + "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A"
1.221 +proof (induct arbitrary: A rule: finite_induct)
1.222 + case empty
1.223 + then show ?case by simp
1.224 +next
1.225 + case (insert x F A)
1.226 + have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F \<Longrightarrow> finite (A - {x})" by fact+
1.227 + show "finite A"
1.228 + proof cases
1.229 + assume x: "x \<in> A"
1.230 + with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
1.231 + with r have "finite (A - {x})" .
1.232 + hence "finite (insert x (A - {x}))" ..
1.233 + also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
1.234 + finally show ?thesis .
1.235 next
1.236 - case (insert x F A)
1.237 - have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
1.238 - show "finite A"
1.239 - proof cases
1.240 - assume x: "x \<in> A"
1.241 - with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
1.242 - with r have "finite (A - {x})" .
1.243 - hence "finite (insert x (A - {x}))" ..
1.244 - also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
1.245 - finally show ?thesis .
1.246 - next
1.247 - show "A \<subseteq> F ==> ?thesis" by fact
1.248 - assume "x \<notin> A"
1.249 - with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
1.250 - qed
1.251 + show "A \<subseteq> F ==> ?thesis" by fact
1.252 + assume "x \<notin> A"
1.253 + with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
1.254 qed
1.255 qed
1.256
1.257 -lemma rev_finite_subset: "finite B ==> A \<subseteq> B ==> finite A"
1.258 -by (rule finite_subset)
1.259 +lemma finite_subset:
1.260 + "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
1.261 + by (rule rev_finite_subset)
1.262
1.263 -lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
1.264 -by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
1.265 +lemma finite_UnI:
1.266 + assumes "finite F" and "finite G"
1.267 + shows "finite (F \<union> G)"
1.268 + using assms by induct simp_all
1.269
1.270 -lemma finite_Collect_disjI[simp]:
1.271 - "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
1.272 -by(simp add:Collect_disj_eq)
1.273 +lemma finite_Un [iff]:
1.274 + "finite (F \<union> G) \<longleftrightarrow> finite F \<and> finite G"
1.275 + by (blast intro: finite_UnI finite_subset [of _ "F \<union> G"])
1.276
1.277 -lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
1.278 - -- {* The converse obviously fails. *}
1.279 -by (blast intro: finite_subset)
1.280 -
1.281 -lemma finite_Collect_conjI [simp, intro]:
1.282 - "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
1.283 - -- {* The converse obviously fails. *}
1.284 -by(simp add:Collect_conj_eq)
1.285 -
1.286 -lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}"
1.287 -by(simp add: le_eq_less_or_eq)
1.288 -
1.289 -lemma finite_insert [simp]: "finite (insert a A) = finite A"
1.290 - apply (subst insert_is_Un)
1.291 - apply (simp only: finite_Un, blast)
1.292 - done
1.293 -
1.294 -lemma finite_Union[simp, intro]:
1.295 - "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
1.296 -by (induct rule:finite_induct) simp_all
1.297 -
1.298 -lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)"
1.299 -by (blast intro: Inter_lower finite_subset)
1.300 -
1.301 -lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)"
1.302 -by (blast intro: INT_lower finite_subset)
1.303 -
1.304 -lemma finite_empty_induct:
1.305 - assumes "finite A"
1.306 - and "P A"
1.307 - and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
1.308 - shows "P {}"
1.309 +lemma finite_insert [simp]: "finite (insert a A) \<longleftrightarrow> finite A"
1.310 proof -
1.311 - have "P (A - A)"
1.312 - proof -
1.313 - {
1.314 - fix c b :: "'a set"
1.315 - assume c: "finite c" and b: "finite b"
1.316 - and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
1.317 - have "c \<subseteq> b ==> P (b - c)"
1.318 - using c
1.319 - proof induct
1.320 - case empty
1.321 - from P1 show ?case by simp
1.322 - next
1.323 - case (insert x F)
1.324 - have "P (b - F - {x})"
1.325 - proof (rule P2)
1.326 - from _ b show "finite (b - F)" by (rule finite_subset) blast
1.327 - from insert show "x \<in> b - F" by simp
1.328 - from insert show "P (b - F)" by simp
1.329 - qed
1.330 - also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
1.331 - finally show ?case .
1.332 - qed
1.333 - }
1.334 - then show ?thesis by this (simp_all add: assms)
1.335 - qed
1.336 + have "finite {a} \<and> finite A \<longleftrightarrow> finite A" by simp
1.337 + then have "finite ({a} \<union> A) \<longleftrightarrow> finite A" by (simp only: finite_Un)
1.338 then show ?thesis by simp
1.339 qed
1.340
1.341 -lemma finite_Diff [simp, intro]: "finite A ==> finite (A - B)"
1.342 -by (rule Diff_subset [THEN finite_subset])
1.343 +lemma finite_Int [simp, intro]:
1.344 + "finite F \<or> finite G \<Longrightarrow> finite (F \<inter> G)"
1.345 + by (blast intro: finite_subset)
1.346 +
1.347 +lemma finite_Collect_conjI [simp, intro]:
1.348 + "finite {x. P x} \<or> finite {x. Q x} \<Longrightarrow> finite {x. P x \<and> Q x}"
1.349 + by (simp add: Collect_conj_eq)
1.350 +
1.351 +lemma finite_Collect_disjI [simp]:
1.352 + "finite {x. P x \<or> Q x} \<longleftrightarrow> finite {x. P x} \<and> finite {x. Q x}"
1.353 + by (simp add: Collect_disj_eq)
1.354 +
1.355 +lemma finite_Diff [simp, intro]:
1.356 + "finite A \<Longrightarrow> finite (A - B)"
1.357 + by (rule finite_subset, rule Diff_subset)
1.358
1.359 lemma finite_Diff2 [simp]:
1.360 - assumes "finite B" shows "finite (A - B) = finite A"
1.361 + assumes "finite B"
1.362 + shows "finite (A - B) \<longleftrightarrow> finite A"
1.363 proof -
1.364 - have "finite A \<longleftrightarrow> finite((A-B) Un (A Int B))" by(simp add: Un_Diff_Int)
1.365 - also have "\<dots> \<longleftrightarrow> finite(A-B)" using `finite B` by(simp)
1.366 + have "finite A \<longleftrightarrow> finite((A - B) \<union> (A \<inter> B))" by (simp add: Un_Diff_Int)
1.367 + also have "\<dots> \<longleftrightarrow> finite (A - B)" using `finite B` by simp
1.368 finally show ?thesis ..
1.369 qed
1.370
1.371 +lemma finite_Diff_insert [iff]:
1.372 + "finite (A - insert a B) \<longleftrightarrow> finite (A - B)"
1.373 +proof -
1.374 + have "finite (A - B) \<longleftrightarrow> finite (A - B - {a})" by simp
1.375 + moreover have "A - insert a B = A - B - {a}" by auto
1.376 + ultimately show ?thesis by simp
1.377 +qed
1.378 +
1.379 lemma finite_compl[simp]:
1.380 - "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
1.381 -by(simp add:Compl_eq_Diff_UNIV)
1.382 + "finite (A :: 'a set) \<Longrightarrow> finite (- A) \<longleftrightarrow> finite (UNIV :: 'a set)"
1.383 + by (simp add: Compl_eq_Diff_UNIV)
1.384
1.385 lemma finite_Collect_not[simp]:
1.386 - "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
1.387 -by(simp add:Collect_neg_eq)
1.388 + "finite {x :: 'a. P x} \<Longrightarrow> finite {x. \<not> P x} \<longleftrightarrow> finite (UNIV :: 'a set)"
1.389 + by (simp add: Collect_neg_eq)
1.390
1.391 -lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
1.392 - apply (subst Diff_insert)
1.393 - apply (case_tac "a : A - B")
1.394 - apply (rule finite_insert [symmetric, THEN trans])
1.395 - apply (subst insert_Diff, simp_all)
1.396 - done
1.397 +lemma finite_Union [simp, intro]:
1.398 + "finite A \<Longrightarrow> (\<And>M. M \<in> A \<Longrightarrow> finite M) \<Longrightarrow> finite(\<Union>A)"
1.399 + by (induct rule: finite_induct) simp_all
1.400
1.401 +lemma finite_UN_I [intro]:
1.402 + "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (\<Union>a\<in>A. B a)"
1.403 + by (induct rule: finite_induct) simp_all
1.404
1.405 -text {* Image and Inverse Image over Finite Sets *}
1.406 +lemma finite_UN [simp]:
1.407 + "finite A \<Longrightarrow> finite (UNION A B) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
1.408 + by (blast intro: finite_subset)
1.409
1.410 -lemma finite_imageI[simp, intro]: "finite F ==> finite (h ` F)"
1.411 - -- {* The image of a finite set is finite. *}
1.412 - by (induct set: finite) simp_all
1.413 +lemma finite_Inter [intro]:
1.414 + "\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)"
1.415 + by (blast intro: Inter_lower finite_subset)
1.416 +
1.417 +lemma finite_INT [intro]:
1.418 + "\<exists>x\<in>I. finite (A x) \<Longrightarrow> finite (\<Inter>x\<in>I. A x)"
1.419 + by (blast intro: INT_lower finite_subset)
1.420 +
1.421 +lemma finite_imageI [simp, intro]:
1.422 + "finite F \<Longrightarrow> finite (h ` F)"
1.423 + by (induct rule: finite_induct) simp_all
1.424
1.425 lemma finite_image_set [simp]:
1.426 "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
1.427 by (simp add: image_Collect [symmetric])
1.428
1.429 -lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
1.430 - apply (frule finite_imageI)
1.431 - apply (erule finite_subset, assumption)
1.432 - done
1.433 -
1.434 -lemma finite_range_imageI:
1.435 - "finite (range g) ==> finite (range (%x. f (g x)))"
1.436 - apply (drule finite_imageI, simp add: range_composition)
1.437 - done
1.438 -
1.439 -lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
1.440 +lemma finite_imageD:
1.441 + "finite (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> finite A"
1.442 proof -
1.443 have aux: "!!A. finite (A - {}) = finite A" by simp
1.444 fix B :: "'a set"
1.445 @@ -340,18 +274,28 @@
1.446 done
1.447 qed (rule refl)
1.448
1.449 +lemma finite_surj:
1.450 + "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"
1.451 + by (erule finite_subset) (rule finite_imageI)
1.452
1.453 -lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
1.454 - -- {* The inverse image of a singleton under an injective function
1.455 - is included in a singleton. *}
1.456 - apply (auto simp add: inj_on_def)
1.457 - apply (blast intro: the_equality [symmetric])
1.458 - done
1.459 +lemma finite_range_imageI:
1.460 + "finite (range g) \<Longrightarrow> finite (range (\<lambda>x. f (g x)))"
1.461 + by (drule finite_imageI) (simp add: range_composition)
1.462
1.463 -lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
1.464 - -- {* The inverse image of a finite set under an injective function
1.465 - is finite. *}
1.466 - apply (induct set: finite)
1.467 +lemma finite_subset_image:
1.468 + assumes "finite B"
1.469 + shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
1.470 +using assms proof induct
1.471 + case empty then show ?case by simp
1.472 +next
1.473 + case insert then show ?case
1.474 + by (clarsimp simp del: image_insert simp add: image_insert [symmetric])
1.475 + blast
1.476 +qed
1.477 +
1.478 +lemma finite_vimageI:
1.479 + "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
1.480 + apply (induct rule: finite_induct)
1.481 apply simp_all
1.482 apply (subst vimage_insert)
1.483 apply (simp add: finite_subset [OF inj_vimage_singleton])
1.484 @@ -369,40 +313,25 @@
1.485 lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
1.486 unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
1.487
1.488 +lemma finite_Collect_bex [simp]:
1.489 + assumes "finite A"
1.490 + shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"
1.491 +proof -
1.492 + have "{x. \<exists>y\<in>A. Q x y} = (\<Union>y\<in>A. {x. Q x y})" by auto
1.493 + with assms show ?thesis by simp
1.494 +qed
1.495
1.496 -text {* The finite UNION of finite sets *}
1.497 +lemma finite_Collect_bounded_ex [simp]:
1.498 + assumes "finite {y. P y}"
1.499 + shows "finite {x. \<exists>y. P y \<and> Q x y} \<longleftrightarrow> (\<forall>y. P y \<longrightarrow> finite {x. Q x y})"
1.500 +proof -
1.501 + have "{x. EX y. P y & Q x y} = (\<Union>y\<in>{y. P y}. {x. Q x y})" by auto
1.502 + with assms show ?thesis by simp
1.503 +qed
1.504
1.505 -lemma finite_UN_I[intro]:
1.506 - "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
1.507 -by (induct set: finite) simp_all
1.508 -
1.509 -text {*
1.510 - Strengthen RHS to
1.511 - @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
1.512 -
1.513 - We'd need to prove
1.514 - @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
1.515 - by induction. *}
1.516 -
1.517 -lemma finite_UN [simp]:
1.518 - "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
1.519 -by (blast intro: finite_subset)
1.520 -
1.521 -lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
1.522 - finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
1.523 -apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})")
1.524 - apply auto
1.525 -done
1.526 -
1.527 -lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow>
1.528 - finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})"
1.529 -apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})")
1.530 - apply auto
1.531 -done
1.532 -
1.533 -
1.534 -lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
1.535 -by (simp add: Plus_def)
1.536 +lemma finite_Plus:
1.537 + "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A <+> B)"
1.538 + by (simp add: Plus_def)
1.539
1.540 lemma finite_PlusD:
1.541 fixes A :: "'a set" and B :: "'b set"
1.542 @@ -410,42 +339,36 @@
1.543 shows "finite A" "finite B"
1.544 proof -
1.545 have "Inl ` A \<subseteq> A <+> B" by auto
1.546 - hence "finite (Inl ` A :: ('a + 'b) set)" using fin by(rule finite_subset)
1.547 - thus "finite A" by(rule finite_imageD)(auto intro: inj_onI)
1.548 + then have "finite (Inl ` A :: ('a + 'b) set)" using fin by (rule finite_subset)
1.549 + then show "finite A" by (rule finite_imageD) (auto intro: inj_onI)
1.550 next
1.551 have "Inr ` B \<subseteq> A <+> B" by auto
1.552 - hence "finite (Inr ` B :: ('a + 'b) set)" using fin by(rule finite_subset)
1.553 - thus "finite B" by(rule finite_imageD)(auto intro: inj_onI)
1.554 + then have "finite (Inr ` B :: ('a + 'b) set)" using fin by (rule finite_subset)
1.555 + then show "finite B" by (rule finite_imageD) (auto intro: inj_onI)
1.556 qed
1.557
1.558 -lemma finite_Plus_iff[simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
1.559 -by(auto intro: finite_PlusD finite_Plus)
1.560 +lemma finite_Plus_iff [simp]:
1.561 + "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
1.562 + by (auto intro: finite_PlusD finite_Plus)
1.563
1.564 -lemma finite_Plus_UNIV_iff[simp]:
1.565 - "finite (UNIV :: ('a + 'b) set) =
1.566 - (finite (UNIV :: 'a set) & finite (UNIV :: 'b set))"
1.567 -by(subst UNIV_Plus_UNIV[symmetric])(rule finite_Plus_iff)
1.568 -
1.569 -
1.570 -text {* Sigma of finite sets *}
1.571 +lemma finite_Plus_UNIV_iff [simp]:
1.572 + "finite (UNIV :: ('a + 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
1.573 + by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff)
1.574
1.575 lemma finite_SigmaI [simp, intro]:
1.576 - "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
1.577 + "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) ==> finite (SIGMA a:A. B a)"
1.578 by (unfold Sigma_def) blast
1.579
1.580 -lemma finite_cartesian_product: "[| finite A; finite B |] ==>
1.581 - finite (A <*> B)"
1.582 +lemma finite_cartesian_product:
1.583 + "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)"
1.584 by (rule finite_SigmaI)
1.585
1.586 lemma finite_Prod_UNIV:
1.587 - "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
1.588 - apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
1.589 - apply (erule ssubst)
1.590 - apply (erule finite_SigmaI, auto)
1.591 - done
1.592 + "finite (UNIV :: 'a set) \<Longrightarrow> finite (UNIV :: 'b set) \<Longrightarrow> finite (UNIV :: ('a \<times> 'b) set)"
1.593 + by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)
1.594
1.595 lemma finite_cartesian_productD1:
1.596 - "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
1.597 + "finite (A \<times> B) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> finite A"
1.598 apply (auto simp add: finite_conv_nat_seg_image)
1.599 apply (drule_tac x=n in spec)
1.600 apply (drule_tac x="fst o f" in spec)
1.601 @@ -474,37 +397,89 @@
1.602 apply (rule_tac x=k in image_eqI, auto)
1.603 done
1.604
1.605 -
1.606 -text {* The powerset of a finite set *}
1.607 -
1.608 -lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
1.609 +lemma finite_Pow_iff [iff]:
1.610 + "finite (Pow A) \<longleftrightarrow> finite A"
1.611 proof
1.612 assume "finite (Pow A)"
1.613 - with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
1.614 - thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
1.615 + then have "finite ((%x. {x}) ` A)" by (blast intro: finite_subset)
1.616 + then show "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
1.617 next
1.618 assume "finite A"
1.619 - thus "finite (Pow A)"
1.620 + then show "finite (Pow A)"
1.621 by induct (simp_all add: Pow_insert)
1.622 qed
1.623
1.624 -lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
1.625 -by(simp add: Pow_def[symmetric])
1.626 -
1.627 +corollary finite_Collect_subsets [simp, intro]:
1.628 + "finite A \<Longrightarrow> finite {B. B \<subseteq> A}"
1.629 + by (simp add: Pow_def [symmetric])
1.630
1.631 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
1.632 -by(blast intro: finite_subset[OF subset_Pow_Union])
1.633 + by (blast intro: finite_subset [OF subset_Pow_Union])
1.634
1.635
1.636 -lemma finite_subset_image:
1.637 - assumes "finite B"
1.638 - shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
1.639 -using assms proof(induct)
1.640 - case empty thus ?case by simp
1.641 +subsubsection {* Further induction rules on finite sets *}
1.642 +
1.643 +lemma finite_ne_induct [case_names singleton insert, consumes 2]:
1.644 + assumes "finite F" and "F \<noteq> {}"
1.645 + assumes "\<And>x. P {x}"
1.646 + and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
1.647 + shows "P F"
1.648 +using assms proof induct
1.649 + case empty then show ?case by simp
1.650 next
1.651 - case insert thus ?case
1.652 - by (clarsimp simp del: image_insert simp add: image_insert[symmetric])
1.653 - blast
1.654 + case (insert x F) then show ?case by cases auto
1.655 +qed
1.656 +
1.657 +lemma finite_subset_induct [consumes 2, case_names empty insert]:
1.658 + assumes "finite F" and "F \<subseteq> A"
1.659 + assumes empty: "P {}"
1.660 + and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
1.661 + shows "P F"
1.662 +using `finite F` `F \<subseteq> A` proof induct
1.663 + show "P {}" by fact
1.664 +next
1.665 + fix x F
1.666 + assume "finite F" and "x \<notin> F" and
1.667 + P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
1.668 + show "P (insert x F)"
1.669 + proof (rule insert)
1.670 + from i show "x \<in> A" by blast
1.671 + from i have "F \<subseteq> A" by blast
1.672 + with P show "P F" .
1.673 + show "finite F" by fact
1.674 + show "x \<notin> F" by fact
1.675 + qed
1.676 +qed
1.677 +
1.678 +lemma finite_empty_induct:
1.679 + assumes "finite A"
1.680 + assumes "P A"
1.681 + and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A - {a})"
1.682 + shows "P {}"
1.683 +proof -
1.684 + have "\<And>B. B \<subseteq> A \<Longrightarrow> P (A - B)"
1.685 + proof -
1.686 + fix B :: "'a set"
1.687 + assume "B \<subseteq> A"
1.688 + with `finite A` have "finite B" by (rule rev_finite_subset)
1.689 + from this `B \<subseteq> A` show "P (A - B)"
1.690 + proof induct
1.691 + case empty
1.692 + from `P A` show ?case by simp
1.693 + next
1.694 + case (insert b B)
1.695 + have "P (A - B - {b})"
1.696 + proof (rule remove)
1.697 + from `finite A` show "finite (A - B)" by induct auto
1.698 + from insert show "b \<in> A - B" by simp
1.699 + from insert show "P (A - B)" by simp
1.700 + qed
1.701 + also have "A - B - {b} = A - insert b B" by (rule Diff_insert [symmetric])
1.702 + finally show ?case .
1.703 + qed
1.704 + qed
1.705 + then have "P (A - A)" by blast
1.706 + then show ?thesis by simp
1.707 qed
1.708
1.709
1.710 @@ -610,7 +585,7 @@
1.711 by (induct set: fold_graph) auto
1.712
1.713 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
1.714 -by (induct set: finite) auto
1.715 +by (induct rule: finite_induct) auto
1.716
1.717
1.718 subsubsection{*From @{const fold_graph} to @{term fold}*}
1.719 @@ -949,13 +924,14 @@
1.720
1.721 lemma fold_image_1:
1.722 "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
1.723 - apply (induct set: finite)
1.724 + apply (induct rule: finite_induct)
1.725 apply simp by auto
1.726
1.727 lemma fold_image_Un_Int:
1.728 "finite A ==> finite B ==>
1.729 fold_image times g 1 A * fold_image times g 1 B =
1.730 fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)"
1.731 + apply (induct rule: finite_induct)
1.732 by (induct set: finite)
1.733 (auto simp add: mult_ac insert_absorb Int_insert_left)
1.734
1.735 @@ -981,7 +957,9 @@
1.736 ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
1.737 \<Longrightarrow> fold_image times g 1 (UNION I A) =
1.738 fold_image times (%i. fold_image times g 1 (A i)) 1 I"
1.739 -apply (induct set: finite, simp, atomize)
1.740 +apply (induct rule: finite_induct)
1.741 +apply simp
1.742 +apply atomize
1.743 apply (subgoal_tac "ALL i:F. x \<noteq> i")
1.744 prefer 2 apply blast
1.745 apply (subgoal_tac "A x Int UNION F A = {}")
1.746 @@ -1599,7 +1577,9 @@
1.747 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
1.748 shows "F g (UNION I A) = F (F g \<circ> A) I"
1.749 apply (insert assms)
1.750 -apply (induct set: finite, simp, atomize)
1.751 +apply (induct rule: finite_induct)
1.752 +apply simp
1.753 +apply atomize
1.754 apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
1.755 prefer 2 apply blast
1.756 apply (subgoal_tac "A x Int UNION Fa A = {}")
1.757 @@ -1975,7 +1955,9 @@
1.758 qed
1.759
1.760 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
1.761 -apply (induct set: finite, simp, clarify)
1.762 +apply (induct rule: finite_induct)
1.763 +apply simp
1.764 +apply clarify
1.765 apply (subgoal_tac "finite A & A - {x} <= F")
1.766 prefer 2 apply (blast intro: finite_subset, atomize)
1.767 apply (drule_tac x = "A - {x}" in spec)
1.768 @@ -2146,7 +2128,7 @@
1.769 subsubsection {* Cardinality of image *}
1.770
1.771 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
1.772 -apply (induct set: finite)
1.773 +apply (induct rule: finite_induct)
1.774 apply simp
1.775 apply (simp add: le_SucI card_insert_if)
1.776 done
1.777 @@ -2198,6 +2180,7 @@
1.778 using assms unfolding bij_betw_def
1.779 using finite_imageD[of f A] by auto
1.780
1.781 +
1.782 subsubsection {* Pigeonhole Principles *}
1.783
1.784 lemma pigeonhole: "card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
1.785 @@ -2267,7 +2250,7 @@
1.786 subsubsection {* Cardinality of the Powerset *}
1.787
1.788 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *)
1.789 -apply (induct set: finite)
1.790 +apply (induct rule: finite_induct)
1.791 apply (simp_all add: Pow_insert)
1.792 apply (subst card_Un_disjoint, blast)
1.793 apply (blast, blast)
1.794 @@ -2284,9 +2267,11 @@
1.795 ALL c : C. k dvd card c ==>
1.796 (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
1.797 k dvd card (Union C)"
1.798 -apply(frule finite_UnionD)
1.799 -apply(rotate_tac -1)
1.800 -apply (induct set: finite, simp_all, clarify)
1.801 +apply (frule finite_UnionD)
1.802 +apply (rotate_tac -1)
1.803 +apply (induct rule: finite_induct)
1.804 +apply simp_all
1.805 +apply clarify
1.806 apply (subst card_Un_disjoint)
1.807 apply (auto simp add: disjoint_eq_subset_Compl)
1.808 done
1.809 @@ -2294,7 +2279,7 @@
1.810
1.811 subsubsection {* Relating injectivity and surjectivity *}
1.812
1.813 -lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
1.814 +lemma finite_surj_inj: "finite A \<Longrightarrow> A \<subseteq> f ` A \<Longrightarrow> inj_on f A"
1.815 apply(rule eq_card_imp_inj_on, assumption)
1.816 apply(frule finite_imageI)
1.817 apply(drule (1) card_seteq)