src/HOL/Library/Disjoint_Sets.thy

 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 = {})"
+abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt"
+
+lemma disjoint_def: "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
+  unfolding pairwise_def disjnt_def by auto
 
 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)

   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 = {})"