src/HOL/Library/Disjoint_Sets.thy
 author paulson Thu Dec 10 13:38:40 2015 +0000 (2015-12-10) changeset 61824 dcbe9f756ae0 parent 60727 53697011b03a child 62390 842917225d56 permissions -rw-r--r--
not_leE -> not_le_imp_less and other tidying
```     1 (*  Title:      HOL/Library/Disjoint_Sets.thy
```
```     2     Author:     Johannes Hölzl, TU München
```
```     3 *)
```
```     4
```
```     5 section \<open>Handling Disjoint Sets\<close>
```
```     6
```
```     7 theory Disjoint_Sets
```
```     8   imports Main
```
```     9 begin
```
```    10
```
```    11 lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
```
```    12   by blast
```
```    13
```
```    14 lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
```
```    15   by blast
```
```    16
```
```    17 lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
```
```    18   by blast
```
```    19
```
```    20 lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
```
```    21   unfolding mono_def by auto
```
```    22
```
```    23 subsection \<open>Set of Disjoint Sets\<close>
```
```    24
```
```    25 definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
```
```    26
```
```    27 lemma disjointI:
```
```    28   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
```
```    29   unfolding disjoint_def by auto
```
```    30
```
```    31 lemma disjointD:
```
```    32   "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
```
```    33   unfolding disjoint_def by auto
```
```    34
```
```    35 lemma disjoint_empty[iff]: "disjoint {}"
```
```    36   by (auto simp: disjoint_def)
```
```    37
```
```    38 lemma disjoint_INT:
```
```    39   assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
```
```    40   shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
```
```    41 proof (safe intro!: disjointI del: equalityI)
```
```    42   fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)"
```
```    43   then obtain i where "A i \<noteq> B i" "i \<in> I"
```
```    44     by auto
```
```    45   moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
```
```    46   ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
```
```    47     using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
```
```    48     by (auto simp: INT_Int_distrib[symmetric])
```
```    49 qed
```
```    50
```
```    51 lemma disjoint_singleton[simp]: "disjoint {A}"
```
```    52   by(simp add: disjoint_def)
```
```    53
```
```    54 subsubsection "Family of Disjoint Sets"
```
```    55
```
```    56 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
```
```    57   "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
```
```    58
```
```    59 abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
```
```    60
```
```    61 lemma disjoint_family_onD:
```
```    62   "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
```
```    63   by (auto simp: disjoint_family_on_def)
```
```    64
```
```    65 lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
```
```    66   by (force simp add: disjoint_family_on_def)
```
```    67
```
```    68 lemma disjoint_family_on_bisimulation:
```
```    69   assumes "disjoint_family_on f S"
```
```    70   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 = {}"
```
```    71   shows "disjoint_family_on g S"
```
```    72   using assms unfolding disjoint_family_on_def by auto
```
```    73
```
```    74 lemma disjoint_family_on_mono:
```
```    75   "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
```
```    76   unfolding disjoint_family_on_def by auto
```
```    77
```
```    78 lemma disjoint_family_Suc:
```
```    79   "(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
```
```    80   using lift_Suc_mono_le[of A]
```
```    81   by (auto simp add: disjoint_family_on_def)
```
```    82      (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
```
```    83
```
```    84 lemma disjoint_family_on_disjoint_image:
```
```    85   "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
```
```    86   unfolding disjoint_family_on_def disjoint_def by force
```
```    87
```
```    88 lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I"
```
```    89   by (auto simp: disjoint_family_on_def)
```
```    90
```
```    91 lemma disjoint_image_disjoint_family_on:
```
```    92   assumes d: "disjoint (A ` I)" and i: "inj_on A I"
```
```    93   shows "disjoint_family_on A I"
```
```    94   unfolding disjoint_family_on_def
```
```    95 proof (intro ballI impI)
```
```    96   fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m"
```
```    97   with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
```
```    98     by (intro disjointD[OF d]) auto
```
```    99 qed
```
```   100
```
```   101 lemma disjoint_UN:
```
```   102   assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
```
```   103   shows "disjoint (\<Union>i\<in>I. F i)"
```
```   104 proof (safe intro!: disjointI del: equalityI)
```
```   105   fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I"
```
```   106   show "A \<inter> B = {}"
```
```   107   proof cases
```
```   108     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 = {}"
```
```   109       by (auto dest: disjointD)
```
```   110   next
```
```   111     assume "i \<noteq> j"
```
```   112     with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}"
```
```   113       by (rule disjoint_family_onD)
```
```   114     with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
```
```   115     show "A \<inter> B = {}"
```
```   116       by auto
```
```   117   qed
```
```   118 qed
```
```   119
```
```   120 lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
```
```   121   using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
```
```   122
```
```   123 subsection \<open>Construct Disjoint Sequences\<close>
```
```   124
```
```   125 definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
```
```   126   "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
```
```   127
```
```   128 lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
```
```   129 proof (induct n)
```
```   130   case 0 show ?case by simp
```
```   131 next
```
```   132   case (Suc n)
```
```   133   thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
```
```   134 qed
```
```   135
```
```   136 lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
```
```   137   by (rule UN_finite2_eq [where k=0])
```
```   138      (simp add: finite_UN_disjointed_eq)
```
```   139
```
```   140 lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
```
```   141   by (auto simp add: disjointed_def)
```
```   142
```
```   143 lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
```
```   144   by (simp add: disjoint_family_on_def)
```
```   145      (metis neq_iff Int_commute less_disjoint_disjointed)
```
```   146
```
```   147 lemma disjointed_subset: "disjointed A n \<subseteq> A n"
```
```   148   by (auto simp add: disjointed_def)
```
```   149
```
```   150 lemma disjointed_0[simp]: "disjointed A 0 = A 0"
```
```   151   by (simp add: disjointed_def)
```
```   152
```
```   153 lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
```
```   154   using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
```
```   155
```
`   156 end`