(* Title: HOL/Finite_Set.thy
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
with contributions by Jeremy Avigad and Andrei Popescu
*)
section \Finite sets\
theory Finite_Set
imports Product_Type Sum_Type Nat
begin
subsection \Predicate for finite sets\
context
notes [[inductive_internals]]
begin
inductive finite :: "'a set \ bool"
where
emptyI [simp, intro!]: "finite {}"
| insertI [simp, intro!]: "finite A \ finite (insert a A)"
end
simproc_setup finite_Collect ("finite (Collect P)") = \K Set_Comprehension_Pointfree.simproc\
declare [[simproc del: finite_Collect]]
lemma finite_induct [case_names empty insert, induct set: finite]:
\ \Discharging \x \ F\ entails extra work.\
assumes "finite F"
assumes "P {}"
and insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)"
shows "P F"
using \finite F\
proof induct
show "P {}" by fact
fix x F assume F: "finite F" and P: "P F"
show "P (insert x F)"
proof cases
assume "x \ F"
hence "insert x F = F" by (rule insert_absorb)
with P show ?thesis by (simp only:)
next
assume "x \ F"
from F this P show ?thesis by (rule insert)
qed
qed
lemma infinite_finite_induct [case_names infinite empty insert]:
assumes infinite: "\A. \ finite A \ P A"
assumes empty: "P {}"
assumes insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)"
shows "P A"
proof (cases "finite A")
case False with infinite show ?thesis .
next
case True then show ?thesis by (induct A) (fact empty insert)+
qed
subsubsection \Choice principles\
lemma ex_new_if_finite: \ "does not depend on def of finite at all"
assumes "\ finite (UNIV :: 'a set)" and "finite A"
shows "\a::'a. a \ A"
proof -
from assms have "A \ UNIV" by blast
then show ?thesis by blast
qed
text \A finite choice principle. Does not need the SOME choice operator.\
lemma finite_set_choice:
"finite A \ \x\A. \y. P x y \ \f. \x\A. P x (f x)"
proof (induct rule: finite_induct)
case empty then show ?case by simp
next
case (insert a A)
then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
show ?case (is "EX f. ?P f")
proof
show "?P(%x. if x = a then b else f x)" using f ab by auto
qed
qed
subsubsection \Finite sets are the images of initial segments of natural numbers\
lemma finite_imp_nat_seg_image_inj_on:
assumes "finite A"
shows "\(n::nat) f. A = f ` {i. i < n} \ inj_on f {i. i < n}"
using assms
proof induct
case empty
show ?case
proof
show "\f. {} = f ` {i::nat. i < 0} \ inj_on f {i. i < 0}" by simp
qed
next
case (insert a A)
have notinA: "a \ A" by fact
from insert.hyps obtain n f
where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
hence "insert a A = f(n:=a) ` {i. i < Suc n}"
"inj_on (f(n:=a)) {i. i < Suc n}" using notinA
by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
thus ?case by blast
qed
lemma nat_seg_image_imp_finite:
"A = f ` {i::nat. i < n} \ finite A"
proof (induct n arbitrary: A)
case 0 thus ?case by simp
next
case (Suc n)
let ?B = "f ` {i. i < n}"
have finB: "finite ?B" by(rule Suc.hyps[OF refl])
show ?case
proof cases
assume "\k(\ k (\(n::nat) f. A = f ` {i::nat. i < n})"
by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
lemma finite_imp_inj_to_nat_seg:
assumes "finite A"
shows "\f n::nat. f ` A = {i. i < n} \ inj_on f A"
proof -
from finite_imp_nat_seg_image_inj_on[OF \finite A\]
obtain f and n::nat where bij: "bij_betw f {i. i k}"
by (simp add: le_eq_less_or_eq Collect_disj_eq)
subsubsection \Finiteness and common set operations\
lemma rev_finite_subset:
"finite B \ A \ B \ finite A"
proof (induct arbitrary: A rule: finite_induct)
case empty
then show ?case by simp
next
case (insert x F A)
have A: "A \ insert x F" and r: "A - {x} \ F \ finite (A - {x})" by fact+
show "finite A"
proof cases
assume x: "x \ A"
with A have "A - {x} \ F" by (simp add: subset_insert_iff)
with r have "finite (A - {x})" .
hence "finite (insert x (A - {x}))" ..
also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
finally show ?thesis .
next
show ?thesis when "A \ F"
using that by fact
assume "x \ A"
with A show "A \ F" by (simp add: subset_insert_iff)
qed
qed
lemma finite_subset:
"A \ B \ finite B \ finite A"
by (rule rev_finite_subset)
lemma finite_UnI:
assumes "finite F" and "finite G"
shows "finite (F \ G)"
using assms by induct simp_all
lemma finite_Un [iff]:
"finite (F \ G) \ finite F \ finite G"
by (blast intro: finite_UnI finite_subset [of _ "F \ G"])
lemma finite_insert [simp]: "finite (insert a A) \ finite A"
proof -
have "finite {a} \ finite A \ finite A" by simp
then have "finite ({a} \ A) \ finite A" by (simp only: finite_Un)
then show ?thesis by simp
qed
lemma finite_Int [simp, intro]:
"finite F \ finite G \ finite (F \ G)"
by (blast intro: finite_subset)
lemma finite_Collect_conjI [simp, intro]:
"finite {x. P x} \ finite {x. Q x} \ finite {x. P x \ Q x}"
by (simp add: Collect_conj_eq)
lemma finite_Collect_disjI [simp]:
"finite {x. P x \ Q x} \ finite {x. P x} \ finite {x. Q x}"
by (simp add: Collect_disj_eq)
lemma finite_Diff [simp, intro]:
"finite A \ finite (A - B)"
by (rule finite_subset, rule Diff_subset)
lemma finite_Diff2 [simp]:
assumes "finite B"
shows "finite (A - B) \ finite A"
proof -
have "finite A \ finite((A - B) \ (A \ B))" by (simp add: Un_Diff_Int)
also have "\ \ finite (A - B)" using \finite B\ by simp
finally show ?thesis ..
qed
lemma finite_Diff_insert [iff]:
"finite (A - insert a B) \ finite (A - B)"
proof -
have "finite (A - B) \ finite (A - B - {a})" by simp
moreover have "A - insert a B = A - B - {a}" by auto
ultimately show ?thesis by simp
qed
lemma finite_compl[simp]:
"finite (A :: 'a set) \ finite (- A) \ finite (UNIV :: 'a set)"
by (simp add: Compl_eq_Diff_UNIV)
lemma finite_Collect_not[simp]:
"finite {x :: 'a. P x} \ finite {x. \ P x} \ finite (UNIV :: 'a set)"
by (simp add: Collect_neg_eq)
lemma finite_Union [simp, intro]:
"finite A \ (\M. M \ A \ finite M) \ finite(\A)"
by (induct rule: finite_induct) simp_all
lemma finite_UN_I [intro]:
"finite A \ (\a. a \ A \ finite (B a)) \ finite (\a\A. B a)"
by (induct rule: finite_induct) simp_all
lemma finite_UN [simp]:
"finite A \ finite (UNION A B) \ (\x\A. finite (B x))"
by (blast intro: finite_subset)
lemma finite_Inter [intro]:
"\A\M. finite A \ finite (\M)"
by (blast intro: Inter_lower finite_subset)
lemma finite_INT [intro]:
"\x\I. finite (A x) \ finite (\x\I. A x)"
by (blast intro: INT_lower finite_subset)
lemma finite_imageI [simp, intro]:
"finite F \ finite (h ` F)"
by (induct rule: finite_induct) simp_all
lemma finite_image_set [simp]:
"finite {x. P x} \ finite { f x | x. P x }"
by (simp add: image_Collect [symmetric])
lemma finite_image_set2:
"finite {x. P x} \ finite {y. Q y} \ finite {f x y | x y. P x \ Q y}"
by (rule finite_subset [where B = "\x \ {x. P x}. \y \ {y. Q y}. {f x y}"]) auto
lemma finite_imageD:
assumes "finite (f ` A)" and "inj_on f A"
shows "finite A"
using assms
proof (induct "f ` A" arbitrary: A)
case empty then show ?case by simp
next
case (insert x B)
then have B_A: "insert x B = f ` A" by simp
then obtain y where "x = f y" and "y \ A" by blast
from B_A \x \ B\ have "B = f ` A - {x}" by blast
with B_A \x \ B\ \x = f y\ \inj_on f A\ \y \ A\ have "B = f ` (A - {y})"
by (simp add: inj_on_image_set_diff Set.Diff_subset)
moreover from \inj_on f A\ have "inj_on f (A - {y})" by (rule inj_on_diff)
ultimately have "finite (A - {y})" by (rule insert.hyps)
then show "finite A" by simp
qed
lemma finite_surj:
"finite A \ B \ f ` A \ finite B"
by (erule finite_subset) (rule finite_imageI)
lemma finite_range_imageI:
"finite (range g) \ finite (range (\x. f (g x)))"
by (drule finite_imageI) (simp add: range_composition)
lemma finite_subset_image:
assumes "finite B"
shows "B \ f ` A \ \C\A. finite C \ B = f ` C"
using assms
proof induct
case empty then show ?case by simp
next
case insert then show ?case
by (clarsimp simp del: image_insert simp add: image_insert [symmetric])
blast
qed
lemma finite_vimage_IntI:
"finite F \ inj_on h A \ finite (h -` F \ A)"
apply (induct rule: finite_induct)
apply simp_all
apply (subst vimage_insert)
apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
done
lemma finite_finite_vimage_IntI:
assumes "finite F" and "\y. y \ F \ finite ((h -` {y}) \ A)"
shows "finite (h -` F \ A)"
proof -
have *: "h -` F \ A = (\ y\F. (h -` {y}) \ A)"
by blast
show ?thesis
by (simp only: * assms finite_UN_I)
qed
lemma finite_vimageI:
"finite F \ inj h \ finite (h -` F)"
using finite_vimage_IntI[of F h UNIV] by auto
lemma finite_vimageD': "\ finite (f -` A); A \ range f \ \ finite A"
by(auto simp add: subset_image_iff intro: finite_subset[rotated])
lemma finite_vimageD: "\ finite (h -` F); surj h \ \ finite F"
by(auto dest: finite_vimageD')
lemma finite_vimage_iff: "bij h \ finite (h -` F) \ finite F"
unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
lemma finite_Collect_bex [simp]:
assumes "finite A"
shows "finite {x. \y\A. Q x y} \ (\y\A. finite {x. Q x y})"
proof -
have "{x. \y\A. Q x y} = (\y\A. {x. Q x y})" by auto
with assms show ?thesis by simp
qed
lemma finite_Collect_bounded_ex [simp]:
assumes "finite {y. P y}"
shows "finite {x. \y. P y \ Q x y} \ (\y. P y \ finite {x. Q x y})"
proof -
have "{x. EX y. P y & Q x y} = (\y\{y. P y}. {x. Q x y})" by auto
with assms show ?thesis by simp
qed
lemma finite_Plus:
"finite A \ finite B \ finite (A <+> B)"
by (simp add: Plus_def)
lemma finite_PlusD:
fixes A :: "'a set" and B :: "'b set"
assumes fin: "finite (A <+> B)"
shows "finite A" "finite B"
proof -
have "Inl ` A \ A <+> B" by auto
then have "finite (Inl ` A :: ('a + 'b) set)" using fin by (rule finite_subset)
then show "finite A" by (rule finite_imageD) (auto intro: inj_onI)
next
have "Inr ` B \ A <+> B" by auto
then have "finite (Inr ` B :: ('a + 'b) set)" using fin by (rule finite_subset)
then show "finite B" by (rule finite_imageD) (auto intro: inj_onI)
qed
lemma finite_Plus_iff [simp]:
"finite (A <+> B) \ finite A \ finite B"
by (auto intro: finite_PlusD finite_Plus)
lemma finite_Plus_UNIV_iff [simp]:
"finite (UNIV :: ('a + 'b) set) \ finite (UNIV :: 'a set) \ finite (UNIV :: 'b set)"
by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff)
lemma finite_SigmaI [simp, intro]:
"finite A \ (\a. a\A \ finite (B a)) ==> finite (SIGMA a:A. B a)"
by (unfold Sigma_def) blast
lemma finite_SigmaI2:
assumes "finite {x\A. B x \ {}}"
and "\a. a \ A \ finite (B a)"
shows "finite (Sigma A B)"
proof -
from assms have "finite (Sigma {x\A. B x \ {}} B)" by auto
also have "Sigma {x:A. B x \ {}} B = Sigma A B" by auto
finally show ?thesis .
qed
lemma finite_cartesian_product:
"finite A \ finite B \ finite (A \ B)"
by (rule finite_SigmaI)
lemma finite_Prod_UNIV:
"finite (UNIV :: 'a set) \ finite (UNIV :: 'b set) \ finite (UNIV :: ('a \ 'b) set)"
by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)
lemma finite_cartesian_productD1:
assumes "finite (A \ B)" and "B \ {}"
shows "finite A"
proof -
from assms obtain n f where "A \ B = f ` {i::nat. i < n}"
by (auto simp add: finite_conv_nat_seg_image)
then have "fst ` (A \ B) = fst ` f ` {i::nat. i < n}" by simp
with \B \ {}\ have "A = (fst \ f) ` {i::nat. i < n}"
by (simp add: image_comp)
then have "\n f. A = f ` {i::nat. i < n}" by blast
then show ?thesis
by (auto simp add: finite_conv_nat_seg_image)
qed
lemma finite_cartesian_productD2:
assumes "finite (A \ B)" and "A \ {}"
shows "finite B"
proof -
from assms obtain n f where "A \ B = f ` {i::nat. i < n}"
by (auto simp add: finite_conv_nat_seg_image)
then have "snd ` (A \