Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Finite_Set.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
    Author:     Jeremy Avigad
    Author:     Andrei Popescu
*)

section \<open>Finite sets\<close>

theory Finite_Set
  imports Product_Type Sum_Type Fields
begin

subsection \<open>Predicate for finite sets\<close>

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)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>

declare [[simproc del: finite_Collect]]

lemma finite_induct [case_names empty insert, induct set: finite]:
  \<comment> \<open>Discharging \<open>x \<notin> F\<close> entails extra work.\<close>
  assumes "finite F"
  assumes "P {}"
    and insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)"
  shows "P F"
  using \<open>finite F\<close>
proof induct
  show "P {}" by fact
next
  fix x F
  assume F: "finite F" and P: "P F"
  show "P (insert x F)"
  proof cases
    assume "x \ F"
    then have "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"
    and empty: "P {}"
    and 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 \<open>Choice principles\<close>

lemma ex_new_if_finite: \<comment> \<open>does not depend on def of finite at all\<close>
  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 \<open>A finite choice principle. Does not need the SOME choice operator.\<close>

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: "\x\A. P x (f x)" and ab: "P a b"
    by auto
  show ?case (is "\f. ?P f")
  proof
    show "?P (\x. if x = a then b else f x)"
      using f ab by auto
  qed
qed

subsubsection \<open>Finite sets are the images of initial segments of natural numbers\<close>

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
  then have "insert a A = f(n:=a) ` {i. i < Suc n}" and "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)
  then show ?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
  then show ?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 "\k
    case True
    then have "A = ?B"
      using Suc.prems by (auto simp:less_Suc_eq)
    then show ?thesis
      using finB by simp
  next
    case False
    then have "A = insert (f n) ?B"
      using Suc.prems by (auto simp:less_Suc_eq)
    then show ?thesis using finB by simp
  qed
qed

lemma finite_conv_nat_seg_image: "finite A \ (\n 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. f ` A = {i::nat. i < n} \ inj_on f A"
proof -
  from finite_imp_nat_seg_image_inj_on [OF \<open>finite A\<close>]
  obtain f and n :: nat where bij: "bij_betw f {i. i
    by (auto simp: bij_betw_def)
  let ?f = "the_inv_into {i. i
  have "inj_on ?f A \ ?f ` A = {i. i
    by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
  then show ?thesis by blast
qed

lemma 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)

subsection \<open>Finiteness and common set operations\<close>

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})" .
    then have "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 \<open>finite B\<close> 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 (\(B ` A)) \ (\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 \<open>x \<notin> B\<close> have "B = f ` A - {x}"
    by blast
  with B_A \<open>x \<notin> B\<close> \<open>x = f y\<close> \<open>inj_on f A\<close> \<open>y \<in> A\<close> have "B = f ` (A - {y})"
    by (simp add: inj_on_image_set_diff)
  moreover from \<open>inj_on f A\<close> 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_image_iff: "inj_on f A \ finite (f ` A) \ finite A"
  using finite_imageD by blast

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 all_subset_image: "(\B. B \ f ` A \ P B) \ (\B. B \ A \ P(f ` B))"
  by (safe elim!: subset_imageE) (use image_mono in \<open>blast+\<close>) (* slow *)

lemma all_finite_subset_image:
  "(\B. finite B \ B \ f ` A \ P B) \ (\B. finite B \ B \ A \ P (f ` B))"
proof safe
  fix B :: "'a set"
  assume B: "finite B" "B \ f ` A" and P: "\B. finite B \ B \ A \ P (f ` B)"
  show "P B"
    using finite_subset_image [OF B] P by blast
qed blast

lemma ex_finite_subset_image:
  "(\B. finite B \ B \ f ` A \ P B) \ (\B. finite B \ B \ A \ P (f ` B))"
proof safe
  fix B :: "'a set"
  assume B: "finite B" "B \ f ` A" and "P B"
  show "\B. finite B \ B \ A \ P (f ` B)"
    using finite_subset_image [OF B] \<open>P B\<close> by blast
qed blast

lemma finite_vimage_IntI: "finite F \ inj_on h A \ finite (h -` F \ A)"
proof (induct rule: finite_induct)
  case (insert x F)
  then show ?case
    by (simp add: vimage_insert [of h x F] finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
qed simp

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. \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)"
  unfolding Sigma_def by 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 \<open>B \<noteq> {}\<close> have "A = (fst \<circ> 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 \ B) = snd ` f ` {i::nat. i < n}"
    by simp
  with \<open>A \<noteq> {}\<close> have "B = (snd \<circ> f) ` {i::nat. i < n}"
    by (simp add: image_comp)
  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_cartesian_product_iff:
  "finite (A \ B) \ (A = {} \ B = {} \ (finite A \ finite B))"
  by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)

lemma finite_prod:
  "finite (UNIV :: ('a \ 'b) set) \ finite (UNIV :: 'a set) \ finite (UNIV :: 'b set)"
  using finite_cartesian_product_iff[of UNIV UNIV] by simp

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)  (* somewhat slow *)
  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_set: "finite (UNIV :: 'a set set) \ finite (UNIV :: 'a set)"
  by (simp only: finite_Pow_iff Pow_UNIV[symmetric])

lemma finite_UnionD: "finite (\A) \ finite A"
  by (blast intro: finite_subset [OF subset_Pow_Union])

lemma finite_bind:
  assumes "finite S"
  assumes "\x \ S. finite (f x)"
  shows "finite (Set.bind S f)"
using assms by (simp add: bind_UNION)

lemma finite_filter [simp]: "finite S \ finite (Set.filter P S)"
unfolding Set.filter_def by simp

lemma finite_set_of_finite_funs:
  assumes "finite A" "finite B"
  shows "finite {f. \x. (x \ A \ f x \ B) \ (x \ A \ f x = d)}" (is "finite ?S")
proof -
  let ?F = "\f. {(a,b). a \ A \ b = f a}"
  have "?F ` ?S \ Pow(A \ B)"
    by auto
  from finite_subset[OF this] assms have 1: "finite (?F ` ?S)"
    by simp
  have 2: "inj_on ?F ?S"
    by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)  (* somewhat slow *)
  show ?thesis
    by (rule finite_imageD [OF 1 2])
qed

lemma not_finite_existsD:
  assumes "\ finite {a. P a}"
  shows "\a. P a"
proof (rule classical)
  assume "\ ?thesis"
  with assms show ?thesis by auto
qed

subsection \<open>Further induction rules on finite sets\<close>

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"
    and empty: "P {}"
    and insert: "\a F. finite F \ a \ A \ a \ F \ P F \ P (insert a F)"
  shows "P F"
  using \<open>finite F\<close> \<open>F \<subseteq> A\<close>
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"
    and "P A"
    and remove: "\a A. finite A \ a \ A \ P A \ P (A - {a})"
  shows "P {}"
proof -
  have "P (A - B)" if "B \ A" for B :: "'a set"
  proof -
    from \<open>finite A\<close> that have "finite B"
      by (rule rev_finite_subset)
    from this \<open>B \<subseteq> A\<close> show "P (A - B)"
    proof induct
      case empty
      from \<open>P A\<close> show ?case by simp
    next
      case (insert b B)
      have "P (A - B - {b})"
      proof (rule remove)
        from \<open>finite A\<close> 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

lemma finite_update_induct [consumes 1, case_names const update]:
  assumes finite: "finite {a. f a \ c}"
    and const: "P (\a. c)"
    and update: "\a b f. finite {a. f a \ c} \ f a = c \ b \ c \ P f \ P (f(a := b))"
  shows "P f"
  using finite
proof (induct "{a. f a \ c}" arbitrary: f)
  case empty
  with const show ?case by simp
next
  case (insert a A)
  then have "A = {a'. (f(a := c)) a' \ c}" and "f a \ c"
    by auto
  with \<open>finite A\<close> have "finite {a'. (f(a := c)) a' \<noteq> c}"
    by simp
  have "(f(a := c)) a = c"
    by simp
  from insert \<open>A = {a'. (f(a := c)) a' \<noteq> c}\<close> have "P (f(a := c))"
    by simp
  with \<open>finite {a'. (f(a := c)) a' \<noteq> c}\<close> \<open>(f(a := c)) a = c\<close> \<open>f a \<noteq> c\<close>
  have "P ((f(a := c))(a := f a))"
    by (rule update)
  then show ?case by simp
qed

lemma finite_subset_induct' [consumes 2, case_names empty insert]:
  assumes "finite F" and "F \ A"
    and empty: "P {}"
    and insert: "\a F. \finite F; a \ A; F \ A; a \ F; P F \ \ P (insert a F)"
  shows "P F"
  using assms(1,2)
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
    show "F \ A" by fact
  qed
qed

subsection \<open>Class \<open>finite\<close>\<close>

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 prod :: (finite, finite) finite
  by standard (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) 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 bool :: finite
  by standard (simp add: UNIV_bool)

instance set :: (finite) finite
  by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)

instance unit :: finite
  by standard (simp add: UNIV_unit)

instance sum :: (finite, finite) finite
  by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)

subsection \<open>A basic fold functional for finite sets\<close>

text \<open>The intended behaviour is
  \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
  if \<open>f\<close> is ``left-commutative'':
\<close>

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 y (f x z) = f x (f y z)"
  using comp_fun_commute by (simp add: fun_eq_iff)

lemma commute_left_comp: "f y \ (f x \ g) = f x \ (f y \ g)"
  by (simp add: o_assoc comp_fun_commute)

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"

lemma fold_graph_closed_lemma:
  "fold_graph f z A x \ x \ B"
  if "fold_graph g z A x"
    "\a b. a \ A \ b \ B \ f a b = g a b"
    "\a b. a \ A \ b \ B \ g a b \ B"
    "z \ B"
  using that(1-3)
proof (induction rule: fold_graph.induct)
  case (insertI x A y)
  have "fold_graph f z A y" "y \ B"
    unfolding atomize_conj
    by (rule insertI.IH) (auto intro: insertI.prems)
  then have "g x y \ B" and f_eq: "f x y = g x y"
    by (auto simp: insertI.prems)
  moreover have "fold_graph f z (insert x A) (f x y)"
    by (rule fold_graph.insertI; fact)
  ultimately
  show ?case
    by (simp add: f_eq)
qed (auto intro!: that)

lemma fold_graph_closed_eq:
  "fold_graph f z A = fold_graph g z A"
  if "\a b. a \ A \ b \ B \ f a b = g a b"
     "\a b. a \ A \ b \ B \ g a b \ B"
     "z \ B"
  using fold_graph_closed_lemma[of f z A _ B g] fold_graph_closed_lemma[of g z A _ B f] that
  by auto

definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"
  where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)"

lemma fold_closed_eq: "fold f z A = fold g z A"
  if "\a b. a \ A \ b \ B \ f a b = g a b"
     "\a b. a \ A \ b \ B \ g a b \ B"
     "z \ B"
  unfolding Finite_Set.fold_def
  by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that)

text \<open>
  A tempting alternative for the definiens is
  \<^term>\<open>if finite A then THE y. fold_graph f z A y else e\<close>.
  It allows the removal of finiteness assumptions from the theorems
  \<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
  The proofs become ugly. It is not worth the effort. (???)
\<close>

lemma finite_imp_fold_graph: "finite A \ \x. fold_graph f z A x"
  by (induct rule: finite_induct) auto

subsubsection \<open>From \<^const>\<open>fold_graph\<close> to \<^term>\<open>fold\<close>\<close>

context comp_fun_commute
begin

lemma fold_graph_finite:
  assumes "fold_graph f z A y"
  shows "finite A"
  using assms by induct simp_all

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 emptyI
  then show ?case by simp
next
  case (insertI x A y)
  show ?case
  proof (cases "x = a")
    case True
    with insertI show ?thesis by auto
  next
    case False
    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 ?thesis
      by fast
  qed
qed

lemma 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 emptyI
  then show ?case by fast
next
  case (insertI x A y v)
  from \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
  obtain y' where "v = f x y'" and "fold_graph f z A y'"
    by (rule fold_graph_insertE)
  from \<open>fold_graph f z A y'\<close> have "y' = y"
    by (rule insertI)
  with \<open>v = f x y'\<close> show "v = f x y"
    by simp
qed

lemma fold_equality: "fold_graph f z A y \ fold f z A = y"
  by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite)

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')
  with assms show ?thesis
    by (simp add: fold_def)
qed

text \<open>The base case for \<open>fold\<close>:\<close>

lemma (in -) fold_infinite [simp]: "\ finite A \ fold f z A = z"
  by (auto simp: fold_def)

lemma (in -) fold_empty [simp]: "fold f z {} = z"
  by (auto simp: fold_def)

text \<open>The various recursion equations for \<^const>\<open>fold\<close>:\<close>

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)
  fix z
  from \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
    by (rule fold_graph_fold)
  with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))"
    by (rule fold_graph.insertI)
  then show "fold_graph f z (insert x A) (f x (fold f z A))"
    by simp
qed

declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
  \<comment> \<open>No more proofs involve these.\<close>

lemma fold_fun_left_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 simp
next
  case insert
  then show ?case
    by (simp add: fun_left_comm [of x])
qed

lemma fold_insert2: "finite A \ x \ A \ fold f z (insert x A) = fold f (f x z) A"
  by (simp add: fold_fun_left_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 \<open>x \<in> A\<close> 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: \<open>finite A\<close>)+
  finally show ?thesis .
qed

lemma fold_insert_remove:
  assumes "finite A"
  shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
proof -
  from \<open>finite A\<close> 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 simp
qed

lemma fold_set_union_disj:
  assumes "finite A" "finite B" "A \ B = {}"
  shows "Finite_Set.fold f z (A \ B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
  using assms(2,1,3) by induct simp_all

end

text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>

lemma fold_image:
  assumes "inj_on g A"
  shows "fold f z (g ` A) = fold (f \ g) z A"
proof (cases "finite A")
  case False
  with assms show ?thesis
    by (auto dest: finite_imageD simp add: fold_def)
next
  case True
  have "fold_graph f z (g ` A) = fold_graph (f \ g) z A"
  proof
    fix w
    show "fold_graph f z (g ` A) w \ fold_graph (f \ g) z A w" (is "?P \ ?Q")
    proof
      assume ?P
      then show ?Q
        using assms
      proof (induct "g ` A" w arbitrary: A)
        case emptyI
        then show ?case by (auto intro: fold_graph.emptyI)
      next
        case (insertI x A r B)
        from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
          where "x' \ A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
          by (rule inj_img_insertE)
        from insertI.prems have "fold_graph (f \ g) z A' r"
          by (auto intro: insertI.hyps)
        with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
          by (rule fold_graph.insertI)
        then show ?case
          by simp
      qed
    next
      assume ?Q
      then show ?P
        using assms
      proof induct
        case emptyI
        then show ?case
          by (auto intro: fold_graph.emptyI)
      next
        case (insertI x A r)
        from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
          by auto
        moreover from insertI have "fold_graph f z (g ` A) r"
          by simp
        ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
          by (rule fold_graph.insertI)
        then show ?case
          by simp
      qed
    qed
  qed
  with True assms show ?thesis
    by (auto simp add: fold_def)
qed

lemma fold_cong:
  assumes "comp_fun_commute f" "comp_fun_commute g"
    and "finite A"
    and cong: "\x. x \ A \ f x = g x"
    and "s = t" and "A = B"
  shows "fold f s A = fold g t B"
proof -
  have "fold f s A = fold g s A"
    using \<open>finite A\<close> cong
  proof (induct A)
    case empty
    then show ?case by simp
  next
    case insert
    interpret f: comp_fun_commute f by (fact \<open>comp_fun_commute f\<close>)
    interpret g: comp_fun_commute g by (fact \<open>comp_fun_commute g\<close>)
    from insert show ?case by simp
  qed
  with assms show ?thesis by simp
qed

text \<open>A simplified version for idempotent functions:\<close>

locale comp_fun_idem = comp_fun_commute +
  assumes comp_fun_idem: "f x \ f x = f x"
begin

lemma 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: comp_fun_idem fun_left_idem)
next
  assume "x \ A"
  then show ?thesis
    using assms by simp
qed

declare 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_left_comm)

end

subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close>

lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \ g)"
  by standard (simp_all add: comp_fun_commute)

lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f \ 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
  show "f y ^^ g y \ f x ^^ g x = f x ^^ g x \ f y ^^ g y" for x 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 \ f x = f x \ f y ^^ g y"
      proof (induct "g y" arbitrary: g)
        case 0
        then show ?case by simp
      next
        case (Suc n g)
        define h where "h z = g z - 1" for z
        with Suc have "n = h y"
          by simp
        with Suc have hyp: "f y ^^ h y \ f x = f x \ 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
      define h where "h z = (if z = x then g x - 1 else g z)" for z
      with Suc have "n = h x"
        by simp
      with Suc have "f y ^^ h y \ f x ^^ h x = f x ^^ h x \ f y ^^ h y"
        by auto
      with False h_def have hyp2: "f y ^^ g y \ f x ^^ h x = f x ^^ h x \ 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
  qed
qed

subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close>

lemma comp_fun_commute_const: "comp_fun_commute (\_. f)"
  by standard rule

lemma comp_fun_idem_insert: "comp_fun_idem insert"
  by standard auto

lemma comp_fun_idem_remove: "comp_fun_idem Set.remove"
  by standard auto

lemma (in semilattice_inf) comp_fun_idem_inf: "comp_fun_idem inf"
  by standard (auto simp add: inf_left_commute)

lemma (in semilattice_sup) comp_fun_idem_sup: "comp_fun_idem sup"
  by standard (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 \<open>finite A\<close> show ?thesis
    by (induct A arbitrary: B) simp_all
qed

lemma 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 \<open>finite A\<close> have "fold Set.remove B A = B - A"
    by (induct A arbitrary: B) auto  (* slow *)
  then show ?thesis ..
qed

lemma 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 standard (auto simp: fun_eq_iff)
qed

lemma 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 assms
  by induct
    (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 (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"
proof -
  interpret comp_fun_commute "\k A. Set.insert (f k) A"
    by standard auto
  show ?thesis
    using assms by (induct A) auto
qed

lemma Ball_fold:
  assumes "finite A"
  shows "Ball A P = fold (\k s. s \ P k) True A"
proof -
  interpret comp_fun_commute "\k s. s \ P k"
    by standard auto
  show ?thesis
    using assms by (induct A) auto
qed

lemma Bex_fold:
  assumes "finite A"
  shows "Bex A P = fold (\k s. s \ P k) False A"
proof -
  interpret comp_fun_commute "\k s. s \ P k"
    by standard auto
  show ?thesis
    using assms by (induct A) auto
qed

lemma 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) blast  (* somewhat slow *)

lemma Pow_fold:
  assumes "finite A"
  shows "Pow A = fold (\x A. A \ Set.insert x ` A) {{}} A"
proof -
  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)
qed

lemma fold_union_pair:
  assumes "finite B"
  shows "(\y\B. {(x, y)}) \ A = fold (\y. Set.insert (x, y)) A B"
proof -
  interpret comp_fun_commute "\y. Set.insert (x, y)"
    by standard auto
  show ?thesis
    using assms by (induct arbitrary: A) simp_all
qed

lemma comp_fun_commute_product_fold:
  "finite B \ comp_fun_commute (\x z. fold (\y. Set.insert (x, y)) z B)"
  by standard (auto simp: fold_union_pair [symmetric])

lemma product_fold:
  assumes "finite A" "finite B"
  shows "A \ B = fold (\x z. fold (\y. Set.insert (x, y)) z 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_lattice
begin

lemma inf_Inf_fold_inf:
  assumes "finite A"
  shows "inf (Inf A) B = fold inf B A"
proof -
  interpret comp_fun_idem inf
    by (fact comp_fun_idem_inf)
  from \<open>finite A\<close> fold_fun_left_comm show ?thesis
    by (induct A arbitrary: B) (simp_all add: inf_commute fun_eq_iff)
qed

lemma sup_Sup_fold_sup:
  assumes "finite A"
  shows "sup (Sup A) B = fold sup B A"
proof -
  interpret comp_fun_idem sup
    by (fact comp_fun_idem_sup)
  from \<open>finite A\<close> fold_fun_left_comm show ?thesis
    by (induct A arbitrary: B) (simp_all add: sup_commute fun_eq_iff)
qed

lemma Inf_fold_inf: "finite A \ Inf A = fold inf top A"
  using inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)

lemma Sup_fold_sup: "finite A \ Sup A = fold sup bot A"
  using sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)

lemma inf_INF_fold_inf:
  assumes "finite A"
  shows "inf B (\(f ` A)) = fold (inf \ f) B A" (is "?inf = ?fold")
proof -
  interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
  interpret comp_fun_idem "inf \ f" by (fact comp_comp_fun_idem)
  from \<open>finite A\<close> have "?fold = ?inf"
    by (induct A arbitrary: B) (simp_all add: inf_left_commute)
  then show ?thesis ..
qed

lemma sup_SUP_fold_sup:
  assumes "finite A"
  shows "sup B (\(f ` A)) = fold (sup \ f) B A" (is "?sup = ?fold")
proof -
  interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
  interpret comp_fun_idem "sup \ f" by (fact comp_comp_fun_idem)
  from \<open>finite A\<close> have "?fold = ?sup"
    by (induct A arbitrary: B) (simp_all add: sup_left_commute)
  then show ?thesis ..
qed

lemma INF_fold_inf: "finite A \ \(f ` A) = fold (inf \ f) top A"
  using inf_INF_fold_inf [of A top] by simp

lemma SUP_fold_sup: "finite A \ \(f ` A) = fold (sup \ f) bot A"
  using sup_SUP_fold_sup [of A bot] by simp

lemma finite_Inf_in:
  assumes "finite A" "A\{}" and inf: "\x y. \x \ A; y \ A\ \ inf x y \ A"
  shows "Inf A \ A"
proof -
  have "Inf B \ A" if "B \ A" "B\{}" for B
    using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
  by (induction B) (use inf in \<open>force+\<close>)
  then show ?thesis
    by (simp add: assms)
qed

lemma finite_Sup_in:
  assumes "finite A" "A\{}" and sup: "\x y. \x \ A; y \ A\ \ sup x y \ A"
  shows "Sup A \ A"
proof -
  have "Sup B \ A" if "B \ A" "B\{}" for B
    using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
  by (induction B) (use sup in \<open>force+\<close>)
  then show ?thesis
    by (simp add: assms)
qed

end

subsection \<open>Locales as mini-packages for fold operations\<close>

subsubsection \<open>The natural case\<close>

locale folding =
  fixes f :: "'a \ 'b \ 'b" and z :: "'b"
  assumes comp_fun_commute: "f y \ f x = f x \ f y"
begin

interpretation fold?: comp_fun_commute f
  by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>)

definition F :: "'a set \ 'b"
  where eq_fold: "F A = fold f z A"

lemma empty [simp]:"F {} = z"
  by (simp add: eq_fold)

lemma infinite [simp]: "\ finite A \ F A = z"
  by (simp add: eq_fold)

lemma insert [simp]:
  assumes "finite A" and "x \ A"
  shows "F (insert x A) = f x (F A)"
proof -
  from fold_insert assms
  have "fold f z (insert x A) = f x (fold f z A)" by simp
  with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
qed

lemma remove:
  assumes "finite A" and "x \ A"
  shows "F A = f x (F (A - {x}))"
proof -
  from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
    by (auto dest: mk_disjoint_insert)
  moreover from \<open>finite A\<close> A have "finite B" by simp
  ultimately show ?thesis by simp
qed

lemma insert_remove: "finite A \ F (insert x A) = f x (F (A - {x}))"
  by (cases "x \ A") (simp_all add: remove insert_absorb)

end

subsubsection \<open>With idempotency\<close>

locale folding_idem = folding +
  assumes comp_fun_idem: "f x \ f x = f x"
begin

declare insert [simp del]

interpretation fold?: comp_fun_idem f
  by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)

lemma insert_idem [simp]:
  assumes "finite A"
  shows "F (insert x A) = f x (F A)"
proof -
  from fold_insert_idem assms
  have "fold f z (insert x A) = f x (fold f z A)" by simp
  with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
qed

end

subsection \<open>Finite cardinality\<close>

text \<open>
  The traditional definition
  \<^prop>\<open>card A \<equiv> LEAST n. \<exists>f. A = {f i |i. i < n}\<close>
  is ugly to work with.
  But now that we have \<^const>\<open>fold\<close> things are easy:
\<close>

global_interpretation card: folding "\_. Suc" 0
  defines card = "folding.F (\_. Suc) 0"
  by standard rule

lemma card_insert_disjoint: "finite A \ x \ A \ card (insert x A) = Suc (card A)"
  by (fact card.insert)

lemma 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) simp

lemma card_0_eq [simp]: "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) simp

lemma card_eq_0_iff: "card A = 0 \ A = {} \ \ finite A"
  by auto

lemma card_range_greater_zero: "finite (range f) \ card (range f) > 0"
  by (rule ccontr) (simp add: card_eq_0_iff)

lemma card_gt_0_iff: "0 < card A \ A \ {} \ finite A"
  by (simp add: neq0_conv [symmetric] card_eq_0_iff)

lemma card_Suc_Diff1:
  assumes "finite A" "x \ A" shows "Suc (card (A - {x})) = card A"
proof -
  have "Suc (card (A - {x})) = card (insert x (A - {x}))"
    using assms by (simp add: card.insert_remove)
  also have "... = card A"
    using assms by (simp add: card_insert_if)
  finally show ?thesis .
qed

lemma card_insert_le_m1:
  assumes "n > 0" "card y \ n - 1" shows "card (insert x y) \ n"
  using assms
  by (cases "finite y") (auto simp: card_insert_if)

lemma 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)
qed

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 \<open>finite A\<close> \<open>x \<notin> A\<close> \<open>finite B\<close> \<open>x \<in> B\<close> show ?case
      by simp (simp only: card.remove)
  qed
qed

lemma card_seteq:
  assumes "finite B" and A: "A \ B" "card B \ card A"
  shows "A = B"
  using assms
proof (induction arbitrary: A rule: finite_induct)
  case (insert b B)
  then have A: "finite A" "A - {b} \ B"
    by force+
  then have "card B \ card (A - {b})"
    using insert by (auto simp add: card_Diff_singleton_if)
  then have "A - {b} = B"
    using A insert.IH by auto
  then show ?case
    using insert.hyps insert.prems by auto
qed auto

lemma psubset_card_mono: "finite B \ A < B \ card A < card B"
  using card_seteq [of B A] by (auto simp add: psubset_eq)

lemma card_Un_Int:
  assumes "finite A" "finite B"
  shows "card A + card B = card (A \ B) + card (A \ B)"
  using assms
proof (induct A)
  case empty
  then show ?case by simp
next
  case insert
  then show ?case
    by (auto simp add: insert_absorb Int_insert_left)
qed

lemma card_Un_disjoint: "finite A \ finite B \ A \ B = {} \ card (A \ B) = card A + card B"
  using card_Un_Int [of A B] by simp

lemma card_Un_disjnt: "\finite A; finite B; disjnt A B\ \ card (A \ B) = card A + card B"
  by (simp add: card_Un_disjoint disjnt_def)

lemma card_Un_le: "card (A \ B) \ card A + card B"
proof (cases "finite A \ finite B")
  case True
  then show ?thesis
    using le_iff_add card_Un_Int [of A B] by auto
qed auto

lemma card_Diff_subset:
  assumes "finite B"
    and "B \ A"
  shows "card (A - B) = card A - card B"
  using assms
proof (cases "finite A")
  case False
  with assms show ?thesis
    by simp
next
  case True
  with assms show ?thesis
    by (induct B arbitrary: A) simp_all
qed

lemma card_Diff_subset_Int:
  assumes "finite (A \ B)"
  shows "card (A - B) = card A - card (A \ B)"
proof -
  have "A - B = A - A \ B" by auto
  with assms show ?thesis
    by (simp add: card_Diff_subset)
qed

lemma 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 .
qed

lemma card_le_sym_Diff:
  assumes "finite A" "finite B" "card A \ card B"
  shows "card(A - B) \ card(B - A)"
proof -
  have "card(A - B) = card A - card (A \ B)" using assms(1,2) by(simp add: card_Diff_subset_Int)
  also have "\ \ card B - card (A \ B)" using assms(3) by linarith
  also have "\ = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute)
  finally show ?thesis .
qed

lemma card_less_sym_Diff:
  assumes "finite A" "finite B" "card A < card B"
  shows "card(A - B) < card(B - A)"
proof -
  have "card(A - B) = card A - card (A \ B)" using assms(1,2) by(simp add: card_Diff_subset_Int)
  also have "\ < card B - card (A \ B)" using assms(1,3) by (simp add: card_mono diff_less_mono)
  also have "\ = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute)
  finally show ?thesis .
qed

lemma card_Diff1_less_iff: "card (A - {x}) < card A \ finite A \ x \ A"
proof (cases "finite A \ x \ A")
  case True
  then show ?thesis
    by (auto simp: card_gt_0_iff intro: diff_less)
qed auto

lemma card_Diff1_less: "finite A \ x \ A \ card (A - {x}) < card A"
  unfolding card_Diff1_less_iff by auto

lemma card_Diff2_less:
  assumes "finite A" "x \ A" "y \ A" shows "card (A - {x} - {y}) < card A"
proof (cases "x = y")
  case True
  with assms show ?thesis
    by (simp add: card_Diff1_less del: card_Diff_insert)
next
  case False
  then have "card (A - {x} - {y}) < card (A - {x})" "card (A - {x}) < card A"
    using assms by (intro card_Diff1_less; simp)+
  then show ?thesis
    by (blast intro: less_trans)
qed

lemma card_Diff1_le: "finite A \ card (A - {x}) \ card A"
  by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le)

lemma card_psubset: "finite B \ A \ B \ card A < card B \ A < B"
  by (erule psubsetI) blast

lemma card_le_inj:
  assumes fA: "finite A"
    and fB: "finite B"
    and c: "card A \ card B"
  shows "\f. f ` A \ B \ inj_on f A"
  using fA fB c
proof (induct arbitrary: B rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x s t)
  then show ?case
  proof (induct rule: finite_induct [OF insert.prems(1)])
    case 1
    then show ?case by simp
  next
    case (2 y t)
    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \ card t"
      by simp
    from "2.prems"(3) [OF "2.hyps"(1) cst]
    obtain f where "f ` s \ t" "inj_on f s"
      by blast
    with "2.prems"(2) "2.hyps"(2) show ?case
      unfolding inj_on_def
      by (rule_tac x = "\z. if z = x then y else f z" in exI) auto
  qed
qed

lemma card_subset_eq:
  assumes fB: "finite B"
    and AB: "A \ B"
    and c: "card A = card B"
  shows "A = B"
proof -
  from fB AB have fA: "finite A"
    by (auto intro: finite_subset)
  from fA fB have fBA: "finite (B - A)"
    by auto
  have e: "A \ (B - A) = {}"
    by blast
  have eq: "A \ (B - A) = B"
    using AB by blast
  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
    by arith
  then have "B - A = {}"
    unfolding card_eq_0_iff using fA fB by simp
  with AB show "A = B"
    by blast
qed

lemma insert_partition:
  "x \ F \ \c1 \ insert x F. \c2 \ insert x F. c1 \ c2 \ c1 \ c2 = {} \ x \ \F = {}"
  by auto  (* somewhat slow *)

lemma finite_psubset_induct [consumes 1, case_names psubset]:
  assumes finite: "finite A"
    and major: "\A. finite A \ (\B. B \ A \ P B) \ P A"
  shows "P A"
  using finite
proof (induct A taking: card rule: measure_induct_rule)
  case (less A)
  have fin: "finite A" by fact
  have ih: "card B < card A \ finite B \ P B" for B by fact
  have "P B" if "B \ A" for B
  proof -
    from that have "card B < card A"
      using psubset_card_mono fin by blast
    moreover
    from that have "B \ A"
      by auto
    then have "finite B"
      using fin finite_subset by blast
    ultimately show ?thesis using ih by simp
  qed
  with fin show "P A" using major by blast
qed

lemma finite_induct_select [consumes 1, case_names empty select]:
  assumes "finite S"
    and "P {}"
    and select: "\T. T \ S \ P T \ \s\S - T. P (insert s T)"
  shows "P S"
proof -
  have "0 \ card S" by simp
  then have "\T \ S. card T = card S \ P T"
  proof (induct rule: dec_induct)
    case base with \<open>P {}\<close>
    show ?case
      by (intro exI[of _ "{}"]) auto
  next
    case (step n)
    then obtain T where T: "T \ S" "card T = n" "P T"
      by auto
    with \<open>n < card S\<close> have "T \<subset> S" "P T"
      by auto
    with select[of T] obtain s where "s \ S" "s \ T" "P (insert s T)"
      by auto
    with step(2) T \<open>finite S\<close> show ?case
      by (intro exI[of _ "insert s T"]) (auto dest: finite_subset)
  qed
  with \<open>finite S\<close> show "P S"
    by (auto dest: card_subset_eq)
qed

lemma remove_induct [case_names empty infinite remove]:
  assumes empty: "P ({} :: 'a set)"
    and infinite: "\ finite B \ P B"
    and remove: "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A"
  shows "P B"
proof (cases "finite B")
  case False
  then show ?thesis by (rule infinite)
next
  case True
  define A where "A = B"
  with True have "finite A" "A \ B"
    by simp_all
  then show "P A"
  proof (induct "card A" arbitrary: A)
    case 0
    then have "A = {}" by auto
    with empty show ?case by simp
  next
    case (Suc n A)
    from \<open>A \<subseteq> B\<close> and \<open>finite B\<close> have "finite A"
      by (rule finite_subset)
    moreover from Suc.hyps have "A \ {}" by auto
    moreover note \<open>A \<subseteq> B\<close>
    moreover have "P (A - {x})" if x: "x \ A" for x
      using x Suc.prems \<open>Suc n = card A\<close> by (intro Suc) auto
    ultimately show ?case by (rule remove)
  qed
qed

lemma finite_remove_induct [consumes 1, case_names empty remove]:
  fixes P :: "'a set \ bool"
  assumes "finite B"
    and "P {}"
    and "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A"
  defines "B' \ B"
  shows "P B'"
  by (induct B' rule: remove_induct) (simp_all add: assms)

text \<open>Main cardinality theorem.\<close>
lemma card_partition [rule_format]:
  "finite C \ finite (\C) \ (\c\C. card c = k) \
    (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}) \<Longrightarrow>
    k * card C = card (\<Union>C)"
proof (induct rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case
    by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\(insert _ _)"])
qed

lemma 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
    show "x \ A" for x
    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
  qed
qed

text \<open>The form of a finite set of given cardinality\<close>

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)+
  qed
qed

lemma card_Suc_eq:
  "card A = Suc k \
    (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
  by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD)

lemma card_1_singletonE:
  assumes "card A = 1"
  obtains x where "A = {x}"
  using assms by (auto simp: card_Suc_eq)

lemma is_singleton_altdef: "is_singleton A \ card A = 1"
  unfolding is_singleton_def
  by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)

lemma card_1_singleton_iff: "card A = Suc 0 \ (\x. A = {x})"
  by (simp add: card_Suc_eq)

lemma card_le_Suc0_iff_eq:
  assumes "finite A"
  shows "card A \ Suc 0 \ (\a1 \ A. \a2 \ A. a1 = a2)" (is "?C = ?A")
proof
  assume ?C thus ?A using assms by (auto simp: le_Suc_eq dest: card_eq_SucD)
next
  assume ?A
  show ?C
  proof cases
    assume "A = {}" thus ?C using \<open>?A\<close> by simp
  next
    assume "A \ {}"
    then obtain a where "A = {a}" using \<open>?A\<close> by blast
    thus ?C by simp
  qed
qed

lemma card_le_Suc_iff:
  "Suc n \ card A = (\a B. A = insert a B \ a \ B \ n \ card B \ finite B)"
proof (cases "finite A")
  case True
  then show ?thesis
    by (fastforce simp: card_Suc_eq less_eq_nat.simps split: nat.splits)
qed auto

lemma finite_fun_UNIVD2:
  assumes fin: "finite (UNIV :: ('a \ 'b) set)"
  shows "finite (UNIV :: 'b set)"
proof -
  from fin have "finite (range (\f :: 'a \ 'b. f arbitrary))" for arbitrary
    by (rule finite_imageI)
  moreover have "UNIV = range (\f :: 'a \ 'b. f arbitrary)" for arbitrary
    by (rule UNIV_eq_I) auto
  ultimately show "finite (UNIV :: 'b set)"
    by simp
qed

lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
  unfolding UNIV_unit by simp

lemma infinite_arbitrarily_large:
  assumes "\ finite A"
  shows "\B. finite B \ card B = n \ B \ A"
proof (induction n)
  case 0
  show ?case by (intro exI[of _ "{}"]) auto
next
  case (Suc n)
  then obtain B where B: "finite B \ card B = n \ B \ A" ..
  with \<open>\<not> finite A\<close> have "A \<noteq> B" by auto
  with B have "B \ A" by auto
  then have "\x. x \ A - B"
    by (elim psubset_imp_ex_mem)
  then obtain x where x: "x \ A - B" ..
  with B have "finite (insert x B) \ card (insert x B) = Suc n \ insert x B \ A"
    by auto
  then show "\B. finite B \ card B = Suc n \ B \ A" ..
qed

text \<open>Sometimes, to prove that a set is finite, it is convenient to work with finite subsets
and to show that their cardinalities are uniformly bounded. This possibility is formalized in
the next criterion.\<close>

lemma finite_if_finite_subsets_card_bdd:
  assumes "\G. G \ F \ finite G \ card G \ C"
  shows "finite F \ card F \ C"
proof (cases "finite F")
  case False
  obtain n::nat where n: "n > max C 0" by auto
  obtain G where G: "G \ F" "card G = n" using infinite_arbitrarily_large[OF False] by auto
  hence "finite G" using \<open>n > max C 0\<close> using card.infinite gr_implies_not0 by blast
  hence False using assms G n not_less by auto
  thus ?thesis ..
next
  case True thus ?thesis using assms[of F] by auto
qed

subsubsection \<open>Cardinality of image\<close>

lemma card_image_le: "finite A \ card (f ` A) \ card A"
  by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if)

lemma card_image: "inj_on f A \ card (f ` A) = card A"
proof (induct A rule: infinite_finite_induct)
  case (infinite A)
  then have "\ finite (f ` A)" by (auto dest: finite_imageD)
  with infinite show ?case by simp
qed simp_all

lemma 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:
  assumes "finite A" "card(f ` A) = card A"
  shows "inj_on f A"
  using assms
proof (induct rule:finite_induct)
  case empty
  show ?case by simp
next
  case (insert x A)
  then show ?case
    using card_image_le [of A f] by (simp add: card_insert_if split: if_splits)
qed

lemma inj_on_iff_eq_card: "finite A \ inj_on f A \ card (f ` A) = card A"
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.79 Sekunden (vorverarbeitet) ¤

zum Wurzelverzeichnis wechseln Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln sprechenden Kalenders
in der Quellcodebibliothek suchen

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Original von: Isabelle^©

¤ Dauer der Verarbeitung: 0.79 Sekunden (vorverarbeitet) ¤

Laden

in der Quellcodebibliothek suchen

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.79 Sekunden (vorverarbeitet) ¤

Laden

in der Quellcodebibliothek suchen

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©