src/HOL/Library/Disjoint_Sets.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63928 d81fb5b46a5c
child 67399 eab6ce8368fa
permissions -rw-r--r--
executable domain membership checks
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@63098
     5
section \<open>Partitions and 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@63098
    23
lemma disjnt_equiv_class: "equiv A r \<Longrightarrow> disjnt (r``{a}) (r``{b}) \<longleftrightarrow> (a, b) \<notin> r"
hoelzl@63098
    24
  by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)
hoelzl@63098
    25
hoelzl@60727
    26
subsection \<open>Set of Disjoint Sets\<close>
hoelzl@60727
    27
lp15@62843
    28
abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt"
lp15@62843
    29
lp15@62843
    30
lemma disjoint_def: "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
lp15@62843
    31
  unfolding pairwise_def disjnt_def by auto
hoelzl@60727
    32
hoelzl@60727
    33
lemma disjointI:
hoelzl@60727
    34
  "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
hoelzl@60727
    35
  unfolding disjoint_def by auto
hoelzl@60727
    36
hoelzl@60727
    37
lemma disjointD:
hoelzl@60727
    38
  "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
hoelzl@60727
    39
  unfolding disjoint_def by auto
hoelzl@60727
    40
eberlm@63099
    41
lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint (op ` f ` A)"
eberlm@63099
    42
  unfolding inj_on_def disjoint_def by blast
eberlm@63099
    43
eberlm@63099
    44
lemma assumes "disjoint (A \<union> B)"
eberlm@63099
    45
      shows   disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
eberlm@63099
    46
  using assms by (simp_all add: disjoint_def)
eberlm@63099
    47
  
hoelzl@60727
    48
lemma disjoint_INT:
hoelzl@60727
    49
  assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
hoelzl@60727
    50
  shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
hoelzl@60727
    51
proof (safe intro!: disjointI del: equalityI)
hoelzl@63098
    52
  fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)"
hoelzl@60727
    53
  then obtain i where "A i \<noteq> B i" "i \<in> I"
hoelzl@60727
    54
    by auto
hoelzl@60727
    55
  moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
hoelzl@60727
    56
  ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
hoelzl@60727
    57
    using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
hoelzl@60727
    58
    by (auto simp: INT_Int_distrib[symmetric])
hoelzl@60727
    59
qed
hoelzl@60727
    60
hoelzl@60727
    61
subsubsection "Family of Disjoint Sets"
hoelzl@60727
    62
hoelzl@60727
    63
definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
hoelzl@60727
    64
  "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
    65
hoelzl@60727
    66
abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
hoelzl@60727
    67
lp15@63928
    68
lemma disjoint_family_elem_disjnt:
lp15@63928
    69
  assumes "infinite A" "finite C"
lp15@63928
    70
      and df: "disjoint_family_on B A"
lp15@63928
    71
  obtains x where "x \<in> A" "disjnt C (B x)"
lp15@63928
    72
proof -
lp15@63928
    73
  have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x"
lp15@63928
    74
  proof -
lp15@63928
    75
    obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x"
lp15@63928
    76
      using * by metis
lp15@63928
    77
    with df have "inj_on g A"
lp15@63928
    78
      by (fastforce simp add: inj_on_def disjoint_family_on_def)
lp15@63928
    79
    then have "infinite (g ` A)"
lp15@63928
    80
      using \<open>infinite A\<close> finite_image_iff by blast
lp15@63928
    81
    then show False
lp15@63928
    82
      by (meson \<open>finite C\<close> finite_subset g image_subset_iff)
lp15@63928
    83
  qed
lp15@63928
    84
  then show ?thesis
lp15@63928
    85
    by (force simp: disjnt_iff intro: that)
lp15@63928
    86
qed
lp15@63928
    87
hoelzl@60727
    88
lemma disjoint_family_onD:
hoelzl@60727
    89
  "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
    90
  by (auto simp: disjoint_family_on_def)
hoelzl@60727
    91
hoelzl@60727
    92
lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
hoelzl@60727
    93
  by (force simp add: disjoint_family_on_def)
hoelzl@60727
    94
hoelzl@60727
    95
lemma disjoint_family_on_bisimulation:
hoelzl@60727
    96
  assumes "disjoint_family_on f S"
hoelzl@60727
    97
  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
    98
  shows "disjoint_family_on g S"
hoelzl@60727
    99
  using assms unfolding disjoint_family_on_def by auto
hoelzl@60727
   100
hoelzl@60727
   101
lemma disjoint_family_on_mono:
hoelzl@60727
   102
  "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
hoelzl@60727
   103
  unfolding disjoint_family_on_def by auto
hoelzl@60727
   104
hoelzl@60727
   105
lemma disjoint_family_Suc:
hoelzl@60727
   106
  "(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
hoelzl@60727
   107
  using lift_Suc_mono_le[of A]
hoelzl@60727
   108
  by (auto simp add: disjoint_family_on_def)
lp15@61824
   109
     (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
hoelzl@60727
   110
hoelzl@60727
   111
lemma disjoint_family_on_disjoint_image:
hoelzl@60727
   112
  "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
hoelzl@60727
   113
  unfolding disjoint_family_on_def disjoint_def by force
eberlm@63099
   114
 
hoelzl@60727
   115
lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I"
hoelzl@60727
   116
  by (auto simp: disjoint_family_on_def)
hoelzl@60727
   117
hoelzl@60727
   118
lemma disjoint_image_disjoint_family_on:
hoelzl@60727
   119
  assumes d: "disjoint (A ` I)" and i: "inj_on A I"
hoelzl@60727
   120
  shows "disjoint_family_on A I"
hoelzl@60727
   121
  unfolding disjoint_family_on_def
hoelzl@60727
   122
proof (intro ballI impI)
hoelzl@60727
   123
  fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m"
hoelzl@60727
   124
  with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
hoelzl@60727
   125
    by (intro disjointD[OF d]) auto
hoelzl@60727
   126
qed
hoelzl@60727
   127
hoelzl@60727
   128
lemma disjoint_UN:
hoelzl@60727
   129
  assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
hoelzl@60727
   130
  shows "disjoint (\<Union>i\<in>I. F i)"
hoelzl@60727
   131
proof (safe intro!: disjointI del: equalityI)
hoelzl@60727
   132
  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
   133
  show "A \<inter> B = {}"
hoelzl@60727
   134
  proof cases
hoelzl@60727
   135
    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
   136
      by (auto dest: disjointD)
hoelzl@60727
   137
  next
hoelzl@60727
   138
    assume "i \<noteq> j"
hoelzl@60727
   139
    with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}"
hoelzl@60727
   140
      by (rule disjoint_family_onD)
hoelzl@60727
   141
    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
   142
    show "A \<inter> B = {}"
hoelzl@60727
   143
      by auto
hoelzl@60727
   144
  qed
hoelzl@60727
   145
qed
hoelzl@60727
   146
eberlm@63099
   147
lemma distinct_list_bind: 
eberlm@63099
   148
  assumes "distinct xs" "\<And>x. x \<in> set xs \<Longrightarrow> distinct (f x)" 
eberlm@63099
   149
          "disjoint_family_on (set \<circ> f) (set xs)"
eberlm@63099
   150
  shows   "distinct (List.bind xs f)"
eberlm@63099
   151
  using assms
eberlm@63099
   152
  by (induction xs)
eberlm@63099
   153
     (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)
eberlm@63099
   154
eberlm@63099
   155
lemma bij_betw_UNION_disjoint:
eberlm@63099
   156
  assumes disj: "disjoint_family_on A' I"
eberlm@63099
   157
  assumes bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
eberlm@63099
   158
  shows   "bij_betw f (\<Union>i\<in>I. A i) (\<Union>i\<in>I. A' i)"
eberlm@63099
   159
unfolding bij_betw_def
eberlm@63099
   160
proof
eberlm@63099
   161
  from bij show eq: "f ` UNION I A = UNION I A'"
eberlm@63099
   162
    by (auto simp: bij_betw_def image_UN)
eberlm@63099
   163
  show "inj_on f (UNION I A)"
eberlm@63099
   164
  proof (rule inj_onI, clarify)
eberlm@63099
   165
    fix i j x y assume A: "i \<in> I" "j \<in> I" "x \<in> A i" "y \<in> A j" and B: "f x = f y"
eberlm@63099
   166
    from A bij[of i] bij[of j] have "f x \<in> A' i" "f y \<in> A' j"
eberlm@63099
   167
      by (auto simp: bij_betw_def)
eberlm@63099
   168
    with B have "A' i \<inter> A' j \<noteq> {}" by auto
eberlm@63099
   169
    with disj A have "i = j" unfolding disjoint_family_on_def by blast
eberlm@63099
   170
    with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
eberlm@63099
   171
  qed
eberlm@63099
   172
qed
eberlm@63099
   173
hoelzl@60727
   174
lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
hoelzl@60727
   175
  using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
hoelzl@60727
   176
eberlm@63099
   177
text \<open>
eberlm@63099
   178
  The union of an infinite disjoint family of non-empty sets is infinite.
eberlm@63099
   179
\<close>
eberlm@63099
   180
lemma infinite_disjoint_family_imp_infinite_UNION:
eberlm@63099
   181
  assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A"
eberlm@63099
   182
  shows   "\<not>finite (UNION A f)"
eberlm@63099
   183
proof -
wenzelm@63148
   184
  define g where "g x = (SOME y. y \<in> f x)" for x
eberlm@63099
   185
  have g: "g x \<in> f x" if "x \<in> A" for x
eberlm@63099
   186
    unfolding g_def by (rule someI_ex, insert assms(2) that) blast
eberlm@63099
   187
  have inj_on_g: "inj_on g A"
eberlm@63099
   188
  proof (rule inj_onI, rule ccontr)
eberlm@63099
   189
    fix x y assume A: "x \<in> A" "y \<in> A" "g x = g y" "x \<noteq> y"
eberlm@63099
   190
    with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto
wenzelm@63145
   191
    with A \<open>x \<noteq> y\<close> assms show False
eberlm@63099
   192
      by (auto simp: disjoint_family_on_def inj_on_def)
eberlm@63099
   193
  qed
eberlm@63099
   194
  from g have "g ` A \<subseteq> UNION A f" by blast
eberlm@63099
   195
  moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
eberlm@63099
   196
    using finite_imageD by blast
eberlm@63099
   197
  ultimately show ?thesis using finite_subset by blast
eberlm@63099
   198
qed  
eberlm@63099
   199
  
eberlm@63099
   200
hoelzl@60727
   201
subsection \<open>Construct Disjoint Sequences\<close>
hoelzl@60727
   202
hoelzl@60727
   203
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
hoelzl@60727
   204
  "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
hoelzl@60727
   205
hoelzl@60727
   206
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
hoelzl@60727
   207
proof (induct n)
hoelzl@60727
   208
  case 0 show ?case by simp
hoelzl@60727
   209
next
hoelzl@60727
   210
  case (Suc n)
hoelzl@60727
   211
  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
hoelzl@60727
   212
qed
hoelzl@60727
   213
hoelzl@60727
   214
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
hoelzl@60727
   215
  by (rule UN_finite2_eq [where k=0])
hoelzl@60727
   216
     (simp add: finite_UN_disjointed_eq)
hoelzl@60727
   217
hoelzl@60727
   218
lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
hoelzl@60727
   219
  by (auto simp add: disjointed_def)
hoelzl@60727
   220
hoelzl@60727
   221
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
hoelzl@60727
   222
  by (simp add: disjoint_family_on_def)
hoelzl@60727
   223
     (metis neq_iff Int_commute less_disjoint_disjointed)
hoelzl@60727
   224
hoelzl@60727
   225
lemma disjointed_subset: "disjointed A n \<subseteq> A n"
hoelzl@60727
   226
  by (auto simp add: disjointed_def)
hoelzl@60727
   227
hoelzl@60727
   228
lemma disjointed_0[simp]: "disjointed A 0 = A 0"
hoelzl@60727
   229
  by (simp add: disjointed_def)
hoelzl@60727
   230
hoelzl@60727
   231
lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
hoelzl@60727
   232
  using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
hoelzl@60727
   233
hoelzl@63098
   234
subsection \<open>Partitions\<close>
hoelzl@63098
   235
hoelzl@63098
   236
text \<open>
hoelzl@63098
   237
  Partitions @{term P} of a set @{term A}. We explicitly disallow empty sets.
hoelzl@63098
   238
\<close>
hoelzl@63098
   239
hoelzl@63098
   240
definition partition_on :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool"
hoelzl@63098
   241
where
hoelzl@63098
   242
  "partition_on A P \<longleftrightarrow> \<Union>P = A \<and> disjoint P \<and> {} \<notin> P"
hoelzl@63098
   243
hoelzl@63098
   244
lemma partition_onI:
hoelzl@63098
   245
  "\<Union>P = A \<Longrightarrow> (\<And>p q. p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> p \<noteq> q \<Longrightarrow> disjnt p q) \<Longrightarrow> {} \<notin> P \<Longrightarrow> partition_on A P"
hoelzl@63098
   246
  by (auto simp: partition_on_def pairwise_def)
hoelzl@63098
   247
hoelzl@63098
   248
lemma partition_onD1: "partition_on A P \<Longrightarrow> A = \<Union>P"
hoelzl@63098
   249
  by (auto simp: partition_on_def)
hoelzl@63098
   250
hoelzl@63098
   251
lemma partition_onD2: "partition_on A P \<Longrightarrow> disjoint P"
hoelzl@63098
   252
  by (auto simp: partition_on_def)
hoelzl@63098
   253
hoelzl@63098
   254
lemma partition_onD3: "partition_on A P \<Longrightarrow> {} \<notin> P"
hoelzl@63098
   255
  by (auto simp: partition_on_def)
hoelzl@63098
   256
hoelzl@63098
   257
subsection \<open>Constructions of partitions\<close>
hoelzl@63098
   258
hoelzl@63098
   259
lemma partition_on_empty: "partition_on {} P \<longleftrightarrow> P = {}"
hoelzl@63098
   260
  unfolding partition_on_def by fastforce
hoelzl@63098
   261
hoelzl@63098
   262
lemma partition_on_space: "A \<noteq> {} \<Longrightarrow> partition_on A {A}"
hoelzl@63098
   263
  by (auto simp: partition_on_def disjoint_def)
hoelzl@63098
   264
hoelzl@63098
   265
lemma partition_on_singletons: "partition_on A ((\<lambda>x. {x}) ` A)"
hoelzl@63098
   266
  by (auto simp: partition_on_def disjoint_def)
hoelzl@63098
   267
hoelzl@63098
   268
lemma partition_on_transform:
hoelzl@63098
   269
  assumes P: "partition_on A P"
hoelzl@63098
   270
  assumes F_UN: "\<Union>(F ` P) = F (\<Union>P)" and F_disjnt: "\<And>p q. p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (F p) (F q)"
hoelzl@63098
   271
  shows "partition_on (F A) (F ` P - {{}})"
hoelzl@63098
   272
proof -
hoelzl@63098
   273
  have "\<Union>(F ` P - {{}}) = F A"
hoelzl@63098
   274
    unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
hoelzl@63098
   275
  with P show ?thesis
hoelzl@63098
   276
    by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
hoelzl@63098
   277
qed
hoelzl@63098
   278
hoelzl@63098
   279
lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) (op \<inter> B ` P - {{}})"
hoelzl@63098
   280
  by (intro partition_on_transform) (auto simp: disjnt_def)
hoelzl@63098
   281
hoelzl@63098
   282
lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) (op -` f ` P - {{}})"
hoelzl@63098
   283
  by (intro partition_on_transform) (auto simp: disjnt_def)
hoelzl@63098
   284
hoelzl@63098
   285
lemma partition_on_inj_image:
hoelzl@63098
   286
  assumes P: "partition_on A P" and f: "inj_on f A"
hoelzl@63098
   287
  shows "partition_on (f ` A) (op ` f ` P - {{}})"
hoelzl@63098
   288
proof (rule partition_on_transform[OF P])
hoelzl@63098
   289
  show "p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (f ` p) (f ` q)" for p q
hoelzl@63098
   290
    using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
hoelzl@63098
   291
qed auto
hoelzl@63098
   292
hoelzl@63098
   293
subsection \<open>Finiteness of partitions\<close>
hoelzl@63098
   294
hoelzl@63098
   295
lemma finitely_many_partition_on:
hoelzl@63098
   296
  assumes "finite A"
hoelzl@63098
   297
  shows "finite {P. partition_on A P}"
hoelzl@63098
   298
proof (rule finite_subset)
hoelzl@63098
   299
  show "{P. partition_on A P} \<subseteq> Pow (Pow A)"
hoelzl@63098
   300
    unfolding partition_on_def by auto
hoelzl@63098
   301
  show "finite (Pow (Pow A))"
hoelzl@63098
   302
    using assms by simp
hoelzl@63098
   303
qed
hoelzl@63098
   304
hoelzl@63098
   305
lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P"
hoelzl@63098
   306
  using partition_onD1[of A P] by (simp add: finite_UnionD)
hoelzl@63098
   307
hoelzl@63098
   308
subsection \<open>Equivalence of partitions and equivalence classes\<close>
hoelzl@63098
   309
hoelzl@63098
   310
lemma partition_on_quotient:
hoelzl@63098
   311
  assumes r: "equiv A r"
hoelzl@63098
   312
  shows "partition_on A (A // r)"
hoelzl@63098
   313
proof (rule partition_onI)
hoelzl@63098
   314
  from r have "refl_on A r"
hoelzl@63098
   315
    by (auto elim: equivE)
hoelzl@63098
   316
  then show "\<Union>(A // r) = A" "{} \<notin> A // r"
hoelzl@63098
   317
    by (auto simp: refl_on_def quotient_def)
hoelzl@63098
   318
hoelzl@63098
   319
  fix p q assume "p \<in> A // r" "q \<in> A // r" "p \<noteq> q"
hoelzl@63098
   320
  then obtain x y where "x \<in> A" "y \<in> A" "p = r `` {x}" "q = r `` {y}"
hoelzl@63098
   321
    by (auto simp: quotient_def)
hoelzl@63098
   322
  with r equiv_class_eq_iff[OF r, of x y] \<open>p \<noteq> q\<close> show "disjnt p q"
hoelzl@63098
   323
    by (auto simp: disjnt_equiv_class)
hoelzl@63098
   324
qed
hoelzl@63098
   325
hoelzl@63098
   326
lemma equiv_partition_on:
hoelzl@63098
   327
  assumes P: "partition_on A P"
hoelzl@63098
   328
  shows "equiv A {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p}"
hoelzl@63098
   329
proof (rule equivI)
hoelzl@63098
   330
  have "A = \<Union>P" "disjoint P" "{} \<notin> P"
hoelzl@63098
   331
    using P by (auto simp: partition_on_def)
hoelzl@63098
   332
  then show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
hoelzl@63098
   333
    unfolding refl_on_def by auto
hoelzl@63098
   334
  show "trans {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
hoelzl@63098
   335
    using \<open>disjoint P\<close> by (auto simp: trans_def disjoint_def)
hoelzl@63098
   336
qed (auto simp: sym_def)
hoelzl@63098
   337
hoelzl@63098
   338
lemma partition_on_eq_quotient:
hoelzl@63098
   339
  assumes P: "partition_on A P"
hoelzl@63098
   340
  shows "A // {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} = P"
hoelzl@63098
   341
  unfolding quotient_def
hoelzl@63098
   342
proof safe
hoelzl@63098
   343
  fix x assume "x \<in> A"
hoelzl@63098
   344
  then obtain p where "p \<in> P" "x \<in> p" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
hoelzl@63098
   345
    using P by (auto simp: partition_on_def disjoint_def)
hoelzl@63098
   346
  then have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p"
hoelzl@63098
   347
    by (safe intro!: bexI[of _ p]) simp
hoelzl@63098
   348
  then show "{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x} \<in> P"
hoelzl@63098
   349
    by (simp add: \<open>p \<in> P\<close>)
hoelzl@63098
   350
next
hoelzl@63098
   351
  fix p assume "p \<in> P"
hoelzl@63098
   352
  then have "p \<noteq> {}"
hoelzl@63098
   353
    using P by (auto simp: partition_on_def)
hoelzl@63098
   354
  then obtain x where "x \<in> p"
hoelzl@63098
   355
    by auto
hoelzl@63098
   356
  then have "x \<in> A" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
hoelzl@63098
   357
    using P \<open>p \<in> P\<close> by (auto simp: partition_on_def disjoint_def)
hoelzl@63098
   358
  with \<open>p\<in>P\<close> \<open>x \<in> p\<close> have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p"
hoelzl@63098
   359
    by (safe intro!: bexI[of _ p]) simp
hoelzl@63098
   360
  then show "p \<in> (\<Union>x\<in>A. {{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x}})"
hoelzl@63098
   361
    by (auto intro: \<open>x \<in> A\<close>)
hoelzl@63098
   362
qed
hoelzl@63098
   363
hoelzl@63098
   364
lemma partition_on_alt: "partition_on A P \<longleftrightarrow> (\<exists>r. equiv A r \<and> P = A // r)"
hoelzl@63098
   365
  by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)
hoelzl@63098
   366
nipkow@62390
   367
end