hoelzl@60727: (* Title: HOL/Library/Disjoint_Sets.thy hoelzl@60727: Author: Johannes Hölzl, TU München hoelzl@60727: *) hoelzl@60727: hoelzl@60727: section \Handling Disjoint Sets\ hoelzl@60727: hoelzl@60727: theory Disjoint_Sets hoelzl@60727: imports Main hoelzl@60727: begin hoelzl@60727: hoelzl@60727: lemma range_subsetD: "range f \ B \ f i \ B" hoelzl@60727: by blast hoelzl@60727: hoelzl@60727: lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}" hoelzl@60727: by blast hoelzl@60727: hoelzl@60727: lemma Int_Diff_Un: "A \ B \ (A - B) = A" hoelzl@60727: by blast hoelzl@60727: hoelzl@60727: lemma mono_Un: "mono A \ (\i\n. A i) = A n" hoelzl@60727: unfolding mono_def by auto hoelzl@60727: hoelzl@60727: subsection \Set of Disjoint Sets\ hoelzl@60727: hoelzl@60727: definition "disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})" hoelzl@60727: hoelzl@60727: lemma disjointI: hoelzl@60727: "(\a b. a \ A \ b \ A \ a \ b \ a \ b = {}) \ disjoint A" hoelzl@60727: unfolding disjoint_def by auto hoelzl@60727: hoelzl@60727: lemma disjointD: hoelzl@60727: "disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}" hoelzl@60727: unfolding disjoint_def by auto hoelzl@60727: hoelzl@60727: lemma disjoint_empty[iff]: "disjoint {}" hoelzl@60727: by (auto simp: disjoint_def) hoelzl@60727: hoelzl@60727: lemma disjoint_INT: hoelzl@60727: assumes *: "\i. i \ I \ disjoint (F i)" hoelzl@60727: shows "disjoint {\i\I. X i | X. \i\I. X i \ F i}" hoelzl@60727: proof (safe intro!: disjointI del: equalityI) hoelzl@60727: fix A B :: "'a \ 'b set" assume "(\i\I. A i) \ (\i\I. B i)" hoelzl@60727: then obtain i where "A i \ B i" "i \ I" hoelzl@60727: by auto hoelzl@60727: moreover assume "\i\I. A i \ F i" "\i\I. B i \ F i" hoelzl@60727: ultimately show "(\i\I. A i) \ (\i\I. B i) = {}" hoelzl@60727: using *[OF \i\I\, THEN disjointD, of "A i" "B i"] hoelzl@60727: by (auto simp: INT_Int_distrib[symmetric]) hoelzl@60727: qed hoelzl@60727: hoelzl@60727: lemma disjoint_singleton[simp]: "disjoint {A}" hoelzl@60727: by(simp add: disjoint_def) hoelzl@60727: hoelzl@60727: subsubsection "Family of Disjoint Sets" hoelzl@60727: hoelzl@60727: definition disjoint_family_on :: "('i \ 'a set) \ 'i set \ bool" where hoelzl@60727: "disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})" hoelzl@60727: hoelzl@60727: abbreviation "disjoint_family A \ disjoint_family_on A UNIV" hoelzl@60727: hoelzl@60727: lemma disjoint_family_onD: hoelzl@60727: "disjoint_family_on A I \ i \ I \ j \ I \ i \ j \ A i \ A j = {}" hoelzl@60727: by (auto simp: disjoint_family_on_def) hoelzl@60727: hoelzl@60727: lemma disjoint_family_subset: "disjoint_family A \ (\x. B x \ A x) \ disjoint_family B" hoelzl@60727: by (force simp add: disjoint_family_on_def) hoelzl@60727: hoelzl@60727: lemma disjoint_family_on_bisimulation: hoelzl@60727: assumes "disjoint_family_on f S" hoelzl@60727: and "\n m. n \ S \ m \ S \ n \ m \ f n \ f m = {} \ g n \ g m = {}" hoelzl@60727: shows "disjoint_family_on g S" hoelzl@60727: using assms unfolding disjoint_family_on_def by auto hoelzl@60727: hoelzl@60727: lemma disjoint_family_on_mono: hoelzl@60727: "A \ B \ disjoint_family_on f B \ disjoint_family_on f A" hoelzl@60727: unfolding disjoint_family_on_def by auto hoelzl@60727: hoelzl@60727: lemma disjoint_family_Suc: hoelzl@60727: "(\n. A n \ A (Suc n)) \ disjoint_family (\i. A (Suc i) - A i)" hoelzl@60727: using lift_Suc_mono_le[of A] hoelzl@60727: by (auto simp add: disjoint_family_on_def) lp15@61824: (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le) hoelzl@60727: hoelzl@60727: lemma disjoint_family_on_disjoint_image: hoelzl@60727: "disjoint_family_on A I \ disjoint (A ` I)" hoelzl@60727: unfolding disjoint_family_on_def disjoint_def by force hoelzl@60727: hoelzl@60727: lemma disjoint_family_on_vimageI: "disjoint_family_on F I \ disjoint_family_on (\i. f -` F i) I" hoelzl@60727: by (auto simp: disjoint_family_on_def) hoelzl@60727: hoelzl@60727: lemma disjoint_image_disjoint_family_on: hoelzl@60727: assumes d: "disjoint (A ` I)" and i: "inj_on A I" hoelzl@60727: shows "disjoint_family_on A I" hoelzl@60727: unfolding disjoint_family_on_def hoelzl@60727: proof (intro ballI impI) hoelzl@60727: fix n m assume nm: "m \ I" "n \ I" and "n \ m" hoelzl@60727: with i[THEN inj_onD, of n m] show "A n \ A m = {}" hoelzl@60727: by (intro disjointD[OF d]) auto hoelzl@60727: qed hoelzl@60727: hoelzl@60727: lemma disjoint_UN: hoelzl@60727: assumes F: "\i. i \ I \ disjoint (F i)" and *: "disjoint_family_on (\i. \F i) I" hoelzl@60727: shows "disjoint (\i\I. F i)" hoelzl@60727: proof (safe intro!: disjointI del: equalityI) hoelzl@60727: fix A B i j assume "A \ B" "A \ F i" "i \ I" "B \ F j" "j \ I" hoelzl@60727: show "A \ B = {}" hoelzl@60727: proof cases hoelzl@60727: assume "i = j" with F[of i] \i \ I\ \A \ F i\ \B \ F j\ \A \ B\ show "A \ B = {}" hoelzl@60727: by (auto dest: disjointD) hoelzl@60727: next hoelzl@60727: assume "i \ j" hoelzl@60727: with * \i\I\ \j\I\ have "(\F i) \ (\F j) = {}" hoelzl@60727: by (rule disjoint_family_onD) hoelzl@60727: with \A\F i\ \i\I\ \B\F j\ \j\I\ hoelzl@60727: show "A \ B = {}" hoelzl@60727: by auto hoelzl@60727: qed hoelzl@60727: qed hoelzl@60727: hoelzl@60727: lemma disjoint_union: "disjoint C \ disjoint B \ \C \ \B = {} \ disjoint (C \ B)" hoelzl@60727: using disjoint_UN[of "{C, B}" "\x. x"] by (auto simp add: disjoint_family_on_def) hoelzl@60727: hoelzl@60727: subsection \Construct Disjoint Sequences\ hoelzl@60727: hoelzl@60727: definition disjointed :: "(nat \ 'a set) \ nat \ 'a set" where hoelzl@60727: "disjointed A n = A n - (\i\{0..i\{0..i\{0..i. disjointed A i) = (\i. A i)" hoelzl@60727: by (rule UN_finite2_eq [where k=0]) hoelzl@60727: (simp add: finite_UN_disjointed_eq) hoelzl@60727: hoelzl@60727: lemma less_disjoint_disjointed: "m < n \ disjointed A m \ disjointed A n = {}" hoelzl@60727: by (auto simp add: disjointed_def) hoelzl@60727: hoelzl@60727: lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" hoelzl@60727: by (simp add: disjoint_family_on_def) hoelzl@60727: (metis neq_iff Int_commute less_disjoint_disjointed) hoelzl@60727: hoelzl@60727: lemma disjointed_subset: "disjointed A n \ A n" hoelzl@60727: by (auto simp add: disjointed_def) hoelzl@60727: hoelzl@60727: lemma disjointed_0[simp]: "disjointed A 0 = A 0" hoelzl@60727: by (simp add: disjointed_def) hoelzl@60727: hoelzl@60727: lemma disjointed_mono: "mono A \ disjointed A (Suc n) = A (Suc n) - A n" hoelzl@60727: using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) hoelzl@60727: hoelzl@60727: end