src/HOL/Library/Disjoint_Sets.thy
changeset 60727 53697011b03a
child 61824 dcbe9f756ae0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Thu Jul 16 10:48:20 2015 +0200
     1.3 @@ -0,0 +1,156 @@
     1.4 +(*  Title:      HOL/Library/Disjoint_Sets.thy
     1.5 +    Author:     Johannes Hölzl, TU München
     1.6 +*)
     1.7 +
     1.8 +section \<open>Handling Disjoint Sets\<close>
     1.9 +
    1.10 +theory Disjoint_Sets
    1.11 +  imports Main
    1.12 +begin
    1.13 +
    1.14 +lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
    1.15 +  by blast
    1.16 +
    1.17 +lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
    1.18 +  by blast
    1.19 +
    1.20 +lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
    1.21 +  by blast
    1.22 +
    1.23 +lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
    1.24 +  unfolding mono_def by auto
    1.25 +
    1.26 +subsection \<open>Set of Disjoint Sets\<close>
    1.27 +
    1.28 +definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
    1.29 +
    1.30 +lemma disjointI:
    1.31 +  "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
    1.32 +  unfolding disjoint_def by auto
    1.33 +
    1.34 +lemma disjointD:
    1.35 +  "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
    1.36 +  unfolding disjoint_def by auto
    1.37 +
    1.38 +lemma disjoint_empty[iff]: "disjoint {}"
    1.39 +  by (auto simp: disjoint_def)
    1.40 +
    1.41 +lemma disjoint_INT:
    1.42 +  assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
    1.43 +  shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
    1.44 +proof (safe intro!: disjointI del: equalityI)
    1.45 +  fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)" 
    1.46 +  then obtain i where "A i \<noteq> B i" "i \<in> I"
    1.47 +    by auto
    1.48 +  moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
    1.49 +  ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
    1.50 +    using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
    1.51 +    by (auto simp: INT_Int_distrib[symmetric])
    1.52 +qed
    1.53 +
    1.54 +lemma disjoint_singleton[simp]: "disjoint {A}"
    1.55 +  by(simp add: disjoint_def)
    1.56 +
    1.57 +subsubsection "Family of Disjoint Sets"
    1.58 +
    1.59 +definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
    1.60 +  "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
    1.61 +
    1.62 +abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
    1.63 +
    1.64 +lemma disjoint_family_onD:
    1.65 +  "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
    1.66 +  by (auto simp: disjoint_family_on_def)
    1.67 +
    1.68 +lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
    1.69 +  by (force simp add: disjoint_family_on_def)
    1.70 +
    1.71 +lemma disjoint_family_on_bisimulation:
    1.72 +  assumes "disjoint_family_on f S"
    1.73 +  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 = {}"
    1.74 +  shows "disjoint_family_on g S"
    1.75 +  using assms unfolding disjoint_family_on_def by auto
    1.76 +
    1.77 +lemma disjoint_family_on_mono:
    1.78 +  "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
    1.79 +  unfolding disjoint_family_on_def by auto
    1.80 +
    1.81 +lemma disjoint_family_Suc:
    1.82 +  "(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
    1.83 +  using lift_Suc_mono_le[of A]
    1.84 +  by (auto simp add: disjoint_family_on_def)
    1.85 +     (metis insert_absorb insert_subset le_SucE le_antisym not_leE less_imp_le)
    1.86 +
    1.87 +lemma disjoint_family_on_disjoint_image:
    1.88 +  "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
    1.89 +  unfolding disjoint_family_on_def disjoint_def by force
    1.90 +
    1.91 +lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I"
    1.92 +  by (auto simp: disjoint_family_on_def)
    1.93 +
    1.94 +lemma disjoint_image_disjoint_family_on:
    1.95 +  assumes d: "disjoint (A ` I)" and i: "inj_on A I"
    1.96 +  shows "disjoint_family_on A I"
    1.97 +  unfolding disjoint_family_on_def
    1.98 +proof (intro ballI impI)
    1.99 +  fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m"
   1.100 +  with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
   1.101 +    by (intro disjointD[OF d]) auto
   1.102 +qed
   1.103 +
   1.104 +lemma disjoint_UN:
   1.105 +  assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
   1.106 +  shows "disjoint (\<Union>i\<in>I. F i)"
   1.107 +proof (safe intro!: disjointI del: equalityI)
   1.108 +  fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I"
   1.109 +  show "A \<inter> B = {}"
   1.110 +  proof cases
   1.111 +    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 = {}"
   1.112 +      by (auto dest: disjointD)
   1.113 +  next
   1.114 +    assume "i \<noteq> j"
   1.115 +    with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}"
   1.116 +      by (rule disjoint_family_onD)
   1.117 +    with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
   1.118 +    show "A \<inter> B = {}"
   1.119 +      by auto
   1.120 +  qed
   1.121 +qed
   1.122 +
   1.123 +lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
   1.124 +  using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
   1.125 +
   1.126 +subsection \<open>Construct Disjoint Sequences\<close>
   1.127 +
   1.128 +definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
   1.129 +  "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
   1.130 +
   1.131 +lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
   1.132 +proof (induct n)
   1.133 +  case 0 show ?case by simp
   1.134 +next
   1.135 +  case (Suc n)
   1.136 +  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
   1.137 +qed
   1.138 +
   1.139 +lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
   1.140 +  by (rule UN_finite2_eq [where k=0])
   1.141 +     (simp add: finite_UN_disjointed_eq)
   1.142 +
   1.143 +lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
   1.144 +  by (auto simp add: disjointed_def)
   1.145 +
   1.146 +lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
   1.147 +  by (simp add: disjoint_family_on_def)
   1.148 +     (metis neq_iff Int_commute less_disjoint_disjointed)
   1.149 +
   1.150 +lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   1.151 +  by (auto simp add: disjointed_def)
   1.152 +
   1.153 +lemma disjointed_0[simp]: "disjointed A 0 = A 0"
   1.154 +  by (simp add: disjointed_def)
   1.155 +
   1.156 +lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
   1.157 +  using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
   1.158 +
   1.159 +end
   1.160 \ No newline at end of file