Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Disjoint_Sets.thy
    Author:     Johannes Hölzl, TU München
*)

section \<open>Partitions and Disjoint Sets\<close>

theory Disjoint_Sets
  imports Main
begin

lemma range_subsetD: "range f \ B \ f i \ B"
  by blast

lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}"
  by blast

lemma Int_Diff_Un: "A \ B \ (A - B) = A"
  by blast

lemma mono_Un: "mono A \ (\i\n. A i) = A n"
  unfolding mono_def by auto

lemma disjnt_equiv_class: "equiv A r \ disjnt (r``{a}) (r``{b}) \ (a, b) \ r"
  by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)

subsection \<open>Set of Disjoint Sets\<close>

abbreviation disjoint :: "'a set set \ bool" where "disjoint \ pairwise disjnt"

lemma disjoint_def: "disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})"
  unfolding pairwise_def disjnt_def by auto

lemma disjointI:
  "(\a b. a \ A \ b \ A \ a \ b \ a \ b = {}) \ disjoint A"
  unfolding disjoint_def by auto

lemma disjointD:
  "disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}"
  unfolding disjoint_def by auto

lemma disjoint_image: "inj_on f (\A) \ disjoint A \ disjoint ((`) f ` A)"
  unfolding inj_on_def disjoint_def by blast

lemma assumes "disjoint (A \ B)"
      shows   disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
  using assms by (simp_all add: disjoint_def)

lemma disjoint_INT:
  assumes *: "\i. i \ I \ disjoint (F i)"
  shows "disjoint {\i\I. X i | X. \i\I. X i \ F i}"
proof (safe intro!: disjointI del: equalityI)
  fix A B :: "'a \ 'b set" assume "(\i\I. A i) \ (\i\I. B i)"
  then obtain i where "A i \ B i" "i \ I"
    by auto
  moreover assume "\i\I. A i \ F i" "\i\I. B i \ F i"
  ultimately show "(\i\I. A i) \ (\i\I. B i) = {}"
    using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
    by (auto simp flip: INT_Int_distrib)
qed

lemma diff_Union_pairwise_disjoint:
  assumes "pairwise disjnt \" "\ \ \"
  shows "\\ - \\ = \(\ - \)"
proof -
  have "False"
    if x: "x \ A" "x \ B" and AB: "A \ \" "A \ \" "B \ \" for x A B
  proof -
    have "A \ B = {}"
      using assms disjointD AB by blast
  with x show ?thesis
    by blast
  qed
  then show ?thesis by auto
qed

lemma Int_Union_pairwise_disjoint:
  assumes "pairwise disjnt (\ \ \)"
  shows "\\ \ \\ = \(\ \ \)"
proof -
  have "False"
    if x: "x \ A" "x \ B" and AB: "A \ \" "A \ \" "B \ \" for x A B
  proof -
    have "A \ B = {}"
      using assms disjointD AB by blast
  with x show ?thesis
    by blast
  qed
  then show ?thesis by auto
qed

lemma psubset_Union_pairwise_disjoint:
  assumes \<B>: "pairwise disjnt \<B>" and "\<A> \<subset> \<B> - {{}}"
  shows "\\ \ \\"
  unfolding psubset_eq
proof
  show "\\ \ \\"
    using assms by blast
  have "\ \ \" "\(\ - \ \ (\ - {{}})) \ {}"
    using assms by blast+
  then show "\\ \ \\"
    using diff_Union_pairwise_disjoint [OF \<B>] by blast
qed

subsubsection "Family of Disjoint Sets"

definition disjoint_family_on :: "('i \ 'a set) \ 'i set \ bool" where
  "disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})"

abbreviation "disjoint_family A \ disjoint_family_on A UNIV"

lemma disjoint_family_elem_disjnt:
  assumes "infinite A" "finite C"
      and df: "disjoint_family_on B A"
  obtains x where "x \ A" "disjnt C (B x)"
proof -
  have "False" if *: "\x \ A. \y. y \ C \ y \ B x"
  proof -
    obtain g where g: "\x \ A. g x \ C \ g x \ B x"
      using * by metis
    with df have "inj_on g A"
      by (fastforce simp add: inj_on_def disjoint_family_on_def)
    then have "infinite (g ` A)"
      using \<open>infinite A\<close> finite_image_iff by blast
    then show False
      by (meson \<open>finite C\<close> finite_subset g image_subset_iff)
  qed
  then show ?thesis
    by (force simp: disjnt_iff intro: that)
qed

lemma disjoint_family_onD:
  "disjoint_family_on A I \ i \ I \ j \ I \ i \ j \ A i \ A j = {}"
  by (auto simp: disjoint_family_on_def)

lemma disjoint_family_subset: "disjoint_family A \ (\x. B x \ A x) \ disjoint_family B"
  by (force simp add: disjoint_family_on_def)

lemma disjoint_family_on_bisimulation:
  assumes "disjoint_family_on f S"
  and "\n m. n \ S \ m \ S \ n \ m \ f n \ f m = {} \ g n \ g m = {}"
  shows "disjoint_family_on g S"
  using assms unfolding disjoint_family_on_def by auto

lemma disjoint_family_on_mono:
  "A \ B \ disjoint_family_on f B \ disjoint_family_on f A"
  unfolding disjoint_family_on_def by auto

lemma disjoint_family_Suc:
  "(\n. A n \ A (Suc n)) \ disjoint_family (\i. A (Suc i) - A i)"
  using lift_Suc_mono_le[of A]
  by (auto simp add: disjoint_family_on_def)
     (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)

lemma disjoint_family_on_disjoint_image:
  "disjoint_family_on A I \ disjoint (A ` I)"
  unfolding disjoint_family_on_def disjoint_def by force

lemma disjoint_family_on_vimageI: "disjoint_family_on F I \ disjoint_family_on (\i. f -` F i) I"
  by (auto simp: disjoint_family_on_def)

lemma disjoint_image_disjoint_family_on:
  assumes d: "disjoint (A ` I)" and i: "inj_on A I"
  shows "disjoint_family_on A I"
  unfolding disjoint_family_on_def
proof (intro ballI impI)
  fix n m assume nm: "m \ I" "n \ I" and "n \ m"
  with i[THEN inj_onD, of n m] show "A n \ A m = {}"
    by (intro disjointD[OF d]) auto
qed

lemma disjoint_UN:
  assumes F: "\i. i \ I \ disjoint (F i)" and *: "disjoint_family_on (\i. \(F i)) I"
  shows "disjoint (\i\I. F i)"
proof (safe intro!: disjointI del: equalityI)
  fix A B i j assume "A \ B" "A \ F i" "i \ I" "B \ F j" "j \ I"
  show "A \ B = {}"
  proof cases
    assume "i = j" with F[of i] \<open>i \<in> I\<close> \<open>A \<in> F i\<close> \<open>B \<in> F j\<close> \<open>A \<noteq> B\<close> show "A \<inter> B = {}"
      by (auto dest: disjointD)
  next
    assume "i \ j"
    with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>(F i)) \<inter> (\<Union>(F j)) = {}"
      by (rule disjoint_family_onD)
    with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
    show "A \ B = {}"
      by auto
  qed
qed

lemma distinct_list_bind:
  assumes "distinct xs" "\x. x \ set xs \ distinct (f x)"
          "disjoint_family_on (set \ f) (set xs)"
  shows   "distinct (List.bind xs f)"
  using assms
  by (induction xs)
     (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)

lemma bij_betw_UNION_disjoint:
  assumes disj: "disjoint_family_on A' I"
  assumes bij: "\i. i \ I \ bij_betw f (A i) (A' i)"
  shows   "bij_betw f (\i\I. A i) (\i\I. A' i)"
unfolding bij_betw_def
proof
  from bij show eq: "f ` \(A ` I) = \(A' ` I)"
    by (auto simp: bij_betw_def image_UN)
  show "inj_on f (\(A ` I))"
  proof (rule inj_onI, clarify)
    fix i j x y assume A: "i \ I" "j \ I" "x \ A i" "y \ A j" and B: "f x = f y"
    from A bij[of i] bij[of j] have "f x \ A' i" "f y \ A' j"
      by (auto simp: bij_betw_def)
    with B have "A' i \ A' j \ {}" by auto
    with disj A have "i = j" unfolding disjoint_family_on_def by blast
    with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
  qed
qed

lemma disjoint_union: "disjoint C \ disjoint B \ \C \ \B = {} \ disjoint (C \ B)"
  using disjoint_UN[of "{C, B}" "\x. x"] by (auto simp add: disjoint_family_on_def)

text \<open>
  The union of an infinite disjoint family of non-empty sets is infinite.
\<close>
lemma infinite_disjoint_family_imp_infinite_UNION:
  assumes "\finite A" "\x. x \ A \ f x \ {}" "disjoint_family_on f A"
  shows   "\finite (\(f ` A))"
proof -
  define g where "g x = (SOME y. y \ f x)" for x
  have g: "g x \ f x" if "x \ A" for x
    unfolding g_def by (rule someI_ex, insert assms(2) that) blast
  have inj_on_g: "inj_on g A"
  proof (rule inj_onI, rule ccontr)
    fix x y assume A: "x \ A" "y \ A" "g x = g y" "x \ y"
    with g[of x] g[of y] have "g x \ f x" "g x \ f y" by auto
    with A \<open>x \<noteq> y\<close> assms show False
      by (auto simp: disjoint_family_on_def inj_on_def)
  qed
  from g have "g ` A \ \(f ` A)" by blast
  moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
    using finite_imageD by blast
  ultimately show ?thesis using finite_subset by blast
qed


subsection \<open>Construct Disjoint Sequences\<close>

definition disjointed :: "(nat \ 'a set) \ nat \ 'a set" where
  "disjointed A n = A n - (\i\{0..

lemma finite_UN_disjointed_eq: "(\i\{0..i\{0..
proof (induct n)
  case 0 show ?case by simp
next
  case (Suc n)
  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
qed

lemma UN_disjointed_eq: "(\i. disjointed A i) = (\i. A i)"
  by (rule UN_finite2_eq [where k=0])
     (simp add: finite_UN_disjointed_eq)

lemma less_disjoint_disjointed: "m < n \ disjointed A m \ disjointed A n = {}"
  by (auto simp add: disjointed_def)

lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
  by (simp add: disjoint_family_on_def)
     (metis neq_iff Int_commute less_disjoint_disjointed)

lemma disjointed_subset: "disjointed A n \ A n"
  by (auto simp add: disjointed_def)

lemma disjointed_0[simp]: "disjointed A 0 = A 0"
  by (simp add: disjointed_def)

lemma disjointed_mono: "mono A \ disjointed A (Suc n) = A (Suc n) - A n"
  using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)

subsection \<open>Partitions\<close>

text \<open>
  Partitions \<^term>\<open>P\<close> of a set \<^term>\<open>A\<close>. We explicitly disallow empty sets.
\<close>

definition partition_on :: "'a set \ 'a set set \ bool"
where
  "partition_on A P \ \P = A \ disjoint P \ {} \ P"

lemma partition_onI:
  "\P = A \ (\p q. p \ P \ q \ P \ p \ q \ disjnt p q) \ {} \ P \ partition_on A P"
  by (auto simp: partition_on_def pairwise_def)

lemma partition_onD1: "partition_on A P \ A = \P"
  by (auto simp: partition_on_def)

lemma partition_onD2: "partition_on A P \ disjoint P"
  by (auto simp: partition_on_def)

lemma partition_onD3: "partition_on A P \ {} \ P"
  by (auto simp: partition_on_def)

subsection \<open>Constructions of partitions\<close>

lemma partition_on_empty: "partition_on {} P \ P = {}"
  unfolding partition_on_def by fastforce

lemma partition_on_space: "A \ {} \ partition_on A {A}"
  by (auto simp: partition_on_def disjoint_def)

lemma partition_on_singletons: "partition_on A ((\x. {x}) ` A)"
  by (auto simp: partition_on_def disjoint_def)

lemma partition_on_transform:
  assumes P: "partition_on A P"
  assumes F_UN: "\(F ` P) = F (\P)" and F_disjnt: "\p q. p \ P \ q \ P \ disjnt p q \ disjnt (F p) (F q)"
  shows "partition_on (F A) (F ` P - {{}})"
proof -
  have "\(F ` P - {{}}) = F A"
    unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
  with P show ?thesis
    by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
qed

lemma partition_on_restrict: "partition_on A P \ partition_on (B \ A) ((\) B ` P - {{}})"
  by (intro partition_on_transform) (auto simp: disjnt_def)

lemma partition_on_vimage: "partition_on A P \ partition_on (f -` A) ((-`) f ` P - {{}})"
  by (intro partition_on_transform) (auto simp: disjnt_def)

lemma partition_on_inj_image:
  assumes P: "partition_on A P" and f: "inj_on f A"
  shows "partition_on (f ` A) ((`) f ` P - {{}})"
proof (rule partition_on_transform[OF P])
  show "p \ P \ q \ P \ disjnt p q \ disjnt (f ` p) (f ` q)" for p q
    using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
qed auto

subsection \<open>Finiteness of partitions\<close>

lemma finitely_many_partition_on:
  assumes "finite A"
  shows "finite {P. partition_on A P}"
proof (rule finite_subset)
  show "{P. partition_on A P} \ Pow (Pow A)"
    unfolding partition_on_def by auto
  show "finite (Pow (Pow A))"
    using assms by simp
qed

lemma finite_elements: "finite A \ partition_on A P \ finite P"
  using partition_onD1[of A P] by (simp add: finite_UnionD)

subsection \<open>Equivalence of partitions and equivalence classes\<close>

lemma partition_on_quotient:
  assumes r: "equiv A r"
  shows "partition_on A (A // r)"
proof (rule partition_onI)
  from r have "refl_on A r"
    by (auto elim: equivE)
  then show "\(A // r) = A" "{} \ A // r"
    by (auto simp: refl_on_def quotient_def)

  fix p q assume "p \ A // r" "q \ A // r" "p \ q"
  then obtain x y where "x \ A" "y \ A" "p = r `` {x}" "q = r `` {y}"
    by (auto simp: quotient_def)
  with r equiv_class_eq_iff[OF r, of x y] \<open>p \<noteq> q\<close> show "disjnt p q"
    by (auto simp: disjnt_equiv_class)
qed

lemma equiv_partition_on:
  assumes P: "partition_on A P"
  shows "equiv A {(x, y). \p \ P. x \ p \ y \ p}"
proof (rule equivI)
  have "A = \P" "disjoint P" "{} \ P"
    using P by (auto simp: partition_on_def)
  then show "refl_on A {(x, y). \p\P. x \ p \ y \ p}"
    unfolding refl_on_def by auto
  show "trans {(x, y). \p\P. x \ p \ y \ p}"
    using \<open>disjoint P\<close> by (auto simp: trans_def disjoint_def)
qed (auto simp: sym_def)

lemma partition_on_eq_quotient:
  assumes P: "partition_on A P"
  shows "A // {(x, y). \p \ P. x \ p \ y \ p} = P"
  unfolding quotient_def
proof safe
  fix x assume "x \ A"
  then obtain p where "p \ P" "x \ p" "\q. q \ P \ x \ q \ p = q"
    using P by (auto simp: partition_on_def disjoint_def)
  then have "{y. \p\P. x \ p \ y \ p} = p"
    by (safe intro!: bexI[of _ p]) simp
  then show "{(x, y). \p\P. x \ p \ y \ p} `` {x} \ P"
    by (simp add: \<open>p \<in> P\<close>)
next
  fix p assume "p \ P"
  then have "p \ {}"
    using P by (auto simp: partition_on_def)
  then obtain x where "x \ p"
    by auto
  then have "x \ A" "\q. q \ P \ x \ q \ p = q"
    using P \<open>p \<in> P\<close> by (auto simp: partition_on_def disjoint_def)
  with \<open>p\<in>P\<close> \<open>x \<in> p\<close> have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p"
    by (safe intro!: bexI[of _ p]) simp
  then show "p \ (\x\A. {{(x, y). \p\P. x \ p \ y \ p} `` {x}})"
    by (auto intro: \<open>x \<in> A\<close>)
qed

lemma partition_on_alt: "partition_on A P \ (\r. equiv A r \ P = A // r)"
  by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

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.21 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©