# Theory Finite_Set

Up to index of Isabelle/HOL-Proofs

theory Finite_Set
imports Option Power
`(*  Title:      HOL/Finite_Set.thy    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel                with contributions by Jeremy Avigad*)header {* Finite sets *}theory Finite_Setimports Option Powerbeginsubsection {* Predicate for finite sets *}inductive finite :: "'a set => bool"  where    emptyI [simp, intro!]: "finite {}"  | insertI [simp, intro!]: "finite A ==> finite (insert a A)"simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *}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)  qedqedsubsubsection {* 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 blastqedtext {* 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 simpnext  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  qedqedsubsubsection {* 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 assmsproof induct  case empty  show ?case  proof    show "∃f. {} = f ` {i::nat. i < 0} ∧ inj_on f {i. i < 0}" by simp   qednext  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 blastqedlemma nat_seg_image_imp_finite:  "A = f ` {i::nat. i < n} ==> finite A"proof (induct n arbitrary: A)  case 0 thus ?case by simpnext  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<n. f n = f k"    hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)    thus ?thesis using finB by simp  next    assume "¬(∃ k<n. f n = f k)"    hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)    thus ?thesis using finB by simp  qedqedlemma finite_conv_nat_seg_image:  "finite A <-> (∃(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<n} A"    by (auto simp:bij_betw_def)  let ?f = "the_inv_into {i. i<n} f"  have "inj_on ?f A & ?f ` A = {i. i<n}"    by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])  thus ?thesis by blastqedlemma finite_Collect_less_nat [iff]:  "finite {n::nat. n < k}"  by (fastforce simp: finite_conv_nat_seg_image)lemma finite_Collect_le_nat [iff]:  "finite {n::nat. n ≤ 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 simpnext  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)  qedqedlemma 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_alllemma 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 simpqedlemma 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 ..qedlemma 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 simpqedlemma 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(\<Union>A)"  by (induct rule: finite_induct) simp_alllemma finite_UN_I [intro]:  "finite A ==> (!!a. a ∈ A ==> finite (B a)) ==> finite (\<Union>a∈A. B a)"  by (induct rule: finite_induct) simp_alllemma 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 (\<Inter>M)"  by (blast intro: Inter_lower finite_subset)lemma finite_INT [intro]:  "∃x∈I. finite (A x) ==> finite (\<Inter>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_alllemma 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 assmsproof (induct "f ` A" arbitrary: A)  case empty then show ?case by simpnext  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 simpqedlemma 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 assmsproof induct  case empty then show ?case by simpnext  case insert then show ?case    by (clarsimp simp del: image_insert simp add: image_insert [symmetric])       blastqedlemma 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)  donelemma finite_vimageI:  "finite F ==> inj h ==> finite (h -` F)"  using finite_vimage_IntI[of F h UNIV] by autolemma 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" .qedlemma 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} = (\<Union>y∈A. {x. Q x y})" by auto  with assms show ?thesis by simpqedlemma 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} = (\<Union>y∈{y. P y}. {x. Q x y})" by auto  with assms show ?thesis by simpqedlemma 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)qedlemma 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) blastlemma 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 o 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)qedlemma 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 o 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)qedlemma finite_prod:   "finite (UNIV :: ('a × 'b) set) <-> finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set)"by(auto simp add: UNIV_Times_UNIV[symmetric] simp del: UNIV_Times_UNIV    dest: finite_cartesian_productD1 finite_cartesian_productD2)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]) simpnext  assume "finite A"  then show "finite (Pow A)"    by induct (simp_all add: Pow_insert)qedcorollary finite_Collect_subsets [simp, intro]:  "finite A ==> finite {B. B ⊆ A}"  by (simp add: Pow_def [symmetric])lemma finite_set: "finite (UNIV :: 'a set set) <-> finite (UNIV :: 'a set)"by(simp only: finite_Pow_iff Pow_UNIV[symmetric])lemma finite_UnionD: "finite(\<Union>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 assmsproof induct  case empty then show ?case by simpnext  case (insert x F) then show ?case by cases autoqedlemma 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 factnext  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  qedqedlemma 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 simpqedsubsection {* Class @{text finite}  *}class finite =  assumes finite_UNIV: "finite (UNIV :: 'a set)"beginlemma finite [simp]: "finite (A :: 'a set)"  by (rule subset_UNIV finite_UNIV finite_subset)+lemma finite_code [code]: "finite (A :: 'a set) <-> True"  by simpendinstance prod :: (finite, finite) finite  by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)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) finiteproof  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)  qedqedinstance bool :: finite  by default (simp add: UNIV_bool)instance set :: (finite) finite  by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)instance unit :: finite  by default (simp add: UNIV_unit)instance sum :: (finite, finite) finite  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus 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  by default (simp add: UNIV_option_conv)subsection {* A basic fold functional for finite sets *}text {* The intended behaviour is@{text "fold f z {x⇣1, ..., x⇣n} = f x⇣1 (… (f x⇣n z)…)"}if @{text f} is ``left-commutative'':*}locale comp_fun_commute =  fixes f :: "'a => 'b => 'b"  assumes comp_fun_commute: "f y o f x = f x o f y"beginlemma fun_left_comm: "f x (f y z) = f y (f x z)"  using comp_fun_commute by (simp add: fun_eq_iff)endinductive 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) autosubsubsection{*From @{const fold_graph} to @{term fold}*}context comp_fun_commutebeginlemma 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  qedqed simplemma fold_graph_insertE:  assumes "fold_graph f z (insert x A) v" and "x ∉ A"  obtains y where "v = f x y" and "fold_graph f z A y"using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])lemma fold_graph_determ:  "fold_graph f z A x ==> fold_graph f z A y ==> y = x"proof (induct arbitrary: y set: fold_graph)  case (insertI x A y v)  from `fold_graph f z (insert x A) v` and `x ∉ A`  obtain y' where "v = f x y'" and "fold_graph f z A y'"    by (rule fold_graph_insertE)  from `fold_graph f z A y'` have "y' = y" by (rule insertI)  with `v = f x y'` show "v = f x y" by simpqed fastlemma fold_equality:  "fold_graph f z A y ==> fold f z A = y"by (unfold fold_def) (blast intro: fold_graph_determ)lemma fold_graph_fold:  assumes "finite A"  shows "fold_graph f z A (fold f z A)"proof -  from assms have "∃x. fold_graph f z A x" by (rule finite_imp_fold_graph)  moreover note fold_graph_determ  ultimately have "∃!x. fold_graph f z A x" by (rule ex_ex1I)  then have "fold_graph f z A (The (fold_graph f z A))" by (rule theI')  then show ?thesis by (unfold fold_def)qedtext{* The base case for @{text fold}: *}lemma (in -) fold_empty [simp]: "fold f z {} = z"by (unfold fold_def) blasttext{* The various recursion equations for @{const fold}: *}lemma fold_insert [simp]:  assumes "finite A" and "x ∉ A"  shows "fold f z (insert x A) = f x (fold f z A)"proof (rule fold_equality)  from `finite A` have "fold_graph f z A (fold f z A)" by (rule fold_graph_fold)  with `x ∉ A`show "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI)qedlemma fold_fun_comm:  "finite A ==> f x (fold f z A) = fold f (f x z) A"proof (induct rule: finite_induct)  case empty then show ?case by simpnext  case (insert y A) then show ?case    by (simp add: fun_left_comm[of x])qedlemma fold_insert2:  "finite A ==> x ∉ A ==> fold f z (insert x A) = fold f (f x z) A"by (simp add: fold_fun_comm)lemma fold_rec:  assumes "finite A" and "x ∈ A"  shows "fold f z A = f x (fold f z (A - {x}))"proof -  have A: "A = insert x (A - {x})" using `x ∈ A` by blast  then have "fold f z A = fold f z (insert x (A - {x}))" by simp  also have "… = f x (fold f z (A - {x}))"    by (rule fold_insert) (simp add: `finite A`)+  finally show ?thesis .qedlemma fold_insert_remove:  assumes "finite A"  shows "fold f z (insert x A) = f x (fold f z (A - {x}))"proof -  from `finite A` have "finite (insert x A)" by auto  moreover have "x ∈ insert x A" by auto  ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"    by (rule fold_rec)  then show ?thesis by simpqedtext{* Other properties of @{const fold}: *}lemma fold_image:  assumes "finite A" and "inj_on g A"  shows "fold f x (g ` A) = fold (f o g) x A"using assmsproof induction  case (insert a F)    interpret comp_fun_commute "λx. f (g x)" by default (simp add: comp_fun_commute)    from insert show ?case by autoqed (simp)endlemma fold_cong:  assumes "comp_fun_commute f" "comp_fun_commute g"  assumes "finite A" and cong: "!!x. x ∈ A ==> f x = g x"    and "A = B" and "s = t"  shows "Finite_Set.fold f s A = Finite_Set.fold g t B"proof -  have "Finite_Set.fold f s A = Finite_Set.fold g s A"    using `finite A` cong proof (induct A)    case empty then show ?case by simp  next    case (insert x A)    interpret f: comp_fun_commute f by (fact `comp_fun_commute f`)    interpret g: comp_fun_commute g by (fact `comp_fun_commute g`)    from insert show ?case by simp  qed  with assms show ?thesis by simpqedtext{* A simplified version for idempotent functions: *}locale comp_fun_idem = comp_fun_commute +  assumes comp_fun_idem: "f x o f x = f x"beginlemma fun_left_idem: "f x (f x z) = f x z"  using comp_fun_idem by (simp add: fun_eq_iff)lemma fold_insert_idem:  assumes fin: "finite A"  shows "fold f z (insert x A) = f x (fold f z A)"proof cases  assume "x ∈ A"  then obtain B where "A = insert x B" and "x ∉ B" by (rule set_insert)  then show ?thesis using assms by (simp add:fun_left_idem)next  assume "x ∉ A" then show ?thesis using assms by simpqeddeclare fold_insert[simp del] fold_insert_idem[simp]lemma fold_insert_idem2:  "finite A ==> fold f z (insert x A) = fold f (f x z) A"by(simp add:fold_fun_comm)endsubsubsection {* Liftings to @{text comp_fun_commute} etc. *}lemma (in comp_fun_commute) comp_comp_fun_commute:  "comp_fun_commute (f o g)"proofqed (simp_all add: comp_fun_commute)lemma (in comp_fun_idem) comp_comp_fun_idem:  "comp_fun_idem (f o g)"  by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)    (simp_all add: comp_fun_idem)lemma (in comp_fun_commute) comp_fun_commute_funpow:  "comp_fun_commute (λx. f x ^^ g x)"proof  fix y x  show "f y ^^ g y o f x ^^ g x = f x ^^ g x o f y ^^ g y"  proof (cases "x = y")    case True then show ?thesis by simp  next    case False show ?thesis    proof (induct "g x" arbitrary: g)      case 0 then show ?case by simp    next      case (Suc n g)      have hyp1: "f y ^^ g y o f x = f x o f y ^^ g y"      proof (induct "g y" arbitrary: g)        case 0 then show ?case by simp      next        case (Suc n g)        def h ≡ "λz. g z - 1"        with Suc have "n = h y" by simp        with Suc have hyp: "f y ^^ h y o f x = f x o f y ^^ h y"          by auto        from Suc h_def have "g y = Suc (h y)" by simp        then show ?case by (simp add: comp_assoc hyp)          (simp add: o_assoc comp_fun_commute)      qed      def h ≡ "λz. if z = x then g x - 1 else g z"      with Suc have "n = h x" by simp      with Suc have "f y ^^ h y o f x ^^ h x = f x ^^ h x o f y ^^ h y"        by auto      with False h_def have hyp2: "f y ^^ g y o f x ^^ h x = f x ^^ h x o f y ^^ g y" by simp      from Suc h_def have "g x = Suc (h x)" by simp      then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)        (simp add: comp_assoc hyp1)    qed  qedqedsubsubsection {* Expressing set operations via @{const fold} *}lemma comp_fun_idem_insert:  "comp_fun_idem insert"proofqed autolemma comp_fun_idem_remove:  "comp_fun_idem Set.remove"proofqed autolemma (in semilattice_inf) comp_fun_idem_inf:  "comp_fun_idem inf"proofqed (auto simp add: inf_left_commute)lemma (in semilattice_sup) comp_fun_idem_sup:  "comp_fun_idem sup"proofqed (auto simp add: sup_left_commute)lemma union_fold_insert:  assumes "finite A"  shows "A ∪ B = fold insert B A"proof -  interpret comp_fun_idem insert by (fact comp_fun_idem_insert)  from `finite A` show ?thesis by (induct A arbitrary: B) simp_allqedlemma minus_fold_remove:  assumes "finite A"  shows "B - A = fold Set.remove B A"proof -  interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove)  from `finite A` have "fold Set.remove B A = B - A" by (induct A arbitrary: B) auto  then show ?thesis ..qedlemma comp_fun_commute_filter_fold: "comp_fun_commute (λx A'. if P x then Set.insert x A' else A')"proof -   interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)  show ?thesis by default (auto simp: fun_eq_iff)qedlemma Set_filter_fold:  assumes "finite A"  shows "Set.filter P A = fold (λx A'. if P x then Set.insert x A' else A') {} A"using assmsby (induct A)   (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])lemma inter_Set_filter:       assumes "finite B"  shows "A ∩ B = Set.filter (λx. x ∈ A) B"using assms by (induct B) (auto simp: Set.filter_def)lemma image_fold_insert:  assumes "finite A"  shows "image f A = fold (λk A. Set.insert (f k) A) {} A"using assmsproof -  interpret comp_fun_commute "λk A. Set.insert (f k) A" by default auto  show ?thesis using assms by (induct A) autoqedlemma Ball_fold:  assumes "finite A"  shows "Ball A P = fold (λk s. s ∧ P k) True A"using assmsproof -  interpret comp_fun_commute "λk s. s ∧ P k" by default auto  show ?thesis using assms by (induct A) autoqedlemma Bex_fold:  assumes "finite A"  shows "Bex A P = fold (λk s. s ∨ P k) False A"using assmsproof -  interpret comp_fun_commute "λk s. s ∨ P k" by default auto  show ?thesis using assms by (induct A) autoqedlemma comp_fun_commute_Pow_fold:   "comp_fun_commute (λx A. A ∪ Set.insert x ` A)"   by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blastlemma Pow_fold:  assumes "finite A"  shows "Pow A = fold (λx A. A ∪ Set.insert x ` A) {{}} A"using assmsproof -  interpret comp_fun_commute "λx A. A ∪ Set.insert x ` A" by (rule comp_fun_commute_Pow_fold)  show ?thesis using assms by (induct A) (auto simp: Pow_insert)qedlemma fold_union_pair:  assumes "finite B"  shows "(\<Union>y∈B. {(x, y)}) ∪ A = fold (λy. Set.insert (x, y)) A B"proof -  interpret comp_fun_commute "λy. Set.insert (x, y)" by default auto  show ?thesis using assms  by (induct B arbitrary: A) simp_allqedlemma comp_fun_commute_product_fold:   assumes "finite B"  shows "comp_fun_commute (λx A. fold (λy. Set.insert (x, y)) A B)" by default (auto simp: fold_union_pair[symmetric] assms)lemma product_fold:  assumes "finite A"  assumes "finite B"  shows "A × B = fold (λx A. fold (λy. Set.insert (x, y)) A B) {} A"using assms unfolding Sigma_def by (induct A)   (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)context complete_latticebeginlemma inf_Inf_fold_inf:  assumes "finite A"  shows "inf B (Inf A) = fold inf B A"proof -  interpret comp_fun_idem inf by (fact comp_fun_idem_inf)  from `finite A` show ?thesis by (induct A arbitrary: B)    (simp_all add: inf_commute fold_fun_comm)qedlemma sup_Sup_fold_sup:  assumes "finite A"  shows "sup B (Sup A) = fold sup B A"proof -  interpret comp_fun_idem sup by (fact comp_fun_idem_sup)  from `finite A` show ?thesis by (induct A arbitrary: B)    (simp_all add: sup_commute fold_fun_comm)qedlemma Inf_fold_inf:  assumes "finite A"  shows "Inf A = fold inf top A"  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)lemma Sup_fold_sup:  assumes "finite A"  shows "Sup A = fold sup bot A"  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)lemma inf_INF_fold_inf:  assumes "finite A"  shows "inf B (INFI A f) = fold (inf o f) B A" (is "?inf = ?fold") proof (rule sym)  interpret comp_fun_idem inf by (fact comp_fun_idem_inf)  interpret comp_fun_idem "inf o f" by (fact comp_comp_fun_idem)  from `finite A` show "?fold = ?inf"    by (induct A arbitrary: B)      (simp_all add: INF_def inf_left_commute)qedlemma sup_SUP_fold_sup:  assumes "finite A"  shows "sup B (SUPR A f) = fold (sup o f) B A" (is "?sup = ?fold") proof (rule sym)  interpret comp_fun_idem sup by (fact comp_fun_idem_sup)  interpret comp_fun_idem "sup o f" by (fact comp_comp_fun_idem)  from `finite A` show "?fold = ?sup"    by (induct A arbitrary: B)      (simp_all add: SUP_def sup_left_commute)qedlemma INF_fold_inf:  assumes "finite A"  shows "INFI A f = fold (inf o f) top A"  using assms inf_INF_fold_inf [of A top] by simplemma SUP_fold_sup:  assumes "finite A"  shows "SUPR A f = fold (sup o f) bot A"  using assms sup_SUP_fold_sup [of A bot] by simpendsubsection {* The derived combinator @{text fold_image} *}definition fold_image :: "('b => 'b => 'b) => ('a => 'b) => 'b => 'a set => 'b"  where "fold_image f g = fold (λx y. f (g x) y)"lemma fold_image_empty[simp]: "fold_image f g z {} = z"  by (simp add:fold_image_def)context ab_semigroup_multbeginlemma fold_image_insert[simp]:  assumes "finite A" and "a ∉ A"  shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"proof -  interpret comp_fun_commute "%x y. (g x) * y"    by default (simp add: fun_eq_iff mult_ac)  from assms show ?thesis by (simp add: fold_image_def)qedlemma fold_image_reindex:  assumes "finite A"  shows "inj_on h A ==> fold_image times g z (h ` A) = fold_image times (g o h) z A"  using assms by induct autolemma fold_image_cong:  assumes "finite A" and g_h: "!!x. x∈A ==> g x = h x"  shows "fold_image times g z A = fold_image times h z A"proof -  from `finite A`  have "!!C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C"  proof (induct arbitrary: C)    case empty then show ?case by simp  next    case (insert x F) then show ?case apply -    apply (simp add: subset_insert_iff, clarify)    apply (subgoal_tac "finite C")      prefer 2 apply (blast dest: finite_subset [rotated])    apply (subgoal_tac "C = insert x (C - {x})")      prefer 2 apply blast    apply (erule ssubst)    apply (simp add: Ball_def del: insert_Diff_single)    done  qed  with g_h show ?thesis by simpqedendcontext comm_monoid_multbeginlemma fold_image_1:  "finite S ==> (∀x∈S. f x = 1) ==> fold_image op * f 1 S = 1"  apply (induct rule: finite_induct)  apply simp by autolemma fold_image_Un_Int:  "finite A ==> finite B ==>    fold_image times g 1 A * fold_image times g 1 B =    fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)"  apply (induct rule: finite_induct)by (induct set: finite)    (auto simp add: mult_ac insert_absorb Int_insert_left)lemma fold_image_Un_one:  assumes fS: "finite S" and fT: "finite T"  and I0: "∀x ∈ S∩T. f x = 1"  shows "fold_image (op *) f 1 (S ∪ T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"proof-  have "fold_image op * f 1 (S ∩ T) = 1"     apply (rule fold_image_1)    using fS fT I0 by auto   with fold_image_Un_Int[OF fS fT] show ?thesis by simpqedcorollary fold_Un_disjoint:  "finite A ==> finite B ==> A Int B = {} ==>   fold_image times g 1 (A Un B) =   fold_image times g 1 A * fold_image times g 1 B"by (simp add: fold_image_Un_Int)lemma fold_image_UN_disjoint:  "[| finite I; ALL i:I. finite (A i);     ALL i:I. ALL j:I. i ≠ j --> A i Int A j = {} |]   ==> fold_image times g 1 (UNION I A) =       fold_image times (%i. fold_image times g 1 (A i)) 1 I"apply (induct rule: finite_induct)apply simpapply atomizeapply (subgoal_tac "ALL i:F. x ≠ i") prefer 2 apply blastapply (subgoal_tac "A x Int UNION F A = {}") prefer 2 apply blastapply (simp add: fold_Un_disjoint)donelemma fold_image_Sigma: "finite A ==> ALL x:A. finite (B x) ==>  fold_image times (%x. fold_image times (g x) 1 (B x)) 1 A =  fold_image times (split g) 1 (SIGMA x:A. B x)"apply (subst Sigma_def)apply (subst fold_image_UN_disjoint, assumption, simp) apply blastapply (erule fold_image_cong)apply (subst fold_image_UN_disjoint, simp, simp) apply blastapply simpdonelemma fold_image_distrib: "finite A ==>   fold_image times (%x. g x * h x) 1 A =   fold_image times g 1 A *  fold_image times h 1 A"by (erule finite_induct) (simp_all add: mult_ac)lemma fold_image_related:   assumes Re: "R e e"   and Rop: "∀x1 y1 x2 y2. R x1 x2 ∧ R y1 y2 --> R (x1 * y1) (x2 * y2)"   and fS: "finite S" and Rfg: "∀x∈S. R (h x) (g x)"  shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)"  using fS by (rule finite_subset_induct) (insert assms, auto)lemma  fold_image_eq_general:  assumes fS: "finite S"  and h: "∀y∈S'. ∃!x. x∈ S ∧ h(x) = y"   and f12:  "∀x∈S. h x ∈ S' ∧ f2(h x) = f1 x"  shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'"proof-  from h f12 have hS: "h ` S = S'" by auto  {fix x y assume H: "x ∈ S" "y ∈ S" "h x = h y"    from f12 h H  have "x = y" by auto }  hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast  from f12 have th: "!!x. x ∈ S ==> (f2 o h) x = f1 x" by auto   from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp  also have "… = fold_image (op *) (f2 o h) e S"     using fold_image_reindex[OF fS hinj, of f2 e] .  also have "… = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e]    by blast  finally show ?thesis ..qedlemma fold_image_eq_general_inverses:  assumes fS: "finite S"   and kh: "!!y. y ∈ T ==> k y ∈ S ∧ h (k y) = y"  and hk: "!!x. x ∈ S ==> h x ∈ T ∧ k (h x) = x  ∧ g (h x) = f x"  shows "fold_image (op *) f e S = fold_image (op *) g e T"  (* metis solves it, but not yet available here *)  apply (rule fold_image_eq_general[OF fS, of T h g f e])  apply (rule ballI)  apply (frule kh)  apply (rule ex1I[])  apply blast  apply clarsimp  apply (drule hk) apply simp  apply (rule sym)  apply (erule conjunct1[OF conjunct2[OF hk]])  apply (rule ballI)  apply (drule  hk)  apply blast  doneendsubsection {* A fold functional for non-empty sets *}text{* Does not require start value. *}inductive  fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"  for f :: "'a => 'a => 'a"where  fold1Set_insertI [intro]:   "[| fold_graph f a A x; a ∉ A |] ==> fold1Set f (insert a A) x"definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where  "fold1 f A == THE x. fold1Set f A x"lemma fold1Set_nonempty:  "fold1Set f A x ==> A ≠ {}"by(erule fold1Set.cases, simp_all)inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"by (blast elim: fold_graph.cases)lemma fold1_singleton [simp]: "fold1 f {a} = a"by (unfold fold1_def) blastlemma finite_nonempty_imp_fold1Set:  "[| finite A; A ≠ {} |] ==> EX x. fold1Set f A x"apply (induct A rule: finite_induct)apply (auto dest: finite_imp_fold_graph [of _ f])donetext{*First, some lemmas about @{const fold_graph}.*}context ab_semigroup_multbeginlemma comp_fun_commute: "comp_fun_commute (op *)"  by default (simp add: fun_eq_iff mult_ac)lemma fold_graph_insert_swap:assumes fold: "fold_graph times (b::'a) A y" and "b ∉ A"shows "fold_graph times z (insert b A) (z * y)"proof -  interpret comp_fun_commute "op *::'a => 'a => 'a" by (rule comp_fun_commute)from assms show ?thesisproof (induct rule: fold_graph.induct)  case emptyI show ?case by (subst mult_commute [of z b], fast)next  case (insertI x A y)    have "fold_graph times z (insert x (insert b A)) (x * (z * y))"      using insertI by force  --{*how does @{term id} get unfolded?*}    thus ?case by (simp add: insert_commute mult_ac)qedqedlemma fold_graph_permute_diff:assumes fold: "fold_graph times b A x"shows "!!a. [|a ∈ A; b ∉ A|] ==> fold_graph times a (insert b (A-{a})) x"using foldproof (induct rule: fold_graph.induct)  case emptyI thus ?case by simpnext  case (insertI x A y)  have "a = x ∨ a ∈ A" using insertI by simp  thus ?case  proof    assume "a = x"    with insertI show ?thesis      by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap)  next    assume ainA: "a ∈ A"    hence "fold_graph times a (insert x (insert b (A - {a}))) (x * y)"      using insertI by force    moreover    have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"      using ainA insertI by blast    ultimately show ?thesis by simp  qedqedlemma fold1_eq_fold:assumes "finite A" "a ∉ A" shows "fold1 times (insert a A) = fold times a A"proof -  interpret comp_fun_commute "op *::'a => 'a => 'a" by (rule comp_fun_commute)  from assms show ?thesisapply (simp add: fold1_def fold_def)apply (rule the_equality)apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])apply (rule sym, clarify)apply (case_tac "Aa=A") apply (best intro: fold_graph_determ)apply (subgoal_tac "fold_graph times a A x") apply (best intro: fold_graph_determ)apply (subgoal_tac "insert aa (Aa - {a}) = A") prefer 2 apply (blast elim: equalityE)apply (auto dest: fold_graph_permute_diff [where a=a])doneqedlemma nonempty_iff: "(A ≠ {}) = (∃x B. A = insert x B & x ∉ B)"apply safe apply simp apply (drule_tac x=x in spec) apply (drule_tac x="A-{x}" in spec, auto)donelemma fold1_insert:  assumes nonempty: "A ≠ {}" and A: "finite A" "x ∉ A"  shows "fold1 times (insert x A) = x * fold1 times A"proof -  interpret comp_fun_commute "op *::'a => 'a => 'a" by (rule comp_fun_commute)  from nonempty obtain a A' where "A = insert a A' & a ~: A'"    by (auto simp add: nonempty_iff)  with A show ?thesis    by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)qedendcontext ab_semigroup_idem_multbeginlemma comp_fun_idem: "comp_fun_idem (op *)"  by default (simp_all add: fun_eq_iff mult_left_commute)lemma fold1_insert_idem [simp]:  assumes nonempty: "A ≠ {}" and A: "finite A"   shows "fold1 times (insert x A) = x * fold1 times A"proof -  interpret comp_fun_idem "op *::'a => 'a => 'a"    by (rule comp_fun_idem)  from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"    by (auto simp add: nonempty_iff)  show ?thesis  proof cases    assume a: "a = x"    show ?thesis    proof cases      assume "A' = {}"      with A' a show ?thesis by simp    next      assume "A' ≠ {}"      with A A' a show ?thesis        by (simp add: fold1_insert mult_assoc [symmetric])    qed  next    assume "a ≠ x"    with A A' show ?thesis      by (simp add: insert_commute fold1_eq_fold)  qedqedlemma hom_fold1_commute:assumes hom: "!!x y. h (x * y) = h x * h y"and N: "finite N" "N ≠ {}" shows "h (fold1 times N) = fold1 times (h ` N)"using Nproof (induct rule: finite_ne_induct)  case singleton thus ?case by simpnext  case (insert n N)  then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp  also have "… = h n * h (fold1 times N)" by(rule hom)  also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)  also have "times (h n) … = fold1 times (insert (h n) (h ` N))"    using insert by(simp)  also have "insert (h n) (h ` N) = h ` insert n N" by simp  finally show ?case .qedlemma fold1_eq_fold_idem:  assumes "finite A"  shows "fold1 times (insert a A) = fold times a A"proof (cases "a ∈ A")  case False  with assms show ?thesis by (simp add: fold1_eq_fold)next  interpret comp_fun_idem times by (fact comp_fun_idem)  case True then obtain b B    where A: "A = insert a B" and "a ∉ B" by (rule set_insert)  with assms have "finite B" by auto  then have "fold times a (insert a B) = fold times (a * a) B"    using `a ∉ B` by (rule fold_insert2)  then show ?thesis    using `a ∉ B` `finite B` by (simp add: fold1_eq_fold A)qedendtext{* Now the recursion rules for definitions: *}lemma fold1_singleton_def: "g = fold1 f ==> g {a} = a"by simplemma (in ab_semigroup_mult) fold1_insert_def:  "[| g = fold1 times; finite A; x ∉ A; A ≠ {} |] ==> g (insert x A) = x * g A"by (simp add:fold1_insert)lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:  "[| g = fold1 times; finite A; A ≠ {} |] ==> g (insert x A) = x * g A"by simpsubsubsection{* Determinacy for @{term fold1Set} *}(*Not actually used!!*)(*context ab_semigroup_multbeginlemma fold_graph_permute:  "[|fold_graph times id b (insert a A) x; a ∉ A; b ∉ A|]   ==> fold_graph times id a (insert b A) x"apply (cases "a=b") apply (auto dest: fold_graph_permute_diff) donelemma fold1Set_determ:  "fold1Set times A x ==> fold1Set times A y ==> y = x"proof (clarify elim!: fold1Set.cases)  fix A x B y a b  assume Ax: "fold_graph times id a A x"  assume By: "fold_graph times id b B y"  assume anotA:  "a ∉ A"  assume bnotB:  "b ∉ B"  assume eq: "insert a A = insert b B"  show "y=x"  proof cases    assume same: "a=b"    hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)    thus ?thesis using Ax By same by (blast intro: fold_graph_determ)  next    assume diff: "a≠b"    let ?D = "B - {a}"    have B: "B = insert a ?D" and A: "A = insert b ?D"     and aB: "a ∈ B" and bA: "b ∈ A"      using eq anotA bnotB diff by (blast elim!:equalityE)+    with aB bnotB By    have "fold_graph times id a (insert b ?D) y"       by (auto intro: fold_graph_permute simp add: insert_absorb)    moreover    have "fold_graph times id a (insert b ?D) x"      by (simp add: A [symmetric] Ax)     ultimately show ?thesis by (blast intro: fold_graph_determ)   qedqedlemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"  by (unfold fold1_def) (blast intro: fold1Set_determ)end*)declare  empty_fold_graphE [rule del]  fold_graph.intros [rule del]  empty_fold1SetE [rule del]  insert_fold1SetE [rule del]  -- {* No more proofs involve these relations. *}subsubsection {* Lemmas about @{text fold1} *}context ab_semigroup_multbeginlemma fold1_Un:assumes A: "finite A" "A ≠ {}"shows "finite B ==> B ≠ {} ==> A Int B = {} ==>       fold1 times (A Un B) = fold1 times A * fold1 times B"using A by (induct rule: finite_ne_induct)  (simp_all add: fold1_insert mult_assoc)lemma fold1_in:  assumes A: "finite (A)" "A ≠ {}" and elem: "!!x y. x * y ∈ {x,y}"  shows "fold1 times A ∈ A"using Aproof (induct rule:finite_ne_induct)  case singleton thus ?case by simpnext  case insert thus ?case using elem by (force simp add:fold1_insert)qedendlemma (in ab_semigroup_idem_mult) fold1_Un2:assumes A: "finite A" "A ≠ {}"shows "finite B ==> B ≠ {} ==>       fold1 times (A Un B) = fold1 times A * fold1 times B"using Aproof(induct rule:finite_ne_induct)  case singleton thus ?case by simpnext  case insert thus ?case by (simp add: mult_assoc)qedsubsection {* Locales as mini-packages for fold operations *}subsubsection {* The natural case *}locale folding =  fixes f :: "'a => 'b => 'b"  fixes F :: "'a set => 'b => 'b"  assumes comp_fun_commute: "f y o f x = f x o f y"  assumes eq_fold: "finite A ==> F A s = fold f s A"beginlemma empty [simp]:  "F {} = id"  by (simp add: eq_fold fun_eq_iff)lemma insert [simp]:  assumes "finite A" and "x ∉ A"  shows "F (insert x A) = F A o f x"proof -  interpret comp_fun_commute f    by default (insert comp_fun_commute, simp add: fun_eq_iff)  from fold_insert2 assms  have "!!s. fold f s (insert x A) = fold f (f x s) A" .  with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)qedlemma remove:  assumes "finite A" and "x ∈ A"  shows "F A = F (A - {x}) o f x"proof -  from `x ∈ A` obtain B where A: "A = insert x B" and "x ∉ B"    by (auto dest: mk_disjoint_insert)  moreover from `finite A` this have "finite B" by simp  ultimately show ?thesis by simpqedlemma insert_remove:  assumes "finite A"  shows "F (insert x A) = F (A - {x}) o f x"  using assms by (cases "x ∈ A") (simp_all add: remove insert_absorb)lemma commute_left_comp:  "f y o (f x o g) = f x o (f y o g)"  by (simp add: o_assoc comp_fun_commute)lemma comp_fun_commute':  assumes "finite A"  shows "f x o F A = F A o f x"  using assms by (induct A)    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: comp_assoc comp_fun_commute)lemma commute_left_comp':  assumes "finite A"  shows "f x o (F A o g) = F A o (f x o g)"  using assms by (simp add: o_assoc comp_fun_commute')lemma comp_fun_commute'':  assumes "finite A" and "finite B"  shows "F B o F A = F A o F B"  using assms by (induct A)    (simp_all add: o_assoc, simp add: comp_assoc comp_fun_commute')lemma commute_left_comp'':  assumes "finite A" and "finite B"  shows "F B o (F A o g) = F A o (F B o g)"  using assms by (simp add: o_assoc comp_fun_commute'')lemmas comp_fun_commutes = comp_assoc comp_fun_commute commute_left_comp  comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp''lemma union_inter:  assumes "finite A" and "finite B"  shows "F (A ∪ B) o F (A ∩ B) = F A o F B"  using assms by (induct A)    (simp_all del: o_apply add: insert_absorb Int_insert_left comp_fun_commutes,      simp add: o_assoc)lemma union:  assumes "finite A" and "finite B"  and "A ∩ B = {}"  shows "F (A ∪ B) = F A o F B"proof -  from union_inter `finite A` `finite B` have "F (A ∪ B) o F (A ∩ B) = F A o F B" .  with `A ∩ B = {}` show ?thesis by simpqedendsubsubsection {* The natural case with idempotency *}locale folding_idem = folding +  assumes idem_comp: "f x o f x = f x"beginlemma idem_left_comp:  "f x o (f x o g) = f x o g"  by (simp add: o_assoc idem_comp)lemma in_comp_idem:  assumes "finite A" and "x ∈ A"  shows "F A o f x = F A"using assms by (induct A)  (auto simp add: comp_fun_commutes idem_comp, simp add: commute_left_comp' [symmetric] comp_fun_commute')lemma subset_comp_idem:  assumes "finite A" and "B ⊆ A"  shows "F A o F B = F A"proof -  from assms have "finite B" by (blast dest: finite_subset)  then show ?thesis using `B ⊆ A` by (induct B)    (simp_all add: o_assoc in_comp_idem `finite A`)qeddeclare insert [simp del]lemma insert_idem [simp]:  assumes "finite A"  shows "F (insert x A) = F A o f x"  using assms by (cases "x ∈ A") (simp_all add: insert in_comp_idem insert_absorb)lemma union_idem:  assumes "finite A" and "finite B"  shows "F (A ∪ B) = F A o F B"proof -  from assms have "finite (A ∪ B)" and "A ∩ B ⊆ A ∪ B" by auto  then have "F (A ∪ B) o F (A ∩ B) = F (A ∪ B)" by (rule subset_comp_idem)  with assms show ?thesis by (simp add: union_inter)qedendsubsubsection {* The image case with fixed function *}no_notation times (infixl "*" 70)no_notation Groups.one ("1")locale folding_image_simple = comm_monoid +  fixes g :: "('b => 'a)"  fixes F :: "'b set => 'a"  assumes eq_fold_g: "finite A ==> F A = fold_image f g 1 A"beginlemma empty [simp]:  "F {} = 1"  by (simp add: eq_fold_g)lemma insert [simp]:  assumes "finite A" and "x ∉ A"  shows "F (insert x A) = g x * F A"proof -  interpret comp_fun_commute "%x y. (g x) * y"    by default (simp add: ac_simps fun_eq_iff)  from assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"    by (simp add: fold_image_def)  with `finite A` show ?thesis by (simp add: eq_fold_g)qedlemma remove:  assumes "finite A" and "x ∈ A"  shows "F A = g x * F (A - {x})"proof -  from `x ∈ A` obtain B where A: "A = insert x B" and "x ∉ B"    by (auto dest: mk_disjoint_insert)  moreover from `finite A` this have "finite B" by simp  ultimately show ?thesis by simpqedlemma insert_remove:  assumes "finite A"  shows "F (insert x A) = g x * F (A - {x})"  using assms by (cases "x ∈ A") (simp_all add: remove insert_absorb)lemma neutral:  assumes "finite A" and "∀x∈A. g x = 1"  shows "F A = 1"  using assms by (induct A) simp_alllemma union_inter:  assumes "finite A" and "finite B"  shows "F (A ∪ B) * F (A ∩ B) = F A * F B"using assms proof (induct A)  case empty then show ?case by simpnext  case (insert x A) then show ?case    by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)qedcorollary union_inter_neutral:  assumes "finite A" and "finite B"  and I0: "∀x ∈ A∩B. g x = 1"  shows "F (A ∪ B) = F A * F B"  using assms by (simp add: union_inter [symmetric] neutral)corollary union_disjoint:  assumes "finite A" and "finite B"  assumes "A ∩ B = {}"  shows "F (A ∪ B) = F A * F B"  using assms by (simp add: union_inter_neutral)endsubsubsection {* The image case with flexible function *}locale folding_image = comm_monoid +  fixes F :: "('b => 'a) => 'b set => 'a"  assumes eq_fold: "!!g. finite A ==> F g A = fold_image f g 1 A"sublocale folding_image < folding_image_simple "op *" 1 g "F g" proofqed (fact eq_fold)context folding_imagebeginlemma reindex: (* FIXME polymorhism *)  assumes "finite A" and "inj_on h A"  shows "F g (h ` A) = F (g o h) A"  using assms by (induct A) autolemma cong:  assumes "finite A" and "!!x. x ∈ A ==> g x = h x"  shows "F g A = F h A"proof -  from assms have "ALL C. C <= A --> (ALL x:C. g x = h x) --> F g C = F h C"  apply - apply (erule finite_induct) apply simp  apply (simp add: subset_insert_iff, clarify)  apply (subgoal_tac "finite C")  prefer 2 apply (blast dest: finite_subset [rotated])  apply (subgoal_tac "C = insert x (C - {x})")  prefer 2 apply blast  apply (erule ssubst)  apply (drule spec)  apply (erule (1) notE impE)  apply (simp add: Ball_def del: insert_Diff_single)  done  with assms show ?thesis by simpqedlemma UNION_disjoint:  assumes "finite I" and "∀i∈I. finite (A i)"  and "∀i∈I. ∀j∈I. i ≠ j --> A i ∩ A j = {}"  shows "F g (UNION I A) = F (F g o A) I"apply (insert assms)apply (induct rule: finite_induct)apply simpapply atomizeapply (subgoal_tac "∀i∈Fa. x ≠ i") prefer 2 apply blastapply (subgoal_tac "A x Int UNION Fa A = {}") prefer 2 apply blastapply (simp add: union_disjoint)donelemma distrib:  assumes "finite A"  shows "F (λx. g x * h x) A = F g A * F h A"  using assms by (rule finite_induct) (simp_all add: assoc commute left_commute)lemma related:   assumes Re: "R 1 1"   and Rop: "∀x1 y1 x2 y2. R x1 x2 ∧ R y1 y2 --> R (x1 * y1) (x2 * y2)"   and fS: "finite S" and Rfg: "∀x∈S. R (h x) (g x)"  shows "R (F h S) (F g S)"  using fS by (rule finite_subset_induct) (insert assms, auto)lemma eq_general:  assumes fS: "finite S"  and h: "∀y∈S'. ∃!x. x ∈ S ∧ h x = y"   and f12:  "∀x∈S. h x ∈ S' ∧ f2 (h x) = f1 x"  shows "F f1 S = F f2 S'"proof-  from h f12 have hS: "h ` S = S'" by blast  {fix x y assume H: "x ∈ S" "y ∈ S" "h x = h y"    from f12 h H  have "x = y" by auto }  hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast  from f12 have th: "!!x. x ∈ S ==> (f2 o h) x = f1 x" by auto   from hS have "F f2 S' = F f2 (h ` S)" by simp  also have "… = F (f2 o h) S" using reindex [OF fS hinj, of f2] .  also have "… = F f1 S " using th cong [OF fS, of "f2 o h" f1]    by blast  finally show ?thesis ..qedlemma eq_general_inverses:  assumes fS: "finite S"   and kh: "!!y. y ∈ T ==> k y ∈ S ∧ h (k y) = y"  and hk: "!!x. x ∈ S ==> h x ∈ T ∧ k (h x) = x ∧ g (h x) = j x"  shows "F j S = F g T"  (* metis solves it, but not yet available here *)  apply (rule eq_general [OF fS, of T h g j])  apply (rule ballI)  apply (frule kh)  apply (rule ex1I[])  apply blast  apply clarsimp  apply (drule hk) apply simp  apply (rule sym)  apply (erule conjunct1[OF conjunct2[OF hk]])  apply (rule ballI)  apply (drule hk)  apply blast  doneendsubsubsection {* The image case with fixed function and idempotency *}locale folding_image_simple_idem = folding_image_simple +  assumes idem: "x * x = x"sublocale folding_image_simple_idem < semilattice: semilattice proofqed (fact idem)context folding_image_simple_idembeginlemma in_idem:  assumes "finite A" and "x ∈ A"  shows "g x * F A = F A"  using assms by (induct A) (auto simp add: left_commute)lemma subset_idem:  assumes "finite A" and "B ⊆ A"  shows "F B * F A = F A"proof -  from assms have "finite B" by (blast dest: finite_subset)  then show ?thesis using `B ⊆ A` by (induct B)    (auto simp add: assoc in_idem `finite A`)qeddeclare insert [simp del]lemma insert_idem [simp]:  assumes "finite A"  shows "F (insert x A) = g x * F A"  using assms by (cases "x ∈ A") (simp_all add: insert in_idem insert_absorb)lemma union_idem:  assumes "finite A" and "finite B"  shows "F (A ∪ B) = F A * F B"proof -  from assms have "finite (A ∪ B)" and "A ∩ B ⊆ A ∪ B" by auto  then have "F (A ∩ B) * F (A ∪ B) = F (A ∪ B)" by (rule subset_idem)  with assms show ?thesis by (simp add: union_inter [of A B, symmetric] commute)qedendsubsubsection {* The image case with flexible function and idempotency *}locale folding_image_idem = folding_image +  assumes idem: "x * x = x"sublocale folding_image_idem < folding_image_simple_idem "op *" 1 g "F g" proofqed (fact idem)subsubsection {* The neutral-less case *}locale folding_one = abel_semigroup +  fixes F :: "'a set => 'a"  assumes eq_fold: "finite A ==> F A = fold1 f A"beginlemma singleton [simp]:  "F {x} = x"  by (simp add: eq_fold)lemma eq_fold':  assumes "finite A" and "x ∉ A"  shows "F (insert x A) = fold (op *) x A"proof -  interpret ab_semigroup_mult "op *" by default (simp_all add: ac_simps)  from assms show ?thesis by (simp add: eq_fold fold1_eq_fold)qedlemma insert [simp]:  assumes "finite A" and "x ∉ A" and "A ≠ {}"  shows "F (insert x A) = x * F A"proof -  from `A ≠ {}` obtain b where "b ∈ A" by blast  then obtain B where *: "A = insert b B" "b ∉ B" by (blast dest: mk_disjoint_insert)  with `finite A` have "finite B" by simp  interpret fold: folding "op *" "λa b. fold (op *) b a" proof  qed (simp_all add: fun_eq_iff ac_simps)  from `finite B` fold.comp_fun_commute' [of B x]    have "op * x o (λb. fold op * b B) = (λb. fold op * b B) o op * x" by simp  then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute)  from `finite B` * fold.insert [of B b]    have "(λx. fold op * x (insert b B)) = (λx. fold op * x B) o op * b" by simp  then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: fun_eq_iff)  from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert)qedlemma remove:  assumes "finite A" and "x ∈ A"  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"proof -  from assms obtain B where "A = insert x B" and "x ∉ B" by (blast dest: mk_disjoint_insert)  with assms show ?thesis by simpqedlemma insert_remove:  assumes "finite A"  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"  using assms by (cases "x ∈ A") (simp_all add: insert_absorb remove)lemma union_disjoint:  assumes "finite A" "A ≠ {}" and "finite B" "B ≠ {}" and "A ∩ B = {}"  shows "F (A ∪ B) = F A * F B"  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)lemma union_inter:  assumes "finite A" and "finite B" and "A ∩ B ≠ {}"  shows "F (A ∪ B) * F (A ∩ B) = F A * F B"proof -  from assms have "A ≠ {}" and "B ≠ {}" by auto  from `finite A` `A ≠ {}` `A ∩ B ≠ {}` show ?thesis proof (induct A rule: finite_ne_induct)    case (singleton x) then show ?case by (simp add: insert_absorb ac_simps)  next    case (insert x A) show ?case proof (cases "x ∈ B")      case True then have "B ≠ {}" by auto      with insert True `finite B` show ?thesis by (cases "A ∩ B = {}")        (simp_all add: insert_absorb ac_simps union_disjoint)    next      case False with insert have "F (A ∪ B) * F (A ∩ B) = F A * F B" by simp      moreover from False `finite B` insert have "finite (A ∪ B)" "x ∉ A ∪ B" "A ∪ B ≠ {}"        by auto      ultimately show ?thesis using False `finite A` `x ∉ A` `A ≠ {}` by (simp add: assoc)    qed  qedqedlemma closed:  assumes "finite A" "A ≠ {}" and elem: "!!x y. x * y ∈ {x, y}"  shows "F A ∈ A"using `finite A` `A ≠ {}` proof (induct rule: finite_ne_induct)  case singleton then show ?case by simpnext  case insert with elem show ?case by forceqedendsubsubsection {* The neutral-less case with idempotency *}locale folding_one_idem = folding_one +  assumes idem: "x * x = x"sublocale folding_one_idem < semilattice: semilattice proofqed (fact idem)context folding_one_idembeginlemma in_idem:  assumes "finite A" and "x ∈ A"  shows "x * F A = F A"proof -  from assms have "A ≠ {}" by auto  with `finite A` show ?thesis using `x ∈ A` by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)qedlemma subset_idem:  assumes "finite A" "B ≠ {}" and "B ⊆ A"  shows "F B * F A = F A"proof -  from assms have "finite B" by (blast dest: finite_subset)  then show ?thesis using `B ≠ {}` `B ⊆ A` by (induct B rule: finite_ne_induct)    (simp_all add: assoc in_idem `finite A`)qedlemma eq_fold_idem':  assumes "finite A"  shows "F (insert a A) = fold (op *) a A"proof -  interpret ab_semigroup_idem_mult "op *" by default (simp_all add: ac_simps)  from assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)qedlemma insert_idem [simp]:  assumes "finite A" and "A ≠ {}"  shows "F (insert x A) = x * F A"proof (cases "x ∈ A")  case False from `finite A` `x ∉ A` `A ≠ {}` show ?thesis by (rule insert)next  case True  from `finite A` `A ≠ {}` show ?thesis by (simp add: in_idem insert_absorb True)qed  lemma union_idem:  assumes "finite A" "A ≠ {}" and "finite B" "B ≠ {}"  shows "F (A ∪ B) = F A * F B"proof (cases "A ∩ B = {}")  case True with assms show ?thesis by (simp add: union_disjoint)next  case False  from assms have "finite (A ∪ B)" and "A ∩ B ⊆ A ∪ B" by auto  with False have "F (A ∩ B) * F (A ∪ B) = F (A ∪ B)" by (auto intro: subset_idem)  with assms False show ?thesis by (simp add: union_inter [of A B, symmetric] commute)qedlemma hom_commute:  assumes hom: "!!x y. h (x * y) = h x * h y"  and N: "finite N" "N ≠ {}" shows "h (F N) = F (h ` N)"using N proof (induct rule: finite_ne_induct)  case singleton thus ?case by simpnext  case (insert n N)  then have "h (F (insert n N)) = h (n * F N)" by simp  also have "… = h n * h (F N)" by (rule hom)  also have "h (F N) = F (h ` N)" by(rule insert)  also have "h n * … = F (insert (h n) (h ` N))"    using insert by(simp)  also have "insert (h n) (h ` N) = h ` insert n N" by simp  finally show ?case .qedendnotation times (infixl "*" 70)notation Groups.one ("1")subsection {* Finite cardinality *}text {* This definition, although traditional, is ugly to work with:@{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.But now that we have @{text fold_image} things are easy:*}definition card :: "'a set => nat" where  "card A = (if finite A then fold_image (op +) (λx. 1) 0 A else 0)"interpretation card: folding_image_simple "op +" 0 "λx. 1" card proofqed (simp add: card_def)lemma card_infinite [simp]:  "¬ finite A ==> card A = 0"  by (simp add: card_def)lemma card_empty:  "card {} = 0"  by (fact card.empty)lemma card_insert_disjoint:  "finite A ==> x ∉ A ==> card (insert x A) = Suc (card A)"  by simplemma card_insert_if:  "finite A ==> card (insert x A) = (if x ∈ A then card A else Suc (card A))"  by auto (simp add: card.insert_remove card.remove)lemma card_ge_0_finite:  "card A > 0 ==> finite A"  by (rule ccontr) simplemma card_0_eq [simp, no_atp]:  "finite A ==> card A = 0 <-> A = {}"  by (auto dest: mk_disjoint_insert)lemma finite_UNIV_card_ge_0:  "finite (UNIV :: 'a set) ==> card (UNIV :: 'a set) > 0"  by (rule ccontr) simplemma card_eq_0_iff:  "card A = 0 <-> A = {} ∨ ¬ finite A"  by autolemma card_gt_0_iff:  "0 < card A <-> A ≠ {} ∧ finite A"  by (simp add: neq0_conv [symmetric] card_eq_0_iff) lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"apply(rule_tac t = A in insert_Diff [THEN subst], assumption)apply(simp del:insert_Diff_single)donelemma card_Diff_singleton:  "finite A ==> x: A ==> card (A - {x}) = card A - 1"by (simp add: card_Suc_Diff1 [symmetric])lemma card_Diff_singleton_if:  "finite A ==> card (A - {x}) = (if x : A then card A - 1 else card A)"by (simp add: card_Diff_singleton)lemma card_Diff_insert[simp]:assumes "finite A" and "a:A" and "a ~: B"shows "card(A - insert a B) = card(A - B) - 1"proof -  have "A - insert a B = (A - B) - {a}" using assms by blast  then show ?thesis using assms by(simp add:card_Diff_singleton)qedlemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)lemma card_insert_le: "finite A ==> card A <= card (insert x A)"by (simp add: card_insert_if)lemma card_Collect_less_nat[simp]: "card{i::nat. i < n} = n"by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = Suc n"using card_Collect_less_nat[of "Suc n"] by(simp add: less_Suc_eq_le)lemma card_mono:  assumes "finite B" and "A ⊆ B"  shows "card A ≤ card B"proof -  from assms have "finite A" by (auto intro: finite_subset)  then show ?thesis using assms proof (induct A arbitrary: B)    case empty then show ?case by simp  next    case (insert x A)    then have "x ∈ B" by simp    from insert have "A ⊆ B - {x}" and "finite (B - {x})" by auto    with insert.hyps have "card A ≤ card (B - {x})" by auto    with `finite A` `x ∉ A` `finite B` `x ∈ B` show ?case by simp (simp only: card.remove)  qedqedlemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"apply (induct rule: finite_induct)apply simpapply clarifyapply (subgoal_tac "finite A & A - {x} <= F") prefer 2 apply (blast intro: finite_subset, atomize)apply (drule_tac x = "A - {x}" in spec)apply (simp add: card_Diff_singleton_if split add: split_if_asm)apply (case_tac "card A", auto)donelemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"apply (simp add: psubset_eq linorder_not_le [symmetric])apply (blast dest: card_seteq)donelemma card_Un_Int: "finite A ==> finite B    ==> card A + card B = card (A Un B) + card (A Int B)"  by (fact card.union_inter [symmetric])lemma card_Un_disjoint: "finite A ==> finite B    ==> A Int B = {} ==> card (A Un B) = card A + card B"  by (fact card.union_disjoint)lemma card_Diff_subset:  assumes "finite B" and "B ⊆ A"  shows "card (A - B) = card A - card B"proof (cases "finite A")  case False with assms show ?thesis by simpnext  case True with assms show ?thesis by (induct B arbitrary: A) simp_allqedlemma card_Diff_subset_Int:  assumes AB: "finite (A ∩ B)" shows "card (A - B) = card A - card (A ∩ B)"proof -  have "A - B = A - A ∩ B" by auto  thus ?thesis    by (simp add: card_Diff_subset AB) qedlemma diff_card_le_card_Diff:assumes "finite B" shows "card A - card B ≤ card(A - B)"proof-  have "card A - card B ≤ card A - card (A ∩ B)"    using card_mono[OF assms Int_lower2, of A] by arith  also have "… = card(A-B)" using assms by(simp add: card_Diff_subset_Int)  finally show ?thesis .qedlemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"apply (rule Suc_less_SucD)apply (simp add: card_Suc_Diff1 del:card_Diff_insert)donelemma card_Diff2_less:  "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"apply (case_tac "x = y") apply (simp add: card_Diff1_less del:card_Diff_insert)apply (rule less_trans) prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)donelemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"apply (case_tac "x : A") apply (simp_all add: card_Diff1_less less_imp_le)donelemma card_psubset: "finite B ==> A ⊆ B ==> card A < card B ==> A < B"by (erule psubsetI, blast)lemma insert_partition:  "[| x ∉ F; ∀c1 ∈ insert x F. ∀c2 ∈ insert x F. c1 ≠ c2 --> c1 ∩ c2 = {} |]  ==> x ∩ \<Union> F = {}"by autolemma finite_psubset_induct[consumes 1, case_names psubset]:  assumes fin: "finite A"   and     major: "!!A. finite A ==> (!!B. B ⊂ A ==> P B) ==> P A"   shows "P A"using finproof (induct A taking: card rule: measure_induct_rule)  case (less A)  have fin: "finite A" by fact  have ih: "!!B. [|card B < card A; finite B|] ==> P B" by fact  { fix B     assume asm: "B ⊂ A"    from asm have "card B < card A" using psubset_card_mono fin by blast    moreover    from asm have "B ⊆ A" by auto    then have "finite B" using fin finite_subset by blast    ultimately     have "P B" using ih by simp  }  with fin show "P A" using major by blastqedtext{* main cardinality theorem *}lemma card_partition [rule_format]:  "finite C ==>     finite (\<Union> C) -->     (∀c∈C. card c = k) -->     (∀c1 ∈ C. ∀c2 ∈ C. c1 ≠ c2 --> c1 ∩ c2 = {}) -->     k * card(C) = card (\<Union> C)"apply (erule finite_induct, simp)apply (simp add: card_Un_disjoint insert_partition        finite_subset [of _ "\<Union> (insert x F)"])donelemma card_eq_UNIV_imp_eq_UNIV:  assumes fin: "finite (UNIV :: 'a set)"  and card: "card A = card (UNIV :: 'a set)"  shows "A = (UNIV :: 'a set)"proof  show "A ⊆ UNIV" by simp  show "UNIV ⊆ A"  proof    fix x    show "x ∈ A"    proof (rule ccontr)      assume "x ∉ A"      then have "A ⊂ UNIV" by auto      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)      with card show False by simp    qed  qedqedtext{*The form of a finite set of given cardinality*}lemma card_eq_SucD:assumes "card A = Suc k"shows "∃b B. A = insert b B & b ∉ B & card B = k & (k=0 --> B={})"proof -  have fin: "finite A" using assms by (auto intro: ccontr)  moreover have "card A ≠ 0" using assms by auto  ultimately obtain b where b: "b ∈ A" by auto  show ?thesis  proof (intro exI conjI)    show "A = insert b (A-{b})" using b by blast    show "b ∉ A - {b}" by blast    show "card (A - {b}) = k" and "k = 0 --> A - {b} = {}"      using assms b fin by(fastforce dest:mk_disjoint_insert)+  qedqedlemma card_Suc_eq:  "(card A = Suc k) =   (∃b B. A = insert b B & b ∉ B & card B = k & (k=0 --> B={}))"apply(rule iffI) apply(erule card_eq_SucD)apply(auto)apply(subst card_insert) apply(auto intro:ccontr)donelemma card_le_Suc_iff: "finite A ==>  Suc n ≤ card A = (∃a B. A = insert a B ∧ a ∉ B ∧ n ≤ card B ∧ finite B)"by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff  dest: subset_singletonD split: nat.splits if_splits)lemma finite_fun_UNIVD2:  assumes fin: "finite (UNIV :: ('a => 'b) set)"  shows "finite (UNIV :: 'b set)"proof -  from fin have "!!arbitrary. finite (range (λf :: 'a => 'b. f arbitrary))"    by (rule finite_imageI)  moreover have "!!arbitrary. UNIV = range (λf :: 'a => 'b. f arbitrary)"    by (rule UNIV_eq_I) auto  ultimately show "finite (UNIV :: 'b set)" by simpqedlemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"  unfolding UNIV_unit by simplemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"  unfolding UNIV_bool by simpsubsubsection {* Cardinality of image *}lemma card_image_le: "finite A ==> card (f ` A) <= card A"apply (induct rule: finite_induct) apply simpapply (simp add: le_SucI card_insert_if)donelemma card_image:  assumes "inj_on f A"  shows "card (f ` A) = card A"proof (cases "finite A")  case True then show ?thesis using assms by (induct A) simp_allnext  case False then have "¬ finite (f ` A)" using assms by (auto dest: finite_imageD)  with False show ?thesis by simpqedlemma bij_betw_same_card: "bij_betw f A B ==> card A = card B"by(auto simp: card_image bij_betw_def)lemma endo_inj_surj: "finite A ==> f ` A ⊆ A ==> inj_on f A ==> f ` A = A"by (simp add: card_seteq card_image)lemma eq_card_imp_inj_on:  "[| finite A; card(f ` A) = card A |] ==> inj_on f A"apply (induct rule:finite_induct)apply simpapply(frule card_image_le[where f = f])apply(simp add:card_insert_if split:if_splits)donelemma inj_on_iff_eq_card:  "finite A ==> inj_on f A = (card(f ` A) = card A)"by(blast intro: card_image eq_card_imp_inj_on)lemma card_inj_on_le:  "[|inj_on f A; f ` A ⊆ B; finite B |] ==> card A ≤ card B"apply (subgoal_tac "finite A")  apply (force intro: card_mono simp add: card_image [symmetric])apply (blast intro: finite_imageD dest: finite_subset) donelemma card_bij_eq:  "[|inj_on f A; f ` A ⊆ B; inj_on g B; g ` B ⊆ A;     finite A; finite B |] ==> card A = card B"by (auto intro: le_antisym card_inj_on_le)lemma bij_betw_finite:  assumes "bij_betw f A B"  shows "finite A <-> finite B"using assms unfolding bij_betw_defusing finite_imageD[of f A] by autosubsubsection {* Pigeonhole Principles *}lemma pigeonhole: "card A > card(f ` A) ==> ~ inj_on f A "by (auto dest: card_image less_irrefl_nat)lemma pigeonhole_infinite:assumes  "~ finite A" and "finite(f`A)"shows "EX a0:A. ~finite{a:A. f a = f a0}"proof -  have "finite(f`A) ==> ~ finite A ==> EX a0:A. ~finite{a:A. f a = f a0}"  proof(induct "f`A" arbitrary: A rule: finite_induct)    case empty thus ?case by simp  next    case (insert b F)    show ?case    proof cases      assume "finite{a:A. f a = b}"      hence "~ finite(A - {a:A. f a = b})" using `¬ finite A` by simp      also have "A - {a:A. f a = b} = {a:A. f a ≠ b}" by blast      finally have "~ finite({a:A. f a ≠ b})" .      from insert(3)[OF _ this]      show ?thesis using insert(2,4) by simp (blast intro: rev_finite_subset)    next      assume 1: "~finite{a:A. f a = b}"      hence "{a ∈ A. f a = b} ≠ {}" by force      thus ?thesis using 1 by blast    qed  qed  from this[OF assms(2,1)] show ?thesis .qedlemma pigeonhole_infinite_rel:assumes "~finite A" and "finite B" and "ALL a:A. EX b:B. R a b"shows "EX b:B. ~finite{a:A. R a b}"proof -   let ?F = "%a. {b:B. R a b}"   from finite_Pow_iff[THEN iffD2, OF `finite B`]   have "finite(?F ` A)" by(blast intro: rev_finite_subset)   from pigeonhole_infinite[where f = ?F, OF assms(1) this]   obtain a0 where "a0∈A" and 1: "¬ finite {a∈A. ?F a = ?F a0}" ..   obtain b0 where "b0 : B" and "R a0 b0" using `a0:A` assms(3) by blast   { assume "finite{a:A. R a b0}"     then have "finite {a∈A. ?F a = ?F a0}"       using `b0 : B` `R a0 b0` by(blast intro: rev_finite_subset)   }   with 1 `b0 : B` show ?thesis by blastqedsubsubsection {* Cardinality of sums *}lemma card_Plus:  assumes "finite A" and "finite B"  shows "card (A <+> B) = card A + card B"proof -  have "Inl`A ∩ Inr`B = {}" by fast  with assms show ?thesis    unfolding Plus_def    by (simp add: card_Un_disjoint card_image)qedlemma card_Plus_conv_if:  "card (A <+> B) = (if finite A ∧ finite B then card A + card B else 0)"  by (auto simp add: card_Plus)subsubsection {* Cardinality of the Powerset *}lemma card_Pow: "finite A ==> card (Pow A) = 2 ^ card A"apply (induct rule: finite_induct) apply (simp_all add: Pow_insert)apply (subst card_Un_disjoint, blast)  apply (blast, blast)apply (subgoal_tac "inj_on (insert x) (Pow F)") apply (subst mult_2) apply (simp add: card_image Pow_insert)apply (unfold inj_on_def)apply (blast elim!: equalityE)donetext {* Relates to equivalence classes.  Based on a theorem of F. Kamm\"uller.  *}lemma dvd_partition:  "finite (Union C) ==>    ALL c : C. k dvd card c ==>    (ALL c1: C. ALL c2: C. c1 ≠ c2 --> c1 Int c2 = {}) ==>  k dvd card (Union C)"apply (frule finite_UnionD)apply (rotate_tac -1)apply (induct rule: finite_induct)apply simp_allapply clarifyapply (subst card_Un_disjoint)   apply (auto simp add: disjoint_eq_subset_Compl)donesubsubsection {* Relating injectivity and surjectivity *}lemma finite_surj_inj: "finite A ==> A ⊆ f ` A ==> inj_on f A"apply(rule eq_card_imp_inj_on, assumption)apply(frule finite_imageI)apply(drule (1) card_seteq) apply(erule card_image_le)apply simpdonelemma finite_UNIV_surj_inj: fixes f :: "'a => 'a"shows "finite(UNIV:: 'a set) ==> surj f ==> inj f"by (blast intro: finite_surj_inj subset_UNIV)lemma finite_UNIV_inj_surj: fixes f :: "'a => 'a"shows "finite(UNIV:: 'a set) ==> inj f ==> surj f"by(fastforce simp:surj_def dest!: endo_inj_surj)corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"proof  assume "finite(UNIV::nat set)"  with finite_UNIV_inj_surj[of Suc]  show False by simp (blast dest: Suc_neq_Zero surjD)qed(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)lemma infinite_UNIV_char_0[no_atp]:  "¬ finite (UNIV::'a::semiring_char_0 set)"proof  assume "finite (UNIV::'a set)"  with subset_UNIV have "finite (range of_nat::'a set)"    by (rule finite_subset)  moreover have "inj (of_nat::nat => 'a)"    by (simp add: inj_on_def)  ultimately have "finite (UNIV::nat set)"    by (rule finite_imageD)  then show "False"    by simpqedhide_const (open) Finite_Set.foldend`