(* Title: HOL/Finite_Set.thy
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
with contributions by Jeremy Avigad
*)
header {* Finite sets *}
theory Finite_Set
imports Option Power
begin
subsection {* Predicate for finite sets *}
inductive finite :: "'a set \ bool"
where
emptyI [simp, intro!]: "finite {}"
| insertI [simp, intro!]: "finite A \ finite (insert a A)"
lemma finite_induct [case_names empty insert, induct set: finite]:
-- {* Discharging @{text "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
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 "A \ F ==> ?thesis" 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_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)
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_vimageI:
"finite F \ inj h \ finite (h -` F)"
apply (induct rule: finite_induct)
apply simp_all
apply (subst vimage_insert)
apply (simp add: finite_subset [OF inj_vimage_singleton])
done
lemma finite_vimageD:
assumes fin: "finite (h -` F)" and surj: "surj h"
shows "finite F"
proof -
have "finite (h ` (h -` F))" using fin by (rule finite_imageI)
also have "h ` (h -` F) = F" using surj by (rule surj_image_vimage_eq)
finally show "finite F" .
qed
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_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_compose)
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 \ B) = snd ` f ` {i::nat. i < n}" by simp
with `A \ {}` have "B = (snd \ f) ` {i::nat. i < n}"
by (simp add: image_compose)
then have "\n f. B = f ` {i::nat. i < n}" by blast
then show ?thesis
by (auto simp add: finite_conv_nat_seg_image)
qed
lemma finite_Pow_iff [iff]:
"finite (Pow A) \ finite A"
proof
assume "finite (Pow A)"
then have "finite ((%x. {x}) ` A)" by (blast intro: finite_subset)
then show "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
next
assume "finite A"
then show "finite (Pow A)"
by induct (simp_all add: Pow_insert)
qed
corollary finite_Collect_subsets [simp, intro]:
"finite A \ finite {B. B \ A}"
by (simp add: Pow_def [symmetric])
lemma finite_UnionD: "finite(\A) \ finite A"
by (blast intro: finite_subset [OF subset_Pow_Union])
subsubsection {* Further induction rules on finite sets *}
lemma finite_ne_induct [case_names singleton insert, consumes 2]:
assumes "finite F" and "F \ {}"
assumes "\x. P {x}"
and "\x F. finite F \ F \ {} \ x \ F \ P F \ P (insert x F)"
shows "P F"
using assms proof induct
case empty then show ?case by simp
next
case (insert x F) then show ?case by cases auto
qed
lemma finite_subset_induct [consumes 2, case_names empty insert]:
assumes "finite F" and "F \ A"
assumes empty: "P {}"
and insert: "\a F. finite F \ a \ A \ a \ F \ P F \ P (insert a F)"
shows "P F"
using `finite F` `F \ A` proof induct
show "P {}" by fact
next
fix x F
assume "finite F" and "x \ F" and
P: "F \ A \ P F" and i: "insert x F \ A"
show "P (insert x F)"
proof (rule insert)
from i show "x \ A" by blast
from i have "F \ A" by blast
with P show "P F" .
show "finite F" by fact
show "x \ F" by fact
qed
qed
lemma finite_empty_induct:
assumes "finite A"
assumes "P A"
and remove: "\a A. finite A \ a \ A \ P A \ P (A - {a})"
shows "P {}"
proof -
have "\B. B \ A \ P (A - B)"
proof -
fix B :: "'a set"
assume "B \ A"
with `finite A` have "finite B" by (rule rev_finite_subset)
from this `B \ A` show "P (A - B)"
proof induct
case empty
from `P A` show ?case by simp
next
case (insert b B)
have "P (A - B - {b})"
proof (rule remove)
from `finite A` show "finite (A - B)" by induct auto
from insert show "b \ A - B" by simp
from insert show "P (A - B)" by simp
qed
also have "A - B - {b} = A - insert b B" by (rule Diff_insert [symmetric])
finally show ?case .
qed
qed
then have "P (A - A)" by blast
then show ?thesis by simp
qed
subsection {* Class @{text finite} *}
class finite =
assumes finite_UNIV: "finite (UNIV \ 'a set)"
begin
lemma finite [simp]: "finite (A \ 'a set)"
by (rule subset_UNIV finite_UNIV finite_subset)+
lemma finite_code [code]: "finite (A \ 'a set) \ True"
by simp
end
instance unit :: finite proof
qed (simp add: UNIV_unit)
instance bool :: finite proof
qed (simp add: UNIV_bool)
instance prod :: (finite, finite) finite proof
qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
lemma finite_option_UNIV [simp]:
"finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
instance option :: (finite) finite proof
qed (simp add: UNIV_option_conv)
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
instance "fun" :: (finite, finite) finite
proof
show "finite (UNIV :: ('a => 'b) set)"
proof (rule finite_imageD)
let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
have "range ?graph \ Pow UNIV" by simp
moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
by (simp only: finite_Pow_iff finite)
ultimately show "finite (range ?graph)"
by (rule finite_subset)
show "inj ?graph" by (rule inj_graph)
qed
qed
instance sum :: (finite, finite) finite proof
qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
subsection {* A basic fold functional for finite sets *}
text {* The intended behaviour is
@{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\ (f x\<^isub>n z)\)"}
if @{text f} is ``left-commutative'':
*}
locale comp_fun_commute =
fixes f :: "'a \ 'b \ 'b"
assumes comp_fun_commute: "f y \ f x = f x \ f y"
begin
lemma fun_left_comm: "f x (f y z) = f y (f x z)"
using comp_fun_commute by (simp add: fun_eq_iff)
end
inductive fold_graph :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b \ bool"
for f :: "'a \ 'b \ 'b" and z :: 'b where
emptyI [intro]: "fold_graph f z {} z" |
insertI [intro]: "x \ A \ fold_graph f z A y
\ fold_graph f z (insert x A) (f x y)"
inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b" where
"fold f z A = (THE y. fold_graph f z A y)"
text{*A tempting alternative for the definiens is
@{term "if finite A then THE y. fold_graph f z A y else e"}.
It allows the removal of finiteness assumptions from the theorems
@{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
The proofs become ugly. It is not worth the effort. (???) *}
lemma finite_imp_fold_graph: "finite A \ \x. fold_graph f z A x"
by (induct rule: finite_induct) auto
subsubsection{*From @{const fold_graph} to @{term fold}*}
context comp_fun_commute
begin
lemma fold_graph_insertE_aux:
"fold_graph f z A y \ a \ A \ \y'. y = f a y' \ fold_graph f z (A - {a}) y'"
proof (induct set: fold_graph)
case (insertI x A y) show ?case
proof (cases "x = a")
assume "x = a" with insertI show ?case by auto
next
assume "x \ a"
then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
using insertI by auto
have "f x y = f a (f x y')"
unfolding y by (rule fun_left_comm)
moreover have "fold_graph f z (insert x A - {a}) (f x y')"
using y' and `x \ a` and `x \ A`
by (simp add: insert_Diff_if fold_graph.insertI)
ultimately show ?case by fast
qed
qed simp
lemma fold_graph_insertE:
assumes "fold_graph f z (insert x A) v" and "x \