Impressum Disjoint_Sets.thy

(*  Author:     Johannes Hölzl, TU München
*)

section ‹Partitions and Disjoint Sets›

theory Disjoint_Sets
  imports FuncSet
begin

lemma mono_imp_UN_eq_last: "mono A ==> (∪i≤n. A i) = A n"
  unfolding mono_def by auto

subsection ‹Set of Disjoint Sets›

abbreviation disjoint :: "'a set set ==> bool" where "disjoint ≡ pairwise disjnt"

lemma disjoint_def: "disjoint A ⟷ (∀a∈A. ∀b∈A. a ≠ b ⟶ a ∩ b = {})"
  unfolding pairwise_def disjnt_def by auto

lemma disjointI:
  "(∧a b. a ∈ A ==> b ∈ A ==> a ≠ b ==> a ∩ b = {}) ==> disjoint A"
  unfolding disjoint_def by auto

lemma disjointD:
  "disjoint A ==> a ∈ A ==> b ∈ A ==> a ≠ b ==> a ∩ b = {}"
  unfolding disjoint_def by auto

lemma disjoint_image: "inj_on f (∪A) ==> disjoint A ==> disjoint ((`) f ` A)"
  unfolding inj_on_def disjoint_def by blast

lemma assumes "disjoint (A ∪ B)"
      shows   disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
  using assms by (simp_all add: disjoint_def)
  
lemma disjoint_INT:
  assumes *: "∧i. i ∈ I ==> disjoint (F i)"
  shows "disjoint {∩i∈I. X i | X. ∀i∈I. X i ∈ F i}"
proof (safe intro!: disjointI del: equalityI)
  fix A B :: "'a ==> 'b set" assume "(∩i∈I. A i) ≠ (∩i∈I. B i)"
  then obtain i where "A i ≠ B i" "i ∈ I"
    by auto
  moreover assume "∀i∈I. A i ∈ F i" "∀i∈I. B i ∈ F i"
  ultimately show "(∩i∈I. A i) ∩ (∩i∈I. B i) = {}"
    using *[OF ‹i∈I›, THEN disjointD, of "A i" "B i"]
    by (auto simp flip: INT_Int_distrib)
qed

lemma diff_Union_pairwise_disjoint:
  assumes "pairwise disjnt A" "B ⊆ A"
  shows "∪A - ∪B = ∪(A - B)"
proof -
  have "False"
    if x: "x ∈ A" "x ∈ B" and AB: "A ∈ A" "A ∉ B" "B ∈ B" for x A B
  proof -
    have "A ∩ B = {}"
      using assms disjointD AB by blast
  with x show ?thesis
    by blast
  qed
  then show ?thesis by auto
qed

lemma Int_Union_pairwise_disjoint:
  assumes "pairwise disjnt (A ∪ B)"
  shows "∪A ∩ ∪B = ∪(A ∩ B)"
proof -
  have "False"
    if x: "x ∈ A" "x ∈ B" and AB: "A ∈ A" "A ∉ B" "B ∈ B" for x A B
  proof -
    have "A ∩ B = {}"
      using assms disjointD AB by blast
  with x show ?thesis
    by blast
  qed
  then show ?thesis by auto
qed

lemma psubset_Union_pairwise_disjoint:
  assumes B: "pairwise disjnt B" and "A ⊂ B - {{}}"
  shows "∪A ⊂ ∪B"
  unfolding psubset_eq
proof
  show "∪A ⊆ ∪B"
    using assms by blast
  have "A ⊆ B" "∪(B - A ∩ (B - {{}})) ≠ {}"
    using assms by blast+
  then show "∪A ≠ ∪B"
    using diff_Union_pairwise_disjoint [OF B] by blast
qed

subsubsection "Family of Disjoint Sets"

definition disjoint_family_on :: "('i ==> 'a set) ==> 'i set ==> bool" where
  "disjoint_family_on A S ⟷ (∀m∈S. ∀n∈S. m ≠ n ⟶ A m ∩ A n = {})"

abbreviation "disjoint_family A ≡ disjoint_family_on A UNIV"

lemma disjoint_family_elem_disjnt:
  assumes "infinite A" "finite C"
      and df: "disjoint_family_on B A"
  obtains x where "x ∈ A" "disjnt C (B x)"
proof -
  have "False" if *: "∀x ∈ A. ∃y. y ∈ C ∧ y ∈ B x"
  proof -
    obtain g where g: "∀x ∈ A. g x ∈ C ∧ g x ∈ B x"
      using * by metis
    with df have "inj_on g A"
      by (fastforce simp add: inj_on_def disjoint_family_on_def)
    then have "infinite (g ` A)"
      using ‹infinite A› finite_image_iff by blast
    then show False
      by (meson ‹finite C› finite_subset g image_subset_iff)
  qed
  then show ?thesis
    by (force simp: disjnt_iff intro: that)
qed

lemma disjoint_family_onD:
  "disjoint_family_on A I ==> i ∈ I ==> j ∈ I ==> i ≠ j ==> A i ∩ A j = {}"
  by (auto simp: disjoint_family_on_def)

lemma disjoint_family_subset: "disjoint_family A ==> (∧x. B x ⊆ A x) ==> disjoint_family B"
  by (force simp add: disjoint_family_on_def)

lemma disjoint_family_on_insert:
  "i ∉ I ==> disjoint_family_on A (insert i I) ⟷ A i ∩ (∪i∈I. A i) = {} ∧ disjoint_family_on A I"
  by (fastforce simp: disjoint_family_on_def)

lemma disjoint_family_on_bisimulation:
  assumes "disjoint_family_on f S"
  and "∧n m. n ∈ S ==> m ∈ S ==> n ≠ m ==> f n ∩ f m = {} ==> g n ∩ g m = {}"
  shows "disjoint_family_on g S"
  using assms unfolding disjoint_family_on_def by auto

lemma disjoint_family_on_mono:
  "A ⊆ B ==> disjoint_family_on f B ==> disjoint_family_on f A"
  unfolding disjoint_family_on_def by auto

lemma disjoint_family_Suc:
  "(∧n. A n ⊆ A (Suc n)) ==> disjoint_family (λi. A (Suc i) - A i)"
  using lift_Suc_mono_le[of A]
  by (auto simp add: disjoint_family_on_def)
     (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)

lemma disjoint_family_on_disjoint_image:
  "disjoint_family_on A I ==> disjoint (A ` I)"
  unfolding disjoint_family_on_def disjoint_def by force
 
lemma disjoint_family_on_vimageI: "disjoint_family_on F I ==> disjoint_family_on (λi. f -` F i) I"
  by (auto simp: disjoint_family_on_def)

lemma disjoint_image_disjoint_family_on:
  assumes d: "disjoint (A ` I)" and i: "inj_on A I"
  shows "disjoint_family_on A I"
  unfolding disjoint_family_on_def
proof (intro ballI impI)
  fix n m assume nm: "m ∈ I" "n ∈ I" and "n ≠ m"
  with i[THEN inj_onD, of n m] show "A n ∩ A m = {}"
    by (intro disjointD[OF d]) auto
qed

lemma disjoint_family_on_iff_disjoint_image:
  assumes "∧i. i ∈ I ==> A i ≠ {}"
  shows "disjoint_family_on A I ⟷ disjoint (A ` I) ∧ inj_on A I"
proof
  assume "disjoint_family_on A I"
  then show "disjoint (A ` I) ∧ inj_on A I"
    by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_image inf.idem inj_onI)
qed (use disjoint_image_disjoint_family_on in metis)

lemma card_UN_disjoint':
  assumes "disjoint_family_on A I" "∧i. i ∈ I ==> finite (A i)" "finite I"
  shows "card (∪i∈I. A i) = (∑i∈I. card (A i))"
  using assms   by (simp add: card_UN_disjoint disjoint_family_on_def)

lemma disjoint_UN:
  assumes F: "∧i. i ∈ I ==> disjoint (F i)" and *: "disjoint_family_on (λi. ∪(F i)) I"
  shows "disjoint (∪i∈I. F i)"
proof (safe intro!: disjointI del: equalityI)
  fix A B i j assume "A ≠ B" "A ∈ F i" "i ∈ I" "B ∈ F j" "j ∈ I"
  show "A ∩ B = {}"
  proof cases
    assume "i = j" with F[of i] ‹i ∈ I› ‹A ∈ F i› ‹B ∈ F j› ‹A ≠ B› show "A ∩ B = {}"
      by (auto dest: disjointD)
  next
    assume "i ≠ j"
    with * ‹i∈I› ‹j∈I› have "(∪(F i)) ∩ (∪(F j)) = {}"
      by (rule disjoint_family_onD)
    with ‹A∈F i› ‹i∈I› ‹B∈F j› ‹j∈I›
    show "A ∩ B = {}"
      by auto
  qed
qed

lemma distinct_list_bind: 
  assumes "distinct xs" "∧x. x ∈ set xs ==> distinct (f x)" 
          "disjoint_family_on (set ∘ f) (set xs)"
  shows   "distinct (List.bind xs f)"
  using assms
  by (induction xs)
     (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)

lemma bij_betw_UNION_disjoint:
  assumes disj: "disjoint_family_on A' I"
  assumes bij: "∧i. i ∈ I ==> bij_betw f (A i) (A' i)"
  shows   "bij_betw f (∪i∈I. A i) (∪i∈I. A' i)"
unfolding bij_betw_def
proof
  from bij show eq: "f ` ∪(A ` I) = ∪(A' ` I)"
    by (auto simp: bij_betw_def image_UN)
  show "inj_on f (∪(A ` I))"
  proof (rule inj_onI, clarify)
    fix i j x y assume A: "i ∈ I" "j ∈ I" "x ∈ A i" "y ∈ A j" and B: "f x = f y"
    from A bij[of i] bij[of j] have "f x ∈ A' i" "f y ∈ A' j"
      by (auto simp: bij_betw_def)
    with B have "A' i ∩ A' j ≠ {}" by auto
    with disj A have "i = j" unfolding disjoint_family_on_def by blast
    with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
  qed
qed

lemma disjoint_union: "disjoint C ==> disjoint B ==> ∪C ∩ ∪B = {} ==> disjoint (C ∪ B)"
  using disjoint_UN[of "{C, B}" "λx. x"] by (auto simp add: disjoint_family_on_def)

text ‹
  Sum/product of the union of a finite disjoint family
 ›
context comm_monoid_set
begin

lemma UNION_disjoint_family:
  assumes "finite I" and "∀i∈I. finite (A i)"
    and "disjoint_family_on A I"
  shows "F g (∪(A ` I)) = F (λx. F g (A x)) I"
  using assms unfolding disjoint_family_on_def  by (rule UNION_disjoint)

lemma Union_disjoint_sets:
  assumes "∀A∈C. finite A" and "disjoint C"
  shows "F g (∪C) = (F ∘ F) g C"
  using assms unfolding disjoint_def  by (rule Union_disjoint)

end

text ‹
  The union of an infinite disjoint family of non-empty sets is infinite.
 ›
lemma infinite_disjoint_family_imp_infinite_UNION:
  assumes "¬finite A" "∧x. x ∈ A ==> f x ≠ {}" "disjoint_family_on f A"
  shows   "¬finite (∪(f ` A))"
proof -
  define g where "g x = (SOME y. y ∈ f x)" for x
  have g: "g x ∈ f x" if "x ∈ A" for x
    unfolding g_def by (rule someI_ex, insert assms(2) that) blast
  have inj_on_g: "inj_on g A"
  proof (rule inj_onI, rule ccontr)
    fix x y assume A: "x ∈ A" "y ∈ A" "g x = g y" "x ≠ y"
    with g[of x] g[of y] have "g x ∈ f x" "g x ∈ f y" by auto
    with A ‹x ≠ y› assms show False
      by (auto simp: disjoint_family_on_def inj_on_def)
  qed
  from g have "g ` A ⊆ ∪(f ` A)" by blast
  moreover from inj_on_g ‹¬finite A› have "¬finite (g ` A)"
    using finite_imageD by blast
  ultimately show ?thesis using finite_subset by blast
qed  
  

subsection ‹Construct Disjoint Sequences›

definition disjointed :: "(nat ==> 'a set) ==> nat ==> 'a set" where
  "disjointed A n = A n - (∪i∈{0..

lemma finite_UN_disjointed_eq: "(∪i∈{0..∪i∈{0..
proof (induct n)
  case 0 show ?case by simp
next
  case (Suc n)
  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
qed

lemma UN_disjointed_eq: "(∪i. disjointed A i) = (∪i. A i)"
  by (rule UN_finite2_eq [where k=0])
     (simp add: finite_UN_disjointed_eq)

lemma less_disjoint_disjointed: "m < n ==> disjointed A m ∩ disjointed A n = {}"
  by (auto simp add: disjointed_def)

lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
  by (simp add: disjoint_family_on_def)
     (metis neq_iff Int_commute less_disjoint_disjointed)

lemma disjointed_subset: "disjointed A n ⊆ A n"
  by (auto simp add: disjointed_def)

lemma disjointed_0[simp]: "disjointed A 0 = A 0"
  by (simp add: disjointed_def)

lemma disjointed_mono: "mono A ==> disjointed A (Suc n) = A (Suc n) - A n"
  using mono_imp_UN_eq_last[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)

subsection ‹Partitions›

text ‹
  Partitions 🍋‹P› of a set 🍋‹A›. We explicitly disallow empty sets.
 ›

definition partition_on :: "'a set ==> 'a set set ==> bool"
where
  "partition_on A P ⟷ ∪P = A ∧ disjoint P ∧ {} ∉ P"

lemma partition_onI:
  "∪P = A ==> (∧p q. p ∈ P ==> q ∈ P ==> p ≠ q ==> disjnt p q) ==> {} ∉ P ==> partition_on A P"
  by (auto simp: partition_on_def pairwise_def)

lemma partition_onD1: "partition_on A P ==> A = ∪P"
  by (auto simp: partition_on_def)

lemma partition_onD2: "partition_on A P ==> disjoint P"
  by (auto simp: partition_on_def)

lemma partition_onD3: "partition_on A P ==> {} ∉ P"
  by (auto simp: partition_on_def)

subsection ‹Constructions of partitions›

lemma partition_on_empty: "partition_on {} P ⟷ P = {}"
  unfolding partition_on_def by fastforce

lemma partition_on_space: "A ≠ {} ==> partition_on A {A}"
  by (auto simp: partition_on_def disjoint_def)

lemma partition_on_singletons: "partition_on A ((λx. {x}) ` A)"
  by (auto simp: partition_on_def disjoint_def)

lemma partition_on_transform:
  assumes P: "partition_on A P"
  assumes F_UN: "∪(F ` P) = F (∪P)" and F_disjnt: "∧p q. p ∈ P ==> q ∈ P ==> disjnt p q ==> disjnt (F p) (F q)"
  shows "partition_on (F A) (F ` P - {{}})"
proof -
  have "∪(F ` P - {{}}) = F A"
    unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
  with P show ?thesis
    by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
qed

lemma partition_on_restrict: "partition_on A P ==> partition_on (B ∩ A) ((∩) B ` P - {{}})"
  by (intro partition_on_transform) (auto simp: disjnt_def)

lemma partition_on_vimage: "partition_on A P ==> partition_on (f -` A) ((-`) f ` P - {{}})"
  by (intro partition_on_transform) (auto simp: disjnt_def)

lemma partition_on_inj_image:
  assumes P: "partition_on A P" and f: "inj_on f A"
  shows "partition_on (f ` A) ((`) f ` P - {{}})"
proof (rule partition_on_transform[OF P])
  show "p ∈ P ==> q ∈ P ==> disjnt p q ==> disjnt (f ` p) (f ` q)" for p q
    using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
qed auto

lemma partition_on_insert:
  assumes "disjnt p (∪P)"
  shows "partition_on A (insert p P) ⟷ partition_on (A-p) P ∧ p ⊆ A ∧ p ≠ {}"
  using assms
  by (auto simp: partition_on_def disjnt_iff pairwise_insert)

subsection ‹Finiteness of partitions›

lemma finitely_many_partition_on:
  assumes "finite A"
  shows "finite {P. partition_on A P}"
proof (rule finite_subset)
  show "{P. partition_on A P} ⊆ Pow (Pow A)"
    unfolding partition_on_def by auto
  show "finite (Pow (Pow A))"
    using assms by simp
qed

lemma finite_elements: "finite A ==> partition_on A P ==> finite P"
  using partition_onD1[of A P] by (simp add: finite_UnionD)

lemma product_partition:
  assumes "partition_on A P" and "∧p. p ∈ P ==> finite p" 
  shows "card A = (∑p∈P. card p)"
  using assms unfolding partition_on_def  by (meson card_Union_disjoint)

subsection ‹Equivalence of partitions and equivalence classes›

lemma partition_on_quotient:
  assumes r: "equiv A r"
  shows "partition_on A (A // r)"
proof (rule partition_onI)
  from r have "r ⊆ A × A" and "refl_on A r"
    by (auto elim: equivE)
  then show "∪(A // r) = A" "{} ∉ A // r"
    by (auto simp: refl_on_def quotient_def)

  fix p q assume "p ∈ A // r" "q ∈ A // r" "p ≠ q"
  then obtain x y where "x ∈ A" "y ∈ A" "p = r `` {x}" "q = r `` {y}"
    by (auto simp: quotient_def)
  with r equiv_class_eq_iff[OF r, of x y] ‹p ≠ q› show "disjnt p q"
    by (auto simp: disjnt_equiv_class)
qed

lemma equiv_partition_on:
  assumes P: "partition_on A P"
  shows "equiv A {(x, y). ∃p ∈ P. x ∈ p ∧ y ∈ p}"
proof (rule equivI)
  have "A = ∪P"
    using P by (auto simp: partition_on_def)

  show "{(x, y). ∃p ∈ P. x ∈ p ∧ y ∈ p} ⊆ A × A"
    unfolding ‹A = ∪P› by blast

  show "refl_on A {(x, y). ∃p∈P. x ∈ p ∧ y ∈ p}"
    unfolding refl_on_def ‹A = ∪P› by auto
next
  show "trans {(x, y). ∃p∈P. x ∈ p ∧ y ∈ p}"
    using P by (auto simp only: trans_def disjoint_def partition_on_def)
next
  show "sym {(x, y). ∃p∈P. x ∈ p ∧ y ∈ p}"
    by (auto simp only: sym_def)
qed

lemma partition_on_eq_quotient:
  assumes P: "partition_on A P"
  shows "A // {(x, y). ∃p ∈ P. x ∈ p ∧ y ∈ p} = P"
  unfolding quotient_def
proof safe
  fix x assume "x ∈ A"
  then obtain p where "p ∈ P" "x ∈ p" "∧q. q ∈ P ==> x ∈ q ==> p = q"
    using P by (auto simp: partition_on_def disjoint_def)
  then have "{y. ∃p∈P. x ∈ p ∧ y ∈ p} = p"
    by (safe intro!: bexI[of _ p]) simp
  then show "{(x, y). ∃p∈P. x ∈ p ∧ y ∈ p} `` {x} ∈ P"
    by (simp add: ‹p ∈ P›)
next
  fix p assume "p ∈ P"
  then have "p ≠ {}"
    using P by (auto simp: partition_on_def)
  then obtain x where "x ∈ p"
    by auto
  then have "x ∈ A" "∧q. q ∈ P ==> x ∈ q ==> p = q"
    using P ‹p ∈ P› by (auto simp: partition_on_def disjoint_def)
  with ‹p∈P› ‹x ∈ p› have "{y. ∃p∈P. x ∈ p ∧ y ∈ p} = p"
    by (safe intro!: bexI[of _ p]) simp
  then show "p ∈ (∪x∈A. {{(x, y). ∃p∈P. x ∈ p ∧ y ∈ p} `` {x}})"
    by (auto intro: ‹x ∈ A›)
qed

lemma partition_on_alt: "partition_on A P ⟷ (∃r. equiv A r ∧ P = A // r)"
  by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)

lemma (in comm_monoid_set) partition:
  assumes "finite X" "partition_on X A"
  shows   "F g X = F (λB. F g B) A"
proof -
  have "finite A"
    using assms finite_UnionD partition_onD1 by auto
  have [intro]: "finite B" if "B ∈ A" for B
    by (rule finite_subset[OF _ assms(1)])
       (use assms that in ‹auto simp: partition_on_def›)
  have "F g X = F g (∪A)"
    using assms by (simp add: partition_on_def)
  also have "… = (F ∘ F) g A"
    by (rule Union_disjoint) (use assms ‹finite A› in ‹auto simp: partition_on_def disjoint_def›)
  finally show ?thesis
    by simp
qed


text ‹
  If $h$ is an involution on $X$ with no fixed points in $X$ and
  $f(h(x)) = -f(x)$ then $\sum_{x\in X} f(x) = 0$.
 
  This is easy to show in a ring with characteristic not equal to $2$, since then we can do
  \[\sum_{x\in X} f(x) = \sum_{x\in X} f(h(x)) = -\sum_{x\in X} f(x)\]
  and therefore $2 \sum_{x\in X} f(x) = 0$.
 
  However, the following proof also works in rings of characteristic 2.
  The idea is to simply partition $X$ into a disjoint union of doubleton sets of the form
  $\{x, h(x)\}$.
 ›
lemma sum_involution_eq_0:
  assumes f_h: "∧x. x ∈ X ==> f (h x) + f x = 0"
  assumes h:   "∧x. x ∈ X ==> h x ∈ X" "∧x. x ∈ X ==> h (h x) = x" "∧x. x ∈ X ==> h x ≠ x"
  shows   "(∑x∈X. f x) = 0"
proof (cases "finite X")
  assume fin: "finite X"
  define R where "R = {(x,y). x ∈ X ∧ y ∈ X ∧ (x = y ∨ h x = y)}"
  have R: "equiv X R"
    unfolding equiv_def R_def using h(2,3)
    by (auto simp: refl_on_def sym_def trans_def)
  define A where "A = X // R"
  have partition: "partition_on X A"
    unfolding A_def using R by (rule partition_on_quotient)

  have "(∑x∈X. f x) = (∑B∈A. ∑x∈B. f x)"
    by (subst sum.partition[OF fin partition]) auto
  also have "… = (∑B∈A. 0)"
  proof (rule sum.cong)
    fix B assume B: "B ∈ A"
    then obtain x where x: "x ∈ X" and [simp]: "B = R `` {x}"
      using R by (metis A_def quotientE)
    have "R `` {x} = {x, h x}" "h x ≠ x"
      using h x(1) by (auto simp: R_def)
    thus "(∑x∈B. f x) = 0"
      using x f_h[of x] by (simp add: add.commute)
  qed auto
  finally show ?thesis
    by simp
qed auto


subsection ‹Refinement of partitions›

definition refines :: "'a set ==> 'a set set ==> 'a set set ==> bool"
  where "refines A P Q ≡
        partition_on A P ∧ partition_on A Q ∧ (∀X∈P. ∃Y∈Q. X ⊆ Y)" 

lemma refines_refl: "partition_on A P ==> refines A P P"
  using refines_def by blast

lemma refines_asym1:
  assumes "refines A P Q" "refines A Q P"
  shows "P ⊆ Q"
proof 
  fix X
  assume "X ∈ P"
  then obtain Y X' where "Y ∈ Q" "X ⊆ Y" "X' ∈ P" "Y ⊆ X'"
    by (meson assms refines_def)
  then have "X' = X"
    using assms(2) unfolding partition_on_def refines_def
    by (metis ‹X ∈ P› ‹X ⊆ Y› disjnt_self_iff_empty disjnt_subset1 pairwiseD)
  then show "X ∈ Q"
    using ‹X ⊆ Y› ‹Y ∈ Q› ‹Y ⊆ X'› by force
qed

lemma refines_asym: "[refines A P Q; refines A Q P] ==> P=Q"
  by (meson antisym_conv refines_asym1)

lemma refines_trans: "[refines A P Q; refines A Q R] ==> refines A P R"
  by (meson order.trans refines_def)

lemma refines_obtains_subset:
  assumes "refines A P Q" "q ∈ Q"
  shows "partition_on q {p ∈ P. p ⊆ q}"
proof -
  have "p ⊆ q ∨ disjnt p q" if "p ∈ P" for p
    using that assms unfolding refines_def partition_on_def disjoint_def
    by (metis disjnt_def disjnt_subset1)
  with assms have "q ⊆ Union {p ∈ P. p ⊆ q}"
    using assms 
   by (clarsimp simp: refines_def disjnt_iff partition_on_def) (metis Union_iff)
  with assms have "q = Union {p ∈ P. p ⊆ q}"
    by auto
  then show ?thesis
    using assms by (auto simp: refines_def disjoint_def partition_on_def)
qed 

subsection ‹The coarsest common refinement of a set of partitions›

definition common_refinement :: "'a set set set ==> 'a set set"
  where "common_refinement P ≡ (∪f ∈ (Π🪙E P∈P. P). {∩ (f ` P)}) - {{}}" 

text ‹With non-extensional function space›
lemma common_refinement: "common_refinement P = (∪f ∈ (Π P∈P. P). {∩ (f ` P)}) - {{}}" 
  (is "?lhs = ?rhs")
proof
  show "?rhs ⊆ ?lhs"
    apply (clarsimp simp add: common_refinement_def PiE_def Ball_def)
    by (metis restrict_Pi_cancel image_restrict_eq restrict_extensional)
qed (auto simp add: common_refinement_def PiE_def)

lemma common_refinement_exists: "[X ∈ common_refinement P; P ∈ P] ==> ∃R∈P. X ⊆ R"
  by (auto simp add: common_refinement)

lemma Union_common_refinement: "∪ (common_refinement P) = (∩ P∈P. ∪P)"
proof
  show "(∩ P∈P. ∪P) ⊆ ∪ (common_refinement P)"
  proof (clarsimp simp: common_refinement)
    fix x
    assume "∀P∈P. ∃X∈P. x ∈ X"
    then obtain F where F: "∧P. P∈P ==> F P ∈ P ∧ x ∈ F P"
      by metis
    then have "x ∈ ∩ (F ` P)"
      by force
    with F show "∃X∈(∪x∈Π P∈P. P. {∩ (x ` P)}) - {{}}. x ∈ X"
      by (auto simp add: Pi_iff Bex_def)
  qed
qed (auto simp: common_refinement_def)

lemma partition_on_common_refinement:
  assumes A: "∧P. P ∈ P ==> partition_on A P" and "P ≠ {}"
  shows "partition_on A (common_refinement P)"
proof (rule partition_onI)
  show "∪ (common_refinement P) = A"
    using assms by (simp add: partition_on_def Union_common_refinement)
  fix P Q
  assume "P ∈ common_refinement P" and "Q ∈ common_refinement P" and "P ≠ Q"
  then obtain f g where f: "f ∈ (Π🪙E P∈P. P)" and P: "P = ∩ (f ` P)" and "P ≠ {}"
                  and   g: "g ∈ (Π🪙E P∈P. P)" and Q: "Q = ∩ (g ` P)" and "Q ≠ {}"
    by (auto simp add: common_refinement_def)
  have "f=g" if "x ∈ P" "x ∈ Q" for x
  proof (rule extensionalityI [of _ P])
    fix R
    assume "R ∈ P"
    with that P Q f g A [unfolded partition_on_def, OF ‹R ∈ P›]
    show "f R = g R"
      by (metis INT_E Int_iff PiE_iff disjointD emptyE)
  qed (use PiE_iff f g in auto)
  then show "disjnt P Q"
    by (metis P Q ‹P ≠ Q› disjnt_iff) 
qed (simp add: common_refinement_def)

lemma refines_common_refinement:
  assumes "∧P. P ∈ P ==> partition_on A P" "P ∈ P"
  shows "refines A (common_refinement P) P"
  unfolding refines_def
proof (intro conjI strip)
  fix X
  assume "X ∈ common_refinement P"
  with assms show "∃Y∈P. X ⊆ Y"
    by (auto simp: common_refinement_def)
qed (use assms partition_on_common_refinement in auto)

text ‹The common refinement is itself refined by any other›
lemma common_refinement_coarsest:
  assumes "∧P. P ∈ P ==> partition_on A P" "partition_on A R" "∧P. P ∈ P ==> refines A R P" "P ≠ {}"
  shows "refines A R (common_refinement P)"
  unfolding refines_def
proof (intro conjI ballI partition_on_common_refinement)
  fix X
  assume "X ∈ R"
  have "∃p ∈ P. X ⊆ p" if "P ∈ P" for P
    by (meson ‹X ∈ R› assms(3) refines_def that)
  then obtain F where f: "∧P. P ∈ P ==> F P ∈ P ∧ X ⊆ F P"
    by metis
  with ‹partition_on A R› ‹X ∈ R› ‹P ≠ {}›
  have "∩ (F ` P) ∈ common_refinement P"
    apply (simp add: partition_on_def common_refinement Pi_iff Bex_def)
    by (metis (no_types, lifting) cINF_greatest subset_empty)
  with f show "∃Y∈common_refinement P. X ⊆ Y"
    by (metis ‹P ≠ {}› cINF_greatest)
qed (use assms in auto)

lemma finite_common_refinement:
  assumes "finite P" "∧P. P ∈ P ==> finite P"
  shows "finite (common_refinement P)"
proof -
  have "finite (Π🪙E P∈P. P)"
    by (simp add: assms finite_PiE)
  then show ?thesis
    by (auto simp: common_refinement_def)
qed

lemma card_common_refinement:
  assumes "finite P" "∧P. P ∈ P ==> finite P"
  shows "card (common_refinement P) ≤ (∏P ∈ P. card P)"
proof -
  have "card (common_refinement P) ≤ card (∪f ∈ (Π🪙E P∈P. P). {∩ (f ` P)})"
    unfolding common_refinement_def by (meson card_Diff1_le)
  also have "… ≤ (∑f∈(Π🪙E P∈P. P). card{∩ (f ` P)})"
    by (metis assms finite_PiE card_UN_le)
  also have "… = card(Π🪙E P∈P. P)"
    by simp
  also have "… = (∏P ∈ P. card P)"
    by (simp add: assms(1) card_PiE dual_order.eq_iff)
  finally show ?thesis .
qed

end