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