--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Disjoint_Sets.thy Thu Jul 16 10:48:20 2015 +0200
@@ -0,0 +1,156 @@
+(* Title: HOL/Library/Disjoint_Sets.thy
+ Author: Johannes Hölzl, TU München
+*)
+
+section \<open>Handling Disjoint Sets\<close>
+
+theory Disjoint_Sets
+ imports Main
+begin
+
+lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
+ by blast
+
+lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
+ by blast
+
+lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
+ by blast
+
+lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
+ unfolding mono_def by auto
+
+subsection \<open>Set of Disjoint Sets\<close>
+
+definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
+
+lemma disjointI:
+ "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
+ unfolding disjoint_def by auto
+
+lemma disjointD:
+ "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
+ unfolding disjoint_def by auto
+
+lemma disjoint_empty[iff]: "disjoint {}"
+ by (auto simp: disjoint_def)
+
+lemma disjoint_INT:
+ assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
+ shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
+proof (safe intro!: disjointI del: equalityI)
+ fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)"
+ then obtain i where "A i \<noteq> B i" "i \<in> I"
+ by auto
+ moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
+ ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
+ using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
+ by (auto simp: INT_Int_distrib[symmetric])
+qed
+
+lemma disjoint_singleton[simp]: "disjoint {A}"
+ by(simp add: disjoint_def)
+
+subsubsection "Family of Disjoint Sets"
+
+definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
+ "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
+
+abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
+
+lemma disjoint_family_onD:
+ "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
+ by (auto simp: disjoint_family_on_def)
+
+lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
+ by (force simp add: disjoint_family_on_def)
+
+lemma disjoint_family_on_bisimulation:
+ assumes "disjoint_family_on f S"
+ and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}"
+ shows "disjoint_family_on g S"
+ using assms unfolding disjoint_family_on_def by auto
+
+lemma disjoint_family_on_mono:
+ "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
+ unfolding disjoint_family_on_def by auto
+
+lemma disjoint_family_Suc:
+ "(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>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_leE less_imp_le)
+
+lemma disjoint_family_on_disjoint_image:
+ "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
+ unfolding disjoint_family_on_def disjoint_def by force
+
+lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>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 \<in> I" "n \<in> I" and "n \<noteq> m"
+ with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
+ by (intro disjointD[OF d]) auto
+qed
+
+lemma disjoint_UN:
+ assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
+ shows "disjoint (\<Union>i\<in>I. F i)"
+proof (safe intro!: disjointI del: equalityI)
+ fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I"
+ show "A \<inter> 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 \<noteq> 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 \<inter> B = {}"
+ by auto
+ qed
+qed
+
+lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
+ using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
+
+subsection \<open>Construct Disjoint Sequences\<close>
+
+definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
+ "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
+
+lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
+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: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
+ by (rule UN_finite2_eq [where k=0])
+ (simp add: finite_UN_disjointed_eq)
+
+lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> 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 \<subseteq> 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 \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
+ using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Library.thy Wed Jul 15 11:25:51 2015 +0200
+++ b/src/HOL/Library/Library.thy Thu Jul 16 10:48:20 2015 +0200
@@ -14,6 +14,7 @@
Countable_Set_Type
Debug
Diagonal_Subsequence
+ Disjoint_Sets
Dlist
Extended
Extended_Nat
--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Jul 15 11:25:51 2015 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Thu Jul 16 10:48:20 2015 +0200
@@ -201,9 +201,6 @@
unfolding Int_stable_def
by safe (auto simp add: times_Int_times)
-lemma disjoint_family_vimageI: "disjoint_family F \<Longrightarrow> disjoint_family (\<lambda>i. f -` F i)"
- by (auto simp: disjoint_family_on_def)
-
lemma (in finite_measure) finite_measure_cut_measurable:
assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^sub>M M)"
shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
@@ -221,7 +218,7 @@
next
case (union F)
then have "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
- by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
+ by (simp add: suminf_emeasure disjoint_family_on_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
with union show ?case
unfolding sets_pair_measure[symmetric] by simp
qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
--- a/src/HOL/Probability/Measure_Space.thy Wed Jul 15 11:25:51 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Thu Jul 16 10:48:20 2015 +0200
@@ -41,6 +41,19 @@
show ?thesis using * by simp
qed simp
+lemma setsum_indicator_disjoint_family:
+ fixes f :: "'d \<Rightarrow> 'e::semiring_1"
+ assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
+ shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
+proof -
+ have "P \<inter> {i. x \<in> A i} = {j}"
+ using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
+ by auto
+ thus ?thesis
+ unfolding indicator_def
+ by (simp add: if_distrib setsum.If_cases[OF `finite P`])
+qed
+
text {*
The type for emeasure spaces is already defined in @{theory Sigma_Algebra}, as it is also used to
represent sigma algebras (with an arbitrary emeasure).
@@ -119,9 +132,9 @@
then have "(\<Sum>i\<le>Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))"
by simp
also have "\<dots> = f (A n \<union> disjointed A (Suc n))"
- using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_incseq)
+ using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_mono)
also have "A n \<union> disjointed A (Suc n) = A (Suc n)"
- using `incseq A` by (auto dest: incseq_SucD simp: disjointed_incseq)
+ using `incseq A` by (auto dest: incseq_SucD simp: disjointed_mono)
finally show ?case .
qed simp
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Jul 15 11:25:51 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu Jul 16 10:48:20 2015 +0200
@@ -14,6 +14,7 @@
"~~/src/HOL/Library/FuncSet"
"~~/src/HOL/Library/Indicator_Function"
"~~/src/HOL/Library/Extended_Real"
+ "~~/src/HOL/Library/Disjoint_Sets"
begin
text {* Sigma algebras are an elementary concept in measure
@@ -35,46 +36,6 @@
subsubsection {* Semiring of sets *}
-definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
-
-lemma disjointI:
- "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
- unfolding disjoint_def by auto
-
-lemma disjointD:
- "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
- unfolding disjoint_def by auto
-
-lemma disjoint_empty[iff]: "disjoint {}"
- by (auto simp: disjoint_def)
-
-lemma disjoint_union:
- assumes C: "disjoint C" and B: "disjoint B" and disj: "\<Union>C \<inter> \<Union>B = {}"
- shows "disjoint (C \<union> B)"
-proof (rule disjointI)
- fix c d assume sets: "c \<in> C \<union> B" "d \<in> C \<union> B" and "c \<noteq> d"
- show "c \<inter> d = {}"
- proof cases
- assume "(c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B)"
- then show ?thesis
- proof
- assume "c \<in> C \<and> d \<in> C" with `c \<noteq> d` C show "c \<inter> d = {}"
- by (auto simp: disjoint_def)
- next
- assume "c \<in> B \<and> d \<in> B" with `c \<noteq> d` B show "c \<inter> d = {}"
- by (auto simp: disjoint_def)
- qed
- next
- assume "\<not> ((c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B))"
- with sets have "(c \<subseteq> \<Union>C \<and> d \<subseteq> \<Union>B) \<or> (c \<subseteq> \<Union>B \<and> d \<subseteq> \<Union>C)"
- by auto
- with disj show "c \<inter> d = {}" by auto
- qed
-qed
-
-lemma disjoint_singleton [simp]: "disjoint {A}"
-by(simp add: disjoint_def)
-
locale semiring_of_sets = subset_class +
assumes empty_sets[iff]: "{} \<in> M"
assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
@@ -787,101 +748,6 @@
qed
qed
-subsubsection "Disjoint families"
-
-definition
- disjoint_family_on where
- "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
-
-abbreviation
- "disjoint_family A \<equiv> disjoint_family_on A UNIV"
-
-lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
- by blast
-
-lemma disjoint_family_onD: "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
- by (auto simp: disjoint_family_on_def)
-
-lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
- by blast
-
-lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
- by blast
-
-lemma disjoint_family_subset:
- "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
- by (force simp add: disjoint_family_on_def)
-
-lemma disjoint_family_on_bisimulation:
- assumes "disjoint_family_on f S"
- and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}"
- shows "disjoint_family_on g S"
- using assms unfolding disjoint_family_on_def by auto
-
-lemma disjoint_family_on_mono:
- "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
- unfolding disjoint_family_on_def by auto
-
-lemma disjoint_family_Suc:
- assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
- shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
-proof -
- {
- fix m
- have "!!n. A n \<subseteq> A (m+n)"
- proof (induct m)
- case 0 show ?case by simp
- next
- case (Suc m) thus ?case
- by (metis Suc_eq_plus1 assms add.commute add.left_commute subset_trans)
- qed
- }
- hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
- by (metis add.commute le_add_diff_inverse nat_less_le)
- thus ?thesis
- by (auto simp add: disjoint_family_on_def)
- (metis insert_absorb insert_subset le_SucE le_antisym not_leE)
-qed
-
-lemma setsum_indicator_disjoint_family:
- fixes f :: "'d \<Rightarrow> 'e::semiring_1"
- assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
- shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
-proof -
- have "P \<inter> {i. x \<in> A i} = {j}"
- using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
- by auto
- thus ?thesis
- unfolding indicator_def
- by (simp add: if_distrib setsum.If_cases[OF `finite P`])
-qed
-
-definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
- where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
-
-lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
-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: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
- apply (rule UN_finite2_eq [where k=0])
- apply (simp add: finite_UN_disjointed_eq)
- done
-
-lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> 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 \<subseteq> A n"
- by (auto simp add: disjointed_def)
-
lemma (in ring_of_sets) UNION_in_sets:
fixes A:: "nat \<Rightarrow> 'a set"
assumes A: "range A \<subseteq> M"
@@ -907,18 +773,6 @@
"range A \<subseteq> M \<Longrightarrow> range (disjointed A) \<subseteq> M"
using range_disjointed_sets .
-lemma disjointed_0[simp]: "disjointed A 0 = A 0"
- by (simp add: disjointed_def)
-
-lemma incseq_Un:
- "incseq A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
- unfolding incseq_def by auto
-
-lemma disjointed_incseq:
- "incseq A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
- using incseq_Un[of A]
- by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
-
lemma sigma_algebra_disjoint_iff:
"sigma_algebra \<Omega> M \<longleftrightarrow> algebra \<Omega> M \<and>
(\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
@@ -935,20 +789,6 @@
thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
qed
-lemma disjoint_family_on_disjoint_image:
- "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
- unfolding disjoint_family_on_def disjoint_def by force
-
-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 \<in> I" "n \<in> I" and "n \<noteq> m"
- with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
- by (intro disjointD[OF d]) auto
-qed
-
subsubsection {* Ring generated by a semiring *}
definition (in semiring_of_sets)