# HG changeset patch
# User hoelzl
# Date 1437036500 -7200
# Node ID 53697011b03af96595ce90c13d2b42433ba03d70
# Parent  6d500a224cbe941068bfb92e501dd5ee4f709689
move disjoint sets to their own theory

diff -r 6d500a224cbe -r 53697011b03a src/HOL/Library/Disjoint_Sets.thy
--- /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
diff -r 6d500a224cbe -r 53697011b03a src/HOL/Library/Library.thy
--- 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
diff -r 6d500a224cbe -r 53697011b03a src/HOL/Probability/Binary_Product_Measure.thy
--- 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)
diff -r 6d500a224cbe -r 53697011b03a src/HOL/Probability/Measure_Space.thy
--- 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
 
diff -r 6d500a224cbe -r 53697011b03a src/HOL/Probability/Sigma_Algebra.thy
--- 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)