Theory CM

section ‹ Closed Mereology ›

(*<*)
theory CM
  imports M
begin
(*>*)

text ‹ The theory of \emph{closed mereology} adds to ground mereology conditions guaranteeing the
existence of sums and products.\footnote{See \<^cite>‹"masolo_atomicity_1999"› p. 238. \<^cite>‹"varzi_parts_1996"› p. 263 
and \<^cite>‹"casati_parts_1999"› p. 43 give a slightly weaker version of the sum closure axiom, which is
equivalent given axioms considered later.} ›

locale CM = M +
  assumes sum_eq: "x ⊕ y = (THE z. ∀v. O v z ⟷ O v x ∨ O v y)"
  assumes sum_closure: "∃z. ∀v. O v z ⟷ O v x ∨ O v y"
  assumes product_eq: 
    "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
  assumes product_closure: 
    "O x y ⟹ ∃z. ∀v. P v z ⟷ P v x ∧ P v y"
begin

subsection ‹ Products ›

lemma product_intro: 
  "(∀w. P w z ⟷ (P w x ∧ P w y)) ⟹ x ⊗ y = z"
proof -
  assume z: "∀w. P w z ⟷ (P w x ∧ P w y)"
  hence "(THE v. ∀w. P w v ⟷ P w x ∧ P w y) = z"
  proof (rule the_equality)
    fix v
    assume v: "∀w. P w v ⟷ (P w x ∧ P w y)"
    have "∀w. P w v ⟷ P w z"
    proof
      fix w
      from z have "P w z ⟷ (P w x ∧ P w y)"..
      moreover from v have "P w v ⟷ (P w x ∧ P w y)"..
      ultimately show "P w v ⟷ P w z" by (rule ssubst)
    qed
    with part_extensionality show "v = z"..
  qed
  thus "x ⊗ y = z"
    using product_eq by (rule subst)
qed

lemma product_idempotence: "x ⊗ x = x"
proof -
  have "∀w. P w x ⟷ P w x ∧ P w x"
  proof
    fix w
    show "P w x ⟷ P w x ∧ P w x"
    proof
      assume "P w x"
      thus "P w x ∧ P w x" using ‹P w x›..
    next
      assume "P w x ∧ P w x"
      thus "P w x"..
    qed
  qed
  thus "x ⊗ x = x" by (rule product_intro)
qed

lemma product_character: 
  "O x y ⟹ (∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y))"
proof -
  assume "O x y"
  hence "∃z. ∀w. P w z ⟷ (P w x ∧ P w y)" by (rule product_closure)
  then obtain z where z: "∀w. P w z ⟷ (P w x ∧ P w y)"..
  hence "x ⊗ y = z" by (rule product_intro)
  thus "∀w. P w (x ⊗ y) ⟷ P w x ∧ P w y"
    using z by (rule ssubst)
qed

lemma product_commutativity: "O x y ⟹ x ⊗ y = y ⊗ x"
proof -
  assume "O x y"
  hence "O y x" by (rule overlap_symmetry)
  hence "∀w. P w (y ⊗ x) ⟷ (P w y ∧ P w x)" by (rule product_character)
  hence "∀w. P w (y ⊗ x) ⟷ (P w x ∧ P w y)" by auto
  thus "x ⊗ y = y ⊗ x" by (rule product_intro)
qed

lemma product_in_factors: "O x y ⟹ P (x ⊗ y) x ∧ P (x ⊗ y) y"
proof -
  assume "O x y"
  hence "∀w. P w (x ⊗ y) ⟷ P w x ∧ P w y" by (rule product_character)
  hence "P (x ⊗ y) (x ⊗ y) ⟷ P (x ⊗ y) x ∧ P (x ⊗ y) y"..
  moreover have "P (x ⊗ y) (x ⊗ y)" by (rule part_reflexivity)
  ultimately show "P (x ⊗ y) x ∧ P (x ⊗ y) y"..
qed

lemma product_in_first_factor: "O x y ⟹ P (x ⊗ y) x"
proof -
  assume "O x y"
  hence "P (x ⊗ y) x ∧ P (x ⊗ y) y" by (rule product_in_factors)
  thus "P (x ⊗ y) x"..
qed

lemma product_in_second_factor: "O x y ⟹ P (x ⊗ y) y"
proof -
  assume "O x y"
  hence "P (x ⊗ y) x ∧ P (x ⊗ y) y" by (rule product_in_factors)
  thus "P (x ⊗ y) y"..
qed

lemma nonpart_implies_proper_product: 
  "¬ P x y ∧ O x y ⟹ PP (x ⊗ y) x"
proof -
  assume antecedent: "¬ P x y ∧ O x y"
  hence "¬ P x y"..
  from antecedent have "O x y"..
  hence "P (x ⊗ y) x" by (rule product_in_first_factor)
  moreover have "(x ⊗ y) ≠ x"
  proof
    assume "(x ⊗ y) = x"
    hence "¬ P (x ⊗ y) y"
      using ‹¬ P x y› by (rule ssubst)
    moreover have "P (x ⊗ y) y"
      using ‹O x y› by (rule product_in_second_factor)
    ultimately show "False"..
  qed
  ultimately have "P (x ⊗ y) x ∧ x ⊗ y ≠ x"..
  with nip_eq show "PP (x ⊗ y) x"..
qed

lemma common_part_in_product: "P z x ∧ P z y ⟹ P z (x ⊗ y)"
proof -
  assume antecedent: "P z x ∧ P z y"
  hence "∃z. P z x ∧ P z y"..
  with overlap_eq have "O x y"..
  hence "∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y)"
    by (rule product_character)
  hence "P z (x ⊗ y) ⟷ (P z x ∧ P z y)"..
  thus "P z (x ⊗ y)" 
    using ‹P z x ∧ P z y›..
qed

lemma product_part_in_factors: 
  "O x y ⟹ P z (x ⊗ y) ⟹ P z x ∧ P z y"
proof -
  assume "O x y"
  hence "∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y)"
    by (rule product_character)
  hence "P z (x ⊗ y) ⟷ (P z x ∧ P z y)"..
  moreover assume "P z (x ⊗ y)"
  ultimately show "P z x ∧ P z y"..
qed

corollary product_part_in_first_factor: 
  "O x y ⟹ P z (x ⊗ y) ⟹ P z x"
proof -
  assume "O x y"
  moreover assume "P z (x ⊗ y)"
  ultimately have "P z x ∧ P z y"
    by (rule product_part_in_factors)
  thus "P z x"..
qed

corollary product_part_in_second_factor: 
  "O x y ⟹ P z (x ⊗ y) ⟹ P z y"
proof -
  assume "O x y"
  moreover assume "P z (x ⊗ y)"
  ultimately have "P z x ∧ P z y"
    by (rule product_part_in_factors)
  thus "P z y"..
qed

lemma part_product_identity: "P x y ⟹ x ⊗ y = x"
proof -
  assume "P x y"
  with part_reflexivity have "P x x ∧ P x y"..
  hence "P x (x ⊗ y)" by (rule common_part_in_product)
  have "O x y" using ‹P x y› by (rule part_implies_overlap)
  hence  "P (x ⊗ y) x" by (rule product_in_first_factor)
  thus "x ⊗ y = x" using ‹P x (x ⊗ y)› by (rule part_antisymmetry)
qed

lemma product_overlap: "P z x ⟹ O z y ⟹ O z (x ⊗ y)"
proof -
  assume "P z x"
  assume "O z y"
  with overlap_eq have "∃v. P v z ∧ P v y"..
  then obtain v where v: "P v z ∧ P v y"..
  hence "P v y"..
  from v have "P v z"..
  hence "P v x" using ‹P z x› by (rule part_transitivity)
  hence "P v x ∧ P v y" using ‹P v y›..
  hence "P v (x ⊗ y)" by (rule common_part_in_product)
  with ‹P v z› have "P v z ∧ P v (x ⊗ y)"..
  hence "∃v. P v z ∧ P v (x ⊗ y)"..
  with overlap_eq show "O z (x ⊗ y)"..
qed

lemma disjoint_from_second_factor: 
  "P x y ∧ ¬ O x (y ⊗ z) ⟹ ¬ O x z" 
proof -
  assume antecedent: "P x y ∧ ¬ O x (y ⊗ z)"
  hence "¬ O x (y ⊗ z)"..
  show "¬ O x z"
  proof
    from antecedent have "P x y"..
    moreover assume "O x z"
    ultimately have "O x (y ⊗ z)"
      by (rule product_overlap)
    with ‹¬ O x (y ⊗ z)› show "False"..
  qed
qed

lemma converse_product_overlap: 
  "O x y ⟹ O z (x ⊗ y) ⟹ O z y"
proof -
  assume "O x y"
  hence "P (x ⊗ y) y" by (rule product_in_second_factor)
  moreover assume "O z (x ⊗ y)"
  ultimately show "O z y"
    by (rule overlap_monotonicity)
qed

lemma part_product_in_whole_product:
  "O x y ⟹ P x v ∧ P y z ⟹ P (x ⊗ y) (v ⊗ z)"
proof -
  assume "O x y"
  assume "P x v ∧ P y z"
  have "∀w. P w (x ⊗ y) ⟶ P w (v ⊗ z)"
  proof
    fix w
    show "P w (x ⊗ y) ⟶ P w (v ⊗ z)"
    proof
      assume "P w (x ⊗ y)"
      with ‹O x y› have "P w x ∧ P w y"
        by (rule product_part_in_factors)
      have "P w v ∧ P w z"
      proof
        from ‹P w x ∧ P w y› have "P w x"..
        moreover from ‹P x v ∧ P y z› have "P x v"..
        ultimately show "P w v" by (rule part_transitivity)
      next
        from ‹P w x ∧ P w y› have "P w y"..
        moreover from ‹P x v ∧ P y z› have "P y z"..
        ultimately show "P w z" by (rule part_transitivity)
      qed     
      thus "P w (v ⊗ z)" by (rule common_part_in_product)
    qed
  qed
  hence "P (x ⊗ y) (x ⊗ y) ⟶ P (x ⊗ y) (v ⊗ z)"..
  moreover have "P (x ⊗ y) (x ⊗ y)" by (rule part_reflexivity)
  ultimately show "P (x ⊗ y) (v ⊗ z)"..
qed

lemma right_associated_product: "(∃w. P w x ∧ P w y ∧ P w z) ⟹
  (∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z))"
proof -
  assume antecedent: "(∃w. P w x ∧ P w y ∧ P w z)"
  then obtain w where w: "P w x ∧ P w y ∧ P w z"..
  hence "P w x"..
  from w have "P w y ∧ P w z"..
  hence "∃w. P w y ∧ P w z"..
  with overlap_eq have "O y z"..
  hence yz: "∀w. P w (y ⊗ z) ⟷ (P w y ∧ P w z)"
    by (rule product_character)
  hence "P w (y ⊗ z) ⟷ (P w y ∧ P w z)"..
  hence "P w (y ⊗ z)"
    using ‹P w y ∧ P w z›..
  with ‹P w x› have "P w x ∧ P w (y ⊗ z)"..
  hence "∃w. P w x ∧ P w (y ⊗ z)"..
  with overlap_eq have "O x (y ⊗ z)"..
  hence xyz: "∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ P w (y ⊗ z)"
    by (rule product_character)
  show "∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z)"
  proof
    fix w
    from yz have wyz: "P w (y ⊗ z) ⟷ (P w y ∧ P w z)"..
    moreover from xyz have 
      "P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ P w (y ⊗ z)"..
    ultimately show 
      "P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z)"
      by (rule subst)
  qed
qed

lemma left_associated_product: "(∃w. P w x ∧ P w y ∧ P w z) ⟹
  (∀w. P w ((x ⊗ y) ⊗ z) ⟷ (P w x ∧ P w y) ∧ P w z)"
proof -
  assume antecedent: "(∃w. P w x ∧ P w y ∧ P w z)"
  then obtain w where w: "P w x ∧ P w y ∧ P w z"..
  hence "P w y ∧ P w z"..
  hence "P w y"..
  have "P w z"
    using ‹P w y ∧ P w z›..
  from w have "P w x"..
  hence "P w x ∧ P w y"
    using ‹P w y›..
  hence "∃z. P z x ∧ P z y"..
  with overlap_eq have "O x y"..
  hence xy: "∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y)"
    by (rule product_character)
  hence "P w (x ⊗ y) ⟷ (P w x ∧ P w y)"..
  hence "P w (x ⊗ y)"
    using ‹P w x ∧ P w y›..
  hence "P w (x ⊗ y) ∧ P w z"
    using ‹P w z›..
  hence "∃w. P w (x ⊗ y) ∧ P w z"..
  with overlap_eq have "O (x ⊗ y) z"..
  hence xyz: "∀w. P w ((x ⊗ y) ⊗ z) ⟷ P w (x ⊗ y) ∧ P w z"
    by (rule product_character)
  show "∀w. P w ((x ⊗ y) ⊗ z) ⟷ (P w x ∧ P w y) ∧ P w z"
  proof
    fix v
    from xy have vxy: "P v (x ⊗ y) ⟷ (P v x ∧ P v y)"..
    moreover from xyz have 
      "P v ((x ⊗ y) ⊗ z) ⟷ P v (x ⊗ y) ∧ P v z"..
    ultimately show "P v ((x ⊗ y) ⊗ z) ⟷ (P v x ∧ P v y) ∧ P v z"
      by (rule subst)
  qed
qed

theorem product_associativity:
  "(∃w. P w x ∧ P w y ∧ P w z) ⟹ x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z"
proof -
  assume ante:"(∃w. P w x ∧ P w y ∧ P w z)"
  hence "(∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z))"
    by (rule right_associated_product)
  moreover from ante have 
    "(∀w. P w ((x ⊗ y) ⊗ z) ⟷ (P w x ∧ P w y) ∧ P w z)"
    by (rule left_associated_product)
  ultimately have "∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w ((x ⊗ y) ⊗ z)" 
    by simp
  with part_extensionality show "x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z"..
qed

end

subsection ‹ Differences  ›

text ‹ Some writers also add to closed mereology the axiom of difference closure.\footnote{See, for example,
\<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"masolo_atomicity_1999"› p. 238.} ›

locale CMD = CM +
  assumes difference_eq: 
    "x ⊖ y = (THE z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)"
  assumes difference_closure:
    "(∃w. P w x ∧ ¬ O w y) ⟹ (∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)"
begin

lemma difference_intro: 
  "(∀w. P w z ⟷ P w x ∧ ¬ O w y) ⟹ x ⊖ y = z"
proof -
  assume antecedent: "(∀w. P w z ⟷ P w x ∧ ¬ O w y)"
  hence "(THE z. ∀w. P w z ⟷ P w x ∧ ¬ O w y) = z"
  proof (rule the_equality)
    fix v
    assume v: "(∀w. P w v ⟷ P w x ∧ ¬ O w y)"
    have "∀w. P w v ⟷ P w z"
    proof
      fix w
      from antecedent have "P w z ⟷ P w x ∧ ¬ O w y"..
      moreover from v have "P w v ⟷ P w x ∧ ¬ O w y"..
      ultimately show "P w v ⟷ P w z" by (rule ssubst)
    qed
    with part_extensionality show "v = z"..
  qed
  with difference_eq show "x ⊖ y = z" by (rule ssubst)
qed

lemma difference_idempotence: "¬ O x y ⟹ (x ⊖ y) = x"
proof -
  assume "¬ O x y"
  hence "¬ O y x" by (rule disjoint_symmetry)
  have "∀w. P w x ⟷ P w x ∧ ¬ O w y"
  proof
    fix w
    show "P w x ⟷ P w x ∧ ¬ O w y"
    proof
      assume "P w x"
      hence "¬ O y w" using ‹¬ O y x›
        by (rule disjoint_demonotonicity)
      hence "¬ O w y" by (rule disjoint_symmetry)
      with ‹P w x› show "P w x ∧ ¬ O w y"..
    next
      assume "P w x ∧ ¬ O w y"
      thus "P w x"..
    qed
  qed
  thus "(x ⊖ y) = x" by (rule difference_intro)
qed

lemma difference_character: "(∃w. P w x ∧ ¬ O w y) ⟹ 
  (∀w. P w (x ⊖ y) ⟷ P w x ∧ ¬ O w y)"
proof -
  assume "∃w. P w x ∧ ¬ O w y"
  hence "∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y" by (rule difference_closure)
  then obtain z where z: "∀w. P w z ⟷ P w x ∧ ¬ O w y"..
  hence "(x ⊖ y) = z" by (rule difference_intro)
  thus "∀w. P w (x ⊖ y) ⟷ P w x ∧ ¬ O w y" using z by (rule ssubst)
qed

lemma difference_disjointness: 
  "(∃z. P z x ∧ ¬ O z y) ⟹ ¬ O y (x ⊖ y)"
proof -
  assume "∃z. P z x ∧ ¬ O z y"
  hence xmy: "∀w. P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)"
    by (rule difference_character)
  show "¬ O y (x ⊖ y)"
  proof
    assume "O y (x ⊖ y)"
    with overlap_eq have "∃v. P v y ∧ P v (x ⊖ y)"..
    then obtain v where v: "P v y ∧ P v (x ⊖ y)"..
    from xmy have "P v (x ⊖ y) ⟷ (P v x ∧ ¬ O v y)"..
    moreover from v have "P v (x ⊖ y)"..
    ultimately have "P v x ∧ ¬ O v y"..
    hence "¬ O v y"..
    moreover from v have "P v y"..
    hence "O v y" by (rule part_implies_overlap)
    ultimately show "False"..
  qed
qed

end

subsection ‹ The Universe ›

text ‹ Another closure condition sometimes considered is the existence of the universe.\footnote{
See, for example, \<^cite>‹"varzi_parts_1996"› p. 264 and \<^cite>‹"casati_parts_1999"› p. 45.}  ›

locale CMU = CM +
  assumes universe_eq: "u = (THE z. ∀w. P w z)" 
  assumes universe_closure: "∃y. ∀x. P x y"
begin

lemma universe_intro: "(∀w. P w z) ⟹ u = z"
proof -
  assume z: "∀w. P w z"
  hence "(THE z. ∀w. P w z) = z"
  proof (rule the_equality)
    fix v
    assume v: "∀w. P w v"
    have "∀w. P w v ⟷ P w z"
    proof
      fix w
      show "P w v ⟷ P w z"
      proof
        assume "P w v"
        from z show "P w z"..
      next
        assume "P w z"
        from v show "P w v"..
      qed
    qed
    with part_extensionality show "v = z"..
  qed
  thus "u = z" using universe_eq by (rule subst)
qed

lemma universe_character: "P x u"
proof -
  from universe_closure obtain y where y: "∀x. P x y"..
  hence "u = y" by (rule universe_intro)
  hence "∀x. P x u" using y by (rule ssubst)
  thus "P x u"..
qed

lemma "¬ PP u x"
proof
  assume "PP u x"
  hence "¬ P x u" by (rule proper_implies_not_part)
  thus "False" using universe_character..
qed

lemma product_universe_implies_factor_universe: 
  "O x y ⟹ x ⊗ y = u ⟹ x = u"
proof -
  assume "x ⊗ y = u"
  moreover assume "O x y"
  hence "P (x ⊗ y) x"
    by (rule product_in_first_factor)  
  ultimately have "P u x"
    by (rule subst)
  with universe_character show "x = u"
    by (rule part_antisymmetry)
qed

end

subsection ‹ Complements ›

text ‹ As is a condition ensuring the existence of complements.\footnote{See, for example, 
 \<^cite>‹"varzi_parts_1996"› p. 264 and \<^cite>‹"casati_parts_1999"› p. 45.} ›

locale CMC = CM +
  assumes complement_eq: "─x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
  assumes complement_closure: 
    "(∃w. ¬ O w x) ⟹ (∃z. ∀w. P w z ⟷ ¬ O w x)"
  assumes difference_eq: 
    "x ⊖ y = (THE z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)"
begin

lemma complement_intro:
  "(∀w. P w z ⟷ ¬ O w x) ⟹ ─x = z"
proof -
  assume antecedent: "∀w. P w z ⟷ ¬ O w x"
  hence "(THE z. ∀w. P w z ⟷ ¬ O w x) = z"
  proof (rule the_equality)
    fix v
    assume v: "∀w. P w v ⟷ ¬ O w x"
    have "∀w. P w v ⟷ P w z"
    proof
      fix w
      from antecedent have "P w z ⟷ ¬ O w x"..
      moreover from v have "P w v ⟷ ¬ O w x"..
      ultimately show "P w v ⟷ P w z" by (rule ssubst)
    qed
    with part_extensionality show "v = z"..
  qed
  with complement_eq show "─x = z" by (rule ssubst)
qed

lemma complement_character:
  "(∃w. ¬ O w x) ⟹ (∀w. P w (─x) ⟷ ¬ O w x)"
proof -
  assume "∃w. ¬ O w x"
  hence "(∃z. ∀w. P w z ⟷ ¬ O w x)" by (rule complement_closure)
  then obtain z where z: "∀w. P w z ⟷ ¬ O w x"..
  hence "─x = z" by (rule complement_intro)
  thus "∀w. P w (─x) ⟷ ¬ O w x"
    using z by (rule ssubst)
qed

lemma not_complement_part: "∃w. ¬ O w x ⟹ ¬ P x (─x)"
proof -
  assume "∃w. ¬ O w x"
  hence "∀w. P w (─x) ⟷ ¬ O w x"
    by (rule complement_character)
  hence "P x (─x) ⟷ ¬ O x x"..
  show "¬ P x (─x)"
  proof
    assume "P x (─x)"
    with ‹P x (─x) ⟷ ¬ O x x› have "¬ O x x"..
    thus "False" using overlap_reflexivity..
  qed
qed

lemma complement_part: "¬ O x y ⟹ P x (─y)"
proof -
  assume "¬ O x y"
  hence "∃z. ¬ O z y"..
  hence "∀w. P w (─y) ⟷ ¬ O w y"
    by (rule complement_character)
  hence "P x (─y) ⟷ ¬ O x y"..
  thus "P x (─y)" using ‹¬ O x y›..
qed

lemma complement_overlap: "¬ O x y ⟹ O x (─y)"
proof -
  assume "¬ O x y"
  hence "P x (─y)"
    by (rule complement_part)
  thus "O x (─y)"
    by (rule part_implies_overlap)
qed

lemma or_complement_overlap: "∀y. O y x ∨ O y (─x)"
proof
  fix y
  show "O y x ∨ O y (─x)"
  proof cases
    assume "O y x"
    thus "O y x ∨ O y (─x)"..
  next
    assume "¬ O y x"
    hence "O y (─x)"
      by (rule complement_overlap)
    thus "O y x ∨ O y (─x)"..
  qed
qed

lemma complement_disjointness: "∃v. ¬ O v x ⟹ ¬ O x (─x)"
proof -
  assume "∃v. ¬ O v x"
  hence w: "∀w. P w (─x) ⟷ ¬ O w x"
    by (rule complement_character)
  show "¬ O x (─x)"
  proof
    assume "O x (─x)"
    with overlap_eq have "∃v. P v x ∧ P v (─x)"..
    then obtain v where v: "P v x ∧ P v (─x)"..
    from w have "P v (─x) ⟷ ¬ O v x"..
    moreover from v have  "P v (─x)"..
    ultimately have "¬ O v x"..
    moreover from v have "P v x"..
    hence "O v x" by (rule part_implies_overlap)
    ultimately show "False"..
  qed
qed

lemma part_disjoint_from_complement:
  "∃v. ¬ O v x ⟹ P y x ⟹ ¬ O y (─x)"
proof
  assume "∃v. ¬ O v x"
  hence "¬ O x (─x)" by (rule complement_disjointness)
  assume "P y x"
  assume "O y (─x)"
  with overlap_eq have "∃v. P v y ∧ P v (─x)"..
  then obtain v where v: "P v y ∧ P v (─x)"..
  hence "P v y"..
  hence "P v x" using ‹P y x› by (rule part_transitivity)
  moreover from v have "P v (─x)"..
  ultimately have "P v x ∧ P v (─x)"..
  hence "∃v. P v x ∧ P v (─x)"..
  with overlap_eq have "O x (─x)"..
  with ‹¬ O x (─x)› show "False"..
qed

lemma product_complement_character: "(∃w. P w x ∧ ¬ O w y) ⟹ 
  (∀w. P w (x ⊗ (─y)) ⟷ (P w x ∧ (¬ O w y)))"
proof -
  assume antecedent: "∃w. P w x ∧ ¬ O w y"
  then obtain w where w: "P w x ∧ ¬ O w y"..
  hence "P w x"..
  moreover from w have "¬ O w y"..
  hence "P w (─y)" by (rule complement_part)  
  ultimately have  "P w x ∧ P w (─y)"..
  hence "∃w. P w x ∧ P w (─y)"..
  with overlap_eq have "O x (─y)"..
  hence prod: "(∀w. P w (x ⊗ (─y)) ⟷ (P w x ∧ P w (─y)))"
    by (rule product_character)
  show "∀w. P w (x ⊗ (─y)) ⟷ (P w x ∧ (¬ O w y))"
  proof
    fix v
    from w have "¬ O w y"..
    hence "∃w. ¬ O w y"..
    hence "∀w. P w (─y) ⟷ ¬ O w y"
      by (rule complement_character)
    hence "P v (─y) ⟷ ¬ O v y"..
    moreover have "P v (x ⊗ (─y)) ⟷ (P v x ∧ P v (─y))"
      using prod..
    ultimately show "P v (x ⊗ (─y)) ⟷ (P v x ∧ (¬ O v y))"
      by (rule subst)
  qed
qed

theorem difference_closure: "(∃w. P w x ∧ ¬ O w y) ⟹ 
  (∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)"
proof -
  assume "∃w. P w x ∧ ¬ O w y"
  hence "∀w. P w (x ⊗ (─y)) ⟷ P w x ∧ ¬ O w y"
    by (rule product_complement_character)
  thus "(∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)" by (rule exI)
qed

end

sublocale CMC ⊆ CMD
proof
  fix x y
  show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
    using difference_eq.
  show "(∃w. P w x ∧ ¬ O w y) ⟹ 
    (∃z. ∀w. P w z = (P w x ∧ ¬ O w y))"
    using difference_closure.
qed

corollary (in CMC) difference_is_product_of_complement:
  "(∃w. P w x ∧ ¬ O w y) ⟹ (x ⊖ y) = x ⊗ (─y)" 
proof -
  assume antecedent: "∃w. P w x ∧ ¬ O w y"
  hence "∀w. P w (x ⊗ (─y)) ⟷ P w x ∧ ¬ O w y"
    by (rule product_complement_character)
  thus "(x ⊖ y) = x ⊗ (─y)" by (rule difference_intro)
qed

text ‹ Universe and difference closure entail complement closure, since the difference of an individual
and the universe is the individual's complement. ›

locale CMUD = CMU + CMD +
  assumes complement_eq: "─x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
begin

lemma universe_difference:
  "(∃w. ¬ O w x) ⟹ (∀w. P w (u ⊖ x) ⟷ ¬ O w x)"
proof -
  assume "∃w. ¬ O w x"
  then obtain w where w: "¬ O w x"..
  from universe_character have "P w u".
  hence "P w u ∧ ¬ O w x" using ‹¬ O w x›..
  hence "∃z. P z u ∧ ¬ O z x"..
  hence ux: "∀w. P w (u ⊖ x) ⟷ (P w u ∧ ¬ O w x)"
    by (rule difference_character)
  show "∀w. P w (u ⊖ x) ⟷ ¬ O w x"
  proof
    fix w
    from ux have wux: "P w (u ⊖ x) ⟷ (P w u ∧ ¬ O w x)"..
    show "P w (u ⊖ x) ⟷ ¬ O w x"
    proof
      assume "P w (u ⊖ x)"
      with wux have "P w u ∧ ¬ O w x"..
      thus "¬ O w x"..
    next
      assume "¬ O w x"
      from universe_character have "P w u".
      hence "P w u ∧ ¬ O w x" using ‹¬ O w x›..
      with wux show "P w (u ⊖ x)"..
    qed
  qed
qed

theorem complement_closure: 
  "(∃w. ¬ O w x) ⟹ (∃z. ∀w. P w z ⟷ ¬ O w x)"
proof -
  assume "∃w. ¬ O w x"
  hence "∀w. P w (u ⊖ x) ⟷ ¬ O w x"
    by (rule universe_difference)
  thus "∃z. ∀w. P w z ⟷ ¬ O w x"..
qed

end

sublocale CMUD ⊆ CMC
proof
  fix x y
  show "─x = (THE z. ∀w. P w z ⟷ (¬ O w x))" 
    using complement_eq.
  show "∃w. ¬ O w x ⟹ ∃z. ∀w. P w z ⟷ (¬ O w x)" 
    using complement_closure.
  show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))" 
    using difference_eq.
qed

corollary (in CMUD) complement_universe_difference: 
  "(∃y. ¬ O y x) ⟹ ─x = (u ⊖ x)"
proof -
  assume "∃w. ¬ O w x"
  hence "∀w. P w (u ⊖ x) ⟷ ¬ O w x"
    by (rule universe_difference)
  thus " ─x = (u ⊖ x)"
    by (rule complement_intro)
qed

(*<*) end (*>*)