# Theory CEM

```section ‹ Closed Extensional Mereology ›

(*<*)
theory CEM
imports CM EM
begin
(*>*)

text ‹ Closed extensional mereology combines closed mereology with extensional mereology.\footnote{
See \<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"casati_parts_1999"› p. 43.} ›

locale CEM = CM + EM

text ‹ Likewise, closed minimal mereology combines closed mereology with minimal mereology.\footnote{
See \<^cite>‹"casati_parts_1999"› p. 43.} ›

locale CMM = CM + MM

text ‹ But famously closed minimal mereology and closed extensional mereology are the same theory,
because in closed minimal mereology product closure and weak supplementation entail strong
supplementation.\footnote{See \<^cite>‹"simons_parts:_1987"› p. 31 and \<^cite>‹"casati_parts_1999"› p. 44.} ›

sublocale CMM ⊆ CEM
proof
fix x y
show strong_supplementation: "¬ P x y ⟹ (∃ z. P z x ∧ ¬ O z y)"
proof -
assume "¬ P x y"
show "∃ z. P z x ∧ ¬ O z y"
proof cases
assume "O x y"
with ‹¬ P x y› have "¬ P x y ∧ O x y"..
hence "PP (x ⊗ y) x" by (rule nonpart_implies_proper_product)
hence "∃ z. P z x ∧ ¬ O z (x ⊗ y)" by (rule weak_supplementation)
then obtain z where z: "P z x ∧ ¬ O z (x ⊗ y)"..
hence "¬ O z y" by (rule disjoint_from_second_factor)
moreover from z have "P z x"..
hence  "P z x ∧ ¬ O z y"
using ‹¬ O z y›..
thus "∃ z. P z x ∧ ¬ O z y"..
next
assume "¬ O x y"
with part_reflexivity have "P x x ∧ ¬ O x y"..
thus "(∃ z. P z x ∧ ¬ O z y)"..
qed
qed
qed

sublocale CEM ⊆ CMM..

subsection ‹ Sums ›

context CEM
begin

lemma sum_intro:
"(∀ w. O w z ⟷ (O w x ∨ O w y)) ⟹ x ⊕ y = z"
proof -
assume sum: "∀ w. O w z ⟷ (O w x ∨ O w y)"
hence "(THE v. ∀ w. O w v ⟷ (O w x ∨ O w y)) = z"
proof (rule the_equality)
fix a
assume a: "∀ w. O w a ⟷ (O w x ∨ O w y)"
have "∀ w. O w a ⟷ O w z"
proof
fix w
from sum have "O w z ⟷ (O w x ∨ O w y)"..
moreover from a have "O w a ⟷ (O w x ∨ O w y)"..
ultimately show "O w a ⟷ O w z" by (rule ssubst)
qed
with overlap_extensionality show "a = z"..
qed
thus "x ⊕ y = z"
using sum_eq by (rule subst)
qed

lemma sum_idempotence: "x ⊕ x = x"
proof -
have "∀ w. O w x ⟷ (O w x ∨ O w x)"
proof
fix w
show "O w x ⟷ (O w x ∨ O w x)"
proof (rule iffI)
assume "O w x"
thus "O w x ∨ O w x"..
next
assume "O w x ∨ O w x"
thus "O w x" by (rule disjE)
qed
qed
thus "x ⊕ x = x" by (rule sum_intro)
qed

lemma part_sum_identity: "P y x ⟹ x ⊕ y = x"
proof -
assume "P y x"
have "∀ w. O w x ⟷ (O w x ∨ O w y)"
proof
fix w
show "O w x ⟷ (O w x ∨ O w y)"
proof
assume "O w x"
thus "O w x ∨ O w y"..
next
assume "O w x ∨ O w y"
thus "O w x"
proof
assume "O w x"
thus "O w x".
next
assume "O w y"
with ‹P y x› show "O w x"
by (rule overlap_monotonicity)
qed
qed
qed
thus "x ⊕ y = x" by (rule sum_intro)
qed

lemma sum_character: "∀ w. O w (x ⊕ y) ⟷ (O w x ∨ O w y)"
proof -
from sum_closure have "(∃ z. ∀ w. O w z ⟷ (O w x ∨ O w y))".
then obtain a where a: "∀ w. O w a ⟷ (O w x ∨ O w y)"..
hence "x ⊕ y = a" by (rule sum_intro)
thus "∀ w. O w (x ⊕ y) ⟷ (O w x ∨ O w y)"
using a by (rule ssubst)
qed

lemma sum_overlap: "O w (x ⊕ y) ⟷ (O w x ∨ O w y)"
using sum_character..

lemma sum_part_character:
"P w (x ⊕ y) ⟷ (∀ v. O v w ⟶ O v x ∨ O v y)"
proof
assume "P w (x ⊕ y)"
show "∀ v. O v w ⟶ O v x ∨ O v y"
proof
fix v
show "O v w ⟶ O v x ∨ O v y"
proof
assume "O v w"
with ‹P w (x ⊕ y)› have "O v (x ⊕ y)"
by (rule overlap_monotonicity)
with sum_overlap show "O v x ∨ O v y"..
qed
qed
next
assume right: "∀ v. O v w ⟶ O v x ∨ O v y"
have "∀ v. O v w ⟶ O v (x ⊕ y)"
proof
fix v
from right have "O v w ⟶ O v x ∨ O v y"..
with sum_overlap show "O v w ⟶ O v (x ⊕ y)"
by (rule ssubst)
qed
with part_overlap_eq show "P w (x ⊕ y)"..
qed

lemma sum_commutativity: "x ⊕ y = y ⊕ x"
proof -
from sum_character have "∀ w. O w (y ⊕ x) ⟷ O w y ∨ O w x".
hence "∀ w. O w (y ⊕ x) ⟷ O w x ∨ O w y" by metis
thus "x ⊕ y = y ⊕ x" by (rule sum_intro)
qed

lemma first_summand_overlap: "O z x ⟹ O z (x ⊕ y)"
proof -
assume "O z x"
hence "O z x ∨ O z y"..
with sum_overlap show "O z (x ⊕ y)"..
qed

lemma first_summand_disjointness: "¬ O z (x ⊕ y) ⟹ ¬ O z x"
proof -
assume "¬ O z (x ⊕ y)"
show "¬ O z x"
proof
assume "O z x"
hence "O z (x ⊕ y)" by (rule first_summand_overlap)
with ‹¬ O z (x ⊕ y)› show "False"..
qed
qed

lemma first_summand_in_sum: "P x (x ⊕ y)"
proof -
have "∀ w. O w x ⟶ O w (x ⊕ y)"
proof
fix w
show "O w x ⟶ O w (x ⊕ y)"
proof
assume "O w x"
thus "O w (x ⊕ y)"
by (rule first_summand_overlap)
qed
qed
with part_overlap_eq show "P x (x ⊕ y)"..
qed

lemma common_first_summand: "P x (x ⊕ y) ∧ P x (x ⊕ z)"
proof
from first_summand_in_sum show "P x (x ⊕ y)".
from first_summand_in_sum show "P x (x ⊕ z)".
qed

lemma common_first_summand_overlap: "O (x ⊕ y) (x ⊕ z)"
proof -
from first_summand_in_sum have "P x (x ⊕ y)".
moreover from first_summand_in_sum have "P x (x ⊕ z)".
ultimately have "P x (x ⊕ y) ∧ P x (x ⊕ z)"..
hence "∃ v. P v (x ⊕ y) ∧ P v (x ⊕ z)"..
with overlap_eq show ?thesis..
qed

lemma second_summand_overlap: "O z y ⟹ O z (x ⊕ y)"
proof -
assume "O z y"
from sum_character have "O z (x ⊕ y) ⟷ (O z x ∨ O z y)"..
moreover from ‹O z y› have "O z x ∨ O z y"..
ultimately show "O z (x ⊕ y)"..
qed

lemma second_summand_disjointness: "¬ O z (x ⊕ y) ⟹ ¬ O z y"
proof -
assume "¬ O z (x ⊕ y)"
show "¬ O z y"
proof
assume  "O z y"
hence "O z (x ⊕ y)"
by (rule second_summand_overlap)
with ‹¬ O z (x ⊕ y)› show False..
qed
qed

lemma second_summand_in_sum: "P y (x ⊕ y)"
proof -
have "∀ w. O w y ⟶ O w (x ⊕ y)"
proof
fix w
show "O w y ⟶ O w (x ⊕ y)"
proof
assume "O w y"
thus "O w (x ⊕ y)"
by (rule second_summand_overlap)
qed
qed
with part_overlap_eq show "P y (x ⊕ y)"..
qed

lemma second_summands_in_sums: "P y (x ⊕ y) ∧ P v (z ⊕ v)"
proof
show "P y (x ⊕ y)" using second_summand_in_sum.
show "P v (z ⊕ v)" using second_summand_in_sum.
qed

lemma disjoint_from_sum: "¬ O z (x ⊕ y) ⟷ ¬ O z x ∧ ¬ O z y"
proof -
from sum_character have "O z (x ⊕ y) ⟷ (O z x ∨ O z y)"..
thus ?thesis by simp
qed

lemma summands_part_implies_sum_part:
"P x z ∧ P y z ⟹ P (x ⊕ y) z"
proof -
assume antecedent: "P x z ∧ P y z"
have "∀ w. O w (x ⊕ y) ⟶ O w z"
proof
fix w
have w: "O w (x ⊕ y) ⟷ (O w x ∨ O w y)"
using sum_character..
show "O w (x ⊕ y) ⟶ O w z"
proof
assume "O w (x ⊕ y)"
with w have "O w x ∨ O w y"..
thus "O w z"
proof
from antecedent have "P x z"..
moreover assume "O w x"
ultimately show "O w z"
by (rule overlap_monotonicity)
next
from antecedent have "P y z"..
moreover assume "O w y"
ultimately show "O w z"
by (rule overlap_monotonicity)
qed
qed
qed
with part_overlap_eq show "P (x ⊕ y) z"..
qed

lemma sum_part_implies_summands_part:
"P (x ⊕ y) z ⟹ P x z ∧ P y z"
proof -
assume antecedent: "P (x ⊕ y) z"
show "P x z ∧ P y z"
proof
from first_summand_in_sum show "P x z"
using antecedent by (rule part_transitivity)
next
from second_summand_in_sum show "P y z"
using antecedent by (rule part_transitivity)
qed
qed

lemma in_second_summand: "P z (x ⊕ y) ∧ ¬ O z x ⟹ P z y"
proof -
assume antecedent: "P z (x ⊕ y) ∧ ¬ O z x"
hence "P z (x ⊕ y)"..
show "P z y"
proof (rule ccontr)
assume "¬ P z y"
hence "∃ v. P v z ∧ ¬ O v y"
by (rule strong_supplementation)
then obtain v where v: "P v z ∧ ¬ O v y"..
hence "¬ O v y"..
from v have "P v z"..
hence "P v (x ⊕ y)"
using ‹P z (x ⊕ y)› by (rule part_transitivity)
hence "O v (x ⊕ y)" by (rule part_implies_overlap)
from sum_character have "O v (x ⊕ y) ⟷ O v x ∨ O v y"..
hence "O v x ∨ O v y" using ‹O v (x ⊕ y)›..
thus "False"
proof (rule disjE)
from antecedent have "¬ O z x"..
moreover assume "O v x"
hence "O x v" by (rule overlap_symmetry)
with ‹P v z› have "O x z"
by (rule overlap_monotonicity)
hence "O z x" by (rule overlap_symmetry)
ultimately show "False"..
next
assume "O v y"
with ‹¬ O v y› show "False"..
qed
qed
qed

lemma disjoint_second_summands:
"P v (x ⊕ y) ∧ P v (x ⊕ z) ⟹ ¬ O y z ⟹ P v x"
proof -
assume antecedent: "P v (x ⊕ y) ∧ P v (x ⊕ z)"
hence "P v (x ⊕ z)"..
assume "¬ O y z"
show "P v x"
proof (rule ccontr)
assume "¬ P v x"
hence "∃ w. P w v ∧ ¬ O w x" by (rule strong_supplementation)
then obtain w where w: "P w v ∧ ¬ O w x"..
hence "¬ O w x"..
from w have "P w v"..
moreover from antecedent have "P v (x ⊕ z)"..
ultimately have "P w (x ⊕ z)" by (rule part_transitivity)
hence "P w (x ⊕ z) ∧ ¬ O w x" using ‹¬ O w x›..
hence "P w z" by (rule in_second_summand)
from antecedent have "P v (x ⊕ y)"..
with ‹P w v› have "P w (x ⊕ y)" by (rule part_transitivity)
hence "P w (x ⊕ y) ∧ ¬ O w x" using ‹¬ O w x›..
hence "P w y" by (rule in_second_summand)
hence "P w y ∧ P w z" using ‹P w z›..
hence "∃ w. P w y ∧ P w z"..
with overlap_eq have "O y z"..
with ‹¬ O y z› show "False"..
qed
qed

lemma right_associated_sum:
"O w (x ⊕ (y ⊕ z)) ⟷ O w x ∨ (O w y ∨ O w z)"
proof -
from sum_character have "O w (y ⊕ z) ⟷ O w y ∨ O w z"..
moreover from sum_character have
"O w (x ⊕ (y ⊕ z)) ⟷ (O w x ∨ O w (y ⊕ z))"..
ultimately show ?thesis
by (rule subst)
qed

lemma left_associated_sum:
"O w ((x ⊕ y) ⊕ z) ⟷ (O w x ∨ O w y) ∨ O w z"
proof -
from sum_character have "O w (x ⊕ y) ⟷ (O w x ∨ O w y)"..
moreover from sum_character have
"O w ((x ⊕ y) ⊕ z) ⟷ O w (x ⊕ y) ∨ O w z"..
ultimately show ?thesis
by (rule subst)
qed

theorem sum_associativity: "x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
proof -
have  "∀ w. O w (x ⊕ (y ⊕ z)) ⟷ O w ((x ⊕ y) ⊕ z)"
proof
fix w
have "O w (x ⊕ (y ⊕ z)) ⟷ (O w x ∨ O w y) ∨ O w z"
using right_associated_sum by simp
with left_associated_sum show
"O w (x ⊕ (y ⊕ z)) ⟷ O w ((x ⊕ y) ⊕ z)" by (rule ssubst)
qed
with overlap_extensionality show "x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"..
qed

subsection ‹ Distributivity ›

text ‹ The proofs in this section are adapted from \<^cite>‹"pietruszczak_metamereology_2018"› pp. 102-4.  ›

lemma common_summand_in_product: "P x ((x ⊕ y) ⊗ (x ⊕ z))"
using common_first_summand by (rule common_part_in_product)

lemma product_in_first_summand:
"¬ O y z ⟹ P ((x ⊕ y) ⊗ (x ⊕ z)) x"
proof -
assume "¬ O y z"
have "∀ v. P v ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ P v x"
proof
fix v
show "P v ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ P v x"
proof
assume "P v ((x ⊕ y) ⊗ (x ⊕ z))"
with common_first_summand_overlap have
"P v (x ⊕ y) ∧ P v (x ⊕ z)" by (rule product_part_in_factors)
thus "P v x" using ‹¬ O y z›  by (rule disjoint_second_summands)
qed
qed
hence "P ((x ⊕ y) ⊗ (x ⊕ z)) ((x ⊕ y) ⊗ (x ⊕ z)) ⟶
P ((x ⊕ y) ⊗ (x ⊕ z)) x"..
thus "P ((x ⊕ y) ⊗ (x ⊕ z)) x" using part_reflexivity..
qed

lemma product_is_first_summand:
"¬ O y z ⟹ (x ⊕ y) ⊗ (x ⊕ z) = x"
proof -
assume "¬ O y z"
hence "P ((x ⊕ y) ⊗ (x ⊕ z)) x"
by (rule product_in_first_summand)
thus "(x ⊕ y) ⊗ (x ⊕ z) = x"
using common_summand_in_product
by (rule part_antisymmetry)
qed

lemma sum_over_product_left: "O y z ⟹ P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))"
proof -
assume "O y z"
hence "P (y ⊗ z) ((x ⊕ y) ⊗ (x ⊕ z))" using second_summands_in_sums
by (rule part_product_in_whole_product)
with common_summand_in_product have
"P x ((x ⊕ y) ⊗ (x ⊕ z)) ∧ P (y ⊗ z) ((x ⊕ y) ⊗ (x ⊕ z))"..
thus "P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))"
by (rule summands_part_implies_sum_part)
qed

lemma sum_over_product_right:
"O y z ⟹ P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
proof -
assume "O y z"
show "P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
proof (rule ccontr)
assume "¬ P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
hence "∃ v. P v ((x ⊕ y) ⊗ (x ⊕ z)) ∧ ¬ O v (x ⊕ (y ⊗ z))"
by (rule strong_supplementation)
then obtain v where v:
"P v ((x ⊕ y) ⊗ (x ⊕ z)) ∧ ¬ O v (x ⊕ (y ⊗ z))"..
hence " ¬ O v (x ⊕ (y ⊗ z))"..
with disjoint_from_sum have vd: "¬ O v x ∧ ¬ O v (y ⊗ z)"..
hence "¬ O v (y ⊗ z)"..
from vd have "¬ O v x"..
from v have "P v ((x ⊕ y) ⊗ (x ⊕ z))"..
with common_first_summand_overlap have
vs: "P v (x ⊕ y) ∧ P v (x ⊕ z)" by (rule product_part_in_factors)
hence "P v (x ⊕ y)"..
hence "P v (x ⊕ y) ∧ ¬ O v x" using ‹¬ O v x›..
hence "P v y" by (rule in_second_summand)
moreover from vs have "P v (x ⊕ z)"..
hence "P v (x ⊕ z) ∧ ¬ O v x" using ‹¬ O v x›..
hence "P v z" by (rule in_second_summand)
ultimately have "P v y ∧ P v z"..
hence "P v (y ⊗ z)" by (rule common_part_in_product)
hence "O v (y ⊗ z)" by (rule part_implies_overlap)
with ‹¬ O v (y ⊗ z)› show "False"..
qed
qed

text ‹ Sums distribute over products. ›

theorem sum_over_product:
"O y z ⟹ x ⊕ (y ⊗ z) = (x ⊕ y) ⊗ (x ⊕ z)"
proof -
assume "O y z"
hence "P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))"
by (rule sum_over_product_left)
moreover have "P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
using ‹O y z› by (rule sum_over_product_right)
ultimately show "x ⊕ (y ⊗ z) = (x ⊕ y) ⊗ (x ⊕ z)"
by (rule part_antisymmetry)
qed

lemma product_in_factor_by_sum:
"O x y ⟹ P (x ⊗ y) (x ⊗ (y ⊕ z))"
proof -
assume "O x y"
hence "P (x ⊗ y) x"
by (rule product_in_first_factor)
moreover have "P (x ⊗ y) y"
using ‹O x y› by (rule product_in_second_factor)
hence "P (x ⊗ y) (y ⊕ z)"
using first_summand_in_sum by (rule part_transitivity)
with ‹P (x ⊗ y) x› have "P (x ⊗ y) x ∧ P (x ⊗ y) (y ⊕ z)"..
thus "P (x ⊗ y) (x ⊗ (y ⊕ z))"
by (rule common_part_in_product)
qed

lemma product_of_first_summand:
"O x y ⟹ ¬ O x z ⟹ P (x ⊗ (y ⊕ z)) (x ⊗ y)"
proof -
assume "O x y"
hence "O x (y ⊕ z)"
by (rule first_summand_overlap)
assume "¬ O x z"
show "P (x ⊗ (y ⊕ z)) (x ⊗ y)"
proof (rule ccontr)
assume "¬ P (x ⊗ (y ⊕ z)) (x ⊗ y)"
hence "∃ v. P v (x ⊗ (y ⊕ z)) ∧ ¬ O v (x ⊗ y)"
by (rule strong_supplementation)
then obtain v where v: "P v (x ⊗ (y ⊕ z)) ∧ ¬ O v (x ⊗ y)"..
hence "P v (x ⊗ (y ⊕ z))"..
with ‹O x (y ⊕ z)› have "P v x ∧ P v (y ⊕ z)"
by (rule product_part_in_factors)
hence "P v x"..
moreover from v have "¬ O v (x ⊗ y)"..
ultimately have  "P v x ∧ ¬ O v (x ⊗ y)"..
hence "¬ O v y" by (rule disjoint_from_second_factor)
from ‹P v x ∧ P v (y ⊕ z)› have "P v (y ⊕ z)"..
hence "P v (y ⊕ z) ∧ ¬ O v y" using ‹¬ O v y›..
hence "P v z" by (rule in_second_summand)
with ‹P v x› have "P v x ∧ P v z"..
hence "∃ v. P v x ∧ P v z"..
with overlap_eq have "O x z"..
with ‹¬ O x z› show "False"..
qed
qed

theorem disjoint_product_over_sum:
"O x y ⟹ ¬ O x z ⟹ x ⊗ (y ⊕ z) = x ⊗ y"
proof -
assume "O x y"
moreover assume "¬ O x z"
ultimately have "P (x ⊗ (y ⊕ z)) (x ⊗ y)"
by (rule product_of_first_summand)
moreover have "P (x ⊗ y)(x ⊗ (y ⊕ z))"
using ‹O x y› by (rule product_in_factor_by_sum)
ultimately show "x ⊗ (y ⊕ z) = x ⊗ y"
by (rule part_antisymmetry)
qed

lemma product_over_sum_left:
"O x y ∧ O x z ⟹ P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
proof -
assume "O x y ∧ O x z"
hence "O x y"..
hence "O x (y ⊕ z)" by (rule first_summand_overlap)
show "P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
proof (rule ccontr)
assume "¬ P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
hence "∃ v. P v (x ⊗ (y ⊕ z)) ∧ ¬ O v ((x ⊗ y) ⊕ (x ⊗ z))"
by (rule strong_supplementation)
then obtain v where v:
"P v (x ⊗ (y ⊕ z)) ∧ ¬ O v ((x ⊗ y) ⊕ (x ⊗ z))"..
hence "¬ O v ((x ⊗ y) ⊕ (x ⊗ z))"..
with disjoint_from_sum have oxyz:
"¬ O v (x ⊗ y) ∧ ¬ O v (x ⊗ z)"..
from v have "P v (x ⊗ (y ⊕ z))"..
with ‹O x (y ⊕ z)› have pxyz: "P v x ∧ P v (y ⊕ z)"
by (rule product_part_in_factors)
hence "P v x"..
moreover from oxyz have "¬ O v (x ⊗ y)"..
ultimately have "P v x ∧ ¬ O v (x ⊗ y)"..
hence "¬ O v y" by (rule disjoint_from_second_factor)
from oxyz have "¬ O v (x ⊗ z)"..
with ‹P v x› have "P v x ∧ ¬ O v (x ⊗ z)"..
hence "¬ O v z" by (rule disjoint_from_second_factor)
with ‹¬ O v y› have "¬ O v y ∧ ¬ O v z"..
with disjoint_from_sum have "¬ O v (y ⊕ z)"..
from pxyz have "P v (y ⊕ z)"..
hence "O v (y ⊕ z)" by (rule part_implies_overlap)
with ‹¬ O v (y ⊕ z)› show "False"..
qed
qed

lemma product_over_sum_right:
"O x y ∧ O x z ⟹ P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))"
proof -
assume antecedent: "O x y ∧ O x z"
have "P (x ⊗ y) (x ⊗ (y ⊕ z)) ∧ P (x ⊗ z) (x ⊗ (y ⊕ z))"
proof
from antecedent have "O x y"..
thus "P (x ⊗ y) (x ⊗ (y ⊕ z))"
by (rule  product_in_factor_by_sum)
next
from antecedent have "O x z"..
hence "P (x ⊗ z) (x ⊗ (z ⊕ y))"
by (rule  product_in_factor_by_sum)
with sum_commutativity show "P (x ⊗ z) (x ⊗ (y ⊕ z))"
by (rule subst)
qed
thus "P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))"
by (rule summands_part_implies_sum_part)
qed

theorem product_over_sum:
"O x y ∧ O x z ⟹ x ⊗ (y ⊕ z) = (x ⊗ y) ⊕ (x ⊗ z)"
proof -
assume antecedent: "O x y ∧ O x z"
hence "P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
by (rule product_over_sum_left)
moreover have "P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))"
using antecedent by (rule product_over_sum_right)
ultimately show "x ⊗ (y ⊕ z) = (x ⊗ y) ⊕ (x ⊗ z)"
by (rule part_antisymmetry)
qed

lemma joint_identical_sums:
"v ⊕ w = x ⊕ y ⟹ O x v ∧ O x w ⟹ ((x ⊗ v) ⊕ (x ⊗ w)) = x"
proof -
assume "v ⊕ w = x ⊕ y"
moreover assume "O x v ∧ O x w"
hence "x ⊗ (v ⊕ w) = x ⊗ v ⊕ x ⊗ w"
by (rule product_over_sum)
ultimately have "x ⊗ (x ⊕ y) = x ⊗ v ⊕ x ⊗ w" by (rule subst)
moreover have "(x ⊗ (x ⊕ y)) = x" using first_summand_in_sum
by (rule part_product_identity)
ultimately show "((x ⊗ v) ⊕ (x ⊗ w)) = x" by (rule subst)
qed

lemma disjoint_identical_sums:
"v ⊕ w = x ⊕ y ⟹ ¬ O y v ∧ ¬ O w x ⟹ x = v ∧ y = w"
proof -
assume identical: "v ⊕ w = x ⊕ y"
assume disjoint: "¬ O y v ∧ ¬ O w x"
show "x = v ∧ y = w"
proof
from disjoint have "¬ O y v"..
hence "(x ⊕ y) ⊗ (x ⊕ v) = x"
by (rule product_is_first_summand)
with identical have "(v ⊕ w) ⊗ (x ⊕ v) = x"
by (rule ssubst)
moreover from disjoint have "¬ O w x"..
hence "(v ⊕ w) ⊗ (v ⊕ x) = v"
by (rule product_is_first_summand)
with sum_commutativity have "(v ⊕ w) ⊗ (x ⊕ v) = v"
by (rule subst)
ultimately show "x = v" by (rule subst)
next
from disjoint have "¬ O w x"..
hence "(y ⊕ w) ⊗ (y ⊕ x) = y"
by (rule product_is_first_summand)
moreover from disjoint have "¬ O y v"..
hence "(w ⊕ y) ⊗ (w ⊕ v) = w"
by (rule product_is_first_summand)
with sum_commutativity have "(w ⊕ y) ⊗ (v ⊕ w) = w"
by (rule subst)
with identical have "(w ⊕ y) ⊗ (x ⊕ y) = w"
by (rule subst)
with sum_commutativity have "(w ⊕ y) ⊗ (y ⊕ x) = w"
by (rule subst)
with sum_commutativity have "(y ⊕ w) ⊗ (y ⊕ x) = w"
by (rule subst)
ultimately show "y = w"
by (rule subst)
qed
qed

end

subsection ‹ Differences ›

locale CEMD = CEM + CMD
begin

lemma plus_minus: "PP y x ⟹ y ⊕ (x ⊖ y) = x"
proof -
assume "PP y x"
hence "∃ z. P z x ∧ ¬ O z y" by (rule weak_supplementation)
hence xmy:"∀ w. P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)"
by (rule difference_character)
have "∀ w. O w x ⟷ (O w y ∨ O w (x ⊖ y))"
proof
fix w
from xmy have w: "P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)"..
show "O w x ⟷ (O w y ∨ O w (x ⊖ y))"
proof
assume "O w x"
with overlap_eq have "∃ v. P v w ∧ P v x"..
then obtain v where v: "P v w ∧ P v x"..
hence "P v w"..
from v have "P v x"..
show "O w y ∨ O w (x ⊖ y)"
proof cases
assume "O v y"
hence "O y v" by (rule overlap_symmetry)
with ‹P v w› have "O y w" by (rule overlap_monotonicity)
hence "O w y" by (rule overlap_symmetry)
thus "O w y ∨ O w (x ⊖ y)"..
next
from xmy have "P v (x ⊖ y) ⟷ (P v x ∧ ¬ O v y)"..
moreover assume "¬ O v y"
with ‹P v x› have  "P v x ∧ ¬ O v y"..
ultimately have "P v (x ⊖ y)"..
with ‹P v w› have "P v w ∧ P v (x ⊖ y)"..
hence "∃ v. P v w ∧ P v (x ⊖ y)"..
with overlap_eq have "O w (x ⊖ y)"..
thus "O w y ∨ O w (x ⊖ y)"..
qed
next
assume "O w y ∨ O w (x ⊖ y)"
thus "O w x"
proof
from ‹PP y x› have "P y x"
by (rule proper_implies_part)
moreover assume "O w y"
ultimately show "O w x"
by (rule overlap_monotonicity)
next
assume "O w (x ⊖ y)"
with overlap_eq have "∃ v. P v w ∧ P v (x ⊖ y)"..
then obtain v where v: "P v w ∧ P v (x ⊖ y)"..
hence "P v w"..
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 "P v x"..
with ‹P v w› have "P v w ∧ P v x"..
hence "∃ v. P v w ∧ P v x"..
with overlap_eq show "O w x"..
qed
qed
qed
thus "y ⊕ (x ⊖ y) = x"
by (rule sum_intro)
qed

end

subsection ‹ The Universe ›

locale CEMU = CEM + CMU
begin

lemma something_disjoint: "x ≠ u ⟹ (∃ v. ¬ O v x)"
proof -
assume "x ≠ u"
with universe_character have "P x u ∧ x ≠ u"..
with nip_eq have "PP x u"..
hence "∃ v. P v u ∧ ¬ O v x"
by (rule weak_supplementation)
then obtain v where "P v u ∧ ¬ O v x"..
hence "¬ O v x"..
thus "∃ v. ¬ O v x"..
qed

lemma overlaps_universe: "O x u"
proof -
from universe_character have "P x u".
thus "O x u" by (rule part_implies_overlap)
qed

lemma universe_absorbing: "x ⊕ u = u"
proof -
from universe_character have "P (x ⊕ u) u".
thus "x ⊕ u = u" using second_summand_in_sum
by (rule part_antisymmetry)
qed

lemma second_summand_not_universe: "x ⊕ y ≠ u ⟹ y ≠ u"
proof -
assume antecedent: "x ⊕ y ≠ u"
show "y ≠ u"
proof
assume "y = u"
hence "x ⊕ u ≠ u" using antecedent by (rule subst)
thus "False" using universe_absorbing..
qed
qed

lemma first_summand_not_universe: "x ⊕ y ≠ u ⟹ x ≠ u"
proof -
assume "x ⊕ y ≠ u"
with sum_commutativity have "y ⊕ x ≠ u" by (rule subst)
thus "x ≠ u" by (rule second_summand_not_universe)
qed

end

subsection ‹ Complements ›

locale CEMC = CEM + CMC +
assumes universe_eq: "u = (THE x. ∀ y. P y x)"
begin

lemma complement_sum_character: "∀ y. P y (x ⊕ (─x))"
proof
fix y
have "∀ v. O v y ⟶ O v x ∨ O v (─x)"
proof
fix v
show "O v y ⟶ O v x ∨ O v (─x)"
proof
assume "O v y"
show "O v x ∨ O v (─x)"
using or_complement_overlap..
qed
qed
with sum_part_character show "P y (x ⊕ (─x))"..
qed

lemma universe_closure: "∃ x. ∀ y. P y x"
using complement_sum_character by (rule exI)

end

sublocale CEMC ⊆ CEMU
proof
show "u = (THE z. ∀w. P w z)" using universe_eq.
show "∃ x. ∀ y. P y x" using universe_closure.
qed

sublocale CEMC ⊆ CEMD
proof
qed

context CEMC
begin

corollary universe_is_complement_sum: "u = x ⊕ (─x)"
using complement_sum_character by (rule universe_intro)

lemma strong_complement_character:
"x ≠ u ⟹ (∀ v. P v (─x) ⟷ ¬ O v x)"
proof -
assume "x ≠ u"
hence "∃ v. ¬ O v x" by (rule something_disjoint)
thus "∀ v. P v (─x) ⟷ ¬ O v x" by (rule complement_character)
qed

lemma complement_part_not_part: "x ≠ u ⟹ P y (─x) ⟹ ¬ P y x"
proof -
assume "x ≠ u"
hence "∀ w. P w (─x) ⟷ ¬ O w x"
by (rule strong_complement_character)
hence y: "P y (─x) ⟷ ¬ O y x"..
moreover assume "P y (─x)"
ultimately have "¬ O y x"..
thus "¬ P y x"
by (rule disjoint_implies_not_part)
qed

lemma complement_involution: "x ≠ u ⟹ x = ─(─x)"
proof -
assume "x ≠ u"
have "¬ P u x"
proof
assume "P u x"
with universe_character have "x = u"
by (rule part_antisymmetry)
with ‹x ≠ u› show "False"..
qed
hence "∃ v. P v u ∧ ¬ O v x"
by (rule strong_supplementation)
then obtain v where v: "P v u ∧ ¬ O v x"..
hence "¬ O v x"..
hence "∃ v. ¬ O v x"..
hence notx: "∀ w. P w (─x) ⟷ ¬ O w x"
by (rule complement_character)
have "─x ≠ u"
proof
assume "─x = u"
hence "∀ w. P w u ⟷ ¬ O w x" using notx by (rule subst)
hence "P x u ⟷ ¬ O x x"..
hence "¬ O x x" using universe_character..
thus "False" using overlap_reflexivity..
qed
have "¬ P u (─x)"
proof
assume "P u (─x)"
with universe_character have "─x = u"
by (rule part_antisymmetry)
with ‹─x ≠ u› show "False"..
qed
hence "∃ v. P v u ∧ ¬ O v (─x)"
by (rule strong_supplementation)
then obtain w where w: "P w u ∧ ¬ O w (─x)"..
hence "¬ O w (─x)"..
hence "∃ v. ¬ O v (─x)"..
hence notnotx: "∀ w. P w (─(─x)) ⟷ ¬ O w (─x)"
by (rule complement_character)
hence "P x (─(─x)) ⟷ ¬ O x (─x)"..
moreover have "¬ O x (─x)"
proof
assume "O x (─x)"
with overlap_eq have "∃ s. P s x ∧ P s (─x)"..
then obtain s where s: "P s x ∧ P s (─x)"..
hence "P s x"..
hence "O s x" by (rule part_implies_overlap)
from notx have "P s (─x) ⟷ ¬ O s x"..
moreover from s have "P s (─x)"..
ultimately have "¬ O s x"..
thus "False" using ‹O s x›..
qed
ultimately have "P x (─(─x))"..
moreover have "P (─(─x)) x"
proof (rule ccontr)
assume "¬ P (─(─x)) x"
hence "∃ s. P s (─(─x)) ∧ ¬ O s x"
by (rule strong_supplementation)
then obtain s where s: "P s (─(─x)) ∧ ¬ O s x"..
hence "¬ O s x"..
from notnotx have "P s (─(─x)) ⟷ (¬ O s (─x))"..
moreover from s have "P s (─(─x))"..
ultimately have "¬ O s (─x)"..
from or_complement_overlap have "O s x ∨ O s (─x)"..
thus "False"
proof
assume "O s x"
with ‹¬ O s x› show "False"..
next
assume "O s (─x)"
with ‹¬ O s (─x )› show "False"..
qed
qed
ultimately show "x = ─(─x)"
by (rule part_antisymmetry)
qed

lemma part_complement_reversal: "y ≠ u ⟹ P x y ⟹ P (─y) (─x)"
proof -
assume "y ≠ u"
hence ny: "∀ w. P w (─y) ⟷ ¬ O w y"
by (rule strong_complement_character)
assume "P x y"
have "x ≠ u"
proof
assume "x = u"
hence "P u y" using ‹P x y› by (rule subst)
with universe_character have "y = u"
by (rule part_antisymmetry)
with ‹y ≠ u› show "False"..
qed
hence "∀ w. P w (─x) ⟷ ¬ O w x"
by (rule strong_complement_character)
hence "P (─y) (─x) ⟷ ¬ O (─y) x"..
moreover have "¬ O (─y) x"
proof
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)"..
from ny have "P v (─y) ⟷ ¬ O v y"..
hence "¬ O v y" using ‹P v (─y)›..
moreover from v have "P v x"..
hence "P v y" using ‹P x y›
by (rule part_transitivity)
hence "O v y"
by (rule part_implies_overlap)
ultimately show "False"..
qed
ultimately show "P (─y) (─x)"..
qed

lemma complements_overlap: "x ⊕ y ≠ u ⟹ O(─x)(─y)"
proof -
assume "x ⊕ y ≠ u"
hence "∃ z. ¬ O z (x ⊕ y)"
by (rule something_disjoint)
then obtain z where z:"¬ O z (x ⊕ y)"..
hence "¬ O z x" by (rule first_summand_disjointness)
hence "P z (─x)" by (rule complement_part)
moreover from z have "¬ O z y"
by (rule second_summand_disjointness)
hence "P z (─y)" by (rule complement_part)
ultimately show "O(─x)(─y)"
by (rule overlap_intro)
qed

lemma sum_complement_in_complement_product:
"x ⊕ y ≠ u ⟹ P(─(x ⊕ y))(─x ⊗ ─y)"
proof -
assume "x ⊕ y ≠ u"
hence "O (─x) (─y)"
by (rule complements_overlap)
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) ∧ P (─(x ⊕ y))(─y)"
proof
show "P (─(x ⊕ y))(─x)" using ‹x ⊕ y ≠ u› first_summand_in_sum
by (rule part_complement_reversal)
next
show  "P (─(x ⊕ y))(─y)" using ‹x ⊕ y ≠ u› second_summand_in_sum
by (rule part_complement_reversal)
qed
ultimately show "P (─(x ⊕ y))(─x ⊗ ─y)"..
qed

lemma complement_product_in_sum_complement:
"x ⊕ y ≠ u ⟹ P(─x ⊗ ─y)(─(x ⊕ y))"
proof -
assume "x ⊕ y ≠ u"
hence "∀w. P w (─(x ⊕ y)) ⟷ ¬ O w (x ⊕ y)"
by (rule strong_complement_character)
hence "P (─x ⊗ ─y) (─(x ⊕ y)) ⟷ (¬ O (─x ⊗ ─y) (x ⊕ y))"..
moreover have "¬ O (─x ⊗ ─y) (x ⊕ y)"
proof
have "O(─x)(─y)" using ‹x ⊕ y ≠ u› by (rule complements_overlap)
hence p: "∀ v. P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))"
by (rule product_character)
have "O(─x ⊗ ─y)(x ⊕ y) ⟷ (O(─x ⊗ ─y) x ∨ O(─x ⊗ ─y)y)"
using sum_character..
moreover assume "O (─x ⊗ ─y)(x ⊕ y)"
ultimately have "O (─x ⊗ ─y) x ∨ O (─x ⊗ ─y) y"..
thus "False"
proof
assume "O (─x ⊗ ─y) x"
with overlap_eq have "∃ v. P v (─x ⊗ ─y) ∧ P v x"..
then obtain v where v: "P v (─x ⊗ ─y) ∧ P v x"..
hence "P v (─x ⊗ ─y)"..
from p have "P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))"..
hence "P v (─x) ∧ P v (─y)" using ‹P v (─x ⊗ ─y)›..
hence "P v (─x)"..
have "x ≠ u" using ‹x ⊕ y ≠ u›
by (rule first_summand_not_universe)
hence "∀w. P w (─x) ⟷ ¬ O w x"
by (rule strong_complement_character)
hence "P v (─x) ⟷ ¬ O v x"..
hence "¬ O v x" using ‹P v (─x)›..
moreover from v have "P v x"..
hence "O v x" by (rule part_implies_overlap)
ultimately show "False"..
next
assume "O (─x ⊗ ─y) y"
with overlap_eq have "∃ v. P v (─x ⊗ ─y) ∧ P v y"..
then obtain v where v: "P v (─x ⊗ ─y) ∧ P v y"..
hence "P v (─x ⊗ ─y)"..
from p have "P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))"..
hence "P v (─x) ∧ P v (─y)" using ‹P v (─x ⊗ ─y)›..
hence "P v (─y)"..
have "y ≠ u" using ‹x ⊕ y ≠ u›
by (rule second_summand_not_universe)
hence "∀w. P w (─y) ⟷ ¬ O w y"
by (rule strong_complement_character)
hence "P v (─y) ⟷ ¬ O v y"..
hence "¬ O v y" using ‹P v (─y)›..
moreover from v have "P v y"..
hence "O v y" by (rule part_implies_overlap)
ultimately show "False"..
qed
qed
ultimately show "P (─x ⊗ ─y) (─(x ⊕ y))"..
qed

theorem sum_complement_is_complements_product:
"x ⊕ y ≠ u ⟹ ─(x ⊕ y) = (─x ⊗ ─y)"
proof -
assume "x ⊕ y ≠ u"
show "─(x ⊕ y) = (─x ⊗ ─y)"
proof (rule part_antisymmetry)
show "P (─ (x ⊕ y)) (─ x ⊗ ─ y)" using  ‹x ⊕ y ≠ u›
by (rule sum_complement_in_complement_product)
show "P (─ x ⊗ ─ y) (─ (x ⊕ y))" using ‹x ⊕ y ≠ u›
by (rule complement_product_in_sum_complement)
qed
qed

lemma complement_sum_in_product_complement:
"O x y ⟹ x ≠ u ⟹ y ≠ u ⟹ P ((─x) ⊕ (─y))(─(x ⊗ y))"
proof -
assume "O x y"
assume "x ≠ u"
assume "y ≠ u"
have "x ⊗ y ≠ u"
proof
assume "x ⊗ y = u"
with ‹O x y› have "x = u"
by (rule product_universe_implies_factor_universe)
with ‹x ≠ u› show "False"..
qed
hence notxty: "∀ w. P w (─(x ⊗ y)) ⟷ ¬ O w (x ⊗ y)"
by (rule strong_complement_character)
hence "P((─x)⊕(─y))(─(x ⊗ y)) ⟷ ¬O((─x)⊕(─y))(x ⊗ y)"..
moreover have "¬ O ((─x) ⊕ (─y)) (x ⊗ y)"
proof
from sum_character have
"∀ w. O w ((─x) ⊕ (─y)) ⟷ (O w (─x) ∨ O w (─y))".
hence "O(x ⊗ y)((─x)⊕(─y)) ⟷ (O(x ⊗ y)(─x) ∨ O(x ⊗ y)(─y))"..
moreover assume "O ((─x) ⊕ (─y)) (x ⊗ y)"
hence "O (x ⊗ y) ((─x) ⊕ (─y))" by (rule overlap_symmetry)
ultimately have "O (x ⊗ y) (─x) ∨ O (x ⊗ y) (─y)"..
thus False
proof
assume "O (x ⊗ y)(─x)"
with overlap_eq have "∃ v. P v (x ⊗ y) ∧ P v (─x)"..
then obtain v where v: "P v (x ⊗ y) ∧ P v (─x)"..
hence "P v (─x)"..
with ‹x ≠ u› have "¬ P v x"
by (rule complement_part_not_part)
moreover from v have "P v (x ⊗ y)"..
with ‹O x y› have "P v x" by (rule product_part_in_first_factor)
ultimately show "False"..
next
assume "O (x ⊗ y) (─y)"
with overlap_eq have "∃ v. P v (x ⊗ y) ∧ P v (─y)"..
then obtain v where v: "P v (x ⊗ y) ∧ P v (─y)"..
hence "P v (─y)"..
with ‹y ≠ u› have "¬ P v y"
by (rule complement_part_not_part)
moreover from v have "P v (x ⊗ y)"..
with ‹O x y› have "P v y" by (rule product_part_in_second_factor)
ultimately show "False"..
qed
qed
ultimately show "P ((─x) ⊕ (─y))(─(x ⊗ y))"..
qed

lemma product_complement_in_complements_sum:
"x ≠ u ⟹ y ≠ u ⟹ P(─(x ⊗ y))((─x) ⊕ (─y))"
proof -
assume "x ≠ u"
hence "x = ─(─x)"
by (rule complement_involution)
assume "y ≠ u"
hence "y = ─(─y)"
by (rule complement_involution)
show "P (─(x ⊗ y))((─x) ⊕ (─y))"
proof cases
assume "─x ⊕ ─y = u"
thus "P (─(x ⊗ y))((─x) ⊕ (─y))"
using universe_character by (rule ssubst)
next
assume "─x ⊕ ─y ≠ u"
hence "─x ⊕ ─y = ─(─(─x ⊕ ─ y))"
by (rule complement_involution)
moreover have "─(─x ⊕ ─y) = ─(─x) ⊗ ─(─y)"
using ‹─x ⊕ ─y ≠ u›
by (rule sum_complement_is_complements_product)
with ‹x = ─(─x)› have  "─(─x ⊕ ─y) = x ⊗ ─(─y)"
by (rule ssubst)
with ‹y = ─(─y)› have  "─(─x ⊕ ─y) = x ⊗ y"
by (rule ssubst)
hence "P (─(x ⊗ y))(─(─(─x ⊕ ─y)))"
using part_reflexivity by (rule subst)
ultimately show "P (─(x ⊗ y))(─x ⊕ ─y)"
by (rule ssubst)
qed
qed

theorem complement_of_product_is_sum_of_complements:
"O x y ⟹ x ⊕ y ≠ u ⟹ ─(x ⊗ y) = (─x) ⊕ (─y)"
proof -
assume "O x y"
assume "x ⊕ y ≠ u"
show "─(x ⊗ y) = (─x) ⊕ (─y)"
proof (rule part_antisymmetry)
have "x ≠ u" using ‹x ⊕ y ≠ u›
by (rule first_summand_not_universe)
have "y ≠ u" using ‹x ⊕ y ≠ u›
by (rule second_summand_not_universe)
show "P (─ (x ⊗ y)) (─ x ⊕ ─ y)"
using ‹x ≠ u› ‹y ≠ u› by (rule product_complement_in_complements_sum)
show " P (─ x ⊕ ─ y) (─ (x ⊗ y))"
using ‹O x y› ‹x ≠ u› ‹y ≠ u› by (rule complement_sum_in_product_complement)
qed
qed

end

(*<*) end (*>*)```